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