Theorem zltp1let 6136

Description: Integer ordering relation.

Assertion

Ref	Expression
zltp1let	|- ((M e. ZZ /\ N e. ZZ) -> (M < N <-> (M + 1) <_ N))

Proof of Theorem zltp1let

Step	Hyp	Ref	Expression
1		nn0ltp1let 6082	. . . . . 6 |- ((M e. NN0 /\ N e. NN0) -> (M < N <-> (M + 1) <_ N))
2	1	a1i 8	. . . . 5 |- ((M e. RR /\ N e. RR) -> ((M e. NN0 /\ N e. NN0) -> (M < N <-> (M + 1) <_ N)))
3		recnt 5293	. . . . . . . . . . 11 |- (M e. RR -> M e. CC)
4		0cn 5308	. . . . . . . . . . . . 13 |- 0 e. CC
5		negcon1t 5390	. . . . . . . . . . . . 13 |- ((M e. CC /\ 0 e. CC) -> (-uM = 0 <-> -u0 = M))
6	4, 5	mpan2 695	. . . . . . . . . . . 12 |- (M e. CC -> (-uM = 0 <-> -u0 = M))
7		neg0 5395	. . . . . . . . . . . . . 14 |- -u0 = 0
8	7	eqeq1i 1479	. . . . . . . . . . . . 13 |- (-u0 = M <-> 0 = M)
9		eqcom 1474	. . . . . . . . . . . . 13 |- (0 = M <-> M = 0)
10	8, 9	bitr 173	. . . . . . . . . . . 12 |- (-u0 = M <-> M = 0)
11	6, 10	syl6bb 535	. . . . . . . . . . 11 |- (M e. CC -> (-uM = 0 <-> M = 0))
12	3, 11	syl 10	. . . . . . . . . 10 |- (M e. RR -> (-uM = 0 <-> M = 0))
13	12	orbi2d 613	. . . . . . . . 9 |- (M e. RR -> ((-uM e. NN \/ -uM = 0) <-> (-uM e. NN \/ M = 0)))
14		elnn0 6056	. . . . . . . . 9 |- (-uM e. NN0 <-> (-uM e. NN \/ -uM = 0))
15	13, 14	syl5bb 531	. . . . . . . 8 |- (M e. RR -> (-uM e. NN0 <-> (-uM e. NN \/ M = 0)))
16		elnn0 6056	. . . . . . . . 9 |- (N e. NN0 <-> (N e. NN \/ N = 0))
17	16	a1i 8	. . . . . . . 8 |- (M e. RR -> (N e. NN0 <-> (N e. NN \/ N = 0)))
18	15, 17	anbi12d 627	. . . . . . 7 |- (M e. RR -> ((-uM e. NN0 /\ N e. NN0) <-> ((-uM e. NN \/ M = 0) /\ (N e. NN \/ N = 0))))
19	18	adantr 389	. . . . . 6 |- ((M e. RR /\ N e. RR) -> ((-uM e. NN0 /\ N e. NN0) <-> ((-uM e. NN \/ M = 0) /\ (N e. NN \/ N = 0))))
20		lt0neg1t 5649	. . . . . . . . . . . . . . . 16 |- (M e. RR -> (M < 0 <-> 0 < -uM))
21		nngt0t 5902	. . . . . . . . . . . . . . . 16 |- (-uM e. NN -> 0 < -uM)
22	20, 21	syl5bir 210	. . . . . . . . . . . . . . 15 |- (M e. RR -> (-uM e. NN -> M < 0))
23	22	imp 350	. . . . . . . . . . . . . 14 |- ((M e. RR /\ -uM e. NN) -> M < 0)
24		nngt0t 5902	. . . . . . . . . . . . . 14 |- (N e. NN -> 0 < N)
25	23, 24	anim12i 333	. . . . . . . . . . . . 13 |- (((M e. RR /\ -uM e. NN) /\ N e. NN) -> (M < 0 /\ 0 < N))
26		0re 5420	. . . . . . . . . . . . . . . 16 |- 0 e. RR
27		axlttrn 5484	. . . . . . . . . . . . . . . 16 |- ((M e. RR /\ 0 e. RR /\ N e. RR) -> ((M < 0 /\ 0 < N) -> M < N))
28	26, 27	mp3an2 902	. . . . . . . . . . . . . . 15 |- ((M e. RR /\ N e. RR) -> ((M < 0 /\ 0 < N) -> M < N))
29		nnret 5885	. . . . . . . . . . . . . . 15 |- (N e. NN -> N e. RR)
30	28, 29	sylan2 451	. . . . . . . . . . . . . 14 |- ((M e. RR /\ N e. NN) -> ((M < 0 /\ 0 < N) -> M < N))
31	30	adantlr 393	. . . . . . . . . . . . 13 |- (((M e. RR /\ -uM e. NN) /\ N e. NN) -> ((M < 0 /\ 0 < N) -> M < N))
32	25, 31	mpd 26	. . . . . . . . . . . 12 |- (((M e. RR /\ -uM e. NN) /\ N e. NN) -> M < N)
33		peano2re 5416	. . . . . . . . . . . . . 14 |- (M e. RR -> (M + 1) e. RR)
34	33	ad2antrr 404	. . . . . . . . . . . . 13 |- (((M e. RR /\ -uM e. NN) /\ N e. NN) -> (M + 1) e. RR)
35		1re 5415	. . . . . . . . . . . . . 14 |- 1 e. RR
36	35	a1i 8	. . . . . . . . . . . . 13 |- (((M e. RR /\ -uM e. NN) /\ N e. NN) -> 1 e. RR)
37	29	adantl 388	. . . . . . . . . . . . 13 |- (((M e. RR /\ -uM e. NN) /\ N e. NN) -> N e. RR)
38		ltlet 5501	. . . . . . . . . . . . . . . . . . 19 |- ((M e. RR /\ 0 e. RR) -> (M < 0 -> M <_ 0))
39	26, 38	mpan2 695	. . . . . . . . . . . . . . . . . 18 |- (M e. RR -> (M < 0 -> M <_ 0))
40	39	adantr 389	. . . . . . . . . . . . . . . . 17 |- ((M e. RR /\ -uM e. NN) -> (M < 0 -> M <_ 0))
41	23, 40	mpd 26	. . . . . . . . . . . . . . . 16 |- ((M e. RR /\ -uM e. NN) -> M <_ 0)
42		leadd1t 5607	. . . . . . . . . . . . . . . . . 18 |- ((M e. RR /\ 0 e. RR /\ 1 e. RR) -> (M <_ 0 <-> (M + 1) <_ (0 + 1)))
43	26, 35, 42	mp3an23 906	. . . . . . . . . . . . . . . . 17 |- (M e. RR -> (M <_ 0 <-> (M + 1) <_ (0 + 1)))
44	43	adantr 389	. . . . . . . . . . . . . . . 16 |- ((M e. RR /\ -uM e. NN) -> (M <_ 0 <-> (M + 1) <_ (0 + 1)))
45	41, 44	mpbid 195	. . . . . . . . . . . . . . 15 |- ((M e. RR /\ -uM e. NN) -> (M + 1) <_ (0 + 1))
46		ax1cn 5249	. . . . . . . . . . . . . . . 16 |- 1 e. CC
47	46	addid2 5311	. . . . . . . . . . . . . . 15 |- (0 + 1) = 1
48	45, 47	syl6breq 2649	. . . . . . . . . . . . . 14 |- ((M e. RR /\ -uM e. NN) -> (M + 1) <_ 1)
49	48	adantr 389	. . . . . . . . . . . . 13 |- (((M e. RR /\ -uM e. NN) /\ N e. NN) -> (M + 1) <_ 1)
50		nnge1t 5899	. . . . . . . . . . . . . 14 |- (N e. NN -> 1 <_ N)
51	50	adantl 388	. . . . . . . . . . . . 13 |- (((M e. RR /\ -uM e. NN) /\ N e. NN) -> 1 <_ N)
52	34, 36, 37, 49, 51	letrd 5507	. . . . . . . . . . . 12 |- (((M e. RR /\ -uM e. NN) /\ N e. NN) -> (M + 1) <_ N)
53	32, 52	jca 288	. . . . . . . . . . 11 |- (((M e. RR /\ -uM e. NN) /\ N e. NN) -> (M < N /\ (M + 1) <_ N))
54	53	exp31 376	. . . . . . . . . 10 |- (M e. RR -> (-uM e. NN -> (N e. NN -> (M < N /\ (M + 1) <_ N))))
55	54	imp3a 361	. . . . . . . . 9 |- (M e. RR -> ((-uM e. NN /\ N e. NN) -> (M < N /\ (M + 1) <_ N)))
56		pm5.1 675	. . . . . . . . 9 |- ((M < N /\ (M + 1) <_ N) -> (M < N <-> (M + 1) <_ N))
57	55, 56	syl6 22	. . . . . . . 8 |- (M e. RR -> ((-uM e. NN /\ N e. NN) -> (M < N <-> (M + 1) <_ N)))
58	57	adantr 389	. . . . . . 7 |- ((M e. RR /\ N e. RR) -> ((-uM e. NN /\ N e. NN) -> (M < N <-> (M + 1) <_ N)))
59		breq1 2617	. . . . . . . . . . 11 |- (M = 0 -> (M < N <-> 0 < N))
60		opreq1 3959	. . . . . . . . . . . . 13 |- (M = 0 -> (M + 1) = (0 + 1))
61	60, 47	syl6eq 1520	. . . . . . . . . . . 12 |- (M = 0 -> (M + 1) = 1)
62	61	breq1d 2624	. . . . . . . . . . 11 |- (M = 0 -> ((M + 1) <_ N <-> 1 <_ N))
63	59, 62	bibi12d 628	. . . . . . . . . 10 |- (M = 0 -> ((M < N <-> (M + 1) <_ N) <-> (0 < N <-> 1 <_ N)))
64		pm5.1 675	. . . . . . . . . . 11 |- ((0 < N /\ 1 <_ N) -> (0 < N <-> 1 <_ N))
65	64, 24, 50	sylanc 471	. . . . . . . . . 10 |- (N e. NN -> (0 < N <-> 1 <_ N))
66	63, 65	syl5bir 210	. . . . . . . . 9 |- (M = 0 -> (N e. NN -> (M < N <-> (M + 1) <_ N)))
67	66	imp 350	. . . . . . . 8 |- ((M = 0 /\ N e. NN) -> (M < N <-> (M + 1) <_ N))
68	67	a1i 8	. . . . . . 7 |- ((M e. RR /\ N e. RR) -> ((M = 0 /\ N e. NN) -> (M < N <-> (M + 1) <_ N)))
69		breq2 2618	. . . . . . . . . . . 12 |- (N = 0 -> (M < N <-> M < 0))
70		breq2 2618	. . . . . . . . . . . 12 |- (N = 0 -> ((M + 1) <_ N <-> (M + 1) <_ 0))
71	69, 70	bibi12d 628	. . . . . . . . . . 11 |- (N = 0 -> ((M < N <-> (M + 1) <_ N) <-> (M < 0 <-> (M + 1) <_ 0)))
72		nnnn0t 6061	. . . . . . . . . . . . . 14 |- (-uM e. NN -> -uM e. NN0)
73		0nn0 6068	. . . . . . . . . . . . . . 15 |- 0 e. NN0
74		nn0ltlem1t 6084	. . . . . . . . . . . . . . 15 |- ((0 e. NN0 /\ -uM e. NN0) -> (0 < -uM <-> 0 <_ (-uM - 1)))
75	73, 74	mpan 694	. . . . . . . . . . . . . 14 |- (-uM e. NN0 -> (0 < -uM <-> 0 <_ (-uM - 1)))
76	72, 75	syl 10	. . . . . . . . . . . . 13 |- (-uM e. NN -> (0 < -uM <-> 0 <_ (-uM - 1)))
77	76	adantl 388	. . . . . . . . . . . 12 |- ((M e. RR /\ -uM e. NN) -> (0 < -uM <-> 0 <_ (-uM - 1)))
78	20	adantr 389	. . . . . . . . . . . 12 |- ((M e. RR /\ -uM e. NN) -> (M < 0 <-> 0 < -uM))
79		le0neg1t 5651	. . . . . . . . . . . . . . 15 |- ((M + 1) e. RR -> ((M + 1) <_ 0 <-> 0 <_ -u(M + 1)))
80	33, 79	syl 10	. . . . . . . . . . . . . 14 |- (M e. RR -> ((M + 1) <_ 0 <-> 0 <_ -u(M + 1)))
81		negdi2t 5436	. . . . . . . . . . . . . . . . 17 |- ((M e. CC /\ 1 e. CC) -> -u(M + 1) = (-uM - 1))
82	46, 81	mpan2 695	. . . . . . . . . . . . . . . 16 |- (M e. CC -> -u(M + 1) = (-uM - 1))
83	3, 82	syl 10	. . . . . . . . . . . . . . 15 |- (M e. RR -> -u(M + 1) = (-uM - 1))
84	83	breq2d 2625	. . . . . . . . . . . . . 14 |- (M e. RR -> (0 <_ -u(M + 1) <-> 0