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

Theorem climcndslem1 15881
Description: Lemma for climcnds 15883: 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 7437 . . . . . . . . . . 11 (𝑥 = 0 → (𝑥 + 1) = (0 + 1))
2 0p1e1 12385 . . . . . . . . . . 11 (0 + 1) = 1
31, 2eqtrdi 2790 . . . . . . . . . 10 (𝑥 = 0 → (𝑥 + 1) = 1)
43oveq2d 7446 . . . . . . . . 9 (𝑥 = 0 → (2↑(𝑥 + 1)) = (2↑1))
5 2cn 12338 . . . . . . . . . . 11 2 ∈ ℂ
6 exp1 14104 . . . . . . . . . . 11 (2 ∈ ℂ → (2↑1) = 2)
75, 6ax-mp 5 . . . . . . . . . 10 (2↑1) = 2
8 df-2 12326 . . . . . . . . . 10 2 = (1 + 1)
97, 8eqtri 2762 . . . . . . . . 9 (2↑1) = (1 + 1)
104, 9eqtrdi 2790 . . . . . . . 8 (𝑥 = 0 → (2↑(𝑥 + 1)) = (1 + 1))
1110oveq1d 7445 . . . . . . 7 (𝑥 = 0 → ((2↑(𝑥 + 1)) − 1) = ((1 + 1) − 1))
12 ax-1cn 11210 . . . . . . . 8 1 ∈ ℂ
1312, 12pncan3oi 11521 . . . . . . 7 ((1 + 1) − 1) = 1
1411, 13eqtrdi 2790 . . . . . 6 (𝑥 = 0 → ((2↑(𝑥 + 1)) − 1) = 1)
1514fveq2d 6910 . . . . 5 (𝑥 = 0 → (seq1( + , 𝐹)‘((2↑(𝑥 + 1)) − 1)) = (seq1( + , 𝐹)‘1))
16 fveq2 6906 . . . . 5 (𝑥 = 0 → (seq0( + , 𝐺)‘𝑥) = (seq0( + , 𝐺)‘0))
1715, 16breq12d 5160 . . . 4 (𝑥 = 0 → ((seq1( + , 𝐹)‘((2↑(𝑥 + 1)) − 1)) ≤ (seq0( + , 𝐺)‘𝑥) ↔ (seq1( + , 𝐹)‘1) ≤ (seq0( + , 𝐺)‘0)))
1817imbi2d 340 . . 3 (𝑥 = 0 → ((𝜑 → (seq1( + , 𝐹)‘((2↑(𝑥 + 1)) − 1)) ≤ (seq0( + , 𝐺)‘𝑥)) ↔ (𝜑 → (seq1( + , 𝐹)‘1) ≤ (seq0( + , 𝐺)‘0))))
19 oveq1 7437 . . . . . . 7 (𝑥 = 𝑗 → (𝑥 + 1) = (𝑗 + 1))
2019oveq2d 7446 . . . . . 6 (𝑥 = 𝑗 → (2↑(𝑥 + 1)) = (2↑(𝑗 + 1)))
2120fvoveq1d 7452 . . . . 5 (𝑥 = 𝑗 → (seq1( + , 𝐹)‘((2↑(𝑥 + 1)) − 1)) = (seq1( + , 𝐹)‘((2↑(𝑗 + 1)) − 1)))
22 fveq2 6906 . . . . 5 (𝑥 = 𝑗 → (seq0( + , 𝐺)‘𝑥) = (seq0( + , 𝐺)‘𝑗))
2321, 22breq12d 5160 . . . 4 (𝑥 = 𝑗 → ((seq1( + , 𝐹)‘((2↑(𝑥 + 1)) − 1)) ≤ (seq0( + , 𝐺)‘𝑥) ↔ (seq1( + , 𝐹)‘((2↑(𝑗 + 1)) − 1)) ≤ (seq0( + , 𝐺)‘𝑗)))
2423imbi2d 340 . . 3 (𝑥 = 𝑗 → ((𝜑 → (seq1( + , 𝐹)‘((2↑(𝑥 + 1)) − 1)) ≤ (seq0( + , 𝐺)‘𝑥)) ↔ (𝜑 → (seq1( + , 𝐹)‘((2↑(𝑗 + 1)) − 1)) ≤ (seq0( + , 𝐺)‘𝑗))))
25 oveq1 7437 . . . . . . 7 (𝑥 = (𝑗 + 1) → (𝑥 + 1) = ((𝑗 + 1) + 1))
2625oveq2d 7446 . . . . . 6 (𝑥 = (𝑗 + 1) → (2↑(𝑥 + 1)) = (2↑((𝑗 + 1) + 1)))
2726fvoveq1d 7452 . . . . 5 (𝑥 = (𝑗 + 1) → (seq1( + , 𝐹)‘((2↑(𝑥 + 1)) − 1)) = (seq1( + , 𝐹)‘((2↑((𝑗 + 1) + 1)) − 1)))
28 fveq2 6906 . . . . 5 (𝑥 = (𝑗 + 1) → (seq0( + , 𝐺)‘𝑥) = (seq0( + , 𝐺)‘(𝑗 + 1)))
2927, 28breq12d 5160 . . . 4 (𝑥 = (𝑗 + 1) → ((seq1( + , 𝐹)‘((2↑(𝑥 + 1)) − 1)) ≤ (seq0( + , 𝐺)‘𝑥) ↔ (seq1( + , 𝐹)‘((2↑((𝑗 + 1) + 1)) − 1)) ≤ (seq0( + , 𝐺)‘(𝑗 + 1))))
3029imbi2d 340 . . 3 (𝑥 = (𝑗 + 1) → ((𝜑 → (seq1( + , 𝐹)‘((2↑(𝑥 + 1)) − 1)) ≤ (seq0( + , 𝐺)‘𝑥)) ↔ (𝜑 → (seq1( + , 𝐹)‘((2↑((𝑗 + 1) + 1)) − 1)) ≤ (seq0( + , 𝐺)‘(𝑗 + 1)))))
31 oveq1 7437 . . . . . . 7 (𝑥 = 𝑁 → (𝑥 + 1) = (𝑁 + 1))
3231oveq2d 7446 . . . . . 6 (𝑥 = 𝑁 → (2↑(𝑥 + 1)) = (2↑(𝑁 + 1)))
3332fvoveq1d 7452 . . . . 5 (𝑥 = 𝑁 → (seq1( + , 𝐹)‘((2↑(𝑥 + 1)) − 1)) = (seq1( + , 𝐹)‘((2↑(𝑁 + 1)) − 1)))
34 fveq2 6906 . . . . 5 (𝑥 = 𝑁 → (seq0( + , 𝐺)‘𝑥) = (seq0( + , 𝐺)‘𝑁))
3533, 34breq12d 5160 . . . 4 (𝑥 = 𝑁 → ((seq1( + , 𝐹)‘((2↑(𝑥 + 1)) − 1)) ≤ (seq0( + , 𝐺)‘𝑥) ↔ (seq1( + , 𝐹)‘((2↑(𝑁 + 1)) − 1)) ≤ (seq0( + , 𝐺)‘𝑁)))
3635imbi2d 340 . . 3 (𝑥 = 𝑁 → ((𝜑 → (seq1( + , 𝐹)‘((2↑(𝑥 + 1)) − 1)) ≤ (seq0( + , 𝐺)‘𝑥)) ↔ (𝜑 → (seq1( + , 𝐹)‘((2↑(𝑁 + 1)) − 1)) ≤ (seq0( + , 𝐺)‘𝑁))))
37 fveq2 6906 . . . . . . . 8 (𝑘 = 1 → (𝐹𝑘) = (𝐹‘1))
3837eleq1d 2823 . . . . . . 7 (𝑘 = 1 → ((𝐹𝑘) ∈ ℝ ↔ (𝐹‘1) ∈ ℝ))
39 climcnds.1 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ) → (𝐹𝑘) ∈ ℝ)
4039ralrimiva 3143 . . . . . . 7 (𝜑 → ∀𝑘 ∈ ℕ (𝐹𝑘) ∈ ℝ)
41 1nn 12274 . . . . . . . 8 1 ∈ ℕ
4241a1i 11 . . . . . . 7 (𝜑 → 1 ∈ ℕ)
4338, 40, 42rspcdva 3622 . . . . . 6 (𝜑 → (𝐹‘1) ∈ ℝ)
4443leidd 11826 . . . . 5 (𝜑 → (𝐹‘1) ≤ (𝐹‘1))
4543recnd 11286 . . . . . 6 (𝜑 → (𝐹‘1) ∈ ℂ)
4645mullidd 11276 . . . . 5 (𝜑 → (1 · (𝐹‘1)) = (𝐹‘1))
4744, 46breqtrrd 5175 . . . 4 (𝜑 → (𝐹‘1) ≤ (1 · (𝐹‘1)))
48 1z 12644 . . . . 5 1 ∈ ℤ
49 eqidd 2735 . . . . 5 (𝜑 → (𝐹‘1) = (𝐹‘1))
5048, 49seq1i 14052 . . . 4 (𝜑 → (seq1( + , 𝐹)‘1) = (𝐹‘1))
51 0z 12621 . . . . 5 0 ∈ ℤ
52 fveq2 6906 . . . . . . 7 (𝑛 = 0 → (𝐺𝑛) = (𝐺‘0))
53 oveq2 7438 . . . . . . . . 9 (𝑛 = 0 → (2↑𝑛) = (2↑0))
54 exp0 14102 . . . . . . . . . 10 (2 ∈ ℂ → (2↑0) = 1)
555, 54ax-mp 5 . . . . . . . . 9 (2↑0) = 1
5653, 55eqtrdi 2790 . . . . . . . 8 (𝑛 = 0 → (2↑𝑛) = 1)
5756fveq2d 6910 . . . . . . . 8 (𝑛 = 0 → (𝐹‘(2↑𝑛)) = (𝐹‘1))
5856, 57oveq12d 7448 . . . . . . 7 (𝑛 = 0 → ((2↑𝑛) · (𝐹‘(2↑𝑛))) = (1 · (𝐹‘1)))
5952, 58eqeq12d 2750 . . . . . 6 (𝑛 = 0 → ((𝐺𝑛) = ((2↑𝑛) · (𝐹‘(2↑𝑛))) ↔ (𝐺‘0) = (1 · (𝐹‘1))))
60 climcnds.4 . . . . . . 7 ((𝜑𝑛 ∈ ℕ0) → (𝐺𝑛) = ((2↑𝑛) · (𝐹‘(2↑𝑛))))
6160ralrimiva 3143 . . . . . 6 (𝜑 → ∀𝑛 ∈ ℕ0 (𝐺𝑛) = ((2↑𝑛) · (𝐹‘(2↑𝑛))))
62 0nn0 12538 . . . . . . 7 0 ∈ ℕ0
6362a1i 11 . . . . . 6 (𝜑 → 0 ∈ ℕ0)
6459, 61, 63rspcdva 3622 . . . . 5 (𝜑 → (𝐺‘0) = (1 · (𝐹‘1)))
6551, 64seq1i 14052 . . . 4 (𝜑 → (seq0( + , 𝐺)‘0) = (1 · (𝐹‘1)))
6647, 50, 653brtr4d 5179 . . 3 (𝜑 → (seq1( + , 𝐹)‘1) ≤ (seq0( + , 𝐺)‘0))
67 fzfid 14010 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ0) → ((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1)) ∈ Fin)
68 simpl 482 . . . . . . . . . 10 ((𝜑𝑗 ∈ ℕ0) → 𝜑)
69 2nn 12336 . . . . . . . . . . . 12 2 ∈ ℕ
70 peano2nn0 12563 . . . . . . . . . . . . 13 (𝑗 ∈ ℕ0 → (𝑗 + 1) ∈ ℕ0)
7170adantl 481 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ0) → (𝑗 + 1) ∈ ℕ0)
72 nnexpcl 14111 . . . . . . . . . . . 12 ((2 ∈ ℕ ∧ (𝑗 + 1) ∈ ℕ0) → (2↑(𝑗 + 1)) ∈ ℕ)
7369, 71, 72sylancr 587 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ℕ0) → (2↑(𝑗 + 1)) ∈ ℕ)
74 elfzuz 13556 . . . . . . . . . . 11 (𝑘 ∈ ((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1)) → 𝑘 ∈ (ℤ‘(2↑(𝑗 + 1))))
75 eluznn 12957 . . . . . . . . . . 11 (((2↑(𝑗 + 1)) ∈ ℕ ∧ 𝑘 ∈ (ℤ‘(2↑(𝑗 + 1)))) → 𝑘 ∈ ℕ)
7673, 74, 75syl2an 596 . . . . . . . . . 10 (((𝜑𝑗 ∈ ℕ0) ∧ 𝑘 ∈ ((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1))) → 𝑘 ∈ ℕ)
7768, 76, 39syl2an2r 685 . . . . . . . . 9 (((𝜑𝑗 ∈ ℕ0) ∧ 𝑘 ∈ ((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1))) → (𝐹𝑘) ∈ ℝ)
78 fveq2 6906 . . . . . . . . . . . 12 (𝑘 = (2↑(𝑗 + 1)) → (𝐹𝑘) = (𝐹‘(2↑(𝑗 + 1))))
7978eleq1d 2823 . . . . . . . . . . 11 (𝑘 = (2↑(𝑗 + 1)) → ((𝐹𝑘) ∈ ℝ ↔ (𝐹‘(2↑(𝑗 + 1))) ∈ ℝ))
8040adantr 480 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ℕ0) → ∀𝑘 ∈ ℕ (𝐹𝑘) ∈ ℝ)
8179, 80, 73rspcdva 3622 . . . . . . . . . 10 ((𝜑𝑗 ∈ ℕ0) → (𝐹‘(2↑(𝑗 + 1))) ∈ ℝ)
8281adantr 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))...𝑛)) → 𝜑)
8573adantr 480 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ ℕ0) ∧ 𝑛 ∈ (ℤ‘(2↑(𝑗 + 1)))) → (2↑(𝑗 + 1)) ∈ ℕ)
86 elfzuz 13556 . . . . . . . . . . . . . 14 (𝑘 ∈ ((2↑(𝑗 + 1))...𝑛) → 𝑘 ∈ (ℤ‘(2↑(𝑗 + 1))))
8785, 86, 75syl2an 596 . . . . . . . . . . . . 13 ((((𝜑𝑗 ∈ ℕ0) ∧ 𝑛 ∈ (ℤ‘(2↑(𝑗 + 1)))) ∧ 𝑘 ∈ ((2↑(𝑗 + 1))...𝑛)) → 𝑘 ∈ ℕ)
8884, 87, 39syl2anc 584 . . . . . . . . . . . 12 ((((𝜑𝑗 ∈ ℕ0) ∧ 𝑛 ∈ (ℤ‘(2↑(𝑗 + 1)))) ∧ 𝑘 ∈ ((2↑(𝑗 + 1))...𝑛)) → (𝐹𝑘) ∈ ℝ)
89 simplll 775 . . . . . . . . . . . . 13 ((((𝜑𝑗 ∈ ℕ0) ∧ 𝑛 ∈ (ℤ‘(2↑(𝑗 + 1)))) ∧ 𝑘 ∈ ((2↑(𝑗 + 1))...(𝑛 − 1))) → 𝜑)
90 elfzuz 13556 . . . . . . . . . . . . . 14 (𝑘 ∈ ((2↑(𝑗 + 1))...(𝑛 − 1)) → 𝑘 ∈ (ℤ‘(2↑(𝑗 + 1))))
9185, 90, 75syl2an 596 . . . . . . . . . . . . 13 ((((𝜑𝑗 ∈ ℕ0) ∧ 𝑛 ∈ (ℤ‘(2↑(𝑗 + 1)))) ∧ 𝑘 ∈ ((2↑(𝑗 + 1))...(𝑛 − 1))) → 𝑘 ∈ ℕ)
92 climcnds.3 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ) → (𝐹‘(𝑘 + 1)) ≤ (𝐹𝑘))
9389, 91, 92syl2anc 584 . . . . . . . . . . . 12 ((((𝜑𝑗 ∈ ℕ0) ∧ 𝑛 ∈ (ℤ‘(2↑(𝑗 + 1)))) ∧ 𝑘 ∈ ((2↑(𝑗 + 1))...(𝑛 − 1))) → (𝐹‘(𝑘 + 1)) ≤ (𝐹𝑘))
9483, 88, 93monoord2 14070 . . . . . . . . . . 11 (((𝜑𝑗 ∈ ℕ0) ∧ 𝑛 ∈ (ℤ‘(2↑(𝑗 + 1)))) → (𝐹𝑛) ≤ (𝐹‘(2↑(𝑗 + 1))))
9594ralrimiva 3143 . . . . . . . . . 10 ((𝜑𝑗 ∈ ℕ0) → ∀𝑛 ∈ (ℤ‘(2↑(𝑗 + 1)))(𝐹𝑛) ≤ (𝐹‘(2↑(𝑗 + 1))))
96 fveq2 6906 . . . . . . . . . . . 12 (𝑛 = 𝑘 → (𝐹𝑛) = (𝐹𝑘))
9796breq1d 5157 . . . . . . . . . . 11 (𝑛 = 𝑘 → ((𝐹𝑛) ≤ (𝐹‘(2↑(𝑗 + 1))) ↔ (𝐹𝑘) ≤ (𝐹‘(2↑(𝑗 + 1)))))
9897rspccva 3620 . . . . . . . . . 10 ((∀𝑛 ∈ (ℤ‘(2↑(𝑗 + 1)))(𝐹𝑛) ≤ (𝐹‘(2↑(𝑗 + 1))) ∧ 𝑘 ∈ (ℤ‘(2↑(𝑗 + 1)))) → (𝐹𝑘) ≤ (𝐹‘(2↑(𝑗 + 1))))
9995, 74, 98syl2an 596 . . . . . . . . 9 (((𝜑𝑗 ∈ ℕ0) ∧ 𝑘 ∈ ((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1))) → (𝐹𝑘) ≤ (𝐹‘(2↑(𝑗 + 1))))
10067, 77, 82, 99fsumle 15831 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ0) → Σ𝑘 ∈ ((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1))(𝐹𝑘) ≤ Σ𝑘 ∈ ((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1))(𝐹‘(2↑(𝑗 + 1))))
101 fzfid 14010 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ ℕ0) → (1...((2↑(𝑗 + 1)) − 1)) ∈ Fin)
102 hashcl 14391 . . . . . . . . . . . . 13 ((1...((2↑(𝑗 + 1)) − 1)) ∈ Fin → (♯‘(1...((2↑(𝑗 + 1)) − 1))) ∈ ℕ0)
103101, 102syl 17 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ0) → (♯‘(1...((2↑(𝑗 + 1)) − 1))) ∈ ℕ0)
104103nn0cnd 12586 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ℕ0) → (♯‘(1...((2↑(𝑗 + 1)) − 1))) ∈ ℂ)
10573nnred 12278 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ0) → (2↑(𝑗 + 1)) ∈ ℝ)
106105recnd 11286 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ℕ0) → (2↑(𝑗 + 1)) ∈ ℂ)
107 hashcl 14391 . . . . . . . . . . . . 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 12586 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ℕ0) → (♯‘((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1))) ∈ ℂ)
110 2z 12646 . . . . . . . . . . . . . . . . . . . 20 2 ∈ ℤ
111 zexpcl 14113 . . . . . . . . . . . . . . . . . . . 20 ((2 ∈ ℤ ∧ (𝑗 + 1) ∈ ℕ0) → (2↑(𝑗 + 1)) ∈ ℤ)
112110, 71, 111sylancr 587 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ ℕ0) → (2↑(𝑗 + 1)) ∈ ℤ)
113 2re 12337 . . . . . . . . . . . . . . . . . . . . 21 2 ∈ ℝ
114 1le2 12472 . . . . . . . . . . . . . . . . . . . . 21 1 ≤ 2
115 nn0p1nn 12562 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 ∈ ℕ0 → (𝑗 + 1) ∈ ℕ)
116115adantl 481 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑗 ∈ ℕ0) → (𝑗 + 1) ∈ ℕ)
117 nnuz 12918 . . . . . . . . . . . . . . . . . . . . . 22 ℕ = (ℤ‘1)
118116, 117eleqtrdi 2848 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗 ∈ ℕ0) → (𝑗 + 1) ∈ (ℤ‘1))
119 leexp2a 14208 . . . . . . . . . . . . . . . . . . . . 21 ((2 ∈ ℝ ∧ 1 ≤ 2 ∧ (𝑗 + 1) ∈ (ℤ‘1)) → (2↑1) ≤ (2↑(𝑗 + 1)))
120113, 114, 118, 119mp3an12i 1464 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ ℕ0) → (2↑1) ≤ (2↑(𝑗 + 1)))
1217, 120eqbrtrrid 5183 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ ℕ0) → 2 ≤ (2↑(𝑗 + 1)))
122110eluz1i 12883 . . . . . . . . . . . . . . . . . . 19 ((2↑(𝑗 + 1)) ∈ (ℤ‘2) ↔ ((2↑(𝑗 + 1)) ∈ ℤ ∧ 2 ≤ (2↑(𝑗 + 1))))
123112, 121, 122sylanbrc 583 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ ℕ0) → (2↑(𝑗 + 1)) ∈ (ℤ‘2))
124 uz2m1nn 12962 . . . . . . . . . . . . . . . . . 18 ((2↑(𝑗 + 1)) ∈ (ℤ‘2) → ((2↑(𝑗 + 1)) − 1) ∈ ℕ)
125123, 124syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ ℕ0) → ((2↑(𝑗 + 1)) − 1) ∈ ℕ)
126125, 117eleqtrdi 2848 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ ℕ0) → ((2↑(𝑗 + 1)) − 1) ∈ (ℤ‘1))
127 peano2zm 12657 . . . . . . . . . . . . . . . . . 18 ((2↑(𝑗 + 1)) ∈ ℤ → ((2↑(𝑗 + 1)) − 1) ∈ ℤ)
128112, 127syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ ℕ0) → ((2↑(𝑗 + 1)) − 1) ∈ ℤ)
129 peano2nn0 12563 . . . . . . . . . . . . . . . . . . . 20 ((𝑗 + 1) ∈ ℕ0 → ((𝑗 + 1) + 1) ∈ ℕ0)
13071, 129syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ ℕ0) → ((𝑗 + 1) + 1) ∈ ℕ0)
131 zexpcl 14113 . . . . . . . . . . . . . . . . . . 19 ((2 ∈ ℤ ∧ ((𝑗 + 1) + 1) ∈ ℕ0) → (2↑((𝑗 + 1) + 1)) ∈ ℤ)
132110, 130, 131sylancr 587 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ ℕ0) → (2↑((𝑗 + 1) + 1)) ∈ ℤ)
133 peano2zm 12657 . . . . . . . . . . . . . . . . . 18 ((2↑((𝑗 + 1) + 1)) ∈ ℤ → ((2↑((𝑗 + 1) + 1)) − 1) ∈ ℤ)
134132, 133syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ ℕ0) → ((2↑((𝑗 + 1) + 1)) − 1) ∈ ℤ)
135112zred 12719 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ ℕ0) → (2↑(𝑗 + 1)) ∈ ℝ)
136132zred 12719 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ ℕ0) → (2↑((𝑗 + 1) + 1)) ∈ ℝ)
137 1red 11259 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ ℕ0) → 1 ∈ ℝ)
13871nn0zd 12636 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ ℕ0) → (𝑗 + 1) ∈ ℤ)
139 uzid 12890 . . . . . . . . . . . . . . . . . . 19 ((𝑗 + 1) ∈ ℤ → (𝑗 + 1) ∈ (ℤ‘(𝑗 + 1)))
140 peano2uz 12940 . . . . . . . . . . . . . . . . . . 19 ((𝑗 + 1) ∈ (ℤ‘(𝑗 + 1)) → ((𝑗 + 1) + 1) ∈ (ℤ‘(𝑗 + 1)))
141 leexp2a 14208 . . . . . . . . . . . . . . . . . . . 20 ((2 ∈ ℝ ∧ 1 ≤ 2 ∧ ((𝑗 + 1) + 1) ∈ (ℤ‘(𝑗 + 1))) → (2↑(𝑗 + 1)) ≤ (2↑((𝑗 + 1) + 1)))
142113, 114, 141mp3an12 1450 . . . . . . . . . . . . . . . . . . 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 11876 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ ℕ0) → ((2↑(𝑗 + 1)) − 1) ≤ ((2↑((𝑗 + 1) + 1)) − 1))
145 eluz2 12881 . . . . . . . . . . . . . . . . 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 1342 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ ℕ0) → ((2↑((𝑗 + 1) + 1)) − 1) ∈ (ℤ‘((2↑(𝑗 + 1)) − 1)))
147 elfzuzb 13554 . . . . . . . . . . . . . . . 16 (((2↑(𝑗 + 1)) − 1) ∈ (1...((2↑((𝑗 + 1) + 1)) − 1)) ↔ (((2↑(𝑗 + 1)) − 1) ∈ (ℤ‘1) ∧ ((2↑((𝑗 + 1) + 1)) − 1) ∈ (ℤ‘((2↑(𝑗 + 1)) − 1))))
148126, 146, 147sylanbrc 583 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ ℕ0) → ((2↑(𝑗 + 1)) − 1) ∈ (1...((2↑((𝑗 + 1) + 1)) − 1)))
149 fzsplit 13586 . . . . . . . . . . . . . . 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 11514 . . . . . . . . . . . . . . . . 17 (((2↑(𝑗 + 1)) ∈ ℂ ∧ 1 ∈ ℂ) → (((2↑(𝑗 + 1)) − 1) + 1) = (2↑(𝑗 + 1)))
152106, 12, 151sylancl 586 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ ℕ0) → (((2↑(𝑗 + 1)) − 1) + 1) = (2↑(𝑗 + 1)))
153152oveq1d 7445 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ ℕ0) → ((((2↑(𝑗 + 1)) − 1) + 1)...((2↑((𝑗 + 1) + 1)) − 1)) = ((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1)))
154153uneq2d 4177 . . . . . . . . . . . . . 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 2774 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ ℕ0) → (1...((2↑((𝑗 + 1) + 1)) − 1)) = ((1...((2↑(𝑗 + 1)) − 1)) ∪ ((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1))))
156155fveq2d 6910 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ0) → (♯‘(1...((2↑((𝑗 + 1) + 1)) − 1))) = (♯‘((1...((2↑(𝑗 + 1)) − 1)) ∪ ((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1)))))
157 expp1 14105 . . . . . . . . . . . . . . . . 17 ((2 ∈ ℂ ∧ (𝑗 + 1) ∈ ℕ0) → (2↑((𝑗 + 1) + 1)) = ((2↑(𝑗 + 1)) · 2))
1585, 71, 157sylancr 587 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ ℕ0) → (2↑((𝑗 + 1) + 1)) = ((2↑(𝑗 + 1)) · 2))
159106times2d 12507 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ ℕ0) → ((2↑(𝑗 + 1)) · 2) = ((2↑(𝑗 + 1)) + (2↑(𝑗 + 1))))
160158, 159eqtrd 2774 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ ℕ0) → (2↑((𝑗 + 1) + 1)) = ((2↑(𝑗 + 1)) + (2↑(𝑗 + 1))))
161160oveq1d 7445 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ ℕ0) → ((2↑((𝑗 + 1) + 1)) − 1) = (((2↑(𝑗 + 1)) + (2↑(𝑗 + 1))) − 1))
162 1cnd 11253 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ ℕ0) → 1 ∈ ℂ)
163106, 106, 162addsubd 11638 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ ℕ0) → (((2↑(𝑗 + 1)) + (2↑(𝑗 + 1))) − 1) = (((2↑(𝑗 + 1)) − 1) + (2↑(𝑗 + 1))))
164161, 163eqtrd 2774 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ ℕ0) → ((2↑((𝑗 + 1) + 1)) − 1) = (((2↑(𝑗 + 1)) − 1) + (2↑(𝑗 + 1))))
165 uztrn 12893 . . . . . . . . . . . . . . . . 17 ((((2↑((𝑗 + 1) + 1)) − 1) ∈ (ℤ‘((2↑(𝑗 + 1)) − 1)) ∧ ((2↑(𝑗 + 1)) − 1) ∈ (ℤ‘1)) → ((2↑((𝑗 + 1) + 1)) − 1) ∈ (ℤ‘1))
166146, 126, 165syl2anc 584 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ ℕ0) → ((2↑((𝑗 + 1) + 1)) − 1) ∈ (ℤ‘1))
167166, 117eleqtrrdi 2849 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ ℕ0) → ((2↑((𝑗 + 1) + 1)) − 1) ∈ ℕ)
168167nnnn0d 12584 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ ℕ0) → ((2↑((𝑗 + 1) + 1)) − 1) ∈ ℕ0)
169 hashfz1 14381 . . . . . . . . . . . . . 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 12584 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ ℕ0) → ((2↑(𝑗 + 1)) − 1) ∈ ℕ0)
172 hashfz1 14381 . . . . . . . . . . . . . . 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 7445 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ ℕ0) → ((♯‘(1...((2↑(𝑗 + 1)) − 1))) + (2↑(𝑗 + 1))) = (((2↑(𝑗 + 1)) − 1) + (2↑(𝑗 + 1))))
175164, 170, 1743eqtr4d 2784 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ0) → (♯‘(1...((2↑((𝑗 + 1) + 1)) − 1))) = ((♯‘(1...((2↑(𝑗 + 1)) − 1))) + (2↑(𝑗 + 1))))
176105ltm1d 12197 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ ℕ0) → ((2↑(𝑗 + 1)) − 1) < (2↑(𝑗 + 1)))
177 fzdisj 13587 . . . . . . . . . . . . . 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 14417 . . . . . . . . . . . . 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 1370 . . . . . . . . . . . 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 2782 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ℕ0) → ((♯‘(1...((2↑(𝑗 + 1)) − 1))) + (2↑(𝑗 + 1))) = ((♯‘(1...((2↑(𝑗 + 1)) − 1))) + (♯‘((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1)))))
182104, 106, 109, 181addcanad 11463 . . . . . . . . . 10 ((𝜑𝑗 ∈ ℕ0) → (2↑(𝑗 + 1)) = (♯‘((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1))))
183182oveq1d 7445 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ0) → ((2↑(𝑗 + 1)) · (𝐹‘(2↑(𝑗 + 1)))) = ((♯‘((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1))) · (𝐹‘(2↑(𝑗 + 1)))))
184 fveq2 6906 . . . . . . . . . . 11 (𝑛 = (𝑗 + 1) → (𝐺𝑛) = (𝐺‘(𝑗 + 1)))
185 oveq2 7438 . . . . . . . . . . . 12 (𝑛 = (𝑗 + 1) → (2↑𝑛) = (2↑(𝑗 + 1)))
186185fveq2d 6910 . . . . . . . . . . . 12 (𝑛 = (𝑗 + 1) → (𝐹‘(2↑𝑛)) = (𝐹‘(2↑(𝑗 + 1))))
187185, 186oveq12d 7448 . . . . . . . . . . 11 (𝑛 = (𝑗 + 1) → ((2↑𝑛) · (𝐹‘(2↑𝑛))) = ((2↑(𝑗 + 1)) · (𝐹‘(2↑(𝑗 + 1)))))
188184, 187eqeq12d 2750 . . . . . . . . . 10 (𝑛 = (𝑗 + 1) → ((𝐺𝑛) = ((2↑𝑛) · (𝐹‘(2↑𝑛))) ↔ (𝐺‘(𝑗 + 1)) = ((2↑(𝑗 + 1)) · (𝐹‘(2↑(𝑗 + 1))))))
18961adantr 480 . . . . . . . . . 10 ((𝜑𝑗 ∈ ℕ0) → ∀𝑛 ∈ ℕ0 (𝐺𝑛) = ((2↑𝑛) · (𝐹‘(2↑𝑛))))
190188, 189, 71rspcdva 3622 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ0) → (𝐺‘(𝑗 + 1)) = ((2↑(𝑗 + 1)) · (𝐹‘(2↑(𝑗 + 1)))))
19181recnd 11286 . . . . . . . . . 10 ((𝜑𝑗 ∈ ℕ0) → (𝐹‘(2↑(𝑗 + 1))) ∈ ℂ)
192 fsumconst 15822 . . . . . . . . . 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 584 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ0) → Σ𝑘 ∈ ((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1))(𝐹‘(2↑(𝑗 + 1))) = ((♯‘((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1))) · (𝐹‘(2↑(𝑗 + 1)))))
194183, 190, 1933eqtr4d 2784 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ0) → (𝐺‘(𝑗 + 1)) = Σ𝑘 ∈ ((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1))(𝐹‘(2↑(𝑗 + 1))))
195100, 194breqtrrd 5175 . . . . . . 7 ((𝜑𝑗 ∈ ℕ0) → Σ𝑘 ∈ ((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1))(𝐹𝑘) ≤ (𝐺‘(𝑗 + 1)))
196 elfznn 13589 . . . . . . . . . 10 (𝑘 ∈ (1...((2↑(𝑗 + 1)) − 1)) → 𝑘 ∈ ℕ)
19768, 196, 39syl2an 596 . . . . . . . . 9 (((𝜑𝑗 ∈ ℕ0) ∧ 𝑘 ∈ (1...((2↑(𝑗 + 1)) − 1))) → (𝐹𝑘) ∈ ℝ)
198101, 197fsumrecl 15766 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ0) → Σ𝑘 ∈ (1...((2↑(𝑗 + 1)) − 1))(𝐹𝑘) ∈ ℝ)
19967, 77fsumrecl 15766 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ0) → Σ𝑘 ∈ ((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1))(𝐹𝑘) ∈ ℝ)
200 nn0uz 12917 . . . . . . . . . 10 0 = (ℤ‘0)
201 0zd 12622 . . . . . . . . . 10 (𝜑 → 0 ∈ ℤ)
202 simpr 484 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ ℕ0) → 𝑛 ∈ ℕ0)
203 nnexpcl 14111 . . . . . . . . . . . . . 14 ((2 ∈ ℕ ∧ 𝑛 ∈ ℕ0) → (2↑𝑛) ∈ ℕ)
20469, 202, 203sylancr 587 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ ℕ0) → (2↑𝑛) ∈ ℕ)
205204nnred 12278 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ0) → (2↑𝑛) ∈ ℝ)
206 fveq2 6906 . . . . . . . . . . . . . 14 (𝑘 = (2↑𝑛) → (𝐹𝑘) = (𝐹‘(2↑𝑛)))
207206eleq1d 2823 . . . . . . . . . . . . 13 (𝑘 = (2↑𝑛) → ((𝐹𝑘) ∈ ℝ ↔ (𝐹‘(2↑𝑛)) ∈ ℝ))
20840adantr 480 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ ℕ0) → ∀𝑘 ∈ ℕ (𝐹𝑘) ∈ ℝ)
209207, 208, 204rspcdva 3622 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ0) → (𝐹‘(2↑𝑛)) ∈ ℝ)
210205, 209remulcld 11288 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ0) → ((2↑𝑛) · (𝐹‘(2↑𝑛))) ∈ ℝ)
21160, 210eqeltrd 2838 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ0) → (𝐺𝑛) ∈ ℝ)
212200, 201, 211serfre 14068 . . . . . . . . 9 (𝜑 → seq0( + , 𝐺):ℕ0⟶ℝ)
213212ffvelcdmda 7103 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ0) → (seq0( + , 𝐺)‘𝑗) ∈ ℝ)
214135, 81remulcld 11288 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ0) → ((2↑(𝑗 + 1)) · (𝐹‘(2↑(𝑗 + 1)))) ∈ ℝ)
215190, 214eqeltrd 2838 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ0) → (𝐺‘(𝑗 + 1)) ∈ ℝ)
216 le2add 11742 . . . . . . . 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 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)))))
218195, 217mpan2d 694 . . . . . 6 ((𝜑𝑗 ∈ ℕ0) → (Σ𝑘 ∈ (1...((2↑(𝑗 + 1)) − 1))(𝐹𝑘) ≤ (seq0( + , 𝐺)‘𝑗) → (Σ𝑘 ∈ (1...((2↑(𝑗 + 1)) − 1))(𝐹𝑘) + Σ𝑘 ∈ ((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1))(𝐹𝑘)) ≤ ((seq0( + , 𝐺)‘𝑗) + (𝐺‘(𝑗 + 1)))))
219 eqidd 2735 . . . . . . . . 9 (((𝜑𝑗 ∈ ℕ0) ∧ 𝑘 ∈ (1...((2↑(𝑗 + 1)) − 1))) → (𝐹𝑘) = (𝐹𝑘))
22039recnd 11286 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ) → (𝐹𝑘) ∈ ℂ)
22168, 196, 220syl2an 596 . . . . . . . . 9 (((𝜑𝑗 ∈ ℕ0) ∧ 𝑘 ∈ (1...((2↑(𝑗 + 1)) − 1))) → (𝐹𝑘) ∈ ℂ)
222219, 126, 221fsumser 15762 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ0) → Σ𝑘 ∈ (1...((2↑(𝑗 + 1)) − 1))(𝐹𝑘) = (seq1( + , 𝐹)‘((2↑(𝑗 + 1)) − 1)))
223222eqcomd 2740 . . . . . . 7 ((𝜑𝑗 ∈ ℕ0) → (seq1( + , 𝐹)‘((2↑(𝑗 + 1)) − 1)) = Σ𝑘 ∈ (1...((2↑(𝑗 + 1)) − 1))(𝐹𝑘))
224223breq1d 5157 . . . . . 6 ((𝜑𝑗 ∈ ℕ0) → ((seq1( + , 𝐹)‘((2↑(𝑗 + 1)) − 1)) ≤ (seq0( + , 𝐺)‘𝑗) ↔ Σ𝑘 ∈ (1...((2↑(𝑗 + 1)) − 1))(𝐹𝑘) ≤ (seq0( + , 𝐺)‘𝑗)))
225 eqidd 2735 . . . . . . . . 9 (((𝜑𝑗 ∈ ℕ0) ∧ 𝑘 ∈ (1...((2↑((𝑗 + 1) + 1)) − 1))) → (𝐹𝑘) = (𝐹𝑘))
226 elfznn 13589 . . . . . . . . . 10 (𝑘 ∈ (1...((2↑((𝑗 + 1) + 1)) − 1)) → 𝑘 ∈ ℕ)
22768, 226, 220syl2an 596 . . . . . . . . 9 (((𝜑𝑗 ∈ ℕ0) ∧ 𝑘 ∈ (1...((2↑((𝑗 + 1) + 1)) − 1))) → (𝐹𝑘) ∈ ℂ)
228225, 166, 227fsumser 15762 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ0) → Σ𝑘 ∈ (1...((2↑((𝑗 + 1) + 1)) − 1))(𝐹𝑘) = (seq1( + , 𝐹)‘((2↑((𝑗 + 1) + 1)) − 1)))
229 fzfid 14010 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ0) → (1...((2↑((𝑗 + 1) + 1)) − 1)) ∈ Fin)
230178, 155, 229, 227fsumsplit 15773 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ0) → Σ𝑘 ∈ (1...((2↑((𝑗 + 1) + 1)) − 1))(𝐹𝑘) = (Σ𝑘 ∈ (1...((2↑(𝑗 + 1)) − 1))(𝐹𝑘) + Σ𝑘 ∈ ((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1))(𝐹𝑘)))
231228, 230eqtr3d 2776 . . . . . . 7 ((𝜑𝑗 ∈ ℕ0) → (seq1( + , 𝐹)‘((2↑((𝑗 + 1) + 1)) − 1)) = (Σ𝑘 ∈ (1...((2↑(𝑗 + 1)) − 1))(𝐹𝑘) + Σ𝑘 ∈ ((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1))(𝐹𝑘)))
232 simpr 484 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ0) → 𝑗 ∈ ℕ0)
233232, 200eleqtrdi 2848 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ0) → 𝑗 ∈ (ℤ‘0))
234 seqp1 14053 . . . . . . . 8 (𝑗 ∈ (ℤ‘0) → (seq0( + , 𝐺)‘(𝑗 + 1)) = ((seq0( + , 𝐺)‘𝑗) + (𝐺‘(𝑗 + 1))))
235233, 234syl 17 . . . . . . 7 ((𝜑𝑗 ∈ ℕ0) → (seq0( + , 𝐺)‘(𝑗 + 1)) = ((seq0( + , 𝐺)‘𝑗) + (𝐺‘(𝑗 + 1))))
236231, 235breq12d 5160 . . . . . 6 ((𝜑𝑗 ∈ ℕ0) → ((seq1( + , 𝐹)‘((2↑((𝑗 + 1) + 1)) − 1)) ≤ (seq0( + , 𝐺)‘(𝑗 + 1)) ↔ (Σ𝑘 ∈ (1...((2↑(𝑗 + 1)) − 1))(𝐹𝑘) + Σ𝑘 ∈ ((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1))(𝐹𝑘)) ≤ ((seq0( + , 𝐺)‘𝑗) + (𝐺‘(𝑗 + 1)))))
237218, 224, 2363imtr4d 294 . . . . 5 ((𝜑𝑗 ∈ ℕ0) → ((seq1( + , 𝐹)‘((2↑(𝑗 + 1)) − 1)) ≤ (seq0( + , 𝐺)‘𝑗) → (seq1( + , 𝐹)‘((2↑((𝑗 + 1) + 1)) − 1)) ≤ (seq0( + , 𝐺)‘(𝑗 + 1))))
238237expcom 413 . . . 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 12710 . 2 (𝑁 ∈ ℕ0 → (𝜑 → (seq1( + , 𝐹)‘((2↑(𝑁 + 1)) − 1)) ≤ (seq0( + , 𝐺)‘𝑁)))
241240impcom 407 1 ((𝜑𝑁 ∈ ℕ0) → (seq1( + , 𝐹)‘((2↑(𝑁 + 1)) − 1)) ≤ (seq0( + , 𝐺)‘𝑁))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395   = wceq 1536  wcel 2105  wral 3058  cun 3960  cin 3961  c0 4338   class class class wbr 5147  cfv 6562  (class class class)co 7430  Fincfn 8983  cc 11150  cr 11151  0cc0 11152  1c1 11153   + caddc 11155   · cmul 11157   < clt 11292  cle 11293  cmin 11489  cn 12263  2c2 12318  0cn0 12523  cz 12610  cuz 12875  ...cfz 13543  seqcseq 14038  cexp 14098  chash 14365  Σcsu 15718
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-rep 5284  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753  ax-inf2 9678  ax-cnex 11208  ax-resscn 11209  ax-1cn 11210  ax-icn 11211  ax-addcl 11212  ax-addrcl 11213  ax-mulcl 11214  ax-mulrcl 11215  ax-mulcom 11216  ax-addass 11217  ax-mulass 11218  ax-distr 11219  ax-i2m1 11220  ax-1ne0 11221  ax-1rid 11222  ax-rnegex 11223  ax-rrecex 11224  ax-cnre 11225  ax-pre-lttri 11226  ax-pre-lttrn 11227  ax-pre-ltadd 11228  ax-pre-mulgt0 11229  ax-pre-sup 11230
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-rmo 3377  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-int 4951  df-iun 4997  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5582  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-se 5641  df-we 5642  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-pred 6322  df-ord 6388  df-on 6389  df-lim 6390  df-suc 6391  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-isom 6571  df-riota 7387  df-ov 7433  df-oprab 7434  df-mpo 7435  df-om 7887  df-1st 8012  df-2nd 8013  df-frecs 8304  df-wrecs 8335  df-recs 8409  df-rdg 8448  df-1o 8504  df-oadd 8508  df-er 8743  df-en 8984  df-dom 8985  df-sdom 8986  df-fin 8987  df-sup 9479  df-oi 9547  df-dju 9938  df-card 9976  df-pnf 11294  df-mnf 11295  df-xr 11296  df-ltxr 11297  df-le 11298  df-sub 11491  df-neg 11492  df-div 11918  df-nn 12264  df-2 12326  df-3 12327  df-n0 12524  df-z 12611  df-uz 12876  df-rp 13032  df-ico 13389  df-fz 13544  df-fzo 13691  df-seq 14039  df-exp 14099  df-hash 14366  df-cj 15134  df-re 15135  df-im 15136  df-sqrt 15270  df-abs 15271  df-clim 15520  df-sum 15719
This theorem is referenced by:  climcnds  15883
  Copyright terms: Public domain W3C validator