Metamath Proof Explorer

Theorem rec11r

Description: Mutual reciprocals. (Contributed by Paul Chapman, 18-Oct-2007)

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

Proof

Step Hyp Ref Expression
1 1cnd 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) ) -> 1 e. CC )
2 simprl 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) ) -> B e. CC )
3 simpll 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) ) -> A e. CC )
4 simplr 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) ) -> A =/= 0 )
5 divmul2 
 |-  ( ( 1 e. CC /\ B e. CC /\ ( A e. CC /\ A =/= 0 ) ) -> ( ( 1 / A ) = B <-> 1 = ( A x. B ) ) )
6 1 2 3 4 5 syl112anc 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) ) -> ( ( 1 / A ) = B <-> 1 = ( A x. B ) ) )
7 simprr 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) ) -> B =/= 0 )
8 divmul3 
 |-  ( ( 1 e. CC /\ A e. CC /\ ( B e. CC /\ B =/= 0 ) ) -> ( ( 1 / B ) = A <-> 1 = ( A x. B ) ) )
9 1 3 2 7 8 syl112anc 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) ) -> ( ( 1 / B ) = A <-> 1 = ( A x. B ) ) )
10 6 9 bitr4d 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) ) -> ( ( 1 / A ) = B <-> ( 1 / B ) = A ) )