Step | Hyp | Ref
| Expression |
1 | | oveq1 7150 |
. . . 4
⊢ (𝑗 = 2 → (𝑗 + 1) = (2 + 1)) |
2 | 1 | oveq2d 7159 |
. . 3
⊢ (𝑗 = 2 → (2↑(𝑗 + 1)) = (2↑(2 +
1))) |
3 | | oveq2 7151 |
. . . . 5
⊢ (𝑗 = 2 → (2 · 𝑗) = (2 ·
2)) |
4 | 3 | oveq1d 7158 |
. . . 4
⊢ (𝑗 = 2 → ((2 · 𝑗) + 1) = ((2 · 2) +
1)) |
5 | | id 22 |
. . . 4
⊢ (𝑗 = 2 → 𝑗 = 2) |
6 | 4, 5 | oveq12d 7161 |
. . 3
⊢ (𝑗 = 2 → (((2 · 𝑗) + 1)C𝑗) = (((2 · 2) +
1)C2)) |
7 | 2, 6 | breq12d 5038 |
. 2
⊢ (𝑗 = 2 → ((2↑(𝑗 + 1)) < (((2 · 𝑗) + 1)C𝑗) ↔ (2↑(2 + 1)) < (((2 ·
2) + 1)C2))) |
8 | | oveq1 7150 |
. . . 4
⊢ (𝑗 = 𝑘 → (𝑗 + 1) = (𝑘 + 1)) |
9 | 8 | oveq2d 7159 |
. . 3
⊢ (𝑗 = 𝑘 → (2↑(𝑗 + 1)) = (2↑(𝑘 + 1))) |
10 | | oveq2 7151 |
. . . . 5
⊢ (𝑗 = 𝑘 → (2 · 𝑗) = (2 · 𝑘)) |
11 | 10 | oveq1d 7158 |
. . . 4
⊢ (𝑗 = 𝑘 → ((2 · 𝑗) + 1) = ((2 · 𝑘) + 1)) |
12 | | id 22 |
. . . 4
⊢ (𝑗 = 𝑘 → 𝑗 = 𝑘) |
13 | 11, 12 | oveq12d 7161 |
. . 3
⊢ (𝑗 = 𝑘 → (((2 · 𝑗) + 1)C𝑗) = (((2 · 𝑘) + 1)C𝑘)) |
14 | 9, 13 | breq12d 5038 |
. 2
⊢ (𝑗 = 𝑘 → ((2↑(𝑗 + 1)) < (((2 · 𝑗) + 1)C𝑗) ↔ (2↑(𝑘 + 1)) < (((2 · 𝑘) + 1)C𝑘))) |
15 | | oveq1 7150 |
. . . 4
⊢ (𝑗 = (𝑘 + 1) → (𝑗 + 1) = ((𝑘 + 1) + 1)) |
16 | 15 | oveq2d 7159 |
. . 3
⊢ (𝑗 = (𝑘 + 1) → (2↑(𝑗 + 1)) = (2↑((𝑘 + 1) + 1))) |
17 | | oveq2 7151 |
. . . . 5
⊢ (𝑗 = (𝑘 + 1) → (2 · 𝑗) = (2 · (𝑘 + 1))) |
18 | 17 | oveq1d 7158 |
. . . 4
⊢ (𝑗 = (𝑘 + 1) → ((2 · 𝑗) + 1) = ((2 · (𝑘 + 1)) + 1)) |
19 | | id 22 |
. . . 4
⊢ (𝑗 = (𝑘 + 1) → 𝑗 = (𝑘 + 1)) |
20 | 18, 19 | oveq12d 7161 |
. . 3
⊢ (𝑗 = (𝑘 + 1) → (((2 · 𝑗) + 1)C𝑗) = (((2 · (𝑘 + 1)) + 1)C(𝑘 + 1))) |
21 | 16, 20 | breq12d 5038 |
. 2
⊢ (𝑗 = (𝑘 + 1) → ((2↑(𝑗 + 1)) < (((2 · 𝑗) + 1)C𝑗) ↔ (2↑((𝑘 + 1) + 1)) < (((2 · (𝑘 + 1)) + 1)C(𝑘 + 1)))) |
22 | | oveq1 7150 |
. . . 4
⊢ (𝑗 = 𝑁 → (𝑗 + 1) = (𝑁 + 1)) |
23 | 22 | oveq2d 7159 |
. . 3
⊢ (𝑗 = 𝑁 → (2↑(𝑗 + 1)) = (2↑(𝑁 + 1))) |
24 | | oveq2 7151 |
. . . . 5
⊢ (𝑗 = 𝑁 → (2 · 𝑗) = (2 · 𝑁)) |
25 | 24 | oveq1d 7158 |
. . . 4
⊢ (𝑗 = 𝑁 → ((2 · 𝑗) + 1) = ((2 · 𝑁) + 1)) |
26 | | id 22 |
. . . 4
⊢ (𝑗 = 𝑁 → 𝑗 = 𝑁) |
27 | 25, 26 | oveq12d 7161 |
. . 3
⊢ (𝑗 = 𝑁 → (((2 · 𝑗) + 1)C𝑗) = (((2 · 𝑁) + 1)C𝑁)) |
28 | 23, 27 | breq12d 5038 |
. 2
⊢ (𝑗 = 𝑁 → ((2↑(𝑗 + 1)) < (((2 · 𝑗) + 1)C𝑗) ↔ (2↑(𝑁 + 1)) < (((2 · 𝑁) + 1)C𝑁))) |
29 | | 8lt10 12254 |
. . . . 5
⊢ 8 <
;10 |
30 | | eqid 2759 |
. . . . . . 7
⊢ 8 =
8 |
31 | | cu2 13598 |
. . . . . . 7
⊢
(2↑3) = 8 |
32 | 30, 31 | eqtr4i 2785 |
. . . . . 6
⊢ 8 =
(2↑3) |
33 | | 5bc2eq10 39628 |
. . . . . . 7
⊢ (5C2) =
;10 |
34 | 33 | eqcomi 2768 |
. . . . . 6
⊢ ;10 = (5C2) |
35 | 32, 34 | breq12i 5034 |
. . . . 5
⊢ (8 <
;10 ↔ (2↑3) <
(5C2)) |
36 | 29, 35 | mpbi 233 |
. . . 4
⊢
(2↑3) < (5C2) |
37 | | df-3 11723 |
. . . . . 6
⊢ 3 = (2 +
1) |
38 | 37 | oveq2i 7154 |
. . . . 5
⊢
(2↑3) = (2↑(2 + 1)) |
39 | | eqid 2759 |
. . . . . . 7
⊢ 5 =
5 |
40 | | 2t2e4 11823 |
. . . . . . . . 9
⊢ (2
· 2) = 4 |
41 | 40 | oveq1i 7153 |
. . . . . . . 8
⊢ ((2
· 2) + 1) = (4 + 1) |
42 | | 4p1e5 11805 |
. . . . . . . 8
⊢ (4 + 1) =
5 |
43 | 41, 42 | eqtri 2782 |
. . . . . . 7
⊢ ((2
· 2) + 1) = 5 |
44 | 39, 43 | eqtr4i 2785 |
. . . . . 6
⊢ 5 = ((2
· 2) + 1) |
45 | 44 | oveq1i 7153 |
. . . . 5
⊢ (5C2) =
(((2 · 2) + 1)C2) |
46 | 38, 45 | breq12i 5034 |
. . . 4
⊢
((2↑3) < (5C2) ↔ (2↑(2 + 1)) < (((2 · 2) +
1)C2)) |
47 | 36, 46 | mpbi 233 |
. . 3
⊢
(2↑(2 + 1)) < (((2 · 2) + 1)C2) |
48 | 47 | a1i 11 |
. 2
⊢ (𝜑 → (2↑(2 + 1)) < (((2
· 2) + 1)C2)) |
49 | | 2re 11733 |
. . . . 5
⊢ 2 ∈
ℝ |
50 | 49 | a1i 11 |
. . . 4
⊢ ((𝜑 ∧ (2↑(𝑘 + 1)) < (((2 · 𝑘) + 1)C𝑘) ∧ (𝑘 ∈ ℤ ∧ 2 ≤ 𝑘)) → 2 ∈
ℝ) |
51 | | simpl 487 |
. . . . . . . . . . . 12
⊢ ((𝑘 ∈ ℤ ∧ 2 ≤
𝑘) → 𝑘 ∈
ℤ) |
52 | | 0red 10667 |
. . . . . . . . . . . . 13
⊢ ((𝑘 ∈ ℤ ∧ 2 ≤
𝑘) → 0 ∈
ℝ) |
53 | 49 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝑘 ∈ ℤ ∧ 2 ≤
𝑘) → 2 ∈
ℝ) |
54 | 51 | zred 12111 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑘 ∈ ℤ ∧ 2 ≤
𝑘) → 𝑘 ∈
ℝ) |
55 | | 2pos 11762 |
. . . . . . . . . . . . . . . . . . 19
⊢ 0 <
2 |
56 | 55 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑘 ∈ ℤ ∧ 2 ≤
𝑘) → 0 <
2) |
57 | | simpr 489 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑘 ∈ ℤ ∧ 2 ≤
𝑘) → 2 ≤ 𝑘) |
58 | 52, 53, 54, 56, 57 | ltletrd 10823 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑘 ∈ ℤ ∧ 2 ≤
𝑘) → 0 < 𝑘) |
59 | 51, 58 | jca 516 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑘 ∈ ℤ ∧ 2 ≤
𝑘) → (𝑘 ∈ ℤ ∧ 0 <
𝑘)) |
60 | | elnnz 12015 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ ℕ ↔ (𝑘 ∈ ℤ ∧ 0 <
𝑘)) |
61 | 59, 60 | sylibr 237 |
. . . . . . . . . . . . . . 15
⊢ ((𝑘 ∈ ℤ ∧ 2 ≤
𝑘) → 𝑘 ∈
ℕ) |
62 | | nnnn0 11926 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℕ0) |
63 | 61, 62 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝑘 ∈ ℤ ∧ 2 ≤
𝑘) → 𝑘 ∈
ℕ0) |
64 | 63 | nn0red 11980 |
. . . . . . . . . . . . 13
⊢ ((𝑘 ∈ ℤ ∧ 2 ≤
𝑘) → 𝑘 ∈
ℝ) |
65 | 52, 53, 64, 56, 57 | ltletrd 10823 |
. . . . . . . . . . . 12
⊢ ((𝑘 ∈ ℤ ∧ 2 ≤
𝑘) → 0 < 𝑘) |
66 | 51, 65 | jca 516 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈ ℤ ∧ 2 ≤
𝑘) → (𝑘 ∈ ℤ ∧ 0 <
𝑘)) |
67 | 66, 60 | sylibr 237 |
. . . . . . . . . 10
⊢ ((𝑘 ∈ ℤ ∧ 2 ≤
𝑘) → 𝑘 ∈
ℕ) |
68 | 67 | nnred 11674 |
. . . . . . . . 9
⊢ ((𝑘 ∈ ℤ ∧ 2 ≤
𝑘) → 𝑘 ∈
ℝ) |
69 | 68 | 3ad2ant3 1133 |
. . . . . . . 8
⊢ ((𝜑 ∧ (2↑(𝑘 + 1)) < (((2 · 𝑘) + 1)C𝑘) ∧ (𝑘 ∈ ℤ ∧ 2 ≤ 𝑘)) → 𝑘 ∈ ℝ) |
70 | 50, 69 | remulcld 10694 |
. . . . . . 7
⊢ ((𝜑 ∧ (2↑(𝑘 + 1)) < (((2 · 𝑘) + 1)C𝑘) ∧ (𝑘 ∈ ℤ ∧ 2 ≤ 𝑘)) → (2 · 𝑘) ∈
ℝ) |
71 | | 3re 11739 |
. . . . . . . 8
⊢ 3 ∈
ℝ |
72 | 71 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ (2↑(𝑘 + 1)) < (((2 · 𝑘) + 1)C𝑘) ∧ (𝑘 ∈ ℤ ∧ 2 ≤ 𝑘)) → 3 ∈
ℝ) |
73 | 70, 72 | readdcld 10693 |
. . . . . 6
⊢ ((𝜑 ∧ (2↑(𝑘 + 1)) < (((2 · 𝑘) + 1)C𝑘) ∧ (𝑘 ∈ ℤ ∧ 2 ≤ 𝑘)) → ((2 · 𝑘) + 3) ∈
ℝ) |
74 | 69, 50 | readdcld 10693 |
. . . . . 6
⊢ ((𝜑 ∧ (2↑(𝑘 + 1)) < (((2 · 𝑘) + 1)C𝑘) ∧ (𝑘 ∈ ℤ ∧ 2 ≤ 𝑘)) → (𝑘 + 2) ∈ ℝ) |
75 | 68, 53 | readdcld 10693 |
. . . . . . . . . 10
⊢ ((𝑘 ∈ ℤ ∧ 2 ≤
𝑘) → (𝑘 + 2) ∈
ℝ) |
76 | 67 | nngt0d 11708 |
. . . . . . . . . 10
⊢ ((𝑘 ∈ ℤ ∧ 2 ≤
𝑘) → 0 < 𝑘) |
77 | | 2rp 12420 |
. . . . . . . . . . . 12
⊢ 2 ∈
ℝ+ |
78 | 77 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈ ℤ ∧ 2 ≤
𝑘) → 2 ∈
ℝ+) |
79 | 68, 78 | ltaddrpd 12490 |
. . . . . . . . . 10
⊢ ((𝑘 ∈ ℤ ∧ 2 ≤
𝑘) → 𝑘 < (𝑘 + 2)) |
80 | 52, 68, 75, 76, 79 | lttrd 10824 |
. . . . . . . . 9
⊢ ((𝑘 ∈ ℤ ∧ 2 ≤
𝑘) → 0 < (𝑘 + 2)) |
81 | 52, 80 | ltned 10799 |
. . . . . . . 8
⊢ ((𝑘 ∈ ℤ ∧ 2 ≤
𝑘) → 0 ≠ (𝑘 + 2)) |
82 | 81 | necomd 3004 |
. . . . . . 7
⊢ ((𝑘 ∈ ℤ ∧ 2 ≤
𝑘) → (𝑘 + 2) ≠ 0) |
83 | 82 | 3ad2ant3 1133 |
. . . . . 6
⊢ ((𝜑 ∧ (2↑(𝑘 + 1)) < (((2 · 𝑘) + 1)C𝑘) ∧ (𝑘 ∈ ℤ ∧ 2 ≤ 𝑘)) → (𝑘 + 2) ≠ 0) |
84 | 73, 74, 83 | redivcld 11491 |
. . . . 5
⊢ ((𝜑 ∧ (2↑(𝑘 + 1)) < (((2 · 𝑘) + 1)C𝑘) ∧ (𝑘 ∈ ℤ ∧ 2 ≤ 𝑘)) → (((2 · 𝑘) + 3) / (𝑘 + 2)) ∈ ℝ) |
85 | 50, 84 | remulcld 10694 |
. . . 4
⊢ ((𝜑 ∧ (2↑(𝑘 + 1)) < (((2 · 𝑘) + 1)C𝑘) ∧ (𝑘 ∈ ℤ ∧ 2 ≤ 𝑘)) → (2 · (((2
· 𝑘) + 3) / (𝑘 + 2))) ∈
ℝ) |
86 | | 1nn0 11935 |
. . . . . . . 8
⊢ 1 ∈
ℕ0 |
87 | 86 | a1i 11 |
. . . . . . 7
⊢ ((𝑘 ∈ ℤ ∧ 2 ≤
𝑘) → 1 ∈
ℕ0) |
88 | 63, 87 | nn0addcld 11983 |
. . . . . 6
⊢ ((𝑘 ∈ ℤ ∧ 2 ≤
𝑘) → (𝑘 + 1) ∈
ℕ0) |
89 | 53, 88 | reexpcld 13562 |
. . . . 5
⊢ ((𝑘 ∈ ℤ ∧ 2 ≤
𝑘) → (2↑(𝑘 + 1)) ∈
ℝ) |
90 | 89 | 3ad2ant3 1133 |
. . . 4
⊢ ((𝜑 ∧ (2↑(𝑘 + 1)) < (((2 · 𝑘) + 1)C𝑘) ∧ (𝑘 ∈ ℤ ∧ 2 ≤ 𝑘)) → (2↑(𝑘 + 1)) ∈
ℝ) |
91 | | 2nn0 11936 |
. . . . . . . . . 10
⊢ 2 ∈
ℕ0 |
92 | 91 | a1i 11 |
. . . . . . . . 9
⊢ ((𝑘 ∈ ℤ ∧ 2 ≤
𝑘) → 2 ∈
ℕ0) |
93 | 92, 63 | nn0mulcld 11984 |
. . . . . . . 8
⊢ ((𝑘 ∈ ℤ ∧ 2 ≤
𝑘) → (2 · 𝑘) ∈
ℕ0) |
94 | 93, 87 | nn0addcld 11983 |
. . . . . . 7
⊢ ((𝑘 ∈ ℤ ∧ 2 ≤
𝑘) → ((2 ·
𝑘) + 1) ∈
ℕ0) |
95 | | bccl 13717 |
. . . . . . 7
⊢ ((((2
· 𝑘) + 1) ∈
ℕ0 ∧ 𝑘
∈ ℤ) → (((2 · 𝑘) + 1)C𝑘) ∈
ℕ0) |
96 | 94, 51, 95 | syl2anc 588 |
. . . . . 6
⊢ ((𝑘 ∈ ℤ ∧ 2 ≤
𝑘) → (((2 ·
𝑘) + 1)C𝑘) ∈
ℕ0) |
97 | 96 | nn0red 11980 |
. . . . 5
⊢ ((𝑘 ∈ ℤ ∧ 2 ≤
𝑘) → (((2 ·
𝑘) + 1)C𝑘) ∈ ℝ) |
98 | 97 | 3ad2ant3 1133 |
. . . 4
⊢ ((𝜑 ∧ (2↑(𝑘 + 1)) < (((2 · 𝑘) + 1)C𝑘) ∧ (𝑘 ∈ ℤ ∧ 2 ≤ 𝑘)) → (((2 · 𝑘) + 1)C𝑘) ∈ ℝ) |
99 | | 0le2 11761 |
. . . . 5
⊢ 0 ≤
2 |
100 | 99 | a1i 11 |
. . . 4
⊢ ((𝜑 ∧ (2↑(𝑘 + 1)) < (((2 · 𝑘) + 1)C𝑘) ∧ (𝑘 ∈ ℤ ∧ 2 ≤ 𝑘)) → 0 ≤
2) |
101 | | eqid 2759 |
. . . . . . . 8
⊢ 2 =
2 |
102 | | 2t1e2 11822 |
. . . . . . . 8
⊢ (2
· 1) = 2 |
103 | 101, 102 | eqtr4i 2785 |
. . . . . . 7
⊢ 2 = (2
· 1) |
104 | 103 | a1i 11 |
. . . . . 6
⊢ ((𝑘 ∈ ℤ ∧ 2 ≤
𝑘) → 2 = (2 ·
1)) |
105 | | 1red 10665 |
. . . . . . 7
⊢ ((𝑘 ∈ ℤ ∧ 2 ≤
𝑘) → 1 ∈
ℝ) |
106 | 53, 68 | remulcld 10694 |
. . . . . . . . 9
⊢ ((𝑘 ∈ ℤ ∧ 2 ≤
𝑘) → (2 · 𝑘) ∈
ℝ) |
107 | 71 | a1i 11 |
. . . . . . . . 9
⊢ ((𝑘 ∈ ℤ ∧ 2 ≤
𝑘) → 3 ∈
ℝ) |
108 | 106, 107 | readdcld 10693 |
. . . . . . . 8
⊢ ((𝑘 ∈ ℤ ∧ 2 ≤
𝑘) → ((2 ·
𝑘) + 3) ∈
ℝ) |
109 | 108, 75, 82 | redivcld 11491 |
. . . . . . 7
⊢ ((𝑘 ∈ ℤ ∧ 2 ≤
𝑘) → (((2 ·
𝑘) + 3) / (𝑘 + 2)) ∈
ℝ) |
110 | | nnrp 12426 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℝ+) |
111 | 77 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ ℕ → 2 ∈
ℝ+) |
112 | 110, 111 | rpaddcld 12472 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ ℕ → (𝑘 + 2) ∈
ℝ+) |
113 | 112 | rpcnd 12459 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ → (𝑘 + 2) ∈
ℂ) |
114 | 113 | mulid1d 10681 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℕ → ((𝑘 + 2) · 1) = (𝑘 + 2)) |
115 | | nnre 11666 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℝ) |
116 | 49 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ → 2 ∈
ℝ) |
117 | 116, 115 | remulcld 10694 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ → (2
· 𝑘) ∈
ℝ) |
118 | 71 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ → 3 ∈
ℝ) |
119 | 110 | rpge0d 12461 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ ℕ → 0 ≤
𝑘) |
120 | | 1le2 11868 |
. . . . . . . . . . . . 13
⊢ 1 ≤
2 |
121 | 120 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ ℕ → 1 ≤
2) |
122 | 115, 116,
119, 121 | lemulge12d 11601 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ → 𝑘 ≤ (2 · 𝑘)) |
123 | | 2lt3 11831 |
. . . . . . . . . . . 12
⊢ 2 <
3 |
124 | 123 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ → 2 <
3) |
125 | 115, 116,
117, 118, 122, 124 | leltaddd 11285 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℕ → (𝑘 + 2) < ((2 · 𝑘) + 3)) |
126 | 114, 125 | eqbrtrd 5047 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℕ → ((𝑘 + 2) · 1) < ((2
· 𝑘) +
3)) |
127 | | 1red 10665 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℕ → 1 ∈
ℝ) |
128 | 117, 118 | readdcld 10693 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℕ → ((2
· 𝑘) + 3) ∈
ℝ) |
129 | 127, 128,
112 | ltmuldiv2d 12505 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℕ → (((𝑘 + 2) · 1) < ((2
· 𝑘) + 3) ↔ 1
< (((2 · 𝑘) + 3)
/ (𝑘 +
2)))) |
130 | 126, 129 | mpbid 235 |
. . . . . . . 8
⊢ (𝑘 ∈ ℕ → 1 <
(((2 · 𝑘) + 3) /
(𝑘 + 2))) |
131 | 67, 130 | syl 17 |
. . . . . . 7
⊢ ((𝑘 ∈ ℤ ∧ 2 ≤
𝑘) → 1 < (((2
· 𝑘) + 3) / (𝑘 + 2))) |
132 | 105, 109,
78, 131 | ltmul2dd 12513 |
. . . . . 6
⊢ ((𝑘 ∈ ℤ ∧ 2 ≤
𝑘) → (2 · 1)
< (2 · (((2 · 𝑘) + 3) / (𝑘 + 2)))) |
133 | 104, 132 | eqbrtrd 5047 |
. . . . 5
⊢ ((𝑘 ∈ ℤ ∧ 2 ≤
𝑘) → 2 < (2
· (((2 · 𝑘) +
3) / (𝑘 +
2)))) |
134 | 133 | 3ad2ant3 1133 |
. . . 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 13563 |
. . . . 5
⊢ ((𝑘 ∈ ℤ ∧ 2 ≤
𝑘) → 0 ≤
(2↑(𝑘 +
1))) |
137 | 136 | 3ad2ant3 1133 |
. . . 4
⊢ ((𝜑 ∧ (2↑(𝑘 + 1)) < (((2 · 𝑘) + 1)C𝑘) ∧ (𝑘 ∈ ℤ ∧ 2 ≤ 𝑘)) → 0 ≤ (2↑(𝑘 + 1))) |
138 | | simp2 1135 |
. . . 4
⊢ ((𝜑 ∧ (2↑(𝑘 + 1)) < (((2 · 𝑘) + 1)C𝑘) ∧ (𝑘 ∈ ℤ ∧ 2 ≤ 𝑘)) → (2↑(𝑘 + 1)) < (((2 · 𝑘) + 1)C𝑘)) |
139 | 50, 85, 90, 98, 100, 134, 137, 138 | ltmul12ad 11604 |
. . 3
⊢ ((𝜑 ∧ (2↑(𝑘 + 1)) < (((2 · 𝑘) + 1)C𝑘) ∧ (𝑘 ∈ ℤ ∧ 2 ≤ 𝑘)) → (2 ·
(2↑(𝑘 + 1))) < ((2
· (((2 · 𝑘) +
3) / (𝑘 + 2))) ·
(((2 · 𝑘) + 1)C𝑘))) |
140 | | 2cnd 11737 |
. . . . . . . 8
⊢ ((𝑘 ∈ ℤ ∧ 2 ≤
𝑘) → 2 ∈
ℂ) |
141 | 140, 87, 88 | expaddd 13547 |
. . . . . . 7
⊢ ((𝑘 ∈ ℤ ∧ 2 ≤
𝑘) → (2↑((𝑘 + 1) + 1)) = ((2↑(𝑘 + 1)) ·
(2↑1))) |
142 | 140, 88 | expcld 13545 |
. . . . . . . . 9
⊢ ((𝑘 ∈ ℤ ∧ 2 ≤
𝑘) → (2↑(𝑘 + 1)) ∈
ℂ) |
143 | 140, 87 | expcld 13545 |
. . . . . . . . 9
⊢ ((𝑘 ∈ ℤ ∧ 2 ≤
𝑘) → (2↑1) ∈
ℂ) |
144 | 142, 143 | mulcomd 10685 |
. . . . . . . 8
⊢ ((𝑘 ∈ ℤ ∧ 2 ≤
𝑘) → ((2↑(𝑘 + 1)) · (2↑1)) =
((2↑1) · (2↑(𝑘 + 1)))) |
145 | 140 | exp1d 13540 |
. . . . . . . . 9
⊢ ((𝑘 ∈ ℤ ∧ 2 ≤
𝑘) → (2↑1) =
2) |
146 | 145 | oveq1d 7158 |
. . . . . . . 8
⊢ ((𝑘 ∈ ℤ ∧ 2 ≤
𝑘) → ((2↑1)
· (2↑(𝑘 + 1)))
= (2 · (2↑(𝑘 +
1)))) |
147 | | eqidd 2760 |
. . . . . . . 8
⊢ ((𝑘 ∈ ℤ ∧ 2 ≤
𝑘) → (2 ·
(2↑(𝑘 + 1))) = (2
· (2↑(𝑘 +
1)))) |
148 | 144, 146,
147 | 3eqtrd 2798 |
. . . . . . 7
⊢ ((𝑘 ∈ ℤ ∧ 2 ≤
𝑘) → ((2↑(𝑘 + 1)) · (2↑1)) = (2
· (2↑(𝑘 +
1)))) |
149 | 141, 148 | eqtrd 2794 |
. . . . . 6
⊢ ((𝑘 ∈ ℤ ∧ 2 ≤
𝑘) → (2↑((𝑘 + 1) + 1)) = (2 ·
(2↑(𝑘 +
1)))) |
150 | 149 | eqcomd 2765 |
. . . . 5
⊢ ((𝑘 ∈ ℤ ∧ 2 ≤
𝑘) → (2 ·
(2↑(𝑘 + 1))) =
(2↑((𝑘 + 1) +
1))) |
151 | 150 | 3ad2ant3 1133 |
. . . 4
⊢ ((𝜑 ∧ (2↑(𝑘 + 1)) < (((2 · 𝑘) + 1)C𝑘) ∧ (𝑘 ∈ ℤ ∧ 2 ≤ 𝑘)) → (2 ·
(2↑(𝑘 + 1))) =
(2↑((𝑘 + 1) +
1))) |
152 | 63 | 2np3bcnp1 39630 |
. . . . . . 7
⊢ ((𝑘 ∈ ℤ ∧ 2 ≤
𝑘) → (((2 ·
(𝑘 + 1)) + 1)C(𝑘 + 1)) = ((((2 · 𝑘) + 1)C𝑘) · (2 · (((2 · 𝑘) + 3) / (𝑘 + 2))))) |
153 | 96 | nn0cnd 11981 |
. . . . . . . 8
⊢ ((𝑘 ∈ ℤ ∧ 2 ≤
𝑘) → (((2 ·
𝑘) + 1)C𝑘) ∈ ℂ) |
154 | 67 | nncnd 11675 |
. . . . . . . . . . . 12
⊢ ((𝑘 ∈ ℤ ∧ 2 ≤
𝑘) → 𝑘 ∈
ℂ) |
155 | 140, 154 | mulcld 10684 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈ ℤ ∧ 2 ≤
𝑘) → (2 · 𝑘) ∈
ℂ) |
156 | | 3cn 11740 |
. . . . . . . . . . . 12
⊢ 3 ∈
ℂ |
157 | 156 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈ ℤ ∧ 2 ≤
𝑘) → 3 ∈
ℂ) |
158 | 155, 157 | addcld 10683 |
. . . . . . . . . 10
⊢ ((𝑘 ∈ ℤ ∧ 2 ≤
𝑘) → ((2 ·
𝑘) + 3) ∈
ℂ) |
159 | 154, 140 | addcld 10683 |
. . . . . . . . . 10
⊢ ((𝑘 ∈ ℤ ∧ 2 ≤
𝑘) → (𝑘 + 2) ∈
ℂ) |
160 | 158, 159,
82 | divcld 11439 |
. . . . . . . . 9
⊢ ((𝑘 ∈ ℤ ∧ 2 ≤
𝑘) → (((2 ·
𝑘) + 3) / (𝑘 + 2)) ∈
ℂ) |
161 | 140, 160 | mulcld 10684 |
. . . . . . . 8
⊢ ((𝑘 ∈ ℤ ∧ 2 ≤
𝑘) → (2 · (((2
· 𝑘) + 3) / (𝑘 + 2))) ∈
ℂ) |
162 | 153, 161 | mulcomd 10685 |
. . . . . . 7
⊢ ((𝑘 ∈ ℤ ∧ 2 ≤
𝑘) → ((((2 ·
𝑘) + 1)C𝑘) · (2 · (((2 · 𝑘) + 3) / (𝑘 + 2)))) = ((2 · (((2 · 𝑘) + 3) / (𝑘 + 2))) · (((2 · 𝑘) + 1)C𝑘))) |
163 | 152, 162 | eqtrd 2794 |
. . . . . 6
⊢ ((𝑘 ∈ ℤ ∧ 2 ≤
𝑘) → (((2 ·
(𝑘 + 1)) + 1)C(𝑘 + 1)) = ((2 · (((2
· 𝑘) + 3) / (𝑘 + 2))) · (((2 ·
𝑘) + 1)C𝑘))) |
164 | 163 | eqcomd 2765 |
. . . . 5
⊢ ((𝑘 ∈ ℤ ∧ 2 ≤
𝑘) → ((2 · (((2
· 𝑘) + 3) / (𝑘 + 2))) · (((2 ·
𝑘) + 1)C𝑘)) = (((2 · (𝑘 + 1)) + 1)C(𝑘 + 1))) |
165 | 164 | 3ad2ant3 1133 |
. . . 4
⊢ ((𝜑 ∧ (2↑(𝑘 + 1)) < (((2 · 𝑘) + 1)C𝑘) ∧ (𝑘 ∈ ℤ ∧ 2 ≤ 𝑘)) → ((2 · (((2
· 𝑘) + 3) / (𝑘 + 2))) · (((2 ·
𝑘) + 1)C𝑘)) = (((2 · (𝑘 + 1)) + 1)C(𝑘 + 1))) |
166 | 151, 165 | breq12d 5038 |
. . 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 235 |
. 2
⊢ ((𝜑 ∧ (2↑(𝑘 + 1)) < (((2 · 𝑘) + 1)C𝑘) ∧ (𝑘 ∈ ℤ ∧ 2 ≤ 𝑘)) → (2↑((𝑘 + 1) + 1)) < (((2 ·
(𝑘 + 1)) + 1)C(𝑘 + 1))) |
168 | | 2z 12038 |
. . 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 39529 |
1
⊢ (𝜑 → (2↑(𝑁 + 1)) < (((2 · 𝑁) + 1)C𝑁)) |