Step |
Hyp |
Ref |
Expression |
1 |
|
0cn |
|- 0 e. CC |
2 |
|
divmul2 |
|- ( ( A e. CC /\ 0 e. CC /\ ( B e. CC /\ B =/= 0 ) ) -> ( ( A / B ) = 0 <-> A = ( B x. 0 ) ) ) |
3 |
1 2
|
mp3an2 |
|- ( ( A e. CC /\ ( B e. CC /\ B =/= 0 ) ) -> ( ( A / B ) = 0 <-> A = ( B x. 0 ) ) ) |
4 |
3
|
3impb |
|- ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( ( A / B ) = 0 <-> A = ( B x. 0 ) ) ) |
5 |
|
simp2 |
|- ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> B e. CC ) |
6 |
5
|
mul01d |
|- ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( B x. 0 ) = 0 ) |
7 |
6
|
eqeq2d |
|- ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( A = ( B x. 0 ) <-> A = 0 ) ) |
8 |
4 7
|
bitrd |
|- ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( ( A / B ) = 0 <-> A = 0 ) ) |