Step | Hyp | Ref
| Expression |
1 | | fveq2 6191 |
. . . . 5
⊢ (𝑥 = 1 → (seq1( + , 𝐺)‘𝑥) = (seq1( + , 𝐺)‘1)) |
2 | | oveq2 6658 |
. . . . . . . 8
⊢ (𝑥 = 1 → (2↑𝑥) = (2↑1)) |
3 | | 2cn 11091 |
. . . . . . . . 9
⊢ 2 ∈
ℂ |
4 | | exp1 12866 |
. . . . . . . . 9
⊢ (2 ∈
ℂ → (2↑1) = 2) |
5 | 3, 4 | ax-mp 5 |
. . . . . . . 8
⊢
(2↑1) = 2 |
6 | 2, 5 | syl6eq 2672 |
. . . . . . 7
⊢ (𝑥 = 1 → (2↑𝑥) = 2) |
7 | 6 | fveq2d 6195 |
. . . . . 6
⊢ (𝑥 = 1 → (seq1( + , 𝐹)‘(2↑𝑥)) = (seq1( + , 𝐹)‘2)) |
8 | 7 | oveq2d 6666 |
. . . . 5
⊢ (𝑥 = 1 → (2 · (seq1( +
, 𝐹)‘(2↑𝑥))) = (2 · (seq1( + ,
𝐹)‘2))) |
9 | 1, 8 | breq12d 4666 |
. . . 4
⊢ (𝑥 = 1 → ((seq1( + , 𝐺)‘𝑥) ≤ (2 · (seq1( + , 𝐹)‘(2↑𝑥))) ↔ (seq1( + , 𝐺)‘1) ≤ (2 ·
(seq1( + , 𝐹)‘2)))) |
10 | 9 | imbi2d 330 |
. . 3
⊢ (𝑥 = 1 → ((𝜑 → (seq1( + , 𝐺)‘𝑥) ≤ (2 · (seq1( + , 𝐹)‘(2↑𝑥)))) ↔ (𝜑 → (seq1( + , 𝐺)‘1) ≤ (2 · (seq1( + , 𝐹)‘2))))) |
11 | | fveq2 6191 |
. . . . 5
⊢ (𝑥 = 𝑗 → (seq1( + , 𝐺)‘𝑥) = (seq1( + , 𝐺)‘𝑗)) |
12 | | oveq2 6658 |
. . . . . . 7
⊢ (𝑥 = 𝑗 → (2↑𝑥) = (2↑𝑗)) |
13 | 12 | fveq2d 6195 |
. . . . . 6
⊢ (𝑥 = 𝑗 → (seq1( + , 𝐹)‘(2↑𝑥)) = (seq1( + , 𝐹)‘(2↑𝑗))) |
14 | 13 | oveq2d 6666 |
. . . . 5
⊢ (𝑥 = 𝑗 → (2 · (seq1( + , 𝐹)‘(2↑𝑥))) = (2 · (seq1( + ,
𝐹)‘(2↑𝑗)))) |
15 | 11, 14 | breq12d 4666 |
. . . 4
⊢ (𝑥 = 𝑗 → ((seq1( + , 𝐺)‘𝑥) ≤ (2 · (seq1( + , 𝐹)‘(2↑𝑥))) ↔ (seq1( + , 𝐺)‘𝑗) ≤ (2 · (seq1( + , 𝐹)‘(2↑𝑗))))) |
16 | 15 | imbi2d 330 |
. . 3
⊢ (𝑥 = 𝑗 → ((𝜑 → (seq1( + , 𝐺)‘𝑥) ≤ (2 · (seq1( + , 𝐹)‘(2↑𝑥)))) ↔ (𝜑 → (seq1( + , 𝐺)‘𝑗) ≤ (2 · (seq1( + , 𝐹)‘(2↑𝑗)))))) |
17 | | fveq2 6191 |
. . . . 5
⊢ (𝑥 = (𝑗 + 1) → (seq1( + , 𝐺)‘𝑥) = (seq1( + , 𝐺)‘(𝑗 + 1))) |
18 | | oveq2 6658 |
. . . . . . 7
⊢ (𝑥 = (𝑗 + 1) → (2↑𝑥) = (2↑(𝑗 + 1))) |
19 | 18 | fveq2d 6195 |
. . . . . 6
⊢ (𝑥 = (𝑗 + 1) → (seq1( + , 𝐹)‘(2↑𝑥)) = (seq1( + , 𝐹)‘(2↑(𝑗 + 1)))) |
20 | 19 | oveq2d 6666 |
. . . . 5
⊢ (𝑥 = (𝑗 + 1) → (2 · (seq1( + , 𝐹)‘(2↑𝑥))) = (2 · (seq1( + ,
𝐹)‘(2↑(𝑗 + 1))))) |
21 | 17, 20 | breq12d 4666 |
. . . 4
⊢ (𝑥 = (𝑗 + 1) → ((seq1( + , 𝐺)‘𝑥) ≤ (2 · (seq1( + , 𝐹)‘(2↑𝑥))) ↔ (seq1( + , 𝐺)‘(𝑗 + 1)) ≤ (2 · (seq1( + , 𝐹)‘(2↑(𝑗 + 1)))))) |
22 | 21 | imbi2d 330 |
. . 3
⊢ (𝑥 = (𝑗 + 1) → ((𝜑 → (seq1( + , 𝐺)‘𝑥) ≤ (2 · (seq1( + , 𝐹)‘(2↑𝑥)))) ↔ (𝜑 → (seq1( + , 𝐺)‘(𝑗 + 1)) ≤ (2 · (seq1( + , 𝐹)‘(2↑(𝑗 + 1))))))) |
23 | | fveq2 6191 |
. . . . 5
⊢ (𝑥 = 𝑁 → (seq1( + , 𝐺)‘𝑥) = (seq1( + , 𝐺)‘𝑁)) |
24 | | oveq2 6658 |
. . . . . . 7
⊢ (𝑥 = 𝑁 → (2↑𝑥) = (2↑𝑁)) |
25 | 24 | fveq2d 6195 |
. . . . . 6
⊢ (𝑥 = 𝑁 → (seq1( + , 𝐹)‘(2↑𝑥)) = (seq1( + , 𝐹)‘(2↑𝑁))) |
26 | 25 | oveq2d 6666 |
. . . . 5
⊢ (𝑥 = 𝑁 → (2 · (seq1( + , 𝐹)‘(2↑𝑥))) = (2 · (seq1( + ,
𝐹)‘(2↑𝑁)))) |
27 | 23, 26 | breq12d 4666 |
. . . 4
⊢ (𝑥 = 𝑁 → ((seq1( + , 𝐺)‘𝑥) ≤ (2 · (seq1( + , 𝐹)‘(2↑𝑥))) ↔ (seq1( + , 𝐺)‘𝑁) ≤ (2 · (seq1( + , 𝐹)‘(2↑𝑁))))) |
28 | 27 | imbi2d 330 |
. . 3
⊢ (𝑥 = 𝑁 → ((𝜑 → (seq1( + , 𝐺)‘𝑥) ≤ (2 · (seq1( + , 𝐹)‘(2↑𝑥)))) ↔ (𝜑 → (seq1( + , 𝐺)‘𝑁) ≤ (2 · (seq1( + , 𝐹)‘(2↑𝑁)))))) |
29 | | 1nn 11031 |
. . . . . . 7
⊢ 1 ∈
ℕ |
30 | | climcnds.2 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 0 ≤ (𝐹‘𝑘)) |
31 | 30 | ralrimiva 2966 |
. . . . . . 7
⊢ (𝜑 → ∀𝑘 ∈ ℕ 0 ≤ (𝐹‘𝑘)) |
32 | | fveq2 6191 |
. . . . . . . . 9
⊢ (𝑘 = 1 → (𝐹‘𝑘) = (𝐹‘1)) |
33 | 32 | breq2d 4665 |
. . . . . . . 8
⊢ (𝑘 = 1 → (0 ≤ (𝐹‘𝑘) ↔ 0 ≤ (𝐹‘1))) |
34 | 33 | rspcv 3305 |
. . . . . . 7
⊢ (1 ∈
ℕ → (∀𝑘
∈ ℕ 0 ≤ (𝐹‘𝑘) → 0 ≤ (𝐹‘1))) |
35 | 29, 31, 34 | mpsyl 68 |
. . . . . 6
⊢ (𝜑 → 0 ≤ (𝐹‘1)) |
36 | | 2nn 11185 |
. . . . . . . 8
⊢ 2 ∈
ℕ |
37 | | climcnds.1 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) ∈ ℝ) |
38 | 37 | ralrimiva 2966 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑘 ∈ ℕ (𝐹‘𝑘) ∈ ℝ) |
39 | | fveq2 6191 |
. . . . . . . . . 10
⊢ (𝑘 = 2 → (𝐹‘𝑘) = (𝐹‘2)) |
40 | 39 | eleq1d 2686 |
. . . . . . . . 9
⊢ (𝑘 = 2 → ((𝐹‘𝑘) ∈ ℝ ↔ (𝐹‘2) ∈ ℝ)) |
41 | 40 | rspcv 3305 |
. . . . . . . 8
⊢ (2 ∈
ℕ → (∀𝑘
∈ ℕ (𝐹‘𝑘) ∈ ℝ → (𝐹‘2) ∈ ℝ)) |
42 | 36, 38, 41 | mpsyl 68 |
. . . . . . 7
⊢ (𝜑 → (𝐹‘2) ∈ ℝ) |
43 | 32 | eleq1d 2686 |
. . . . . . . . 9
⊢ (𝑘 = 1 → ((𝐹‘𝑘) ∈ ℝ ↔ (𝐹‘1) ∈ ℝ)) |
44 | 43 | rspcv 3305 |
. . . . . . . 8
⊢ (1 ∈
ℕ → (∀𝑘
∈ ℕ (𝐹‘𝑘) ∈ ℝ → (𝐹‘1) ∈ ℝ)) |
45 | 29, 38, 44 | mpsyl 68 |
. . . . . . 7
⊢ (𝜑 → (𝐹‘1) ∈ ℝ) |
46 | 42, 45 | addge02d 10616 |
. . . . . 6
⊢ (𝜑 → (0 ≤ (𝐹‘1) ↔ (𝐹‘2) ≤ ((𝐹‘1) + (𝐹‘2)))) |
47 | 35, 46 | mpbid 222 |
. . . . 5
⊢ (𝜑 → (𝐹‘2) ≤ ((𝐹‘1) + (𝐹‘2))) |
48 | 45, 42 | readdcld 10069 |
. . . . . 6
⊢ (𝜑 → ((𝐹‘1) + (𝐹‘2)) ∈ ℝ) |
49 | | 2re 11090 |
. . . . . . . 8
⊢ 2 ∈
ℝ |
50 | | 2pos 11112 |
. . . . . . . 8
⊢ 0 <
2 |
51 | 49, 50 | pm3.2i 471 |
. . . . . . 7
⊢ (2 ∈
ℝ ∧ 0 < 2) |
52 | 51 | a1i 11 |
. . . . . 6
⊢ (𝜑 → (2 ∈ ℝ ∧ 0
< 2)) |
53 | | lemul2 10876 |
. . . . . 6
⊢ (((𝐹‘2) ∈ ℝ ∧
((𝐹‘1) + (𝐹‘2)) ∈ ℝ ∧
(2 ∈ ℝ ∧ 0 < 2)) → ((𝐹‘2) ≤ ((𝐹‘1) + (𝐹‘2)) ↔ (2 · (𝐹‘2)) ≤ (2 ·
((𝐹‘1) + (𝐹‘2))))) |
54 | 42, 48, 52, 53 | syl3anc 1326 |
. . . . 5
⊢ (𝜑 → ((𝐹‘2) ≤ ((𝐹‘1) + (𝐹‘2)) ↔ (2 · (𝐹‘2)) ≤ (2 ·
((𝐹‘1) + (𝐹‘2))))) |
55 | 47, 54 | mpbid 222 |
. . . 4
⊢ (𝜑 → (2 · (𝐹‘2)) ≤ (2 ·
((𝐹‘1) + (𝐹‘2)))) |
56 | | 1z 11407 |
. . . . 5
⊢ 1 ∈
ℤ |
57 | | 1nn0 11308 |
. . . . . 6
⊢ 1 ∈
ℕ0 |
58 | | climcnds.4 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → (𝐺‘𝑛) = ((2↑𝑛) · (𝐹‘(2↑𝑛)))) |
59 | 58 | ralrimiva 2966 |
. . . . . 6
⊢ (𝜑 → ∀𝑛 ∈ ℕ0 (𝐺‘𝑛) = ((2↑𝑛) · (𝐹‘(2↑𝑛)))) |
60 | | fveq2 6191 |
. . . . . . . 8
⊢ (𝑛 = 1 → (𝐺‘𝑛) = (𝐺‘1)) |
61 | | oveq2 6658 |
. . . . . . . . . 10
⊢ (𝑛 = 1 → (2↑𝑛) = (2↑1)) |
62 | 61, 5 | syl6eq 2672 |
. . . . . . . . 9
⊢ (𝑛 = 1 → (2↑𝑛) = 2) |
63 | 62 | fveq2d 6195 |
. . . . . . . . 9
⊢ (𝑛 = 1 → (𝐹‘(2↑𝑛)) = (𝐹‘2)) |
64 | 62, 63 | oveq12d 6668 |
. . . . . . . 8
⊢ (𝑛 = 1 → ((2↑𝑛) · (𝐹‘(2↑𝑛))) = (2 · (𝐹‘2))) |
65 | 60, 64 | eqeq12d 2637 |
. . . . . . 7
⊢ (𝑛 = 1 → ((𝐺‘𝑛) = ((2↑𝑛) · (𝐹‘(2↑𝑛))) ↔ (𝐺‘1) = (2 · (𝐹‘2)))) |
66 | 65 | rspcv 3305 |
. . . . . 6
⊢ (1 ∈
ℕ0 → (∀𝑛 ∈ ℕ0 (𝐺‘𝑛) = ((2↑𝑛) · (𝐹‘(2↑𝑛))) → (𝐺‘1) = (2 · (𝐹‘2)))) |
67 | 57, 59, 66 | mpsyl 68 |
. . . . 5
⊢ (𝜑 → (𝐺‘1) = (2 · (𝐹‘2))) |
68 | 56, 67 | seq1i 12815 |
. . . 4
⊢ (𝜑 → (seq1( + , 𝐺)‘1) = (2 · (𝐹‘2))) |
69 | | nnuz 11723 |
. . . . . 6
⊢ ℕ =
(ℤ≥‘1) |
70 | | df-2 11079 |
. . . . . 6
⊢ 2 = (1 +
1) |
71 | | eqidd 2623 |
. . . . . . 7
⊢ (𝜑 → (𝐹‘1) = (𝐹‘1)) |
72 | 56, 71 | seq1i 12815 |
. . . . . 6
⊢ (𝜑 → (seq1( + , 𝐹)‘1) = (𝐹‘1)) |
73 | | eqidd 2623 |
. . . . . 6
⊢ (𝜑 → (𝐹‘2) = (𝐹‘2)) |
74 | 69, 29, 70, 72, 73 | seqp1i 12817 |
. . . . 5
⊢ (𝜑 → (seq1( + , 𝐹)‘2) = ((𝐹‘1) + (𝐹‘2))) |
75 | 74 | oveq2d 6666 |
. . . 4
⊢ (𝜑 → (2 · (seq1( + ,
𝐹)‘2)) = (2 ·
((𝐹‘1) + (𝐹‘2)))) |
76 | 55, 68, 75 | 3brtr4d 4685 |
. . 3
⊢ (𝜑 → (seq1( + , 𝐺)‘1) ≤ (2 ·
(seq1( + , 𝐹)‘2))) |
77 | | peano2nn 11032 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈ ℕ → (𝑗 + 1) ∈
ℕ) |
78 | 77 | adantl 482 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑗 + 1) ∈ ℕ) |
79 | 78 | nnnn0d 11351 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑗 + 1) ∈
ℕ0) |
80 | 59 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ∀𝑛 ∈ ℕ0
(𝐺‘𝑛) = ((2↑𝑛) · (𝐹‘(2↑𝑛)))) |
81 | | fveq2 6191 |
. . . . . . . . . . . 12
⊢ (𝑛 = (𝑗 + 1) → (𝐺‘𝑛) = (𝐺‘(𝑗 + 1))) |
82 | | oveq2 6658 |
. . . . . . . . . . . . 13
⊢ (𝑛 = (𝑗 + 1) → (2↑𝑛) = (2↑(𝑗 + 1))) |
83 | 82 | fveq2d 6195 |
. . . . . . . . . . . . 13
⊢ (𝑛 = (𝑗 + 1) → (𝐹‘(2↑𝑛)) = (𝐹‘(2↑(𝑗 + 1)))) |
84 | 82, 83 | oveq12d 6668 |
. . . . . . . . . . . 12
⊢ (𝑛 = (𝑗 + 1) → ((2↑𝑛) · (𝐹‘(2↑𝑛))) = ((2↑(𝑗 + 1)) · (𝐹‘(2↑(𝑗 + 1))))) |
85 | 81, 84 | eqeq12d 2637 |
. . . . . . . . . . 11
⊢ (𝑛 = (𝑗 + 1) → ((𝐺‘𝑛) = ((2↑𝑛) · (𝐹‘(2↑𝑛))) ↔ (𝐺‘(𝑗 + 1)) = ((2↑(𝑗 + 1)) · (𝐹‘(2↑(𝑗 + 1)))))) |
86 | 85 | rspcv 3305 |
. . . . . . . . . 10
⊢ ((𝑗 + 1) ∈ ℕ0
→ (∀𝑛 ∈
ℕ0 (𝐺‘𝑛) = ((2↑𝑛) · (𝐹‘(2↑𝑛))) → (𝐺‘(𝑗 + 1)) = ((2↑(𝑗 + 1)) · (𝐹‘(2↑(𝑗 + 1)))))) |
87 | 79, 80, 86 | sylc 65 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐺‘(𝑗 + 1)) = ((2↑(𝑗 + 1)) · (𝐹‘(2↑(𝑗 + 1))))) |
88 | | nnnn0 11299 |
. . . . . . . . . . . . 13
⊢ (𝑗 ∈ ℕ → 𝑗 ∈
ℕ0) |
89 | 88 | adantl 482 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ ℕ0) |
90 | | expp1 12867 |
. . . . . . . . . . . 12
⊢ ((2
∈ ℂ ∧ 𝑗
∈ ℕ0) → (2↑(𝑗 + 1)) = ((2↑𝑗) · 2)) |
91 | 3, 89, 90 | sylancr 695 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (2↑(𝑗 + 1)) = ((2↑𝑗) · 2)) |
92 | | nnexpcl 12873 |
. . . . . . . . . . . . . . 15
⊢ ((2
∈ ℕ ∧ 𝑗
∈ ℕ0) → (2↑𝑗) ∈ ℕ) |
93 | 36, 88, 92 | sylancr 695 |
. . . . . . . . . . . . . 14
⊢ (𝑗 ∈ ℕ →
(2↑𝑗) ∈
ℕ) |
94 | 93 | adantl 482 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (2↑𝑗) ∈
ℕ) |
95 | 94 | nncnd 11036 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (2↑𝑗) ∈
ℂ) |
96 | | mulcom 10022 |
. . . . . . . . . . . 12
⊢
(((2↑𝑗) ∈
ℂ ∧ 2 ∈ ℂ) → ((2↑𝑗) · 2) = (2 · (2↑𝑗))) |
97 | 95, 3, 96 | sylancl 694 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((2↑𝑗) · 2) = (2 ·
(2↑𝑗))) |
98 | 91, 97 | eqtrd 2656 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (2↑(𝑗 + 1)) = (2 ·
(2↑𝑗))) |
99 | 98 | oveq1d 6665 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((2↑(𝑗 + 1)) · (𝐹‘(2↑(𝑗 + 1)))) = ((2 ·
(2↑𝑗)) · (𝐹‘(2↑(𝑗 + 1))))) |
100 | 3 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 2 ∈
ℂ) |
101 | | nnexpcl 12873 |
. . . . . . . . . . . . 13
⊢ ((2
∈ ℕ ∧ (𝑗 +
1) ∈ ℕ0) → (2↑(𝑗 + 1)) ∈ ℕ) |
102 | 36, 79, 101 | sylancr 695 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (2↑(𝑗 + 1)) ∈
ℕ) |
103 | 38 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ∀𝑘 ∈ ℕ (𝐹‘𝑘) ∈ ℝ) |
104 | | fveq2 6191 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = (2↑(𝑗 + 1)) → (𝐹‘𝑘) = (𝐹‘(2↑(𝑗 + 1)))) |
105 | 104 | eleq1d 2686 |
. . . . . . . . . . . . 13
⊢ (𝑘 = (2↑(𝑗 + 1)) → ((𝐹‘𝑘) ∈ ℝ ↔ (𝐹‘(2↑(𝑗 + 1))) ∈ ℝ)) |
106 | 105 | rspcv 3305 |
. . . . . . . . . . . 12
⊢
((2↑(𝑗 + 1))
∈ ℕ → (∀𝑘 ∈ ℕ (𝐹‘𝑘) ∈ ℝ → (𝐹‘(2↑(𝑗 + 1))) ∈ ℝ)) |
107 | 102, 103,
106 | sylc 65 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐹‘(2↑(𝑗 + 1))) ∈ ℝ) |
108 | 107 | recnd 10068 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐹‘(2↑(𝑗 + 1))) ∈ ℂ) |
109 | 100, 95, 108 | mulassd 10063 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((2 ·
(2↑𝑗)) · (𝐹‘(2↑(𝑗 + 1)))) = (2 ·
((2↑𝑗) · (𝐹‘(2↑(𝑗 + 1)))))) |
110 | 87, 99, 109 | 3eqtrd 2660 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐺‘(𝑗 + 1)) = (2 · ((2↑𝑗) · (𝐹‘(2↑(𝑗 + 1)))))) |
111 | 94 | nnnn0d 11351 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (2↑𝑗) ∈
ℕ0) |
112 | | hashfz1 13134 |
. . . . . . . . . . . . . . 15
⊢
((2↑𝑗) ∈
ℕ0 → (#‘(1...(2↑𝑗))) = (2↑𝑗)) |
113 | 111, 112 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) →
(#‘(1...(2↑𝑗)))
= (2↑𝑗)) |
114 | 113, 95 | eqeltrd 2701 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) →
(#‘(1...(2↑𝑗)))
∈ ℂ) |
115 | | fzfid 12772 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (((2↑𝑗) + 1)...(2↑(𝑗 + 1))) ∈
Fin) |
116 | | hashcl 13147 |
. . . . . . . . . . . . . . 15
⊢
((((2↑𝑗) +
1)...(2↑(𝑗 + 1)))
∈ Fin → (#‘(((2↑𝑗) + 1)...(2↑(𝑗 + 1)))) ∈
ℕ0) |
117 | 115, 116 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) →
(#‘(((2↑𝑗) +
1)...(2↑(𝑗 + 1))))
∈ ℕ0) |
118 | 117 | nn0cnd 11353 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) →
(#‘(((2↑𝑗) +
1)...(2↑(𝑗 + 1))))
∈ ℂ) |
119 | | simpr 477 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ ℕ) |
120 | 119 | nnzd 11481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ ℤ) |
121 | | uzid 11702 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 ∈ ℤ → 𝑗 ∈
(ℤ≥‘𝑗)) |
122 | | peano2uz 11741 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 ∈
(ℤ≥‘𝑗) → (𝑗 + 1) ∈
(ℤ≥‘𝑗)) |
123 | | 1le2 11241 |
. . . . . . . . . . . . . . . . . . 19
⊢ 1 ≤
2 |
124 | | leexp2a 12916 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((2
∈ ℝ ∧ 1 ≤ 2 ∧ (𝑗 + 1) ∈
(ℤ≥‘𝑗)) → (2↑𝑗) ≤ (2↑(𝑗 + 1))) |
125 | 49, 123, 124 | mp3an12 1414 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑗 + 1) ∈
(ℤ≥‘𝑗) → (2↑𝑗) ≤ (2↑(𝑗 + 1))) |
126 | 120, 121,
122, 125 | 4syl 19 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (2↑𝑗) ≤ (2↑(𝑗 + 1))) |
127 | 94, 69 | syl6eleq 2711 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (2↑𝑗) ∈
(ℤ≥‘1)) |
128 | 102 | nnzd 11481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (2↑(𝑗 + 1)) ∈
ℤ) |
129 | | elfz5 12334 |
. . . . . . . . . . . . . . . . . 18
⊢
(((2↑𝑗) ∈
(ℤ≥‘1) ∧ (2↑(𝑗 + 1)) ∈ ℤ) → ((2↑𝑗) ∈ (1...(2↑(𝑗 + 1))) ↔ (2↑𝑗) ≤ (2↑(𝑗 + 1)))) |
130 | 127, 128,
129 | syl2anc 693 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((2↑𝑗) ∈ (1...(2↑(𝑗 + 1))) ↔ (2↑𝑗) ≤ (2↑(𝑗 + 1)))) |
131 | 126, 130 | mpbird 247 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (2↑𝑗) ∈ (1...(2↑(𝑗 + 1)))) |
132 | | fzsplit 12367 |
. . . . . . . . . . . . . . . 16
⊢
((2↑𝑗) ∈
(1...(2↑(𝑗 + 1)))
→ (1...(2↑(𝑗 +
1))) = ((1...(2↑𝑗))
∪ (((2↑𝑗) +
1)...(2↑(𝑗 +
1))))) |
133 | 131, 132 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (1...(2↑(𝑗 + 1))) = ((1...(2↑𝑗)) ∪ (((2↑𝑗) + 1)...(2↑(𝑗 + 1))))) |
134 | 133 | fveq2d 6195 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) →
(#‘(1...(2↑(𝑗 +
1)))) = (#‘((1...(2↑𝑗)) ∪ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))))) |
135 | 95 | times2d 11276 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((2↑𝑗) · 2) = ((2↑𝑗) + (2↑𝑗))) |
136 | 91, 135 | eqtrd 2656 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (2↑(𝑗 + 1)) = ((2↑𝑗) + (2↑𝑗))) |
137 | 102 | nnnn0d 11351 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (2↑(𝑗 + 1)) ∈
ℕ0) |
138 | | hashfz1 13134 |
. . . . . . . . . . . . . . . 16
⊢
((2↑(𝑗 + 1))
∈ ℕ0 → (#‘(1...(2↑(𝑗 + 1)))) = (2↑(𝑗 + 1))) |
139 | 137, 138 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) →
(#‘(1...(2↑(𝑗 +
1)))) = (2↑(𝑗 +
1))) |
140 | 113 | oveq1d 6665 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) →
((#‘(1...(2↑𝑗)))
+ (2↑𝑗)) =
((2↑𝑗) + (2↑𝑗))) |
141 | 136, 139,
140 | 3eqtr4d 2666 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) →
(#‘(1...(2↑(𝑗 +
1)))) = ((#‘(1...(2↑𝑗))) + (2↑𝑗))) |
142 | | fzfid 12772 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (1...(2↑𝑗)) ∈ Fin) |
143 | 94 | nnred 11035 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (2↑𝑗) ∈
ℝ) |
144 | 143 | ltp1d 10954 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (2↑𝑗) < ((2↑𝑗) + 1)) |
145 | | fzdisj 12368 |
. . . . . . . . . . . . . . . 16
⊢
((2↑𝑗) <
((2↑𝑗) + 1) →
((1...(2↑𝑗)) ∩
(((2↑𝑗) +
1)...(2↑(𝑗 + 1)))) =
∅) |
146 | 144, 145 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((1...(2↑𝑗)) ∩ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))) =
∅) |
147 | | hashun 13171 |
. . . . . . . . . . . . . . 15
⊢
(((1...(2↑𝑗))
∈ Fin ∧ (((2↑𝑗) + 1)...(2↑(𝑗 + 1))) ∈ Fin ∧ ((1...(2↑𝑗)) ∩ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))) = ∅) →
(#‘((1...(2↑𝑗))
∪ (((2↑𝑗) +
1)...(2↑(𝑗 + 1))))) =
((#‘(1...(2↑𝑗)))
+ (#‘(((2↑𝑗) +
1)...(2↑(𝑗 +
1)))))) |
148 | 142, 115,
146, 147 | syl3anc 1326 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) →
(#‘((1...(2↑𝑗))
∪ (((2↑𝑗) +
1)...(2↑(𝑗 + 1))))) =
((#‘(1...(2↑𝑗)))
+ (#‘(((2↑𝑗) +
1)...(2↑(𝑗 +
1)))))) |
149 | 134, 141,
148 | 3eqtr3d 2664 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) →
((#‘(1...(2↑𝑗)))
+ (2↑𝑗)) =
((#‘(1...(2↑𝑗)))
+ (#‘(((2↑𝑗) +
1)...(2↑(𝑗 +
1)))))) |
150 | 114, 95, 118, 149 | addcanad 10241 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (2↑𝑗) = (#‘(((2↑𝑗) + 1)...(2↑(𝑗 + 1))))) |
151 | 150 | oveq1d 6665 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((2↑𝑗) · (𝐹‘(2↑(𝑗 + 1)))) = ((#‘(((2↑𝑗) + 1)...(2↑(𝑗 + 1)))) · (𝐹‘(2↑(𝑗 + 1))))) |
152 | | fsumconst 14522 |
. . . . . . . . . . . 12
⊢
(((((2↑𝑗) +
1)...(2↑(𝑗 + 1)))
∈ Fin ∧ (𝐹‘(2↑(𝑗 + 1))) ∈ ℂ) → Σ𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))(𝐹‘(2↑(𝑗 + 1))) = ((#‘(((2↑𝑗) + 1)...(2↑(𝑗 + 1)))) · (𝐹‘(2↑(𝑗 + 1))))) |
153 | 115, 108,
152 | syl2anc 693 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → Σ𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))(𝐹‘(2↑(𝑗 + 1))) = ((#‘(((2↑𝑗) + 1)...(2↑(𝑗 + 1)))) · (𝐹‘(2↑(𝑗 + 1))))) |
154 | 151, 153 | eqtr4d 2659 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((2↑𝑗) · (𝐹‘(2↑(𝑗 + 1)))) = Σ𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))(𝐹‘(2↑(𝑗 + 1)))) |
155 | 107 | adantr 481 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))) → (𝐹‘(2↑(𝑗 + 1))) ∈ ℝ) |
156 | | simpl 473 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝜑) |
157 | 156 | adantr 481 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))) → 𝜑) |
158 | | peano2nn 11032 |
. . . . . . . . . . . . . 14
⊢
((2↑𝑗) ∈
ℕ → ((2↑𝑗)
+ 1) ∈ ℕ) |
159 | 94, 158 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((2↑𝑗) + 1) ∈
ℕ) |
160 | | elfzuz 12338 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1))) → 𝑘 ∈
(ℤ≥‘((2↑𝑗) + 1))) |
161 | | eluznn 11758 |
. . . . . . . . . . . . 13
⊢
((((2↑𝑗) + 1)
∈ ℕ ∧ 𝑘
∈ (ℤ≥‘((2↑𝑗) + 1))) → 𝑘 ∈ ℕ) |
162 | 159, 160,
161 | syl2an 494 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))) → 𝑘 ∈ ℕ) |
163 | 157, 162,
37 | syl2anc 693 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))) → (𝐹‘𝑘) ∈ ℝ) |
164 | | elfzuz3 12339 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1))) → (2↑(𝑗 + 1)) ∈
(ℤ≥‘𝑛)) |
165 | 164 | adantl 482 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))) → (2↑(𝑗 + 1)) ∈
(ℤ≥‘𝑛)) |
166 | | simplll 798 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))) ∧ 𝑘 ∈ (𝑛...(2↑(𝑗 + 1)))) → 𝜑) |
167 | | elfzuz 12338 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1))) → 𝑛 ∈
(ℤ≥‘((2↑𝑗) + 1))) |
168 | | eluznn 11758 |
. . . . . . . . . . . . . . . . 17
⊢
((((2↑𝑗) + 1)
∈ ℕ ∧ 𝑛
∈ (ℤ≥‘((2↑𝑗) + 1))) → 𝑛 ∈ ℕ) |
169 | 159, 167,
168 | syl2an 494 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))) → 𝑛 ∈ ℕ) |
170 | | elfzuz 12338 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ (𝑛...(2↑(𝑗 + 1))) → 𝑘 ∈ (ℤ≥‘𝑛)) |
171 | | eluznn 11758 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑛 ∈ ℕ ∧ 𝑘 ∈
(ℤ≥‘𝑛)) → 𝑘 ∈ ℕ) |
172 | 169, 170,
171 | syl2an 494 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))) ∧ 𝑘 ∈ (𝑛...(2↑(𝑗 + 1)))) → 𝑘 ∈ ℕ) |
173 | 166, 172,
37 | syl2anc 693 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))) ∧ 𝑘 ∈ (𝑛...(2↑(𝑗 + 1)))) → (𝐹‘𝑘) ∈ ℝ) |
174 | | simplll 798 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))) ∧ 𝑘 ∈ (𝑛...((2↑(𝑗 + 1)) − 1))) → 𝜑) |
175 | | elfzuz 12338 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ (𝑛...((2↑(𝑗 + 1)) − 1)) → 𝑘 ∈ (ℤ≥‘𝑛)) |
176 | 169, 175,
171 | syl2an 494 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))) ∧ 𝑘 ∈ (𝑛...((2↑(𝑗 + 1)) − 1))) → 𝑘 ∈ ℕ) |
177 | | climcnds.3 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘(𝑘 + 1)) ≤ (𝐹‘𝑘)) |
178 | 174, 176,
177 | syl2anc 693 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))) ∧ 𝑘 ∈ (𝑛...((2↑(𝑗 + 1)) − 1))) → (𝐹‘(𝑘 + 1)) ≤ (𝐹‘𝑘)) |
179 | 165, 173,
178 | monoord2 12832 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))) → (𝐹‘(2↑(𝑗 + 1))) ≤ (𝐹‘𝑛)) |
180 | 179 | ralrimiva 2966 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ∀𝑛 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))(𝐹‘(2↑(𝑗 + 1))) ≤ (𝐹‘𝑛)) |
181 | | fveq2 6191 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = 𝑘 → (𝐹‘𝑛) = (𝐹‘𝑘)) |
182 | 181 | breq2d 4665 |
. . . . . . . . . . . . 13
⊢ (𝑛 = 𝑘 → ((𝐹‘(2↑(𝑗 + 1))) ≤ (𝐹‘𝑛) ↔ (𝐹‘(2↑(𝑗 + 1))) ≤ (𝐹‘𝑘))) |
183 | 182 | rspccva 3308 |
. . . . . . . . . . . 12
⊢
((∀𝑛 ∈
(((2↑𝑗) +
1)...(2↑(𝑗 +
1)))(𝐹‘(2↑(𝑗 + 1))) ≤ (𝐹‘𝑛) ∧ 𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))) → (𝐹‘(2↑(𝑗 + 1))) ≤ (𝐹‘𝑘)) |
184 | 180, 183 | sylan 488 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))) → (𝐹‘(2↑(𝑗 + 1))) ≤ (𝐹‘𝑘)) |
185 | 115, 155,
163, 184 | fsumle 14531 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → Σ𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))(𝐹‘(2↑(𝑗 + 1))) ≤ Σ𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))(𝐹‘𝑘)) |
186 | 154, 185 | eqbrtrd 4675 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((2↑𝑗) · (𝐹‘(2↑(𝑗 + 1)))) ≤ Σ𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))(𝐹‘𝑘)) |
187 | 143, 107 | remulcld 10070 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((2↑𝑗) · (𝐹‘(2↑(𝑗 + 1)))) ∈ ℝ) |
188 | 115, 163 | fsumrecl 14465 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → Σ𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))(𝐹‘𝑘) ∈ ℝ) |
189 | 51 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (2 ∈ ℝ
∧ 0 < 2)) |
190 | | lemul2 10876 |
. . . . . . . . . 10
⊢
((((2↑𝑗)
· (𝐹‘(2↑(𝑗 + 1)))) ∈ ℝ ∧ Σ𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))(𝐹‘𝑘) ∈ ℝ ∧ (2 ∈ ℝ
∧ 0 < 2)) → (((2↑𝑗) · (𝐹‘(2↑(𝑗 + 1)))) ≤ Σ𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))(𝐹‘𝑘) ↔ (2 · ((2↑𝑗) · (𝐹‘(2↑(𝑗 + 1))))) ≤ (2 · Σ𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))(𝐹‘𝑘)))) |
191 | 187, 188,
189, 190 | syl3anc 1326 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (((2↑𝑗) · (𝐹‘(2↑(𝑗 + 1)))) ≤ Σ𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))(𝐹‘𝑘) ↔ (2 · ((2↑𝑗) · (𝐹‘(2↑(𝑗 + 1))))) ≤ (2 · Σ𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))(𝐹‘𝑘)))) |
192 | 186, 191 | mpbid 222 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (2 ·
((2↑𝑗) · (𝐹‘(2↑(𝑗 + 1))))) ≤ (2 ·
Σ𝑘 ∈
(((2↑𝑗) +
1)...(2↑(𝑗 +
1)))(𝐹‘𝑘))) |
193 | 110, 192 | eqbrtrd 4675 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐺‘(𝑗 + 1)) ≤ (2 · Σ𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))(𝐹‘𝑘))) |
194 | | 1zzd 11408 |
. . . . . . . . . 10
⊢ (𝜑 → 1 ∈
ℤ) |
195 | | nnnn0 11299 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℕ0) |
196 | | simpr 477 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → 𝑛 ∈
ℕ0) |
197 | | nnexpcl 12873 |
. . . . . . . . . . . . . . 15
⊢ ((2
∈ ℕ ∧ 𝑛
∈ ℕ0) → (2↑𝑛) ∈ ℕ) |
198 | 36, 196, 197 | sylancr 695 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) →
(2↑𝑛) ∈
ℕ) |
199 | 198 | nnred 11035 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) →
(2↑𝑛) ∈
ℝ) |
200 | 38 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) →
∀𝑘 ∈ ℕ
(𝐹‘𝑘) ∈ ℝ) |
201 | | fveq2 6191 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = (2↑𝑛) → (𝐹‘𝑘) = (𝐹‘(2↑𝑛))) |
202 | 201 | eleq1d 2686 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = (2↑𝑛) → ((𝐹‘𝑘) ∈ ℝ ↔ (𝐹‘(2↑𝑛)) ∈ ℝ)) |
203 | 202 | rspcv 3305 |
. . . . . . . . . . . . . 14
⊢
((2↑𝑛) ∈
ℕ → (∀𝑘
∈ ℕ (𝐹‘𝑘) ∈ ℝ → (𝐹‘(2↑𝑛)) ∈ ℝ)) |
204 | 198, 200,
203 | sylc 65 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → (𝐹‘(2↑𝑛)) ∈
ℝ) |
205 | 199, 204 | remulcld 10070 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) →
((2↑𝑛) · (𝐹‘(2↑𝑛))) ∈
ℝ) |
206 | 58, 205 | eqeltrd 2701 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → (𝐺‘𝑛) ∈ ℝ) |
207 | 195, 206 | sylan2 491 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐺‘𝑛) ∈ ℝ) |
208 | 69, 194, 207 | serfre 12830 |
. . . . . . . . 9
⊢ (𝜑 → seq1( + , 𝐺):ℕ⟶ℝ) |
209 | 208 | ffvelrnda 6359 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (seq1( + , 𝐺)‘𝑗) ∈ ℝ) |
210 | 207 | ralrimiva 2966 |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑛 ∈ ℕ (𝐺‘𝑛) ∈ ℝ) |
211 | 210 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ∀𝑛 ∈ ℕ (𝐺‘𝑛) ∈ ℝ) |
212 | 81 | eleq1d 2686 |
. . . . . . . . . 10
⊢ (𝑛 = (𝑗 + 1) → ((𝐺‘𝑛) ∈ ℝ ↔ (𝐺‘(𝑗 + 1)) ∈ ℝ)) |
213 | 212 | rspcv 3305 |
. . . . . . . . 9
⊢ ((𝑗 + 1) ∈ ℕ →
(∀𝑛 ∈ ℕ
(𝐺‘𝑛) ∈ ℝ → (𝐺‘(𝑗 + 1)) ∈ ℝ)) |
214 | 78, 211, 213 | sylc 65 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐺‘(𝑗 + 1)) ∈ ℝ) |
215 | 69, 194, 37 | serfre 12830 |
. . . . . . . . . 10
⊢ (𝜑 → seq1( + , 𝐹):ℕ⟶ℝ) |
216 | | ffvelrn 6357 |
. . . . . . . . . 10
⊢ ((seq1( +
, 𝐹):ℕ⟶ℝ
∧ (2↑𝑗) ∈
ℕ) → (seq1( + , 𝐹)‘(2↑𝑗)) ∈ ℝ) |
217 | 215, 93, 216 | syl2an 494 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (seq1( + , 𝐹)‘(2↑𝑗)) ∈
ℝ) |
218 | | remulcl 10021 |
. . . . . . . . 9
⊢ ((2
∈ ℝ ∧ (seq1( + , 𝐹)‘(2↑𝑗)) ∈ ℝ) → (2 · (seq1(
+ , 𝐹)‘(2↑𝑗))) ∈
ℝ) |
219 | 49, 217, 218 | sylancr 695 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (2 · (seq1( +
, 𝐹)‘(2↑𝑗))) ∈
ℝ) |
220 | | remulcl 10021 |
. . . . . . . . 9
⊢ ((2
∈ ℝ ∧ Σ𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))(𝐹‘𝑘) ∈ ℝ) → (2 ·
Σ𝑘 ∈
(((2↑𝑗) +
1)...(2↑(𝑗 +
1)))(𝐹‘𝑘)) ∈
ℝ) |
221 | 49, 188, 220 | sylancr 695 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (2 ·
Σ𝑘 ∈
(((2↑𝑗) +
1)...(2↑(𝑗 +
1)))(𝐹‘𝑘)) ∈
ℝ) |
222 | | le2add 10510 |
. . . . . . . 8
⊢ ((((seq1(
+ , 𝐺)‘𝑗) ∈ ℝ ∧ (𝐺‘(𝑗 + 1)) ∈ ℝ) ∧ ((2 ·
(seq1( + , 𝐹)‘(2↑𝑗))) ∈ ℝ ∧ (2 ·
Σ𝑘 ∈
(((2↑𝑗) +
1)...(2↑(𝑗 +
1)))(𝐹‘𝑘)) ∈ ℝ)) →
(((seq1( + , 𝐺)‘𝑗) ≤ (2 · (seq1( + ,
𝐹)‘(2↑𝑗))) ∧ (𝐺‘(𝑗 + 1)) ≤ (2 · Σ𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))(𝐹‘𝑘))) → ((seq1( + , 𝐺)‘𝑗) + (𝐺‘(𝑗 + 1))) ≤ ((2 · (seq1( + , 𝐹)‘(2↑𝑗))) + (2 · Σ𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))(𝐹‘𝑘))))) |
223 | 209, 214,
219, 221, 222 | syl22anc 1327 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (((seq1( + , 𝐺)‘𝑗) ≤ (2 · (seq1( + , 𝐹)‘(2↑𝑗))) ∧ (𝐺‘(𝑗 + 1)) ≤ (2 · Σ𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))(𝐹‘𝑘))) → ((seq1( + , 𝐺)‘𝑗) + (𝐺‘(𝑗 + 1))) ≤ ((2 · (seq1( + , 𝐹)‘(2↑𝑗))) + (2 · Σ𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))(𝐹‘𝑘))))) |
224 | 193, 223 | mpan2d 710 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((seq1( + , 𝐺)‘𝑗) ≤ (2 · (seq1( + , 𝐹)‘(2↑𝑗))) → ((seq1( + , 𝐺)‘𝑗) + (𝐺‘(𝑗 + 1))) ≤ ((2 · (seq1( + , 𝐹)‘(2↑𝑗))) + (2 · Σ𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))(𝐹‘𝑘))))) |
225 | 119, 69 | syl6eleq 2711 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑗 ∈
(ℤ≥‘1)) |
226 | | seqp1 12816 |
. . . . . . . 8
⊢ (𝑗 ∈
(ℤ≥‘1) → (seq1( + , 𝐺)‘(𝑗 + 1)) = ((seq1( + , 𝐺)‘𝑗) + (𝐺‘(𝑗 + 1)))) |
227 | 225, 226 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (seq1( + , 𝐺)‘(𝑗 + 1)) = ((seq1( + , 𝐺)‘𝑗) + (𝐺‘(𝑗 + 1)))) |
228 | | fzfid 12772 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (1...(2↑(𝑗 + 1))) ∈
Fin) |
229 | | elfznn 12370 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ (1...(2↑(𝑗 + 1))) → 𝑘 ∈
ℕ) |
230 | 37 | recnd 10068 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) ∈ ℂ) |
231 | 156, 229,
230 | syl2an 494 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ (1...(2↑(𝑗 + 1)))) → (𝐹‘𝑘) ∈ ℂ) |
232 | 146, 133,
228, 231 | fsumsplit 14471 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → Σ𝑘 ∈ (1...(2↑(𝑗 + 1)))(𝐹‘𝑘) = (Σ𝑘 ∈ (1...(2↑𝑗))(𝐹‘𝑘) + Σ𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))(𝐹‘𝑘))) |
233 | | eqidd 2623 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ (1...(2↑(𝑗 + 1)))) → (𝐹‘𝑘) = (𝐹‘𝑘)) |
234 | 102, 69 | syl6eleq 2711 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (2↑(𝑗 + 1)) ∈
(ℤ≥‘1)) |
235 | 233, 234,
231 | fsumser 14461 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → Σ𝑘 ∈ (1...(2↑(𝑗 + 1)))(𝐹‘𝑘) = (seq1( + , 𝐹)‘(2↑(𝑗 + 1)))) |
236 | | eqidd 2623 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ (1...(2↑𝑗))) → (𝐹‘𝑘) = (𝐹‘𝑘)) |
237 | | elfznn 12370 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ (1...(2↑𝑗)) → 𝑘 ∈ ℕ) |
238 | 156, 237,
230 | syl2an 494 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ (1...(2↑𝑗))) → (𝐹‘𝑘) ∈ ℂ) |
239 | 236, 127,
238 | fsumser 14461 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → Σ𝑘 ∈ (1...(2↑𝑗))(𝐹‘𝑘) = (seq1( + , 𝐹)‘(2↑𝑗))) |
240 | 239 | oveq1d 6665 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (Σ𝑘 ∈ (1...(2↑𝑗))(𝐹‘𝑘) + Σ𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))(𝐹‘𝑘)) = ((seq1( + , 𝐹)‘(2↑𝑗)) + Σ𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))(𝐹‘𝑘))) |
241 | 232, 235,
240 | 3eqtr3d 2664 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (seq1( + , 𝐹)‘(2↑(𝑗 + 1))) = ((seq1( + , 𝐹)‘(2↑𝑗)) + Σ𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))(𝐹‘𝑘))) |
242 | 241 | oveq2d 6666 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (2 · (seq1( +
, 𝐹)‘(2↑(𝑗 + 1)))) = (2 · ((seq1( +
, 𝐹)‘(2↑𝑗)) + Σ𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))(𝐹‘𝑘)))) |
243 | 217 | recnd 10068 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (seq1( + , 𝐹)‘(2↑𝑗)) ∈
ℂ) |
244 | 188 | recnd 10068 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → Σ𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))(𝐹‘𝑘) ∈ ℂ) |
245 | 100, 243,
244 | adddid 10064 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (2 · ((seq1( +
, 𝐹)‘(2↑𝑗)) + Σ𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))(𝐹‘𝑘))) = ((2 · (seq1( + , 𝐹)‘(2↑𝑗))) + (2 · Σ𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))(𝐹‘𝑘)))) |
246 | 242, 245 | eqtrd 2656 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (2 · (seq1( +
, 𝐹)‘(2↑(𝑗 + 1)))) = ((2 · (seq1( +
, 𝐹)‘(2↑𝑗))) + (2 · Σ𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))(𝐹‘𝑘)))) |
247 | 227, 246 | breq12d 4666 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((seq1( + , 𝐺)‘(𝑗 + 1)) ≤ (2 · (seq1( + , 𝐹)‘(2↑(𝑗 + 1)))) ↔ ((seq1( + ,
𝐺)‘𝑗) + (𝐺‘(𝑗 + 1))) ≤ ((2 · (seq1( + , 𝐹)‘(2↑𝑗))) + (2 · Σ𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))(𝐹‘𝑘))))) |
248 | 224, 247 | sylibrd 249 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((seq1( + , 𝐺)‘𝑗) ≤ (2 · (seq1( + , 𝐹)‘(2↑𝑗))) → (seq1( + , 𝐺)‘(𝑗 + 1)) ≤ (2 · (seq1( + , 𝐹)‘(2↑(𝑗 + 1)))))) |
249 | 248 | expcom 451 |
. . . 4
⊢ (𝑗 ∈ ℕ → (𝜑 → ((seq1( + , 𝐺)‘𝑗) ≤ (2 · (seq1( + , 𝐹)‘(2↑𝑗))) → (seq1( + , 𝐺)‘(𝑗 + 1)) ≤ (2 · (seq1( + , 𝐹)‘(2↑(𝑗 + 1))))))) |
250 | 249 | a2d 29 |
. . 3
⊢ (𝑗 ∈ ℕ → ((𝜑 → (seq1( + , 𝐺)‘𝑗) ≤ (2 · (seq1( + , 𝐹)‘(2↑𝑗)))) → (𝜑 → (seq1( + , 𝐺)‘(𝑗 + 1)) ≤ (2 · (seq1( + , 𝐹)‘(2↑(𝑗 + 1))))))) |
251 | 10, 16, 22, 28, 76, 250 | nnind 11038 |
. 2
⊢ (𝑁 ∈ ℕ → (𝜑 → (seq1( + , 𝐺)‘𝑁) ≤ (2 · (seq1( + , 𝐹)‘(2↑𝑁))))) |
252 | 251 | impcom 446 |
1
⊢ ((𝜑 ∧ 𝑁 ∈ ℕ) → (seq1( + , 𝐺)‘𝑁) ≤ (2 · (seq1( + , 𝐹)‘(2↑𝑁)))) |