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

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 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
sn-remul0ord.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
Assertion sn-remul0ord ( 𝜑 → ( ( 𝐴 · 𝐵 ) = 0 ↔ ( 𝐴 = 0 ∨ 𝐵 = 0 ) ) )

Proof

Step Hyp Ref Expression
1 sn-remul0ord.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2 sn-remul0ord.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3 remul02 ⊢ ( 𝐵 ∈ ℝ → ( 0 · 𝐵 ) = 0 )
4 2 3 syl ⊢ ( 𝜑 → ( 0 · 𝐵 ) = 0 )
5 4 adantr ⊢ ( ( 𝜑 ∧ 𝐵 ≠ 0 ) → ( 0 · 𝐵 ) = 0 )
6 5 eqeq2d ⊢ ( ( 𝜑 ∧ 𝐵 ≠ 0 ) → ( ( 𝐴 · 𝐵 ) = ( 0 · 𝐵 ) ↔ ( 𝐴 · 𝐵 ) = 0 ) )
7 1 adantr ⊢ ( ( 𝜑 ∧ 𝐵 ≠ 0 ) → 𝐴 ∈ ℝ )
8 0red ⊢ ( ( 𝜑 ∧ 𝐵 ≠ 0 ) → 0 ∈ ℝ )
9 2 adantr ⊢ ( ( 𝜑 ∧ 𝐵 ≠ 0 ) → 𝐵 ∈ ℝ )
10 simpr ⊢ ( ( 𝜑 ∧ 𝐵 ≠ 0 ) → 𝐵 ≠ 0 )
11 7 8 9 10 remulcan2d ⊢ ( ( 𝜑 ∧ 𝐵 ≠ 0 ) → ( ( 𝐴 · 𝐵 ) = ( 0 · 𝐵 ) ↔ 𝐴 = 0 ) )
12 6 11 bitr3d ⊢ ( ( 𝜑 ∧ 𝐵 ≠ 0 ) → ( ( 𝐴 · 𝐵 ) = 0 ↔ 𝐴 = 0 ) )
13 12 biimpd ⊢ ( ( 𝜑 ∧ 𝐵 ≠ 0 ) → ( ( 𝐴 · 𝐵 ) = 0 → 𝐴 = 0 ) )
14 13 impancom ⊢ ( ( 𝜑 ∧ ( 𝐴 · 𝐵 ) = 0 ) → ( 𝐵 ≠ 0 → 𝐴 = 0 ) )
15 14 necon1bd ⊢ ( ( 𝜑 ∧ ( 𝐴 · 𝐵 ) = 0 ) → ( ¬ 𝐴 = 0 → 𝐵 = 0 ) )
16 15 orrd ⊢ ( ( 𝜑 ∧ ( 𝐴 · 𝐵 ) = 0 ) → ( 𝐴 = 0 ∨ 𝐵 = 0 ) )
17 16 ex ⊢ ( 𝜑 → ( ( 𝐴 · 𝐵 ) = 0 → ( 𝐴 = 0 ∨ 𝐵 = 0 ) ) )
18 oveq1 ⊢ ( 𝐴 = 0 → ( 𝐴 · 𝐵 ) = ( 0 · 𝐵 ) )
19 18 eqeq1d ⊢ ( 𝐴 = 0 → ( ( 𝐴 · 𝐵 ) = 0 ↔ ( 0 · 𝐵 ) = 0 ) )
20 4 19 syl5ibrcom ⊢ ( 𝜑 → ( 𝐴 = 0 → ( 𝐴 · 𝐵 ) = 0 ) )
21 remul01 ⊢ ( 𝐴 ∈ ℝ → ( 𝐴 · 0 ) = 0 )
22 1 21 syl ⊢ ( 𝜑 → ( 𝐴 · 0 ) = 0 )
23 oveq2 ⊢ ( 𝐵 = 0 → ( 𝐴 · 𝐵 ) = ( 𝐴 · 0 ) )
24 23 eqeq1d ⊢ ( 𝐵 = 0 → ( ( 𝐴 · 𝐵 ) = 0 ↔ ( 𝐴 · 0 ) = 0 ) )
25 22 24 syl5ibrcom ⊢ ( 𝜑 → ( 𝐵 = 0 → ( 𝐴 · 𝐵 ) = 0 ) )
26 20 25 jaod ⊢ ( 𝜑 → ( ( 𝐴 = 0 ∨ 𝐵 = 0 ) → ( 𝐴 · 𝐵 ) = 0 ) )
27 17 26 impbid ⊢ ( 𝜑 → ( ( 𝐴 · 𝐵 ) = 0 ↔ ( 𝐴 = 0 ∨ 𝐵 = 0 ) ) )