Theorem xnn0lem1lt

Description: Extended nonnegative integer ordering relation. (Contributed by Thierry Arnoux, 30-Jul-2023)

	Ref	Expression
Assertion	xnn0lem1lt	$$⊢\left(M\in {\mathbb{N}}_0\wedge N\in {\mathbb{N}}_0^{*}\right)\to \left(M\le N\leftrightarrow M-1<N\right)$$

Proof

Step	Hyp	Ref	Expression
1		nn0lem1lt	$$⊢\left(M\in {\mathbb{N}}_0\wedge N\in {\mathbb{N}}_0\right)\to \left(M\le N\leftrightarrow M-1<N\right)$$
2	1	adantlr	$$⊢\left(\left(M\in {\mathbb{N}}_0\wedge N\in {\mathbb{N}}_0^{*}\right)\wedge N\in {\mathbb{N}}_0\right)\to \left(M\le N\leftrightarrow M-1<N\right)$$
3		nn0re	$$⊢M\in {\mathbb{N}}_0\to M\in ℝ$$
4	3	rexrd	$$⊢M\in {\mathbb{N}}_0\to M\in {ℝ}^{*}$$
5		pnfge	$$⊢M\in {ℝ}^{*}\to M\le \mathrm{+\infty }$$
6	4 5	syl	$$⊢M\in {\mathbb{N}}_0\to M\le \mathrm{+\infty }$$
7	6	ad2antrr	$$⊢\left(\left(M\in {\mathbb{N}}_0\wedge N\in {\mathbb{N}}_0^{*}\right)\wedge \neg N\in {\mathbb{N}}_0\right)\to M\le \mathrm{+\infty }$$
8		simpll	$$⊢\left(\left(M\in {\mathbb{N}}_0\wedge N\in {\mathbb{N}}_0^{*}\right)\wedge \neg N\in {\mathbb{N}}_0\right)\to M\in {\mathbb{N}}_0$$
9		peano2rem	$$⊢M\in ℝ\to M-1\in ℝ$$
10		ltpnf	$$⊢M-1\in ℝ\to M-1<\mathrm{+\infty }$$
11	8 3 9 10	4syl	$$⊢\left(\left(M\in {\mathbb{N}}_0\wedge N\in {\mathbb{N}}_0^{*}\right)\wedge \neg N\in {\mathbb{N}}_0\right)\to M-1<\mathrm{+\infty }$$
12	7 11	2thd	$$⊢\left(\left(M\in {\mathbb{N}}_0\wedge N\in {\mathbb{N}}_0^{*}\right)\wedge \neg N\in {\mathbb{N}}_0\right)\to \left(M\le \mathrm{+\infty }\leftrightarrow M-1<\mathrm{+\infty }\right)$$
13		xnn0nnn0pnf	$$⊢\left(N\in {\mathbb{N}}_0^{*}\wedge \neg N\in {\mathbb{N}}_0\right)\to N=\mathrm{+\infty }$$
14	13	adantll	$$⊢\left(\left(M\in {\mathbb{N}}_0\wedge N\in {\mathbb{N}}_0^{*}\right)\wedge \neg N\in {\mathbb{N}}_0\right)\to N=\mathrm{+\infty }$$
15	14	breq2d	$$⊢\left(\left(M\in {\mathbb{N}}_0\wedge N\in {\mathbb{N}}_0^{*}\right)\wedge \neg N\in {\mathbb{N}}_0\right)\to \left(M\le N\leftrightarrow M\le \mathrm{+\infty }\right)$$
16	14	breq2d	$$⊢\left(\left(M\in {\mathbb{N}}_0\wedge N\in {\mathbb{N}}_0^{*}\right)\wedge \neg N\in {\mathbb{N}}_0\right)\to \left(M-1<N\leftrightarrow M-1<\mathrm{+\infty }\right)$$
17	12 15 16	3bitr4d	$$⊢\left(\left(M\in {\mathbb{N}}_0\wedge N\in {\mathbb{N}}_0^{*}\right)\wedge \neg N\in {\mathbb{N}}_0\right)\to \left(M\le N\leftrightarrow M-1<N\right)$$
18	2 17	pm2.61dan	$$⊢\left(M\in {\mathbb{N}}_0\wedge N\in {\mathbb{N}}_0^{*}\right)\to \left(M\le N\leftrightarrow M-1<N\right)$$