Metamath Proof Explorer

Theorem muls0ord

Description: If a surreal product is zero, one of its factors must be zero. (Contributed by Scott Fenton, 16-Apr-2025)

Ref Expression
Hypotheses muls0ord.1 ⊢ φ → A ∈ No
muls0ord.2 ⊢ φ → B ∈ No
Assertion muls0ord ⊢ φ → A ⋅ s B = 0 s ↔ A = 0 s ∨ B = 0 s

Proof

Step Hyp Ref Expression
1 muls0ord.1 ⊢ φ → A ∈ No
2 muls0ord.2 ⊢ φ → B ∈ No
3 muls02 ⊢ B ∈ No → 0 s ⋅ s B = 0 s
4 2 3 syl ⊢ φ → 0 s ⋅ s B = 0 s
5 4 adantr ⊢ φ ∧ B ≠ 0 s → 0 s ⋅ s B = 0 s
6 5 eqeq2d ⊢ φ ∧ B ≠ 0 s → A ⋅ s B = 0 s ⋅ s B ↔ A ⋅ s B = 0 s
7 1 adantr ⊢ φ ∧ B ≠ 0 s → A ∈ No
8 0no ⊢ 0 s ∈ No
9 8 a1i ⊢ φ ∧ B ≠ 0 s → 0 s ∈ No
10 2 adantr ⊢ φ ∧ B ≠ 0 s → B ∈ No
11 simpr ⊢ φ ∧ B ≠ 0 s → B ≠ 0 s
12 7 9 10 11 mulscan2d ⊢ φ ∧ B ≠ 0 s → A ⋅ s B = 0 s ⋅ s B ↔ A = 0 s
13 6 12 bitr3d ⊢ φ ∧ B ≠ 0 s → A ⋅ s B = 0 s ↔ A = 0 s
14 13 biimpd ⊢ φ ∧ B ≠ 0 s → A ⋅ s B = 0 s → A = 0 s
15 14 impancom ⊢ φ ∧ A ⋅ s B = 0 s → B ≠ 0 s → A = 0 s
16 15 necon1bd ⊢ φ ∧ A ⋅ s B = 0 s → ¬ A = 0 s → B = 0 s
17 16 orrd ⊢ φ ∧ A ⋅ s B = 0 s → A = 0 s ∨ B = 0 s
18 17 ex ⊢ φ → A ⋅ s B = 0 s → A = 0 s ∨ B = 0 s
19 oveq1 ⊢ A = 0 s → A ⋅ s B = 0 s ⋅ s B
20 19 eqeq1d ⊢ A = 0 s → A ⋅ s B = 0 s ↔ 0 s ⋅ s B = 0 s
21 4 20 syl5ibrcom ⊢ φ → A = 0 s → A ⋅ s B = 0 s
22 muls01 ⊢ A ∈ No → A ⋅ s 0 s = 0 s
23 1 22 syl ⊢ φ → A ⋅ s 0 s = 0 s
24 oveq2 ⊢ B = 0 s → A ⋅ s B = A ⋅ s 0 s
25 24 eqeq1d ⊢ B = 0 s → A ⋅ s B = 0 s ↔ A ⋅ s 0 s = 0 s
26 23 25 syl5ibrcom ⊢ φ → B = 0 s → A ⋅ s B = 0 s
27 21 26 jaod ⊢ φ → A = 0 s ∨ B = 0 s → A ⋅ s B = 0 s
28 18 27 impbid ⊢ φ → A ⋅ s B = 0 s ↔ A = 0 s ∨ B = 0 s