Theorem n0lesm1lt

Description: Non-negative surreal ordering relation. (Contributed by Scott Fenton, 8-Nov-2025)

	Ref	Expression
Assertion	n0lesm1lt	⊢ ( ( 𝑀 ∈ ℕ0s ∧ 𝑁 ∈ ℕ0s ) → ( 𝑀 ≤s 𝑁 ↔ ( 𝑀 −s 1s ) <s 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		n0lesltp1	⊢ ( ( 𝑀 ∈ ℕ0s ∧ 𝑁 ∈ ℕ0s ) → ( 𝑀 ≤s 𝑁 ↔ 𝑀 <s ( 𝑁 +s 1s ) ) )
2		n0no	⊢ ( 𝑀 ∈ ℕ0s → 𝑀 ∈ No )
3	2	adantr	⊢ ( ( 𝑀 ∈ ℕ0s ∧ 𝑁 ∈ ℕ0s ) → 𝑀 ∈ No )
4		n0no	⊢ ( 𝑁 ∈ ℕ0s → 𝑁 ∈ No )
5	4	adantl	⊢ ( ( 𝑀 ∈ ℕ0s ∧ 𝑁 ∈ ℕ0s ) → 𝑁 ∈ No )
6		peano2no	⊢ ( 𝑁 ∈ No → ( 𝑁 +s 1s ) ∈ No )
7	5 6	syl	⊢ ( ( 𝑀 ∈ ℕ0s ∧ 𝑁 ∈ ℕ0s ) → ( 𝑁 +s 1s ) ∈ No )
8		1no	⊢ 1s ∈ No
9	8	a1i	⊢ ( ( 𝑀 ∈ ℕ0s ∧ 𝑁 ∈ ℕ0s ) → 1s ∈ No )
10	3 7 9	ltsubs1d	⊢ ( ( 𝑀 ∈ ℕ0s ∧ 𝑁 ∈ ℕ0s ) → ( 𝑀 <s ( 𝑁 +s 1s ) ↔ ( 𝑀 −s 1s ) <s ( ( 𝑁 +s 1s ) −s 1s ) ) )
11		pncans	⊢ ( ( 𝑁 ∈ No ∧ 1s ∈ No ) → ( ( 𝑁 +s 1s ) −s 1s ) = 𝑁 )
12	4 8 11	sylancl	⊢ ( 𝑁 ∈ ℕ0s → ( ( 𝑁 +s 1s ) −s 1s ) = 𝑁 )
13	12	adantl	⊢ ( ( 𝑀 ∈ ℕ0s ∧ 𝑁 ∈ ℕ0s ) → ( ( 𝑁 +s 1s ) −s 1s ) = 𝑁 )
14	13	breq2d	⊢ ( ( 𝑀 ∈ ℕ0s ∧ 𝑁 ∈ ℕ0s ) → ( ( 𝑀 −s 1s ) <s ( ( 𝑁 +s 1s ) −s 1s ) ↔ ( 𝑀 −s 1s ) <s 𝑁 ) )
15	1 10 14	3bitrd	⊢ ( ( 𝑀 ∈ ℕ0s ∧ 𝑁 ∈ ℕ0s ) → ( 𝑀 ≤s 𝑁 ↔ ( 𝑀 −s 1s ) <s 𝑁 ) )