Metamath Proof Explorer

Theorem recexsrlem

Description: The reciprocal of a positive signed real exists. Part of Proposition 9-4.3 of Gleason p. 126. (Contributed by NM, 15-May-1996) (New usage is discouraged.)

Ref Expression
Assertion recexsrlem 
|- ( 0R  E. x e. R. ( A .R x ) = 1R )

Proof

Step Hyp Ref Expression
1 ltrelsr 
 |-
2 1 brel 
 |-  ( 0R  ( 0R e. R. /\ A e. R. ) )
3 2 simprd 
 |-  ( 0R  A e. R. )
4 df-nr 
 |-  R. = ( ( P. X. P. ) /. ~R )
5 breq2 
 |-  ( [ <. y , z >. ] ~R = A -> ( 0R . ] ~R <-> 0R
6 oveq1 
 |-  ( [ <. y , z >. ] ~R = A -> ( [ <. y , z >. ] ~R .R x ) = ( A .R x ) )
7 6 eqeq1d 
 |-  ( [ <. y , z >. ] ~R = A -> ( ( [ <. y , z >. ] ~R .R x ) = 1R <-> ( A .R x ) = 1R ) )
8 7 rexbidv 
 |-  ( [ <. y , z >. ] ~R = A -> ( E. x e. R. ( [ <. y , z >. ] ~R .R x ) = 1R <-> E. x e. R. ( A .R x ) = 1R ) )
9 5 8 imbi12d 
 |-  ( [ <. y , z >. ] ~R = A -> ( ( 0R . ] ~R -> E. x e. R. ( [ <. y , z >. ] ~R .R x ) = 1R ) <-> ( 0R  E. x e. R. ( A .R x ) = 1R ) ) )
10 gt0srpr 
 |-  ( 0R . ] ~R <-> z
11 ltexpri 
 |-  ( z 
 E. w e. P. ( z +P. w ) = y )
12 10 11 sylbi 
 |-  ( 0R . ] ~R -> E. w e. P. ( z +P. w ) = y )
13 recexpr 
 |-  ( w e. P. -> E. v e. P. ( w .P. v ) = 1P )
14 1pr 
 |-  1P e. P.
15 addclpr 
 |-  ( ( v e. P. /\ 1P e. P. ) -> ( v +P. 1P ) e. P. )
16 14 15 mpan2 
 |-  ( v e. P. -> ( v +P. 1P ) e. P. )
17 enrex 
 |-  ~R e. _V
18 17 4 ecopqsi 
 |-  ( ( ( v +P. 1P ) e. P. /\ 1P e. P. ) -> [ <. ( v +P. 1P ) , 1P >. ] ~R e. R. )
19 16 14 18 sylancl 
 |-  ( v e. P. -> [ <. ( v +P. 1P ) , 1P >. ] ~R e. R. )
20 19 ad2antlr 
 |-  ( ( ( ( y e. P. /\ z e. P. ) /\ v e. P. ) /\ ( ( w .P. v ) = 1P /\ ( z +P. w ) = y ) ) -> [ <. ( v +P. 1P ) , 1P >. ] ~R e. R. )
21 16 14 jctir 
 |-  ( v e. P. -> ( ( v +P. 1P ) e. P. /\ 1P e. P. ) )
22 21 anim2i 
 |-  ( ( ( y e. P. /\ z e. P. ) /\ v e. P. ) -> ( ( y e. P. /\ z e. P. ) /\ ( ( v +P. 1P ) e. P. /\ 1P e. P. ) ) )
23 22 adantr 
 |-  ( ( ( ( y e. P. /\ z e. P. ) /\ v e. P. ) /\ ( ( w .P. v ) = 1P /\ ( z +P. w ) = y ) ) -> ( ( y e. P. /\ z e. P. ) /\ ( ( v +P. 1P ) e. P. /\ 1P e. P. ) ) )
24 mulsrpr 
 |-  ( ( ( y e. P. /\ z e. P. ) /\ ( ( v +P. 1P ) e. P. /\ 1P e. P. ) ) -> ( [ <. y , z >. ] ~R .R [ <. ( v +P. 1P ) , 1P >. ] ~R ) = [ <. ( ( y .P. ( v +P. 1P ) ) +P. ( z .P. 1P ) ) , ( ( y .P. 1P ) +P. ( z .P. ( v +P. 1P ) ) ) >. ] ~R )
25 23 24 syl 
 |-  ( ( ( ( y e. P. /\ z e. P. ) /\ v e. P. ) /\ ( ( w .P. v ) = 1P /\ ( z +P. w ) = y ) ) -> ( [ <. y , z >. ] ~R .R [ <. ( v +P. 1P ) , 1P >. ] ~R ) = [ <. ( ( y .P. ( v +P. 1P ) ) +P. ( z .P. 1P ) ) , ( ( y .P. 1P ) +P. ( z .P. ( v +P. 1P ) ) ) >. ] ~R )
26 oveq1 
 |-  ( ( z +P. w ) = y -> ( ( z +P. w ) .P. v ) = ( y .P. v ) )
27 26 eqcomd 
 |-  ( ( z +P. w ) = y -> ( y .P. v ) = ( ( z +P. w ) .P. v ) )
28 vex 
 |-  z e. _V
29 vex 
 |-  w e. _V
30 vex 
 |-  v e. _V
31 mulcompr 
 |-  ( u .P. f ) = ( f .P. u )
32 distrpr 
 |-  ( u .P. ( f +P. x ) ) = ( ( u .P. f ) +P. ( u .P. x ) )
33 28 29 30 31 32 caovdir 
 |-  ( ( z +P. w ) .P. v ) = ( ( z .P. v ) +P. ( w .P. v ) )
34 oveq2 
 |-  ( ( w .P. v ) = 1P -> ( ( z .P. v ) +P. ( w .P. v ) ) = ( ( z .P. v ) +P. 1P ) )
35 33 34 syl5eq 
 |-  ( ( w .P. v ) = 1P -> ( ( z +P. w ) .P. v ) = ( ( z .P. v ) +P. 1P ) )
36 27 35 sylan9eqr 
 |-  ( ( ( w .P. v ) = 1P /\ ( z +P. w ) = y ) -> ( y .P. v ) = ( ( z .P. v ) +P. 1P ) )
37 36 oveq1d 
 |-  ( ( ( w .P. v ) = 1P /\ ( z +P. w ) = y ) -> ( ( y .P. v ) +P. ( ( y .P. 1P ) +P. ( z .P. 1P ) ) ) = ( ( ( z .P. v ) +P. 1P ) +P. ( ( y .P. 1P ) +P. ( z .P. 1P ) ) ) )
38 ovex 
 |-  ( z .P. v ) e. _V
39 14 elexi 
 |-  1P e. _V
40 ovex 
 |-  ( ( y .P. 1P ) +P. ( z .P. 1P ) ) e. _V
41 addcompr 
 |-  ( u +P. f ) = ( f +P. u )
42 addasspr 
 |-  ( ( u +P. f ) +P. x ) = ( u +P. ( f +P. x ) )
43 38 39 40 41 42 caov32 
 |-  ( ( ( z .P. v ) +P. 1P ) +P. ( ( y .P. 1P ) +P. ( z .P. 1P ) ) ) = ( ( ( z .P. v ) +P. ( ( y .P. 1P ) +P. ( z .P. 1P ) ) ) +P. 1P )
44 37 43 eqtrdi 
 |-  ( ( ( w .P. v ) = 1P /\ ( z +P. w ) = y ) -> ( ( y .P. v ) +P. ( ( y .P. 1P ) +P. ( z .P. 1P ) ) ) = ( ( ( z .P. v ) +P. ( ( y .P. 1P ) +P. ( z .P. 1P ) ) ) +P. 1P ) )
45 44 oveq1d 
 |-  ( ( ( w .P. v ) = 1P /\ ( z +P. w ) = y ) -> ( ( ( y .P. v ) +P. ( ( y .P. 1P ) +P. ( z .P. 1P ) ) ) +P. 1P ) = ( ( ( ( z .P. v ) +P. ( ( y .P. 1P ) +P. ( z .P. 1P ) ) ) +P. 1P ) +P. 1P ) )
46 addasspr 
 |-  ( ( ( ( z .P. v ) +P. ( ( y .P. 1P ) +P. ( z .P. 1P ) ) ) +P. 1P ) +P. 1P ) = ( ( ( z .P. v ) +P. ( ( y .P. 1P ) +P. ( z .P. 1P ) ) ) +P. ( 1P +P. 1P ) )
47 45 46 eqtrdi 
 |-  ( ( ( w .P. v ) = 1P /\ ( z +P. w ) = y ) -> ( ( ( y .P. v ) +P. ( ( y .P. 1P ) +P. ( z .P. 1P ) ) ) +P. 1P ) = ( ( ( z .P. v ) +P. ( ( y .P. 1P ) +P. ( z .P. 1P ) ) ) +P. ( 1P +P. 1P ) ) )
48 distrpr 
 |-  ( y .P. ( v +P. 1P ) ) = ( ( y .P. v ) +P. ( y .P. 1P ) )
49 48 oveq1i 
 |-  ( ( y .P. ( v +P. 1P ) ) +P. ( z .P. 1P ) ) = ( ( ( y .P. v ) +P. ( y .P. 1P ) ) +P. ( z .P. 1P ) )
50 addasspr 
 |-  ( ( ( y .P. v ) +P. ( y .P. 1P ) ) +P. ( z .P. 1P ) ) = ( ( y .P. v ) +P. ( ( y .P. 1P ) +P. ( z .P. 1P ) ) )
51 49 50 eqtri 
 |-  ( ( y .P. ( v +P. 1P ) ) +P. ( z .P. 1P ) ) = ( ( y .P. v ) +P. ( ( y .P. 1P ) +P. ( z .P. 1P ) ) )
52 51 oveq1i 
 |-  ( ( ( y .P. ( v +P. 1P ) ) +P. ( z .P. 1P ) ) +P. 1P ) = ( ( ( y .P. v ) +P. ( ( y .P. 1P ) +P. ( z .P. 1P ) ) ) +P. 1P )
53 distrpr 
 |-  ( z .P. ( v +P. 1P ) ) = ( ( z .P. v ) +P. ( z .P. 1P ) )
54 53 oveq2i 
 |-  ( ( y .P. 1P ) +P. ( z .P. ( v +P. 1P ) ) ) = ( ( y .P. 1P ) +P. ( ( z .P. v ) +P. ( z .P. 1P ) ) )
55 ovex 
 |-  ( y .P. 1P ) e. _V
56 ovex 
 |-  ( z .P. 1P ) e. _V
57 55 38 56 41 42 caov12 
 |-  ( ( y .P. 1P ) +P. ( ( z .P. v ) +P. ( z .P. 1P ) ) ) = ( ( z .P. v ) +P. ( ( y .P. 1P ) +P. ( z .P. 1P ) ) )
58 54 57 eqtri 
 |-  ( ( y .P. 1P ) +P. ( z .P. ( v +P. 1P ) ) ) = ( ( z .P. v ) +P. ( ( y .P. 1P ) +P. ( z .P. 1P ) ) )
59 58 oveq1i 
 |-  ( ( ( y .P. 1P ) +P. ( z .P. ( v +P. 1P ) ) ) +P. ( 1P +P. 1P ) ) = ( ( ( z .P. v ) +P. ( ( y .P. 1P ) +P. ( z .P. 1P ) ) ) +P. ( 1P +P. 1P ) )
60 47 52 59 3eqtr4g 
 |-  ( ( ( w .P. v ) = 1P /\ ( z +P. w ) = y ) -> ( ( ( y .P. ( v +P. 1P ) ) +P. ( z .P. 1P ) ) +P. 1P ) = ( ( ( y .P. 1P ) +P. ( z .P. ( v +P. 1P ) ) ) +P. ( 1P +P. 1P ) ) )
61 mulclpr 
 |-  ( ( y e. P. /\ ( v +P. 1P ) e. P. ) -> ( y .P. ( v +P. 1P ) ) e. P. )
62 16 61 sylan2 
 |-  ( ( y e. P. /\ v e. P. ) -> ( y .P. ( v +P. 1P ) ) e. P. )
63 mulclpr 
 |-  ( ( z e. P. /\ 1P e. P. ) -> ( z .P. 1P ) e. P. )
64 14 63 mpan2 
 |-  ( z e. P. -> ( z .P. 1P ) e. P. )
65 addclpr 
 |-  ( ( ( y .P. ( v +P. 1P ) ) e. P. /\ ( z .P. 1P ) e. P. ) -> ( ( y .P. ( v +P. 1P ) ) +P. ( z .P. 1P ) ) e. P. )
66 62 64 65 syl2an 
 |-  ( ( ( y e. P. /\ v e. P. ) /\ z e. P. ) -> ( ( y .P. ( v +P. 1P ) ) +P. ( z .P. 1P ) ) e. P. )
67 66 an32s 
 |-  ( ( ( y e. P. /\ z e. P. ) /\ v e. P. ) -> ( ( y .P. ( v +P. 1P ) ) +P. ( z .P. 1P ) ) e. P. )
68 mulclpr 
 |-  ( ( y e. P. /\ 1P e. P. ) -> ( y .P. 1P ) e. P. )
69 14 68 mpan2 
 |-  ( y e. P. -> ( y .P. 1P ) e. P. )
70 mulclpr 
 |-  ( ( z e. P. /\ ( v +P. 1P ) e. P. ) -> ( z .P. ( v +P. 1P ) ) e. P. )
71 16 70 sylan2 
 |-  ( ( z e. P. /\ v e. P. ) -> ( z .P. ( v +P. 1P ) ) e. P. )
72 addclpr 
 |-  ( ( ( y .P. 1P ) e. P. /\ ( z .P. ( v +P. 1P ) ) e. P. ) -> ( ( y .P. 1P ) +P. ( z .P. ( v +P. 1P ) ) ) e. P. )
73 69 71 72 syl2an 
 |-  ( ( y e. P. /\ ( z e. P. /\ v e. P. ) ) -> ( ( y .P. 1P ) +P. ( z .P. ( v +P. 1P ) ) ) e. P. )
74 73 anassrs 
 |-  ( ( ( y e. P. /\ z e. P. ) /\ v e. P. ) -> ( ( y .P. 1P ) +P. ( z .P. ( v +P. 1P ) ) ) e. P. )
75 67 74 jca 
 |-  ( ( ( y e. P. /\ z e. P. ) /\ v e. P. ) -> ( ( ( y .P. ( v +P. 1P ) ) +P. ( z .P. 1P ) ) e. P. /\ ( ( y .P. 1P ) +P. ( z .P. ( v +P. 1P ) ) ) e. P. ) )
76 addclpr 
 |-  ( ( 1P e. P. /\ 1P e. P. ) -> ( 1P +P. 1P ) e. P. )
77 14 14 76 mp2an 
 |-  ( 1P +P. 1P ) e. P.
78 77 14 pm3.2i 
 |-  ( ( 1P +P. 1P ) e. P. /\ 1P e. P. )
79 enreceq 
 |-  ( ( ( ( ( y .P. ( v +P. 1P ) ) +P. ( z .P. 1P ) ) e. P. /\ ( ( y .P. 1P ) +P. ( z .P. ( v +P. 1P ) ) ) e. P. ) /\ ( ( 1P +P. 1P ) e. P. /\ 1P e. P. ) ) -> ( [ <. ( ( y .P. ( v +P. 1P ) ) +P. ( z .P. 1P ) ) , ( ( y .P. 1P ) +P. ( z .P. ( v +P. 1P ) ) ) >. ] ~R = [ <. ( 1P +P. 1P ) , 1P >. ] ~R <-> ( ( ( y .P. ( v +P. 1P ) ) +P. ( z .P. 1P ) ) +P. 1P ) = ( ( ( y .P. 1P ) +P. ( z .P. ( v +P. 1P ) ) ) +P. ( 1P +P. 1P ) ) ) )
80 75 78 79 sylancl 
 |-  ( ( ( y e. P. /\ z e. P. ) /\ v e. P. ) -> ( [ <. ( ( y .P. ( v +P. 1P ) ) +P. ( z .P. 1P ) ) , ( ( y .P. 1P ) +P. ( z .P. ( v +P. 1P ) ) ) >. ] ~R = [ <. ( 1P +P. 1P ) , 1P >. ] ~R <-> ( ( ( y .P. ( v +P. 1P ) ) +P. ( z .P. 1P ) ) +P. 1P ) = ( ( ( y .P. 1P ) +P. ( z .P. ( v +P. 1P ) ) ) +P. ( 1P +P. 1P ) ) ) )
81 60 80 syl5ibr 
 |-  ( ( ( y e. P. /\ z e. P. ) /\ v e. P. ) -> ( ( ( w .P. v ) = 1P /\ ( z +P. w ) = y ) -> [ <. ( ( y .P. ( v +P. 1P ) ) +P. ( z .P. 1P ) ) , ( ( y .P. 1P ) +P. ( z .P. ( v +P. 1P ) ) ) >. ] ~R = [ <. ( 1P +P. 1P ) , 1P >. ] ~R ) )
82 81 imp 
 |-  ( ( ( ( y e. P. /\ z e. P. ) /\ v e. P. ) /\ ( ( w .P. v ) = 1P /\ ( z +P. w ) = y ) ) -> [ <. ( ( y .P. ( v +P. 1P ) ) +P. ( z .P. 1P ) ) , ( ( y .P. 1P ) +P. ( z .P. ( v +P. 1P ) ) ) >. ] ~R = [ <. ( 1P +P. 1P ) , 1P >. ] ~R )
83 25 82 eqtrd 
 |-  ( ( ( ( y e. P. /\ z e. P. ) /\ v e. P. ) /\ ( ( w .P. v ) = 1P /\ ( z +P. w ) = y ) ) -> ( [ <. y , z >. ] ~R .R [ <. ( v +P. 1P ) , 1P >. ] ~R ) = [ <. ( 1P +P. 1P ) , 1P >. ] ~R )
84 df-1r 
 |-  1R = [ <. ( 1P +P. 1P ) , 1P >. ] ~R
85 83 84 eqtr4di 
 |-  ( ( ( ( y e. P. /\ z e. P. ) /\ v e. P. ) /\ ( ( w .P. v ) = 1P /\ ( z +P. w ) = y ) ) -> ( [ <. y , z >. ] ~R .R [ <. ( v +P. 1P ) , 1P >. ] ~R ) = 1R )
86 oveq2 
 |-  ( x = [ <. ( v +P. 1P ) , 1P >. ] ~R -> ( [ <. y , z >. ] ~R .R x ) = ( [ <. y , z >. ] ~R .R [ <. ( v +P. 1P ) , 1P >. ] ~R ) )
87 86 eqeq1d 
 |-  ( x = [ <. ( v +P. 1P ) , 1P >. ] ~R -> ( ( [ <. y , z >. ] ~R .R x ) = 1R <-> ( [ <. y , z >. ] ~R .R [ <. ( v +P. 1P ) , 1P >. ] ~R ) = 1R ) )
88 87 rspcev 
 |-  ( ( [ <. ( v +P. 1P ) , 1P >. ] ~R e. R. /\ ( [ <. y , z >. ] ~R .R [ <. ( v +P. 1P ) , 1P >. ] ~R ) = 1R ) -> E. x e. R. ( [ <. y , z >. ] ~R .R x ) = 1R )
89 20 85 88 syl2anc 
 |-  ( ( ( ( y e. P. /\ z e. P. ) /\ v e. P. ) /\ ( ( w .P. v ) = 1P /\ ( z +P. w ) = y ) ) -> E. x e. R. ( [ <. y , z >. ] ~R .R x ) = 1R )
90 89 exp43 
 |-  ( ( y e. P. /\ z e. P. ) -> ( v e. P. -> ( ( w .P. v ) = 1P -> ( ( z +P. w ) = y -> E. x e. R. ( [ <. y , z >. ] ~R .R x ) = 1R ) ) ) )
91 90 rexlimdv 
 |-  ( ( y e. P. /\ z e. P. ) -> ( E. v e. P. ( w .P. v ) = 1P -> ( ( z +P. w ) = y -> E. x e. R. ( [ <. y , z >. ] ~R .R x ) = 1R ) ) )
92 13 91 syl5 
 |-  ( ( y e. P. /\ z e. P. ) -> ( w e. P. -> ( ( z +P. w ) = y -> E. x e. R. ( [ <. y , z >. ] ~R .R x ) = 1R ) ) )
93 92 rexlimdv 
 |-  ( ( y e. P. /\ z e. P. ) -> ( E. w e. P. ( z +P. w ) = y -> E. x e. R. ( [ <. y , z >. ] ~R .R x ) = 1R ) )
94 12 93 syl5 
 |-  ( ( y e. P. /\ z e. P. ) -> ( 0R . ] ~R -> E. x e. R. ( [ <. y , z >. ] ~R .R x ) = 1R ) )
95 4 9 94 ecoptocl 
 |-  ( A e. R. -> ( 0R  E. x e. R. ( A .R x ) = 1R ) )
96 3 95 mpcom 
 |-  ( 0R  E. x e. R. ( A .R x ) = 1R )