Metamath Proof Explorer

Theorem divmulswd

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

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

Proof

Step Hyp Ref Expression
1 divmulswd.1 ⊢ φ → A ∈ No
2 divmulswd.2 ⊢ φ → B ∈ No
3 divmulswd.3 ⊢ φ → C ∈ No
4 divmulswd.4 ⊢ φ → C ≠ 0 s
5 divmulswd.5 ⊢ φ → ∃ x ∈ No C ⋅ s x = 1 s
6 3 4 jca ⊢ φ → C ∈ No ∧ C ≠ 0 s
7 divmulsw ⊢ 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