Metamath Proof Explorer

Theorem divmuls

Description: Relationship between surreal division and multiplication. (Contributed by Scott Fenton, 16-Mar-2025)

Ref Expression
Assertion divmuls ⊢ A ∈ No ∧ B ∈ No ∧ C ∈ No ∧ C ≠ 0 s → A / su C = B ↔ C ⋅ s B = A

Proof

Step Hyp Ref Expression
1 recsex ⊢ C ∈ No ∧ C ≠ 0 s → ∃ x ∈ No C ⋅ s x = 1 s
2 1 3ad2ant3 ⊢ A ∈ No ∧ B ∈ No ∧ C ∈ No ∧ C ≠ 0 s → ∃ x ∈ No C ⋅ s x = 1 s
3 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
4 2 3 mpdan ⊢ A ∈ No ∧ B ∈ No ∧ C ∈ No ∧ C ≠ 0 s → A / su C = B ↔ C ⋅ s B = A