Theorem n0sge0

Description: A non-negative integer is greater than or equal to zero. (Contributed by Scott Fenton, 15-Apr-2025)

	Ref	Expression
Assertion	n0sge0	⊢ ( 𝐴 ∈ ℕ0s → 0s ≤s 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		breq2	⊢ ( 𝑛 = 0s → ( 0s ≤s 𝑛 ↔ 0s ≤s 0s ) )
2		breq2	⊢ ( 𝑛 = 𝑚 → ( 0s ≤s 𝑛 ↔ 0s ≤s 𝑚 ) )
3		breq2	⊢ ( 𝑛 = ( 𝑚 +s 1s ) → ( 0s ≤s 𝑛 ↔ 0s ≤s ( 𝑚 +s 1s ) ) )
4		breq2	⊢ ( 𝑛 = 𝐴 → ( 0s ≤s 𝑛 ↔ 0s ≤s 𝐴 ) )
5		0no	⊢ 0s ∈ No
6		lesid	⊢ ( 0s ∈ No → 0s ≤s 0s )
7	5 6	ax-mp	⊢ 0s ≤s 0s
8	5	a1i	⊢ ( ( 𝑚 ∈ ℕ0s ∧ 0s ≤s 𝑚 ) → 0s ∈ No )
9		n0no	⊢ ( 𝑚 ∈ ℕ0s → 𝑚 ∈ No )
10	9	adantr	⊢ ( ( 𝑚 ∈ ℕ0s ∧ 0s ≤s 𝑚 ) → 𝑚 ∈ No )
11		peano2no	⊢ ( 𝑚 ∈ No → ( 𝑚 +s 1s ) ∈ No )
12	9 11	syl	⊢ ( 𝑚 ∈ ℕ0s → ( 𝑚 +s 1s ) ∈ No )
13	12	adantr	⊢ ( ( 𝑚 ∈ ℕ0s ∧ 0s ≤s 𝑚 ) → ( 𝑚 +s 1s ) ∈ No )
14		simpr	⊢ ( ( 𝑚 ∈ ℕ0s ∧ 0s ≤s 𝑚 ) → 0s ≤s 𝑚 )
15	9	addsridd	⊢ ( 𝑚 ∈ ℕ0s → ( 𝑚 +s 0s ) = 𝑚 )
16	15	adantr	⊢ ( ( 𝑚 ∈ ℕ0s ∧ 0s ≤s 𝑚 ) → ( 𝑚 +s 0s ) = 𝑚 )
17	5	a1i	⊢ ( ⊤ → 0s ∈ No )
18		1no	⊢ 1s ∈ No
19	18	a1i	⊢ ( ⊤ → 1s ∈ No )
20		0lt1s	⊢ 0s <s 1s
21	20	a1i	⊢ ( ⊤ → 0s <s 1s )
22	17 19 21	ltlesd	⊢ ( ⊤ → 0s ≤s 1s )
23	22	mptru	⊢ 0s ≤s 1s
24	5	a1i	⊢ ( 𝑚 ∈ ℕ0s → 0s ∈ No )
25	18	a1i	⊢ ( 𝑚 ∈ ℕ0s → 1s ∈ No )
26	24 25 9	leadds2d	⊢ ( 𝑚 ∈ ℕ0s → ( 0s ≤s 1s ↔ ( 𝑚 +s 0s ) ≤s ( 𝑚 +s 1s ) ) )
27	23 26	mpbii	⊢ ( 𝑚 ∈ ℕ0s → ( 𝑚 +s 0s ) ≤s ( 𝑚 +s 1s ) )
28	27	adantr	⊢ ( ( 𝑚 ∈ ℕ0s ∧ 0s ≤s 𝑚 ) → ( 𝑚 +s 0s ) ≤s ( 𝑚 +s 1s ) )
29	16 28	eqbrtrrd	⊢ ( ( 𝑚 ∈ ℕ0s ∧ 0s ≤s 𝑚 ) → 𝑚 ≤s ( 𝑚 +s 1s ) )
30	8 10 13 14 29	lestrd	⊢ ( ( 𝑚 ∈ ℕ0s ∧ 0s ≤s 𝑚 ) → 0s ≤s ( 𝑚 +s 1s ) )
31	30	ex	⊢ ( 𝑚 ∈ ℕ0s → ( 0s ≤s 𝑚 → 0s ≤s ( 𝑚 +s 1s ) ) )
32	1 2 3 4 7 31	n0sind	⊢ ( 𝐴 ∈ ℕ0s → 0s ≤s 𝐴 )