| Step | Hyp | Ref
| Expression |
| 1 | | fveq2 6906 |
. . . . 5
⊢ (𝑥 = 1 → (seq1( + , 𝐺)‘𝑥) = (seq1( + , 𝐺)‘1)) |
| 2 | | oveq2 7439 |
. . . . . . . 8
⊢ (𝑥 = 1 → (2↑𝑥) = (2↑1)) |
| 3 | | 2cn 12341 |
. . . . . . . . 9
⊢ 2 ∈
ℂ |
| 4 | | exp1 14108 |
. . . . . . . . 9
⊢ (2 ∈
ℂ → (2↑1) = 2) |
| 5 | 3, 4 | ax-mp 5 |
. . . . . . . 8
⊢
(2↑1) = 2 |
| 6 | 2, 5 | eqtrdi 2793 |
. . . . . . 7
⊢ (𝑥 = 1 → (2↑𝑥) = 2) |
| 7 | 6 | fveq2d 6910 |
. . . . . 6
⊢ (𝑥 = 1 → (seq1( + , 𝐹)‘(2↑𝑥)) = (seq1( + , 𝐹)‘2)) |
| 8 | 7 | oveq2d 7447 |
. . . . 5
⊢ (𝑥 = 1 → (2 · (seq1( +
, 𝐹)‘(2↑𝑥))) = (2 · (seq1( + ,
𝐹)‘2))) |
| 9 | 1, 8 | breq12d 5156 |
. . . 4
⊢ (𝑥 = 1 → ((seq1( + , 𝐺)‘𝑥) ≤ (2 · (seq1( + , 𝐹)‘(2↑𝑥))) ↔ (seq1( + , 𝐺)‘1) ≤ (2 ·
(seq1( + , 𝐹)‘2)))) |
| 10 | 9 | imbi2d 340 |
. . 3
⊢ (𝑥 = 1 → ((𝜑 → (seq1( + , 𝐺)‘𝑥) ≤ (2 · (seq1( + , 𝐹)‘(2↑𝑥)))) ↔ (𝜑 → (seq1( + , 𝐺)‘1) ≤ (2 · (seq1( + , 𝐹)‘2))))) |
| 11 | | fveq2 6906 |
. . . . 5
⊢ (𝑥 = 𝑗 → (seq1( + , 𝐺)‘𝑥) = (seq1( + , 𝐺)‘𝑗)) |
| 12 | | oveq2 7439 |
. . . . . . 7
⊢ (𝑥 = 𝑗 → (2↑𝑥) = (2↑𝑗)) |
| 13 | 12 | fveq2d 6910 |
. . . . . 6
⊢ (𝑥 = 𝑗 → (seq1( + , 𝐹)‘(2↑𝑥)) = (seq1( + , 𝐹)‘(2↑𝑗))) |
| 14 | 13 | oveq2d 7447 |
. . . . 5
⊢ (𝑥 = 𝑗 → (2 · (seq1( + , 𝐹)‘(2↑𝑥))) = (2 · (seq1( + ,
𝐹)‘(2↑𝑗)))) |
| 15 | 11, 14 | breq12d 5156 |
. . . 4
⊢ (𝑥 = 𝑗 → ((seq1( + , 𝐺)‘𝑥) ≤ (2 · (seq1( + , 𝐹)‘(2↑𝑥))) ↔ (seq1( + , 𝐺)‘𝑗) ≤ (2 · (seq1( + , 𝐹)‘(2↑𝑗))))) |
| 16 | 15 | imbi2d 340 |
. . 3
⊢ (𝑥 = 𝑗 → ((𝜑 → (seq1( + , 𝐺)‘𝑥) ≤ (2 · (seq1( + , 𝐹)‘(2↑𝑥)))) ↔ (𝜑 → (seq1( + , 𝐺)‘𝑗) ≤ (2 · (seq1( + , 𝐹)‘(2↑𝑗)))))) |
| 17 | | fveq2 6906 |
. . . . 5
⊢ (𝑥 = (𝑗 + 1) → (seq1( + , 𝐺)‘𝑥) = (seq1( + , 𝐺)‘(𝑗 + 1))) |
| 18 | | oveq2 7439 |
. . . . . . 7
⊢ (𝑥 = (𝑗 + 1) → (2↑𝑥) = (2↑(𝑗 + 1))) |
| 19 | 18 | fveq2d 6910 |
. . . . . 6
⊢ (𝑥 = (𝑗 + 1) → (seq1( + , 𝐹)‘(2↑𝑥)) = (seq1( + , 𝐹)‘(2↑(𝑗 + 1)))) |
| 20 | 19 | oveq2d 7447 |
. . . . 5
⊢ (𝑥 = (𝑗 + 1) → (2 · (seq1( + , 𝐹)‘(2↑𝑥))) = (2 · (seq1( + ,
𝐹)‘(2↑(𝑗 + 1))))) |
| 21 | 17, 20 | breq12d 5156 |
. . . 4
⊢ (𝑥 = (𝑗 + 1) → ((seq1( + , 𝐺)‘𝑥) ≤ (2 · (seq1( + , 𝐹)‘(2↑𝑥))) ↔ (seq1( + , 𝐺)‘(𝑗 + 1)) ≤ (2 · (seq1( + , 𝐹)‘(2↑(𝑗 + 1)))))) |
| 22 | 21 | imbi2d 340 |
. . 3
⊢ (𝑥 = (𝑗 + 1) → ((𝜑 → (seq1( + , 𝐺)‘𝑥) ≤ (2 · (seq1( + , 𝐹)‘(2↑𝑥)))) ↔ (𝜑 → (seq1( + , 𝐺)‘(𝑗 + 1)) ≤ (2 · (seq1( + , 𝐹)‘(2↑(𝑗 + 1))))))) |
| 23 | | fveq2 6906 |
. . . . 5
⊢ (𝑥 = 𝑁 → (seq1( + , 𝐺)‘𝑥) = (seq1( + , 𝐺)‘𝑁)) |
| 24 | | oveq2 7439 |
. . . . . . 7
⊢ (𝑥 = 𝑁 → (2↑𝑥) = (2↑𝑁)) |
| 25 | 24 | fveq2d 6910 |
. . . . . 6
⊢ (𝑥 = 𝑁 → (seq1( + , 𝐹)‘(2↑𝑥)) = (seq1( + , 𝐹)‘(2↑𝑁))) |
| 26 | 25 | oveq2d 7447 |
. . . . 5
⊢ (𝑥 = 𝑁 → (2 · (seq1( + , 𝐹)‘(2↑𝑥))) = (2 · (seq1( + ,
𝐹)‘(2↑𝑁)))) |
| 27 | 23, 26 | breq12d 5156 |
. . . 4
⊢ (𝑥 = 𝑁 → ((seq1( + , 𝐺)‘𝑥) ≤ (2 · (seq1( + , 𝐹)‘(2↑𝑥))) ↔ (seq1( + , 𝐺)‘𝑁) ≤ (2 · (seq1( + , 𝐹)‘(2↑𝑁))))) |
| 28 | 27 | imbi2d 340 |
. . 3
⊢ (𝑥 = 𝑁 → ((𝜑 → (seq1( + , 𝐺)‘𝑥) ≤ (2 · (seq1( + , 𝐹)‘(2↑𝑥)))) ↔ (𝜑 → (seq1( + , 𝐺)‘𝑁) ≤ (2 · (seq1( + , 𝐹)‘(2↑𝑁)))))) |
| 29 | | fveq2 6906 |
. . . . . . . 8
⊢ (𝑘 = 1 → (𝐹‘𝑘) = (𝐹‘1)) |
| 30 | 29 | breq2d 5155 |
. . . . . . 7
⊢ (𝑘 = 1 → (0 ≤ (𝐹‘𝑘) ↔ 0 ≤ (𝐹‘1))) |
| 31 | | climcnds.2 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 0 ≤ (𝐹‘𝑘)) |
| 32 | 31 | ralrimiva 3146 |
. . . . . . 7
⊢ (𝜑 → ∀𝑘 ∈ ℕ 0 ≤ (𝐹‘𝑘)) |
| 33 | | 1nn 12277 |
. . . . . . . 8
⊢ 1 ∈
ℕ |
| 34 | 33 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → 1 ∈
ℕ) |
| 35 | 30, 32, 34 | rspcdva 3623 |
. . . . . 6
⊢ (𝜑 → 0 ≤ (𝐹‘1)) |
| 36 | | fveq2 6906 |
. . . . . . . . 9
⊢ (𝑘 = 2 → (𝐹‘𝑘) = (𝐹‘2)) |
| 37 | 36 | eleq1d 2826 |
. . . . . . . 8
⊢ (𝑘 = 2 → ((𝐹‘𝑘) ∈ ℝ ↔ (𝐹‘2) ∈ ℝ)) |
| 38 | | climcnds.1 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) ∈ ℝ) |
| 39 | 38 | ralrimiva 3146 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑘 ∈ ℕ (𝐹‘𝑘) ∈ ℝ) |
| 40 | | 2nn 12339 |
. . . . . . . . 9
⊢ 2 ∈
ℕ |
| 41 | 40 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → 2 ∈
ℕ) |
| 42 | 37, 39, 41 | rspcdva 3623 |
. . . . . . 7
⊢ (𝜑 → (𝐹‘2) ∈ ℝ) |
| 43 | 29 | eleq1d 2826 |
. . . . . . . 8
⊢ (𝑘 = 1 → ((𝐹‘𝑘) ∈ ℝ ↔ (𝐹‘1) ∈ ℝ)) |
| 44 | 43, 39, 34 | rspcdva 3623 |
. . . . . . 7
⊢ (𝜑 → (𝐹‘1) ∈ ℝ) |
| 45 | 42, 44 | addge02d 11852 |
. . . . . 6
⊢ (𝜑 → (0 ≤ (𝐹‘1) ↔ (𝐹‘2) ≤ ((𝐹‘1) + (𝐹‘2)))) |
| 46 | 35, 45 | mpbid 232 |
. . . . 5
⊢ (𝜑 → (𝐹‘2) ≤ ((𝐹‘1) + (𝐹‘2))) |
| 47 | 44, 42 | readdcld 11290 |
. . . . . 6
⊢ (𝜑 → ((𝐹‘1) + (𝐹‘2)) ∈ ℝ) |
| 48 | 41 | nnrpd 13075 |
. . . . . 6
⊢ (𝜑 → 2 ∈
ℝ+) |
| 49 | 42, 47, 48 | lemul2d 13121 |
. . . . 5
⊢ (𝜑 → ((𝐹‘2) ≤ ((𝐹‘1) + (𝐹‘2)) ↔ (2 · (𝐹‘2)) ≤ (2 ·
((𝐹‘1) + (𝐹‘2))))) |
| 50 | 46, 49 | mpbid 232 |
. . . 4
⊢ (𝜑 → (2 · (𝐹‘2)) ≤ (2 ·
((𝐹‘1) + (𝐹‘2)))) |
| 51 | | 1z 12647 |
. . . . 5
⊢ 1 ∈
ℤ |
| 52 | | fveq2 6906 |
. . . . . . 7
⊢ (𝑛 = 1 → (𝐺‘𝑛) = (𝐺‘1)) |
| 53 | | oveq2 7439 |
. . . . . . . . 9
⊢ (𝑛 = 1 → (2↑𝑛) = (2↑1)) |
| 54 | 53, 5 | eqtrdi 2793 |
. . . . . . . 8
⊢ (𝑛 = 1 → (2↑𝑛) = 2) |
| 55 | 54 | fveq2d 6910 |
. . . . . . . 8
⊢ (𝑛 = 1 → (𝐹‘(2↑𝑛)) = (𝐹‘2)) |
| 56 | 54, 55 | oveq12d 7449 |
. . . . . . 7
⊢ (𝑛 = 1 → ((2↑𝑛) · (𝐹‘(2↑𝑛))) = (2 · (𝐹‘2))) |
| 57 | 52, 56 | eqeq12d 2753 |
. . . . . 6
⊢ (𝑛 = 1 → ((𝐺‘𝑛) = ((2↑𝑛) · (𝐹‘(2↑𝑛))) ↔ (𝐺‘1) = (2 · (𝐹‘2)))) |
| 58 | | climcnds.4 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → (𝐺‘𝑛) = ((2↑𝑛) · (𝐹‘(2↑𝑛)))) |
| 59 | 58 | ralrimiva 3146 |
. . . . . 6
⊢ (𝜑 → ∀𝑛 ∈ ℕ0 (𝐺‘𝑛) = ((2↑𝑛) · (𝐹‘(2↑𝑛)))) |
| 60 | | 1nn0 12542 |
. . . . . . 7
⊢ 1 ∈
ℕ0 |
| 61 | 60 | a1i 11 |
. . . . . 6
⊢ (𝜑 → 1 ∈
ℕ0) |
| 62 | 57, 59, 61 | rspcdva 3623 |
. . . . 5
⊢ (𝜑 → (𝐺‘1) = (2 · (𝐹‘2))) |
| 63 | 51, 62 | seq1i 14056 |
. . . 4
⊢ (𝜑 → (seq1( + , 𝐺)‘1) = (2 · (𝐹‘2))) |
| 64 | | nnuz 12921 |
. . . . . 6
⊢ ℕ =
(ℤ≥‘1) |
| 65 | | df-2 12329 |
. . . . . 6
⊢ 2 = (1 +
1) |
| 66 | | eqidd 2738 |
. . . . . . 7
⊢ (𝜑 → (𝐹‘1) = (𝐹‘1)) |
| 67 | 51, 66 | seq1i 14056 |
. . . . . 6
⊢ (𝜑 → (seq1( + , 𝐹)‘1) = (𝐹‘1)) |
| 68 | | eqidd 2738 |
. . . . . 6
⊢ (𝜑 → (𝐹‘2) = (𝐹‘2)) |
| 69 | 64, 34, 65, 67, 68 | seqp1d 14059 |
. . . . 5
⊢ (𝜑 → (seq1( + , 𝐹)‘2) = ((𝐹‘1) + (𝐹‘2))) |
| 70 | 69 | oveq2d 7447 |
. . . 4
⊢ (𝜑 → (2 · (seq1( + ,
𝐹)‘2)) = (2 ·
((𝐹‘1) + (𝐹‘2)))) |
| 71 | 50, 63, 70 | 3brtr4d 5175 |
. . 3
⊢ (𝜑 → (seq1( + , 𝐺)‘1) ≤ (2 ·
(seq1( + , 𝐹)‘2))) |
| 72 | | fveq2 6906 |
. . . . . . . . . . 11
⊢ (𝑛 = (𝑗 + 1) → (𝐺‘𝑛) = (𝐺‘(𝑗 + 1))) |
| 73 | | oveq2 7439 |
. . . . . . . . . . . 12
⊢ (𝑛 = (𝑗 + 1) → (2↑𝑛) = (2↑(𝑗 + 1))) |
| 74 | 73 | fveq2d 6910 |
. . . . . . . . . . . 12
⊢ (𝑛 = (𝑗 + 1) → (𝐹‘(2↑𝑛)) = (𝐹‘(2↑(𝑗 + 1)))) |
| 75 | 73, 74 | oveq12d 7449 |
. . . . . . . . . . 11
⊢ (𝑛 = (𝑗 + 1) → ((2↑𝑛) · (𝐹‘(2↑𝑛))) = ((2↑(𝑗 + 1)) · (𝐹‘(2↑(𝑗 + 1))))) |
| 76 | 72, 75 | eqeq12d 2753 |
. . . . . . . . . 10
⊢ (𝑛 = (𝑗 + 1) → ((𝐺‘𝑛) = ((2↑𝑛) · (𝐹‘(2↑𝑛))) ↔ (𝐺‘(𝑗 + 1)) = ((2↑(𝑗 + 1)) · (𝐹‘(2↑(𝑗 + 1)))))) |
| 77 | 59 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ∀𝑛 ∈ ℕ0
(𝐺‘𝑛) = ((2↑𝑛) · (𝐹‘(2↑𝑛)))) |
| 78 | | peano2nn 12278 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈ ℕ → (𝑗 + 1) ∈
ℕ) |
| 79 | 78 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑗 + 1) ∈ ℕ) |
| 80 | 79 | nnnn0d 12587 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑗 + 1) ∈
ℕ0) |
| 81 | 76, 77, 80 | rspcdva 3623 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐺‘(𝑗 + 1)) = ((2↑(𝑗 + 1)) · (𝐹‘(2↑(𝑗 + 1))))) |
| 82 | | nnnn0 12533 |
. . . . . . . . . . . . 13
⊢ (𝑗 ∈ ℕ → 𝑗 ∈
ℕ0) |
| 83 | 82 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ ℕ0) |
| 84 | | expp1 14109 |
. . . . . . . . . . . 12
⊢ ((2
∈ ℂ ∧ 𝑗
∈ ℕ0) → (2↑(𝑗 + 1)) = ((2↑𝑗) · 2)) |
| 85 | 3, 83, 84 | sylancr 587 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (2↑(𝑗 + 1)) = ((2↑𝑗) · 2)) |
| 86 | | nnexpcl 14115 |
. . . . . . . . . . . . . . 15
⊢ ((2
∈ ℕ ∧ 𝑗
∈ ℕ0) → (2↑𝑗) ∈ ℕ) |
| 87 | 40, 82, 86 | sylancr 587 |
. . . . . . . . . . . . . 14
⊢ (𝑗 ∈ ℕ →
(2↑𝑗) ∈
ℕ) |
| 88 | 87 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (2↑𝑗) ∈
ℕ) |
| 89 | 88 | nncnd 12282 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (2↑𝑗) ∈
ℂ) |
| 90 | | mulcom 11241 |
. . . . . . . . . . . 12
⊢
(((2↑𝑗) ∈
ℂ ∧ 2 ∈ ℂ) → ((2↑𝑗) · 2) = (2 · (2↑𝑗))) |
| 91 | 89, 3, 90 | sylancl 586 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((2↑𝑗) · 2) = (2 ·
(2↑𝑗))) |
| 92 | 85, 91 | eqtrd 2777 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (2↑(𝑗 + 1)) = (2 ·
(2↑𝑗))) |
| 93 | 92 | oveq1d 7446 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((2↑(𝑗 + 1)) · (𝐹‘(2↑(𝑗 + 1)))) = ((2 ·
(2↑𝑗)) · (𝐹‘(2↑(𝑗 + 1))))) |
| 94 | 3 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 2 ∈
ℂ) |
| 95 | | fveq2 6906 |
. . . . . . . . . . . . 13
⊢ (𝑘 = (2↑(𝑗 + 1)) → (𝐹‘𝑘) = (𝐹‘(2↑(𝑗 + 1)))) |
| 96 | 95 | eleq1d 2826 |
. . . . . . . . . . . 12
⊢ (𝑘 = (2↑(𝑗 + 1)) → ((𝐹‘𝑘) ∈ ℝ ↔ (𝐹‘(2↑(𝑗 + 1))) ∈ ℝ)) |
| 97 | 39 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ∀𝑘 ∈ ℕ (𝐹‘𝑘) ∈ ℝ) |
| 98 | | nnexpcl 14115 |
. . . . . . . . . . . . 13
⊢ ((2
∈ ℕ ∧ (𝑗 +
1) ∈ ℕ0) → (2↑(𝑗 + 1)) ∈ ℕ) |
| 99 | 40, 80, 98 | sylancr 587 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (2↑(𝑗 + 1)) ∈
ℕ) |
| 100 | 96, 97, 99 | rspcdva 3623 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐹‘(2↑(𝑗 + 1))) ∈ ℝ) |
| 101 | 100 | recnd 11289 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐹‘(2↑(𝑗 + 1))) ∈ ℂ) |
| 102 | 94, 89, 101 | mulassd 11284 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((2 ·
(2↑𝑗)) · (𝐹‘(2↑(𝑗 + 1)))) = (2 ·
((2↑𝑗) · (𝐹‘(2↑(𝑗 + 1)))))) |
| 103 | 81, 93, 102 | 3eqtrd 2781 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐺‘(𝑗 + 1)) = (2 · ((2↑𝑗) · (𝐹‘(2↑(𝑗 + 1)))))) |
| 104 | 88 | nnnn0d 12587 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (2↑𝑗) ∈
ℕ0) |
| 105 | | hashfz1 14385 |
. . . . . . . . . . . . . . 15
⊢
((2↑𝑗) ∈
ℕ0 → (♯‘(1...(2↑𝑗))) = (2↑𝑗)) |
| 106 | 104, 105 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) →
(♯‘(1...(2↑𝑗))) = (2↑𝑗)) |
| 107 | 106, 89 | eqeltrd 2841 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) →
(♯‘(1...(2↑𝑗))) ∈ ℂ) |
| 108 | | fzfid 14014 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (((2↑𝑗) + 1)...(2↑(𝑗 + 1))) ∈
Fin) |
| 109 | | hashcl 14395 |
. . . . . . . . . . . . . . 15
⊢
((((2↑𝑗) +
1)...(2↑(𝑗 + 1)))
∈ Fin → (♯‘(((2↑𝑗) + 1)...(2↑(𝑗 + 1)))) ∈
ℕ0) |
| 110 | 108, 109 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) →
(♯‘(((2↑𝑗)
+ 1)...(2↑(𝑗 + 1))))
∈ ℕ0) |
| 111 | 110 | nn0cnd 12589 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) →
(♯‘(((2↑𝑗)
+ 1)...(2↑(𝑗 + 1))))
∈ ℂ) |
| 112 | | simpr 484 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ ℕ) |
| 113 | 112 | nnzd 12640 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ ℤ) |
| 114 | | uzid 12893 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 ∈ ℤ → 𝑗 ∈
(ℤ≥‘𝑗)) |
| 115 | | peano2uz 12943 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 ∈
(ℤ≥‘𝑗) → (𝑗 + 1) ∈
(ℤ≥‘𝑗)) |
| 116 | | 2re 12340 |
. . . . . . . . . . . . . . . . . . 19
⊢ 2 ∈
ℝ |
| 117 | | 1le2 12475 |
. . . . . . . . . . . . . . . . . . 19
⊢ 1 ≤
2 |
| 118 | | leexp2a 14212 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((2
∈ ℝ ∧ 1 ≤ 2 ∧ (𝑗 + 1) ∈
(ℤ≥‘𝑗)) → (2↑𝑗) ≤ (2↑(𝑗 + 1))) |
| 119 | 116, 117,
118 | mp3an12 1453 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑗 + 1) ∈
(ℤ≥‘𝑗) → (2↑𝑗) ≤ (2↑(𝑗 + 1))) |
| 120 | 113, 114,
115, 119 | 4syl 19 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (2↑𝑗) ≤ (2↑(𝑗 + 1))) |
| 121 | 88, 64 | eleqtrdi 2851 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (2↑𝑗) ∈
(ℤ≥‘1)) |
| 122 | 99 | nnzd 12640 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (2↑(𝑗 + 1)) ∈
ℤ) |
| 123 | | elfz5 13556 |
. . . . . . . . . . . . . . . . . 18
⊢
(((2↑𝑗) ∈
(ℤ≥‘1) ∧ (2↑(𝑗 + 1)) ∈ ℤ) → ((2↑𝑗) ∈ (1...(2↑(𝑗 + 1))) ↔ (2↑𝑗) ≤ (2↑(𝑗 + 1)))) |
| 124 | 121, 122,
123 | syl2anc 584 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((2↑𝑗) ∈ (1...(2↑(𝑗 + 1))) ↔ (2↑𝑗) ≤ (2↑(𝑗 + 1)))) |
| 125 | 120, 124 | mpbird 257 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (2↑𝑗) ∈ (1...(2↑(𝑗 + 1)))) |
| 126 | | fzsplit 13590 |
. . . . . . . . . . . . . . . 16
⊢
((2↑𝑗) ∈
(1...(2↑(𝑗 + 1)))
→ (1...(2↑(𝑗 +
1))) = ((1...(2↑𝑗))
∪ (((2↑𝑗) +
1)...(2↑(𝑗 +
1))))) |
| 127 | 125, 126 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (1...(2↑(𝑗 + 1))) = ((1...(2↑𝑗)) ∪ (((2↑𝑗) + 1)...(2↑(𝑗 + 1))))) |
| 128 | 127 | fveq2d 6910 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) →
(♯‘(1...(2↑(𝑗 + 1)))) = (♯‘((1...(2↑𝑗)) ∪ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))))) |
| 129 | 89 | times2d 12510 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((2↑𝑗) · 2) = ((2↑𝑗) + (2↑𝑗))) |
| 130 | 85, 129 | eqtrd 2777 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (2↑(𝑗 + 1)) = ((2↑𝑗) + (2↑𝑗))) |
| 131 | 99 | nnnn0d 12587 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (2↑(𝑗 + 1)) ∈
ℕ0) |
| 132 | | hashfz1 14385 |
. . . . . . . . . . . . . . . 16
⊢
((2↑(𝑗 + 1))
∈ ℕ0 → (♯‘(1...(2↑(𝑗 + 1)))) = (2↑(𝑗 + 1))) |
| 133 | 131, 132 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) →
(♯‘(1...(2↑(𝑗 + 1)))) = (2↑(𝑗 + 1))) |
| 134 | 106 | oveq1d 7446 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) →
((♯‘(1...(2↑𝑗))) + (2↑𝑗)) = ((2↑𝑗) + (2↑𝑗))) |
| 135 | 130, 133,
134 | 3eqtr4d 2787 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) →
(♯‘(1...(2↑(𝑗 + 1)))) = ((♯‘(1...(2↑𝑗))) + (2↑𝑗))) |
| 136 | | fzfid 14014 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (1...(2↑𝑗)) ∈ Fin) |
| 137 | 88 | nnred 12281 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (2↑𝑗) ∈
ℝ) |
| 138 | 137 | ltp1d 12198 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (2↑𝑗) < ((2↑𝑗) + 1)) |
| 139 | | fzdisj 13591 |
. . . . . . . . . . . . . . . 16
⊢
((2↑𝑗) <
((2↑𝑗) + 1) →
((1...(2↑𝑗)) ∩
(((2↑𝑗) +
1)...(2↑(𝑗 + 1)))) =
∅) |
| 140 | 138, 139 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((1...(2↑𝑗)) ∩ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))) =
∅) |
| 141 | | hashun 14421 |
. . . . . . . . . . . . . . 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)))))) |
| 142 | 136, 108,
140, 141 | syl3anc 1373 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) →
(♯‘((1...(2↑𝑗)) ∪ (((2↑𝑗) + 1)...(2↑(𝑗 + 1))))) =
((♯‘(1...(2↑𝑗))) + (♯‘(((2↑𝑗) + 1)...(2↑(𝑗 + 1)))))) |
| 143 | 128, 135,
142 | 3eqtr3d 2785 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) →
((♯‘(1...(2↑𝑗))) + (2↑𝑗)) = ((♯‘(1...(2↑𝑗))) +
(♯‘(((2↑𝑗)
+ 1)...(2↑(𝑗 +
1)))))) |
| 144 | 107, 89, 111, 143 | addcanad 11466 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (2↑𝑗) =
(♯‘(((2↑𝑗)
+ 1)...(2↑(𝑗 +
1))))) |
| 145 | 144 | oveq1d 7446 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((2↑𝑗) · (𝐹‘(2↑(𝑗 + 1)))) = ((♯‘(((2↑𝑗) + 1)...(2↑(𝑗 + 1)))) · (𝐹‘(2↑(𝑗 + 1))))) |
| 146 | | fsumconst 15826 |
. . . . . . . . . . . 12
⊢
(((((2↑𝑗) +
1)...(2↑(𝑗 + 1)))
∈ Fin ∧ (𝐹‘(2↑(𝑗 + 1))) ∈ ℂ) → Σ𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))(𝐹‘(2↑(𝑗 + 1))) = ((♯‘(((2↑𝑗) + 1)...(2↑(𝑗 + 1)))) · (𝐹‘(2↑(𝑗 + 1))))) |
| 147 | 108, 101,
146 | syl2anc 584 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → Σ𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))(𝐹‘(2↑(𝑗 + 1))) = ((♯‘(((2↑𝑗) + 1)...(2↑(𝑗 + 1)))) · (𝐹‘(2↑(𝑗 + 1))))) |
| 148 | 145, 147 | eqtr4d 2780 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((2↑𝑗) · (𝐹‘(2↑(𝑗 + 1)))) = Σ𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))(𝐹‘(2↑(𝑗 + 1)))) |
| 149 | 100 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))) → (𝐹‘(2↑(𝑗 + 1))) ∈ ℝ) |
| 150 | | simpl 482 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝜑) |
| 151 | | peano2nn 12278 |
. . . . . . . . . . . . . 14
⊢
((2↑𝑗) ∈
ℕ → ((2↑𝑗)
+ 1) ∈ ℕ) |
| 152 | 88, 151 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((2↑𝑗) + 1) ∈
ℕ) |
| 153 | | elfzuz 13560 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1))) → 𝑘 ∈
(ℤ≥‘((2↑𝑗) + 1))) |
| 154 | | eluznn 12960 |
. . . . . . . . . . . . 13
⊢
((((2↑𝑗) + 1)
∈ ℕ ∧ 𝑘
∈ (ℤ≥‘((2↑𝑗) + 1))) → 𝑘 ∈ ℕ) |
| 155 | 152, 153,
154 | syl2an 596 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))) → 𝑘 ∈ ℕ) |
| 156 | 150, 155,
38 | syl2an2r 685 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))) → (𝐹‘𝑘) ∈ ℝ) |
| 157 | | elfzuz3 13561 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1))) → (2↑(𝑗 + 1)) ∈
(ℤ≥‘𝑛)) |
| 158 | 157 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))) → (2↑(𝑗 + 1)) ∈
(ℤ≥‘𝑛)) |
| 159 | | simplll 775 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))) ∧ 𝑘 ∈ (𝑛...(2↑(𝑗 + 1)))) → 𝜑) |
| 160 | | elfzuz 13560 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1))) → 𝑛 ∈
(ℤ≥‘((2↑𝑗) + 1))) |
| 161 | | eluznn 12960 |
. . . . . . . . . . . . . . . . 17
⊢
((((2↑𝑗) + 1)
∈ ℕ ∧ 𝑛
∈ (ℤ≥‘((2↑𝑗) + 1))) → 𝑛 ∈ ℕ) |
| 162 | 152, 160,
161 | syl2an 596 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))) → 𝑛 ∈ ℕ) |
| 163 | | elfzuz 13560 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ (𝑛...(2↑(𝑗 + 1))) → 𝑘 ∈ (ℤ≥‘𝑛)) |
| 164 | | eluznn 12960 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑛 ∈ ℕ ∧ 𝑘 ∈
(ℤ≥‘𝑛)) → 𝑘 ∈ ℕ) |
| 165 | 162, 163,
164 | syl2an 596 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))) ∧ 𝑘 ∈ (𝑛...(2↑(𝑗 + 1)))) → 𝑘 ∈ ℕ) |
| 166 | 159, 165,
38 | syl2anc 584 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))) ∧ 𝑘 ∈ (𝑛...(2↑(𝑗 + 1)))) → (𝐹‘𝑘) ∈ ℝ) |
| 167 | | simplll 775 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))) ∧ 𝑘 ∈ (𝑛...((2↑(𝑗 + 1)) − 1))) → 𝜑) |
| 168 | | elfzuz 13560 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ (𝑛...((2↑(𝑗 + 1)) − 1)) → 𝑘 ∈ (ℤ≥‘𝑛)) |
| 169 | 162, 168,
164 | syl2an 596 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))) ∧ 𝑘 ∈ (𝑛...((2↑(𝑗 + 1)) − 1))) → 𝑘 ∈ ℕ) |
| 170 | | climcnds.3 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘(𝑘 + 1)) ≤ (𝐹‘𝑘)) |
| 171 | 167, 169,
170 | syl2anc 584 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))) ∧ 𝑘 ∈ (𝑛...((2↑(𝑗 + 1)) − 1))) → (𝐹‘(𝑘 + 1)) ≤ (𝐹‘𝑘)) |
| 172 | 158, 166,
171 | monoord2 14074 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))) → (𝐹‘(2↑(𝑗 + 1))) ≤ (𝐹‘𝑛)) |
| 173 | 172 | ralrimiva 3146 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ∀𝑛 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))(𝐹‘(2↑(𝑗 + 1))) ≤ (𝐹‘𝑛)) |
| 174 | | fveq2 6906 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = 𝑘 → (𝐹‘𝑛) = (𝐹‘𝑘)) |
| 175 | 174 | breq2d 5155 |
. . . . . . . . . . . . 13
⊢ (𝑛 = 𝑘 → ((𝐹‘(2↑(𝑗 + 1))) ≤ (𝐹‘𝑛) ↔ (𝐹‘(2↑(𝑗 + 1))) ≤ (𝐹‘𝑘))) |
| 176 | 175 | rspccva 3621 |
. . . . . . . . . . . 12
⊢
((∀𝑛 ∈
(((2↑𝑗) +
1)...(2↑(𝑗 +
1)))(𝐹‘(2↑(𝑗 + 1))) ≤ (𝐹‘𝑛) ∧ 𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))) → (𝐹‘(2↑(𝑗 + 1))) ≤ (𝐹‘𝑘)) |
| 177 | 173, 176 | sylan 580 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))) → (𝐹‘(2↑(𝑗 + 1))) ≤ (𝐹‘𝑘)) |
| 178 | 108, 149,
156, 177 | fsumle 15835 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → Σ𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))(𝐹‘(2↑(𝑗 + 1))) ≤ Σ𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))(𝐹‘𝑘)) |
| 179 | 148, 178 | eqbrtrd 5165 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((2↑𝑗) · (𝐹‘(2↑(𝑗 + 1)))) ≤ Σ𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))(𝐹‘𝑘)) |
| 180 | 137, 100 | remulcld 11291 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((2↑𝑗) · (𝐹‘(2↑(𝑗 + 1)))) ∈ ℝ) |
| 181 | 108, 156 | fsumrecl 15770 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → Σ𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))(𝐹‘𝑘) ∈ ℝ) |
| 182 | | 2rp 13039 |
. . . . . . . . . . 11
⊢ 2 ∈
ℝ+ |
| 183 | 182 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 2 ∈
ℝ+) |
| 184 | 180, 181,
183 | lemul2d 13121 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (((2↑𝑗) · (𝐹‘(2↑(𝑗 + 1)))) ≤ Σ𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))(𝐹‘𝑘) ↔ (2 · ((2↑𝑗) · (𝐹‘(2↑(𝑗 + 1))))) ≤ (2 · Σ𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))(𝐹‘𝑘)))) |
| 185 | 179, 184 | mpbid 232 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (2 ·
((2↑𝑗) · (𝐹‘(2↑(𝑗 + 1))))) ≤ (2 ·
Σ𝑘 ∈
(((2↑𝑗) +
1)...(2↑(𝑗 +
1)))(𝐹‘𝑘))) |
| 186 | 103, 185 | eqbrtrd 5165 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐺‘(𝑗 + 1)) ≤ (2 · Σ𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))(𝐹‘𝑘))) |
| 187 | | 1zzd 12648 |
. . . . . . . . . 10
⊢ (𝜑 → 1 ∈
ℤ) |
| 188 | | nnnn0 12533 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℕ0) |
| 189 | | simpr 484 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → 𝑛 ∈
ℕ0) |
| 190 | | nnexpcl 14115 |
. . . . . . . . . . . . . . 15
⊢ ((2
∈ ℕ ∧ 𝑛
∈ ℕ0) → (2↑𝑛) ∈ ℕ) |
| 191 | 40, 189, 190 | sylancr 587 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) →
(2↑𝑛) ∈
ℕ) |
| 192 | 191 | nnred 12281 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) →
(2↑𝑛) ∈
ℝ) |
| 193 | | fveq2 6906 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = (2↑𝑛) → (𝐹‘𝑘) = (𝐹‘(2↑𝑛))) |
| 194 | 193 | eleq1d 2826 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = (2↑𝑛) → ((𝐹‘𝑘) ∈ ℝ ↔ (𝐹‘(2↑𝑛)) ∈ ℝ)) |
| 195 | 39 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) →
∀𝑘 ∈ ℕ
(𝐹‘𝑘) ∈ ℝ) |
| 196 | 194, 195,
191 | rspcdva 3623 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → (𝐹‘(2↑𝑛)) ∈
ℝ) |
| 197 | 192, 196 | remulcld 11291 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) →
((2↑𝑛) · (𝐹‘(2↑𝑛))) ∈
ℝ) |
| 198 | 58, 197 | eqeltrd 2841 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → (𝐺‘𝑛) ∈ ℝ) |
| 199 | 188, 198 | sylan2 593 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐺‘𝑛) ∈ ℝ) |
| 200 | 64, 187, 199 | serfre 14072 |
. . . . . . . . 9
⊢ (𝜑 → seq1( + , 𝐺):ℕ⟶ℝ) |
| 201 | 200 | ffvelcdmda 7104 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (seq1( + , 𝐺)‘𝑗) ∈ ℝ) |
| 202 | 72 | eleq1d 2826 |
. . . . . . . . 9
⊢ (𝑛 = (𝑗 + 1) → ((𝐺‘𝑛) ∈ ℝ ↔ (𝐺‘(𝑗 + 1)) ∈ ℝ)) |
| 203 | 199 | ralrimiva 3146 |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑛 ∈ ℕ (𝐺‘𝑛) ∈ ℝ) |
| 204 | 203 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ∀𝑛 ∈ ℕ (𝐺‘𝑛) ∈ ℝ) |
| 205 | 202, 204,
79 | rspcdva 3623 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐺‘(𝑗 + 1)) ∈ ℝ) |
| 206 | 64, 187, 38 | serfre 14072 |
. . . . . . . . . 10
⊢ (𝜑 → seq1( + , 𝐹):ℕ⟶ℝ) |
| 207 | | ffvelcdm 7101 |
. . . . . . . . . 10
⊢ ((seq1( +
, 𝐹):ℕ⟶ℝ
∧ (2↑𝑗) ∈
ℕ) → (seq1( + , 𝐹)‘(2↑𝑗)) ∈ ℝ) |
| 208 | 206, 87, 207 | syl2an 596 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (seq1( + , 𝐹)‘(2↑𝑗)) ∈
ℝ) |
| 209 | | remulcl 11240 |
. . . . . . . . 9
⊢ ((2
∈ ℝ ∧ (seq1( + , 𝐹)‘(2↑𝑗)) ∈ ℝ) → (2 · (seq1(
+ , 𝐹)‘(2↑𝑗))) ∈
ℝ) |
| 210 | 116, 208,
209 | sylancr 587 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (2 · (seq1( +
, 𝐹)‘(2↑𝑗))) ∈
ℝ) |
| 211 | | remulcl 11240 |
. . . . . . . . 9
⊢ ((2
∈ ℝ ∧ Σ𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))(𝐹‘𝑘) ∈ ℝ) → (2 ·
Σ𝑘 ∈
(((2↑𝑗) +
1)...(2↑(𝑗 +
1)))(𝐹‘𝑘)) ∈
ℝ) |
| 212 | 116, 181,
211 | sylancr 587 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (2 ·
Σ𝑘 ∈
(((2↑𝑗) +
1)...(2↑(𝑗 +
1)))(𝐹‘𝑘)) ∈
ℝ) |
| 213 | | le2add 11745 |
. . . . . . . 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)))(𝐹‘𝑘))))) |
| 214 | 201, 205,
210, 212, 213 | syl22anc 839 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (((seq1( + , 𝐺)‘𝑗) ≤ (2 · (seq1( + , 𝐹)‘(2↑𝑗))) ∧ (𝐺‘(𝑗 + 1)) ≤ (2 · Σ𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))(𝐹‘𝑘))) → ((seq1( + , 𝐺)‘𝑗) + (𝐺‘(𝑗 + 1))) ≤ ((2 · (seq1( + , 𝐹)‘(2↑𝑗))) + (2 · Σ𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))(𝐹‘𝑘))))) |
| 215 | 186, 214 | mpan2d 694 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((seq1( + , 𝐺)‘𝑗) ≤ (2 · (seq1( + , 𝐹)‘(2↑𝑗))) → ((seq1( + , 𝐺)‘𝑗) + (𝐺‘(𝑗 + 1))) ≤ ((2 · (seq1( + , 𝐹)‘(2↑𝑗))) + (2 · Σ𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))(𝐹‘𝑘))))) |
| 216 | 112, 64 | eleqtrdi 2851 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑗 ∈
(ℤ≥‘1)) |
| 217 | | seqp1 14057 |
. . . . . . . 8
⊢ (𝑗 ∈
(ℤ≥‘1) → (seq1( + , 𝐺)‘(𝑗 + 1)) = ((seq1( + , 𝐺)‘𝑗) + (𝐺‘(𝑗 + 1)))) |
| 218 | 216, 217 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (seq1( + , 𝐺)‘(𝑗 + 1)) = ((seq1( + , 𝐺)‘𝑗) + (𝐺‘(𝑗 + 1)))) |
| 219 | | fzfid 14014 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (1...(2↑(𝑗 + 1))) ∈
Fin) |
| 220 | | elfznn 13593 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ (1...(2↑(𝑗 + 1))) → 𝑘 ∈
ℕ) |
| 221 | 38 | recnd 11289 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) ∈ ℂ) |
| 222 | 150, 220,
221 | syl2an 596 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ (1...(2↑(𝑗 + 1)))) → (𝐹‘𝑘) ∈ ℂ) |
| 223 | 140, 127,
219, 222 | fsumsplit 15777 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → Σ𝑘 ∈ (1...(2↑(𝑗 + 1)))(𝐹‘𝑘) = (Σ𝑘 ∈ (1...(2↑𝑗))(𝐹‘𝑘) + Σ𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))(𝐹‘𝑘))) |
| 224 | | eqidd 2738 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ (1...(2↑(𝑗 + 1)))) → (𝐹‘𝑘) = (𝐹‘𝑘)) |
| 225 | 99, 64 | eleqtrdi 2851 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (2↑(𝑗 + 1)) ∈
(ℤ≥‘1)) |
| 226 | 224, 225,
222 | fsumser 15766 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → Σ𝑘 ∈ (1...(2↑(𝑗 + 1)))(𝐹‘𝑘) = (seq1( + , 𝐹)‘(2↑(𝑗 + 1)))) |
| 227 | | eqidd 2738 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ (1...(2↑𝑗))) → (𝐹‘𝑘) = (𝐹‘𝑘)) |
| 228 | | elfznn 13593 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ (1...(2↑𝑗)) → 𝑘 ∈ ℕ) |
| 229 | 150, 228,
221 | syl2an 596 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ (1...(2↑𝑗))) → (𝐹‘𝑘) ∈ ℂ) |
| 230 | 227, 121,
229 | fsumser 15766 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → Σ𝑘 ∈ (1...(2↑𝑗))(𝐹‘𝑘) = (seq1( + , 𝐹)‘(2↑𝑗))) |
| 231 | 230 | oveq1d 7446 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (Σ𝑘 ∈ (1...(2↑𝑗))(𝐹‘𝑘) + Σ𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))(𝐹‘𝑘)) = ((seq1( + , 𝐹)‘(2↑𝑗)) + Σ𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))(𝐹‘𝑘))) |
| 232 | 223, 226,
231 | 3eqtr3d 2785 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (seq1( + , 𝐹)‘(2↑(𝑗 + 1))) = ((seq1( + , 𝐹)‘(2↑𝑗)) + Σ𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))(𝐹‘𝑘))) |
| 233 | 232 | oveq2d 7447 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (2 · (seq1( +
, 𝐹)‘(2↑(𝑗 + 1)))) = (2 · ((seq1( +
, 𝐹)‘(2↑𝑗)) + Σ𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))(𝐹‘𝑘)))) |
| 234 | 208 | recnd 11289 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (seq1( + , 𝐹)‘(2↑𝑗)) ∈
ℂ) |
| 235 | 181 | recnd 11289 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → Σ𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))(𝐹‘𝑘) ∈ ℂ) |
| 236 | 94, 234, 235 | adddid 11285 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (2 · ((seq1( +
, 𝐹)‘(2↑𝑗)) + Σ𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))(𝐹‘𝑘))) = ((2 · (seq1( + , 𝐹)‘(2↑𝑗))) + (2 · Σ𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))(𝐹‘𝑘)))) |
| 237 | 233, 236 | eqtrd 2777 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (2 · (seq1( +
, 𝐹)‘(2↑(𝑗 + 1)))) = ((2 · (seq1( +
, 𝐹)‘(2↑𝑗))) + (2 · Σ𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))(𝐹‘𝑘)))) |
| 238 | 218, 237 | breq12d 5156 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((seq1( + , 𝐺)‘(𝑗 + 1)) ≤ (2 · (seq1( + , 𝐹)‘(2↑(𝑗 + 1)))) ↔ ((seq1( + ,
𝐺)‘𝑗) + (𝐺‘(𝑗 + 1))) ≤ ((2 · (seq1( + , 𝐹)‘(2↑𝑗))) + (2 · Σ𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))(𝐹‘𝑘))))) |
| 239 | 215, 238 | sylibrd 259 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((seq1( + , 𝐺)‘𝑗) ≤ (2 · (seq1( + , 𝐹)‘(2↑𝑗))) → (seq1( + , 𝐺)‘(𝑗 + 1)) ≤ (2 · (seq1( + , 𝐹)‘(2↑(𝑗 + 1)))))) |
| 240 | 239 | expcom 413 |
. . . 4
⊢ (𝑗 ∈ ℕ → (𝜑 → ((seq1( + , 𝐺)‘𝑗) ≤ (2 · (seq1( + , 𝐹)‘(2↑𝑗))) → (seq1( + , 𝐺)‘(𝑗 + 1)) ≤ (2 · (seq1( + , 𝐹)‘(2↑(𝑗 + 1))))))) |
| 241 | 240 | a2d 29 |
. . 3
⊢ (𝑗 ∈ ℕ → ((𝜑 → (seq1( + , 𝐺)‘𝑗) ≤ (2 · (seq1( + , 𝐹)‘(2↑𝑗)))) → (𝜑 → (seq1( + , 𝐺)‘(𝑗 + 1)) ≤ (2 · (seq1( + , 𝐹)‘(2↑(𝑗 + 1))))))) |
| 242 | 10, 16, 22, 28, 71, 241 | nnind 12284 |
. 2
⊢ (𝑁 ∈ ℕ → (𝜑 → (seq1( + , 𝐺)‘𝑁) ≤ (2 · (seq1( + , 𝐹)‘(2↑𝑁))))) |
| 243 | 242 | impcom 407 |
1
⊢ ((𝜑 ∧ 𝑁 ∈ ℕ) → (seq1( + , 𝐺)‘𝑁) ≤ (2 · (seq1( + , 𝐹)‘(2↑𝑁)))) |