Metamath Proof Explorer

Theorem xreceu

Description: Existential uniqueness of reciprocals. Theorem I.8 of Apostol p. 18. (Contributed by Thierry Arnoux, 17-Dec-2016)

Ref Expression
Assertion xreceu 
|- ( ( A e. RR* /\ B e. RR /\ B =/= 0 ) -> E! x e. RR* ( B *e x ) = A )

Proof

Step Hyp Ref Expression
1 ressxr 
 |-  RR C_ RR*
2 xrecex 
 |-  ( ( B e. RR /\ B =/= 0 ) -> E. y e. RR ( B *e y ) = 1 )
3 2 3adant1 
 |-  ( ( A e. RR* /\ B e. RR /\ B =/= 0 ) -> E. y e. RR ( B *e y ) = 1 )
4 ssrexv 
 |-  ( RR C_ RR* -> ( E. y e. RR ( B *e y ) = 1 -> E. y e. RR* ( B *e y ) = 1 ) )
5 1 3 4 mpsyl 
 |-  ( ( A e. RR* /\ B e. RR /\ B =/= 0 ) -> E. y e. RR* ( B *e y ) = 1 )
6 simprl 
 |-  ( ( ( A e. RR* /\ B e. RR ) /\ ( y e. RR* /\ ( B *e y ) = 1 ) ) -> y e. RR* )
7 simpll 
 |-  ( ( ( A e. RR* /\ B e. RR ) /\ ( y e. RR* /\ ( B *e y ) = 1 ) ) -> A e. RR* )
8 6 7 xmulcld 
 |-  ( ( ( A e. RR* /\ B e. RR ) /\ ( y e. RR* /\ ( B *e y ) = 1 ) ) -> ( y *e A ) e. RR* )
9 oveq1 
 |-  ( ( B *e y ) = 1 -> ( ( B *e y ) *e A ) = ( 1 *e A ) )
10 9 ad2antll 
 |-  ( ( ( A e. RR* /\ B e. RR ) /\ ( y e. RR* /\ ( B *e y ) = 1 ) ) -> ( ( B *e y ) *e A ) = ( 1 *e A ) )
11 simplr 
 |-  ( ( ( A e. RR* /\ B e. RR ) /\ ( y e. RR* /\ ( B *e y ) = 1 ) ) -> B e. RR )
12 11 rexrd 
 |-  ( ( ( A e. RR* /\ B e. RR ) /\ ( y e. RR* /\ ( B *e y ) = 1 ) ) -> B e. RR* )
13 xmulass 
 |-  ( ( B e. RR* /\ y e. RR* /\ A e. RR* ) -> ( ( B *e y ) *e A ) = ( B *e ( y *e A ) ) )
14 12 6 7 13 syl3anc 
 |-  ( ( ( A e. RR* /\ B e. RR ) /\ ( y e. RR* /\ ( B *e y ) = 1 ) ) -> ( ( B *e y ) *e A ) = ( B *e ( y *e A ) ) )
15 xmulid2 
 |-  ( A e. RR* -> ( 1 *e A ) = A )
16 7 15 syl 
 |-  ( ( ( A e. RR* /\ B e. RR ) /\ ( y e. RR* /\ ( B *e y ) = 1 ) ) -> ( 1 *e A ) = A )
17 10 14 16 3eqtr3d 
 |-  ( ( ( A e. RR* /\ B e. RR ) /\ ( y e. RR* /\ ( B *e y ) = 1 ) ) -> ( B *e ( y *e A ) ) = A )
18 oveq2 
 |-  ( x = ( y *e A ) -> ( B *e x ) = ( B *e ( y *e A ) ) )
19 18 eqeq1d 
 |-  ( x = ( y *e A ) -> ( ( B *e x ) = A <-> ( B *e ( y *e A ) ) = A ) )
20 19 rspcev 
 |-  ( ( ( y *e A ) e. RR* /\ ( B *e ( y *e A ) ) = A ) -> E. x e. RR* ( B *e x ) = A )
21 8 17 20 syl2anc 
 |-  ( ( ( A e. RR* /\ B e. RR ) /\ ( y e. RR* /\ ( B *e y ) = 1 ) ) -> E. x e. RR* ( B *e x ) = A )
22 21 rexlimdvaa 
 |-  ( ( A e. RR* /\ B e. RR ) -> ( E. y e. RR* ( B *e y ) = 1 -> E. x e. RR* ( B *e x ) = A ) )
23 22 3adant3 
 |-  ( ( A e. RR* /\ B e. RR /\ B =/= 0 ) -> ( E. y e. RR* ( B *e y ) = 1 -> E. x e. RR* ( B *e x ) = A ) )
24 5 23 mpd 
 |-  ( ( A e. RR* /\ B e. RR /\ B =/= 0 ) -> E. x e. RR* ( B *e x ) = A )
25 eqtr3 
 |-  ( ( ( B *e x ) = A /\ ( B *e y ) = A ) -> ( B *e x ) = ( B *e y ) )
26 simp1 
 |-  ( ( x e. RR* /\ y e. RR* /\ ( B e. RR /\ B =/= 0 ) ) -> x e. RR* )
27 simp2 
 |-  ( ( x e. RR* /\ y e. RR* /\ ( B e. RR /\ B =/= 0 ) ) -> y e. RR* )
28 simp3l 
 |-  ( ( x e. RR* /\ y e. RR* /\ ( B e. RR /\ B =/= 0 ) ) -> B e. RR )
29 simp3r 
 |-  ( ( x e. RR* /\ y e. RR* /\ ( B e. RR /\ B =/= 0 ) ) -> B =/= 0 )
30 26 27 28 29 xmulcand 
 |-  ( ( x e. RR* /\ y e. RR* /\ ( B e. RR /\ B =/= 0 ) ) -> ( ( B *e x ) = ( B *e y ) <-> x = y ) )
31 25 30 syl5ib 
 |-  ( ( x e. RR* /\ y e. RR* /\ ( B e. RR /\ B =/= 0 ) ) -> ( ( ( B *e x ) = A /\ ( B *e y ) = A ) -> x = y ) )
32 31 3expa 
 |-  ( ( ( x e. RR* /\ y e. RR* ) /\ ( B e. RR /\ B =/= 0 ) ) -> ( ( ( B *e x ) = A /\ ( B *e y ) = A ) -> x = y ) )
33 32 expcom 
 |-  ( ( B e. RR /\ B =/= 0 ) -> ( ( x e. RR* /\ y e. RR* ) -> ( ( ( B *e x ) = A /\ ( B *e y ) = A ) -> x = y ) ) )
34 33 3adant1 
 |-  ( ( A e. RR* /\ B e. RR /\ B =/= 0 ) -> ( ( x e. RR* /\ y e. RR* ) -> ( ( ( B *e x ) = A /\ ( B *e y ) = A ) -> x = y ) ) )
35 34 ralrimivv 
 |-  ( ( A e. RR* /\ B e. RR /\ B =/= 0 ) -> A. x e. RR* A. y e. RR* ( ( ( B *e x ) = A /\ ( B *e y ) = A ) -> x = y ) )
36 oveq2 
 |-  ( x = y -> ( B *e x ) = ( B *e y ) )
37 36 eqeq1d 
 |-  ( x = y -> ( ( B *e x ) = A <-> ( B *e y ) = A ) )
38 37 reu4 
 |-  ( E! x e. RR* ( B *e x ) = A <-> ( E. x e. RR* ( B *e x ) = A /\ A. x e. RR* A. y e. RR* ( ( ( B *e x ) = A /\ ( B *e y ) = A ) -> x = y ) ) )
39 24 35 38 sylanbrc 
 |-  ( ( A e. RR* /\ B e. RR /\ B =/= 0 ) -> E! x e. RR* ( B *e x ) = A )