Metamath Proof Explorer

Theorem axrrecex

Description: Existence of reciprocal of nonzero real number. Axiom 16 of 22 for real and complex numbers, derived from ZF set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-rrecex . (Contributed by NM, 15-May-1996) (New usage is discouraged.)

Ref Expression
Assertion axrrecex 
|- ( ( A e. RR /\ A =/= 0 ) -> E. x e. RR ( A x. x ) = 1 )

Proof

Step Hyp Ref Expression
1 elreal 
 |-  ( A e. RR <-> E. y e. R. <. y , 0R >. = A )
2 df-rex 
 |-  ( E. y e. R. <. y , 0R >. = A <-> E. y ( y e. R. /\ <. y , 0R >. = A ) )
3 1 2 bitri 
 |-  ( A e. RR <-> E. y ( y e. R. /\ <. y , 0R >. = A ) )
4 neeq1 
 |-  ( <. y , 0R >. = A -> ( <. y , 0R >. =/= 0 <-> A =/= 0 ) )
5 oveq1 
 |-  ( <. y , 0R >. = A -> ( <. y , 0R >. x. x ) = ( A x. x ) )
6 5 eqeq1d 
 |-  ( <. y , 0R >. = A -> ( ( <. y , 0R >. x. x ) = 1 <-> ( A x. x ) = 1 ) )
7 6 rexbidv 
 |-  ( <. y , 0R >. = A -> ( E. x e. RR ( <. y , 0R >. x. x ) = 1 <-> E. x e. RR ( A x. x ) = 1 ) )
8 4 7 imbi12d 
 |-  ( <. y , 0R >. = A -> ( ( <. y , 0R >. =/= 0 -> E. x e. RR ( <. y , 0R >. x. x ) = 1 ) <-> ( A =/= 0 -> E. x e. RR ( A x. x ) = 1 ) ) )
9 df-0 
 |-  0 = <. 0R , 0R >.
10 9 eqeq2i 
 |-  ( <. y , 0R >. = 0 <-> <. y , 0R >. = <. 0R , 0R >. )
11 vex 
 |-  y e. _V
12 11 eqresr 
 |-  ( <. y , 0R >. = <. 0R , 0R >. <-> y = 0R )
13 10 12 bitri 
 |-  ( <. y , 0R >. = 0 <-> y = 0R )
14 13 necon3bii 
 |-  ( <. y , 0R >. =/= 0 <-> y =/= 0R )
15 recexsr 
 |-  ( ( y e. R. /\ y =/= 0R ) -> E. z e. R. ( y .R z ) = 1R )
16 15 ex 
 |-  ( y e. R. -> ( y =/= 0R -> E. z e. R. ( y .R z ) = 1R ) )
17 opelreal 
 |-  ( <. z , 0R >. e. RR <-> z e. R. )
18 17 anbi1i 
 |-  ( ( <. z , 0R >. e. RR /\ ( <. y , 0R >. x. <. z , 0R >. ) = 1 ) <-> ( z e. R. /\ ( <. y , 0R >. x. <. z , 0R >. ) = 1 ) )
19 mulresr 
 |-  ( ( y e. R. /\ z e. R. ) -> ( <. y , 0R >. x. <. z , 0R >. ) = <. ( y .R z ) , 0R >. )
20 19 eqeq1d 
 |-  ( ( y e. R. /\ z e. R. ) -> ( ( <. y , 0R >. x. <. z , 0R >. ) = 1 <-> <. ( y .R z ) , 0R >. = 1 ) )
21 df-1 
 |-  1 = <. 1R , 0R >.
22 21 eqeq2i 
 |-  ( <. ( y .R z ) , 0R >. = 1 <-> <. ( y .R z ) , 0R >. = <. 1R , 0R >. )
23 ovex 
 |-  ( y .R z ) e. _V
24 23 eqresr 
 |-  ( <. ( y .R z ) , 0R >. = <. 1R , 0R >. <-> ( y .R z ) = 1R )
25 22 24 bitri 
 |-  ( <. ( y .R z ) , 0R >. = 1 <-> ( y .R z ) = 1R )
26 20 25 bitrdi 
 |-  ( ( y e. R. /\ z e. R. ) -> ( ( <. y , 0R >. x. <. z , 0R >. ) = 1 <-> ( y .R z ) = 1R ) )
27 26 pm5.32da 
 |-  ( y e. R. -> ( ( z e. R. /\ ( <. y , 0R >. x. <. z , 0R >. ) = 1 ) <-> ( z e. R. /\ ( y .R z ) = 1R ) ) )
28 18 27 syl5bb 
 |-  ( y e. R. -> ( ( <. z , 0R >. e. RR /\ ( <. y , 0R >. x. <. z , 0R >. ) = 1 ) <-> ( z e. R. /\ ( y .R z ) = 1R ) ) )
29 oveq2 
 |-  ( x = <. z , 0R >. -> ( <. y , 0R >. x. x ) = ( <. y , 0R >. x. <. z , 0R >. ) )
30 29 eqeq1d 
 |-  ( x = <. z , 0R >. -> ( ( <. y , 0R >. x. x ) = 1 <-> ( <. y , 0R >. x. <. z , 0R >. ) = 1 ) )
31 30 rspcev 
 |-  ( ( <. z , 0R >. e. RR /\ ( <. y , 0R >. x. <. z , 0R >. ) = 1 ) -> E. x e. RR ( <. y , 0R >. x. x ) = 1 )
32 28 31 syl6bir 
 |-  ( y e. R. -> ( ( z e. R. /\ ( y .R z ) = 1R ) -> E. x e. RR ( <. y , 0R >. x. x ) = 1 ) )
33 32 expd 
 |-  ( y e. R. -> ( z e. R. -> ( ( y .R z ) = 1R -> E. x e. RR ( <. y , 0R >. x. x ) = 1 ) ) )
34 33 rexlimdv 
 |-  ( y e. R. -> ( E. z e. R. ( y .R z ) = 1R -> E. x e. RR ( <. y , 0R >. x. x ) = 1 ) )
35 16 34 syld 
 |-  ( y e. R. -> ( y =/= 0R -> E. x e. RR ( <. y , 0R >. x. x ) = 1 ) )
36 14 35 syl5bi 
 |-  ( y e. R. -> ( <. y , 0R >. =/= 0 -> E. x e. RR ( <. y , 0R >. x. x ) = 1 ) )
37 3 8 36 gencl 
 |-  ( A e. RR -> ( A =/= 0 -> E. x e. RR ( A x. x ) = 1 ) )
38 37 imp 
 |-  ( ( A e. RR /\ A =/= 0 ) -> E. x e. RR ( A x. x ) = 1 )