Theorem nnleltp1t 4448

Description: Natural number ordering relation.

Assertion

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

Proof of Theorem nnleltp1t

Step	Hyp	Ref	Expression
1		leloet 4284	. . 3 |- ((A e. RR /\ B e. RR) -> (A <_ B <-> (A < B \/ A = B)))
2		nnret 4427	. . 3 |- (A e. NN -> A e. RR)
3		nnret 4427	. . 3 |- (B e. NN -> B e. RR)
4	1, 2, 3	syl2an 349	. 2 |- ((A e. NN /\ B e. NN) -> (A <_ B <-> (A < B \/ A = B)))
5		lt01 4377	. . . . . . 7 |- 0 < 1
6		ax0re 4063	. . . . . . . . 9 |- 0 e. RR
7		ax1re 4064	. . . . . . . . 9 |- 1 e. RR
8	6, 7	pm3.2i 234	. . . . . . . 8 |- (0 e. RR /\ 1 e. RR)
9		lt2addt 4361	. . . . . . . . 9 |- (((A e. RR /\ 0 e. RR) /\ (B e. RR /\ 1 e. RR)) -> ((A < B /\ 0 < 1) -> (A + 0) < (B + 1)))
10	9	an4s 390	. . . . . . . 8 |- (((A e. RR /\ B e. RR) /\ (0 e. RR /\ 1 e. RR)) -> ((A < B /\ 0 < 1) -> (A + 0) < (B + 1)))
11	8, 10	mpan2 519	. . . . . . 7 |- ((A e. RR /\ B e. RR) -> ((A < B /\ 0 < 1) -> (A + 0) < (B + 1)))
12	5, 11	mpan2i 522	. . . . . 6 |- ((A e. RR /\ B e. RR) -> (A < B -> (A + 0) < (B + 1)))
13		pm3.26 256	. . . . . . . 8 |- ((A e. RR /\ B e. RR) -> A e. RR)
14		recnt 4097	. . . . . . . 8 |- (A e. RR -> A e. CC)
15		ax0id 4076	. . . . . . . 8 |- (A e. CC -> (A + 0) = A)
16	13, 14, 15	3syl 21	. . . . . . 7 |- ((A e. RR /\ B e. RR) -> (A + 0) = A)
17	16	breq1d 2071	. . . . . 6 |- ((A e. RR /\ B e. RR) -> ((A + 0) < (B + 1) <-> A < (B + 1)))
18	12, 17	sylibd 177	. . . . 5 |- ((A e. RR /\ B e. RR) -> (A < B -> A < (B + 1)))
19		breq1 2065	. . . . . . . 8 |- (A = B -> (A < (B + 1) <-> B < (B + 1)))
20		ltplus1t 4383	. . . . . . . 8 |- (B e. RR -> B < (B + 1))
21	19, 20	syl5bir 184	. . . . . . 7 |- (A = B -> (B e. RR -> A < (B + 1)))
22	21	com12 13	. . . . . 6 |- (B e. RR -> (A = B -> A < (B + 1)))
23	22	adantl 305	. . . . 5 |- ((A e. RR /\ B e. RR) -> (A = B -> A < (B + 1)))
24	18, 23	jaod 329	. . . 4 |- ((A e. RR /\ B e. RR) -> ((A < B \/ A = B) -> A < (B + 1)))
25	24, 2, 3	syl2an 349	. . 3 |- ((A e. NN /\ B e. NN) -> ((A < B \/ A = B) -> A < (B + 1)))
26		opreq1 3006	. . . . . . . . . 10 |- (x = 1 -> (x + 1) = (1 + 1))
27	26	breq2d 2072	. . . . . . . . 9 |- (x = 1 -> (z < (x + 1) <-> z < (1 + 1)))
28		breq2 2066	. . . . . . . . . 10 |- (x = 1 -> (z < x <-> z < 1))
29		cleq2 1110	. . . . . . . . . 10 |- (x = 1 -> (z = x <-> z = 1))
30	28, 29	orbi12d 475	. . . . . . . . 9 |- (x = 1 -> ((z < x \/ z = x) <-> (z < 1 \/ z = 1)))
31	27, 30	imbi12d 474	. . . . . . . 8 |- (x = 1 -> ((z < (x + 1) -> (z < x \/ z = x)) <-> (z < (1 + 1) -> (z < 1 \/ z = 1))))
32	31	biraldv 1219	. . . . . . 7 |- (x = 1 -> (A.z e. NN (z < (x + 1) -> (z < x \/ z = x)) <-> A.z e. NN (z < (1 + 1) -> (z < 1 \/ z = 1))))
33		opreq1 3006	. . . . . . . . . 10 |- (x = y -> (x + 1) = (y + 1))
34	33	breq2d 2072	. . . . . . . . 9 |- (x = y -> (z < (x + 1) <-> z < (y + 1)))
35		breq2 2066	. . . . . . . . . 10 |- (x = y -> (z < x <-> z < y))
36		cleq2 1110	. . . . . . . . . 10 |- (x = y -> (z = x <-> z = y))
37	35, 36	orbi12d 475	. . . . . . . . 9 |- (x = y -> ((z < x \/ z = x) <-> (z < y \/ z = y)))
38	34, 37	imbi12d 474	. . . . . . . 8 |- (x = y -> ((z < (x + 1) -> (z < x \/ z = x)) <-> (z < (y + 1) -> (z < y \/ z = y))))
39	38	biraldv 1219	. . . . . . 7 |- (x = y -> (A.z e. NN (z < (x + 1) -> (z < x \/ z = x)) <-> A.z e. NN (z < (y + 1) -> (z < y \/ z = y))))
40		opreq1 3006	. . . . . . . . . 10 |- (x = (y + 1) -> (x + 1) = ((y + 1) + 1))
41	40	breq2d 2072	. . . . . . . . 9 |- (x = (y + 1) -> (z < (x + 1) <-> z < ((y + 1) + 1)))
42		breq2 2066	. . . . . . . . . 10 |- (x = (y + 1) -> (z < x <-> z < (y + 1)))
43		cleq2 1110	. . . . . . . . . 10 |- (x = (y + 1) -> (z = x <-> z = (y + 1)))
44	42, 43	orbi12d 475	. . . . . . . . 9 |- (x = (y + 1) -> ((z < x \/ z = x) <-> (z < (y + 1) \/ z = (y + 1))))
45	41, 44	imbi12d 474	. . . . . . . 8 |- (x = (y + 1) -> ((z < (x + 1) -> (z < x \/ z = x)) <-> (z < ((y + 1) + 1) -> (z < (y + 1) \/ z = (y + 1)))))
46	45	biraldv 1219	. . . . . . 7 |- (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)))))
47		opreq1 3006	. . . . . . . . . 10 |- (x = B -> (x + 1) = (B + 1))
48	47	breq2d 2072	. . . . . . . . 9 |- (x = B -> (z < (x + 1) <-> z < (B + 1)))
49		breq2 2066	. . . . . . . . . 10 |- (x = B -> (z < x <-> z < B))
50		cleq2 1110	. . . . . . . . . 10 |- (x = B -> (z = x <-> z = B))
51	49, 50	orbi12d 475	. . . . . . . . 9 |- (x = B -> ((z < x \/ z = x) <-> (z < B \/ z = B)))
52	48, 51	imbi12d 474	. . . . . . . 8 |- (x = B -> ((z < (x + 1) -> (z < x \/ z = x)) <-> (z < (B + 1) -> (z < B \/ z = B))))
53	52	biraldv 1219	. . . . . . 7 |- (x = B -> (A.z e. NN (z < (x + 1) -> (z < x \/ z = x)) <-> A.z e. NN (z < (B + 1) -> (z < B \/ z = B))))
54		breq1 2065	. . . . . . . . . 10 |- (x = 1 -> (x < (1 + 1) <-> 1 < (1 + 1)))
55		breq1 2065	. . . . . . . . . . 11 |- (x = 1 -> (x < 1 <-> 1 < 1))
56		cleq1 1107	. . . . . . . . . . 11 |- (x = 1 -> (x = 1 <-> 1 = 1))
57	55, 56	orbi12d 475	. . . . . . . . . 10 |- (x = 1 -> ((x < 1 \/ x = 1) <-> (1 < 1 \/ 1 = 1)))
58	54, 57	imbi12d 474	. . . . . . . . 9 |- (x = 1 -> ((x < (1 + 1) -> (x < 1 \/ x = 1)) <-> (1 < (1 + 1) -> (1 < 1 \/ 1 = 1))))
59		breq1 2065	. . . . . . . . . 10 |- (x = y -> (x < (1 + 1) <-> y < (1 + 1)))
60		breq1 2065	. . . . . . . . . . 11 |- (x = y -> (x < 1 <-> y < 1))
61		cleq1 1107	. . . . . . . . . . 11 |- (x = y -> (x = 1 <-> y = 1))
62	60, 61	orbi12d 475	. . . . . . . . . 10 |- (x = y -> ((x < 1 \/ x = 1) <-> (y < 1 \/ y = 1)))
63	59, 62	imbi12d 474	. . . . . . . . 9 |- (x = y -> ((x < (1 + 1) -> (x < 1 \/ x = 1)) <-> (y < (1 + 1) -> (y < 1 \/ y = 1))))
64		breq1 2065	. . . . . . . . . 10 |- (x = (y + 1) -> (x < (1 + 1) <-> (y + 1) < (1 + 1)))
65		breq1 2065	. . . . . . . . . . 11 |- (x = (y + 1) -> (x < 1 <-> (y + 1) < 1))
66		cleq1 1107	. . . . . . . . . . 11 |- (x = (y + 1) -> (x = 1 <-> (y + 1) = 1))
67	65, 66	orbi12d 475	. . . . . . . . . 10 |- (x = (y + 1) -> ((x < 1 \/ x = 1) <-> ((y + 1) < 1 \/ (y + 1) = 1)))
68	64, 67	imbi12d 474	. . . . . . . . 9 |- (x = (y + 1) -> ((x < (1 + 1) -> (x < 1 \/ x = 1)) <-> ((y + 1) < (1 + 1) -> ((y + 1) < 1 \/ (y + 1) = 1))))
69		breq1 2065	. . . . . . . . . 10 |- (x = z -> (x < (1 + 1) <-> z < (1 + 1)))
70		breq1 2065	. . . . . . . . . . 11 |- (x = z -> (x < 1 <-> z < 1))
71		cleq1 1107	. . . . . . . . . . 11 |- (x = z -> (x = 1 <-> z = 1))
72	70, 71	orbi12d 475	. . . . . . . . . 10 |- (x = z -> ((x < 1 \/ x = 1) <-> (z < 1 \/ z = 1)))
73	69, 72	imbi12d 474	. . . . . . . . 9 |- (x = z -> ((x < (1 + 1) -> (x < 1 \/ x = 1)) <-> (z < (1