Theorem divscl

Description: Surreal division closure law. (Contributed by Scott Fenton, 16-Mar-2025)

	Ref	Expression
Assertion	divscl	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐵 ≠ 0s ) → ( 𝐴 /su 𝐵 ) ∈ No )

Proof

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