Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  recexpr Structured version   GIF version

Theorem recexpr 6610
 Description: The reciprocal of a positive real exists. Part of Proposition 9-3.7(v) of [Gleason] p. 124. (Contributed by NM, 15-May-1996.) (Revised by Mario Carneiro, 12-Jun-2013.)
Assertion
Ref Expression
recexpr (A Px P (A ·P x) = 1P)
Distinct variable group:   x,A

Proof of Theorem recexpr
Dummy variables u v w z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 breq12 3760 . . . . . . 7 ((z = u w = v) → (z <Q wu <Q v))
2 simpr 103 . . . . . . . . 9 ((z = u w = v) → w = v)
32fveq2d 5125 . . . . . . . 8 ((z = u w = v) → (*Qw) = (*Qv))
43eleq1d 2103 . . . . . . 7 ((z = u w = v) → ((*Qw) (2ndA) ↔ (*Qv) (2ndA)))
51, 4anbi12d 442 . . . . . 6 ((z = u w = v) → ((z <Q w (*Qw) (2ndA)) ↔ (u <Q v (*Qv) (2ndA))))
65cbvexdva 1801 . . . . 5 (z = u → (w(z <Q w (*Qw) (2ndA)) ↔ v(u <Q v (*Qv) (2ndA))))
76cbvabv 2158 . . . 4 {zw(z <Q w (*Qw) (2ndA))} = {uv(u <Q v (*Qv) (2ndA))}
8 simpl 102 . . . . . . . 8 ((z = u w = v) → z = u)
92, 8breq12d 3768 . . . . . . 7 ((z = u w = v) → (w <Q zv <Q u))
103eleq1d 2103 . . . . . . 7 ((z = u w = v) → ((*Qw) (1stA) ↔ (*Qv) (1stA)))
119, 10anbi12d 442 . . . . . 6 ((z = u w = v) → ((w <Q z (*Qw) (1stA)) ↔ (v <Q u (*Qv) (1stA))))
1211cbvexdva 1801 . . . . 5 (z = u → (w(w <Q z (*Qw) (1stA)) ↔ v(v <Q u (*Qv) (1stA))))
1312cbvabv 2158 . . . 4 {zw(w <Q z (*Qw) (1stA))} = {uv(v <Q u (*Qv) (1stA))}
147, 13opeq12i 3545 . . 3 ⟨{zw(z <Q w (*Qw) (2ndA))}, {zw(w <Q z (*Qw) (1stA))}⟩ = ⟨{uv(u <Q v (*Qv) (2ndA))}, {uv(v <Q u (*Qv) (1stA))}⟩
1514recexprlempr 6604 . 2 (A P → ⟨{zw(z <Q w (*Qw) (2ndA))}, {zw(w <Q z (*Qw) (1stA))}⟩ P)
1614recexprlemex 6609 . 2 (A P → (A ·P ⟨{zw(z <Q w (*Qw) (2ndA))}, {zw(w <Q z (*Qw) (1stA))}⟩) = 1P)
17 oveq2 5463 . . . 4 (x = ⟨{zw(z <Q w (*Qw) (2ndA))}, {zw(w <Q z (*Qw) (1stA))}⟩ → (A ·P x) = (A ·P ⟨{zw(z <Q w (*Qw) (2ndA))}, {zw(w <Q z (*Qw) (1stA))}⟩))
1817eqeq1d 2045 . . 3 (x = ⟨{zw(z <Q w (*Qw) (2ndA))}, {zw(w <Q z (*Qw) (1stA))}⟩ → ((A ·P x) = 1P ↔ (A ·P ⟨{zw(z <Q w (*Qw) (2ndA))}, {zw(w <Q z (*Qw) (1stA))}⟩) = 1P))
1918rspcev 2650 . 2 ((⟨{zw(z <Q w (*Qw) (2ndA))}, {zw(w <Q z (*Qw) (1stA))}⟩ P (A ·P ⟨{zw(z <Q w (*Qw) (2ndA))}, {zw(w <Q z (*Qw) (1stA))}⟩) = 1P) → x P (A ·P x) = 1P)
2015, 16, 19syl2anc 391 1 (A Px P (A ·P x) = 1P)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 97   = wceq 1242  ∃wex 1378   ∈ wcel 1390  {cab 2023  ∃wrex 2301  ⟨cop 3370   class class class wbr 3755  ‘cfv 4845  (class class class)co 5455  1st c1st 5707  2nd c2nd 5708  *Qcrq 6268
 Copyright terms: Public domain W3C validator