Metamath Proof Explorer


Theorem mul0or

Description: If a product is zero, one of its factors must be zero. Theorem I.11 of Apostol p. 18. (Contributed by NM, 9-Oct-1999) (Revised by Mario Carneiro, 27-May-2016)

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

Proof

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