Theorem nnleltp1 6100

Description: Natural number ordering relation.

Assertion

Ref	Expression
nnleltp1	|- ((A e. NN /\ B e. NN) -> (A <_ B <-> A < (B + 1)))

Proof of Theorem nnleltp1

Step	Hyp	Ref	Expression
1		leloe 5672	. . 3 |- ((A e. RR /\ B e. RR) -> (A <_ B <-> (A < B \/ A = B)))
2		nnre 6074	. . 3 |- (A e. NN -> A e. RR)
3		nnre 6074	. . 3 |- (B e. NN -> B e. RR)
4	1, 2, 3	syl2an 456	. 2 |- ((A e. NN /\ B e. NN) -> (A <_ B <-> (A < B \/ A = B)))
5		lt01 5836	. . . . . . 7 |- 0 < 1
6		0re 5594	. . . . . . . 8 |- 0 e. RR
7		1re 5589	. . . . . . . 8 |- 1 e. RR
8		lt2add 5797	. . . . . . . . 9 |- (((A e. RR /\ 0 e. RR) /\ (B e. RR /\ 1 e. RR)) -> ((A < B /\ 0 < 1) -> (A + 0) < (B + 1)))
9	8	an4s 511	. . . . . . . 8 |- (((A e. RR /\ B e. RR) /\ (0 e. RR /\ 1 e. RR)) -> ((A < B /\ 0 < 1) -> (A + 0) < (B + 1)))
10	6, 7, 9	mpanr12 715	. . . . . . 7 |- ((A e. RR /\ B e. RR) -> ((A < B /\ 0 < 1) -> (A + 0) < (B + 1)))
11	5, 10	mpan2i 703	. . . . . 6 |- ((A e. RR /\ B e. RR) -> (A < B -> (A + 0) < (B + 1)))
12		pm3.26 317	. . . . . . . 8 |- ((A e. RR /\ B e. RR) -> A e. RR)
13		recn 5467	. . . . . . . 8 |- (A e. RR -> A e. CC)
14		addid1 5464	. . . . . . . 8 |- (A e. CC -> (A + 0) = A)
15	12, 13, 14	3syl 20	. . . . . . 7 |- ((A e. RR /\ B e. RR) -> (A + 0) = A)
16	15	breq1d 2702	. . . . . 6 |- ((A e. RR /\ B e. RR) -> ((A + 0) < (B + 1) <-> A < (B + 1)))
17	11, 16	sylibd 200	. . . . 5 |- ((A e. RR /\ B e. RR) -> (A < B -> A < (B + 1)))
18		breq1 2695	. . . . . . 7 |- (A = B -> (A < (B + 1) <-> B < (B + 1)))
19		ltp1 5951	. . . . . . 7 |- (B e. RR -> B < (B + 1))
20	18, 19	syl5cbir 209	. . . . . 6 |- (B e. RR -> (A = B -> A < (B + 1)))
21	20	adantl 388	. . . . 5 |- ((A e. RR /\ B e. RR) -> (A = B -> A < (B + 1)))
22	17, 21	jaod 424	. . . 4 |- ((A e. RR /\ B e. RR) -> ((A < B \/ A = B) -> A < (B + 1)))
23	22, 2, 3	syl2an 456	. . 3 |- ((A e. NN /\ B e. NN) -> ((A < B \/ A = B) -> A < (B + 1)))
24		breq1 2695	. . . . . . 7 |- (z = A -> (z < (B + 1) <-> A < (B + 1)))
25		breq1 2695	. . . . . . . 8 |- (z = A -> (z < B <-> A < B))
26		eqeq1 1524	. . . . . . . 8 |- (z = A -> (z = B <-> A = B))
27	25, 26	orbi12d 630	. . . . . . 7 |- (z = A -> ((z < B \/ z = B) <-> (A < B \/ A = B)))
28	24, 27	imbi12d 629	. . . . . 6 |- (z = A -> ((z < (B + 1) -> (z < B \/ z = B)) <-> (A < (B + 1) -> (A < B \/ A = B))))
29	28	rcla4v 1919	. . . . 5 |- (A e. NN -> (A.z e. NN (z < (B + 1) -> (z < B \/ z = B)) -> (A < (B + 1) -> (A < B \/ A = B))))
30		opreq1 4026	. . . . . . . . 9 |- (x = 1 -> (x + 1) = (1 + 1))
31	30	breq2d 2703	. . . . . . . 8 |- (x = 1 -> (z < (x + 1) <-> z < (1 + 1)))
32		breq2 2696	. . . . . . . . 9 |- (x = 1 -> (z < x <-> z < 1))
33		eqeq2 1527	. . . . . . . . 9 |- (x = 1 -> (z = x <-> z = 1))
34	32, 33	orbi12d 630	. . . . . . . 8 |- (x = 1 -> ((z < x \/ z = x) <-> (z < 1 \/ z = 1)))
35	31, 34	imbi12d 629	. . . . . . 7 |- (x = 1 -> ((z < (x + 1) -> (z < x \/ z = x)) <-> (z < (1 + 1) -> (z < 1 \/ z = 1))))
36	35	ralbidv 1709	. . . . . 6 |- (x = 1 -> (A.z e. NN (z < (x + 1) -> (z < x \/ z = x)) <-> A.z e. NN (z < (1 + 1) -> (z < 1 \/ z = 1))))
37		opreq1 4026	. . . . . . . . 9 |- (x = y -> (x + 1) = (y + 1))
38	37	breq2d 2703	. . . . . . . 8 |- (x = y -> (z < (x + 1) <-> z < (y + 1)))
39		breq2 2696	. . . . . . . . 9 |- (x = y -> (z < x <-> z < y))
40		eqeq2 1527	. . . . . . . . 9 |- (x = y -> (z = x <-> z = y))
41	39, 40	orbi12d 630	. . . . . . . 8 |- (x = y -> ((z < x \/ z = x) <-> (z < y \/ z = y)))
42	38, 41	imbi12d 629	. . . . . . 7 |- (x = y -> ((z < (x + 1) -> (z < x \/ z = x)) <-> (z < (y + 1) -> (z < y \/ z = y))))
43	42	ralbidv 1709	. . . . . 6 |- (x = y -> (A.z e. NN (z < (x + 1) -> (z < x \/ z = x)) <-> A.z e. NN (z < (y + 1) -> (z < y \/ z = y))))
44		opreq1 4026	. . . . . . . . 9 |- (x = (y + 1) -> (x + 1) = ((y + 1) + 1))
45	44	breq2d 2703	. . . . . . . 8 |- (x = (y + 1) -> (z < (x + 1) <-> z < ((y + 1) + 1)))
46		breq2 2696	. . . . . . . . 9 |- (x = (y + 1) -> (z < x <-> z < (y + 1)))
47		eqeq2 1527	. . . . . . . . 9 |- (x = (y + 1) -> (z = x <-> z = (y + 1)))
48	46, 47	orbi12d 630	. . . . . . . 8 |- (x = (y + 1) -> ((z < x \/ z = x) <-> (z < (y + 1) \/ z = (y + 1))))
49	45, 48	imbi12d 629	. . . . . . 7 |- (x = (y + 1) -> ((z < (x + 1) -> (z < x \/ z = x)) <-> (z < ((y + 1) + 1) -> (z < (y + 1) \/ z = (y + 1)))))
50	49	ralbidv 1709	. . . . . 6 |- (x = (y + 1) -> (A.z e. NN (z < (x + 1) -> (z < x \/ z = x)) <-> A.z e. NN (z < ((y + 1) + 1) -> (z < (y + 1) \/ z = (y + 1)))))
51		opreq1 4026	. . . . . . . . 9 |- (x = B -> (x + 1) = (B + 1))
52	51	breq2d 2703	. . . . . . . 8 |- (x = B -> (z < (x + 1) <-> z < (B + 1)))
53		breq2 2696	. . . . . . . . 9 |- (x = B -> (z < x <-> z < B))
54		eqeq2 1527	. . . . . . . . 9 |- (x = B -> (z = x <-> z = B))
55	53, 54	orbi12d 630	. . . . . . . 8 |- (x = B -> ((z < x \/ z = x) <-> (z < B \/ z = B)))
56	52, 55	imbi12d 629	. . . . . . 7 |- (x = B -> ((z < (x + 1) -> (z < x \/ z = x)) <-> (z < (B + 1) -> (z < B \/ z = B))))
57	56	ralbidv 1709	. . . . . 6 |- (x = B -> (A.z e. NN (z < (x + 1) -> (z < x \/ z = x)) <-> A.z e. NN (z < (B + 1) -> (z < B \/ z = B))))
58		breq1 2695	. . . . . . . . 9 |- (x = 1 -> (x < (1 + 1) <-> 1 < (1 + 1)))
59		breq1 2695	. . . . . . . . . 10 |- (x = 1 -> (x < 1 <-> 1 < 1))
60		eqeq1 1524	. . . . . . . . . 10 |- (x = 1 -> (x = 1 <-> 1 = 1))
61	59, 60	orbi12d 630	. . . . . . . . 9 |- (x = 1 -> ((x < 1 \/ x = 1) <-> (1 < 1 \/ 1 = 1)))
62	58, 61	imbi12d 629	. . . . . . . 8 |- (x = 1 -> ((x < (1 + 1) -> (x < 1 \/ x = 1)) <-> (1 < (1 + 1) -> (1 < 1 \/ 1 = 1))))
63		breq1 2695	. . . . . . . . 9 |- (x = (y + 1) -> (x < (1 + 1) <-> (y + 1) < (1 + 1)))
64		breq1 2695	. . . . . . . . . 10 |- (x = (y + 1) -> (x < 1 <-> (y + 1) < 1))
65		eqeq1 1524	. . . . . . . . . 10 |- (x = (y + 1) -> (x = 1 <-> (y + 1) = 1))
66	64, 65	orbi12d 630	. . . . . . . . 9 |- (x = (y + 1) -> ((x < 1 \/ x = 1) <-> ((y + 1) < 1 \/ (y + 1) = 1)))
67	63, 66	imbi12d 629	. . . . . . . 8 |- (x = (y + 1) -> ((x < (1 + 1) -> (x < 1 \/ x = 1)) <-> ((y + 1) < (1 + 1) -> ((y + 1) < 1 \/ (y + 1) = 1))))
68		breq1 2695	. . . . . . . . 9 |- (x = z -> (x < (1 + 1) <-> z < (1 + 1)))
69		breq1 2695	. . . . . . . . . 10 |- (x = z -> (x < 1 <-> z < 1))
70		eqeq1 1524	. . . . . . . . . 10 |- (x = z -> (x = 1 <-> z = 1))
71	69, 70	orbi12d 630	. . . . . . . . 9 |- (x = z -> ((x < 1 \/ x = 1) <-> (z < 1 \/ z = 1)))
72	68, 71	imbi12d 629	. . . . . . . 8 |- (x = z -> ((x < (1 + 1) -> (x < 1 \/ x = 1)) <-> (z < (1 + 1) -> (z < 1 \/ z = 1))))
73		eqid 1518	. . . . . . . . . 10 |- 1 = 1
74	73	olci 269	. . . . . . . . 9 |- (1 < 1 \/ 1 = 1)
75	74	a1i 8	. . . . . . . 8 |- (1 < (1 + 1) -> (1 < 1 \/ 1 = 1))
76		nnre 6074	. . . . . . . . . 10 |- (y e. NN -> y e. RR)
77		ltadd1 5777	. . . . . . . . . . 11 |- ((y e. RR /\ 1 e. RR /\ 1 e. RR) -> (y < 1 <-> (y + 1) < (1 + 1)))
78	7, 7, 77	mp3an23 914	. . . . . . . . . 10 |- (y e. RR -> (y < 1 <-> (y + 1) < (1 + 1)))
79	76, 78	syl 10	. . . . . . . . 9 |- (y e. NN -> (y < 1 <-> (y + 1) < (1 + 1)))
80		nnge1 6088	. . . . . . . . . . 11 |- (y e. NN -> 1 <_ y)
81		lenlt 5664	. . . . . . . . . . . . 13 |- ((1 e. RR /\ y e. RR) -> (1 <_ y <-> -. y < 1))
82	7, 81	mpan 699	. . . . . . . . . . . 12 |- (y e. RR -> (1 <_ y <-> -. y < 1))
83	76, 82	syl 10	. . . . . . . . . . 11 |- (y e. NN -> (1 <_ y <-> -. y < 1))
84	80, 83	mpbid 193	. . . . . . . . . 10 |- (y e. NN -> -. y < 1)
85	84	pm2.21d 78	. . . . . . . . 9 |- (y e. NN -> (y < 1 -> ((y + 1) < 1 \/ (y + 1) = 1)))
86	79, 85	sylbird 203	. . . . . . . 8 |- (y e. NN -> ((y + 1) < (1 + 1) -> ((y + 1) < 1 \/ (y + 1) = 1)))
87	62, 67, 72, 75, 86	nn1suc 6084	. . . . . . 7 |- (z e. NN -> (z < (1 + 1) -> (z < 1 \/ z = 1)))
88	87	rgen 1744	. . . . . 6 |- A.z e. NN (z < (1 + 1) -> (z < 1 \/ z = 1))
89		breq1 2695	. . . . . . . . . . . . 13 |- (x = 1 -> (x < ((y + 1) + 1) <-> 1 < ((y + 1) + 1)))
90		breq1 2695	. . . . . . . . . . . . . 14 |- (x = 1 -> (x < (y + 1) <-> 1 < (y + 1)))
91		eqeq1 1524	. . . . . . . . . . . . . 14 |- (x = 1 -> (x = (y + 1) <-> 1 = (y + 1)))
92	90, 91	orbi12d 630	. . . . . . . . . . . . 13 |- (x = 1 -> ((x < (y + 1) \/ x = (y + 1)) <-> (1 < (y + 1) \/ 1 = (y + 1))))
93	89, 92	imbi12d 629	. . . . . . . . . . . 12 |- (x = 1 -> ((x < ((y + 1) + 1) -> (x < (y + 1) \/ x = (y + 1))) <-> (1 < ((y + 1) + 1) -> (1 < (y + 1) \/ 1 = (y + 1)))))
94	93	imbi2d 615	. . . . . . . . . . 11 |- (x = 1 -> (((y e. NN /\ A.w e. NN (w < (y + 1) -> (w < y \/ w = y))) -> (x < ((y + 1) + 1) -> (x < (y + 1) \/ x = (y + 1)))) <-> ((y e. NN /\ A.w e. NN (w < (y + 1) -> (w < y \/ w = y))) -> (1 < ((y + 1) + 1) -> (1 < (y + 1) \/ 1 = (y + 1))))))
95		breq1 2695	. . . . . . . . . . . . 13 |- (x = (v + 1) -> (x < ((y + 1) + 1) <-> (v + 1) < ((y + 1) + 1)))
96		breq1 2695	. . . . . . . . . . . . . 14 |- (x = (v + 1) -> (x < (y + 1) <-> (v + 1) < (y + 1)))
97		eqeq1 1524	. . . . . . . . . . . . . 14 |- (x = (v + 1) -> (x = (y + 1) <-> (v + 1) = (y + 1)))
98	96, 97	orbi12d 630	. . . . . . . . . . . . 13 |- (x = (v + 1) -> ((x < (y + 1) \/ x = (y + 1)) <-> ((v + 1) < (y + 1) \/ (v + 1) = (y + 1))))
99	95, 98	imbi12d 629	. . . . . . . . . . . 12 |- (x = (v + 1) -> ((x < ((y + 1) + 1) -> (x < (y + 1) \/ x = (y + 1))) <-> ((v + 1) < ((y + 1) + 1) -> ((v + 1) < (y + 1) \/ (v + 1) = (y + 1)))))
100	99	imbi2d 615	. . . . . . . . . . 11 |- (x = (v + 1) -> (((y e. NN /\ A.w e. NN (w < (y + 1) -> (w < y \/ w = y))) -> (x < ((y + 1) + 1) -> (x < (y + 1) \/ x = (y + 1)))) <-> ((y e. NN /\ A.w e. NN (w < (y + 1) -> (w < y \/ w = y))) -> ((v + 1) < ((y + 1) + 1) -> ((v + 1) < (y + 1) \/ (v + 1) = (y + 1))))))
101		breq1 2695	. . . . . . . . . . . . 13 |- (x = z -> (x < ((y + 1) + 1) <-> z < ((y + 1) + 1)))
102		breq1 2695	. . . . . . . . . . . . . 14 |- (x = z -> (x < (y + 1) <-> z < (y + 1)))
103		eqeq1 1524	. . . . . . . . . . . . . 14 |- (x = z -> (x = (y + 1) <-> z = (y + 1)))
104	102, 103	orbi12d 630	. . . . . . . . . . . . 13 |- (x = z -> ((x < (y + 1) \/ x = (y + 1)) <-> (z < (y + 1) \/ z = (y + 1))))
105	101, 104	imbi12d 629	. . . . . . . . . . . 12 |- (x = z -> ((x < ((y + 1) + 1) -> (x < (y + 1) \/ x = (y + 1))) <-> (z < ((y + 1) + 1) -> (z < (y + 1) \/ z = (y + 1)))))
106	105	imbi2d 615	. . . . . . . . . . 11 |- (x = z -> (((y e. NN /\ A.w e. NN (w < (y + 1) -> (w < y \/ w = y))) -> (x < ((y + 1) + 1) -> (x < (y + 1) \/ x = (y + 1)))) <-> ((y e. NN /\ A.w e. NN (w < (y + 1) -> (w < y \/ w = y))) -> (z < ((y + 1) + 1) -> (z < (y + 1) \/ z = (y + 1))))))
107		nngt0 6091	. . . . . . . . . . . . . . . 16 |- (y e. NN -> 0 < y)
108		ltadd1 5777	. . . . . . . . . . . . . . . . . 18 |- ((0 e. RR /\ y e. RR /\ 1 e. RR) -> (0 < y <-> (0 + 1) < (y + 1)))
109	6, 7, 108	mp3an13 913	. . . . . . . . . . . . . . . . 17 |- (y e. RR -> (0 < y <-> (0 + 1) < (y + 1)))
110	76, 109	syl 10	. . . . . . . . . . . . . . . 16 |- (y e. NN -> (0 < y <-> (0 + 1) < (y + 1)))
111	107, 110	mpbid 193	. . . . . . . . . . . . . . 15 |- (y e. NN -> (0 + 1) < (y + 1))
112		ax1cn 5423	. . . . . . . . . . . . . . . 16 |- 1 e. CC
113	112	addid2i 5485	. . . . . . . . . . . . . . 15 |- (0 + 1) = 1
114	111, 113	syl5eqbrr 2722	. . . . . . . . . . . . . 14 |- (y e. NN -> 1 < (y + 1))
115	114	orcd 270	. . . . . . . . . . . . 13 |- (y e. NN -> (1 < (y + 1) \/ 1 = (y + 1)))
116	115	a1d 12	. . . . . . . . . . . 12 |- (y e. NN -> (1 < ((y + 1) + 1) -> (1 < (y + 1) \/ 1 = (y + 1))))
117	116	adantr 389	. . . . . . . . . . 11 |- ((y e. NN /\ A.w e. NN (w < (y + 1) -> (w < y \/ w = y))) -> (1 < ((y + 1) + 1) -> (1 < (y + 1) \/ 1 = (y + 1))))
118		breq1 2695	. . . . . . . . . . . . . . . . 17 |- (w = v -> (w < (y + 1) <-> v < (y + 1)))
119		breq1 2695	. . . . . . . . . . . . . . . . . 18 |- (w = v -> (w < y <-> v < y))
120		eqeq1 1524	. . . . . . . . . . . . . . . . . 18 |- (w = v -> (w = y <-> v = y))
121	119, 120	orbi12d 630	. . . . . . . . . . . . . . . . 17 |- (w = v -> ((w < y \/ w = y) <-> (v < y \/ v = y)))
122	118, 121	imbi12d 629	. . . . . . . . . . . . . . . 16 |- (w = v -> ((w < (y + 1) -> (w < y \/ w = y)) <-> (v < (y + 1) -> (v < y \/ v = y))))
123	122	rcla4va 1921	. . . . . . . . . . . . . . 15 |- ((v e. NN /\ A.w e. NN (w < (y + 1) -> (w < y \/ w = y))) -> (v < (y + 1) -> (v < y \/ v = y)))
124	123	adantlr 393	. . . . . . . . . . . . . 14 |- (((v e. NN /\ y e. NN) /\ A.w e. NN (w < (y + 1) -> (w < y \/ w = y))) -> (v < (y + 1) -> (v < y \/ v = y)))
125		ltadd1 5777	. . . . . . . . . . . . . . . . 17 |- ((v e. RR /\ (y + 1) e. RR /\ 1 e. RR) -> (v < (y + 1) <-> (v + 1) < ((y + 1) + 1)))
126	7, 125	mp3an3 911	. . . . . . . . . . . . . . . 16 |- ((v e. RR /\ (y + 1) e. RR) -> (v < (y + 1) <-> (v + 1) < ((y + 1) + 1)))
127		nnre 6074	. . . . . . . . . . . . . . . 16 |- (v e. NN -> v e. RR)
128		peano2nn 6080	. . . . . . . . . . . . . . . . 17 |- (y e. NN -> (y + 1) e. NN)
129		nnre 6074	. . . . . . . . . . . . . . . . 17 |- ((y + 1) e. NN -> (y + 1) e. RR)
130	128, 129	syl 10	. . . . . . . . . . . . . . . 16 |- (y e. NN -> (y + 1) e. RR)
131	126, 127, 130	syl2an 456	. . . . . . . . . . . . . . 15 |- ((v e. NN /\ y e. NN) -> (v < (y + 1) <-> (v + 1) < ((y + 1) + 1)))
132	131	adantr 389	. . . . . . . . . . . . . 14 |- (((v e. NN /\ y e. NN) /\ A.w e. NN (w < (y + 1) -> (w < y \/ w = y))) -> (v < (y + 1) <-> (v + 1) < ((y + 1) + 1)))
133		ltadd1 5777	. . . . . . . . . . . . . . . . . 18 |- ((v e. RR /\ y e. RR /\ 1 e. RR) -> (v < y <-> (v + 1) < (y + 1)))
134		recn 5467	. . . . . . . . . . . . . . . . . . . . 21 |- (v e. RR -> v e. CC)
135		recn 5467	. . . . . . . . . . . . . . . . . . . . 21 |- (y e. RR -> y e. CC)
136		recn 5467	. . . . . . . . . . . . . . . . . . . . 21 |- (1 e. RR -> 1 e. CC)
137	134, 135, 136	3anim123i 827	. . . . . . . . . . . . . . . . . . . 20 |- ((v e. RR /\ y e. RR /\ 1 e. RR) -> (v e. CC /\ y e. CC /\ 1 e. CC))
138		3anrot 786	. . . . . . . . . . . . . . . . . . . 20 |- ((1 e. CC /\ v e. CC /\ y e. CC) <-> (v e. CC /\ y e. CC /\ 1 e. CC))
139	137, 138	sylibr 198	. . . . . . . . . . . . . . . . . . 19 |- ((v e. RR /\ y e. RR /\ 1 e. RR) -> (1 e. CC /\ v e. CC /\ y e. CC))
140		3simpc 793	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((1 e. CC /\ v e. CC /\ y e. CC) -> (v e. CC /\ y e. CC))
141		3simp1 794	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((1 e. CC /\ v e. CC /\ y e. CC) -> 1 e. CC)
142	140, 141	jca 286	. . . . . . . . . . . . . . . . . . . . . 22 |- ((1 e. CC /\ v e. CC /\ y e. CC) -> ((v e. CC /\ y e. CC) /\ 1 e. CC))
143		anandir 514	. . . . . . . . . . . . . . . . . . . . . 22 |- (((v e. CC /\ y e. CC) /\ 1 e. CC) <-> ((v e. CC /\ 1 e. CC) /\ (y e. CC /\ 1 e. CC)))
144	142, 143	sylib 196	. . . . . . . . . . . . . . . . . . . . 21 |- ((1 e. CC /\ v e. CC /\ y e. CC) -> ((v e. CC /\ 1 e. CC) /\ (y e. CC /\ 1 e. CC)))
145		addcom 5459	. . . . . . . . . . . . . . . . . . . . . 22 |- ((v e. CC /\ 1 e. CC) -> (v + 1) = (1 + v))
146		addcom 5459	. . . . . . . . . . . . . . . . . . . . . 22 |- ((y e. CC /\ 1 e. CC) -> (y + 1) = (1 + y))
147	145, 146	eqeqan12d 1533	. . . . . . . . . . . . . . . . . . . . 21 |- (((v e. CC /\ 1 e. CC) /\ (y e. CC /\ 1 e. CC)) -> ((v + 1) = (y + 1) <-> (1 + v) = (1 + y)))
148	144, 147	syl 10	. . . . . . . . . . . . . . . . . . . 20 |- ((1 e. CC /\ v e. CC /\ y e. CC) -> ((v + 1) = (y + 1) <-> (1 + v) = (1 + y)))
149		addcan 5506	. . . . . . . . . . . . . . . . . . . 20 |- ((1 e. CC /\ v e. CC /\ y e. CC) -> ((1 + v) = (1 + y) <-> v = y))
150	148, 149	bitr2d 532	. . . . . . . . . . . . . . . . . . 19 |- ((1 e. CC /\ v e. CC /\ y e. CC) -> (v = y <-> (v + 1) = (y + 1)))
151	139, 150	syl 10	. . . . . . . . . . . . . . . . . 18 |- ((v e. RR /\ y e. RR /\ 1 e. RR) -> (v = y <-> (v + 1) = (y + 1)))
152	133, 151	orbi12d 630	. . . . . . . . . . . . . . . . 17 |- ((v e. RR /\ y e. RR /\ 1 e. RR) -> ((v < y \/ v = y) <-> ((v + 1) < (y + 1) \/ (v + 1) = (y + 1))))
153	7, 152	mp3an3 911	. . . . . . . . . . . . . . . 16 |- ((v e. RR /\ y e. RR) -> ((v < y \/ v = y) <-> ((v + 1) < (y + 1) \/ (v + 1) = (y + 1))))
154	153, 127, 76	syl2an 456	. . . . . . . . . . . . . . 15 |- ((v e. NN /\ y e. NN) -> ((v < y \/ v = y) <-> ((v + 1) < (y + 1) \/ (v + 1) = (y + 1))))
155	154	adantr 389	. . . . . . . . . . . . . 14 |- (((v e. NN /\ y e. NN) /\ A.w e. NN (w < (y + 1) -> (w < y \/ w = y))) -> ((v < y \/ v = y) <-> ((v + 1) < (y + 1) \/ (v + 1) = (y + 1))))
156	124, 132, 155	3imtr3d 545	. . . . . . . . . . . . 13 |- (((v e. NN /\ y e. NN) /\ A.w e. NN (w < (y + 1) -> (w < y \/ w = y))) -> ((v + 1) < ((y + 1) + 1) -> ((v + 1) < (y + 1) \/ (v + 1) = (y + 1))))
157	156	exp31 376	. . . . . . . . . . . 12 |- (v e. NN -> (y e. NN -> (A.w e. NN (w < (y + 1) -> (w < y \/ w = y)) -> ((v + 1) < ((y + 1) + 1) -> ((v + 1) < (y + 1) \/ (v + 1) = (y + 1))))))
158	157	imp3a 359	. . . . . . . . . . 11 |- (v e. NN -> ((y e. NN /\ A.w e. NN (w < (y + 1) -> (w < y \/ w = y))) -> ((v + 1) < ((y + 1) + 1) -> ((v + 1) < (y + 1) \/ (v + 1) = (y + 1)))))
159	94, 100, 106, 117, 158	nn1suc 6084	. . . . . . . . . 10 |- (z e. NN -> ((y e. NN /\ A.w e. NN (w < (y + 1) -> (w < y \/ w = y))) -> (z < ((y + 1) + 1) -> (z < (y + 1) \/ z = (y + 1)))))
160	159	exp3a 374	. . . . . . . . 9 |- (z e. NN -> (y e. NN -> (A.w e. NN (w < (y + 1) -> (w < y \/ w = y)) -> (z < ((y + 1) + 1) -> (z < (y + 1) \/ z = (y + 1))))))
161	160	com3l 34	. . . . . . . 8 |- (y e. NN -> (A.w e. NN (w < (y + 1) -> (w < y \/ w = y)) -> (z e. NN -> (z < ((y + 1) + 1) -> (z < (y + 1) \/ z = (y + 1))))))
162	161	r19.21adv 1764	. . . . . . 7 |- (y e. NN -> (A.w e. NN (w < (y + 1) -> (w < y \/ w = y)) -> A.z e. NN (z < ((y + 1) + 1) -> (z < (y + 1) \/ z = (y + 1)))))
163		breq1 2695	. . . . . . . . 9 |- (z = w -> (z < (y + 1) <-> w < (y + 1)))
164		breq1 2695	. . . . . . . . . 10 |- (z = w -> (z < y <-> w < y))
165		eqeq1 1524	. . . . . . . . . 10 |- (z = w -> (z = y <-> w = y))
166	164, 165	orbi12d 630	. . . . . . . . 9 |- (z = w -> ((z < y \/ z = y) <-> (w < y \/ w = y)))
167	163, 166	imbi12d 629	. . . . . . . 8 |- (z = w -> ((z < (y + 1) -> (z < y \/ z = y)) <-> (w < (y + 1) -> (w < y \/ w = y))))
168	167	cbvralv 1846	. . . . . . 7 |- (A.z e. NN (z < (y + 1) -> (z < y \/ z = y)) <-> A.w e. NN (w < (y + 1) -> (w < y \/ w = y)))
169	162, 168	syl5ib 204	. . . . . 6 |- (y e. NN -> (A.z e. NN (z < (y + 1) -> (z < y \/ z = y)) -> A.z e. NN (z < ((y + 1) + 1) -> (z < (y + 1) \/ z = (y + 1)))))
170	36, 43, 50, 57, 88, 169	nnind 6082	. . . . 5 |- (B e. NN -> A.z e. NN (z < (B + 1) -> (z < B \/ z = B)))
171	29, 170	syl5 21	. . . 4 |- (A e. NN -> (B e. NN -> (A < (B + 1) -> (A < B \/ A = B))))
172	171	imp 348	. . 3 |- ((A e. NN /\ B e. NN) -> (A < (B + 1) -> (A < B \/ A = B)))
173	23, 172	impbid 519	. 2 |- ((A e. NN /\ B e. NN) -> ((A < B \/ A = B) <-> A < (B + 1)))
174	4, 173	bitrd 531	1 |- ((A e. NN /\ B e. NN) -> (A <_ B <-> A < (B + 1)))

Syntax hints:  -. wn 2   -> wi 3   <-> wb 144   \/ wo 220   /\ wa 221   /\ w3a 781   = wceq 992   e. wcel 994  A.wral 1691   class class class wbr 2692  (class class class)co 4021  CCcc 5386  RRcr 5387  0cc0 5388  1c1 5389   + caddc 5391   <_ cle 5449  NNcn 5450   < clt 5640

This theorem is referenced by:  nnltp1le 6101  nnsubi 6102  monoord 6482  seq1bndi 7113  bcpasc2i 7170  bccl2 7174  efcltlem1 7509  ef1tllem 7586  infpnlem2 7719  bcthlem18 8227

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 998  ax-gen 999  ax-8 1000  ax-9 1001  ax-10 1002  ax-11 1003  ax-12 1004  ax-13 1005  ax-14 1006  ax-17 1007  ax-4 1009  ax-5o 1011  ax-6o 1014  ax-9o 1159  ax-10o 1177  ax-16 1247  ax-11o 1255  ax-ext 1500  ax-rep 2767  ax-sep 2777  ax-nul 2784  ax-pow 2818  ax-pr 2855  ax-un 3089  ax-inf2 4770

This theorem depends on definitions:  df-bi 145  df-or 222  df-an 223  df-3or 782  df-3an 783  df-ex 1017  df-sb 1209  df-eu 1421  df-mo 1422  df-clab 1506  df-cleq 1511  df-clel 1514  df-ne 1630  df-nel 1631  df-ral 1695  df-rex 1696  df-reu 1697  df-rab 1698  df-v 1858  df-sbc 1987  df-csb 2052  df-dif 2101  df-un 2102  df-in 2103  df-ss 2105  df-pss 2107  df-nul 2333  df-if 2416  df-pw 2459  df-sn 2470  df-pr 2471  df-tp 2473  df-op 2474  df-uni 2570  df-int 2601  df-iun 2635  df-br 2693  df-opab 2741  df-tr 2755  df-eprel 2910  df-id 2913  df-po 2918  df-so 2929  df-fr 2947  df-we 2962  df-ord 2978  df-on 2979  df-lim 2980  df-suc 2981  df-om 3219  df-xp 3265  df-rel 3266  df-cnv 3267  df-co 3268  df-dm 3269  df-rn 3270  df-res 3271  df-ima 3272  df-fun 3273  df-fn 3274  df-f 3275  df-f1 3276  df-fo 3277  df-f1o 3278  df-fv 3279  df-opr 4023  df-oprab 4024  df-1st 4140  df-2nd 4141  df-rdg 4233  df-1o 4269  df-oadd 4271  df-omul 4272  df-er 4401  df-ec 4403  df-qs 4406  df-en 4509  df-dom 4510  df-sdom 4511  df-ni 5154  df-pli 5155  df-mi 5156  df-lti 5157  df-plpq 5189  df-mpq 5190  df-enq 5191  df-nq 5192  df-plq 5193  df-mq 5194  df-rq 5195  df-ltq 5196  df-1q 5197  df-np 5240  df-1p 5241  df-plp 5242  df-mp 5243  df-ltp 5244  df-plpr 5318  df-mpr 5319  df-enr 5320  df-nr 5321  df-plr 5322  df-mr 5323  df-ltr 5324  df-0r 5325  df-1r 5326  df-m1r 5327  df-c 5394  df-0 5395  df-1 5396  df-i 5397  df-r 5398  df-plus 5399  df-mul 5400  df-lt 5401  df-sub 5510  df-neg 5512  df-pnf 5641  df-mnf 5642  df-xr 5643  df-ltxr 5644  df-le 5645  df-n 6070

Copyright terms: Public domain