Theorem nnsge1

Description: A positive surreal integer is greater than or equal to one. (Contributed by Scott Fenton, 26-Jul-2025)

	Ref	Expression
Assertion	nnsge1	⊢ ( 𝑁 ∈ ℕs → 1s ≤s 𝑁 )

Proof

Step	Hyp	Ref	Expression
1		elnns	⊢ ( 𝑁 ∈ ℕs ↔ ( 𝑁 ∈ ℕ0s ∧ 𝑁 ≠ 0s ) )
2		n0s0suc	⊢ ( 𝑁 ∈ ℕ0s → ( 𝑁 = 0s ∨ ∃ 𝑥 ∈ ℕ0s 𝑁 = ( 𝑥 +s 1s ) ) )
3		neneq	⊢ ( 𝑁 ≠ 0s → ¬ 𝑁 = 0s )
4		pm2.53	⊢ ( ( 𝑁 = 0s ∨ ∃ 𝑥 ∈ ℕ0s 𝑁 = ( 𝑥 +s 1s ) ) → ( ¬ 𝑁 = 0s → ∃ 𝑥 ∈ ℕ0s 𝑁 = ( 𝑥 +s 1s ) ) )
5	4	imp	⊢ ( ( ( 𝑁 = 0s ∨ ∃ 𝑥 ∈ ℕ0s 𝑁 = ( 𝑥 +s 1s ) ) ∧ ¬ 𝑁 = 0s ) → ∃ 𝑥 ∈ ℕ0s 𝑁 = ( 𝑥 +s 1s ) )
6		1no	⊢ 1s ∈ No
7		addslid	⊢ ( 1s ∈ No → ( 0s +s 1s ) = 1s )
8	6 7	ax-mp	⊢ ( 0s +s 1s ) = 1s
9		n0sge0	⊢ ( 𝑥 ∈ ℕ0s → 0s ≤s 𝑥 )
10		n0no	⊢ ( 𝑥 ∈ ℕ0s → 𝑥 ∈ No )
11		0no	⊢ 0s ∈ No
12		leadds1	⊢ ( ( 0s ∈ No ∧ 𝑥 ∈ No ∧ 1s ∈ No ) → ( 0s ≤s 𝑥 ↔ ( 0s +s 1s ) ≤s ( 𝑥 +s 1s ) ) )
13	11 6 12	mp3an13	⊢ ( 𝑥 ∈ No → ( 0s ≤s 𝑥 ↔ ( 0s +s 1s ) ≤s ( 𝑥 +s 1s ) ) )
14	10 13	syl	⊢ ( 𝑥 ∈ ℕ0s → ( 0s ≤s 𝑥 ↔ ( 0s +s 1s ) ≤s ( 𝑥 +s 1s ) ) )
15	9 14	mpbid	⊢ ( 𝑥 ∈ ℕ0s → ( 0s +s 1s ) ≤s ( 𝑥 +s 1s ) )
16	8 15	eqbrtrrid	⊢ ( 𝑥 ∈ ℕ0s → 1s ≤s ( 𝑥 +s 1s ) )
17		breq2	⊢ ( 𝑁 = ( 𝑥 +s 1s ) → ( 1s ≤s 𝑁 ↔ 1s ≤s ( 𝑥 +s 1s ) ) )
18	16 17	syl5ibrcom	⊢ ( 𝑥 ∈ ℕ0s → ( 𝑁 = ( 𝑥 +s 1s ) → 1s ≤s 𝑁 ) )
19	18	rexlimiv	⊢ ( ∃ 𝑥 ∈ ℕ0s 𝑁 = ( 𝑥 +s 1s ) → 1s ≤s 𝑁 )
20	5 19	syl	⊢ ( ( ( 𝑁 = 0s ∨ ∃ 𝑥 ∈ ℕ0s 𝑁 = ( 𝑥 +s 1s ) ) ∧ ¬ 𝑁 = 0s ) → 1s ≤s 𝑁 )
21	2 3 20	syl2an	⊢ ( ( 𝑁 ∈ ℕ0s ∧ 𝑁 ≠ 0s ) → 1s ≤s 𝑁 )
22	1 21	sylbi	⊢ ( 𝑁 ∈ ℕs → 1s ≤s 𝑁 )