Theorem xnn0lem1lt

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

	Ref	Expression
Assertion	xnn0lem1lt	|- ( ( M e. NN0 /\ N e. NN0* ) -> ( M <_ N <-> ( M - 1 ) < N ) )

Proof

Step	Hyp	Ref	Expression
1		nn0lem1lt	|- ( ( M e. NN0 /\ N e. NN0 ) -> ( M <_ N <-> ( M - 1 ) < N ) )
2	1	adantlr	|- ( ( ( M e. NN0 /\ N e. NN0* ) /\ N e. NN0 ) -> ( M <_ N <-> ( M - 1 ) < N ) )
3		nn0re	|- ( M e. NN0 -> M e. RR )
4	3	rexrd	|- ( M e. NN0 -> M e. RR* )
5		pnfge	|- ( M e. RR* -> M <_ +oo )
6	4 5	syl	|- ( M e. NN0 -> M <_ +oo )
7	6	ad2antrr	|- ( ( ( M e. NN0 /\ N e. NN0* ) /\ -. N e. NN0 ) -> M <_ +oo )
8		simpll	|- ( ( ( M e. NN0 /\ N e. NN0* ) /\ -. N e. NN0 ) -> M e. NN0 )
9		peano2rem	|- ( M e. RR -> ( M - 1 ) e. RR )
10		ltpnf	|- ( ( M - 1 ) e. RR -> ( M - 1 ) < +oo )
11	8 3 9 10	4syl	|- ( ( ( M e. NN0 /\ N e. NN0* ) /\ -. N e. NN0 ) -> ( M - 1 ) < +oo )
12	7 11	2thd	|- ( ( ( M e. NN0 /\ N e. NN0* ) /\ -. N e. NN0 ) -> ( M <_ +oo <-> ( M - 1 ) < +oo ) )
13		xnn0nnn0pnf	|- ( ( N e. NN0* /\ -. N e. NN0 ) -> N = +oo )
14	13	adantll	|- ( ( ( M e. NN0 /\ N e. NN0* ) /\ -. N e. NN0 ) -> N = +oo )
15	14	breq2d	|- ( ( ( M e. NN0 /\ N e. NN0* ) /\ -. N e. NN0 ) -> ( M <_ N <-> M <_ +oo ) )
16	14	breq2d	|- ( ( ( M e. NN0 /\ N e. NN0* ) /\ -. N e. NN0 ) -> ( ( M - 1 ) < N <-> ( M - 1 ) < +oo ) )
17	12 15 16	3bitr4d	|- ( ( ( M e. NN0 /\ N e. NN0* ) /\ -. N e. NN0 ) -> ( M <_ N <-> ( M - 1 ) < N ) )
18	2 17	pm2.61dan	|- ( ( M e. NN0 /\ N e. NN0* ) -> ( M <_ N <-> ( M - 1 ) < N ) )