Metamath Proof Explorer

Theorem rec11

Description: Reciprocal is one-to-one. (Contributed by NM, 16-Sep-1999) (Revised by Mario Carneiro, 27-May-2016)

Ref Expression
Assertion rec11 
|- ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) ) -> ( ( 1 / A ) = ( 1 / B ) <-> A = B ) )

Proof

Step Hyp Ref Expression
1 1cnd 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) ) -> 1 e. CC )
2 reccl 
 |-  ( ( B e. CC /\ B =/= 0 ) -> ( 1 / B ) e. CC )
3 2 adantl 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) ) -> ( 1 / B ) e. CC )
4 simpl 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) ) -> ( A e. CC /\ A =/= 0 ) )
5 divmul 
 |-  ( ( 1 e. CC /\ ( 1 / B ) e. CC /\ ( A e. CC /\ A =/= 0 ) ) -> ( ( 1 / A ) = ( 1 / B ) <-> ( A x. ( 1 / B ) ) = 1 ) )
6 1 3 4 5 syl3anc 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) ) -> ( ( 1 / A ) = ( 1 / B ) <-> ( A x. ( 1 / B ) ) = 1 ) )
7 simpll 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) ) -> A e. CC )
8 simprl 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) ) -> B e. CC )
9 simprr 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) ) -> B =/= 0 )
10 divrec 
 |-  ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( A / B ) = ( A x. ( 1 / B ) ) )
11 7 8 9 10 syl3anc 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) ) -> ( A / B ) = ( A x. ( 1 / B ) ) )
12 11 eqeq1d 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) ) -> ( ( A / B ) = 1 <-> ( A x. ( 1 / B ) ) = 1 ) )
13 diveq1 
 |-  ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( ( A / B ) = 1 <-> A = B ) )
14 7 8 9 13 syl3anc 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) ) -> ( ( A / B ) = 1 <-> A = B ) )
15 6 12 14 3bitr2d 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) ) -> ( ( 1 / A ) = ( 1 / B ) <-> A = B ) )