HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem nnleltp1t 5901
Description: Natural number ordering relation.
Assertion
Ref Expression
nnleltp1t |- ((A e. NN /\ B e. NN) -> (A <_ B <-> A < (B + 1)))
Proof of Theorem nnleltp1t
StepHypRef Expression
1 leloet 5491 . . 3 |- ((A e. RR /\ B e. RR) -> (A <_ B <-> (A < B \/ A = B)))
2 nnret 5877 . . 3 |- (A e. NN -> A e. RR)
3 nnret 5877 . . 3 |- (B e. NN -> B e. RR)
41, 2, 3syl2an 454 . 2 |- ((A e. NN /\ B e. NN) -> (A <_ B <-> (A < B \/ A = B)))
5 lt01 5653 . . . . . . 7 |- 0 < 1
6 0re 5412 . . . . . . . . 9 |- 0 e. RR
7 1re 5407 . . . . . . . . 9 |- 1 e. RR
86, 7pm3.2i 285 . . . . . . . 8 |- (0 e. RR /\ 1 e. RR)
9 lt2addt 5617 . . . . . . . . 9 |- (((A e. RR /\ 0 e. RR) /\ (B e. RR /\ 1 e. RR)) -> ((A < B /\ 0 < 1) -> (A + 0) < (B + 1)))
109an4s 507 . . . . . . . 8 |- (((A e. RR /\ B e. RR) /\ (0 e. RR /\ 1 e. RR)) -> ((A < B /\ 0 < 1) -> (A + 0) < (B + 1)))
118, 10mpan2 694 . . . . . . 7 |- ((A e. RR /\ B e. RR) -> ((A < B /\ 0 < 1) -> (A + 0) < (B + 1)))
125, 11mpan2i 697 . . . . . 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 5285 . . . . . . . 8 |- (A e. RR -> A e. CC)
15 ax0id 5253 . . . . . . . 8 |- (A e. CC -> (A + 0) = A)
1613, 14, 153syl 20 . . . . . . 7 |- ((A e. RR /\ B e. RR) -> (A + 0) = A)
1716breq1d 2619 . . . . . 6 |- ((A e. RR /\ B e. RR) -> ((A + 0) < (B + 1) <-> A < (B + 1)))
1812, 17sylibd 202 . . . . 5 |- ((A e. RR /\ B e. RR) -> (A < B -> A < (B + 1)))
19 breq1 2612 . . . . . . 7 |- (A = B -> (A < (B + 1) <-> B < (B + 1)))
20 ltp1t 5767 . . . . . . 7 |- (B e. RR -> B < (B + 1))
2119, 20syl5cbir 211 . . . . . 6 |- (B e. RR -> (A = B -> A < (B + 1)))
2221adantl 388 . . . . 5 |- ((A e. RR /\ B e. RR) -> (A = B -> A < (B + 1)))
2318, 22jaod 424 . . . 4 |- ((A e. RR /\ B e. RR) -> ((A < B \/ A = B) -> A < (B + 1)))
2423, 2, 3syl2an 454 . . 3 |- ((A e. NN /\ B e. NN) -> ((A < B \/ A = B) -> A < (B + 1)))
25 breq1 2612 . . . . . . 7 |- (z = A -> (z < (B + 1) <-> A < (B + 1)))
26 breq1 2612 . . . . . . . 8 |- (z = A -> (z < B <-> A < B))
27 eqeq1 1473 . . . . . . . 8 |- (z = A -> (z = B <-> A = B))
2826, 27orbi12d 625 . . . . . . 7 |- (z = A -> ((z < B \/ z = B) <-> (A < B \/ A = B)))
2925, 28imbi12d 624 . . . . . 6 |- (z = A -> ((z < (B + 1) -> (z < B \/ z = B)) <-> (A < (B + 1) -> (A < B \/ A = B))))
3029rcla4v 1864 . . . . 5 |- (A e. NN -> (A.z e. NN (z < (B + 1) -> (z < B \/ z = B)) -> (A < (B + 1) -> (A < B \/ A = B))))
31 opreq1 3953 . . . . . . . . 9 |- (x = 1 -> (x + 1) = (1 + 1))
3231breq2d 2620 . . . . . . . 8 |- (x = 1 -> (z < (x + 1) <-> z < (1 + 1)))
33 breq2 2613 . . . . . . . . 9 |- (x = 1 -> (z < x <-> z < 1))
34 eqeq2 1476 . . . . . . . . 9 |- (x = 1 -> (z = x <-> z = 1))
3533, 34orbi12d 625 . . . . . . . 8 |- (x = 1 -> ((z < x \/ z = x) <-> (z < 1 \/ z = 1)))
3632, 35imbi12d 624 . . . . . . 7 |- (x = 1 -> ((z < (x + 1) -> (z < x \/ z = x)) <-> (z < (1 + 1) -> (z < 1 \/ z = 1))))
3736ralbidv 1655 . . . . . 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 3953 . . . . . . . . 9 |- (x = y -> (x + 1) = (y + 1))
3938breq2d 2620 . . . . . . . 8 |- (x = y -> (z < (x + 1) <-> z < (y + 1)))
40 breq2 2613 . . . . . . . . 9 |- (x = y -> (z < x <-> z < y))
41 eqeq2 1476 . . . . . . . . 9 |- (x = y -> (z = x <-> z = y))
4240, 41orbi12d 625 . . . . . . . 8 |- (x = y -> ((z < x \/ z = x) <-> (z < y \/ z = y)))
4339, 42imbi12d 624 . . . . . . 7 |- (x = y -> ((z < (x + 1) -> (z < x \/ z = x)) <-> (z < (y + 1) -> (z < y \/ z = y))))
4443ralbidv 1655 . . . . . 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 3953 . . . . . . . . 9 |- (x = (y + 1) -> (x + 1) = ((y + 1) + 1))
4645breq2d 2620 . . . . . . . 8 |- (x = (y + 1) -> (z < (x + 1) <-> z < ((y + 1) + 1)))
47 breq2 2613 . . . . . . . . 9 |- (x = (y + 1) -> (z < x <-> z < (y + 1)))
48 eqeq2 1476 . . . . . . . . 9 |- (x = (y + 1) -> (z = x <-> z = (y + 1)))
4947, 48orbi12d 625 . . . . . . . 8 |- (x = (y + 1) -> ((z < x \/ z = x) <-> (z < (y + 1) \/ z = (y + 1))))
5046, 49imbi12d 624 . . . . . . 7 |- (x = (y + 1) -> ((z < (x + 1) -> (z < x \/ z = x)) <-> (z < ((y + 1) + 1) -> (z < (y + 1) \/ z = (y + 1)))))
5150ralbidv 1655 . . . . . 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 3953 . . . . . . . . 9 |- (x = B -> (x + 1) = (B + 1))
5352breq2d 2620 . . . . . . . 8 |- (x = B -> (z < (x + 1) <-> z < (B + 1)))
54 breq2 2613 . . . . . . . . 9 |- (x = B -> (z < x <-> z < B))
55 eqeq2 1476 . . . . . . . . 9 |- (x = B -> (z = x <-> z = B))
5654, 55orbi12d 625 . . . . . . . 8 |- (x = B -> ((z < x \/ z = x) <-> (z < B \/ z = B)))
5753, 56imbi12d 624 . . . . . . 7 |- (x = B -> ((z < (x + 1) -> (z < x \/ z = x)) <-> (z < (B + 1) -> (z < B \/ z = B))))
5857ralbidv 1655 . . . . . 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 2612 . . . . . . . . 9 |- (x = 1 -> (x < (1 + 1) <-> 1 < (1 + 1)))
60 breq1 2612 . . . . . . . . . 10 |- (x = 1 -> (x < 1 <-> 1 < 1))
61 eqeq1 1473 . . . . . . . . . 10 |- (x = 1 -> (x = 1 <-> 1 = 1))
6260, 61orbi12d 625 . . . . . . . . 9 |- (x = 1 -> ((x < 1 \/ x = 1) <-> (1 < 1 \/ 1 = 1)))
6359, 62imbi12d 624 . . . . . . . 8 |- (x = 1 -> ((x < (1 + 1) -> (x < 1 \/ x = 1)) <-> (1 < (1 + 1) -> (1 < 1 \/ 1 = 1))))
64 breq1 2612 . . . . . . . . 9 |- (x = (y + 1) -> (x < (1 + 1) <-> (y + 1) < (1 + 1)))
65 breq1 2612 . . . . . . . . . 10 |- (x = (y + 1) -> (x < 1 <-> (y + 1) < 1))
66 eqeq1 1473 . . . . . . . . . 10 |- (x = (y + 1) -> (x = 1 <-> (y + 1) = 1))
6765, 66orbi12d 625 . . . . . . . . 9 |- (x = (y + 1) -> ((x < 1 \/ x = 1) <-> ((y + 1) < 1 \/ (y + 1) = 1)))
6864, 67imbi12d 624 . . . . . . . 8 |- (x = (y + 1) -> ((x < (1 + 1) -> (x < 1 \/ x = 1)) <-> ((y + 1) < (1 + 1) -> ((y + 1) < 1 \/ (y + 1) = 1))))
69 breq1 2612 . . . . . . . . 9 |- (x = z -> (x < (1 + 1) <-> z < (1 + 1)))
70