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	$$⊢A\in {\mathbb{N}}_{\mathrm{0s}}\to 0_s{\le }_{s}A$$

Proof

Step	Hyp	Ref	Expression
1		breq2	$$⊢n=0_s\to \left(0_s{\le }_{s}n\leftrightarrow 0_s{\le }_s{0}_s\right)$$
2		breq2	$$⊢n=m\to \left(0_s{\le }_{s}n\leftrightarrow 0_s{\le }_{s}m\right)$$
3		breq2	$$⊢n=m{+}_s{1}_s\to \left(0_s{\le }_{s}n\leftrightarrow 0_s{\le }_s\left(m{+}_s{1}_s\right)\right)$$
4		breq2	$$⊢n=A\to \left(0_s{\le }_{s}n\leftrightarrow 0_s{\le }_{s}A\right)$$
5		0sno	$$⊢0_s\in \mathrm{No}$$
6		slerflex	$$⊢0_s\in \mathrm{No}\to 0_s{\le }_s{0}_s$$
7	5 6	ax-mp	$$⊢0_s{\le }_s{0}_s$$
8	5	a1i	$$⊢\left(m\in {\mathbb{N}}_{\mathrm{0s}}\wedge 0_s{\le }_{s}m\right)\to 0_s\in \mathrm{No}$$
9		n0sno	$$⊢m\in {\mathbb{N}}_{\mathrm{0s}}\to m\in \mathrm{No}$$
10	9	adantr	$$⊢\left(m\in {\mathbb{N}}_{\mathrm{0s}}\wedge 0_s{\le }_{s}m\right)\to m\in \mathrm{No}$$
11		peano2no	$$⊢m\in \mathrm{No}\to m{+}_s{1}_s\in \mathrm{No}$$
12	9 11	syl	$$⊢m\in {\mathbb{N}}_{\mathrm{0s}}\to m{+}_s{1}_s\in \mathrm{No}$$
13	12	adantr	$$⊢\left(m\in {\mathbb{N}}_{\mathrm{0s}}\wedge 0_s{\le }_{s}m\right)\to m{+}_s{1}_s\in \mathrm{No}$$
14		simpr	$$⊢\left(m\in {\mathbb{N}}_{\mathrm{0s}}\wedge 0_s{\le }_{s}m\right)\to 0_s{\le }_{s}m$$
15	9	addsridd	$$⊢m\in {\mathbb{N}}_{\mathrm{0s}}\to m{+}_s{0}_s=m$$
16	15	adantr	$$⊢\left(m\in {\mathbb{N}}_{\mathrm{0s}}\wedge 0_s{\le }_{s}m\right)\to m{+}_s{0}_s=m$$
17	5	a1i	$$⊢\top \to 0_s\in \mathrm{No}$$
18		1sno	$$⊢1_s\in \mathrm{No}$$
19	18	a1i	$$⊢\top \to 1_s\in \mathrm{No}$$
20		0slt1s	$$⊢0_s{<}_s{1}_s$$
21	20	a1i	$$⊢\top \to 0_s{<}_s{1}_s$$
22	17 19 21	sltled	$$⊢\top \to 0_s{\le }_s{1}_s$$
23	22	mptru	$$⊢0_s{\le }_s{1}_s$$
24	5	a1i	$$⊢m\in {\mathbb{N}}_{\mathrm{0s}}\to 0_s\in \mathrm{No}$$
25	18	a1i	$$⊢m\in {\mathbb{N}}_{\mathrm{0s}}\to 1_s\in \mathrm{No}$$
26	24 25 9	sleadd2d	$$⊢m\in {\mathbb{N}}_{\mathrm{0s}}\to \left(0_s{\le }_s{1}_s\leftrightarrow \left(m{+}_s{0}_s\right){\le }_s\left(m{+}_s{1}_s\right)\right)$$
27	23 26	mpbii	$$⊢m\in {\mathbb{N}}_{\mathrm{0s}}\to \left(m{+}_s{0}_s\right){\le }_s\left(m{+}_s{1}_s\right)$$
28	27	adantr	$$⊢\left(m\in {\mathbb{N}}_{\mathrm{0s}}\wedge 0_s{\le }_{s}m\right)\to \left(m{+}_s{0}_s\right){\le }_s\left(m{+}_s{1}_s\right)$$
29	16 28	eqbrtrrd	$$⊢\left(m\in {\mathbb{N}}_{\mathrm{0s}}\wedge 0_s{\le }_{s}m\right)\to m{\le }_s\left(m{+}_s{1}_s\right)$$
30	8 10 13 14 29	sletrd	$$⊢\left(m\in {\mathbb{N}}_{\mathrm{0s}}\wedge 0_s{\le }_{s}m\right)\to 0_s{\le }_s\left(m{+}_s{1}_s\right)$$
31	30	ex	$$⊢m\in {\mathbb{N}}_{\mathrm{0s}}\to \left(0_s{\le }_{s}m\to 0_s{\le }_s\left(m{+}_s{1}_s\right)\right)$$
32	1 2 3 4 7 31	n0sind	$$⊢A\in {\mathbb{N}}_{\mathrm{0s}}\to 0_s{\le }_{s}A$$