This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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