| Step | Hyp | Ref
| Expression |
| 1 | | oveq1 7438 |
. . . . . . . . . . 11
⊢ (𝑥 = 0 → (𝑥 + 1) = (0 + 1)) |
| 2 | | 0p1e1 12388 |
. . . . . . . . . . 11
⊢ (0 + 1) =
1 |
| 3 | 1, 2 | eqtrdi 2793 |
. . . . . . . . . 10
⊢ (𝑥 = 0 → (𝑥 + 1) = 1) |
| 4 | 3 | oveq2d 7447 |
. . . . . . . . 9
⊢ (𝑥 = 0 → (2↑(𝑥 + 1)) =
(2↑1)) |
| 5 | | 2cn 12341 |
. . . . . . . . . . 11
⊢ 2 ∈
ℂ |
| 6 | | exp1 14108 |
. . . . . . . . . . 11
⊢ (2 ∈
ℂ → (2↑1) = 2) |
| 7 | 5, 6 | ax-mp 5 |
. . . . . . . . . 10
⊢
(2↑1) = 2 |
| 8 | | df-2 12329 |
. . . . . . . . . 10
⊢ 2 = (1 +
1) |
| 9 | 7, 8 | eqtri 2765 |
. . . . . . . . 9
⊢
(2↑1) = (1 + 1) |
| 10 | 4, 9 | eqtrdi 2793 |
. . . . . . . 8
⊢ (𝑥 = 0 → (2↑(𝑥 + 1)) = (1 +
1)) |
| 11 | 10 | oveq1d 7446 |
. . . . . . 7
⊢ (𝑥 = 0 → ((2↑(𝑥 + 1)) − 1) = ((1 + 1)
− 1)) |
| 12 | | ax-1cn 11213 |
. . . . . . . 8
⊢ 1 ∈
ℂ |
| 13 | 12, 12 | pncan3oi 11524 |
. . . . . . 7
⊢ ((1 + 1)
− 1) = 1 |
| 14 | 11, 13 | eqtrdi 2793 |
. . . . . 6
⊢ (𝑥 = 0 → ((2↑(𝑥 + 1)) − 1) =
1) |
| 15 | 14 | fveq2d 6910 |
. . . . 5
⊢ (𝑥 = 0 → (seq1( + , 𝐹)‘((2↑(𝑥 + 1)) − 1)) = (seq1( + ,
𝐹)‘1)) |
| 16 | | fveq2 6906 |
. . . . 5
⊢ (𝑥 = 0 → (seq0( + , 𝐺)‘𝑥) = (seq0( + , 𝐺)‘0)) |
| 17 | 15, 16 | breq12d 5156 |
. . . 4
⊢ (𝑥 = 0 → ((seq1( + , 𝐹)‘((2↑(𝑥 + 1)) − 1)) ≤ (seq0( +
, 𝐺)‘𝑥) ↔ (seq1( + , 𝐹)‘1) ≤ (seq0( + , 𝐺)‘0))) |
| 18 | 17 | imbi2d 340 |
. . 3
⊢ (𝑥 = 0 → ((𝜑 → (seq1( + , 𝐹)‘((2↑(𝑥 + 1)) − 1)) ≤ (seq0( + , 𝐺)‘𝑥)) ↔ (𝜑 → (seq1( + , 𝐹)‘1) ≤ (seq0( + , 𝐺)‘0)))) |
| 19 | | oveq1 7438 |
. . . . . . 7
⊢ (𝑥 = 𝑗 → (𝑥 + 1) = (𝑗 + 1)) |
| 20 | 19 | oveq2d 7447 |
. . . . . 6
⊢ (𝑥 = 𝑗 → (2↑(𝑥 + 1)) = (2↑(𝑗 + 1))) |
| 21 | 20 | fvoveq1d 7453 |
. . . . 5
⊢ (𝑥 = 𝑗 → (seq1( + , 𝐹)‘((2↑(𝑥 + 1)) − 1)) = (seq1( + , 𝐹)‘((2↑(𝑗 + 1)) −
1))) |
| 22 | | fveq2 6906 |
. . . . 5
⊢ (𝑥 = 𝑗 → (seq0( + , 𝐺)‘𝑥) = (seq0( + , 𝐺)‘𝑗)) |
| 23 | 21, 22 | breq12d 5156 |
. . . 4
⊢ (𝑥 = 𝑗 → ((seq1( + , 𝐹)‘((2↑(𝑥 + 1)) − 1)) ≤ (seq0( + , 𝐺)‘𝑥) ↔ (seq1( + , 𝐹)‘((2↑(𝑗 + 1)) − 1)) ≤ (seq0( + , 𝐺)‘𝑗))) |
| 24 | 23 | imbi2d 340 |
. . 3
⊢ (𝑥 = 𝑗 → ((𝜑 → (seq1( + , 𝐹)‘((2↑(𝑥 + 1)) − 1)) ≤ (seq0( + , 𝐺)‘𝑥)) ↔ (𝜑 → (seq1( + , 𝐹)‘((2↑(𝑗 + 1)) − 1)) ≤ (seq0( + , 𝐺)‘𝑗)))) |
| 25 | | oveq1 7438 |
. . . . . . 7
⊢ (𝑥 = (𝑗 + 1) → (𝑥 + 1) = ((𝑗 + 1) + 1)) |
| 26 | 25 | oveq2d 7447 |
. . . . . 6
⊢ (𝑥 = (𝑗 + 1) → (2↑(𝑥 + 1)) = (2↑((𝑗 + 1) + 1))) |
| 27 | 26 | fvoveq1d 7453 |
. . . . 5
⊢ (𝑥 = (𝑗 + 1) → (seq1( + , 𝐹)‘((2↑(𝑥 + 1)) − 1)) = (seq1( + , 𝐹)‘((2↑((𝑗 + 1) + 1)) −
1))) |
| 28 | | fveq2 6906 |
. . . . 5
⊢ (𝑥 = (𝑗 + 1) → (seq0( + , 𝐺)‘𝑥) = (seq0( + , 𝐺)‘(𝑗 + 1))) |
| 29 | 27, 28 | breq12d 5156 |
. . . 4
⊢ (𝑥 = (𝑗 + 1) → ((seq1( + , 𝐹)‘((2↑(𝑥 + 1)) − 1)) ≤ (seq0( + , 𝐺)‘𝑥) ↔ (seq1( + , 𝐹)‘((2↑((𝑗 + 1) + 1)) − 1)) ≤ (seq0( + , 𝐺)‘(𝑗 + 1)))) |
| 30 | 29 | imbi2d 340 |
. . 3
⊢ (𝑥 = (𝑗 + 1) → ((𝜑 → (seq1( + , 𝐹)‘((2↑(𝑥 + 1)) − 1)) ≤ (seq0( + , 𝐺)‘𝑥)) ↔ (𝜑 → (seq1( + , 𝐹)‘((2↑((𝑗 + 1) + 1)) − 1)) ≤ (seq0( + , 𝐺)‘(𝑗 + 1))))) |
| 31 | | oveq1 7438 |
. . . . . . 7
⊢ (𝑥 = 𝑁 → (𝑥 + 1) = (𝑁 + 1)) |
| 32 | 31 | oveq2d 7447 |
. . . . . 6
⊢ (𝑥 = 𝑁 → (2↑(𝑥 + 1)) = (2↑(𝑁 + 1))) |
| 33 | 32 | fvoveq1d 7453 |
. . . . 5
⊢ (𝑥 = 𝑁 → (seq1( + , 𝐹)‘((2↑(𝑥 + 1)) − 1)) = (seq1( + , 𝐹)‘((2↑(𝑁 + 1)) −
1))) |
| 34 | | fveq2 6906 |
. . . . 5
⊢ (𝑥 = 𝑁 → (seq0( + , 𝐺)‘𝑥) = (seq0( + , 𝐺)‘𝑁)) |
| 35 | 33, 34 | breq12d 5156 |
. . . 4
⊢ (𝑥 = 𝑁 → ((seq1( + , 𝐹)‘((2↑(𝑥 + 1)) − 1)) ≤ (seq0( + , 𝐺)‘𝑥) ↔ (seq1( + , 𝐹)‘((2↑(𝑁 + 1)) − 1)) ≤ (seq0( + , 𝐺)‘𝑁))) |
| 36 | 35 | imbi2d 340 |
. . 3
⊢ (𝑥 = 𝑁 → ((𝜑 → (seq1( + , 𝐹)‘((2↑(𝑥 + 1)) − 1)) ≤ (seq0( + , 𝐺)‘𝑥)) ↔ (𝜑 → (seq1( + , 𝐹)‘((2↑(𝑁 + 1)) − 1)) ≤ (seq0( + , 𝐺)‘𝑁)))) |
| 37 | | fveq2 6906 |
. . . . . . . 8
⊢ (𝑘 = 1 → (𝐹‘𝑘) = (𝐹‘1)) |
| 38 | 37 | eleq1d 2826 |
. . . . . . 7
⊢ (𝑘 = 1 → ((𝐹‘𝑘) ∈ ℝ ↔ (𝐹‘1) ∈ ℝ)) |
| 39 | | climcnds.1 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) ∈ ℝ) |
| 40 | 39 | ralrimiva 3146 |
. . . . . . 7
⊢ (𝜑 → ∀𝑘 ∈ ℕ (𝐹‘𝑘) ∈ ℝ) |
| 41 | | 1nn 12277 |
. . . . . . . 8
⊢ 1 ∈
ℕ |
| 42 | 41 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → 1 ∈
ℕ) |
| 43 | 38, 40, 42 | rspcdva 3623 |
. . . . . 6
⊢ (𝜑 → (𝐹‘1) ∈ ℝ) |
| 44 | 43 | leidd 11829 |
. . . . 5
⊢ (𝜑 → (𝐹‘1) ≤ (𝐹‘1)) |
| 45 | 43 | recnd 11289 |
. . . . . 6
⊢ (𝜑 → (𝐹‘1) ∈ ℂ) |
| 46 | 45 | mullidd 11279 |
. . . . 5
⊢ (𝜑 → (1 · (𝐹‘1)) = (𝐹‘1)) |
| 47 | 44, 46 | breqtrrd 5171 |
. . . 4
⊢ (𝜑 → (𝐹‘1) ≤ (1 · (𝐹‘1))) |
| 48 | | 1z 12647 |
. . . . 5
⊢ 1 ∈
ℤ |
| 49 | | eqidd 2738 |
. . . . 5
⊢ (𝜑 → (𝐹‘1) = (𝐹‘1)) |
| 50 | 48, 49 | seq1i 14056 |
. . . 4
⊢ (𝜑 → (seq1( + , 𝐹)‘1) = (𝐹‘1)) |
| 51 | | 0z 12624 |
. . . . 5
⊢ 0 ∈
ℤ |
| 52 | | fveq2 6906 |
. . . . . . 7
⊢ (𝑛 = 0 → (𝐺‘𝑛) = (𝐺‘0)) |
| 53 | | oveq2 7439 |
. . . . . . . . 9
⊢ (𝑛 = 0 → (2↑𝑛) = (2↑0)) |
| 54 | | exp0 14106 |
. . . . . . . . . 10
⊢ (2 ∈
ℂ → (2↑0) = 1) |
| 55 | 5, 54 | ax-mp 5 |
. . . . . . . . 9
⊢
(2↑0) = 1 |
| 56 | 53, 55 | eqtrdi 2793 |
. . . . . . . 8
⊢ (𝑛 = 0 → (2↑𝑛) = 1) |
| 57 | 56 | fveq2d 6910 |
. . . . . . . 8
⊢ (𝑛 = 0 → (𝐹‘(2↑𝑛)) = (𝐹‘1)) |
| 58 | 56, 57 | oveq12d 7449 |
. . . . . . 7
⊢ (𝑛 = 0 → ((2↑𝑛) · (𝐹‘(2↑𝑛))) = (1 · (𝐹‘1))) |
| 59 | 52, 58 | eqeq12d 2753 |
. . . . . 6
⊢ (𝑛 = 0 → ((𝐺‘𝑛) = ((2↑𝑛) · (𝐹‘(2↑𝑛))) ↔ (𝐺‘0) = (1 · (𝐹‘1)))) |
| 60 | | climcnds.4 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → (𝐺‘𝑛) = ((2↑𝑛) · (𝐹‘(2↑𝑛)))) |
| 61 | 60 | ralrimiva 3146 |
. . . . . 6
⊢ (𝜑 → ∀𝑛 ∈ ℕ0 (𝐺‘𝑛) = ((2↑𝑛) · (𝐹‘(2↑𝑛)))) |
| 62 | | 0nn0 12541 |
. . . . . . 7
⊢ 0 ∈
ℕ0 |
| 63 | 62 | a1i 11 |
. . . . . 6
⊢ (𝜑 → 0 ∈
ℕ0) |
| 64 | 59, 61, 63 | rspcdva 3623 |
. . . . 5
⊢ (𝜑 → (𝐺‘0) = (1 · (𝐹‘1))) |
| 65 | 51, 64 | seq1i 14056 |
. . . 4
⊢ (𝜑 → (seq0( + , 𝐺)‘0) = (1 · (𝐹‘1))) |
| 66 | 47, 50, 65 | 3brtr4d 5175 |
. . 3
⊢ (𝜑 → (seq1( + , 𝐹)‘1) ≤ (seq0( + , 𝐺)‘0)) |
| 67 | | fzfid 14014 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
((2↑(𝑗 +
1))...((2↑((𝑗 + 1) +
1)) − 1)) ∈ Fin) |
| 68 | | simpl 482 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → 𝜑) |
| 69 | | 2nn 12339 |
. . . . . . . . . . . 12
⊢ 2 ∈
ℕ |
| 70 | | peano2nn0 12566 |
. . . . . . . . . . . . 13
⊢ (𝑗 ∈ ℕ0
→ (𝑗 + 1) ∈
ℕ0) |
| 71 | 70 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → (𝑗 + 1) ∈
ℕ0) |
| 72 | | nnexpcl 14115 |
. . . . . . . . . . . 12
⊢ ((2
∈ ℕ ∧ (𝑗 +
1) ∈ ℕ0) → (2↑(𝑗 + 1)) ∈ ℕ) |
| 73 | 69, 71, 72 | sylancr 587 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
(2↑(𝑗 + 1)) ∈
ℕ) |
| 74 | | elfzuz 13560 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1)) →
𝑘 ∈
(ℤ≥‘(2↑(𝑗 + 1)))) |
| 75 | | eluznn 12960 |
. . . . . . . . . . 11
⊢
(((2↑(𝑗 + 1))
∈ ℕ ∧ 𝑘
∈ (ℤ≥‘(2↑(𝑗 + 1)))) → 𝑘 ∈ ℕ) |
| 76 | 73, 74, 75 | syl2an 596 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ0) ∧ 𝑘 ∈ ((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1))) →
𝑘 ∈
ℕ) |
| 77 | 68, 76, 39 | syl2an2r 685 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ0) ∧ 𝑘 ∈ ((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1))) →
(𝐹‘𝑘) ∈ ℝ) |
| 78 | | fveq2 6906 |
. . . . . . . . . . . 12
⊢ (𝑘 = (2↑(𝑗 + 1)) → (𝐹‘𝑘) = (𝐹‘(2↑(𝑗 + 1)))) |
| 79 | 78 | eleq1d 2826 |
. . . . . . . . . . 11
⊢ (𝑘 = (2↑(𝑗 + 1)) → ((𝐹‘𝑘) ∈ ℝ ↔ (𝐹‘(2↑(𝑗 + 1))) ∈ ℝ)) |
| 80 | 40 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
∀𝑘 ∈ ℕ
(𝐹‘𝑘) ∈ ℝ) |
| 81 | 79, 80, 73 | rspcdva 3623 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → (𝐹‘(2↑(𝑗 + 1))) ∈
ℝ) |
| 82 | 81 | adantr 480 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ0) ∧ 𝑘 ∈ ((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1))) →
(𝐹‘(2↑(𝑗 + 1))) ∈
ℝ) |
| 83 | | simpr 484 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ0) ∧ 𝑛 ∈
(ℤ≥‘(2↑(𝑗 + 1)))) → 𝑛 ∈
(ℤ≥‘(2↑(𝑗 + 1)))) |
| 84 | | simplll 775 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ0) ∧ 𝑛 ∈
(ℤ≥‘(2↑(𝑗 + 1)))) ∧ 𝑘 ∈ ((2↑(𝑗 + 1))...𝑛)) → 𝜑) |
| 85 | 73 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ0) ∧ 𝑛 ∈
(ℤ≥‘(2↑(𝑗 + 1)))) → (2↑(𝑗 + 1)) ∈ ℕ) |
| 86 | | elfzuz 13560 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ ((2↑(𝑗 + 1))...𝑛) → 𝑘 ∈
(ℤ≥‘(2↑(𝑗 + 1)))) |
| 87 | 85, 86, 75 | syl2an 596 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ0) ∧ 𝑛 ∈
(ℤ≥‘(2↑(𝑗 + 1)))) ∧ 𝑘 ∈ ((2↑(𝑗 + 1))...𝑛)) → 𝑘 ∈ ℕ) |
| 88 | 84, 87, 39 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ0) ∧ 𝑛 ∈
(ℤ≥‘(2↑(𝑗 + 1)))) ∧ 𝑘 ∈ ((2↑(𝑗 + 1))...𝑛)) → (𝐹‘𝑘) ∈ ℝ) |
| 89 | | simplll 775 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ0) ∧ 𝑛 ∈
(ℤ≥‘(2↑(𝑗 + 1)))) ∧ 𝑘 ∈ ((2↑(𝑗 + 1))...(𝑛 − 1))) → 𝜑) |
| 90 | | elfzuz 13560 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ ((2↑(𝑗 + 1))...(𝑛 − 1)) → 𝑘 ∈
(ℤ≥‘(2↑(𝑗 + 1)))) |
| 91 | 85, 90, 75 | syl2an 596 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ0) ∧ 𝑛 ∈
(ℤ≥‘(2↑(𝑗 + 1)))) ∧ 𝑘 ∈ ((2↑(𝑗 + 1))...(𝑛 − 1))) → 𝑘 ∈ ℕ) |
| 92 | | climcnds.3 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘(𝑘 + 1)) ≤ (𝐹‘𝑘)) |
| 93 | 89, 91, 92 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ0) ∧ 𝑛 ∈
(ℤ≥‘(2↑(𝑗 + 1)))) ∧ 𝑘 ∈ ((2↑(𝑗 + 1))...(𝑛 − 1))) → (𝐹‘(𝑘 + 1)) ≤ (𝐹‘𝑘)) |
| 94 | 83, 88, 93 | monoord2 14074 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ0) ∧ 𝑛 ∈
(ℤ≥‘(2↑(𝑗 + 1)))) → (𝐹‘𝑛) ≤ (𝐹‘(2↑(𝑗 + 1)))) |
| 95 | 94 | ralrimiva 3146 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
∀𝑛 ∈
(ℤ≥‘(2↑(𝑗 + 1)))(𝐹‘𝑛) ≤ (𝐹‘(2↑(𝑗 + 1)))) |
| 96 | | fveq2 6906 |
. . . . . . . . . . . 12
⊢ (𝑛 = 𝑘 → (𝐹‘𝑛) = (𝐹‘𝑘)) |
| 97 | 96 | breq1d 5153 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑘 → ((𝐹‘𝑛) ≤ (𝐹‘(2↑(𝑗 + 1))) ↔ (𝐹‘𝑘) ≤ (𝐹‘(2↑(𝑗 + 1))))) |
| 98 | 97 | rspccva 3621 |
. . . . . . . . . 10
⊢
((∀𝑛 ∈
(ℤ≥‘(2↑(𝑗 + 1)))(𝐹‘𝑛) ≤ (𝐹‘(2↑(𝑗 + 1))) ∧ 𝑘 ∈
(ℤ≥‘(2↑(𝑗 + 1)))) → (𝐹‘𝑘) ≤ (𝐹‘(2↑(𝑗 + 1)))) |
| 99 | 95, 74, 98 | syl2an 596 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ0) ∧ 𝑘 ∈ ((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1))) →
(𝐹‘𝑘) ≤ (𝐹‘(2↑(𝑗 + 1)))) |
| 100 | 67, 77, 82, 99 | fsumle 15835 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
Σ𝑘 ∈
((2↑(𝑗 +
1))...((2↑((𝑗 + 1) +
1)) − 1))(𝐹‘𝑘) ≤ Σ𝑘 ∈ ((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1))(𝐹‘(2↑(𝑗 + 1)))) |
| 101 | | fzfid 14014 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
(1...((2↑(𝑗 + 1))
− 1)) ∈ Fin) |
| 102 | | hashcl 14395 |
. . . . . . . . . . . . 13
⊢
((1...((2↑(𝑗 +
1)) − 1)) ∈ Fin → (♯‘(1...((2↑(𝑗 + 1)) − 1))) ∈
ℕ0) |
| 103 | 101, 102 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
(♯‘(1...((2↑(𝑗 + 1)) − 1))) ∈
ℕ0) |
| 104 | 103 | nn0cnd 12589 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
(♯‘(1...((2↑(𝑗 + 1)) − 1))) ∈
ℂ) |
| 105 | 73 | nnred 12281 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
(2↑(𝑗 + 1)) ∈
ℝ) |
| 106 | 105 | recnd 11289 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
(2↑(𝑗 + 1)) ∈
ℂ) |
| 107 | | hashcl 14395 |
. . . . . . . . . . . . 13
⊢
(((2↑(𝑗 +
1))...((2↑((𝑗 + 1) +
1)) − 1)) ∈ Fin → (♯‘((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1))) ∈
ℕ0) |
| 108 | 67, 107 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
(♯‘((2↑(𝑗
+ 1))...((2↑((𝑗 + 1) +
1)) − 1))) ∈ ℕ0) |
| 109 | 108 | nn0cnd 12589 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
(♯‘((2↑(𝑗
+ 1))...((2↑((𝑗 + 1) +
1)) − 1))) ∈ ℂ) |
| 110 | | 2z 12649 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 2 ∈
ℤ |
| 111 | | zexpcl 14117 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((2
∈ ℤ ∧ (𝑗 +
1) ∈ ℕ0) → (2↑(𝑗 + 1)) ∈ ℤ) |
| 112 | 110, 71, 111 | sylancr 587 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
(2↑(𝑗 + 1)) ∈
ℤ) |
| 113 | | 2re 12340 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 2 ∈
ℝ |
| 114 | | 1le2 12475 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 1 ≤
2 |
| 115 | | nn0p1nn 12565 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑗 ∈ ℕ0
→ (𝑗 + 1) ∈
ℕ) |
| 116 | 115 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → (𝑗 + 1) ∈
ℕ) |
| 117 | | nnuz 12921 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ℕ =
(ℤ≥‘1) |
| 118 | 116, 117 | eleqtrdi 2851 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → (𝑗 + 1) ∈
(ℤ≥‘1)) |
| 119 | | leexp2a 14212 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((2
∈ ℝ ∧ 1 ≤ 2 ∧ (𝑗 + 1) ∈
(ℤ≥‘1)) → (2↑1) ≤ (2↑(𝑗 + 1))) |
| 120 | 113, 114,
118, 119 | mp3an12i 1467 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
(2↑1) ≤ (2↑(𝑗
+ 1))) |
| 121 | 7, 120 | eqbrtrrid 5179 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → 2 ≤
(2↑(𝑗 +
1))) |
| 122 | 110 | eluz1i 12886 |
. . . . . . . . . . . . . . . . . . 19
⊢
((2↑(𝑗 + 1))
∈ (ℤ≥‘2) ↔ ((2↑(𝑗 + 1)) ∈ ℤ ∧ 2 ≤
(2↑(𝑗 +
1)))) |
| 123 | 112, 121,
122 | sylanbrc 583 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
(2↑(𝑗 + 1)) ∈
(ℤ≥‘2)) |
| 124 | | uz2m1nn 12965 |
. . . . . . . . . . . . . . . . . 18
⊢
((2↑(𝑗 + 1))
∈ (ℤ≥‘2) → ((2↑(𝑗 + 1)) − 1) ∈
ℕ) |
| 125 | 123, 124 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
((2↑(𝑗 + 1)) −
1) ∈ ℕ) |
| 126 | 125, 117 | eleqtrdi 2851 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
((2↑(𝑗 + 1)) −
1) ∈ (ℤ≥‘1)) |
| 127 | | peano2zm 12660 |
. . . . . . . . . . . . . . . . . 18
⊢
((2↑(𝑗 + 1))
∈ ℤ → ((2↑(𝑗 + 1)) − 1) ∈
ℤ) |
| 128 | 112, 127 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
((2↑(𝑗 + 1)) −
1) ∈ ℤ) |
| 129 | | peano2nn0 12566 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑗 + 1) ∈ ℕ0
→ ((𝑗 + 1) + 1) ∈
ℕ0) |
| 130 | 71, 129 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → ((𝑗 + 1) + 1) ∈
ℕ0) |
| 131 | | zexpcl 14117 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((2
∈ ℤ ∧ ((𝑗 +
1) + 1) ∈ ℕ0) → (2↑((𝑗 + 1) + 1)) ∈ ℤ) |
| 132 | 110, 130,
131 | sylancr 587 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
(2↑((𝑗 + 1) + 1))
∈ ℤ) |
| 133 | | peano2zm 12660 |
. . . . . . . . . . . . . . . . . 18
⊢
((2↑((𝑗 + 1) +
1)) ∈ ℤ → ((2↑((𝑗 + 1) + 1)) − 1) ∈
ℤ) |
| 134 | 132, 133 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
((2↑((𝑗 + 1) + 1))
− 1) ∈ ℤ) |
| 135 | 112 | zred 12722 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
(2↑(𝑗 + 1)) ∈
ℝ) |
| 136 | 132 | zred 12722 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
(2↑((𝑗 + 1) + 1))
∈ ℝ) |
| 137 | | 1red 11262 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → 1 ∈
ℝ) |
| 138 | 71 | nn0zd 12639 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → (𝑗 + 1) ∈
ℤ) |
| 139 | | uzid 12893 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑗 + 1) ∈ ℤ →
(𝑗 + 1) ∈
(ℤ≥‘(𝑗 + 1))) |
| 140 | | peano2uz 12943 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑗 + 1) ∈
(ℤ≥‘(𝑗 + 1)) → ((𝑗 + 1) + 1) ∈
(ℤ≥‘(𝑗 + 1))) |
| 141 | | leexp2a 14212 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((2
∈ ℝ ∧ 1 ≤ 2 ∧ ((𝑗 + 1) + 1) ∈
(ℤ≥‘(𝑗 + 1))) → (2↑(𝑗 + 1)) ≤ (2↑((𝑗 + 1) + 1))) |
| 142 | 113, 114,
141 | mp3an12 1453 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑗 + 1) + 1) ∈
(ℤ≥‘(𝑗 + 1)) → (2↑(𝑗 + 1)) ≤ (2↑((𝑗 + 1) + 1))) |
| 143 | 138, 139,
140, 142 | 4syl 19 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
(2↑(𝑗 + 1)) ≤
(2↑((𝑗 + 1) +
1))) |
| 144 | 135, 136,
137, 143 | lesub1dd 11879 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
((2↑(𝑗 + 1)) −
1) ≤ ((2↑((𝑗 + 1) +
1)) − 1)) |
| 145 | | eluz2 12884 |
. . . . . . . . . . . . . . . . 17
⊢
(((2↑((𝑗 + 1) +
1)) − 1) ∈ (ℤ≥‘((2↑(𝑗 + 1)) − 1)) ↔
(((2↑(𝑗 + 1)) −
1) ∈ ℤ ∧ ((2↑((𝑗 + 1) + 1)) − 1) ∈ ℤ ∧
((2↑(𝑗 + 1)) −
1) ≤ ((2↑((𝑗 + 1) +
1)) − 1))) |
| 146 | 128, 134,
144, 145 | syl3anbrc 1344 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
((2↑((𝑗 + 1) + 1))
− 1) ∈ (ℤ≥‘((2↑(𝑗 + 1)) − 1))) |
| 147 | | elfzuzb 13558 |
. . . . . . . . . . . . . . . 16
⊢
(((2↑(𝑗 + 1))
− 1) ∈ (1...((2↑((𝑗 + 1) + 1)) − 1)) ↔
(((2↑(𝑗 + 1)) −
1) ∈ (ℤ≥‘1) ∧ ((2↑((𝑗 + 1) + 1)) − 1) ∈
(ℤ≥‘((2↑(𝑗 + 1)) − 1)))) |
| 148 | 126, 146,
147 | sylanbrc 583 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
((2↑(𝑗 + 1)) −
1) ∈ (1...((2↑((𝑗
+ 1) + 1)) − 1))) |
| 149 | | fzsplit 13590 |
. . . . . . . . . . . . . . 15
⊢
(((2↑(𝑗 + 1))
− 1) ∈ (1...((2↑((𝑗 + 1) + 1)) − 1)) →
(1...((2↑((𝑗 + 1) +
1)) − 1)) = ((1...((2↑(𝑗 + 1)) − 1)) ∪ ((((2↑(𝑗 + 1)) − 1) +
1)...((2↑((𝑗 + 1) +
1)) − 1)))) |
| 150 | 148, 149 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
(1...((2↑((𝑗 + 1) +
1)) − 1)) = ((1...((2↑(𝑗 + 1)) − 1)) ∪ ((((2↑(𝑗 + 1)) − 1) +
1)...((2↑((𝑗 + 1) +
1)) − 1)))) |
| 151 | | npcan 11517 |
. . . . . . . . . . . . . . . . 17
⊢
(((2↑(𝑗 + 1))
∈ ℂ ∧ 1 ∈ ℂ) → (((2↑(𝑗 + 1)) − 1) + 1) = (2↑(𝑗 + 1))) |
| 152 | 106, 12, 151 | sylancl 586 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
(((2↑(𝑗 + 1)) −
1) + 1) = (2↑(𝑗 +
1))) |
| 153 | 152 | oveq1d 7446 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
((((2↑(𝑗 + 1)) −
1) + 1)...((2↑((𝑗 + 1)
+ 1)) − 1)) = ((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1))) |
| 154 | 153 | uneq2d 4168 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
((1...((2↑(𝑗 + 1))
− 1)) ∪ ((((2↑(𝑗 + 1)) − 1) + 1)...((2↑((𝑗 + 1) + 1)) − 1))) =
((1...((2↑(𝑗 + 1))
− 1)) ∪ ((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1)))) |
| 155 | 150, 154 | eqtrd 2777 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
(1...((2↑((𝑗 + 1) +
1)) − 1)) = ((1...((2↑(𝑗 + 1)) − 1)) ∪ ((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) −
1)))) |
| 156 | 155 | fveq2d 6910 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
(♯‘(1...((2↑((𝑗 + 1) + 1)) − 1))) =
(♯‘((1...((2↑(𝑗 + 1)) − 1)) ∪ ((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) −
1))))) |
| 157 | | expp1 14109 |
. . . . . . . . . . . . . . . . 17
⊢ ((2
∈ ℂ ∧ (𝑗 +
1) ∈ ℕ0) → (2↑((𝑗 + 1) + 1)) = ((2↑(𝑗 + 1)) · 2)) |
| 158 | 5, 71, 157 | sylancr 587 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
(2↑((𝑗 + 1) + 1)) =
((2↑(𝑗 + 1)) ·
2)) |
| 159 | 106 | times2d 12510 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
((2↑(𝑗 + 1)) ·
2) = ((2↑(𝑗 + 1)) +
(2↑(𝑗 +
1)))) |
| 160 | 158, 159 | eqtrd 2777 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
(2↑((𝑗 + 1) + 1)) =
((2↑(𝑗 + 1)) +
(2↑(𝑗 +
1)))) |
| 161 | 160 | oveq1d 7446 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
((2↑((𝑗 + 1) + 1))
− 1) = (((2↑(𝑗 +
1)) + (2↑(𝑗 + 1)))
− 1)) |
| 162 | | 1cnd 11256 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → 1 ∈
ℂ) |
| 163 | 106, 106,
162 | addsubd 11641 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
(((2↑(𝑗 + 1)) +
(2↑(𝑗 + 1))) −
1) = (((2↑(𝑗 + 1))
− 1) + (2↑(𝑗 +
1)))) |
| 164 | 161, 163 | eqtrd 2777 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
((2↑((𝑗 + 1) + 1))
− 1) = (((2↑(𝑗 +
1)) − 1) + (2↑(𝑗
+ 1)))) |
| 165 | | uztrn 12896 |
. . . . . . . . . . . . . . . . 17
⊢
((((2↑((𝑗 + 1)
+ 1)) − 1) ∈ (ℤ≥‘((2↑(𝑗 + 1)) − 1)) ∧
((2↑(𝑗 + 1)) −
1) ∈ (ℤ≥‘1)) → ((2↑((𝑗 + 1) + 1)) − 1) ∈
(ℤ≥‘1)) |
| 166 | 146, 126,
165 | syl2anc 584 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
((2↑((𝑗 + 1) + 1))
− 1) ∈ (ℤ≥‘1)) |
| 167 | 166, 117 | eleqtrrdi 2852 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
((2↑((𝑗 + 1) + 1))
− 1) ∈ ℕ) |
| 168 | 167 | nnnn0d 12587 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
((2↑((𝑗 + 1) + 1))
− 1) ∈ ℕ0) |
| 169 | | hashfz1 14385 |
. . . . . . . . . . . . . 14
⊢
(((2↑((𝑗 + 1) +
1)) − 1) ∈ ℕ0 →
(♯‘(1...((2↑((𝑗 + 1) + 1)) − 1))) = ((2↑((𝑗 + 1) + 1)) −
1)) |
| 170 | 168, 169 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
(♯‘(1...((2↑((𝑗 + 1) + 1)) − 1))) = ((2↑((𝑗 + 1) + 1)) −
1)) |
| 171 | 125 | nnnn0d 12587 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
((2↑(𝑗 + 1)) −
1) ∈ ℕ0) |
| 172 | | hashfz1 14385 |
. . . . . . . . . . . . . . 15
⊢
(((2↑(𝑗 + 1))
− 1) ∈ ℕ0 →
(♯‘(1...((2↑(𝑗 + 1)) − 1))) = ((2↑(𝑗 + 1)) −
1)) |
| 173 | 171, 172 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
(♯‘(1...((2↑(𝑗 + 1)) − 1))) = ((2↑(𝑗 + 1)) −
1)) |
| 174 | 173 | oveq1d 7446 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
((♯‘(1...((2↑(𝑗 + 1)) − 1))) + (2↑(𝑗 + 1))) = (((2↑(𝑗 + 1)) − 1) +
(2↑(𝑗 +
1)))) |
| 175 | 164, 170,
174 | 3eqtr4d 2787 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
(♯‘(1...((2↑((𝑗 + 1) + 1)) − 1))) =
((♯‘(1...((2↑(𝑗 + 1)) − 1))) + (2↑(𝑗 + 1)))) |
| 176 | 105 | ltm1d 12200 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
((2↑(𝑗 + 1)) −
1) < (2↑(𝑗 +
1))) |
| 177 | | fzdisj 13591 |
. . . . . . . . . . . . . 14
⊢
(((2↑(𝑗 + 1))
− 1) < (2↑(𝑗
+ 1)) → ((1...((2↑(𝑗 + 1)) − 1)) ∩ ((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1))) =
∅) |
| 178 | 176, 177 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
((1...((2↑(𝑗 + 1))
− 1)) ∩ ((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1))) =
∅) |
| 179 | | hashun 14421 |
. . . . . . . . . . . . 13
⊢
(((1...((2↑(𝑗 +
1)) − 1)) ∈ Fin ∧ ((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1)) ∈ Fin ∧
((1...((2↑(𝑗 + 1))
− 1)) ∩ ((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1))) = ∅) →
(♯‘((1...((2↑(𝑗 + 1)) − 1)) ∪ ((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1)))) =
((♯‘(1...((2↑(𝑗 + 1)) − 1))) +
(♯‘((2↑(𝑗
+ 1))...((2↑((𝑗 + 1) +
1)) − 1))))) |
| 180 | 101, 67, 178, 179 | syl3anc 1373 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
(♯‘((1...((2↑(𝑗 + 1)) − 1)) ∪ ((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1)))) =
((♯‘(1...((2↑(𝑗 + 1)) − 1))) +
(♯‘((2↑(𝑗
+ 1))...((2↑((𝑗 + 1) +
1)) − 1))))) |
| 181 | 156, 175,
180 | 3eqtr3d 2785 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
((♯‘(1...((2↑(𝑗 + 1)) − 1))) + (2↑(𝑗 + 1))) =
((♯‘(1...((2↑(𝑗 + 1)) − 1))) +
(♯‘((2↑(𝑗
+ 1))...((2↑((𝑗 + 1) +
1)) − 1))))) |
| 182 | 104, 106,
109, 181 | addcanad 11466 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
(2↑(𝑗 + 1)) =
(♯‘((2↑(𝑗
+ 1))...((2↑((𝑗 + 1) +
1)) − 1)))) |
| 183 | 182 | oveq1d 7446 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
((2↑(𝑗 + 1)) ·
(𝐹‘(2↑(𝑗 + 1)))) =
((♯‘((2↑(𝑗
+ 1))...((2↑((𝑗 + 1) +
1)) − 1))) · (𝐹‘(2↑(𝑗 + 1))))) |
| 184 | | fveq2 6906 |
. . . . . . . . . . 11
⊢ (𝑛 = (𝑗 + 1) → (𝐺‘𝑛) = (𝐺‘(𝑗 + 1))) |
| 185 | | oveq2 7439 |
. . . . . . . . . . . 12
⊢ (𝑛 = (𝑗 + 1) → (2↑𝑛) = (2↑(𝑗 + 1))) |
| 186 | 185 | fveq2d 6910 |
. . . . . . . . . . . 12
⊢ (𝑛 = (𝑗 + 1) → (𝐹‘(2↑𝑛)) = (𝐹‘(2↑(𝑗 + 1)))) |
| 187 | 185, 186 | oveq12d 7449 |
. . . . . . . . . . 11
⊢ (𝑛 = (𝑗 + 1) → ((2↑𝑛) · (𝐹‘(2↑𝑛))) = ((2↑(𝑗 + 1)) · (𝐹‘(2↑(𝑗 + 1))))) |
| 188 | 184, 187 | eqeq12d 2753 |
. . . . . . . . . 10
⊢ (𝑛 = (𝑗 + 1) → ((𝐺‘𝑛) = ((2↑𝑛) · (𝐹‘(2↑𝑛))) ↔ (𝐺‘(𝑗 + 1)) = ((2↑(𝑗 + 1)) · (𝐹‘(2↑(𝑗 + 1)))))) |
| 189 | 61 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
∀𝑛 ∈
ℕ0 (𝐺‘𝑛) = ((2↑𝑛) · (𝐹‘(2↑𝑛)))) |
| 190 | 188, 189,
71 | rspcdva 3623 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → (𝐺‘(𝑗 + 1)) = ((2↑(𝑗 + 1)) · (𝐹‘(2↑(𝑗 + 1))))) |
| 191 | 81 | recnd 11289 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → (𝐹‘(2↑(𝑗 + 1))) ∈
ℂ) |
| 192 | | fsumconst 15826 |
. . . . . . . . . 10
⊢
((((2↑(𝑗 +
1))...((2↑((𝑗 + 1) +
1)) − 1)) ∈ Fin ∧ (𝐹‘(2↑(𝑗 + 1))) ∈ ℂ) → Σ𝑘 ∈ ((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1))(𝐹‘(2↑(𝑗 + 1))) =
((♯‘((2↑(𝑗
+ 1))...((2↑((𝑗 + 1) +
1)) − 1))) · (𝐹‘(2↑(𝑗 + 1))))) |
| 193 | 67, 191, 192 | syl2anc 584 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
Σ𝑘 ∈
((2↑(𝑗 +
1))...((2↑((𝑗 + 1) +
1)) − 1))(𝐹‘(2↑(𝑗 + 1))) = ((♯‘((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1)))
· (𝐹‘(2↑(𝑗 + 1))))) |
| 194 | 183, 190,
193 | 3eqtr4d 2787 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → (𝐺‘(𝑗 + 1)) = Σ𝑘 ∈ ((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1))(𝐹‘(2↑(𝑗 + 1)))) |
| 195 | 100, 194 | breqtrrd 5171 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
Σ𝑘 ∈
((2↑(𝑗 +
1))...((2↑((𝑗 + 1) +
1)) − 1))(𝐹‘𝑘) ≤ (𝐺‘(𝑗 + 1))) |
| 196 | | elfznn 13593 |
. . . . . . . . . 10
⊢ (𝑘 ∈ (1...((2↑(𝑗 + 1)) − 1)) → 𝑘 ∈
ℕ) |
| 197 | 68, 196, 39 | syl2an 596 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ0) ∧ 𝑘 ∈ (1...((2↑(𝑗 + 1)) − 1))) →
(𝐹‘𝑘) ∈ ℝ) |
| 198 | 101, 197 | fsumrecl 15770 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
Σ𝑘 ∈
(1...((2↑(𝑗 + 1))
− 1))(𝐹‘𝑘) ∈
ℝ) |
| 199 | 67, 77 | fsumrecl 15770 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
Σ𝑘 ∈
((2↑(𝑗 +
1))...((2↑((𝑗 + 1) +
1)) − 1))(𝐹‘𝑘) ∈ ℝ) |
| 200 | | nn0uz 12920 |
. . . . . . . . . 10
⊢
ℕ0 = (ℤ≥‘0) |
| 201 | | 0zd 12625 |
. . . . . . . . . 10
⊢ (𝜑 → 0 ∈
ℤ) |
| 202 | | simpr 484 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → 𝑛 ∈
ℕ0) |
| 203 | | nnexpcl 14115 |
. . . . . . . . . . . . . 14
⊢ ((2
∈ ℕ ∧ 𝑛
∈ ℕ0) → (2↑𝑛) ∈ ℕ) |
| 204 | 69, 202, 203 | sylancr 587 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) →
(2↑𝑛) ∈
ℕ) |
| 205 | 204 | nnred 12281 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) →
(2↑𝑛) ∈
ℝ) |
| 206 | | fveq2 6906 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = (2↑𝑛) → (𝐹‘𝑘) = (𝐹‘(2↑𝑛))) |
| 207 | 206 | eleq1d 2826 |
. . . . . . . . . . . . 13
⊢ (𝑘 = (2↑𝑛) → ((𝐹‘𝑘) ∈ ℝ ↔ (𝐹‘(2↑𝑛)) ∈ ℝ)) |
| 208 | 40 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) →
∀𝑘 ∈ ℕ
(𝐹‘𝑘) ∈ ℝ) |
| 209 | 207, 208,
204 | rspcdva 3623 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → (𝐹‘(2↑𝑛)) ∈
ℝ) |
| 210 | 205, 209 | remulcld 11291 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) →
((2↑𝑛) · (𝐹‘(2↑𝑛))) ∈
ℝ) |
| 211 | 60, 210 | eqeltrd 2841 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → (𝐺‘𝑛) ∈ ℝ) |
| 212 | 200, 201,
211 | serfre 14072 |
. . . . . . . . 9
⊢ (𝜑 → seq0( + , 𝐺):ℕ0⟶ℝ) |
| 213 | 212 | ffvelcdmda 7104 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → (seq0( +
, 𝐺)‘𝑗) ∈
ℝ) |
| 214 | 135, 81 | remulcld 11291 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
((2↑(𝑗 + 1)) ·
(𝐹‘(2↑(𝑗 + 1)))) ∈
ℝ) |
| 215 | 190, 214 | eqeltrd 2841 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → (𝐺‘(𝑗 + 1)) ∈ ℝ) |
| 216 | | le2add 11745 |
. . . . . . . 8
⊢
(((Σ𝑘 ∈
(1...((2↑(𝑗 + 1))
− 1))(𝐹‘𝑘) ∈ ℝ ∧
Σ𝑘 ∈
((2↑(𝑗 +
1))...((2↑((𝑗 + 1) +
1)) − 1))(𝐹‘𝑘) ∈ ℝ) ∧ ((seq0( + , 𝐺)‘𝑗) ∈ ℝ ∧ (𝐺‘(𝑗 + 1)) ∈ ℝ)) → ((Σ𝑘 ∈ (1...((2↑(𝑗 + 1)) − 1))(𝐹‘𝑘) ≤ (seq0( + , 𝐺)‘𝑗) ∧ Σ𝑘 ∈ ((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1))(𝐹‘𝑘) ≤ (𝐺‘(𝑗 + 1))) → (Σ𝑘 ∈ (1...((2↑(𝑗 + 1)) − 1))(𝐹‘𝑘) + Σ𝑘 ∈ ((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1))(𝐹‘𝑘)) ≤ ((seq0( + , 𝐺)‘𝑗) + (𝐺‘(𝑗 + 1))))) |
| 217 | 198, 199,
213, 215, 216 | syl22anc 839 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
((Σ𝑘 ∈
(1...((2↑(𝑗 + 1))
− 1))(𝐹‘𝑘) ≤ (seq0( + , 𝐺)‘𝑗) ∧ Σ𝑘 ∈ ((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1))(𝐹‘𝑘) ≤ (𝐺‘(𝑗 + 1))) → (Σ𝑘 ∈ (1...((2↑(𝑗 + 1)) − 1))(𝐹‘𝑘) + Σ𝑘 ∈ ((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1))(𝐹‘𝑘)) ≤ ((seq0( + , 𝐺)‘𝑗) + (𝐺‘(𝑗 + 1))))) |
| 218 | 195, 217 | mpan2d 694 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
(Σ𝑘 ∈
(1...((2↑(𝑗 + 1))
− 1))(𝐹‘𝑘) ≤ (seq0( + , 𝐺)‘𝑗) → (Σ𝑘 ∈ (1...((2↑(𝑗 + 1)) − 1))(𝐹‘𝑘) + Σ𝑘 ∈ ((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1))(𝐹‘𝑘)) ≤ ((seq0( + , 𝐺)‘𝑗) + (𝐺‘(𝑗 + 1))))) |
| 219 | | eqidd 2738 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ0) ∧ 𝑘 ∈ (1...((2↑(𝑗 + 1)) − 1))) →
(𝐹‘𝑘) = (𝐹‘𝑘)) |
| 220 | 39 | recnd 11289 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) ∈ ℂ) |
| 221 | 68, 196, 220 | syl2an 596 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ0) ∧ 𝑘 ∈ (1...((2↑(𝑗 + 1)) − 1))) →
(𝐹‘𝑘) ∈ ℂ) |
| 222 | 219, 126,
221 | fsumser 15766 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
Σ𝑘 ∈
(1...((2↑(𝑗 + 1))
− 1))(𝐹‘𝑘) = (seq1( + , 𝐹)‘((2↑(𝑗 + 1)) − 1))) |
| 223 | 222 | eqcomd 2743 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → (seq1( +
, 𝐹)‘((2↑(𝑗 + 1)) − 1)) =
Σ𝑘 ∈
(1...((2↑(𝑗 + 1))
− 1))(𝐹‘𝑘)) |
| 224 | 223 | breq1d 5153 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → ((seq1( +
, 𝐹)‘((2↑(𝑗 + 1)) − 1)) ≤ (seq0( +
, 𝐺)‘𝑗) ↔ Σ𝑘 ∈ (1...((2↑(𝑗 + 1)) − 1))(𝐹‘𝑘) ≤ (seq0( + , 𝐺)‘𝑗))) |
| 225 | | eqidd 2738 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ0) ∧ 𝑘 ∈ (1...((2↑((𝑗 + 1) + 1)) − 1))) →
(𝐹‘𝑘) = (𝐹‘𝑘)) |
| 226 | | elfznn 13593 |
. . . . . . . . . 10
⊢ (𝑘 ∈ (1...((2↑((𝑗 + 1) + 1)) − 1)) →
𝑘 ∈
ℕ) |
| 227 | 68, 226, 220 | syl2an 596 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ0) ∧ 𝑘 ∈ (1...((2↑((𝑗 + 1) + 1)) − 1))) →
(𝐹‘𝑘) ∈ ℂ) |
| 228 | 225, 166,
227 | fsumser 15766 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
Σ𝑘 ∈
(1...((2↑((𝑗 + 1) +
1)) − 1))(𝐹‘𝑘) = (seq1( + , 𝐹)‘((2↑((𝑗 + 1) + 1)) − 1))) |
| 229 | | fzfid 14014 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
(1...((2↑((𝑗 + 1) +
1)) − 1)) ∈ Fin) |
| 230 | 178, 155,
229, 227 | fsumsplit 15777 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
Σ𝑘 ∈
(1...((2↑((𝑗 + 1) +
1)) − 1))(𝐹‘𝑘) = (Σ𝑘 ∈ (1...((2↑(𝑗 + 1)) − 1))(𝐹‘𝑘) + Σ𝑘 ∈ ((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1))(𝐹‘𝑘))) |
| 231 | 228, 230 | eqtr3d 2779 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → (seq1( +
, 𝐹)‘((2↑((𝑗 + 1) + 1)) − 1)) =
(Σ𝑘 ∈
(1...((2↑(𝑗 + 1))
− 1))(𝐹‘𝑘) + Σ𝑘 ∈ ((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1))(𝐹‘𝑘))) |
| 232 | | simpr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → 𝑗 ∈
ℕ0) |
| 233 | 232, 200 | eleqtrdi 2851 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → 𝑗 ∈
(ℤ≥‘0)) |
| 234 | | seqp1 14057 |
. . . . . . . 8
⊢ (𝑗 ∈
(ℤ≥‘0) → (seq0( + , 𝐺)‘(𝑗 + 1)) = ((seq0( + , 𝐺)‘𝑗) + (𝐺‘(𝑗 + 1)))) |
| 235 | 233, 234 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → (seq0( +
, 𝐺)‘(𝑗 + 1)) = ((seq0( + , 𝐺)‘𝑗) + (𝐺‘(𝑗 + 1)))) |
| 236 | 231, 235 | breq12d 5156 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → ((seq1( +
, 𝐹)‘((2↑((𝑗 + 1) + 1)) − 1)) ≤
(seq0( + , 𝐺)‘(𝑗 + 1)) ↔ (Σ𝑘 ∈ (1...((2↑(𝑗 + 1)) − 1))(𝐹‘𝑘) + Σ𝑘 ∈ ((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1))(𝐹‘𝑘)) ≤ ((seq0( + , 𝐺)‘𝑗) + (𝐺‘(𝑗 + 1))))) |
| 237 | 218, 224,
236 | 3imtr4d 294 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → ((seq1( +
, 𝐹)‘((2↑(𝑗 + 1)) − 1)) ≤ (seq0( +
, 𝐺)‘𝑗) → (seq1( + , 𝐹)‘((2↑((𝑗 + 1) + 1)) − 1)) ≤
(seq0( + , 𝐺)‘(𝑗 + 1)))) |
| 238 | 237 | expcom 413 |
. . . 4
⊢ (𝑗 ∈ ℕ0
→ (𝜑 → ((seq1( + ,
𝐹)‘((2↑(𝑗 + 1)) − 1)) ≤ (seq0( +
, 𝐺)‘𝑗) → (seq1( + , 𝐹)‘((2↑((𝑗 + 1) + 1)) − 1)) ≤
(seq0( + , 𝐺)‘(𝑗 + 1))))) |
| 239 | 238 | a2d 29 |
. . 3
⊢ (𝑗 ∈ ℕ0
→ ((𝜑 → (seq1( + ,
𝐹)‘((2↑(𝑗 + 1)) − 1)) ≤ (seq0( +
, 𝐺)‘𝑗)) → (𝜑 → (seq1( + , 𝐹)‘((2↑((𝑗 + 1) + 1)) − 1)) ≤ (seq0( + , 𝐺)‘(𝑗 + 1))))) |
| 240 | 18, 24, 30, 36, 66, 239 | nn0ind 12713 |
. 2
⊢ (𝑁 ∈ ℕ0
→ (𝜑 → (seq1( + ,
𝐹)‘((2↑(𝑁 + 1)) − 1)) ≤ (seq0( +
, 𝐺)‘𝑁))) |
| 241 | 240 | impcom 407 |
1
⊢ ((𝜑 ∧ 𝑁 ∈ ℕ0) → (seq1( +
, 𝐹)‘((2↑(𝑁 + 1)) − 1)) ≤ (seq0( +
, 𝐺)‘𝑁)) |