Metamath Proof Explorer

Theorem divsmulwd

Description: Relationship between surreal division and multiplication. Weak version that does not assume reciprocals. (Contributed by Scott Fenton, 12-Mar-2025)

Ref Expression
Hypotheses divsmulwd.1 ⊢ φ → A ∈ No
divsmulwd.2 ⊢ φ → B ∈ No
divsmulwd.3 ⊢ φ → C ∈ No
divsmulwd.4 ⊢ φ → C ≠ 0 s
divsmulwd.5 ⊢ φ → ∃ x ∈ No C ⋅ s x = 1 s
Assertion divsmulwd ⊢ φ → A / su C = B ↔ C ⋅ s B = A

Proof

Step Hyp Ref Expression
1 divsmulwd.1 ⊢ φ → A ∈ No
2 divsmulwd.2 ⊢ φ → B ∈ No
3 divsmulwd.3 ⊢ φ → C ∈ No
4 divsmulwd.4 ⊢ φ → C ≠ 0 s
5 divsmulwd.5 ⊢ φ → ∃ x ∈ No C ⋅ s x = 1 s
6 3 4 jca ⊢ φ → C ∈ No ∧ C ≠ 0 s
7 divsmulw ⊢ A ∈ No ∧ B ∈ No ∧ C ∈ No ∧ C ≠ 0 s ∧ ∃ x ∈ No C ⋅ s x = 1 s → A / su C = B ↔ C ⋅ s B = A
8 1 2 6 5 7 syl31anc ⊢ φ → A / su C = B ↔ C ⋅ s B = A