Metamath Proof Explorer

Theorem sn-remul0ord

Description: A product is zero iff one of its factors are zero. (Contributed by SN, 24-Nov-2025)

Ref Expression
Hypotheses sn-remul0ord.a 
|- ( ph -> A e. RR )
sn-remul0ord.b 
|- ( ph -> B e. RR )
Assertion sn-remul0ord 
|- ( ph -> ( ( A x. B ) = 0 <-> ( A = 0 \/ B = 0 ) ) )

Proof

Step Hyp Ref Expression
1 sn-remul0ord.a 
 |-  ( ph -> A e. RR )
2 sn-remul0ord.b 
 |-  ( ph -> B e. RR )
3 remul02 
 |-  ( B e. RR -> ( 0 x. B ) = 0 )
4 2 3 syl 
 |-  ( ph -> ( 0 x. B ) = 0 )
5 4 adantr 
 |-  ( ( ph /\ B =/= 0 ) -> ( 0 x. B ) = 0 )
6 5 eqeq2d 
 |-  ( ( ph /\ B =/= 0 ) -> ( ( A x. B ) = ( 0 x. B ) <-> ( A x. B ) = 0 ) )
7 1 adantr 
 |-  ( ( ph /\ B =/= 0 ) -> A e. RR )
8 0red 
 |-  ( ( ph /\ B =/= 0 ) -> 0 e. RR )
9 2 adantr 
 |-  ( ( ph /\ B =/= 0 ) -> B e. RR )
10 simpr 
 |-  ( ( ph /\ B =/= 0 ) -> B =/= 0 )
11 7 8 9 10 remulcan2d 
 |-  ( ( ph /\ B =/= 0 ) -> ( ( A x. B ) = ( 0 x. B ) <-> A = 0 ) )
12 6 11 bitr3d 
 |-  ( ( ph /\ B =/= 0 ) -> ( ( A x. B ) = 0 <-> A = 0 ) )
13 12 biimpd 
 |-  ( ( ph /\ B =/= 0 ) -> ( ( A x. B ) = 0 -> A = 0 ) )
14 13 impancom 
 |-  ( ( ph /\ ( A x. B ) = 0 ) -> ( B =/= 0 -> A = 0 ) )
15 14 necon1bd 
 |-  ( ( ph /\ ( A x. B ) = 0 ) -> ( -. A = 0 -> B = 0 ) )
16 15 orrd 
 |-  ( ( ph /\ ( A x. B ) = 0 ) -> ( A = 0 \/ B = 0 ) )
17 16 ex 
 |-  ( ph -> ( ( A x. B ) = 0 -> ( A = 0 \/ B = 0 ) ) )
18 oveq1 
 |-  ( A = 0 -> ( A x. B ) = ( 0 x. B ) )
19 18 eqeq1d 
 |-  ( A = 0 -> ( ( A x. B ) = 0 <-> ( 0 x. B ) = 0 ) )
20 4 19 syl5ibrcom 
 |-  ( ph -> ( A = 0 -> ( A x. B ) = 0 ) )
21 remul01 
 |-  ( A e. RR -> ( A x. 0 ) = 0 )
22 1 21 syl 
 |-  ( ph -> ( A x. 0 ) = 0 )
23 oveq2 
 |-  ( B = 0 -> ( A x. B ) = ( A x. 0 ) )
24 23 eqeq1d 
 |-  ( B = 0 -> ( ( A x. B ) = 0 <-> ( A x. 0 ) = 0 ) )
25 22 24 syl5ibrcom 
 |-  ( ph -> ( B = 0 -> ( A x. B ) = 0 ) )
26 20 25 jaod 
 |-  ( ph -> ( ( A = 0 \/ B = 0 ) -> ( A x. B ) = 0 ) )
27 17 26 impbid 
 |-  ( ph -> ( ( A x. B ) = 0 <-> ( A = 0 \/ B = 0 ) ) )