| Step | Hyp | Ref
| Expression |
| 1 | | oveq1 7438 |
. . . 4
⊢ (𝑗 = 2 → (𝑗 + 1) = (2 + 1)) |
| 2 | 1 | oveq2d 7447 |
. . 3
⊢ (𝑗 = 2 → (2↑(𝑗 + 1)) = (2↑(2 +
1))) |
| 3 | | oveq2 7439 |
. . . . 5
⊢ (𝑗 = 2 → (2 · 𝑗) = (2 ·
2)) |
| 4 | 3 | oveq1d 7446 |
. . . 4
⊢ (𝑗 = 2 → ((2 · 𝑗) + 1) = ((2 · 2) +
1)) |
| 5 | | id 22 |
. . . 4
⊢ (𝑗 = 2 → 𝑗 = 2) |
| 6 | 4, 5 | oveq12d 7449 |
. . 3
⊢ (𝑗 = 2 → (((2 · 𝑗) + 1)C𝑗) = (((2 · 2) +
1)C2)) |
| 7 | 2, 6 | breq12d 5156 |
. 2
⊢ (𝑗 = 2 → ((2↑(𝑗 + 1)) < (((2 · 𝑗) + 1)C𝑗) ↔ (2↑(2 + 1)) < (((2 ·
2) + 1)C2))) |
| 8 | | oveq1 7438 |
. . . 4
⊢ (𝑗 = 𝑘 → (𝑗 + 1) = (𝑘 + 1)) |
| 9 | 8 | oveq2d 7447 |
. . 3
⊢ (𝑗 = 𝑘 → (2↑(𝑗 + 1)) = (2↑(𝑘 + 1))) |
| 10 | | oveq2 7439 |
. . . . 5
⊢ (𝑗 = 𝑘 → (2 · 𝑗) = (2 · 𝑘)) |
| 11 | 10 | oveq1d 7446 |
. . . 4
⊢ (𝑗 = 𝑘 → ((2 · 𝑗) + 1) = ((2 · 𝑘) + 1)) |
| 12 | | id 22 |
. . . 4
⊢ (𝑗 = 𝑘 → 𝑗 = 𝑘) |
| 13 | 11, 12 | oveq12d 7449 |
. . 3
⊢ (𝑗 = 𝑘 → (((2 · 𝑗) + 1)C𝑗) = (((2 · 𝑘) + 1)C𝑘)) |
| 14 | 9, 13 | breq12d 5156 |
. 2
⊢ (𝑗 = 𝑘 → ((2↑(𝑗 + 1)) < (((2 · 𝑗) + 1)C𝑗) ↔ (2↑(𝑘 + 1)) < (((2 · 𝑘) + 1)C𝑘))) |
| 15 | | oveq1 7438 |
. . . 4
⊢ (𝑗 = (𝑘 + 1) → (𝑗 + 1) = ((𝑘 + 1) + 1)) |
| 16 | 15 | oveq2d 7447 |
. . 3
⊢ (𝑗 = (𝑘 + 1) → (2↑(𝑗 + 1)) = (2↑((𝑘 + 1) + 1))) |
| 17 | | oveq2 7439 |
. . . . 5
⊢ (𝑗 = (𝑘 + 1) → (2 · 𝑗) = (2 · (𝑘 + 1))) |
| 18 | 17 | oveq1d 7446 |
. . . 4
⊢ (𝑗 = (𝑘 + 1) → ((2 · 𝑗) + 1) = ((2 · (𝑘 + 1)) + 1)) |
| 19 | | id 22 |
. . . 4
⊢ (𝑗 = (𝑘 + 1) → 𝑗 = (𝑘 + 1)) |
| 20 | 18, 19 | oveq12d 7449 |
. . 3
⊢ (𝑗 = (𝑘 + 1) → (((2 · 𝑗) + 1)C𝑗) = (((2 · (𝑘 + 1)) + 1)C(𝑘 + 1))) |
| 21 | 16, 20 | breq12d 5156 |
. 2
⊢ (𝑗 = (𝑘 + 1) → ((2↑(𝑗 + 1)) < (((2 · 𝑗) + 1)C𝑗) ↔ (2↑((𝑘 + 1) + 1)) < (((2 · (𝑘 + 1)) + 1)C(𝑘 + 1)))) |
| 22 | | oveq1 7438 |
. . . 4
⊢ (𝑗 = 𝑁 → (𝑗 + 1) = (𝑁 + 1)) |
| 23 | 22 | oveq2d 7447 |
. . 3
⊢ (𝑗 = 𝑁 → (2↑(𝑗 + 1)) = (2↑(𝑁 + 1))) |
| 24 | | oveq2 7439 |
. . . . 5
⊢ (𝑗 = 𝑁 → (2 · 𝑗) = (2 · 𝑁)) |
| 25 | 24 | oveq1d 7446 |
. . . 4
⊢ (𝑗 = 𝑁 → ((2 · 𝑗) + 1) = ((2 · 𝑁) + 1)) |
| 26 | | id 22 |
. . . 4
⊢ (𝑗 = 𝑁 → 𝑗 = 𝑁) |
| 27 | 25, 26 | oveq12d 7449 |
. . 3
⊢ (𝑗 = 𝑁 → (((2 · 𝑗) + 1)C𝑗) = (((2 · 𝑁) + 1)C𝑁)) |
| 28 | 23, 27 | breq12d 5156 |
. 2
⊢ (𝑗 = 𝑁 → ((2↑(𝑗 + 1)) < (((2 · 𝑗) + 1)C𝑗) ↔ (2↑(𝑁 + 1)) < (((2 · 𝑁) + 1)C𝑁))) |
| 29 | | 8lt10 12865 |
. . . . 5
⊢ 8 <
;10 |
| 30 | | eqid 2737 |
. . . . . . 7
⊢ 8 =
8 |
| 31 | | cu2 14239 |
. . . . . . 7
⊢
(2↑3) = 8 |
| 32 | 30, 31 | eqtr4i 2768 |
. . . . . 6
⊢ 8 =
(2↑3) |
| 33 | | 5bc2eq10 42143 |
. . . . . . 7
⊢ (5C2) =
;10 |
| 34 | 33 | eqcomi 2746 |
. . . . . 6
⊢ ;10 = (5C2) |
| 35 | 32, 34 | breq12i 5152 |
. . . . 5
⊢ (8 <
;10 ↔ (2↑3) <
(5C2)) |
| 36 | 29, 35 | mpbi 230 |
. . . 4
⊢
(2↑3) < (5C2) |
| 37 | | df-3 12330 |
. . . . . 6
⊢ 3 = (2 +
1) |
| 38 | 37 | oveq2i 7442 |
. . . . 5
⊢
(2↑3) = (2↑(2 + 1)) |
| 39 | | eqid 2737 |
. . . . . . 7
⊢ 5 =
5 |
| 40 | | 2t2e4 12430 |
. . . . . . . . 9
⊢ (2
· 2) = 4 |
| 41 | 40 | oveq1i 7441 |
. . . . . . . 8
⊢ ((2
· 2) + 1) = (4 + 1) |
| 42 | | 4p1e5 12412 |
. . . . . . . 8
⊢ (4 + 1) =
5 |
| 43 | 41, 42 | eqtri 2765 |
. . . . . . 7
⊢ ((2
· 2) + 1) = 5 |
| 44 | 39, 43 | eqtr4i 2768 |
. . . . . 6
⊢ 5 = ((2
· 2) + 1) |
| 45 | 44 | oveq1i 7441 |
. . . . 5
⊢ (5C2) =
(((2 · 2) + 1)C2) |
| 46 | 38, 45 | breq12i 5152 |
. . . 4
⊢
((2↑3) < (5C2) ↔ (2↑(2 + 1)) < (((2 · 2) +
1)C2)) |
| 47 | 36, 46 | mpbi 230 |
. . 3
⊢
(2↑(2 + 1)) < (((2 · 2) + 1)C2) |
| 48 | 47 | a1i 11 |
. 2
⊢ (𝜑 → (2↑(2 + 1)) < (((2
· 2) + 1)C2)) |
| 49 | | 2re 12340 |
. . . . 5
⊢ 2 ∈
ℝ |
| 50 | 49 | a1i 11 |
. . . 4
⊢ ((𝜑 ∧ (2↑(𝑘 + 1)) < (((2 · 𝑘) + 1)C𝑘) ∧ (𝑘 ∈ ℤ ∧ 2 ≤ 𝑘)) → 2 ∈
ℝ) |
| 51 | | simpl 482 |
. . . . . . . . . . . 12
⊢ ((𝑘 ∈ ℤ ∧ 2 ≤
𝑘) → 𝑘 ∈
ℤ) |
| 52 | | 0red 11264 |
. . . . . . . . . . . . 13
⊢ ((𝑘 ∈ ℤ ∧ 2 ≤
𝑘) → 0 ∈
ℝ) |
| 53 | 49 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝑘 ∈ ℤ ∧ 2 ≤
𝑘) → 2 ∈
ℝ) |
| 54 | 51 | zred 12722 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑘 ∈ ℤ ∧ 2 ≤
𝑘) → 𝑘 ∈
ℝ) |
| 55 | | 2pos 12369 |
. . . . . . . . . . . . . . . . . . 19
⊢ 0 <
2 |
| 56 | 55 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑘 ∈ ℤ ∧ 2 ≤
𝑘) → 0 <
2) |
| 57 | | simpr 484 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑘 ∈ ℤ ∧ 2 ≤
𝑘) → 2 ≤ 𝑘) |
| 58 | 52, 53, 54, 56, 57 | ltletrd 11421 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑘 ∈ ℤ ∧ 2 ≤
𝑘) → 0 < 𝑘) |
| 59 | 51, 58 | jca 511 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑘 ∈ ℤ ∧ 2 ≤
𝑘) → (𝑘 ∈ ℤ ∧ 0 <
𝑘)) |
| 60 | | elnnz 12623 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ ℕ ↔ (𝑘 ∈ ℤ ∧ 0 <
𝑘)) |
| 61 | 59, 60 | sylibr 234 |
. . . . . . . . . . . . . . 15
⊢ ((𝑘 ∈ ℤ ∧ 2 ≤
𝑘) → 𝑘 ∈
ℕ) |
| 62 | | nnnn0 12533 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℕ0) |
| 63 | 61, 62 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝑘 ∈ ℤ ∧ 2 ≤
𝑘) → 𝑘 ∈
ℕ0) |
| 64 | 63 | nn0red 12588 |
. . . . . . . . . . . . 13
⊢ ((𝑘 ∈ ℤ ∧ 2 ≤
𝑘) → 𝑘 ∈
ℝ) |
| 65 | 52, 53, 64, 56, 57 | ltletrd 11421 |
. . . . . . . . . . . 12
⊢ ((𝑘 ∈ ℤ ∧ 2 ≤
𝑘) → 0 < 𝑘) |
| 66 | 51, 65 | jca 511 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈ ℤ ∧ 2 ≤
𝑘) → (𝑘 ∈ ℤ ∧ 0 <
𝑘)) |
| 67 | 66, 60 | sylibr 234 |
. . . . . . . . . 10
⊢ ((𝑘 ∈ ℤ ∧ 2 ≤
𝑘) → 𝑘 ∈
ℕ) |
| 68 | 67 | nnred 12281 |
. . . . . . . . 9
⊢ ((𝑘 ∈ ℤ ∧ 2 ≤
𝑘) → 𝑘 ∈
ℝ) |
| 69 | 68 | 3ad2ant3 1136 |
. . . . . . . 8
⊢ ((𝜑 ∧ (2↑(𝑘 + 1)) < (((2 · 𝑘) + 1)C𝑘) ∧ (𝑘 ∈ ℤ ∧ 2 ≤ 𝑘)) → 𝑘 ∈ ℝ) |
| 70 | 50, 69 | remulcld 11291 |
. . . . . . 7
⊢ ((𝜑 ∧ (2↑(𝑘 + 1)) < (((2 · 𝑘) + 1)C𝑘) ∧ (𝑘 ∈ ℤ ∧ 2 ≤ 𝑘)) → (2 · 𝑘) ∈
ℝ) |
| 71 | | 3re 12346 |
. . . . . . . 8
⊢ 3 ∈
ℝ |
| 72 | 71 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ (2↑(𝑘 + 1)) < (((2 · 𝑘) + 1)C𝑘) ∧ (𝑘 ∈ ℤ ∧ 2 ≤ 𝑘)) → 3 ∈
ℝ) |
| 73 | 70, 72 | readdcld 11290 |
. . . . . 6
⊢ ((𝜑 ∧ (2↑(𝑘 + 1)) < (((2 · 𝑘) + 1)C𝑘) ∧ (𝑘 ∈ ℤ ∧ 2 ≤ 𝑘)) → ((2 · 𝑘) + 3) ∈
ℝ) |
| 74 | 69, 50 | readdcld 11290 |
. . . . . 6
⊢ ((𝜑 ∧ (2↑(𝑘 + 1)) < (((2 · 𝑘) + 1)C𝑘) ∧ (𝑘 ∈ ℤ ∧ 2 ≤ 𝑘)) → (𝑘 + 2) ∈ ℝ) |
| 75 | 68, 53 | readdcld 11290 |
. . . . . . . . . 10
⊢ ((𝑘 ∈ ℤ ∧ 2 ≤
𝑘) → (𝑘 + 2) ∈
ℝ) |
| 76 | 67 | nngt0d 12315 |
. . . . . . . . . 10
⊢ ((𝑘 ∈ ℤ ∧ 2 ≤
𝑘) → 0 < 𝑘) |
| 77 | | 2rp 13039 |
. . . . . . . . . . . 12
⊢ 2 ∈
ℝ+ |
| 78 | 77 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈ ℤ ∧ 2 ≤
𝑘) → 2 ∈
ℝ+) |
| 79 | 68, 78 | ltaddrpd 13110 |
. . . . . . . . . 10
⊢ ((𝑘 ∈ ℤ ∧ 2 ≤
𝑘) → 𝑘 < (𝑘 + 2)) |
| 80 | 52, 68, 75, 76, 79 | lttrd 11422 |
. . . . . . . . 9
⊢ ((𝑘 ∈ ℤ ∧ 2 ≤
𝑘) → 0 < (𝑘 + 2)) |
| 81 | 52, 80 | ltned 11397 |
. . . . . . . 8
⊢ ((𝑘 ∈ ℤ ∧ 2 ≤
𝑘) → 0 ≠ (𝑘 + 2)) |
| 82 | 81 | necomd 2996 |
. . . . . . 7
⊢ ((𝑘 ∈ ℤ ∧ 2 ≤
𝑘) → (𝑘 + 2) ≠ 0) |
| 83 | 82 | 3ad2ant3 1136 |
. . . . . 6
⊢ ((𝜑 ∧ (2↑(𝑘 + 1)) < (((2 · 𝑘) + 1)C𝑘) ∧ (𝑘 ∈ ℤ ∧ 2 ≤ 𝑘)) → (𝑘 + 2) ≠ 0) |
| 84 | 73, 74, 83 | redivcld 12095 |
. . . . 5
⊢ ((𝜑 ∧ (2↑(𝑘 + 1)) < (((2 · 𝑘) + 1)C𝑘) ∧ (𝑘 ∈ ℤ ∧ 2 ≤ 𝑘)) → (((2 · 𝑘) + 3) / (𝑘 + 2)) ∈ ℝ) |
| 85 | 50, 84 | remulcld 11291 |
. . . 4
⊢ ((𝜑 ∧ (2↑(𝑘 + 1)) < (((2 · 𝑘) + 1)C𝑘) ∧ (𝑘 ∈ ℤ ∧ 2 ≤ 𝑘)) → (2 · (((2
· 𝑘) + 3) / (𝑘 + 2))) ∈
ℝ) |
| 86 | | 1nn0 12542 |
. . . . . . . 8
⊢ 1 ∈
ℕ0 |
| 87 | 86 | a1i 11 |
. . . . . . 7
⊢ ((𝑘 ∈ ℤ ∧ 2 ≤
𝑘) → 1 ∈
ℕ0) |
| 88 | 63, 87 | nn0addcld 12591 |
. . . . . 6
⊢ ((𝑘 ∈ ℤ ∧ 2 ≤
𝑘) → (𝑘 + 1) ∈
ℕ0) |
| 89 | 53, 88 | reexpcld 14203 |
. . . . 5
⊢ ((𝑘 ∈ ℤ ∧ 2 ≤
𝑘) → (2↑(𝑘 + 1)) ∈
ℝ) |
| 90 | 89 | 3ad2ant3 1136 |
. . . 4
⊢ ((𝜑 ∧ (2↑(𝑘 + 1)) < (((2 · 𝑘) + 1)C𝑘) ∧ (𝑘 ∈ ℤ ∧ 2 ≤ 𝑘)) → (2↑(𝑘 + 1)) ∈
ℝ) |
| 91 | | 2nn0 12543 |
. . . . . . . . . 10
⊢ 2 ∈
ℕ0 |
| 92 | 91 | a1i 11 |
. . . . . . . . 9
⊢ ((𝑘 ∈ ℤ ∧ 2 ≤
𝑘) → 2 ∈
ℕ0) |
| 93 | 92, 63 | nn0mulcld 12592 |
. . . . . . . 8
⊢ ((𝑘 ∈ ℤ ∧ 2 ≤
𝑘) → (2 · 𝑘) ∈
ℕ0) |
| 94 | 93, 87 | nn0addcld 12591 |
. . . . . . 7
⊢ ((𝑘 ∈ ℤ ∧ 2 ≤
𝑘) → ((2 ·
𝑘) + 1) ∈
ℕ0) |
| 95 | | bccl 14361 |
. . . . . . 7
⊢ ((((2
· 𝑘) + 1) ∈
ℕ0 ∧ 𝑘
∈ ℤ) → (((2 · 𝑘) + 1)C𝑘) ∈
ℕ0) |
| 96 | 94, 51, 95 | syl2anc 584 |
. . . . . 6
⊢ ((𝑘 ∈ ℤ ∧ 2 ≤
𝑘) → (((2 ·
𝑘) + 1)C𝑘) ∈
ℕ0) |
| 97 | 96 | nn0red 12588 |
. . . . 5
⊢ ((𝑘 ∈ ℤ ∧ 2 ≤
𝑘) → (((2 ·
𝑘) + 1)C𝑘) ∈ ℝ) |
| 98 | 97 | 3ad2ant3 1136 |
. . . 4
⊢ ((𝜑 ∧ (2↑(𝑘 + 1)) < (((2 · 𝑘) + 1)C𝑘) ∧ (𝑘 ∈ ℤ ∧ 2 ≤ 𝑘)) → (((2 · 𝑘) + 1)C𝑘) ∈ ℝ) |
| 99 | | 0le2 12368 |
. . . . 5
⊢ 0 ≤
2 |
| 100 | 99 | a1i 11 |
. . . 4
⊢ ((𝜑 ∧ (2↑(𝑘 + 1)) < (((2 · 𝑘) + 1)C𝑘) ∧ (𝑘 ∈ ℤ ∧ 2 ≤ 𝑘)) → 0 ≤
2) |
| 101 | | eqid 2737 |
. . . . . . . 8
⊢ 2 =
2 |
| 102 | | 2t1e2 12429 |
. . . . . . . 8
⊢ (2
· 1) = 2 |
| 103 | 101, 102 | eqtr4i 2768 |
. . . . . . 7
⊢ 2 = (2
· 1) |
| 104 | 103 | a1i 11 |
. . . . . 6
⊢ ((𝑘 ∈ ℤ ∧ 2 ≤
𝑘) → 2 = (2 ·
1)) |
| 105 | | 1red 11262 |
. . . . . . 7
⊢ ((𝑘 ∈ ℤ ∧ 2 ≤
𝑘) → 1 ∈
ℝ) |
| 106 | 53, 68 | remulcld 11291 |
. . . . . . . . 9
⊢ ((𝑘 ∈ ℤ ∧ 2 ≤
𝑘) → (2 · 𝑘) ∈
ℝ) |
| 107 | 71 | a1i 11 |
. . . . . . . . 9
⊢ ((𝑘 ∈ ℤ ∧ 2 ≤
𝑘) → 3 ∈
ℝ) |
| 108 | 106, 107 | readdcld 11290 |
. . . . . . . 8
⊢ ((𝑘 ∈ ℤ ∧ 2 ≤
𝑘) → ((2 ·
𝑘) + 3) ∈
ℝ) |
| 109 | 108, 75, 82 | redivcld 12095 |
. . . . . . 7
⊢ ((𝑘 ∈ ℤ ∧ 2 ≤
𝑘) → (((2 ·
𝑘) + 3) / (𝑘 + 2)) ∈
ℝ) |
| 110 | | nnrp 13046 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℝ+) |
| 111 | 77 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ ℕ → 2 ∈
ℝ+) |
| 112 | 110, 111 | rpaddcld 13092 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ ℕ → (𝑘 + 2) ∈
ℝ+) |
| 113 | 112 | rpcnd 13079 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ → (𝑘 + 2) ∈
ℂ) |
| 114 | 113 | mulridd 11278 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℕ → ((𝑘 + 2) · 1) = (𝑘 + 2)) |
| 115 | | nnre 12273 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℝ) |
| 116 | 49 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ → 2 ∈
ℝ) |
| 117 | 116, 115 | remulcld 11291 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ → (2
· 𝑘) ∈
ℝ) |
| 118 | 71 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ → 3 ∈
ℝ) |
| 119 | 110 | rpge0d 13081 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ ℕ → 0 ≤
𝑘) |
| 120 | | 1le2 12475 |
. . . . . . . . . . . . 13
⊢ 1 ≤
2 |
| 121 | 120 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ ℕ → 1 ≤
2) |
| 122 | 115, 116,
119, 121 | lemulge12d 12206 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ → 𝑘 ≤ (2 · 𝑘)) |
| 123 | | 2lt3 12438 |
. . . . . . . . . . . 12
⊢ 2 <
3 |
| 124 | 123 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ → 2 <
3) |
| 125 | 115, 116,
117, 118, 122, 124 | leltaddd 11885 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℕ → (𝑘 + 2) < ((2 · 𝑘) + 3)) |
| 126 | 114, 125 | eqbrtrd 5165 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℕ → ((𝑘 + 2) · 1) < ((2
· 𝑘) +
3)) |
| 127 | | 1red 11262 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℕ → 1 ∈
ℝ) |
| 128 | 117, 118 | readdcld 11290 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℕ → ((2
· 𝑘) + 3) ∈
ℝ) |
| 129 | 127, 128,
112 | ltmuldiv2d 13125 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℕ → (((𝑘 + 2) · 1) < ((2
· 𝑘) + 3) ↔ 1
< (((2 · 𝑘) + 3)
/ (𝑘 +
2)))) |
| 130 | 126, 129 | mpbid 232 |
. . . . . . . 8
⊢ (𝑘 ∈ ℕ → 1 <
(((2 · 𝑘) + 3) /
(𝑘 + 2))) |
| 131 | 67, 130 | syl 17 |
. . . . . . 7
⊢ ((𝑘 ∈ ℤ ∧ 2 ≤
𝑘) → 1 < (((2
· 𝑘) + 3) / (𝑘 + 2))) |
| 132 | 105, 109,
78, 131 | ltmul2dd 13133 |
. . . . . 6
⊢ ((𝑘 ∈ ℤ ∧ 2 ≤
𝑘) → (2 · 1)
< (2 · (((2 · 𝑘) + 3) / (𝑘 + 2)))) |
| 133 | 104, 132 | eqbrtrd 5165 |
. . . . 5
⊢ ((𝑘 ∈ ℤ ∧ 2 ≤
𝑘) → 2 < (2
· (((2 · 𝑘) +
3) / (𝑘 +
2)))) |
| 134 | 133 | 3ad2ant3 1136 |
. . . 4
⊢ ((𝜑 ∧ (2↑(𝑘 + 1)) < (((2 · 𝑘) + 1)C𝑘) ∧ (𝑘 ∈ ℤ ∧ 2 ≤ 𝑘)) → 2 < (2 ·
(((2 · 𝑘) + 3) /
(𝑘 + 2)))) |
| 135 | 99 | a1i 11 |
. . . . . 6
⊢ ((𝑘 ∈ ℤ ∧ 2 ≤
𝑘) → 0 ≤
2) |
| 136 | 53, 88, 135 | expge0d 14204 |
. . . . 5
⊢ ((𝑘 ∈ ℤ ∧ 2 ≤
𝑘) → 0 ≤
(2↑(𝑘 +
1))) |
| 137 | 136 | 3ad2ant3 1136 |
. . . 4
⊢ ((𝜑 ∧ (2↑(𝑘 + 1)) < (((2 · 𝑘) + 1)C𝑘) ∧ (𝑘 ∈ ℤ ∧ 2 ≤ 𝑘)) → 0 ≤ (2↑(𝑘 + 1))) |
| 138 | | simp2 1138 |
. . . 4
⊢ ((𝜑 ∧ (2↑(𝑘 + 1)) < (((2 · 𝑘) + 1)C𝑘) ∧ (𝑘 ∈ ℤ ∧ 2 ≤ 𝑘)) → (2↑(𝑘 + 1)) < (((2 · 𝑘) + 1)C𝑘)) |
| 139 | 50, 85, 90, 98, 100, 134, 137, 138 | ltmul12ad 12209 |
. . 3
⊢ ((𝜑 ∧ (2↑(𝑘 + 1)) < (((2 · 𝑘) + 1)C𝑘) ∧ (𝑘 ∈ ℤ ∧ 2 ≤ 𝑘)) → (2 ·
(2↑(𝑘 + 1))) < ((2
· (((2 · 𝑘) +
3) / (𝑘 + 2))) ·
(((2 · 𝑘) + 1)C𝑘))) |
| 140 | | 2cnd 12344 |
. . . . . . . 8
⊢ ((𝑘 ∈ ℤ ∧ 2 ≤
𝑘) → 2 ∈
ℂ) |
| 141 | 140, 87, 88 | expaddd 14188 |
. . . . . . 7
⊢ ((𝑘 ∈ ℤ ∧ 2 ≤
𝑘) → (2↑((𝑘 + 1) + 1)) = ((2↑(𝑘 + 1)) ·
(2↑1))) |
| 142 | 140, 88 | expcld 14186 |
. . . . . . . . 9
⊢ ((𝑘 ∈ ℤ ∧ 2 ≤
𝑘) → (2↑(𝑘 + 1)) ∈
ℂ) |
| 143 | 140, 87 | expcld 14186 |
. . . . . . . . 9
⊢ ((𝑘 ∈ ℤ ∧ 2 ≤
𝑘) → (2↑1) ∈
ℂ) |
| 144 | 142, 143 | mulcomd 11282 |
. . . . . . . 8
⊢ ((𝑘 ∈ ℤ ∧ 2 ≤
𝑘) → ((2↑(𝑘 + 1)) · (2↑1)) =
((2↑1) · (2↑(𝑘 + 1)))) |
| 145 | 140 | exp1d 14181 |
. . . . . . . . 9
⊢ ((𝑘 ∈ ℤ ∧ 2 ≤
𝑘) → (2↑1) =
2) |
| 146 | 145 | oveq1d 7446 |
. . . . . . . 8
⊢ ((𝑘 ∈ ℤ ∧ 2 ≤
𝑘) → ((2↑1)
· (2↑(𝑘 + 1)))
= (2 · (2↑(𝑘 +
1)))) |
| 147 | | eqidd 2738 |
. . . . . . . 8
⊢ ((𝑘 ∈ ℤ ∧ 2 ≤
𝑘) → (2 ·
(2↑(𝑘 + 1))) = (2
· (2↑(𝑘 +
1)))) |
| 148 | 144, 146,
147 | 3eqtrd 2781 |
. . . . . . 7
⊢ ((𝑘 ∈ ℤ ∧ 2 ≤
𝑘) → ((2↑(𝑘 + 1)) · (2↑1)) = (2
· (2↑(𝑘 +
1)))) |
| 149 | 141, 148 | eqtrd 2777 |
. . . . . 6
⊢ ((𝑘 ∈ ℤ ∧ 2 ≤
𝑘) → (2↑((𝑘 + 1) + 1)) = (2 ·
(2↑(𝑘 +
1)))) |
| 150 | 149 | eqcomd 2743 |
. . . . 5
⊢ ((𝑘 ∈ ℤ ∧ 2 ≤
𝑘) → (2 ·
(2↑(𝑘 + 1))) =
(2↑((𝑘 + 1) +
1))) |
| 151 | 150 | 3ad2ant3 1136 |
. . . 4
⊢ ((𝜑 ∧ (2↑(𝑘 + 1)) < (((2 · 𝑘) + 1)C𝑘) ∧ (𝑘 ∈ ℤ ∧ 2 ≤ 𝑘)) → (2 ·
(2↑(𝑘 + 1))) =
(2↑((𝑘 + 1) +
1))) |
| 152 | 63 | 2np3bcnp1 42145 |
. . . . . . 7
⊢ ((𝑘 ∈ ℤ ∧ 2 ≤
𝑘) → (((2 ·
(𝑘 + 1)) + 1)C(𝑘 + 1)) = ((((2 · 𝑘) + 1)C𝑘) · (2 · (((2 · 𝑘) + 3) / (𝑘 + 2))))) |
| 153 | 96 | nn0cnd 12589 |
. . . . . . . 8
⊢ ((𝑘 ∈ ℤ ∧ 2 ≤
𝑘) → (((2 ·
𝑘) + 1)C𝑘) ∈ ℂ) |
| 154 | 67 | nncnd 12282 |
. . . . . . . . . . . 12
⊢ ((𝑘 ∈ ℤ ∧ 2 ≤
𝑘) → 𝑘 ∈
ℂ) |
| 155 | 140, 154 | mulcld 11281 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈ ℤ ∧ 2 ≤
𝑘) → (2 · 𝑘) ∈
ℂ) |
| 156 | | 3cn 12347 |
. . . . . . . . . . . 12
⊢ 3 ∈
ℂ |
| 157 | 156 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈ ℤ ∧ 2 ≤
𝑘) → 3 ∈
ℂ) |
| 158 | 155, 157 | addcld 11280 |
. . . . . . . . . 10
⊢ ((𝑘 ∈ ℤ ∧ 2 ≤
𝑘) → ((2 ·
𝑘) + 3) ∈
ℂ) |
| 159 | 154, 140 | addcld 11280 |
. . . . . . . . . 10
⊢ ((𝑘 ∈ ℤ ∧ 2 ≤
𝑘) → (𝑘 + 2) ∈
ℂ) |
| 160 | 158, 159,
82 | divcld 12043 |
. . . . . . . . 9
⊢ ((𝑘 ∈ ℤ ∧ 2 ≤
𝑘) → (((2 ·
𝑘) + 3) / (𝑘 + 2)) ∈
ℂ) |
| 161 | 140, 160 | mulcld 11281 |
. . . . . . . 8
⊢ ((𝑘 ∈ ℤ ∧ 2 ≤
𝑘) → (2 · (((2
· 𝑘) + 3) / (𝑘 + 2))) ∈
ℂ) |
| 162 | 153, 161 | mulcomd 11282 |
. . . . . . 7
⊢ ((𝑘 ∈ ℤ ∧ 2 ≤
𝑘) → ((((2 ·
𝑘) + 1)C𝑘) · (2 · (((2 · 𝑘) + 3) / (𝑘 + 2)))) = ((2 · (((2 · 𝑘) + 3) / (𝑘 + 2))) · (((2 · 𝑘) + 1)C𝑘))) |
| 163 | 152, 162 | eqtrd 2777 |
. . . . . 6
⊢ ((𝑘 ∈ ℤ ∧ 2 ≤
𝑘) → (((2 ·
(𝑘 + 1)) + 1)C(𝑘 + 1)) = ((2 · (((2
· 𝑘) + 3) / (𝑘 + 2))) · (((2 ·
𝑘) + 1)C𝑘))) |
| 164 | 163 | eqcomd 2743 |
. . . . 5
⊢ ((𝑘 ∈ ℤ ∧ 2 ≤
𝑘) → ((2 · (((2
· 𝑘) + 3) / (𝑘 + 2))) · (((2 ·
𝑘) + 1)C𝑘)) = (((2 · (𝑘 + 1)) + 1)C(𝑘 + 1))) |
| 165 | 164 | 3ad2ant3 1136 |
. . . 4
⊢ ((𝜑 ∧ (2↑(𝑘 + 1)) < (((2 · 𝑘) + 1)C𝑘) ∧ (𝑘 ∈ ℤ ∧ 2 ≤ 𝑘)) → ((2 · (((2
· 𝑘) + 3) / (𝑘 + 2))) · (((2 ·
𝑘) + 1)C𝑘)) = (((2 · (𝑘 + 1)) + 1)C(𝑘 + 1))) |
| 166 | 151, 165 | breq12d 5156 |
. . 3
⊢ ((𝜑 ∧ (2↑(𝑘 + 1)) < (((2 · 𝑘) + 1)C𝑘) ∧ (𝑘 ∈ ℤ ∧ 2 ≤ 𝑘)) → ((2 ·
(2↑(𝑘 + 1))) < ((2
· (((2 · 𝑘) +
3) / (𝑘 + 2))) ·
(((2 · 𝑘) + 1)C𝑘)) ↔ (2↑((𝑘 + 1) + 1)) < (((2 ·
(𝑘 + 1)) + 1)C(𝑘 + 1)))) |
| 167 | 139, 166 | mpbid 232 |
. 2
⊢ ((𝜑 ∧ (2↑(𝑘 + 1)) < (((2 · 𝑘) + 1)C𝑘) ∧ (𝑘 ∈ ℤ ∧ 2 ≤ 𝑘)) → (2↑((𝑘 + 1) + 1)) < (((2 ·
(𝑘 + 1)) + 1)C(𝑘 + 1))) |
| 168 | | 2z 12649 |
. . 3
⊢ 2 ∈
ℤ |
| 169 | 168 | a1i 11 |
. 2
⊢ (𝜑 → 2 ∈
ℤ) |
| 170 | | 2ap1caineq.1 |
. 2
⊢ (𝜑 → 𝑁 ∈ ℤ) |
| 171 | | 2ap1caineq.2 |
. 2
⊢ (𝜑 → 2 ≤ 𝑁) |
| 172 | 7, 14, 21, 28, 48, 167, 169, 170, 171 | uzindd 41978 |
1
⊢ (𝜑 → (2↑(𝑁 + 1)) < (((2 · 𝑁) + 1)C𝑁)) |