Step | Hyp | Ref
| Expression |
1 | | nnltp1clem1 6261 |
. 2
⊢ {x ∣ x <c (x +c 1c)} ∈ V |
2 | | id 19 |
. . 3
⊢ (x = 0c → x = 0c) |
3 | | addceq1 4383 |
. . 3
⊢ (x = 0c → (x +c 1c) =
(0c +c
1c)) |
4 | 2, 3 | breq12d 4652 |
. 2
⊢ (x = 0c → (x <c (x +c 1c) ↔
0c <c (0c
+c 1c))) |
5 | | id 19 |
. . 3
⊢ (x = n →
x = n) |
6 | | addceq1 4383 |
. . 3
⊢ (x = n →
(x +c
1c) = (n
+c 1c)) |
7 | 5, 6 | breq12d 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)) |
10 | 8, 9 | breq12d 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 = N →
x = N) |
12 | | addceq1 4383 |
. . 3
⊢ (x = N →
(x +c
1c) = (N
+c 1c)) |
13 | 11, 12 | breq12d 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 ) → 0c ≤c
(0c +c
1c)) |
17 | 14, 15, 16 | mp2an 653 |
. . 3
⊢
0c ≤c (0c
+c 1c) |
18 | | 0cnsuc 4401 |
. . . 4
⊢
(0c +c 1c) ≠
0c |
19 | 18 | necomi 2598 |
. . 3
⊢
0c ≠ (0c +c
1c) |
20 | | brltc 6114 |
. . 3
⊢
(0c <c (0c
+c 1c) ↔ (0c
≤c (0c +c
1c) ∧ 0c
≠ (0c +c
1c))) |
21 | 17, 19, 20 | mpbir2an 886 |
. 2
⊢
0c <c (0c
+c 1c) |
22 | | nnnc 6146 |
. . . . 5
⊢ (n ∈ Nn → n ∈ NC
) |
23 | | peano2nc 6145 |
. . . . . 6
⊢ (n ∈ NC → (n
+c 1c) ∈
NC ) |
24 | 22, 23 | syl 15 |
. . . . 5
⊢ (n ∈ Nn → (n
+c 1c) ∈
NC ) |
25 | | leaddc1 6214 |
. . . . . . 7
⊢ (((n ∈ NC ∧ (n +c 1c) ∈ NC ∧ 1c ∈ NC ) ∧ n
≤c (n +c
1c)) → (n
+c 1c) ≤c ((n +c 1c)
+c 1c)) |
26 | 25 | ex 423 |
. . . . . 6
⊢ ((n ∈ NC ∧ (n +c 1c) ∈ NC ∧ 1c ∈ NC ) →
(n ≤c (n +c 1c) →
(n +c
1c) ≤c ((n
+c 1c) +c
1c))) |
27 | 15, 26 | mp3an3 1266 |
. . . . 5
⊢ ((n ∈ NC ∧ (n +c 1c) ∈ NC ) →
(n ≤c (n +c 1c) →
(n +c
1c) ≤c ((n
+c 1c) +c
1c))) |
28 | 22, 24, 27 | syl2anc 642 |
. . . 4
⊢ (n ∈ Nn → (n
≤c (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))) |
31 | 29, 30 | mpdan 649 |
. . . . . 6
⊢ (n ∈ Nn → ((n
+c 1c) = ((n +c 1c)
+c 1c) ↔ n = (n
+c 1c))) |
32 | 31 | biimpd 198 |
. . . . 5
⊢ (n ∈ Nn → ((n
+c 1c) = ((n +c 1c)
+c 1c) → n = (n
+c 1c))) |
33 | 32 | necon3d 2554 |
. . . 4
⊢ (n ∈ Nn → (n ≠
(n +c
1c) → (n
+c 1c) ≠ ((n +c 1c)
+c 1c))) |
34 | 28, 33 | anim12d 546 |
. . 3
⊢ (n ∈ Nn → ((n
≤c (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) ↔
(n ≤c (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))) |
37 | 34, 35, 36 | 3imtr4g 261 |
. 2
⊢ (n ∈ Nn → (n
<c (n +c
1c) → (n
+c 1c) <c ((n +c 1c)
+c 1c))) |
38 | 1, 4, 7, 10, 13, 21, 37 | finds 4411 |
1
⊢ (N ∈ Nn → N
<c (N +c
1c)) |