Theorem xnn0lenn0nn0

Description: An extended nonnegative integer which is less than or equal to a nonnegative integer is a nonnegative integer. (Contributed by AV, 24-Nov-2021)

	Ref	Expression
Assertion	xnn0lenn0nn0	$$⊢\left(M\in {\mathbb{N}}_0^{*}\wedge N\in {\mathbb{N}}_0\wedge M\le N\right)\to M\in {\mathbb{N}}_0$$

Proof

Step	Hyp	Ref	Expression
1		elxnn0	$$⊢M\in {\mathbb{N}}_0^{*}\leftrightarrow \left(M\in {\mathbb{N}}_0\vee M=\mathrm{+\infty }\right)$$
2		2a1	$$⊢M\in {\mathbb{N}}_0\to \left(N\in {\mathbb{N}}_0\to \left(M\le N\to M\in {\mathbb{N}}_0\right)\right)$$
3		breq1	$$⊢M=\mathrm{+\infty }\to \left(M\le N\leftrightarrow \mathrm{+\infty }\le N\right)$$
4	3	adantr	$$⊢\left(M=\mathrm{+\infty }\wedge N\in {\mathbb{N}}_0\right)\to \left(M\le N\leftrightarrow \mathrm{+\infty }\le N\right)$$
5		nn0re	$$⊢N\in {\mathbb{N}}_0\to N\in ℝ$$
6	5	rexrd	$$⊢N\in {\mathbb{N}}_0\to N\in {ℝ}^{*}$$
7		xgepnf	$$⊢N\in {ℝ}^{*}\to \left(\mathrm{+\infty }\le N\leftrightarrow N=\mathrm{+\infty }\right)$$
8	6 7	syl	$$⊢N\in {\mathbb{N}}_0\to \left(\mathrm{+\infty }\le N\leftrightarrow N=\mathrm{+\infty }\right)$$
9		pnfnre	$$⊢\mathrm{+\infty }\notin ℝ$$
10		eleq1	$$⊢N=\mathrm{+\infty }\to \left(N\in {\mathbb{N}}_0\leftrightarrow \mathrm{+\infty }\in {\mathbb{N}}_0\right)$$
11		nn0re	$$⊢\mathrm{+\infty }\in {\mathbb{N}}_0\to \mathrm{+\infty }\in ℝ$$
12		pm2.24nel	$$⊢\mathrm{+\infty }\in ℝ\to \left(\mathrm{+\infty }\notin ℝ\to M\in {\mathbb{N}}_0\right)$$
13	11 12	syl	$$⊢\mathrm{+\infty }\in {\mathbb{N}}_0\to \left(\mathrm{+\infty }\notin ℝ\to M\in {\mathbb{N}}_0\right)$$
14	10 13	syl6bi	$$⊢N=\mathrm{+\infty }\to \left(N\in {\mathbb{N}}_0\to \left(\mathrm{+\infty }\notin ℝ\to M\in {\mathbb{N}}_0\right)\right)$$
15	14	com13	$$⊢\mathrm{+\infty }\notin ℝ\to \left(N\in {\mathbb{N}}_0\to \left(N=\mathrm{+\infty }\to M\in {\mathbb{N}}_0\right)\right)$$
16	9 15	ax-mp	$$⊢N\in {\mathbb{N}}_0\to \left(N=\mathrm{+\infty }\to M\in {\mathbb{N}}_0\right)$$
17	8 16	sylbid	$$⊢N\in {\mathbb{N}}_0\to \left(\mathrm{+\infty }\le N\to M\in {\mathbb{N}}_0\right)$$
18	17	adantl	$$⊢\left(M=\mathrm{+\infty }\wedge N\in {\mathbb{N}}_0\right)\to \left(\mathrm{+\infty }\le N\to M\in {\mathbb{N}}_0\right)$$
19	4 18	sylbid	$$⊢\left(M=\mathrm{+\infty }\wedge N\in {\mathbb{N}}_0\right)\to \left(M\le N\to M\in {\mathbb{N}}_0\right)$$
20	19	ex	$$⊢M=\mathrm{+\infty }\to \left(N\in {\mathbb{N}}_0\to \left(M\le N\to M\in {\mathbb{N}}_0\right)\right)$$
21	2 20	jaoi	$$⊢\left(M\in {\mathbb{N}}_0\vee M=\mathrm{+\infty }\right)\to \left(N\in {\mathbb{N}}_0\to \left(M\le N\to M\in {\mathbb{N}}_0\right)\right)$$
22	1 21	sylbi	$$⊢M\in {\mathbb{N}}_0^{*}\to \left(N\in {\mathbb{N}}_0\to \left(M\le N\to M\in {\mathbb{N}}_0\right)\right)$$
23	22	3imp	$$⊢\left(M\in {\mathbb{N}}_0^{*}\wedge N\in {\mathbb{N}}_0\wedge M\le N\right)\to M\in {\mathbb{N}}_0$$