New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  nnltp1c GIF version

Theorem nnltp1c 6262
 Description: Any natural is less than one plus itself. (Contributed by SF, 25-Mar-2015.)
Assertion
Ref Expression
nnltp1c (N NnN <c (N +c 1c))

Proof of Theorem nnltp1c
Dummy variables x n are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nnltp1clem1 6261 . 2 {x x <c (x +c 1c)} V
2 id 19 . . 3 (x = 0cx = 0c)
3 addceq1 4383 . . 3 (x = 0c → (x +c 1c) = (0c +c 1c))
42, 3breq12d 4652 . 2 (x = 0c → (x <c (x +c 1c) ↔ 0c <c (0c +c 1c)))
5 id 19 . . 3 (x = nx = n)
6 addceq1 4383 . . 3 (x = n → (x +c 1c) = (n +c 1c))
75, 6breq12d 4652 . 2 (x = n → (x <c (x +c 1c) ↔ n <c (n +c 1c)))
8 id 19 . . 3 (x = (n +c 1c) → x = (n +c 1c))
9 addceq1 4383 . . 3 (x = (n +c 1c) → (x +c 1c) = ((n +c 1c) +c 1c))
108, 9breq12d 4652 . 2 (x = (n +c 1c) → (x <c (x +c 1c) ↔ (n +c 1c) <c ((n +c 1c) +c 1c)))
11 id 19 . . 3 (x = Nx = N)
12 addceq1 4383 . . 3 (x = N → (x +c 1c) = (N +c 1c))
1311, 12breq12d 4652 . 2 (x = N → (x <c (x +c 1c) ↔ N <c (N +c 1c)))
14 0cnc 6138 . . . 4 0c NC
15 1cnc 6139 . . . 4 1c NC
16 addlecncs 6209 . . . 4 ((0c NC 1c NC ) → 0cc (0c +c 1c))
1714, 15, 16mp2an 653 . . 3 0cc (0c +c 1c)
18 0cnsuc 4401 . . . 4 (0c +c 1c) ≠ 0c
1918necomi 2598 . . 3 0c ≠ (0c +c 1c)
20 brltc 6114 . . 3 (0c <c (0c +c 1c) ↔ (0cc (0c +c 1c) 0c ≠ (0c +c 1c)))
2117, 19, 20mpbir2an 886 . 2 0c <c (0c +c 1c)
22 nnnc 6146 . . . . 5 (n Nnn NC )
23 peano2nc 6145 . . . . . 6 (n NC → (n +c 1c) NC )
2422, 23syl 15 . . . . 5 (n Nn → (n +c 1c) NC )
25 leaddc1 6214 . . . . . . 7 (((n NC (n +c 1c) NC 1c NC ) nc (n +c 1c)) → (n +c 1c) ≤c ((n +c 1c) +c 1c))
2625ex 423 . . . . . 6 ((n NC (n +c 1c) NC 1c NC ) → (nc (n +c 1c) → (n +c 1c) ≤c ((n +c 1c) +c 1c)))
2715, 26mp3an3 1266 . . . . 5 ((n NC (n +c 1c) NC ) → (nc (n +c 1c) → (n +c 1c) ≤c ((n +c 1c) +c 1c)))
2822, 24, 27syl2anc 642 . . . 4 (n Nn → (nc (n +c 1c) → (n +c 1c) ≤c ((n +c 1c) +c 1c)))
29 peano2 4403 . . . . . . 7 (n Nn → (n +c 1c) Nn )
30 suc11nnc 4558 . . . . . . 7 ((n Nn (n +c 1c) Nn ) → ((n +c 1c) = ((n +c 1c) +c 1c) ↔ n = (n +c 1c)))
3129, 30mpdan 649 . . . . . 6 (n Nn → ((n +c 1c) = ((n +c 1c) +c 1c) ↔ n = (n +c 1c)))
3231biimpd 198 . . . . 5 (n Nn → ((n +c 1c) = ((n +c 1c) +c 1c) → n = (n +c 1c)))
3332necon3d 2554 . . . 4 (n Nn → (n ≠ (n +c 1c) → (n +c 1c) ≠ ((n +c 1c) +c 1c)))
3428, 33anim12d 546 . . 3 (n Nn → ((nc (n +c 1c) n ≠ (n +c 1c)) → ((n +c 1c) ≤c ((n +c 1c) +c 1c) (n +c 1c) ≠ ((n +c 1c) +c 1c))))
35 brltc 6114 . . 3 (n <c (n +c 1c) ↔ (nc (n +c 1c) n ≠ (n +c 1c)))
36 brltc 6114 . . 3 ((n +c 1c) <c ((n +c 1c) +c 1c) ↔ ((n +c 1c) ≤c ((n +c 1c) +c 1c) (n +c 1c) ≠ ((n +c 1c) +c 1c)))
3734, 35, 363imtr4g 261 . 2 (n Nn → (n <c (n +c 1c) → (n +c 1c) <c ((n +c 1c) +c 1c)))
381, 4, 7, 10, 13, 21, 37finds 4411 1 (N NnN <c (N +c 1c))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 176   ∧ wa 358   ∧ w3a 934   = wceq 1642   ∈ wcel 1710   ≠ wne 2516  1cc1c 4134   Nn cnnc 4373  0cc0c 4374   +c cplc 4375   class class class wbr 4639   NC cncs 6088   ≤c clec 6089
 Copyright terms: Public domain W3C validator