Theorem n0ltsp1le

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

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

Proof

Step	Hyp	Ref	Expression
1		n0subs2	⊢ ( ( 𝑀 ∈ ℕ0s ∧ 𝑁 ∈ ℕ0s ) → ( 𝑀 <s 𝑁 ↔ ( 𝑁 -s 𝑀 ) ∈ ℕs ) )
2		nnsge1	⊢ ( ( 𝑁 -s 𝑀 ) ∈ ℕs → 1s ≤s ( 𝑁 -s 𝑀 ) )
3		1no	⊢ 1s ∈ No
4	3	a1i	⊢ ( ( 𝑀 ∈ ℕ0s ∧ 𝑁 ∈ ℕ0s ) → 1s ∈ No )
5		simpr	⊢ ( ( 𝑀 ∈ ℕ0s ∧ 𝑁 ∈ ℕ0s ) → 𝑁 ∈ ℕ0s )
6		n0no	⊢ ( 𝑁 ∈ ℕ0s → 𝑁 ∈ No )
7	5 6	syl	⊢ ( ( 𝑀 ∈ ℕ0s ∧ 𝑁 ∈ ℕ0s ) → 𝑁 ∈ No )
8		n0no	⊢ ( 𝑀 ∈ ℕ0s → 𝑀 ∈ No )
9	8	adantr	⊢ ( ( 𝑀 ∈ ℕ0s ∧ 𝑁 ∈ ℕ0s ) → 𝑀 ∈ No )
10	7 9	subscld	⊢ ( ( 𝑀 ∈ ℕ0s ∧ 𝑁 ∈ ℕ0s ) → ( 𝑁 -s 𝑀 ) ∈ No )
11	4 10 9	leadds2d	⊢ ( ( 𝑀 ∈ ℕ0s ∧ 𝑁 ∈ ℕ0s ) → ( 1s ≤s ( 𝑁 -s 𝑀 ) ↔ ( 𝑀 +s 1s ) ≤s ( 𝑀 +s ( 𝑁 -s 𝑀 ) ) ) )
12		pncan3s	⊢ ( ( 𝑀 ∈ No ∧ 𝑁 ∈ No ) → ( 𝑀 +s ( 𝑁 -s 𝑀 ) ) = 𝑁 )
13	8 6 12	syl2an	⊢ ( ( 𝑀 ∈ ℕ0s ∧ 𝑁 ∈ ℕ0s ) → ( 𝑀 +s ( 𝑁 -s 𝑀 ) ) = 𝑁 )
14	13	breq2d	⊢ ( ( 𝑀 ∈ ℕ0s ∧ 𝑁 ∈ ℕ0s ) → ( ( 𝑀 +s 1s ) ≤s ( 𝑀 +s ( 𝑁 -s 𝑀 ) ) ↔ ( 𝑀 +s 1s ) ≤s 𝑁 ) )
15	11 14	bitrd	⊢ ( ( 𝑀 ∈ ℕ0s ∧ 𝑁 ∈ ℕ0s ) → ( 1s ≤s ( 𝑁 -s 𝑀 ) ↔ ( 𝑀 +s 1s ) ≤s 𝑁 ) )
16	2 15	imbitrid	⊢ ( ( 𝑀 ∈ ℕ0s ∧ 𝑁 ∈ ℕ0s ) → ( ( 𝑁 -s 𝑀 ) ∈ ℕs → ( 𝑀 +s 1s ) ≤s 𝑁 ) )
17	1 16	sylbid	⊢ ( ( 𝑀 ∈ ℕ0s ∧ 𝑁 ∈ ℕ0s ) → ( 𝑀 <s 𝑁 → ( 𝑀 +s 1s ) ≤s 𝑁 ) )
18	8	ad2antrr	⊢ ( ( ( 𝑀 ∈ ℕ0s ∧ 𝑁 ∈ ℕ0s ) ∧ ( 𝑀 +s 1s ) ≤s 𝑁 ) → 𝑀 ∈ No )
19		peano2no	⊢ ( 𝑀 ∈ No → ( 𝑀 +s 1s ) ∈ No )
20	18 19	syl	⊢ ( ( ( 𝑀 ∈ ℕ0s ∧ 𝑁 ∈ ℕ0s ) ∧ ( 𝑀 +s 1s ) ≤s 𝑁 ) → ( 𝑀 +s 1s ) ∈ No )
21	6	ad2antlr	⊢ ( ( ( 𝑀 ∈ ℕ0s ∧ 𝑁 ∈ ℕ0s ) ∧ ( 𝑀 +s 1s ) ≤s 𝑁 ) → 𝑁 ∈ No )
22	18	ltsp1d	⊢ ( ( ( 𝑀 ∈ ℕ0s ∧ 𝑁 ∈ ℕ0s ) ∧ ( 𝑀 +s 1s ) ≤s 𝑁 ) → 𝑀 <s ( 𝑀 +s 1s ) )
23		simpr	⊢ ( ( ( 𝑀 ∈ ℕ0s ∧ 𝑁 ∈ ℕ0s ) ∧ ( 𝑀 +s 1s ) ≤s 𝑁 ) → ( 𝑀 +s 1s ) ≤s 𝑁 )
24	18 20 21 22 23	ltlestrd	⊢ ( ( ( 𝑀 ∈ ℕ0s ∧ 𝑁 ∈ ℕ0s ) ∧ ( 𝑀 +s 1s ) ≤s 𝑁 ) → 𝑀 <s 𝑁 )
25	24	ex	⊢ ( ( 𝑀 ∈ ℕ0s ∧ 𝑁 ∈ ℕ0s ) → ( ( 𝑀 +s 1s ) ≤s 𝑁 → 𝑀 <s 𝑁 ) )
26	17 25	impbid	⊢ ( ( 𝑀 ∈ ℕ0s ∧ 𝑁 ∈ ℕ0s ) → ( 𝑀 <s 𝑁 ↔ ( 𝑀 +s 1s ) ≤s 𝑁 ) )