Theorem nnleltp1t 5954

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 5518	. . 3 |- ((A e. RR /\ B e. RR) -> (A <_ B <-> (A < B \/ A = B)))
2		nnret 5929	. . 3 |- (A e. NN -> A e. RR)
3		nnret 5929	. . 3 |- (B e. NN -> B e. RR)
4	1, 2, 3	syl2an 454	. 2 |- ((A e. NN /\ B e. NN) -> (A <_ B <-> (A < B \/ A = B)))
5		lt01 5680	. . . . . . 7 |- 0 < 1
6		0re 5440	. . . . . . . . 9 |- 0 e. RR
7		1re 5435	. . . . . . . . 9 |- 1 e. RR
8	6, 7	pm3.2i 285	. . . . . . . 8 |- (0 e. RR /\ 1 e. RR)
9		lt2addt 5643	. . . . . . . . 9 |- (((A e. RR /\ 0 e. RR) /\ (B e. RR /\ 1 e. RR)) -> ((A < B /\ 0 < 1) -> (A + 0) < (B + 1)))
10	9	an4s 508	. . . . . . . 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 696	. . . . . . 7 |- ((A e. RR /\ B e. RR) -> ((A < B /\ 0 < 1) -> (A + 0) < (B + 1)))
12	5, 11	mpan2i 699	. . . . . 6 |- ((A e. RR /\ B e. RR) -> (A < B -> (A + 0) < (B + 1)))
13		pm3.26 319	. . . . . . . 8 |- ((A e. RR /\ B e. RR) -> A e. RR)
14		recnt 5313	. . . . . . . 8 |- (A e. RR -> A e. CC)
15		ax0id 5281	. . . . . . . 8 |- (A e. CC -> (A + 0) = A)
16	13, 14, 15	3syl 20	. . . . . . 7 |- ((A e. RR /\ B e. RR) -> (A + 0) = A)
17	16	breq1d 2629	. . . . . 6 |- ((A e. RR /\ B e. RR) -> ((A + 0) < (B + 1) <-> A < (B + 1)))
18	12, 17	sylibd 202	. . . . 5 |- ((A e. RR /\ B e. RR) -> (A < B -> A < (B + 1)))
19		breq1 2622	. . . . . . 7 |- (A = B -> (A < (B + 1) <-> B < (B + 1)))
20		ltp1t 5811	. . . . . . 7 |- (B e. RR -> B < (B + 1))
21	19, 20	syl5cbir 211	. . . . . 6 |- (B e. RR -> (A = B -> A < (B + 1)))
22	21	adantl 388	. . . . 5 |- ((A e. RR /\ B e. RR) -> (A = B -> A < (B + 1)))
23	18, 22	jaod 424	. . . 4 |- ((A e. RR /\ B e. RR) -> ((A < B \/ A = B) -> A < (B + 1)))
24	23, 2, 3	syl2an 454	. . 3 |- ((A e. NN /\ B e. NN) -> ((A < B \/ A = B) -> A < (B + 1)))
25		breq1 2622	. . . . . . 7 |- (z = A -> (z < (B + 1) <-> A < (B + 1)))
26		breq1 2622	. . . . . . . 8 |- (z = A -> (z < B <-> A < B))
27		eqeq1 1481	. . . . . . . 8 |- (z = A -> (z = B <-> A = B))
28	26, 27	orbi12d 627	. . . . . . 7 |- (z = A -> ((z < B \/ z = B) <-> (A < B \/ A = B)))
29	25, 28	imbi12d 626	. . . . . 6 |- (z = A -> ((z < (B + 1) -> (z < B \/ z = B)) <-> (A < (B + 1) -> (A < B \/ A = B))))
30	29	rcla4v 1873	. . . . 5 |- (A e. NN -> (A.z e. NN (z < (B + 1) -> (z < B \/ z = B)) -> (A < (B + 1) -> (A < B \/ A = B))))
31		opreq1 3968	. . . . . . . . 9 |- (x = 1 -> (x + 1) = (1 + 1))
32	31	breq2d 2630	. . . . . . . 8 |- (x = 1 -> (z < (x + 1) <-> z < (1 + 1)))
33		breq2 2623	. . . . . . . . 9 |- (x = 1 -> (z < x <-> z < 1))
34		eqeq2 1484	. . . . . . . . 9 |- (x = 1 -> (z = x <-> z = 1))
35	33, 34	orbi12d 627	. . . . . . . 8 |- (x = 1 -> ((z < x \/ z = x) <-> (z < 1 \/ z = 1)))
36	32, 35	imbi12d 626	. . . . . . 7 |- (x = 1 -> ((z < (x + 1) -> (z < x \/ z = x)) <-> (z < (1 + 1) -> (z < 1 \/ z = 1))))
37	36	ralbidv 1663	. . . . . 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))))
38		opreq1 3968	. . . . . . . . 9 |- (x = y -> (x + 1) = (y + 1))
39	38	breq2d 2630	. . . . . . . 8 |- (x = y -> (z < (x + 1) <-> z < (y + 1)))
40		breq2 2623	. . . . . . . . 9 |- (x = y -> (z < x <-> z < y))
41		eqeq2 1484	. . . . . . . . 9 |- (x = y -> (z = x <-> z = y))
42	40, 41	orbi12d 627	. . . . . . . 8 |- (x = y -> ((z < x \/ z = x) <-> (z < y \/ z = y)))
43	39, 42	imbi12d 626	. . . . . . 7 |- (x = y -> ((z < (x + 1) -> (z < x \/ z = x)) <-> (z < (y + 1) -> (z < y \/ z = y))))
44	43	ralbidv 1663	. . . . . 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))))
45		opreq1 3968	. . . . . . . . 9 |- (x = (y + 1) -> (x + 1) = ((y + 1) + 1))
46	45	breq2d 2630	. . . . . . . 8 |- (x = (y + 1) -> (z < (x + 1) <-> z < ((y + 1) + 1)))
47		breq2 2623	. . . . . . . . 9 |- (x = (y + 1) -> (z < x <-> z < (y + 1)))
48		eqeq2 1484	. . . . . . . . 9 |- (x = (y + 1) -> (z = x <-> z = (y + 1)))
49	47, 48	orbi12d 627	. . . . . . . 8 |- (x = (y + 1) -> ((z < x \/ z = x) <-> (z < (y + 1) \/ z = (y + 1))))
50	46, 49	imbi12d 626	. . . . . . 7 |- (x = (y + 1) -> ((z < (x + 1) -> (z < x \/ z = x)) <-> (z < ((y + 1) + 1) -> (z < (y + 1) \/ z = (y + 1)))))
51	50	ralbidv 1663	. . . . . 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)))))
52		opreq1 3968	. . . . . . . . 9 |- (x = B -> (x + 1) = (B + 1))
53	52	breq2d 2630	. . . . . . . 8 |- (x = B -> (z < (x + 1) <-> z < (B + 1)))
54		breq2 2623	. . . . . . . . 9 |- (x = B -> (z < x <-> z < B))
55		eqeq2 1484	. . . . . . . . 9 |- (x = B -> (z = x <-> z = B))
56	54, 55	orbi12d 627	. . . . . . . 8 |- (x = B -> ((z < x \/ z = x) <-> (z < B \/ z = B)))
57	53, 56	imbi12d 626	. . . . . . 7 |- (x = B -> ((z < (x + 1) -> (z < x \/ z = x)) <-> (z < (B + 1) -> (z < B \/ z = B))))
58	57	ralbidv 1663	. . . . . 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))))
59		breq1 2622	. . . . . . . . 9 |- (x = 1 -> (x < (1 + 1) <-> 1 < (1 + 1)))
60		breq1 2622	. . . . . . . . . 10 |- (x = 1 -> (x < 1 <-> 1 < 1))
61		eqeq1 1481	. . . . . . . . . 10 |- (x = 1 -> (x = 1 <-> 1 = 1))
62	60, 61	orbi12d 627	. . . . . . . . 9 |- (x = 1 -> ((x < 1 \/ x = 1) <-> (1 < 1 \/ 1 = 1)))
63	59, 62	imbi12d 626	. . . . . . . 8 |- (x = 1 -> ((x < (1 + 1) -> (x < 1 \/ x = 1)) <-> (1 < (1 + 1) -> (1 < 1 \/ 1 = 1))))
64		breq1 2622	. . . . . . . . 9 |- (x = (y + 1) -> (x < (1 + 1) <-> (y + 1) < (1 + 1)))
65		breq1 2622	. . . . . . . . . 10 |- (x = (y + 1) -> (x < 1 <-> (y + 1) < 1))
66		eqeq1 1481	. . . . . . . . . 10 |- (x = (y + 1) -> (x = 1 <-> (y + 1) = 1))
67	65, 66	orbi12d 627	. . . . . . . . 9 |- (x = (y + 1) -> ((x < 1 \/ x = 1) <-> ((y + 1) < 1 \/ (y + 1) = 1)))
68	64, 67	imbi12d 626	. . . . . . . 8 |- (x = (y + 1) -> ((x < (1 + 1) -> (x < 1 \/ x = 1)) <-> ((y + 1) < (1 + 1) -> ((y + 1) < 1 \/ (y + 1) = 1))))
69		breq1 2622	. . . . . . . . 9 |- (x = z -> (x < (1 + 1) <-> z < (1 + 1)))
70