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

Theorem climcndslem2 14507
Description: Lemma for climcnds 14508: bound the condensed series by the original 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
climcndslem2 ((𝜑𝑁 ∈ ℕ) → (seq1( + , 𝐺)‘𝑁) ≤ (2 · (seq1( + , 𝐹)‘(2↑𝑁))))
Distinct variable groups:   𝑘,𝑛,𝐹   𝑘,𝐺,𝑛   𝜑,𝑘,𝑛
Allowed substitution hints:   𝑁(𝑘,𝑛)

Proof of Theorem climcndslem2
Dummy variables 𝑗 𝑥 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fveq2 6148 . . . . 5 (𝑥 = 1 → (seq1( + , 𝐺)‘𝑥) = (seq1( + , 𝐺)‘1))
2 oveq2 6612 . . . . . . . 8 (𝑥 = 1 → (2↑𝑥) = (2↑1))
3 2cn 11035 . . . . . . . . 9 2 ∈ ℂ
4 exp1 12806 . . . . . . . . 9 (2 ∈ ℂ → (2↑1) = 2)
53, 4ax-mp 5 . . . . . . . 8 (2↑1) = 2
62, 5syl6eq 2671 . . . . . . 7 (𝑥 = 1 → (2↑𝑥) = 2)
76fveq2d 6152 . . . . . 6 (𝑥 = 1 → (seq1( + , 𝐹)‘(2↑𝑥)) = (seq1( + , 𝐹)‘2))
87oveq2d 6620 . . . . 5 (𝑥 = 1 → (2 · (seq1( + , 𝐹)‘(2↑𝑥))) = (2 · (seq1( + , 𝐹)‘2)))
91, 8breq12d 4626 . . . 4 (𝑥 = 1 → ((seq1( + , 𝐺)‘𝑥) ≤ (2 · (seq1( + , 𝐹)‘(2↑𝑥))) ↔ (seq1( + , 𝐺)‘1) ≤ (2 · (seq1( + , 𝐹)‘2))))
109imbi2d 330 . . 3 (𝑥 = 1 → ((𝜑 → (seq1( + , 𝐺)‘𝑥) ≤ (2 · (seq1( + , 𝐹)‘(2↑𝑥)))) ↔ (𝜑 → (seq1( + , 𝐺)‘1) ≤ (2 · (seq1( + , 𝐹)‘2)))))
11 fveq2 6148 . . . . 5 (𝑥 = 𝑗 → (seq1( + , 𝐺)‘𝑥) = (seq1( + , 𝐺)‘𝑗))
12 oveq2 6612 . . . . . . 7 (𝑥 = 𝑗 → (2↑𝑥) = (2↑𝑗))
1312fveq2d 6152 . . . . . 6 (𝑥 = 𝑗 → (seq1( + , 𝐹)‘(2↑𝑥)) = (seq1( + , 𝐹)‘(2↑𝑗)))
1413oveq2d 6620 . . . . 5 (𝑥 = 𝑗 → (2 · (seq1( + , 𝐹)‘(2↑𝑥))) = (2 · (seq1( + , 𝐹)‘(2↑𝑗))))
1511, 14breq12d 4626 . . . 4 (𝑥 = 𝑗 → ((seq1( + , 𝐺)‘𝑥) ≤ (2 · (seq1( + , 𝐹)‘(2↑𝑥))) ↔ (seq1( + , 𝐺)‘𝑗) ≤ (2 · (seq1( + , 𝐹)‘(2↑𝑗)))))
1615imbi2d 330 . . 3 (𝑥 = 𝑗 → ((𝜑 → (seq1( + , 𝐺)‘𝑥) ≤ (2 · (seq1( + , 𝐹)‘(2↑𝑥)))) ↔ (𝜑 → (seq1( + , 𝐺)‘𝑗) ≤ (2 · (seq1( + , 𝐹)‘(2↑𝑗))))))
17 fveq2 6148 . . . . 5 (𝑥 = (𝑗 + 1) → (seq1( + , 𝐺)‘𝑥) = (seq1( + , 𝐺)‘(𝑗 + 1)))
18 oveq2 6612 . . . . . . 7 (𝑥 = (𝑗 + 1) → (2↑𝑥) = (2↑(𝑗 + 1)))
1918fveq2d 6152 . . . . . 6 (𝑥 = (𝑗 + 1) → (seq1( + , 𝐹)‘(2↑𝑥)) = (seq1( + , 𝐹)‘(2↑(𝑗 + 1))))
2019oveq2d 6620 . . . . 5 (𝑥 = (𝑗 + 1) → (2 · (seq1( + , 𝐹)‘(2↑𝑥))) = (2 · (seq1( + , 𝐹)‘(2↑(𝑗 + 1)))))
2117, 20breq12d 4626 . . . 4 (𝑥 = (𝑗 + 1) → ((seq1( + , 𝐺)‘𝑥) ≤ (2 · (seq1( + , 𝐹)‘(2↑𝑥))) ↔ (seq1( + , 𝐺)‘(𝑗 + 1)) ≤ (2 · (seq1( + , 𝐹)‘(2↑(𝑗 + 1))))))
2221imbi2d 330 . . 3 (𝑥 = (𝑗 + 1) → ((𝜑 → (seq1( + , 𝐺)‘𝑥) ≤ (2 · (seq1( + , 𝐹)‘(2↑𝑥)))) ↔ (𝜑 → (seq1( + , 𝐺)‘(𝑗 + 1)) ≤ (2 · (seq1( + , 𝐹)‘(2↑(𝑗 + 1)))))))
23 fveq2 6148 . . . . 5 (𝑥 = 𝑁 → (seq1( + , 𝐺)‘𝑥) = (seq1( + , 𝐺)‘𝑁))
24 oveq2 6612 . . . . . . 7 (𝑥 = 𝑁 → (2↑𝑥) = (2↑𝑁))
2524fveq2d 6152 . . . . . 6 (𝑥 = 𝑁 → (seq1( + , 𝐹)‘(2↑𝑥)) = (seq1( + , 𝐹)‘(2↑𝑁)))
2625oveq2d 6620 . . . . 5 (𝑥 = 𝑁 → (2 · (seq1( + , 𝐹)‘(2↑𝑥))) = (2 · (seq1( + , 𝐹)‘(2↑𝑁))))
2723, 26breq12d 4626 . . . 4 (𝑥 = 𝑁 → ((seq1( + , 𝐺)‘𝑥) ≤ (2 · (seq1( + , 𝐹)‘(2↑𝑥))) ↔ (seq1( + , 𝐺)‘𝑁) ≤ (2 · (seq1( + , 𝐹)‘(2↑𝑁)))))
2827imbi2d 330 . . 3 (𝑥 = 𝑁 → ((𝜑 → (seq1( + , 𝐺)‘𝑥) ≤ (2 · (seq1( + , 𝐹)‘(2↑𝑥)))) ↔ (𝜑 → (seq1( + , 𝐺)‘𝑁) ≤ (2 · (seq1( + , 𝐹)‘(2↑𝑁))))))
29 1nn 10975 . . . . . . 7 1 ∈ ℕ
30 climcnds.2 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ) → 0 ≤ (𝐹𝑘))
3130ralrimiva 2960 . . . . . . 7 (𝜑 → ∀𝑘 ∈ ℕ 0 ≤ (𝐹𝑘))
32 fveq2 6148 . . . . . . . . 9 (𝑘 = 1 → (𝐹𝑘) = (𝐹‘1))
3332breq2d 4625 . . . . . . . 8 (𝑘 = 1 → (0 ≤ (𝐹𝑘) ↔ 0 ≤ (𝐹‘1)))
3433rspcv 3291 . . . . . . 7 (1 ∈ ℕ → (∀𝑘 ∈ ℕ 0 ≤ (𝐹𝑘) → 0 ≤ (𝐹‘1)))
3529, 31, 34mpsyl 68 . . . . . 6 (𝜑 → 0 ≤ (𝐹‘1))
36 2nn 11129 . . . . . . . 8 2 ∈ ℕ
37 climcnds.1 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ) → (𝐹𝑘) ∈ ℝ)
3837ralrimiva 2960 . . . . . . . 8 (𝜑 → ∀𝑘 ∈ ℕ (𝐹𝑘) ∈ ℝ)
39 fveq2 6148 . . . . . . . . . 10 (𝑘 = 2 → (𝐹𝑘) = (𝐹‘2))
4039eleq1d 2683 . . . . . . . . 9 (𝑘 = 2 → ((𝐹𝑘) ∈ ℝ ↔ (𝐹‘2) ∈ ℝ))
4140rspcv 3291 . . . . . . . 8 (2 ∈ ℕ → (∀𝑘 ∈ ℕ (𝐹𝑘) ∈ ℝ → (𝐹‘2) ∈ ℝ))
4236, 38, 41mpsyl 68 . . . . . . 7 (𝜑 → (𝐹‘2) ∈ ℝ)
4332eleq1d 2683 . . . . . . . . 9 (𝑘 = 1 → ((𝐹𝑘) ∈ ℝ ↔ (𝐹‘1) ∈ ℝ))
4443rspcv 3291 . . . . . . . 8 (1 ∈ ℕ → (∀𝑘 ∈ ℕ (𝐹𝑘) ∈ ℝ → (𝐹‘1) ∈ ℝ))
4529, 38, 44mpsyl 68 . . . . . . 7 (𝜑 → (𝐹‘1) ∈ ℝ)
4642, 45addge02d 10560 . . . . . 6 (𝜑 → (0 ≤ (𝐹‘1) ↔ (𝐹‘2) ≤ ((𝐹‘1) + (𝐹‘2))))
4735, 46mpbid 222 . . . . 5 (𝜑 → (𝐹‘2) ≤ ((𝐹‘1) + (𝐹‘2)))
4845, 42readdcld 10013 . . . . . 6 (𝜑 → ((𝐹‘1) + (𝐹‘2)) ∈ ℝ)
49 2re 11034 . . . . . . . 8 2 ∈ ℝ
50 2pos 11056 . . . . . . . 8 0 < 2
5149, 50pm3.2i 471 . . . . . . 7 (2 ∈ ℝ ∧ 0 < 2)
5251a1i 11 . . . . . 6 (𝜑 → (2 ∈ ℝ ∧ 0 < 2))
53 lemul2 10820 . . . . . 6 (((𝐹‘2) ∈ ℝ ∧ ((𝐹‘1) + (𝐹‘2)) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((𝐹‘2) ≤ ((𝐹‘1) + (𝐹‘2)) ↔ (2 · (𝐹‘2)) ≤ (2 · ((𝐹‘1) + (𝐹‘2)))))
5442, 48, 52, 53syl3anc 1323 . . . . 5 (𝜑 → ((𝐹‘2) ≤ ((𝐹‘1) + (𝐹‘2)) ↔ (2 · (𝐹‘2)) ≤ (2 · ((𝐹‘1) + (𝐹‘2)))))
5547, 54mpbid 222 . . . 4 (𝜑 → (2 · (𝐹‘2)) ≤ (2 · ((𝐹‘1) + (𝐹‘2))))
56 1z 11351 . . . . 5 1 ∈ ℤ
57 1nn0 11252 . . . . . 6 1 ∈ ℕ0
58 climcnds.4 . . . . . . 7 ((𝜑𝑛 ∈ ℕ0) → (𝐺𝑛) = ((2↑𝑛) · (𝐹‘(2↑𝑛))))
5958ralrimiva 2960 . . . . . 6 (𝜑 → ∀𝑛 ∈ ℕ0 (𝐺𝑛) = ((2↑𝑛) · (𝐹‘(2↑𝑛))))
60 fveq2 6148 . . . . . . . 8 (𝑛 = 1 → (𝐺𝑛) = (𝐺‘1))
61 oveq2 6612 . . . . . . . . . 10 (𝑛 = 1 → (2↑𝑛) = (2↑1))
6261, 5syl6eq 2671 . . . . . . . . 9 (𝑛 = 1 → (2↑𝑛) = 2)
6362fveq2d 6152 . . . . . . . . 9 (𝑛 = 1 → (𝐹‘(2↑𝑛)) = (𝐹‘2))
6462, 63oveq12d 6622 . . . . . . . 8 (𝑛 = 1 → ((2↑𝑛) · (𝐹‘(2↑𝑛))) = (2 · (𝐹‘2)))
6560, 64eqeq12d 2636 . . . . . . 7 (𝑛 = 1 → ((𝐺𝑛) = ((2↑𝑛) · (𝐹‘(2↑𝑛))) ↔ (𝐺‘1) = (2 · (𝐹‘2))))
6665rspcv 3291 . . . . . 6 (1 ∈ ℕ0 → (∀𝑛 ∈ ℕ0 (𝐺𝑛) = ((2↑𝑛) · (𝐹‘(2↑𝑛))) → (𝐺‘1) = (2 · (𝐹‘2))))
6757, 59, 66mpsyl 68 . . . . 5 (𝜑 → (𝐺‘1) = (2 · (𝐹‘2)))
6856, 67seq1i 12755 . . . 4 (𝜑 → (seq1( + , 𝐺)‘1) = (2 · (𝐹‘2)))
69 nnuz 11667 . . . . . 6 ℕ = (ℤ‘1)
70 df-2 11023 . . . . . 6 2 = (1 + 1)
71 eqidd 2622 . . . . . . 7 (𝜑 → (𝐹‘1) = (𝐹‘1))
7256, 71seq1i 12755 . . . . . 6 (𝜑 → (seq1( + , 𝐹)‘1) = (𝐹‘1))
73 eqidd 2622 . . . . . 6 (𝜑 → (𝐹‘2) = (𝐹‘2))
7469, 29, 70, 72, 73seqp1i 12757 . . . . 5 (𝜑 → (seq1( + , 𝐹)‘2) = ((𝐹‘1) + (𝐹‘2)))
7574oveq2d 6620 . . . 4 (𝜑 → (2 · (seq1( + , 𝐹)‘2)) = (2 · ((𝐹‘1) + (𝐹‘2))))
7655, 68, 753brtr4d 4645 . . 3 (𝜑 → (seq1( + , 𝐺)‘1) ≤ (2 · (seq1( + , 𝐹)‘2)))
77 peano2nn 10976 . . . . . . . . . . . 12 (𝑗 ∈ ℕ → (𝑗 + 1) ∈ ℕ)
7877adantl 482 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ℕ) → (𝑗 + 1) ∈ ℕ)
7978nnnn0d 11295 . . . . . . . . . 10 ((𝜑𝑗 ∈ ℕ) → (𝑗 + 1) ∈ ℕ0)
8059adantr 481 . . . . . . . . . 10 ((𝜑𝑗 ∈ ℕ) → ∀𝑛 ∈ ℕ0 (𝐺𝑛) = ((2↑𝑛) · (𝐹‘(2↑𝑛))))
81 fveq2 6148 . . . . . . . . . . . 12 (𝑛 = (𝑗 + 1) → (𝐺𝑛) = (𝐺‘(𝑗 + 1)))
82 oveq2 6612 . . . . . . . . . . . . 13 (𝑛 = (𝑗 + 1) → (2↑𝑛) = (2↑(𝑗 + 1)))
8382fveq2d 6152 . . . . . . . . . . . . 13 (𝑛 = (𝑗 + 1) → (𝐹‘(2↑𝑛)) = (𝐹‘(2↑(𝑗 + 1))))
8482, 83oveq12d 6622 . . . . . . . . . . . 12 (𝑛 = (𝑗 + 1) → ((2↑𝑛) · (𝐹‘(2↑𝑛))) = ((2↑(𝑗 + 1)) · (𝐹‘(2↑(𝑗 + 1)))))
8581, 84eqeq12d 2636 . . . . . . . . . . 11 (𝑛 = (𝑗 + 1) → ((𝐺𝑛) = ((2↑𝑛) · (𝐹‘(2↑𝑛))) ↔ (𝐺‘(𝑗 + 1)) = ((2↑(𝑗 + 1)) · (𝐹‘(2↑(𝑗 + 1))))))
8685rspcv 3291 . . . . . . . . . 10 ((𝑗 + 1) ∈ ℕ0 → (∀𝑛 ∈ ℕ0 (𝐺𝑛) = ((2↑𝑛) · (𝐹‘(2↑𝑛))) → (𝐺‘(𝑗 + 1)) = ((2↑(𝑗 + 1)) · (𝐹‘(2↑(𝑗 + 1))))))
8779, 80, 86sylc 65 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ) → (𝐺‘(𝑗 + 1)) = ((2↑(𝑗 + 1)) · (𝐹‘(2↑(𝑗 + 1)))))
88 nnnn0 11243 . . . . . . . . . . . . 13 (𝑗 ∈ ℕ → 𝑗 ∈ ℕ0)
8988adantl 482 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ) → 𝑗 ∈ ℕ0)
90 expp1 12807 . . . . . . . . . . . 12 ((2 ∈ ℂ ∧ 𝑗 ∈ ℕ0) → (2↑(𝑗 + 1)) = ((2↑𝑗) · 2))
913, 89, 90sylancr 694 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ℕ) → (2↑(𝑗 + 1)) = ((2↑𝑗) · 2))
92 nnexpcl 12813 . . . . . . . . . . . . . . 15 ((2 ∈ ℕ ∧ 𝑗 ∈ ℕ0) → (2↑𝑗) ∈ ℕ)
9336, 88, 92sylancr 694 . . . . . . . . . . . . . 14 (𝑗 ∈ ℕ → (2↑𝑗) ∈ ℕ)
9493adantl 482 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ ℕ) → (2↑𝑗) ∈ ℕ)
9594nncnd 10980 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ) → (2↑𝑗) ∈ ℂ)
96 mulcom 9966 . . . . . . . . . . . 12 (((2↑𝑗) ∈ ℂ ∧ 2 ∈ ℂ) → ((2↑𝑗) · 2) = (2 · (2↑𝑗)))
9795, 3, 96sylancl 693 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ℕ) → ((2↑𝑗) · 2) = (2 · (2↑𝑗)))
9891, 97eqtrd 2655 . . . . . . . . . 10 ((𝜑𝑗 ∈ ℕ) → (2↑(𝑗 + 1)) = (2 · (2↑𝑗)))
9998oveq1d 6619 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ) → ((2↑(𝑗 + 1)) · (𝐹‘(2↑(𝑗 + 1)))) = ((2 · (2↑𝑗)) · (𝐹‘(2↑(𝑗 + 1)))))
1003a1i 11 . . . . . . . . . 10 ((𝜑𝑗 ∈ ℕ) → 2 ∈ ℂ)
101 nnexpcl 12813 . . . . . . . . . . . . 13 ((2 ∈ ℕ ∧ (𝑗 + 1) ∈ ℕ0) → (2↑(𝑗 + 1)) ∈ ℕ)
10236, 79, 101sylancr 694 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ) → (2↑(𝑗 + 1)) ∈ ℕ)
10338adantr 481 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ) → ∀𝑘 ∈ ℕ (𝐹𝑘) ∈ ℝ)
104 fveq2 6148 . . . . . . . . . . . . . 14 (𝑘 = (2↑(𝑗 + 1)) → (𝐹𝑘) = (𝐹‘(2↑(𝑗 + 1))))
105104eleq1d 2683 . . . . . . . . . . . . 13 (𝑘 = (2↑(𝑗 + 1)) → ((𝐹𝑘) ∈ ℝ ↔ (𝐹‘(2↑(𝑗 + 1))) ∈ ℝ))
106105rspcv 3291 . . . . . . . . . . . 12 ((2↑(𝑗 + 1)) ∈ ℕ → (∀𝑘 ∈ ℕ (𝐹𝑘) ∈ ℝ → (𝐹‘(2↑(𝑗 + 1))) ∈ ℝ))
107102, 103, 106sylc 65 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ℕ) → (𝐹‘(2↑(𝑗 + 1))) ∈ ℝ)
108107recnd 10012 . . . . . . . . . 10 ((𝜑𝑗 ∈ ℕ) → (𝐹‘(2↑(𝑗 + 1))) ∈ ℂ)
109100, 95, 108mulassd 10007 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ) → ((2 · (2↑𝑗)) · (𝐹‘(2↑(𝑗 + 1)))) = (2 · ((2↑𝑗) · (𝐹‘(2↑(𝑗 + 1))))))
11087, 99, 1093eqtrd 2659 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ) → (𝐺‘(𝑗 + 1)) = (2 · ((2↑𝑗) · (𝐹‘(2↑(𝑗 + 1))))))
11194nnnn0d 11295 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ ℕ) → (2↑𝑗) ∈ ℕ0)
112 hashfz1 13074 . . . . . . . . . . . . . . 15 ((2↑𝑗) ∈ ℕ0 → (#‘(1...(2↑𝑗))) = (2↑𝑗))
113111, 112syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ ℕ) → (#‘(1...(2↑𝑗))) = (2↑𝑗))
114113, 95eqeltrd 2698 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ ℕ) → (#‘(1...(2↑𝑗))) ∈ ℂ)
115 fzfid 12712 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ ℕ) → (((2↑𝑗) + 1)...(2↑(𝑗 + 1))) ∈ Fin)
116 hashcl 13087 . . . . . . . . . . . . . . 15 ((((2↑𝑗) + 1)...(2↑(𝑗 + 1))) ∈ Fin → (#‘(((2↑𝑗) + 1)...(2↑(𝑗 + 1)))) ∈ ℕ0)
117115, 116syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ ℕ) → (#‘(((2↑𝑗) + 1)...(2↑(𝑗 + 1)))) ∈ ℕ0)
118117nn0cnd 11297 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ ℕ) → (#‘(((2↑𝑗) + 1)...(2↑(𝑗 + 1)))) ∈ ℂ)
119 simpr 477 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ ℕ) → 𝑗 ∈ ℕ)
120119nnzd 11425 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ ℕ) → 𝑗 ∈ ℤ)
121 uzid 11646 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ ℤ → 𝑗 ∈ (ℤ𝑗))
122 peano2uz 11685 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (ℤ𝑗) → (𝑗 + 1) ∈ (ℤ𝑗))
123 1le2 11185 . . . . . . . . . . . . . . . . . . 19 1 ≤ 2
124 leexp2a 12856 . . . . . . . . . . . . . . . . . . 19 ((2 ∈ ℝ ∧ 1 ≤ 2 ∧ (𝑗 + 1) ∈ (ℤ𝑗)) → (2↑𝑗) ≤ (2↑(𝑗 + 1)))
12549, 123, 124mp3an12 1411 . . . . . . . . . . . . . . . . . 18 ((𝑗 + 1) ∈ (ℤ𝑗) → (2↑𝑗) ≤ (2↑(𝑗 + 1)))
126120, 121, 122, 1254syl 19 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ ℕ) → (2↑𝑗) ≤ (2↑(𝑗 + 1)))
12794, 69syl6eleq 2708 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ ℕ) → (2↑𝑗) ∈ (ℤ‘1))
128102nnzd 11425 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ ℕ) → (2↑(𝑗 + 1)) ∈ ℤ)
129 elfz5 12276 . . . . . . . . . . . . . . . . . 18 (((2↑𝑗) ∈ (ℤ‘1) ∧ (2↑(𝑗 + 1)) ∈ ℤ) → ((2↑𝑗) ∈ (1...(2↑(𝑗 + 1))) ↔ (2↑𝑗) ≤ (2↑(𝑗 + 1))))
130127, 128, 129syl2anc 692 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ ℕ) → ((2↑𝑗) ∈ (1...(2↑(𝑗 + 1))) ↔ (2↑𝑗) ≤ (2↑(𝑗 + 1))))
131126, 130mpbird 247 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ ℕ) → (2↑𝑗) ∈ (1...(2↑(𝑗 + 1))))
132 fzsplit 12309 . . . . . . . . . . . . . . . 16 ((2↑𝑗) ∈ (1...(2↑(𝑗 + 1))) → (1...(2↑(𝑗 + 1))) = ((1...(2↑𝑗)) ∪ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))))
133131, 132syl 17 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ ℕ) → (1...(2↑(𝑗 + 1))) = ((1...(2↑𝑗)) ∪ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))))
134133fveq2d 6152 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ ℕ) → (#‘(1...(2↑(𝑗 + 1)))) = (#‘((1...(2↑𝑗)) ∪ (((2↑𝑗) + 1)...(2↑(𝑗 + 1))))))
13595times2d 11220 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ ℕ) → ((2↑𝑗) · 2) = ((2↑𝑗) + (2↑𝑗)))
13691, 135eqtrd 2655 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ ℕ) → (2↑(𝑗 + 1)) = ((2↑𝑗) + (2↑𝑗)))
137102nnnn0d 11295 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ ℕ) → (2↑(𝑗 + 1)) ∈ ℕ0)
138 hashfz1 13074 . . . . . . . . . . . . . . . 16 ((2↑(𝑗 + 1)) ∈ ℕ0 → (#‘(1...(2↑(𝑗 + 1)))) = (2↑(𝑗 + 1)))
139137, 138syl 17 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ ℕ) → (#‘(1...(2↑(𝑗 + 1)))) = (2↑(𝑗 + 1)))
140113oveq1d 6619 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ ℕ) → ((#‘(1...(2↑𝑗))) + (2↑𝑗)) = ((2↑𝑗) + (2↑𝑗)))
141136, 139, 1403eqtr4d 2665 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ ℕ) → (#‘(1...(2↑(𝑗 + 1)))) = ((#‘(1...(2↑𝑗))) + (2↑𝑗)))
142 fzfid 12712 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ ℕ) → (1...(2↑𝑗)) ∈ Fin)
14394nnred 10979 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ ℕ) → (2↑𝑗) ∈ ℝ)
144143ltp1d 10898 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ ℕ) → (2↑𝑗) < ((2↑𝑗) + 1))
145 fzdisj 12310 . . . . . . . . . . . . . . . 16 ((2↑𝑗) < ((2↑𝑗) + 1) → ((1...(2↑𝑗)) ∩ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))) = ∅)
146144, 145syl 17 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ ℕ) → ((1...(2↑𝑗)) ∩ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))) = ∅)
147 hashun 13111 . . . . . . . . . . . . . . 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))))))
148142, 115, 146, 147syl3anc 1323 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ ℕ) → (#‘((1...(2↑𝑗)) ∪ (((2↑𝑗) + 1)...(2↑(𝑗 + 1))))) = ((#‘(1...(2↑𝑗))) + (#‘(((2↑𝑗) + 1)...(2↑(𝑗 + 1))))))
149134, 141, 1483eqtr3d 2663 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ ℕ) → ((#‘(1...(2↑𝑗))) + (2↑𝑗)) = ((#‘(1...(2↑𝑗))) + (#‘(((2↑𝑗) + 1)...(2↑(𝑗 + 1))))))
150114, 95, 118, 149addcanad 10185 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ) → (2↑𝑗) = (#‘(((2↑𝑗) + 1)...(2↑(𝑗 + 1)))))
151150oveq1d 6619 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ℕ) → ((2↑𝑗) · (𝐹‘(2↑(𝑗 + 1)))) = ((#‘(((2↑𝑗) + 1)...(2↑(𝑗 + 1)))) · (𝐹‘(2↑(𝑗 + 1)))))
152 fsumconst 14450 . . . . . . . . . . . 12 (((((2↑𝑗) + 1)...(2↑(𝑗 + 1))) ∈ Fin ∧ (𝐹‘(2↑(𝑗 + 1))) ∈ ℂ) → Σ𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))(𝐹‘(2↑(𝑗 + 1))) = ((#‘(((2↑𝑗) + 1)...(2↑(𝑗 + 1)))) · (𝐹‘(2↑(𝑗 + 1)))))
153115, 108, 152syl2anc 692 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ℕ) → Σ𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))(𝐹‘(2↑(𝑗 + 1))) = ((#‘(((2↑𝑗) + 1)...(2↑(𝑗 + 1)))) · (𝐹‘(2↑(𝑗 + 1)))))
154151, 153eqtr4d 2658 . . . . . . . . . 10 ((𝜑𝑗 ∈ ℕ) → ((2↑𝑗) · (𝐹‘(2↑(𝑗 + 1)))) = Σ𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))(𝐹‘(2↑(𝑗 + 1))))
155107adantr 481 . . . . . . . . . . 11 (((𝜑𝑗 ∈ ℕ) ∧ 𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))) → (𝐹‘(2↑(𝑗 + 1))) ∈ ℝ)
156 simpl 473 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ ℕ) → 𝜑)
157156adantr 481 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ ℕ) ∧ 𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))) → 𝜑)
158 peano2nn 10976 . . . . . . . . . . . . . 14 ((2↑𝑗) ∈ ℕ → ((2↑𝑗) + 1) ∈ ℕ)
15994, 158syl 17 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ ℕ) → ((2↑𝑗) + 1) ∈ ℕ)
160 elfzuz 12280 . . . . . . . . . . . . 13 (𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1))) → 𝑘 ∈ (ℤ‘((2↑𝑗) + 1)))
161 eluznn 11702 . . . . . . . . . . . . 13 ((((2↑𝑗) + 1) ∈ ℕ ∧ 𝑘 ∈ (ℤ‘((2↑𝑗) + 1))) → 𝑘 ∈ ℕ)
162159, 160, 161syl2an 494 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ ℕ) ∧ 𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))) → 𝑘 ∈ ℕ)
163157, 162, 37syl2anc 692 . . . . . . . . . . 11 (((𝜑𝑗 ∈ ℕ) ∧ 𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))) → (𝐹𝑘) ∈ ℝ)
164 elfzuz3 12281 . . . . . . . . . . . . . . 15 (𝑛 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1))) → (2↑(𝑗 + 1)) ∈ (ℤ𝑛))
165164adantl 482 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ ℕ) ∧ 𝑛 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))) → (2↑(𝑗 + 1)) ∈ (ℤ𝑛))
166 simplll 797 . . . . . . . . . . . . . . 15 ((((𝜑𝑗 ∈ ℕ) ∧ 𝑛 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))) ∧ 𝑘 ∈ (𝑛...(2↑(𝑗 + 1)))) → 𝜑)
167 elfzuz 12280 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1))) → 𝑛 ∈ (ℤ‘((2↑𝑗) + 1)))
168 eluznn 11702 . . . . . . . . . . . . . . . . 17 ((((2↑𝑗) + 1) ∈ ℕ ∧ 𝑛 ∈ (ℤ‘((2↑𝑗) + 1))) → 𝑛 ∈ ℕ)
169159, 167, 168syl2an 494 . . . . . . . . . . . . . . . 16 (((𝜑𝑗 ∈ ℕ) ∧ 𝑛 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))) → 𝑛 ∈ ℕ)
170 elfzuz 12280 . . . . . . . . . . . . . . . 16 (𝑘 ∈ (𝑛...(2↑(𝑗 + 1))) → 𝑘 ∈ (ℤ𝑛))
171 eluznn 11702 . . . . . . . . . . . . . . . 16 ((𝑛 ∈ ℕ ∧ 𝑘 ∈ (ℤ𝑛)) → 𝑘 ∈ ℕ)
172169, 170, 171syl2an 494 . . . . . . . . . . . . . . 15 ((((𝜑𝑗 ∈ ℕ) ∧ 𝑛 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))) ∧ 𝑘 ∈ (𝑛...(2↑(𝑗 + 1)))) → 𝑘 ∈ ℕ)
173166, 172, 37syl2anc 692 . . . . . . . . . . . . . 14 ((((𝜑𝑗 ∈ ℕ) ∧ 𝑛 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))) ∧ 𝑘 ∈ (𝑛...(2↑(𝑗 + 1)))) → (𝐹𝑘) ∈ ℝ)
174 simplll 797 . . . . . . . . . . . . . . 15 ((((𝜑𝑗 ∈ ℕ) ∧ 𝑛 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))) ∧ 𝑘 ∈ (𝑛...((2↑(𝑗 + 1)) − 1))) → 𝜑)
175 elfzuz 12280 . . . . . . . . . . . . . . . 16 (𝑘 ∈ (𝑛...((2↑(𝑗 + 1)) − 1)) → 𝑘 ∈ (ℤ𝑛))
176169, 175, 171syl2an 494 . . . . . . . . . . . . . . 15 ((((𝜑𝑗 ∈ ℕ) ∧ 𝑛 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))) ∧ 𝑘 ∈ (𝑛...((2↑(𝑗 + 1)) − 1))) → 𝑘 ∈ ℕ)
177 climcnds.3 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ ℕ) → (𝐹‘(𝑘 + 1)) ≤ (𝐹𝑘))
178174, 176, 177syl2anc 692 . . . . . . . . . . . . . 14 ((((𝜑𝑗 ∈ ℕ) ∧ 𝑛 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))) ∧ 𝑘 ∈ (𝑛...((2↑(𝑗 + 1)) − 1))) → (𝐹‘(𝑘 + 1)) ≤ (𝐹𝑘))
179165, 173, 178monoord2 12772 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ ℕ) ∧ 𝑛 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))) → (𝐹‘(2↑(𝑗 + 1))) ≤ (𝐹𝑛))
180179ralrimiva 2960 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ) → ∀𝑛 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))(𝐹‘(2↑(𝑗 + 1))) ≤ (𝐹𝑛))
181 fveq2 6148 . . . . . . . . . . . . . 14 (𝑛 = 𝑘 → (𝐹𝑛) = (𝐹𝑘))
182181breq2d 4625 . . . . . . . . . . . . 13 (𝑛 = 𝑘 → ((𝐹‘(2↑(𝑗 + 1))) ≤ (𝐹𝑛) ↔ (𝐹‘(2↑(𝑗 + 1))) ≤ (𝐹𝑘)))
183182rspccva 3294 . . . . . . . . . . . 12 ((∀𝑛 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))(𝐹‘(2↑(𝑗 + 1))) ≤ (𝐹𝑛) ∧ 𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))) → (𝐹‘(2↑(𝑗 + 1))) ≤ (𝐹𝑘))
184180, 183sylan 488 . . . . . . . . . . 11 (((𝜑𝑗 ∈ ℕ) ∧ 𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))) → (𝐹‘(2↑(𝑗 + 1))) ≤ (𝐹𝑘))
185115, 155, 163, 184fsumle 14458 . . . . . . . . . 10 ((𝜑𝑗 ∈ ℕ) → Σ𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))(𝐹‘(2↑(𝑗 + 1))) ≤ Σ𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))(𝐹𝑘))
186154, 185eqbrtrd 4635 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ) → ((2↑𝑗) · (𝐹‘(2↑(𝑗 + 1)))) ≤ Σ𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))(𝐹𝑘))
187143, 107remulcld 10014 . . . . . . . . . 10 ((𝜑𝑗 ∈ ℕ) → ((2↑𝑗) · (𝐹‘(2↑(𝑗 + 1)))) ∈ ℝ)
188115, 163fsumrecl 14398 . . . . . . . . . 10 ((𝜑𝑗 ∈ ℕ) → Σ𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))(𝐹𝑘) ∈ ℝ)
18951a1i 11 . . . . . . . . . 10 ((𝜑𝑗 ∈ ℕ) → (2 ∈ ℝ ∧ 0 < 2))
190 lemul2 10820 . . . . . . . . . 10 ((((2↑𝑗) · (𝐹‘(2↑(𝑗 + 1)))) ∈ ℝ ∧ Σ𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))(𝐹𝑘) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → (((2↑𝑗) · (𝐹‘(2↑(𝑗 + 1)))) ≤ Σ𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))(𝐹𝑘) ↔ (2 · ((2↑𝑗) · (𝐹‘(2↑(𝑗 + 1))))) ≤ (2 · Σ𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))(𝐹𝑘))))
191187, 188, 189, 190syl3anc 1323 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ) → (((2↑𝑗) · (𝐹‘(2↑(𝑗 + 1)))) ≤ Σ𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))(𝐹𝑘) ↔ (2 · ((2↑𝑗) · (𝐹‘(2↑(𝑗 + 1))))) ≤ (2 · Σ𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))(𝐹𝑘))))
192186, 191mpbid 222 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ) → (2 · ((2↑𝑗) · (𝐹‘(2↑(𝑗 + 1))))) ≤ (2 · Σ𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))(𝐹𝑘)))
193110, 192eqbrtrd 4635 . . . . . . 7 ((𝜑𝑗 ∈ ℕ) → (𝐺‘(𝑗 + 1)) ≤ (2 · Σ𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))(𝐹𝑘)))
194 1zzd 11352 . . . . . . . . . 10 (𝜑 → 1 ∈ ℤ)
195 nnnn0 11243 . . . . . . . . . . 11 (𝑛 ∈ ℕ → 𝑛 ∈ ℕ0)
196 simpr 477 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ0) → 𝑛 ∈ ℕ0)
197 nnexpcl 12813 . . . . . . . . . . . . . . 15 ((2 ∈ ℕ ∧ 𝑛 ∈ ℕ0) → (2↑𝑛) ∈ ℕ)
19836, 196, 197sylancr 694 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ ℕ0) → (2↑𝑛) ∈ ℕ)
199198nnred 10979 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ ℕ0) → (2↑𝑛) ∈ ℝ)
20038adantr 481 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ ℕ0) → ∀𝑘 ∈ ℕ (𝐹𝑘) ∈ ℝ)
201 fveq2 6148 . . . . . . . . . . . . . . . 16 (𝑘 = (2↑𝑛) → (𝐹𝑘) = (𝐹‘(2↑𝑛)))
202201eleq1d 2683 . . . . . . . . . . . . . . 15 (𝑘 = (2↑𝑛) → ((𝐹𝑘) ∈ ℝ ↔ (𝐹‘(2↑𝑛)) ∈ ℝ))
203202rspcv 3291 . . . . . . . . . . . . . 14 ((2↑𝑛) ∈ ℕ → (∀𝑘 ∈ ℕ (𝐹𝑘) ∈ ℝ → (𝐹‘(2↑𝑛)) ∈ ℝ))
204198, 200, 203sylc 65 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ ℕ0) → (𝐹‘(2↑𝑛)) ∈ ℝ)
205199, 204remulcld 10014 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ0) → ((2↑𝑛) · (𝐹‘(2↑𝑛))) ∈ ℝ)
20658, 205eqeltrd 2698 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ0) → (𝐺𝑛) ∈ ℝ)
207195, 206sylan2 491 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → (𝐺𝑛) ∈ ℝ)
20869, 194, 207serfre 12770 . . . . . . . . 9 (𝜑 → seq1( + , 𝐺):ℕ⟶ℝ)
209208ffvelrnda 6315 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ) → (seq1( + , 𝐺)‘𝑗) ∈ ℝ)
210207ralrimiva 2960 . . . . . . . . . 10 (𝜑 → ∀𝑛 ∈ ℕ (𝐺𝑛) ∈ ℝ)
211210adantr 481 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ) → ∀𝑛 ∈ ℕ (𝐺𝑛) ∈ ℝ)
21281eleq1d 2683 . . . . . . . . . 10 (𝑛 = (𝑗 + 1) → ((𝐺𝑛) ∈ ℝ ↔ (𝐺‘(𝑗 + 1)) ∈ ℝ))
213212rspcv 3291 . . . . . . . . 9 ((𝑗 + 1) ∈ ℕ → (∀𝑛 ∈ ℕ (𝐺𝑛) ∈ ℝ → (𝐺‘(𝑗 + 1)) ∈ ℝ))
21478, 211, 213sylc 65 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ) → (𝐺‘(𝑗 + 1)) ∈ ℝ)
21569, 194, 37serfre 12770 . . . . . . . . . 10 (𝜑 → seq1( + , 𝐹):ℕ⟶ℝ)
216 ffvelrn 6313 . . . . . . . . . 10 ((seq1( + , 𝐹):ℕ⟶ℝ ∧ (2↑𝑗) ∈ ℕ) → (seq1( + , 𝐹)‘(2↑𝑗)) ∈ ℝ)
217215, 93, 216syl2an 494 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ) → (seq1( + , 𝐹)‘(2↑𝑗)) ∈ ℝ)
218 remulcl 9965 . . . . . . . . 9 ((2 ∈ ℝ ∧ (seq1( + , 𝐹)‘(2↑𝑗)) ∈ ℝ) → (2 · (seq1( + , 𝐹)‘(2↑𝑗))) ∈ ℝ)
21949, 217, 218sylancr 694 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ) → (2 · (seq1( + , 𝐹)‘(2↑𝑗))) ∈ ℝ)
220 remulcl 9965 . . . . . . . . 9 ((2 ∈ ℝ ∧ Σ𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))(𝐹𝑘) ∈ ℝ) → (2 · Σ𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))(𝐹𝑘)) ∈ ℝ)
22149, 188, 220sylancr 694 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ) → (2 · Σ𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))(𝐹𝑘)) ∈ ℝ)
222 le2add 10454 . . . . . . . 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)))(𝐹𝑘)))))
223209, 214, 219, 221, 222syl22anc 1324 . . . . . . 7 ((𝜑𝑗 ∈ ℕ) → (((seq1( + , 𝐺)‘𝑗) ≤ (2 · (seq1( + , 𝐹)‘(2↑𝑗))) ∧ (𝐺‘(𝑗 + 1)) ≤ (2 · Σ𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))(𝐹𝑘))) → ((seq1( + , 𝐺)‘𝑗) + (𝐺‘(𝑗 + 1))) ≤ ((2 · (seq1( + , 𝐹)‘(2↑𝑗))) + (2 · Σ𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))(𝐹𝑘)))))
224193, 223mpan2d 709 . . . . . 6 ((𝜑𝑗 ∈ ℕ) → ((seq1( + , 𝐺)‘𝑗) ≤ (2 · (seq1( + , 𝐹)‘(2↑𝑗))) → ((seq1( + , 𝐺)‘𝑗) + (𝐺‘(𝑗 + 1))) ≤ ((2 · (seq1( + , 𝐹)‘(2↑𝑗))) + (2 · Σ𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))(𝐹𝑘)))))
225119, 69syl6eleq 2708 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ) → 𝑗 ∈ (ℤ‘1))
226 seqp1 12756 . . . . . . . 8 (𝑗 ∈ (ℤ‘1) → (seq1( + , 𝐺)‘(𝑗 + 1)) = ((seq1( + , 𝐺)‘𝑗) + (𝐺‘(𝑗 + 1))))
227225, 226syl 17 . . . . . . 7 ((𝜑𝑗 ∈ ℕ) → (seq1( + , 𝐺)‘(𝑗 + 1)) = ((seq1( + , 𝐺)‘𝑗) + (𝐺‘(𝑗 + 1))))
228 fzfid 12712 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ℕ) → (1...(2↑(𝑗 + 1))) ∈ Fin)
229 elfznn 12312 . . . . . . . . . . . 12 (𝑘 ∈ (1...(2↑(𝑗 + 1))) → 𝑘 ∈ ℕ)
23037recnd 10012 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ) → (𝐹𝑘) ∈ ℂ)
231156, 229, 230syl2an 494 . . . . . . . . . . 11 (((𝜑𝑗 ∈ ℕ) ∧ 𝑘 ∈ (1...(2↑(𝑗 + 1)))) → (𝐹𝑘) ∈ ℂ)
232146, 133, 228, 231fsumsplit 14404 . . . . . . . . . 10 ((𝜑𝑗 ∈ ℕ) → Σ𝑘 ∈ (1...(2↑(𝑗 + 1)))(𝐹𝑘) = (Σ𝑘 ∈ (1...(2↑𝑗))(𝐹𝑘) + Σ𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))(𝐹𝑘)))
233 eqidd 2622 . . . . . . . . . . 11 (((𝜑𝑗 ∈ ℕ) ∧ 𝑘 ∈ (1...(2↑(𝑗 + 1)))) → (𝐹𝑘) = (𝐹𝑘))
234102, 69syl6eleq 2708 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ℕ) → (2↑(𝑗 + 1)) ∈ (ℤ‘1))
235233, 234, 231fsumser 14394 . . . . . . . . . 10 ((𝜑𝑗 ∈ ℕ) → Σ𝑘 ∈ (1...(2↑(𝑗 + 1)))(𝐹𝑘) = (seq1( + , 𝐹)‘(2↑(𝑗 + 1))))
236 eqidd 2622 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ ℕ) ∧ 𝑘 ∈ (1...(2↑𝑗))) → (𝐹𝑘) = (𝐹𝑘))
237 elfznn 12312 . . . . . . . . . . . . 13 (𝑘 ∈ (1...(2↑𝑗)) → 𝑘 ∈ ℕ)
238156, 237, 230syl2an 494 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ ℕ) ∧ 𝑘 ∈ (1...(2↑𝑗))) → (𝐹𝑘) ∈ ℂ)
239236, 127, 238fsumser 14394 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ℕ) → Σ𝑘 ∈ (1...(2↑𝑗))(𝐹𝑘) = (seq1( + , 𝐹)‘(2↑𝑗)))
240239oveq1d 6619 . . . . . . . . . 10 ((𝜑𝑗 ∈ ℕ) → (Σ𝑘 ∈ (1...(2↑𝑗))(𝐹𝑘) + Σ𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))(𝐹𝑘)) = ((seq1( + , 𝐹)‘(2↑𝑗)) + Σ𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))(𝐹𝑘)))
241232, 235, 2403eqtr3d 2663 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ) → (seq1( + , 𝐹)‘(2↑(𝑗 + 1))) = ((seq1( + , 𝐹)‘(2↑𝑗)) + Σ𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))(𝐹𝑘)))
242241oveq2d 6620 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ) → (2 · (seq1( + , 𝐹)‘(2↑(𝑗 + 1)))) = (2 · ((seq1( + , 𝐹)‘(2↑𝑗)) + Σ𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))(𝐹𝑘))))
243217recnd 10012 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ) → (seq1( + , 𝐹)‘(2↑𝑗)) ∈ ℂ)
244188recnd 10012 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ) → Σ𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))(𝐹𝑘) ∈ ℂ)
245100, 243, 244adddid 10008 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ) → (2 · ((seq1( + , 𝐹)‘(2↑𝑗)) + Σ𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))(𝐹𝑘))) = ((2 · (seq1( + , 𝐹)‘(2↑𝑗))) + (2 · Σ𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))(𝐹𝑘))))
246242, 245eqtrd 2655 . . . . . . 7 ((𝜑𝑗 ∈ ℕ) → (2 · (seq1( + , 𝐹)‘(2↑(𝑗 + 1)))) = ((2 · (seq1( + , 𝐹)‘(2↑𝑗))) + (2 · Σ𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))(𝐹𝑘))))
247227, 246breq12d 4626 . . . . . 6 ((𝜑𝑗 ∈ ℕ) → ((seq1( + , 𝐺)‘(𝑗 + 1)) ≤ (2 · (seq1( + , 𝐹)‘(2↑(𝑗 + 1)))) ↔ ((seq1( + , 𝐺)‘𝑗) + (𝐺‘(𝑗 + 1))) ≤ ((2 · (seq1( + , 𝐹)‘(2↑𝑗))) + (2 · Σ𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))(𝐹𝑘)))))
248224, 247sylibrd 249 . . . . 5 ((𝜑𝑗 ∈ ℕ) → ((seq1( + , 𝐺)‘𝑗) ≤ (2 · (seq1( + , 𝐹)‘(2↑𝑗))) → (seq1( + , 𝐺)‘(𝑗 + 1)) ≤ (2 · (seq1( + , 𝐹)‘(2↑(𝑗 + 1))))))
249248expcom 451 . . . 4 (𝑗 ∈ ℕ → (𝜑 → ((seq1( + , 𝐺)‘𝑗) ≤ (2 · (seq1( + , 𝐹)‘(2↑𝑗))) → (seq1( + , 𝐺)‘(𝑗 + 1)) ≤ (2 · (seq1( + , 𝐹)‘(2↑(𝑗 + 1)))))))
250249a2d 29 . . 3 (𝑗 ∈ ℕ → ((𝜑 → (seq1( + , 𝐺)‘𝑗) ≤ (2 · (seq1( + , 𝐹)‘(2↑𝑗)))) → (𝜑 → (seq1( + , 𝐺)‘(𝑗 + 1)) ≤ (2 · (seq1( + , 𝐹)‘(2↑(𝑗 + 1)))))))
25110, 16, 22, 28, 76, 250nnind 10982 . 2 (𝑁 ∈ ℕ → (𝜑 → (seq1( + , 𝐺)‘𝑁) ≤ (2 · (seq1( + , 𝐹)‘(2↑𝑁)))))
252251impcom 446 1 ((𝜑𝑁 ∈ ℕ) → (seq1( + , 𝐺)‘𝑁) ≤ (2 · (seq1( + , 𝐹)‘(2↑𝑁))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384   = wceq 1480  wcel 1987  wral 2907  cun 3553  cin 3554  c0 3891   class class class wbr 4613  wf 5843  cfv 5847  (class class class)co 6604  Fincfn 7899  cc 9878  cr 9879  0cc0 9880  1c1 9881   + caddc 9883   · cmul 9885   < clt 10018  cle 10019  cmin 10210  cn 10964  2c2 11014  0cn0 11236  cz 11321  cuz 11631  ...cfz 12268  seqcseq 12741  cexp 12800  #chash 13057  Σcsu 14350
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4731  ax-sep 4741  ax-nul 4749  ax-pow 4803  ax-pr 4867  ax-un 6902  ax-inf2 8482  ax-cnex 9936  ax-resscn 9937  ax-1cn 9938  ax-icn 9939  ax-addcl 9940  ax-addrcl 9941  ax-mulcl 9942  ax-mulrcl 9943  ax-mulcom 9944  ax-addass 9945  ax-mulass 9946  ax-distr 9947  ax-i2m1 9948  ax-1ne0 9949  ax-1rid 9950  ax-rnegex 9951  ax-rrecex 9952  ax-cnre 9953  ax-pre-lttri 9954  ax-pre-lttrn 9955  ax-pre-ltadd 9956  ax-pre-mulgt0 9957  ax-pre-sup 9958
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-fal 1486  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2912  df-rex 2913  df-reu 2914  df-rmo 2915  df-rab 2916  df-v 3188  df-sbc 3418  df-csb 3515  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-pss 3571  df-nul 3892  df-if 4059  df-pw 4132  df-sn 4149  df-pr 4151  df-tp 4153  df-op 4155  df-uni 4403  df-int 4441  df-iun 4487  df-br 4614  df-opab 4674  df-mpt 4675  df-tr 4713  df-eprel 4985  df-id 4989  df-po 4995  df-so 4996  df-fr 5033  df-se 5034  df-we 5035  df-xp 5080  df-rel 5081  df-cnv 5082  df-co 5083  df-dm 5084  df-rn 5085  df-res 5086  df-ima 5087  df-pred 5639  df-ord 5685  df-on 5686  df-lim 5687  df-suc 5688  df-iota 5810  df-fun 5849  df-fn 5850  df-f 5851  df-f1 5852  df-fo 5853  df-f1o 5854  df-fv 5855  df-isom 5856  df-riota 6565  df-ov 6607  df-oprab 6608  df-mpt2 6609  df-om 7013  df-1st 7113  df-2nd 7114  df-wrecs 7352  df-recs 7413  df-rdg 7451  df-1o 7505  df-oadd 7509  df-er 7687  df-en 7900  df-dom 7901  df-sdom 7902  df-fin 7903  df-sup 8292  df-oi 8359  df-card 8709  df-cda 8934  df-pnf 10020  df-mnf 10021  df-xr 10022  df-ltxr 10023  df-le 10024  df-sub 10212  df-neg 10213  df-div 10629  df-nn 10965  df-2 11023  df-3 11024  df-n0 11237  df-z 11322  df-uz 11632  df-rp 11777  df-ico 12123  df-fz 12269  df-fzo 12407  df-seq 12742  df-exp 12801  df-hash 13058  df-cj 13773  df-re 13774  df-im 13775  df-sqrt 13909  df-abs 13910  df-clim 14153  df-sum 14351
This theorem is referenced by:  climcnds  14508
  Copyright terms: Public domain W3C validator