Theorem posdifsd

Description: Comparison of two surreals whose difference is positive. (Contributed by Scott Fenton, 10-Mar-2025)

	Ref	Expression
Hypotheses	posdifsd.1	⊢ ( 𝜑 → 𝐴 ∈ No )
	posdifsd.2	⊢ ( 𝜑 → 𝐵 ∈ No )
Assertion	posdifsd	⊢ ( 𝜑 → ( 𝐴 <s 𝐵 ↔ 0s <s ( 𝐵 -s 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		posdifsd.1	⊢ ( 𝜑 → 𝐴 ∈ No )
2		posdifsd.2	⊢ ( 𝜑 → 𝐵 ∈ No )
3		0no	⊢ 0s ∈ No
4	3	a1i	⊢ ( 𝜑 → 0s ∈ No )
5	2 1	subscld	⊢ ( 𝜑 → ( 𝐵 -s 𝐴 ) ∈ No )
6	4 5 1	ltadds1d	⊢ ( 𝜑 → ( 0s <s ( 𝐵 -s 𝐴 ) ↔ ( 0s +s 𝐴 ) <s ( ( 𝐵 -s 𝐴 ) +s 𝐴 ) ) )
7		addslid	⊢ ( 𝐴 ∈ No → ( 0s +s 𝐴 ) = 𝐴 )
8	1 7	syl	⊢ ( 𝜑 → ( 0s +s 𝐴 ) = 𝐴 )
9		npcans	⊢ ( ( 𝐵 ∈ No ∧ 𝐴 ∈ No ) → ( ( 𝐵 -s 𝐴 ) +s 𝐴 ) = 𝐵 )
10	2 1 9	syl2anc	⊢ ( 𝜑 → ( ( 𝐵 -s 𝐴 ) +s 𝐴 ) = 𝐵 )
11	8 10	breq12d	⊢ ( 𝜑 → ( ( 0s +s 𝐴 ) <s ( ( 𝐵 -s 𝐴 ) +s 𝐴 ) ↔ 𝐴 <s 𝐵 ) )
12	6 11	bitr2d	⊢ ( 𝜑 → ( 𝐴 <s 𝐵 ↔ 0s <s ( 𝐵 -s 𝐴 ) ) )