Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  climcndslem1 Structured version   Visualization version   GIF version

Theorem climcndslem1 15198
 Description: Lemma for climcnds 15200: bound the original series by the condensed series. (Contributed by Mario Carneiro, 18-Jul-2014.)
Hypotheses
Ref Expression
climcnds.1 ((𝜑𝑘 ∈ ℕ) → (𝐹𝑘) ∈ ℝ)
climcnds.2 ((𝜑𝑘 ∈ ℕ) → 0 ≤ (𝐹𝑘))
climcnds.3 ((𝜑𝑘 ∈ ℕ) → (𝐹‘(𝑘 + 1)) ≤ (𝐹𝑘))
climcnds.4 ((𝜑𝑛 ∈ ℕ0) → (𝐺𝑛) = ((2↑𝑛) · (𝐹‘(2↑𝑛))))
Assertion
Ref Expression
climcndslem1 ((𝜑𝑁 ∈ ℕ0) → (seq1( + , 𝐹)‘((2↑(𝑁 + 1)) − 1)) ≤ (seq0( + , 𝐺)‘𝑁))
Distinct variable groups:   𝑘,𝑛,𝐹   𝑘,𝐺,𝑛   𝜑,𝑘,𝑛
Allowed substitution hints:   𝑁(𝑘,𝑛)

Proof of Theorem climcndslem1
Dummy variables 𝑗 𝑥 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 oveq1 7157 . . . . . . . . . . 11 (𝑥 = 0 → (𝑥 + 1) = (0 + 1))
2 0p1e1 11753 . . . . . . . . . . 11 (0 + 1) = 1
31, 2syl6eq 2872 . . . . . . . . . 10 (𝑥 = 0 → (𝑥 + 1) = 1)
43oveq2d 7166 . . . . . . . . 9 (𝑥 = 0 → (2↑(𝑥 + 1)) = (2↑1))
5 2cn 11706 . . . . . . . . . . 11 2 ∈ ℂ
6 exp1 13429 . . . . . . . . . . 11 (2 ∈ ℂ → (2↑1) = 2)
75, 6ax-mp 5 . . . . . . . . . 10 (2↑1) = 2
8 df-2 11694 . . . . . . . . . 10 2 = (1 + 1)
97, 8eqtri 2844 . . . . . . . . 9 (2↑1) = (1 + 1)
104, 9syl6eq 2872 . . . . . . . 8 (𝑥 = 0 → (2↑(𝑥 + 1)) = (1 + 1))
1110oveq1d 7165 . . . . . . 7 (𝑥 = 0 → ((2↑(𝑥 + 1)) − 1) = ((1 + 1) − 1))
12 ax-1cn 10589 . . . . . . . 8 1 ∈ ℂ
1312, 12pncan3oi 10896 . . . . . . 7 ((1 + 1) − 1) = 1
1411, 13syl6eq 2872 . . . . . 6 (𝑥 = 0 → ((2↑(𝑥 + 1)) − 1) = 1)
1514fveq2d 6669 . . . . 5 (𝑥 = 0 → (seq1( + , 𝐹)‘((2↑(𝑥 + 1)) − 1)) = (seq1( + , 𝐹)‘1))
16 fveq2 6665 . . . . 5 (𝑥 = 0 → (seq0( + , 𝐺)‘𝑥) = (seq0( + , 𝐺)‘0))
1715, 16breq12d 5072 . . . 4 (𝑥 = 0 → ((seq1( + , 𝐹)‘((2↑(𝑥 + 1)) − 1)) ≤ (seq0( + , 𝐺)‘𝑥) ↔ (seq1( + , 𝐹)‘1) ≤ (seq0( + , 𝐺)‘0)))
1817imbi2d 343 . . 3 (𝑥 = 0 → ((𝜑 → (seq1( + , 𝐹)‘((2↑(𝑥 + 1)) − 1)) ≤ (seq0( + , 𝐺)‘𝑥)) ↔ (𝜑 → (seq1( + , 𝐹)‘1) ≤ (seq0( + , 𝐺)‘0))))
19 oveq1 7157 . . . . . . 7 (𝑥 = 𝑗 → (𝑥 + 1) = (𝑗 + 1))
2019oveq2d 7166 . . . . . 6 (𝑥 = 𝑗 → (2↑(𝑥 + 1)) = (2↑(𝑗 + 1)))
2120fvoveq1d 7172 . . . . 5 (𝑥 = 𝑗 → (seq1( + , 𝐹)‘((2↑(𝑥 + 1)) − 1)) = (seq1( + , 𝐹)‘((2↑(𝑗 + 1)) − 1)))
22 fveq2 6665 . . . . 5 (𝑥 = 𝑗 → (seq0( + , 𝐺)‘𝑥) = (seq0( + , 𝐺)‘𝑗))
2321, 22breq12d 5072 . . . 4 (𝑥 = 𝑗 → ((seq1( + , 𝐹)‘((2↑(𝑥 + 1)) − 1)) ≤ (seq0( + , 𝐺)‘𝑥) ↔ (seq1( + , 𝐹)‘((2↑(𝑗 + 1)) − 1)) ≤ (seq0( + , 𝐺)‘𝑗)))
2423imbi2d 343 . . 3 (𝑥 = 𝑗 → ((𝜑 → (seq1( + , 𝐹)‘((2↑(𝑥 + 1)) − 1)) ≤ (seq0( + , 𝐺)‘𝑥)) ↔ (𝜑 → (seq1( + , 𝐹)‘((2↑(𝑗 + 1)) − 1)) ≤ (seq0( + , 𝐺)‘𝑗))))
25 oveq1 7157 . . . . . . 7 (𝑥 = (𝑗 + 1) → (𝑥 + 1) = ((𝑗 + 1) + 1))
2625oveq2d 7166 . . . . . 6 (𝑥 = (𝑗 + 1) → (2↑(𝑥 + 1)) = (2↑((𝑗 + 1) + 1)))
2726fvoveq1d 7172 . . . . 5 (𝑥 = (𝑗 + 1) → (seq1( + , 𝐹)‘((2↑(𝑥 + 1)) − 1)) = (seq1( + , 𝐹)‘((2↑((𝑗 + 1) + 1)) − 1)))
28 fveq2 6665 . . . . 5 (𝑥 = (𝑗 + 1) → (seq0( + , 𝐺)‘𝑥) = (seq0( + , 𝐺)‘(𝑗 + 1)))
2927, 28breq12d 5072 . . . 4 (𝑥 = (𝑗 + 1) → ((seq1( + , 𝐹)‘((2↑(𝑥 + 1)) − 1)) ≤ (seq0( + , 𝐺)‘𝑥) ↔ (seq1( + , 𝐹)‘((2↑((𝑗 + 1) + 1)) − 1)) ≤ (seq0( + , 𝐺)‘(𝑗 + 1))))
3029imbi2d 343 . . 3 (𝑥 = (𝑗 + 1) → ((𝜑 → (seq1( + , 𝐹)‘((2↑(𝑥 + 1)) − 1)) ≤ (seq0( + , 𝐺)‘𝑥)) ↔ (𝜑 → (seq1( + , 𝐹)‘((2↑((𝑗 + 1) + 1)) − 1)) ≤ (seq0( + , 𝐺)‘(𝑗 + 1)))))
31 oveq1 7157 . . . . . . 7 (𝑥 = 𝑁 → (𝑥 + 1) = (𝑁 + 1))
3231oveq2d 7166 . . . . . 6 (𝑥 = 𝑁 → (2↑(𝑥 + 1)) = (2↑(𝑁 + 1)))
3332fvoveq1d 7172 . . . . 5 (𝑥 = 𝑁 → (seq1( + , 𝐹)‘((2↑(𝑥 + 1)) − 1)) = (seq1( + , 𝐹)‘((2↑(𝑁 + 1)) − 1)))
34 fveq2 6665 . . . . 5 (𝑥 = 𝑁 → (seq0( + , 𝐺)‘𝑥) = (seq0( + , 𝐺)‘𝑁))
3533, 34breq12d 5072 . . . 4 (𝑥 = 𝑁 → ((seq1( + , 𝐹)‘((2↑(𝑥 + 1)) − 1)) ≤ (seq0( + , 𝐺)‘𝑥) ↔ (seq1( + , 𝐹)‘((2↑(𝑁 + 1)) − 1)) ≤ (seq0( + , 𝐺)‘𝑁)))
3635imbi2d 343 . . 3 (𝑥 = 𝑁 → ((𝜑 → (seq1( + , 𝐹)‘((2↑(𝑥 + 1)) − 1)) ≤ (seq0( + , 𝐺)‘𝑥)) ↔ (𝜑 → (seq1( + , 𝐹)‘((2↑(𝑁 + 1)) − 1)) ≤ (seq0( + , 𝐺)‘𝑁))))
37 fveq2 6665 . . . . . . . 8 (𝑘 = 1 → (𝐹𝑘) = (𝐹‘1))
3837eleq1d 2897 . . . . . . 7 (𝑘 = 1 → ((𝐹𝑘) ∈ ℝ ↔ (𝐹‘1) ∈ ℝ))
39 climcnds.1 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ) → (𝐹𝑘) ∈ ℝ)
4039ralrimiva 3182 . . . . . . 7 (𝜑 → ∀𝑘 ∈ ℕ (𝐹𝑘) ∈ ℝ)
41 1nn 11643 . . . . . . . 8 1 ∈ ℕ
4241a1i 11 . . . . . . 7 (𝜑 → 1 ∈ ℕ)
4338, 40, 42rspcdva 3625 . . . . . 6 (𝜑 → (𝐹‘1) ∈ ℝ)
4443leidd 11200 . . . . 5 (𝜑 → (𝐹‘1) ≤ (𝐹‘1))
4543recnd 10663 . . . . . 6 (𝜑 → (𝐹‘1) ∈ ℂ)
4645mulid2d 10653 . . . . 5 (𝜑 → (1 · (𝐹‘1)) = (𝐹‘1))
4744, 46breqtrrd 5087 . . . 4 (𝜑 → (𝐹‘1) ≤ (1 · (𝐹‘1)))
48 1z 12006 . . . . 5 1 ∈ ℤ
49 eqidd 2822 . . . . 5 (𝜑 → (𝐹‘1) = (𝐹‘1))
5048, 49seq1i 13377 . . . 4 (𝜑 → (seq1( + , 𝐹)‘1) = (𝐹‘1))
51 0z 11986 . . . . 5 0 ∈ ℤ
52 fveq2 6665 . . . . . . 7 (𝑛 = 0 → (𝐺𝑛) = (𝐺‘0))
53 oveq2 7158 . . . . . . . . 9 (𝑛 = 0 → (2↑𝑛) = (2↑0))
54 exp0 13427 . . . . . . . . . 10 (2 ∈ ℂ → (2↑0) = 1)
555, 54ax-mp 5 . . . . . . . . 9 (2↑0) = 1
5653, 55syl6eq 2872 . . . . . . . 8 (𝑛 = 0 → (2↑𝑛) = 1)
5756fveq2d 6669 . . . . . . . 8 (𝑛 = 0 → (𝐹‘(2↑𝑛)) = (𝐹‘1))
5856, 57oveq12d 7168 . . . . . . 7 (𝑛 = 0 → ((2↑𝑛) · (𝐹‘(2↑𝑛))) = (1 · (𝐹‘1)))
5952, 58eqeq12d 2837 . . . . . 6 (𝑛 = 0 → ((𝐺𝑛) = ((2↑𝑛) · (𝐹‘(2↑𝑛))) ↔ (𝐺‘0) = (1 · (𝐹‘1))))
60 climcnds.4 . . . . . . 7 ((𝜑𝑛 ∈ ℕ0) → (𝐺𝑛) = ((2↑𝑛) · (𝐹‘(2↑𝑛))))
6160ralrimiva 3182 . . . . . 6 (𝜑 → ∀𝑛 ∈ ℕ0 (𝐺𝑛) = ((2↑𝑛) · (𝐹‘(2↑𝑛))))
62 0nn0 11906 . . . . . . 7 0 ∈ ℕ0
6362a1i 11 . . . . . 6 (𝜑 → 0 ∈ ℕ0)
6459, 61, 63rspcdva 3625 . . . . 5 (𝜑 → (𝐺‘0) = (1 · (𝐹‘1)))
6551, 64seq1i 13377 . . . 4 (𝜑 → (seq0( + , 𝐺)‘0) = (1 · (𝐹‘1)))
6647, 50, 653brtr4d 5091 . . 3 (𝜑 → (seq1( + , 𝐹)‘1) ≤ (seq0( + , 𝐺)‘0))
67 fzfid 13335 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ0) → ((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1)) ∈ Fin)
68 simpl 485 . . . . . . . . . 10 ((𝜑𝑗 ∈ ℕ0) → 𝜑)
69 2nn 11704 . . . . . . . . . . . 12 2 ∈ ℕ
70 peano2nn0 11931 . . . . . . . . . . . . 13 (𝑗 ∈ ℕ0 → (𝑗 + 1) ∈ ℕ0)
7170adantl 484 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ0) → (𝑗 + 1) ∈ ℕ0)
72 nnexpcl 13436 . . . . . . . . . . . 12 ((2 ∈ ℕ ∧ (𝑗 + 1) ∈ ℕ0) → (2↑(𝑗 + 1)) ∈ ℕ)
7369, 71, 72sylancr 589 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ℕ0) → (2↑(𝑗 + 1)) ∈ ℕ)
74 elfzuz 12898 . . . . . . . . . . 11 (𝑘 ∈ ((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1)) → 𝑘 ∈ (ℤ‘(2↑(𝑗 + 1))))
75 eluznn 12312 . . . . . . . . . . 11 (((2↑(𝑗 + 1)) ∈ ℕ ∧ 𝑘 ∈ (ℤ‘(2↑(𝑗 + 1)))) → 𝑘 ∈ ℕ)
7673, 74, 75syl2an 597 . . . . . . . . . 10 (((𝜑𝑗 ∈ ℕ0) ∧ 𝑘 ∈ ((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1))) → 𝑘 ∈ ℕ)
7768, 76, 39syl2an2r 683 . . . . . . . . 9 (((𝜑𝑗 ∈ ℕ0) ∧ 𝑘 ∈ ((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1))) → (𝐹𝑘) ∈ ℝ)
78 fveq2 6665 . . . . . . . . . . . 12 (𝑘 = (2↑(𝑗 + 1)) → (𝐹𝑘) = (𝐹‘(2↑(𝑗 + 1))))
7978eleq1d 2897 . . . . . . . . . . 11 (𝑘 = (2↑(𝑗 + 1)) → ((𝐹𝑘) ∈ ℝ ↔ (𝐹‘(2↑(𝑗 + 1))) ∈ ℝ))
8040adantr 483 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ℕ0) → ∀𝑘 ∈ ℕ (𝐹𝑘) ∈ ℝ)
8179, 80, 73rspcdva 3625 . . . . . . . . . 10 ((𝜑𝑗 ∈ ℕ0) → (𝐹‘(2↑(𝑗 + 1))) ∈ ℝ)
8281adantr 483 . . . . . . . . 9 (((𝜑𝑗 ∈ ℕ0) ∧ 𝑘 ∈ ((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1))) → (𝐹‘(2↑(𝑗 + 1))) ∈ ℝ)
83 simpr 487 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ ℕ0) ∧ 𝑛 ∈ (ℤ‘(2↑(𝑗 + 1)))) → 𝑛 ∈ (ℤ‘(2↑(𝑗 + 1))))
84 simplll 773 . . . . . . . . . . . . 13 ((((𝜑𝑗 ∈ ℕ0) ∧ 𝑛 ∈ (ℤ‘(2↑(𝑗 + 1)))) ∧ 𝑘 ∈ ((2↑(𝑗 + 1))...𝑛)) → 𝜑)
8573adantr 483 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ ℕ0) ∧ 𝑛 ∈ (ℤ‘(2↑(𝑗 + 1)))) → (2↑(𝑗 + 1)) ∈ ℕ)
86 elfzuz 12898 . . . . . . . . . . . . . 14 (𝑘 ∈ ((2↑(𝑗 + 1))...𝑛) → 𝑘 ∈ (ℤ‘(2↑(𝑗 + 1))))
8785, 86, 75syl2an 597 . . . . . . . . . . . . 13 ((((𝜑𝑗 ∈ ℕ0) ∧ 𝑛 ∈ (ℤ‘(2↑(𝑗 + 1)))) ∧ 𝑘 ∈ ((2↑(𝑗 + 1))...𝑛)) → 𝑘 ∈ ℕ)
8884, 87, 39syl2anc 586 . . . . . . . . . . . 12 ((((𝜑𝑗 ∈ ℕ0) ∧ 𝑛 ∈ (ℤ‘(2↑(𝑗 + 1)))) ∧ 𝑘 ∈ ((2↑(𝑗 + 1))...𝑛)) → (𝐹𝑘) ∈ ℝ)
89 simplll 773 . . . . . . . . . . . . 13 ((((𝜑𝑗 ∈ ℕ0) ∧ 𝑛 ∈ (ℤ‘(2↑(𝑗 + 1)))) ∧ 𝑘 ∈ ((2↑(𝑗 + 1))...(𝑛 − 1))) → 𝜑)
90 elfzuz 12898 . . . . . . . . . . . . . 14 (𝑘 ∈ ((2↑(𝑗 + 1))...(𝑛 − 1)) → 𝑘 ∈ (ℤ‘(2↑(𝑗 + 1))))
9185, 90, 75syl2an 597 . . . . . . . . . . . . 13 ((((𝜑𝑗 ∈ ℕ0) ∧ 𝑛 ∈ (ℤ‘(2↑(𝑗 + 1)))) ∧ 𝑘 ∈ ((2↑(𝑗 + 1))...(𝑛 − 1))) → 𝑘 ∈ ℕ)
92 climcnds.3 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ) → (𝐹‘(𝑘 + 1)) ≤ (𝐹𝑘))
9389, 91, 92syl2anc 586 . . . . . . . . . . . 12 ((((𝜑𝑗 ∈ ℕ0) ∧ 𝑛 ∈ (ℤ‘(2↑(𝑗 + 1)))) ∧ 𝑘 ∈ ((2↑(𝑗 + 1))...(𝑛 − 1))) → (𝐹‘(𝑘 + 1)) ≤ (𝐹𝑘))
9483, 88, 93monoord2 13395 . . . . . . . . . . 11 (((𝜑𝑗 ∈ ℕ0) ∧ 𝑛 ∈ (ℤ‘(2↑(𝑗 + 1)))) → (𝐹𝑛) ≤ (𝐹‘(2↑(𝑗 + 1))))
9594ralrimiva 3182 . . . . . . . . . 10 ((𝜑𝑗 ∈ ℕ0) → ∀𝑛 ∈ (ℤ‘(2↑(𝑗 + 1)))(𝐹𝑛) ≤ (𝐹‘(2↑(𝑗 + 1))))
96 fveq2 6665 . . . . . . . . . . . 12 (𝑛 = 𝑘 → (𝐹𝑛) = (𝐹𝑘))
9796breq1d 5069 . . . . . . . . . . 11 (𝑛 = 𝑘 → ((𝐹𝑛) ≤ (𝐹‘(2↑(𝑗 + 1))) ↔ (𝐹𝑘) ≤ (𝐹‘(2↑(𝑗 + 1)))))
9897rspccva 3622 . . . . . . . . . 10 ((∀𝑛 ∈ (ℤ‘(2↑(𝑗 + 1)))(𝐹𝑛) ≤ (𝐹‘(2↑(𝑗 + 1))) ∧ 𝑘 ∈ (ℤ‘(2↑(𝑗 + 1)))) → (𝐹𝑘) ≤ (𝐹‘(2↑(𝑗 + 1))))
9995, 74, 98syl2an 597 . . . . . . . . 9 (((𝜑𝑗 ∈ ℕ0) ∧ 𝑘 ∈ ((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1))) → (𝐹𝑘) ≤ (𝐹‘(2↑(𝑗 + 1))))
10067, 77, 82, 99fsumle 15148 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ0) → Σ𝑘 ∈ ((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1))(𝐹𝑘) ≤ Σ𝑘 ∈ ((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1))(𝐹‘(2↑(𝑗 + 1))))
101 fzfid 13335 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ ℕ0) → (1...((2↑(𝑗 + 1)) − 1)) ∈ Fin)
102 hashcl 13711 . . . . . . . . . . . . 13 ((1...((2↑(𝑗 + 1)) − 1)) ∈ Fin → (♯‘(1...((2↑(𝑗 + 1)) − 1))) ∈ ℕ0)
103101, 102syl 17 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ0) → (♯‘(1...((2↑(𝑗 + 1)) − 1))) ∈ ℕ0)
104103nn0cnd 11951 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ℕ0) → (♯‘(1...((2↑(𝑗 + 1)) − 1))) ∈ ℂ)
10573nnred 11647 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ0) → (2↑(𝑗 + 1)) ∈ ℝ)
106105recnd 10663 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ℕ0) → (2↑(𝑗 + 1)) ∈ ℂ)
107 hashcl 13711 . . . . . . . . . . . . 13 (((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1)) ∈ Fin → (♯‘((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1))) ∈ ℕ0)
10867, 107syl 17 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ0) → (♯‘((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1))) ∈ ℕ0)
109108nn0cnd 11951 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ℕ0) → (♯‘((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1))) ∈ ℂ)
110 2z 12008 . . . . . . . . . . . . . . . . . . . 20 2 ∈ ℤ
111 zexpcl 13438 . . . . . . . . . . . . . . . . . . . 20 ((2 ∈ ℤ ∧ (𝑗 + 1) ∈ ℕ0) → (2↑(𝑗 + 1)) ∈ ℤ)
112110, 71, 111sylancr 589 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ ℕ0) → (2↑(𝑗 + 1)) ∈ ℤ)
113 2re 11705 . . . . . . . . . . . . . . . . . . . . 21 2 ∈ ℝ
114 1le2 11840 . . . . . . . . . . . . . . . . . . . . 21 1 ≤ 2
115 nn0p1nn 11930 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 ∈ ℕ0 → (𝑗 + 1) ∈ ℕ)
116115adantl 484 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑗 ∈ ℕ0) → (𝑗 + 1) ∈ ℕ)
117 nnuz 12275 . . . . . . . . . . . . . . . . . . . . . 22 ℕ = (ℤ‘1)
118116, 117eleqtrdi 2923 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗 ∈ ℕ0) → (𝑗 + 1) ∈ (ℤ‘1))
119 leexp2a 13530 . . . . . . . . . . . . . . . . . . . . 21 ((2 ∈ ℝ ∧ 1 ≤ 2 ∧ (𝑗 + 1) ∈ (ℤ‘1)) → (2↑1) ≤ (2↑(𝑗 + 1)))
120113, 114, 118, 119mp3an12i 1461 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ ℕ0) → (2↑1) ≤ (2↑(𝑗 + 1)))
1217, 120eqbrtrrid 5095 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ ℕ0) → 2 ≤ (2↑(𝑗 + 1)))
122110eluz1i 12245 . . . . . . . . . . . . . . . . . . 19 ((2↑(𝑗 + 1)) ∈ (ℤ‘2) ↔ ((2↑(𝑗 + 1)) ∈ ℤ ∧ 2 ≤ (2↑(𝑗 + 1))))
123112, 121, 122sylanbrc 585 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ ℕ0) → (2↑(𝑗 + 1)) ∈ (ℤ‘2))
124 uz2m1nn 12317 . . . . . . . . . . . . . . . . . 18 ((2↑(𝑗 + 1)) ∈ (ℤ‘2) → ((2↑(𝑗 + 1)) − 1) ∈ ℕ)
125123, 124syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ ℕ0) → ((2↑(𝑗 + 1)) − 1) ∈ ℕ)
126125, 117eleqtrdi 2923 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ ℕ0) → ((2↑(𝑗 + 1)) − 1) ∈ (ℤ‘1))
127 peano2zm 12019 . . . . . . . . . . . . . . . . . 18 ((2↑(𝑗 + 1)) ∈ ℤ → ((2↑(𝑗 + 1)) − 1) ∈ ℤ)
128112, 127syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ ℕ0) → ((2↑(𝑗 + 1)) − 1) ∈ ℤ)
129 peano2nn0 11931 . . . . . . . . . . . . . . . . . . . 20 ((𝑗 + 1) ∈ ℕ0 → ((𝑗 + 1) + 1) ∈ ℕ0)
13071, 129syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ ℕ0) → ((𝑗 + 1) + 1) ∈ ℕ0)
131 zexpcl 13438 . . . . . . . . . . . . . . . . . . 19 ((2 ∈ ℤ ∧ ((𝑗 + 1) + 1) ∈ ℕ0) → (2↑((𝑗 + 1) + 1)) ∈ ℤ)
132110, 130, 131sylancr 589 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ ℕ0) → (2↑((𝑗 + 1) + 1)) ∈ ℤ)
133 peano2zm 12019 . . . . . . . . . . . . . . . . . 18 ((2↑((𝑗 + 1) + 1)) ∈ ℤ → ((2↑((𝑗 + 1) + 1)) − 1) ∈ ℤ)
134132, 133syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ ℕ0) → ((2↑((𝑗 + 1) + 1)) − 1) ∈ ℤ)
135112zred 12081 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ ℕ0) → (2↑(𝑗 + 1)) ∈ ℝ)
136132zred 12081 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ ℕ0) → (2↑((𝑗 + 1) + 1)) ∈ ℝ)
137 1red 10636 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ ℕ0) → 1 ∈ ℝ)
13871nn0zd 12079 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ ℕ0) → (𝑗 + 1) ∈ ℤ)
139 uzid 12252 . . . . . . . . . . . . . . . . . . 19 ((𝑗 + 1) ∈ ℤ → (𝑗 + 1) ∈ (ℤ‘(𝑗 + 1)))
140 peano2uz 12295 . . . . . . . . . . . . . . . . . . 19 ((𝑗 + 1) ∈ (ℤ‘(𝑗 + 1)) → ((𝑗 + 1) + 1) ∈ (ℤ‘(𝑗 + 1)))
141 leexp2a 13530 . . . . . . . . . . . . . . . . . . . 20 ((2 ∈ ℝ ∧ 1 ≤ 2 ∧ ((𝑗 + 1) + 1) ∈ (ℤ‘(𝑗 + 1))) → (2↑(𝑗 + 1)) ≤ (2↑((𝑗 + 1) + 1)))
142113, 114, 141mp3an12 1447 . . . . . . . . . . . . . . . . . . 19 (((𝑗 + 1) + 1) ∈ (ℤ‘(𝑗 + 1)) → (2↑(𝑗 + 1)) ≤ (2↑((𝑗 + 1) + 1)))
143138, 139, 140, 1424syl 19 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ ℕ0) → (2↑(𝑗 + 1)) ≤ (2↑((𝑗 + 1) + 1)))
144135, 136, 137, 143lesub1dd 11250 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ ℕ0) → ((2↑(𝑗 + 1)) − 1) ≤ ((2↑((𝑗 + 1) + 1)) − 1))
145 eluz2 12243 . . . . . . . . . . . . . . . . 17 (((2↑((𝑗 + 1) + 1)) − 1) ∈ (ℤ‘((2↑(𝑗 + 1)) − 1)) ↔ (((2↑(𝑗 + 1)) − 1) ∈ ℤ ∧ ((2↑((𝑗 + 1) + 1)) − 1) ∈ ℤ ∧ ((2↑(𝑗 + 1)) − 1) ≤ ((2↑((𝑗 + 1) + 1)) − 1)))
146128, 134, 144, 145syl3anbrc 1339 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ ℕ0) → ((2↑((𝑗 + 1) + 1)) − 1) ∈ (ℤ‘((2↑(𝑗 + 1)) − 1)))
147 elfzuzb 12896 . . . . . . . . . . . . . . . 16 (((2↑(𝑗 + 1)) − 1) ∈ (1...((2↑((𝑗 + 1) + 1)) − 1)) ↔ (((2↑(𝑗 + 1)) − 1) ∈ (ℤ‘1) ∧ ((2↑((𝑗 + 1) + 1)) − 1) ∈ (ℤ‘((2↑(𝑗 + 1)) − 1))))
148126, 146, 147sylanbrc 585 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ ℕ0) → ((2↑(𝑗 + 1)) − 1) ∈ (1...((2↑((𝑗 + 1) + 1)) − 1)))
149 fzsplit 12927 . . . . . . . . . . . . . . 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))))
150148, 149syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ ℕ0) → (1...((2↑((𝑗 + 1) + 1)) − 1)) = ((1...((2↑(𝑗 + 1)) − 1)) ∪ ((((2↑(𝑗 + 1)) − 1) + 1)...((2↑((𝑗 + 1) + 1)) − 1))))
151 npcan 10889 . . . . . . . . . . . . . . . . 17 (((2↑(𝑗 + 1)) ∈ ℂ ∧ 1 ∈ ℂ) → (((2↑(𝑗 + 1)) − 1) + 1) = (2↑(𝑗 + 1)))
152106, 12, 151sylancl 588 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ ℕ0) → (((2↑(𝑗 + 1)) − 1) + 1) = (2↑(𝑗 + 1)))
153152oveq1d 7165 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ ℕ0) → ((((2↑(𝑗 + 1)) − 1) + 1)...((2↑((𝑗 + 1) + 1)) − 1)) = ((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1)))
154153uneq2d 4139 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ ℕ0) → ((1...((2↑(𝑗 + 1)) − 1)) ∪ ((((2↑(𝑗 + 1)) − 1) + 1)...((2↑((𝑗 + 1) + 1)) − 1))) = ((1...((2↑(𝑗 + 1)) − 1)) ∪ ((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1))))
155150, 154eqtrd 2856 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ ℕ0) → (1...((2↑((𝑗 + 1) + 1)) − 1)) = ((1...((2↑(𝑗 + 1)) − 1)) ∪ ((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1))))
156155fveq2d 6669 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ0) → (♯‘(1...((2↑((𝑗 + 1) + 1)) − 1))) = (♯‘((1...((2↑(𝑗 + 1)) − 1)) ∪ ((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1)))))
157 expp1 13430 . . . . . . . . . . . . . . . . 17 ((2 ∈ ℂ ∧ (𝑗 + 1) ∈ ℕ0) → (2↑((𝑗 + 1) + 1)) = ((2↑(𝑗 + 1)) · 2))
1585, 71, 157sylancr 589 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ ℕ0) → (2↑((𝑗 + 1) + 1)) = ((2↑(𝑗 + 1)) · 2))
159106times2d 11875 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ ℕ0) → ((2↑(𝑗 + 1)) · 2) = ((2↑(𝑗 + 1)) + (2↑(𝑗 + 1))))
160158, 159eqtrd 2856 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ ℕ0) → (2↑((𝑗 + 1) + 1)) = ((2↑(𝑗 + 1)) + (2↑(𝑗 + 1))))
161160oveq1d 7165 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ ℕ0) → ((2↑((𝑗 + 1) + 1)) − 1) = (((2↑(𝑗 + 1)) + (2↑(𝑗 + 1))) − 1))
162 1cnd 10630 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ ℕ0) → 1 ∈ ℂ)
163106, 106, 162addsubd 11012 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ ℕ0) → (((2↑(𝑗 + 1)) + (2↑(𝑗 + 1))) − 1) = (((2↑(𝑗 + 1)) − 1) + (2↑(𝑗 + 1))))
164161, 163eqtrd 2856 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ ℕ0) → ((2↑((𝑗 + 1) + 1)) − 1) = (((2↑(𝑗 + 1)) − 1) + (2↑(𝑗 + 1))))
165 uztrn 12255 . . . . . . . . . . . . . . . . 17 ((((2↑((𝑗 + 1) + 1)) − 1) ∈ (ℤ‘((2↑(𝑗 + 1)) − 1)) ∧ ((2↑(𝑗 + 1)) − 1) ∈ (ℤ‘1)) → ((2↑((𝑗 + 1) + 1)) − 1) ∈ (ℤ‘1))
166146, 126, 165syl2anc 586 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ ℕ0) → ((2↑((𝑗 + 1) + 1)) − 1) ∈ (ℤ‘1))
167166, 117eleqtrrdi 2924 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ ℕ0) → ((2↑((𝑗 + 1) + 1)) − 1) ∈ ℕ)
168167nnnn0d 11949 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ ℕ0) → ((2↑((𝑗 + 1) + 1)) − 1) ∈ ℕ0)
169 hashfz1 13700 . . . . . . . . . . . . . 14 (((2↑((𝑗 + 1) + 1)) − 1) ∈ ℕ0 → (♯‘(1...((2↑((𝑗 + 1) + 1)) − 1))) = ((2↑((𝑗 + 1) + 1)) − 1))
170168, 169syl 17 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ ℕ0) → (♯‘(1...((2↑((𝑗 + 1) + 1)) − 1))) = ((2↑((𝑗 + 1) + 1)) − 1))
171125nnnn0d 11949 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ ℕ0) → ((2↑(𝑗 + 1)) − 1) ∈ ℕ0)
172 hashfz1 13700 . . . . . . . . . . . . . . 15 (((2↑(𝑗 + 1)) − 1) ∈ ℕ0 → (♯‘(1...((2↑(𝑗 + 1)) − 1))) = ((2↑(𝑗 + 1)) − 1))
173171, 172syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ ℕ0) → (♯‘(1...((2↑(𝑗 + 1)) − 1))) = ((2↑(𝑗 + 1)) − 1))
174173oveq1d 7165 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ ℕ0) → ((♯‘(1...((2↑(𝑗 + 1)) − 1))) + (2↑(𝑗 + 1))) = (((2↑(𝑗 + 1)) − 1) + (2↑(𝑗 + 1))))
175164, 170, 1743eqtr4d 2866 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ0) → (♯‘(1...((2↑((𝑗 + 1) + 1)) − 1))) = ((♯‘(1...((2↑(𝑗 + 1)) − 1))) + (2↑(𝑗 + 1))))
176105ltm1d 11566 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ ℕ0) → ((2↑(𝑗 + 1)) − 1) < (2↑(𝑗 + 1)))
177 fzdisj 12928 . . . . . . . . . . . . . 14 (((2↑(𝑗 + 1)) − 1) < (2↑(𝑗 + 1)) → ((1...((2↑(𝑗 + 1)) − 1)) ∩ ((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1))) = ∅)
178176, 177syl 17 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ ℕ0) → ((1...((2↑(𝑗 + 1)) − 1)) ∩ ((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1))) = ∅)
179 hashun 13737 . . . . . . . . . . . . 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)))))
180101, 67, 178, 179syl3anc 1367 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ0) → (♯‘((1...((2↑(𝑗 + 1)) − 1)) ∪ ((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1)))) = ((♯‘(1...((2↑(𝑗 + 1)) − 1))) + (♯‘((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1)))))
181156, 175, 1803eqtr3d 2864 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ℕ0) → ((♯‘(1...((2↑(𝑗 + 1)) − 1))) + (2↑(𝑗 + 1))) = ((♯‘(1...((2↑(𝑗 + 1)) − 1))) + (♯‘((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1)))))
182104, 106, 109, 181addcanad 10839 . . . . . . . . . 10 ((𝜑𝑗 ∈ ℕ0) → (2↑(𝑗 + 1)) = (♯‘((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1))))
183182oveq1d 7165 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ0) → ((2↑(𝑗 + 1)) · (𝐹‘(2↑(𝑗 + 1)))) = ((♯‘((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1))) · (𝐹‘(2↑(𝑗 + 1)))))
184 fveq2 6665 . . . . . . . . . . 11 (𝑛 = (𝑗 + 1) → (𝐺𝑛) = (𝐺‘(𝑗 + 1)))
185 oveq2 7158 . . . . . . . . . . . 12 (𝑛 = (𝑗 + 1) → (2↑𝑛) = (2↑(𝑗 + 1)))
186185fveq2d 6669 . . . . . . . . . . . 12 (𝑛 = (𝑗 + 1) → (𝐹‘(2↑𝑛)) = (𝐹‘(2↑(𝑗 + 1))))
187185, 186oveq12d 7168 . . . . . . . . . . 11 (𝑛 = (𝑗 + 1) → ((2↑𝑛) · (𝐹‘(2↑𝑛))) = ((2↑(𝑗 + 1)) · (𝐹‘(2↑(𝑗 + 1)))))
188184, 187eqeq12d 2837 . . . . . . . . . 10 (𝑛 = (𝑗 + 1) → ((𝐺𝑛) = ((2↑𝑛) · (𝐹‘(2↑𝑛))) ↔ (𝐺‘(𝑗 + 1)) = ((2↑(𝑗 + 1)) · (𝐹‘(2↑(𝑗 + 1))))))
18961adantr 483 . . . . . . . . . 10 ((𝜑𝑗 ∈ ℕ0) → ∀𝑛 ∈ ℕ0 (𝐺𝑛) = ((2↑𝑛) · (𝐹‘(2↑𝑛))))
190188, 189, 71rspcdva 3625 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ0) → (𝐺‘(𝑗 + 1)) = ((2↑(𝑗 + 1)) · (𝐹‘(2↑(𝑗 + 1)))))
19181recnd 10663 . . . . . . . . . 10 ((𝜑𝑗 ∈ ℕ0) → (𝐹‘(2↑(𝑗 + 1))) ∈ ℂ)
192 fsumconst 15139 . . . . . . . . . 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)))))
19367, 191, 192syl2anc 586 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ0) → Σ𝑘 ∈ ((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1))(𝐹‘(2↑(𝑗 + 1))) = ((♯‘((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1))) · (𝐹‘(2↑(𝑗 + 1)))))
194183, 190, 1933eqtr4d 2866 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ0) → (𝐺‘(𝑗 + 1)) = Σ𝑘 ∈ ((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1))(𝐹‘(2↑(𝑗 + 1))))
195100, 194breqtrrd 5087 . . . . . . 7 ((𝜑𝑗 ∈ ℕ0) → Σ𝑘 ∈ ((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1))(𝐹𝑘) ≤ (𝐺‘(𝑗 + 1)))
196 elfznn 12930 . . . . . . . . . 10 (𝑘 ∈ (1...((2↑(𝑗 + 1)) − 1)) → 𝑘 ∈ ℕ)
19768, 196, 39syl2an 597 . . . . . . . . 9 (((𝜑𝑗 ∈ ℕ0) ∧ 𝑘 ∈ (1...((2↑(𝑗 + 1)) − 1))) → (𝐹𝑘) ∈ ℝ)
198101, 197fsumrecl 15085 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ0) → Σ𝑘 ∈ (1...((2↑(𝑗 + 1)) − 1))(𝐹𝑘) ∈ ℝ)
19967, 77fsumrecl 15085 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ0) → Σ𝑘 ∈ ((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1))(𝐹𝑘) ∈ ℝ)
200 nn0uz 12274 . . . . . . . . . 10 0 = (ℤ‘0)
201 0zd 11987 . . . . . . . . . 10 (𝜑 → 0 ∈ ℤ)
202 simpr 487 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ ℕ0) → 𝑛 ∈ ℕ0)
203 nnexpcl 13436 . . . . . . . . . . . . . 14 ((2 ∈ ℕ ∧ 𝑛 ∈ ℕ0) → (2↑𝑛) ∈ ℕ)
20469, 202, 203sylancr 589 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ ℕ0) → (2↑𝑛) ∈ ℕ)
205204nnred 11647 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ0) → (2↑𝑛) ∈ ℝ)
206 fveq2 6665 . . . . . . . . . . . . . 14 (𝑘 = (2↑𝑛) → (𝐹𝑘) = (𝐹‘(2↑𝑛)))
207206eleq1d 2897 . . . . . . . . . . . . 13 (𝑘 = (2↑𝑛) → ((𝐹𝑘) ∈ ℝ ↔ (𝐹‘(2↑𝑛)) ∈ ℝ))
20840adantr 483 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ ℕ0) → ∀𝑘 ∈ ℕ (𝐹𝑘) ∈ ℝ)
209207, 208, 204rspcdva 3625 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ0) → (𝐹‘(2↑𝑛)) ∈ ℝ)
210205, 209remulcld 10665 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ0) → ((2↑𝑛) · (𝐹‘(2↑𝑛))) ∈ ℝ)
21160, 210eqeltrd 2913 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ0) → (𝐺𝑛) ∈ ℝ)
212200, 201, 211serfre 13393 . . . . . . . . 9 (𝜑 → seq0( + , 𝐺):ℕ0⟶ℝ)
213212ffvelrnda 6846 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ0) → (seq0( + , 𝐺)‘𝑗) ∈ ℝ)
214135, 81remulcld 10665 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ0) → ((2↑(𝑗 + 1)) · (𝐹‘(2↑(𝑗 + 1)))) ∈ ℝ)
215190, 214eqeltrd 2913 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ0) → (𝐺‘(𝑗 + 1)) ∈ ℝ)
216 le2add 11116 . . . . . . . 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)))))
217198, 199, 213, 215, 216syl22anc 836 . . . . . . 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)))))
218195, 217mpan2d 692 . . . . . 6 ((𝜑𝑗 ∈ ℕ0) → (Σ𝑘 ∈ (1...((2↑(𝑗 + 1)) − 1))(𝐹𝑘) ≤ (seq0( + , 𝐺)‘𝑗) → (Σ𝑘 ∈ (1...((2↑(𝑗 + 1)) − 1))(𝐹𝑘) + Σ𝑘 ∈ ((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1))(𝐹𝑘)) ≤ ((seq0( + , 𝐺)‘𝑗) + (𝐺‘(𝑗 + 1)))))
219 eqidd 2822 . . . . . . . . 9 (((𝜑𝑗 ∈ ℕ0) ∧ 𝑘 ∈ (1...((2↑(𝑗 + 1)) − 1))) → (𝐹𝑘) = (𝐹𝑘))
22039recnd 10663 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ) → (𝐹𝑘) ∈ ℂ)
22168, 196, 220syl2an 597 . . . . . . . . 9 (((𝜑𝑗 ∈ ℕ0) ∧ 𝑘 ∈ (1...((2↑(𝑗 + 1)) − 1))) → (𝐹𝑘) ∈ ℂ)
222219, 126, 221fsumser 15081 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ0) → Σ𝑘 ∈ (1...((2↑(𝑗 + 1)) − 1))(𝐹𝑘) = (seq1( + , 𝐹)‘((2↑(𝑗 + 1)) − 1)))
223222eqcomd 2827 . . . . . . 7 ((𝜑𝑗 ∈ ℕ0) → (seq1( + , 𝐹)‘((2↑(𝑗 + 1)) − 1)) = Σ𝑘 ∈ (1...((2↑(𝑗 + 1)) − 1))(𝐹𝑘))
224223breq1d 5069 . . . . . 6 ((𝜑𝑗 ∈ ℕ0) → ((seq1( + , 𝐹)‘((2↑(𝑗 + 1)) − 1)) ≤ (seq0( + , 𝐺)‘𝑗) ↔ Σ𝑘 ∈ (1...((2↑(𝑗 + 1)) − 1))(𝐹𝑘) ≤ (seq0( + , 𝐺)‘𝑗)))
225 eqidd 2822 . . . . . . . . 9 (((𝜑𝑗 ∈ ℕ0) ∧ 𝑘 ∈ (1...((2↑((𝑗 + 1) + 1)) − 1))) → (𝐹𝑘) = (𝐹𝑘))
226 elfznn 12930 . . . . . . . . . 10 (𝑘 ∈ (1...((2↑((𝑗 + 1) + 1)) − 1)) → 𝑘 ∈ ℕ)
22768, 226, 220syl2an 597 . . . . . . . . 9 (((𝜑𝑗 ∈ ℕ0) ∧ 𝑘 ∈ (1...((2↑((𝑗 + 1) + 1)) − 1))) → (𝐹𝑘) ∈ ℂ)
228225, 166, 227fsumser 15081 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ0) → Σ𝑘 ∈ (1...((2↑((𝑗 + 1) + 1)) − 1))(𝐹𝑘) = (seq1( + , 𝐹)‘((2↑((𝑗 + 1) + 1)) − 1)))
229 fzfid 13335 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ0) → (1...((2↑((𝑗 + 1) + 1)) − 1)) ∈ Fin)
230178, 155, 229, 227fsumsplit 15091 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ0) → Σ𝑘 ∈ (1...((2↑((𝑗 + 1) + 1)) − 1))(𝐹𝑘) = (Σ𝑘 ∈ (1...((2↑(𝑗 + 1)) − 1))(𝐹𝑘) + Σ𝑘 ∈ ((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1))(𝐹𝑘)))
231228, 230eqtr3d 2858 . . . . . . 7 ((𝜑𝑗 ∈ ℕ0) → (seq1( + , 𝐹)‘((2↑((𝑗 + 1) + 1)) − 1)) = (Σ𝑘 ∈ (1...((2↑(𝑗 + 1)) − 1))(𝐹𝑘) + Σ𝑘 ∈ ((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1))(𝐹𝑘)))
232 simpr 487 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ0) → 𝑗 ∈ ℕ0)
233232, 200eleqtrdi 2923 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ0) → 𝑗 ∈ (ℤ‘0))
234 seqp1 13378 . . . . . . . 8 (𝑗 ∈ (ℤ‘0) → (seq0( + , 𝐺)‘(𝑗 + 1)) = ((seq0( + , 𝐺)‘𝑗) + (𝐺‘(𝑗 + 1))))
235233, 234syl 17 . . . . . . 7 ((𝜑𝑗 ∈ ℕ0) → (seq0( + , 𝐺)‘(𝑗 + 1)) = ((seq0( + , 𝐺)‘𝑗) + (𝐺‘(𝑗 + 1))))
236231, 235breq12d 5072 . . . . . 6 ((𝜑𝑗 ∈ ℕ0) → ((seq1( + , 𝐹)‘((2↑((𝑗 + 1) + 1)) − 1)) ≤ (seq0( + , 𝐺)‘(𝑗 + 1)) ↔ (Σ𝑘 ∈ (1...((2↑(𝑗 + 1)) − 1))(𝐹𝑘) + Σ𝑘 ∈ ((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1))(𝐹𝑘)) ≤ ((seq0( + , 𝐺)‘𝑗) + (𝐺‘(𝑗 + 1)))))
237218, 224, 2363imtr4d 296 . . . . 5 ((𝜑𝑗 ∈ ℕ0) → ((seq1( + , 𝐹)‘((2↑(𝑗 + 1)) − 1)) ≤ (seq0( + , 𝐺)‘𝑗) → (seq1( + , 𝐹)‘((2↑((𝑗 + 1) + 1)) − 1)) ≤ (seq0( + , 𝐺)‘(𝑗 + 1))))
238237expcom 416 . . . 4 (𝑗 ∈ ℕ0 → (𝜑 → ((seq1( + , 𝐹)‘((2↑(𝑗 + 1)) − 1)) ≤ (seq0( + , 𝐺)‘𝑗) → (seq1( + , 𝐹)‘((2↑((𝑗 + 1) + 1)) − 1)) ≤ (seq0( + , 𝐺)‘(𝑗 + 1)))))
239238a2d 29 . . 3 (𝑗 ∈ ℕ0 → ((𝜑 → (seq1( + , 𝐹)‘((2↑(𝑗 + 1)) − 1)) ≤ (seq0( + , 𝐺)‘𝑗)) → (𝜑 → (seq1( + , 𝐹)‘((2↑((𝑗 + 1) + 1)) − 1)) ≤ (seq0( + , 𝐺)‘(𝑗 + 1)))))
24018, 24, 30, 36, 66, 239nn0ind 12071 . 2 (𝑁 ∈ ℕ0 → (𝜑 → (seq1( + , 𝐹)‘((2↑(𝑁 + 1)) − 1)) ≤ (seq0( + , 𝐺)‘𝑁)))
241240impcom 410 1 ((𝜑𝑁 ∈ ℕ0) → (seq1( + , 𝐹)‘((2↑(𝑁 + 1)) − 1)) ≤ (seq0( + , 𝐺)‘𝑁))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 398   = wceq 1533   ∈ wcel 2110  ∀wral 3138   ∪ cun 3934   ∩ cin 3935  ∅c0 4291   class class class wbr 5059  ‘cfv 6350  (class class class)co 7150  Fincfn 8503  ℂcc 10529  ℝcr 10530  0cc0 10531  1c1 10532   + caddc 10534   · cmul 10536   < clt 10669   ≤ cle 10670   − cmin 10864  ℕcn 11632  2c2 11686  ℕ0cn0 11891  ℤcz 11975  ℤ≥cuz 12237  ...cfz 12886  seqcseq 13363  ↑cexp 13423  ♯chash 13684  Σcsu 15036 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2156  ax-12 2172  ax-ext 2793  ax-rep 5183  ax-sep 5196  ax-nul 5203  ax-pow 5259  ax-pr 5322  ax-un 7455  ax-inf2 9098  ax-cnex 10587  ax-resscn 10588  ax-1cn 10589  ax-icn 10590  ax-addcl 10591  ax-addrcl 10592  ax-mulcl 10593  ax-mulrcl 10594  ax-mulcom 10595  ax-addass 10596  ax-mulass 10597  ax-distr 10598  ax-i2m1 10599  ax-1ne0 10600  ax-1rid 10601  ax-rnegex 10602  ax-rrecex 10603  ax-cnre 10604  ax-pre-lttri 10605  ax-pre-lttrn 10606  ax-pre-ltadd 10607  ax-pre-mulgt0 10608  ax-pre-sup 10609 This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1536  df-fal 1546  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-nel 3124  df-ral 3143  df-rex 3144  df-reu 3145  df-rmo 3146  df-rab 3147  df-v 3497  df-sbc 3773  df-csb 3884  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-pss 3954  df-nul 4292  df-if 4468  df-pw 4541  df-sn 4562  df-pr 4564  df-tp 4566  df-op 4568  df-uni 4833  df-int 4870  df-iun 4914  df-br 5060  df-opab 5122  df-mpt 5140  df-tr 5166  df-id 5455  df-eprel 5460  df-po 5469  df-so 5470  df-fr 5509  df-se 5510  df-we 5511  df-xp 5556  df-rel 5557  df-cnv 5558  df-co 5559  df-dm 5560  df-rn 5561  df-res 5562  df-ima 5563  df-pred 6143  df-ord 6189  df-on 6190  df-lim 6191  df-suc 6192  df-iota 6309  df-fun 6352  df-fn 6353  df-f 6354  df-f1 6355  df-fo 6356  df-f1o 6357  df-fv 6358  df-isom 6359  df-riota 7108  df-ov 7153  df-oprab 7154  df-mpo 7155  df-om 7575  df-1st 7683  df-2nd 7684  df-wrecs 7941  df-recs 8002  df-rdg 8040  df-1o 8096  df-oadd 8100  df-er 8283  df-en 8504  df-dom 8505  df-sdom 8506  df-fin 8507  df-sup 8900  df-oi 8968  df-dju 9324  df-card 9362  df-pnf 10671  df-mnf 10672  df-xr 10673  df-ltxr 10674  df-le 10675  df-sub 10866  df-neg 10867  df-div 11292  df-nn 11633  df-2 11694  df-3 11695  df-n0 11892  df-z 11976  df-uz 12238  df-rp 12384  df-ico 12738  df-fz 12887  df-fzo 13028  df-seq 13364  df-exp 13424  df-hash 13685  df-cj 14452  df-re 14453  df-im 14454  df-sqrt 14588  df-abs 14589  df-clim 14839  df-sum 15037 This theorem is referenced by:  climcnds  15200
 Copyright terms: Public domain W3C validator