Step |
Hyp |
Ref |
Expression |
1 |
|
simpr |
|- ( ( A e. CC /\ B e. CC ) -> B e. CC ) |
2 |
1
|
adantr |
|- ( ( ( A e. CC /\ B e. CC ) /\ B =/= 0 ) -> B e. CC ) |
3 |
2
|
mul02d |
|- ( ( ( A e. CC /\ B e. CC ) /\ B =/= 0 ) -> ( 0 x. B ) = 0 ) |
4 |
3
|
eqeq2d |
|- ( ( ( A e. CC /\ B e. CC ) /\ B =/= 0 ) -> ( ( A x. B ) = ( 0 x. B ) <-> ( A x. B ) = 0 ) ) |
5 |
|
simpl |
|- ( ( A e. CC /\ B e. CC ) -> A e. CC ) |
6 |
5
|
adantr |
|- ( ( ( A e. CC /\ B e. CC ) /\ B =/= 0 ) -> A e. CC ) |
7 |
|
0cnd |
|- ( ( ( A e. CC /\ B e. CC ) /\ B =/= 0 ) -> 0 e. CC ) |
8 |
|
simpr |
|- ( ( ( A e. CC /\ B e. CC ) /\ B =/= 0 ) -> B =/= 0 ) |
9 |
6 7 2 8
|
mulcan2d |
|- ( ( ( A e. CC /\ B e. CC ) /\ B =/= 0 ) -> ( ( A x. B ) = ( 0 x. B ) <-> A = 0 ) ) |
10 |
4 9
|
bitr3d |
|- ( ( ( A e. CC /\ B e. CC ) /\ B =/= 0 ) -> ( ( A x. B ) = 0 <-> A = 0 ) ) |
11 |
10
|
biimpd |
|- ( ( ( A e. CC /\ B e. CC ) /\ B =/= 0 ) -> ( ( A x. B ) = 0 -> A = 0 ) ) |
12 |
11
|
impancom |
|- ( ( ( A e. CC /\ B e. CC ) /\ ( A x. B ) = 0 ) -> ( B =/= 0 -> A = 0 ) ) |
13 |
12
|
necon1bd |
|- ( ( ( A e. CC /\ B e. CC ) /\ ( A x. B ) = 0 ) -> ( -. A = 0 -> B = 0 ) ) |
14 |
13
|
orrd |
|- ( ( ( A e. CC /\ B e. CC ) /\ ( A x. B ) = 0 ) -> ( A = 0 \/ B = 0 ) ) |
15 |
14
|
ex |
|- ( ( A e. CC /\ B e. CC ) -> ( ( A x. B ) = 0 -> ( A = 0 \/ B = 0 ) ) ) |
16 |
1
|
mul02d |
|- ( ( A e. CC /\ B e. CC ) -> ( 0 x. B ) = 0 ) |
17 |
|
oveq1 |
|- ( A = 0 -> ( A x. B ) = ( 0 x. B ) ) |
18 |
17
|
eqeq1d |
|- ( A = 0 -> ( ( A x. B ) = 0 <-> ( 0 x. B ) = 0 ) ) |
19 |
16 18
|
syl5ibrcom |
|- ( ( A e. CC /\ B e. CC ) -> ( A = 0 -> ( A x. B ) = 0 ) ) |
20 |
5
|
mul01d |
|- ( ( A e. CC /\ B e. CC ) -> ( A x. 0 ) = 0 ) |
21 |
|
oveq2 |
|- ( B = 0 -> ( A x. B ) = ( A x. 0 ) ) |
22 |
21
|
eqeq1d |
|- ( B = 0 -> ( ( A x. B ) = 0 <-> ( A x. 0 ) = 0 ) ) |
23 |
20 22
|
syl5ibrcom |
|- ( ( A e. CC /\ B e. CC ) -> ( B = 0 -> ( A x. B ) = 0 ) ) |
24 |
19 23
|
jaod |
|- ( ( A e. CC /\ B e. CC ) -> ( ( A = 0 \/ B = 0 ) -> ( A x. B ) = 0 ) ) |
25 |
15 24
|
impbid |
|- ( ( A e. CC /\ B e. CC ) -> ( ( A x. B ) = 0 <-> ( A = 0 \/ B = 0 ) ) ) |