Theorem zltp1le 7390

Description: Integer ordering relation.

Assertion

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

Proof of Theorem zltp1le

Step	Hyp	Ref	Expression
1		nn0ltp1le 7336	. . . . . 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		recn 6466	. . . . . . . . . . 11 |- (M e. RR -> M e. CC)
4		0cn 6481	. . . . . . . . . . . . 13 |- 0 e. CC
5		negcon1 6570	. . . . . . . . . . . . 13 |- ((M e. CC /\ 0 e. CC) -> (-uM = 0 <-> -u0 = M))
6	4, 5	mpan2 760	. . . . . . . . . . . 12 |- (M e. CC -> (-uM = 0 <-> -u0 = M))
7		neg0 6575	. . . . . . . . . . . . . 14 |- -u0 = 0
8	7	eqeq1i 1891	. . . . . . . . . . . . 13 |- (-u0 = M <-> 0 = M)
9		eqcom 1886	. . . . . . . . . . . . 13 |- (0 = M <-> M = 0)
10	8, 9	bitri 190	. . . . . . . . . . . 12 |- (-u0 = M <-> M = 0)
11	6, 10	syl6bb 595	. . . . . . . . . . 11 |- (M e. CC -> (-uM = 0 <-> M = 0))
12	3, 11	syl 12	. . . . . . . . . 10 |- (M e. RR -> (-uM = 0 <-> M = 0))
13	12	orbi2d 676	. . . . . . . . 9 |- (M e. RR -> ((-uM e. NN \/ -uM = 0) <-> (-uM e. NN \/ M = 0)))
14		elnn0 7310	. . . . . . . . 9 |- (-uM e. NN0 <-> (-uM e. NN \/ -uM = 0))
15	13, 14	syl5bb 591	. . . . . . . 8 |- (M e. RR -> (-uM e. NN0 <-> (-uM e. NN \/ M = 0)))
16		elnn0 7310	. . . . . . . . 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 690	. . . . . . 7 |- (M e. RR -> ((-uM e. NN0 /\ N e. NN0) <-> ((-uM e. NN \/ M = 0) /\ (N e. NN \/ N = 0))))
19	18	adantr 425	. . . . . 6 |- ((M e. RR /\ N e. RR) -> ((-uM e. NN0 /\ N e. NN0) <-> ((-uM e. NN \/ M = 0) /\ (N e. NN \/ N = 0))))
20		lt0neg1 6857	. . . . . . . . . . . . . . 15 |- (M e. RR -> (M < 0 <-> 0 < -uM))
21		nngt0 7129	. . . . . . . . . . . . . . 15 |- (-uM e. NN -> 0 < -uM)
22	20, 21	syl5bir 227	. . . . . . . . . . . . . 14 |- (M e. RR -> (-uM e. NN -> M < 0))
23	22	imp 377	. . . . . . . . . . . . 13 |- ((M e. RR /\ -uM e. NN) -> M < 0)
24		nngt0 7129	. . . . . . . . . . . . 13 |- (N e. NN -> 0 < N)
25	23, 24	anim12i 360	. . . . . . . . . . . 12 |- (((M e. RR /\ -uM e. NN) /\ N e. NN) -> (M < 0 /\ 0 < N))
26		0re 6603	. . . . . . . . . . . . . . 15 |- 0 e. RR
27		axlttrn 6673	. . . . . . . . . . . . . . 15 |- ((M e. RR /\ 0 e. RR /\ N e. RR) -> ((M < 0 /\ 0 < N) -> M < N))
28	26, 27	mp3an2 1179	. . . . . . . . . . . . . 14 |- ((M e. RR /\ N e. RR) -> ((M < 0 /\ 0 < N) -> M < N))
29		nnre 7112	. . . . . . . . . . . . . 14 |- (N e. NN -> N e. RR)
30	28, 29	sylan2 500	. . . . . . . . . . . . 13 |- ((M e. RR /\ N e. NN) -> ((M < 0 /\ 0 < N) -> M < N))
31	30	adantlr 429	. . . . . . . . . . . 12 |- (((M e. RR /\ -uM e. NN) /\ N e. NN) -> ((M < 0 /\ 0 < N) -> M < N))
32	25, 31	mpd 29	. . . . . . . . . . 11 |- (((M e. RR /\ -uM e. NN) /\ N e. NN) -> M < N)
33		peano2re 6599	. . . . . . . . . . . . 13 |- (M e. RR -> (M + 1) e. RR)
34	33	ad2antrr 440	. . . . . . . . . . . 12 |- (((M e. RR /\ -uM e. NN) /\ N e. NN) -> (M + 1) e. RR)
35		1re 6598	. . . . . . . . . . . . 13 |- 1 e. RR
36	35	a1i 8	. . . . . . . . . . . 12 |- (((M e. RR /\ -uM e. NN) /\ N e. NN) -> 1 e. RR)
37	29	adantl 424	. . . . . . . . . . . 12 |- (((M e. RR /\ -uM e. NN) /\ N e. NN) -> N e. RR)
38		ltle 6690	. . . . . . . . . . . . . . . . . 18 |- ((M e. RR /\ 0 e. RR) -> (M < 0 -> M <_ 0))
39	26, 38	mpan2 760	. . . . . . . . . . . . . . . . 17 |- (M e. RR -> (M < 0 -> M <_ 0))
40	39	adantr 425	. . . . . . . . . . . . . . . 16 |- ((M e. RR /\ -uM e. NN) -> (M < 0 -> M <_ 0))
41	23, 40	mpd 29	. . . . . . . . . . . . . . 15 |- ((M e. RR /\ -uM e. NN) -> M <_ 0)
42		leadd1 6808	. . . . . . . . . . . . . . . . 17 |- ((M e. RR /\ 0 e. RR /\ 1 e. RR) -> (M <_ 0 <-> (M + 1) <_ (0 + 1)))
43	26, 35, 42	mp3an23 1183	. . . . . . . . . . . . . . . 16 |- (M e. RR -> (M <_ 0 <-> (M + 1) <_ (0 + 1)))
44	43	adantr 425	. . . . . . . . . . . . . . 15 |- ((M e. RR /\ -uM e. NN) -> (M <_ 0 <-> (M + 1) <_ (0 + 1)))
45	41, 44	mpbid 212	. . . . . . . . . . . . . 14 |- ((M e. RR /\ -uM e. NN) -> (M + 1) <_ (0 + 1))
46		ax1cn 6422	. . . . . . . . . . . . . . 15 |- 1 e. CC
47	46	addid2i 6484	. . . . . . . . . . . . . 14 |- (0 + 1) = 1
48	45, 47	syl6breq 3376	. . . . . . . . . . . . 13 |- ((M e. RR /\ -uM e. NN) -> (M + 1) <_ 1)
49	48	adantr 425	. . . . . . . . . . . 12 |- (((M e. RR /\ -uM e. NN) /\ N e. NN) -> (M + 1) <_ 1)
50		nnge1 7126	. . . . . . . . . . . . 13 |- (N e. NN -> 1 <_ N)
51	50	adantl 424	. . . . . . . . . . . 12 |- (((M e. RR /\ -uM e. NN) /\ N e. NN) -> 1 <_ N)
52	34, 36, 37, 49, 51	letrd 6696	. . . . . . . . . . 11 |- (((M e. RR /\ -uM e. NN) /\ N e. NN) -> (M + 1) <_ N)
53	32, 52	jca 310	. . . . . . . . . 10 |- (((M e. RR /\ -uM e. NN) /\ N e. NN) -> (M < N /\ (M + 1) <_ N))
54	53	expl 420	. . . . . . . . 9 |- (M e. RR -> ((-uM e. NN /\ N e. NN) -> (M < N /\ (M + 1) <_ N)))
55		pm5.1 740	. . . . . . . . 9 |- ((M < N /\ (M + 1) <_ N) -> (M < N <-> (M + 1) <_ N))
56	54, 55	syl6 25	. . . . . . . 8 |- (M e. RR -> ((-uM e. NN /\ N e. NN) -> (M < N <-> (M + 1) <_ N)))
57	56	adantr 425	. . . . . . 7 |- ((M e. RR /\ N e. RR) -> ((-uM e. NN /\ N e. NN) -> (M < N <-> (M + 1) <_ N)))
58		breq1 3341	. . . . . . . . . . 11 |- (M = 0 -> (M < N <-> 0 < N))
59		opreq1 4889	. . . . . . . . . . . . 13 |- (M = 0 -> (M + 1) = (0 + 1))
60	59, 47	syl6eq 1944	. . . . . . . . . . . 12 |- (M = 0 -> (M + 1) = 1)
61	60	breq1d 3348	. . . . . . . . . . 11 |- (M = 0 -> ((M + 1) <_ N <-> 1 <_ N))
62	58, 61	bibi12d 691	. . . . . . . . . 10 |- (M = 0 -> ((M < N <-> (M + 1) <_ N) <-> (0 < N <-> 1 <_ N)))
63		pm5.1 740	. . . . . . . . . . 11 |- ((0 < N /\ 1 <_ N) -> (0 < N <-> 1 <_ N))
64	24, 50, 63	syl11anc 524	. . . . . . . . . 10 |- (N e. NN -> (0 < N <-> 1 <_ N))
65	62, 64	syl5bir 227	. . . . . . . . 9 |- (M = 0 -> (N e. NN -> (M < N <-> (M + 1) <_ N)))
66	65	imp 377	. . . . . . . 8 |- ((M = 0 /\ N e. NN) -> (M < N <-> (M + 1) <_ N))
67	66	a1i 8	. . . . . . 7 |- ((M e. RR /\ N e. RR) -> ((M = 0 /\ N e. NN) -> (M < N <-> (M + 1) <_ N)))
68		breq2 3342	. . . . . . . . . . 11 |- (N = 0 -> (M < N <-> M < 0))
69		breq2 3342	. . . . . . . . . . 11 |- (N = 0 -> ((M + 1) <_ N <-> (M + 1) <_ 0))
70	68, 69	bibi12d 691	. . . . . . . . . 10 |- (N = 0 -> ((M < N <-> (M + 1) <_ N) <-> (M < 0 <-> (M + 1) <_ 0)))
71		nn0ltlem1 7338	. . . . . . . . . . . . 13 |- ((0 e. NN0 /\ -uM e. NN0) -> (0 < -uM <-> 0 <_ (-uM - 1)))
72		0nn0 7322	. . . . . . . . . . . . 13 |- 0 e. NN0
73		nnnn0 7315	. . . . . . . . . . . . 13 |- (-uM e. NN -> -uM e. NN0)
74	71, 72, 73	sylancr 526	. . . . . . . . . . . 12 |- (-uM e. NN -> (0 < -uM <-> 0 <_ (-uM - 1)))
75	74	adantl 424	. . . . . . . . . . 11 |- ((M e. RR /\ -uM e. NN) -> (0 < -uM <-> 0 <_ (-uM - 1)))
76	20	adantr 425	. . . . . . . . . . 11 |- ((M e. RR /\ -uM e. NN) -> (M < 0 <-> 0 < -uM))
77		le0neg1 6859	. . . . . . . . . . . . . 14 |- ((M + 1) e. RR -> ((M + 1) <_ 0 <-> 0 <_ -u(M + 1)))
78	33, 77	syl 12	. . . . . . . . . . . . 13 |- (M e. RR -> ((M + 1) <_ 0 <-> 0 <_ -u(M + 1)))
79		negdi2 6621	. . . . . . . . . . . . . . 15 |- ((M e. CC /\ 1 e. CC) -> -u(M + 1) = (-uM - 1))
80	79, 3, 46	sylancl 525	. . . . . . . . . . . . . 14 |- (M e. RR -> -u(M + 1) = (-uM - 1))
81	80	breq2d 3350	. . . . . . . . . . . . 13 |- (M e. RR -> (0 <_ -u(M + 1) <-> 0 <_ (-uM - 1)))
82	78, 81	bitrd 587	. . . . . . . . . . . 12 |- (M e. RR -> ((M + 1) <_ 0 <-> 0 <_ (-uM - 1)))
83	82	adantr 425	. . . . . . . . . . 11 |- ((M e. RR /\ -uM e. NN) -> ((M + 1) <_ 0 <-> 0 <_ (-uM - 1)))
84	75, 76, 83	3bitr4d 609	. . . . . . . . . 10 |- ((M e. RR /\ -uM e. NN) -> (M < 0 <-> (M + 1) <_ 0))
85	70, 84	syl5cbir 228	. . . . . . . . 9 |- ((M e. RR /\ -uM e. NN) -> (N = 0 -> (M < N <-> (M + 1) <_ N)))
86	85	expimpd 404	. . . . . . . 8 |- (M e. RR -> ((-uM e. NN /\ N = 0) -> (M < N <-> (M + 1) <_ N)))
87	86	adantr 425	. . . . . . 7 |- ((M e. RR /\ N e. RR) -> ((-uM e. NN /\ N = 0) -> (M < N <-> (M + 1) <_ N)))
88	26	ltnri 6789	. . . . . . . . . 10 |- -. 0 < 0
89		lt01 6871	. . . . . . . . . . 11 |- 0 < 1
90	26, 35	ltnlei 6754	. . . . . . . . . . 11 |- (0 < 1 <-> -. 1 <_ 0)
91	89, 90	mpbi 206	. . . . . . . . . 10 |- -. 1 <_ 0
92	88, 91	2false 787	. . . . . . . . 9 |- (0 < 0 <-> 1 <_ 0)
93		breq2 3342	. . . . . . . . . . 11 |- (N = 0 -> (0 < N <-> 0 < 0))
94		breq2 3342	. . . . . . . . . . 11 |- (N = 0 -> (1 <_ N <-> 1 <_ 0))
95	93, 94	bibi12d 691	. . . . . . . . . 10 |- (N = 0 -> ((0 < N <-> 1 <_ N) <-> (0 < 0 <-> 1 <_ 0)))
96	62, 95	sylan9bb 599	. . . . . . . . 9 |- ((M = 0 /\ N = 0) -> ((M < N <-> (M + 1) <_ N) <-> (0 < 0 <-> 1 <_ 0)))
97	92, 96	mpbiri 211	. . . . . . . 8 |- ((M = 0 /\ N = 0) -> (M < N <-> (M + 1) <_ N))
98	97	a1i 8	. . . . . . 7 |- ((M e. RR /\ N e. RR) -> ((M = 0 /\ N = 0) -> (M < N <-> (M + 1) <_ N)))
99	57, 67, 87, 98	ccased 830	. . . . . 6 |- ((M e. RR /\ N e. RR) -> (((-uM e. NN \/ M = 0) /\ (N e. NN \/ N = 0)) -> (M < N <-> (M + 1) <_ N)))
100	19, 99	sylbid 220	. . . . 5 |- ((M e. RR /\ N e. RR) -> ((-uM e. NN0 /\ N e. NN0) -> (M < N <-> (M + 1) <_ N)))
101		simplr 449	. . . . . . . . . 10 |- (((M e. RR /\ N e. RR) /\ (M e. NN0 /\ -uN e. NN0)) -> N e. RR)
102	26	a1i 8	. . . . . . . . . 10 |- (((M e. RR /\ N e. RR) /\ (M e. NN0 /\ -uN e. NN0)) -> 0 e. RR)
103		simpll 448	. . . . . . . . . 10 |- (((M e. RR /\ N e. RR) /\ (M e. NN0 /\ -uN e. NN0)) -> M e. RR)
104		nn0ge0 7326	. . . . . . . . . . . . 13 |- (-uN e. NN0 -> 0 <_ -uN)
105	104	adantl 424	. . . . . . . . . . . 12 |- ((N e. RR /\ -uN e. NN0) -> 0 <_ -uN)
106		le0neg1 6859	. . . . . . . . . . . . 13 |- (N e. RR -> (N <_ 0 <-> 0 <_ -uN))
107	106	adantr 425	. . . . . . . . . . . 12 |- ((N e. RR /\ -uN e. NN0) -> (N <_ 0 <-> 0 <_ -uN))
108	105, 107	mpbird 213	. . . . . . . . . . 11 |- ((N e. RR /\ -uN e. NN0) -> N <_ 0)
109	108	ad2ant2l 444	. . . . . . . . . 10 |- (((M e. RR /\ N e. RR) /\ (M e. NN0 /\ -uN e. NN0)) -> N <_ 0)
110		nn0ge0 7326	. . . . . . . . . . 11 |- (M e. NN0 -> 0 <_ M)
111	110	ad2antrl 442	. . . . . . . . . 10 |- (((M e. RR /\ N e. RR) /\ (M e. NN0 /\ -uN e. NN0)) -> 0 <_ M)
112	101, 102, 103, 109, 111	letrd 6696	. . . . . . . . 9 |- (((M e. RR /\ N e. RR) /\ (M e. NN0 /\ -uN e. NN0)) -> N <_ M)
113		lenlt 6679	. . . . . . . . . . 11 |- ((N e. RR /\ M e. RR) -> (N <_ M <-> -. M < N))
114	113	ancoms 484	. . . . . . . . . 10 |- ((M e. RR /\ N e. RR) -> (N <_ M <-> -. M < N))
115	114	adantr 425	. . . . . . . . 9 |- (((M e. RR /\ N e. RR) /\ (M e. NN0 /\ -uN e. NN0)) -> (N <_ M <-> -. M < N))
116	112, 115	mpbid 212	. . . . . . . 8 |- (((M e. RR /\ N e. RR) /\ (M e. NN0 /\ -uN e. NN0)) -> -. M < N)
117		ltp1 6989	. . . . . . . . . . 11 |- (M e. RR -> M < (M + 1))
118	117	ad2antrr 440	. . . . . . . . . 10 |- (((M e. RR /\ N e. RR) /\ (M e. NN0 /\ -uN e. NN0)) -> M < (M + 1))
119		lelttr 6693	. . . . . . . . . . . . . 14 |- ((N e. RR /\ M e. RR /\ (M + 1) e. RR) -> ((N <_ M /\ M < (M + 1)) -> N < (M + 1)))
120	119	3expb 1068	. . . . . . . . . . . . 13 |- ((N e. RR /\ (M e. RR /\ (M + 1) e. RR)) -> ((N <_ M /\ M < (M + 1)) -> N < (M + 1)))
121	33	ancli 320	. . . . . . . . . . . . 13 |- (M e. RR -> (M e. RR /\ (M + 1) e. RR))
122	120, 121	sylan2 500	. . . . . . . . . . . 12 |- ((N e. RR /\ M e. RR) -> ((N <_ M /\ M < (M + 1)) -> N < (M + 1)))
123	122	ancoms 484	. . . . . . . . . . 11 |- ((M e. RR /\ N e. RR) -> ((N <_ M /\ M < (M + 1)) -> N < (M + 1)))
124	123	adantr 425	. . . . . . . . . 10 |- (((M e. RR /\ N e. RR) /\ (M e. NN0 /\ -uN e. NN0)) -> ((N <_ M /\ M < (M + 1)) -> N < (M + 1)))
125	112, 118, 124	mp2and 767	. . . . . . . . 9 |- (((M e. RR /\ N e. RR) /\ (M e. NN0 /\ -uN e. NN0)) -> N < (M + 1))
126		ltnle 6680	. . . . . . . . . . . 12 |- ((N e. RR /\ (M + 1) e. RR) -> (N < (M + 1) <-> -. (M + 1) <_ N))
127	126, 33	sylan2 500	. . . . . . . . . . 11 |- ((N e. RR /\ M e. RR) -> (N < (M + 1) <-> -. (M + 1) <_ N))
128	127	ancoms 484	. . . . . . . . . 10 |- ((M e. RR /\ N e. RR) -> (N < (M + 1) <-> -. (M + 1) <_ N))
129	128	adantr 425	. . . . . . . . 9 |- (((M e. RR /\ N e. RR) /\ (M e. NN0 /\ -uN e. NN0)) -> (N < (M + 1) <-> -. (M + 1) <_ N))
130	125, 129	mpbid 212	. . . . . . . 8 |- (((M e. RR /\ N e. RR) /\ (M e. NN0 /\ -uN e. NN0)) -> -. (M + 1) <_ N)
131	116, 130	jca 310	. . . . . . 7 |- (((M e. RR /\ N e. RR) /\ (M e. NN0 /\ -uN e. NN0)) -> (-. M < N /\ -. (M + 1) <_ N))
132	131	ex 402	. . . . . 6 |- ((M e. RR /\ N e. RR) -> ((M e. NN0 /\ -uN e. NN0) -> (-. M < N /\ -. (M + 1) <_ N)))
133		pm5.21 741	. . . . . 6 |- ((-. M < N /\ -. (M + 1) <_ N) -> (M < N <-> (M + 1) <_ N))
134	132, 133	syl6 25	. . . . 5 |- ((M e. RR /\ N e. RR) -> ((M e. NN0 /\ -uN e. NN0) -> (M < N <-> (M + 1) <_ N)))
135		nn0ltlem1 7338	. . . . . . . . 9 |- ((-uN e. NN0 /\ -uM e. NN0) -> (-uN < -uM <-> -uN <_ (-uM - 1)))
136	135	ancoms 484	. . . . . . . 8 |- ((-uM e. NN0 /\ -uN e. NN0) -> (-uN < -uM <-> -uN <_ (-uM - 1)))
137	136	adantl 424	. . . . . . 7 |- (((M e. RR /\ N e. RR) /\ (-uM e. NN0 /\ -uN e. NN0)) -> (-uN < -uM <-> -uN <_ (-uM - 1)))
138		ltneg 6844	. . . . . . . 8 |- ((M e. RR /\ N e. RR) -> (M < N <-> -uN < -uM))
139	138	adantr 425	. . . . . . 7 |- (((M e. RR /\ N e. RR) /\ (-uM e. NN0 /\ -uN e. NN0)) -> (M < N <-> -uN < -uM))
140		leneg 6846	. . . . . . . . . 10 |- (((M + 1) e. RR /\ N e. RR) -> ((M + 1) <_ N <-> -uN <_ -u(M + 1)))
141	140, 33	sylan 497	. . . . . . . . 9 |- ((M e. RR /\ N e. RR) -> ((M + 1) <_ N <-> -uN <_ -u(M + 1)))
142		negdi 6620	. . . . . . . . . . . . . 14 |- ((M e. CC /\ 1 e. CC) -> -u(M + 1) = (-uM + -u1))
143	46, 142	mpan2 760	. . . . . . . . . . . . 13 |- (M e. CC -> -u(M + 1) = (-uM + -u1))
144		negsub 6540	. . . . . . . . . . . . . 14 |- ((-uM e. CC /\ 1 e. CC) -> (-uM + -u1) = (-uM - 1))
145		negcl 6525	. . . . . . . . . . . . . 14 |- (M e. CC -> -uM e. CC)
146	144, 145, 46	sylancl 525	. . . . . . . . . . . . 13 |- (M e. CC -> (-uM + -u1) = (-uM - 1))
147	143, 146	eqtrd 1925	. . . . . . . . . . . 12 |- (M e. CC -> -u(M + 1) = (-uM - 1))
148	3, 147	syl 12	. . . . . . . . . . 11 |- (M e. RR -> -u(M + 1) = (-uM - 1))
149	148	breq2d 3350	. . . . . . . . . 10 |- (M e. RR -> (-uN <_ -u(M + 1) <-> -uN <_ (-uM - 1)))
150	149	adantr 425	. . . . . . . . 9 |- ((M e. RR /\ N e. RR) -> (-uN <_ -u(M + 1) <-> -uN <_ (-uM - 1)))
151	141, 150	bitrd 587	. . . . . . . 8 |- ((M e. RR /\ N e. RR) -> ((M + 1) <_ N <-> -uN <_ (-uM - 1)))
152	151	adantr 425	. . . . . . 7 |- (((M e. RR /\ N e. RR) /\ (-uM e. NN0 /\ -uN e. NN0)) -> ((M + 1) <_ N <-> -uN <_ (-uM - 1)))
153	137, 139, 152	3bitr4d 609	. . . . . 6 |- (((M e. RR /\ N e. RR) /\ (-uM e. NN0 /\ -uN e. NN0)) -> (M < N <-> (M + 1) <_ N))
154	153	ex 402	. . . . 5 |- ((M e. RR /\ N e. RR) -> ((-uM e. NN0 /\ -uN e. NN0) -> (M < N <-> (M + 1) <_ N)))
155	2, 100, 134, 154	ccased 830	. . . 4 |- ((M e. RR /\ N e. RR) -> (((M e. NN0 \/ -uM e. NN0) /\ (N e. NN0 \/ -uN e. NN0)) -> (M < N <-> (M + 1) <_ N)))
156	155	imp 377	. . 3 |- (((M e. RR /\ N e. RR) /\ ((M e. NN0 \/ -uM e. NN0) /\ (N e. NN0 \/ -uN e. NN0))) -> (M < N <-> (M + 1) <_ N))
157	156	an4s 566	. 2 |- (((M e. RR /\ (M e. NN0 \/ -uM e. NN0)) /\ (N e. RR /\ (N e. NN0 \/ -uN e. NN0))) -> (M < N <-> (M + 1) <_ N))
158		elznn0 7358	. 2 |- (M e. ZZ <-> (M e. RR /\ (M e. NN0 \/ -uM e. NN0)))
159		elznn0 7358	. 2 |- (N e. ZZ <-> (N e. RR /\ (N e. NN0 \/ -uN e. NN0)))
160	157, 158, 159	syl2anb 504	1 |- ((M e. ZZ /\ N e. ZZ) -> (M < N <-> (M + 1) <_ N))

Syntax hints:  -. wn 2   -> wi 3   <-> wb 163   \/ wo 239   /\ wa 240   = wceq 1298   e. wcel 1300   class class class wbr 3338  (class class class)co 4884  CCcc 6384  RRcr 6385  0cc0 6386  1c1 6387   + caddc 6389   - cmin 6445  -ucneg 6446   <_ cle 6448  NNcn 6449  NN0cn0 6450  ZZcz 6451   < clt 6653

This theorem is referenced by:  zleltp1 7391  zlem1lt 7392  recnz 7403  btwnnz 7404  uzind2 7418  eluzp1l 7603  cvg1 8173  bcpasci 8221  fsum1ps 8278  fsumsplit 8280  fsumcmpndx2 8302  serz1p 8312  iserzexi 8406  fzind 13610  fseq1cl 13619  divalglem6 13701  zgt1b2 13772  isprm3 13776  fzsplit 15792

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-13 1311  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-rep 3428  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524  ax-un 3790  ax-inf2 5731

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3or 859  df-3an 860  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-nel 2020  df-ral 2109  df-rex 2110  df-reu 2111  df-rab 2112  df-v 2294  df-sbc 2454  df-csb 2541  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-pss 2607  df-nul 2876  df-if 2983  df-pw 3035  df-sn 3049  df-pr 3050  df-tp 3052  df-op 3053  df-uni 3178  df-int 3215  df-iun 3257  df-br 3339  df-opab 3396  df-tr 3412  df-eprel 3583  df-id 3586  df-po 3591  df-so 3604  df-fr 3625  df-we 3644  df-ord 3660  df-on 3661  df-lim 3662  df-suc 3663  df-om 3950  df-xp 4000  df-rel 4001  df-cnv 4002  df-co 4003  df-dm 4004  df-rn 4005  df-res 4006  df-ima 4007  df-fun 4008  df-fn 4009  df-f 4010  df-f1 4011  df-fo 4012  df-f1o 4013  df-fv 4014  df-opr 4886  df-oprab 4887  df-mpt 5006  df-1st 5020  df-2nd 5021  df-iota 5089  df-rdg 5140  df-1o 5177  df-oadd 5179  df-omul 5180  df-er 5318  df-ec 5320  df-qs 5323  df-en 5427  df-dom 5428  df-sdom 5429  df-undef 5556  df-riota 5560  df-ni 6152  df-pli 6153  df-mi 6154  df-lti 6155  df-plpq 6187  df-mpq 6188  df-enq 6189  df-nq 6190  df-plq 6191  df-mq 6192  df-rq 6193  df-ltq 6194  df-1q 6195  df-np 6238  df-1p 6239  df-plp 6240  df-mp 6241  df-ltp 6242  df-plpr 6316  df-mpr 6317  df-enr 6318  df-nr 6319  df-plr 6320  df-mr 6321  df-ltr 6322  df-0r 6323  df-1r 6324  df-m1r 6325  df-c 6392  df-0 6393  df-1 6394  df-i 6395  df-r 6396  df-plus 6397  df-mul 6398  df-lt 6399  df-sub 6511  df-neg 6513  df-pnf 6654  df-mnf 6655  df-xr 6656  df-ltxr 6657  df-le 6658  df-n 7108  df-n0 7309  df-z 7345

Copyright terms: Public domain