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 ) )