Metamath Proof Explorer

Theorem receu

Description: Existential uniqueness of reciprocals. Theorem I.8 of Apostol p. 18. (Contributed by NM, 29-Jan-1995) (Revised by Mario Carneiro, 17-Feb-2014)

Ref Expression
Assertion receu 
|- ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> E! x e. CC ( B x. x ) = A )

Proof

Step Hyp Ref Expression
1 recex 
 |-  ( ( B e. CC /\ B =/= 0 ) -> E. y e. CC ( B x. y ) = 1 )
2 1 3adant1 
 |-  ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> E. y e. CC ( B x. y ) = 1 )
3 simprl 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( y e. CC /\ ( B x. y ) = 1 ) ) -> y e. CC )
4 simpll 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( y e. CC /\ ( B x. y ) = 1 ) ) -> A e. CC )
5 3 4 mulcld 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( y e. CC /\ ( B x. y ) = 1 ) ) -> ( y x. A ) e. CC )
6 oveq1 
 |-  ( ( B x. y ) = 1 -> ( ( B x. y ) x. A ) = ( 1 x. A ) )
7 6 ad2antll 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( y e. CC /\ ( B x. y ) = 1 ) ) -> ( ( B x. y ) x. A ) = ( 1 x. A ) )
8 simplr 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( y e. CC /\ ( B x. y ) = 1 ) ) -> B e. CC )
9 8 3 4 mulassd 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( y e. CC /\ ( B x. y ) = 1 ) ) -> ( ( B x. y ) x. A ) = ( B x. ( y x. A ) ) )
10 4 mullidd 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( y e. CC /\ ( B x. y ) = 1 ) ) -> ( 1 x. A ) = A )
11 7 9 10 3eqtr3d 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( y e. CC /\ ( B x. y ) = 1 ) ) -> ( B x. ( y x. A ) ) = A )
12 oveq2 
 |-  ( x = ( y x. A ) -> ( B x. x ) = ( B x. ( y x. A ) ) )
13 12 eqeq1d 
 |-  ( x = ( y x. A ) -> ( ( B x. x ) = A <-> ( B x. ( y x. A ) ) = A ) )
14 13 rspcev 
 |-  ( ( ( y x. A ) e. CC /\ ( B x. ( y x. A ) ) = A ) -> E. x e. CC ( B x. x ) = A )
15 5 11 14 syl2anc 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( y e. CC /\ ( B x. y ) = 1 ) ) -> E. x e. CC ( B x. x ) = A )
16 15 rexlimdvaa 
 |-  ( ( A e. CC /\ B e. CC ) -> ( E. y e. CC ( B x. y ) = 1 -> E. x e. CC ( B x. x ) = A ) )
17 16 3adant3 
 |-  ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( E. y e. CC ( B x. y ) = 1 -> E. x e. CC ( B x. x ) = A ) )
18 2 17 mpd 
 |-  ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> E. x e. CC ( B x. x ) = A )
19 eqtr3 
 |-  ( ( ( B x. x ) = A /\ ( B x. y ) = A ) -> ( B x. x ) = ( B x. y ) )
20 mulcan 
 |-  ( ( x e. CC /\ y e. CC /\ ( B e. CC /\ B =/= 0 ) ) -> ( ( B x. x ) = ( B x. y ) <-> x = y ) )
21 19 20 imbitrid 
 |-  ( ( x e. CC /\ y e. CC /\ ( B e. CC /\ B =/= 0 ) ) -> ( ( ( B x. x ) = A /\ ( B x. y ) = A ) -> x = y ) )
22 21 3expa 
 |-  ( ( ( x e. CC /\ y e. CC ) /\ ( B e. CC /\ B =/= 0 ) ) -> ( ( ( B x. x ) = A /\ ( B x. y ) = A ) -> x = y ) )
23 22 expcom 
 |-  ( ( B e. CC /\ B =/= 0 ) -> ( ( x e. CC /\ y e. CC ) -> ( ( ( B x. x ) = A /\ ( B x. y ) = A ) -> x = y ) ) )
24 23 3adant1 
 |-  ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( ( x e. CC /\ y e. CC ) -> ( ( ( B x. x ) = A /\ ( B x. y ) = A ) -> x = y ) ) )
25 24 ralrimivv 
 |-  ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> A. x e. CC A. y e. CC ( ( ( B x. x ) = A /\ ( B x. y ) = A ) -> x = y ) )
26 oveq2 
 |-  ( x = y -> ( B x. x ) = ( B x. y ) )
27 26 eqeq1d 
 |-  ( x = y -> ( ( B x. x ) = A <-> ( B x. y ) = A ) )
28 27 reu4 
 |-  ( E! x e. CC ( B x. x ) = A <-> ( E. x e. CC ( B x. x ) = A /\ A. x e. CC A. y e. CC ( ( ( B x. x ) = A /\ ( B x. y ) = A ) -> x = y ) ) )
29 18 25 28 sylanbrc 
 |-  ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> E! x e. CC ( B x. x ) = A )