Theorem divsmul

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

	Ref	Expression
Assertion	divsmul	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ ( 𝐶 ∈ No ∧ 𝐶 ≠ 0s ) ) → ( ( 𝐴 /su 𝐶 ) = 𝐵 ↔ ( 𝐶 ·s 𝐵 ) = 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		recsex	⊢ ( ( 𝐶 ∈ No ∧ 𝐶 ≠ 0s ) → ∃ 𝑥 ∈ No ( 𝐶 ·s 𝑥 ) = 1s )
2	1	3ad2ant3	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ ( 𝐶 ∈ No ∧ 𝐶 ≠ 0s ) ) → ∃ 𝑥 ∈ No ( 𝐶 ·s 𝑥 ) = 1s )
3		divsmulw	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ ( 𝐶 ∈ No ∧ 𝐶 ≠ 0s ) ) ∧ ∃ 𝑥 ∈ No ( 𝐶 ·s 𝑥 ) = 1s ) → ( ( 𝐴 /su 𝐶 ) = 𝐵 ↔ ( 𝐶 ·s 𝐵 ) = 𝐴 ) )
4	2 3	mpdan	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ ( 𝐶 ∈ No ∧ 𝐶 ≠ 0s ) ) → ( ( 𝐴 /su 𝐶 ) = 𝐵 ↔ ( 𝐶 ·s 𝐵 ) = 𝐴 ) )