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

Theorem climcndslem2 15854
Description: Lemma for climcnds 15855: bound the condensed series by the original series. (Contributed by Mario Carneiro, 18-Jul-2014.) (Proof shortened by AV, 10-Jul-2022.)
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 6901 . . . . 5 (𝑥 = 1 → (seq1( + , 𝐺)‘𝑥) = (seq1( + , 𝐺)‘1))
2 oveq2 7432 . . . . . . . 8 (𝑥 = 1 → (2↑𝑥) = (2↑1))
3 2cn 12339 . . . . . . . . 9 2 ∈ ℂ
4 exp1 14087 . . . . . . . . 9 (2 ∈ ℂ → (2↑1) = 2)
53, 4ax-mp 5 . . . . . . . 8 (2↑1) = 2
62, 5eqtrdi 2782 . . . . . . 7 (𝑥 = 1 → (2↑𝑥) = 2)
76fveq2d 6905 . . . . . 6 (𝑥 = 1 → (seq1( + , 𝐹)‘(2↑𝑥)) = (seq1( + , 𝐹)‘2))
87oveq2d 7440 . . . . 5 (𝑥 = 1 → (2 · (seq1( + , 𝐹)‘(2↑𝑥))) = (2 · (seq1( + , 𝐹)‘2)))
91, 8breq12d 5166 . . . 4 (𝑥 = 1 → ((seq1( + , 𝐺)‘𝑥) ≤ (2 · (seq1( + , 𝐹)‘(2↑𝑥))) ↔ (seq1( + , 𝐺)‘1) ≤ (2 · (seq1( + , 𝐹)‘2))))
109imbi2d 339 . . 3 (𝑥 = 1 → ((𝜑 → (seq1( + , 𝐺)‘𝑥) ≤ (2 · (seq1( + , 𝐹)‘(2↑𝑥)))) ↔ (𝜑 → (seq1( + , 𝐺)‘1) ≤ (2 · (seq1( + , 𝐹)‘2)))))
11 fveq2 6901 . . . . 5 (𝑥 = 𝑗 → (seq1( + , 𝐺)‘𝑥) = (seq1( + , 𝐺)‘𝑗))
12 oveq2 7432 . . . . . . 7 (𝑥 = 𝑗 → (2↑𝑥) = (2↑𝑗))
1312fveq2d 6905 . . . . . 6 (𝑥 = 𝑗 → (seq1( + , 𝐹)‘(2↑𝑥)) = (seq1( + , 𝐹)‘(2↑𝑗)))
1413oveq2d 7440 . . . . 5 (𝑥 = 𝑗 → (2 · (seq1( + , 𝐹)‘(2↑𝑥))) = (2 · (seq1( + , 𝐹)‘(2↑𝑗))))
1511, 14breq12d 5166 . . . 4 (𝑥 = 𝑗 → ((seq1( + , 𝐺)‘𝑥) ≤ (2 · (seq1( + , 𝐹)‘(2↑𝑥))) ↔ (seq1( + , 𝐺)‘𝑗) ≤ (2 · (seq1( + , 𝐹)‘(2↑𝑗)))))
1615imbi2d 339 . . 3 (𝑥 = 𝑗 → ((𝜑 → (seq1( + , 𝐺)‘𝑥) ≤ (2 · (seq1( + , 𝐹)‘(2↑𝑥)))) ↔ (𝜑 → (seq1( + , 𝐺)‘𝑗) ≤ (2 · (seq1( + , 𝐹)‘(2↑𝑗))))))
17 fveq2 6901 . . . . 5 (𝑥 = (𝑗 + 1) → (seq1( + , 𝐺)‘𝑥) = (seq1( + , 𝐺)‘(𝑗 + 1)))
18 oveq2 7432 . . . . . . 7 (𝑥 = (𝑗 + 1) → (2↑𝑥) = (2↑(𝑗 + 1)))
1918fveq2d 6905 . . . . . 6 (𝑥 = (𝑗 + 1) → (seq1( + , 𝐹)‘(2↑𝑥)) = (seq1( + , 𝐹)‘(2↑(𝑗 + 1))))
2019oveq2d 7440 . . . . 5 (𝑥 = (𝑗 + 1) → (2 · (seq1( + , 𝐹)‘(2↑𝑥))) = (2 · (seq1( + , 𝐹)‘(2↑(𝑗 + 1)))))
2117, 20breq12d 5166 . . . 4 (𝑥 = (𝑗 + 1) → ((seq1( + , 𝐺)‘𝑥) ≤ (2 · (seq1( + , 𝐹)‘(2↑𝑥))) ↔ (seq1( + , 𝐺)‘(𝑗 + 1)) ≤ (2 · (seq1( + , 𝐹)‘(2↑(𝑗 + 1))))))
2221imbi2d 339 . . 3 (𝑥 = (𝑗 + 1) → ((𝜑 → (seq1( + , 𝐺)‘𝑥) ≤ (2 · (seq1( + , 𝐹)‘(2↑𝑥)))) ↔ (𝜑 → (seq1( + , 𝐺)‘(𝑗 + 1)) ≤ (2 · (seq1( + , 𝐹)‘(2↑(𝑗 + 1)))))))
23 fveq2 6901 . . . . 5 (𝑥 = 𝑁 → (seq1( + , 𝐺)‘𝑥) = (seq1( + , 𝐺)‘𝑁))
24 oveq2 7432 . . . . . . 7 (𝑥 = 𝑁 → (2↑𝑥) = (2↑𝑁))
2524fveq2d 6905 . . . . . 6 (𝑥 = 𝑁 → (seq1( + , 𝐹)‘(2↑𝑥)) = (seq1( + , 𝐹)‘(2↑𝑁)))
2625oveq2d 7440 . . . . 5 (𝑥 = 𝑁 → (2 · (seq1( + , 𝐹)‘(2↑𝑥))) = (2 · (seq1( + , 𝐹)‘(2↑𝑁))))
2723, 26breq12d 5166 . . . 4 (𝑥 = 𝑁 → ((seq1( + , 𝐺)‘𝑥) ≤ (2 · (seq1( + , 𝐹)‘(2↑𝑥))) ↔ (seq1( + , 𝐺)‘𝑁) ≤ (2 · (seq1( + , 𝐹)‘(2↑𝑁)))))
2827imbi2d 339 . . 3 (𝑥 = 𝑁 → ((𝜑 → (seq1( + , 𝐺)‘𝑥) ≤ (2 · (seq1( + , 𝐹)‘(2↑𝑥)))) ↔ (𝜑 → (seq1( + , 𝐺)‘𝑁) ≤ (2 · (seq1( + , 𝐹)‘(2↑𝑁))))))
29 fveq2 6901 . . . . . . . 8 (𝑘 = 1 → (𝐹𝑘) = (𝐹‘1))
3029breq2d 5165 . . . . . . 7 (𝑘 = 1 → (0 ≤ (𝐹𝑘) ↔ 0 ≤ (𝐹‘1)))
31 climcnds.2 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ) → 0 ≤ (𝐹𝑘))
3231ralrimiva 3136 . . . . . . 7 (𝜑 → ∀𝑘 ∈ ℕ 0 ≤ (𝐹𝑘))
33 1nn 12275 . . . . . . . 8 1 ∈ ℕ
3433a1i 11 . . . . . . 7 (𝜑 → 1 ∈ ℕ)
3530, 32, 34rspcdva 3609 . . . . . 6 (𝜑 → 0 ≤ (𝐹‘1))
36 fveq2 6901 . . . . . . . . 9 (𝑘 = 2 → (𝐹𝑘) = (𝐹‘2))
3736eleq1d 2811 . . . . . . . 8 (𝑘 = 2 → ((𝐹𝑘) ∈ ℝ ↔ (𝐹‘2) ∈ ℝ))
38 climcnds.1 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ) → (𝐹𝑘) ∈ ℝ)
3938ralrimiva 3136 . . . . . . . 8 (𝜑 → ∀𝑘 ∈ ℕ (𝐹𝑘) ∈ ℝ)
40 2nn 12337 . . . . . . . . 9 2 ∈ ℕ
4140a1i 11 . . . . . . . 8 (𝜑 → 2 ∈ ℕ)
4237, 39, 41rspcdva 3609 . . . . . . 7 (𝜑 → (𝐹‘2) ∈ ℝ)
4329eleq1d 2811 . . . . . . . 8 (𝑘 = 1 → ((𝐹𝑘) ∈ ℝ ↔ (𝐹‘1) ∈ ℝ))
4443, 39, 34rspcdva 3609 . . . . . . 7 (𝜑 → (𝐹‘1) ∈ ℝ)
4542, 44addge02d 11853 . . . . . 6 (𝜑 → (0 ≤ (𝐹‘1) ↔ (𝐹‘2) ≤ ((𝐹‘1) + (𝐹‘2))))
4635, 45mpbid 231 . . . . 5 (𝜑 → (𝐹‘2) ≤ ((𝐹‘1) + (𝐹‘2)))
4744, 42readdcld 11293 . . . . . 6 (𝜑 → ((𝐹‘1) + (𝐹‘2)) ∈ ℝ)
4841nnrpd 13068 . . . . . 6 (𝜑 → 2 ∈ ℝ+)
4942, 47, 48lemul2d 13114 . . . . 5 (𝜑 → ((𝐹‘2) ≤ ((𝐹‘1) + (𝐹‘2)) ↔ (2 · (𝐹‘2)) ≤ (2 · ((𝐹‘1) + (𝐹‘2)))))
5046, 49mpbid 231 . . . 4 (𝜑 → (2 · (𝐹‘2)) ≤ (2 · ((𝐹‘1) + (𝐹‘2))))
51 1z 12644 . . . . 5 1 ∈ ℤ
52 fveq2 6901 . . . . . . 7 (𝑛 = 1 → (𝐺𝑛) = (𝐺‘1))
53 oveq2 7432 . . . . . . . . 9 (𝑛 = 1 → (2↑𝑛) = (2↑1))
5453, 5eqtrdi 2782 . . . . . . . 8 (𝑛 = 1 → (2↑𝑛) = 2)
5554fveq2d 6905 . . . . . . . 8 (𝑛 = 1 → (𝐹‘(2↑𝑛)) = (𝐹‘2))
5654, 55oveq12d 7442 . . . . . . 7 (𝑛 = 1 → ((2↑𝑛) · (𝐹‘(2↑𝑛))) = (2 · (𝐹‘2)))
5752, 56eqeq12d 2742 . . . . . 6 (𝑛 = 1 → ((𝐺𝑛) = ((2↑𝑛) · (𝐹‘(2↑𝑛))) ↔ (𝐺‘1) = (2 · (𝐹‘2))))
58 climcnds.4 . . . . . . 7 ((𝜑𝑛 ∈ ℕ0) → (𝐺𝑛) = ((2↑𝑛) · (𝐹‘(2↑𝑛))))
5958ralrimiva 3136 . . . . . 6 (𝜑 → ∀𝑛 ∈ ℕ0 (𝐺𝑛) = ((2↑𝑛) · (𝐹‘(2↑𝑛))))
60 1nn0 12540 . . . . . . 7 1 ∈ ℕ0
6160a1i 11 . . . . . 6 (𝜑 → 1 ∈ ℕ0)
6257, 59, 61rspcdva 3609 . . . . 5 (𝜑 → (𝐺‘1) = (2 · (𝐹‘2)))
6351, 62seq1i 14035 . . . 4 (𝜑 → (seq1( + , 𝐺)‘1) = (2 · (𝐹‘2)))
64 nnuz 12917 . . . . . 6 ℕ = (ℤ‘1)
65 df-2 12327 . . . . . 6 2 = (1 + 1)
66 eqidd 2727 . . . . . . 7 (𝜑 → (𝐹‘1) = (𝐹‘1))
6751, 66seq1i 14035 . . . . . 6 (𝜑 → (seq1( + , 𝐹)‘1) = (𝐹‘1))
68 eqidd 2727 . . . . . 6 (𝜑 → (𝐹‘2) = (𝐹‘2))
6964, 34, 65, 67, 68seqp1d 14038 . . . . 5 (𝜑 → (seq1( + , 𝐹)‘2) = ((𝐹‘1) + (𝐹‘2)))
7069oveq2d 7440 . . . 4 (𝜑 → (2 · (seq1( + , 𝐹)‘2)) = (2 · ((𝐹‘1) + (𝐹‘2))))
7150, 63, 703brtr4d 5185 . . 3 (𝜑 → (seq1( + , 𝐺)‘1) ≤ (2 · (seq1( + , 𝐹)‘2)))
72 fveq2 6901 . . . . . . . . . . 11 (𝑛 = (𝑗 + 1) → (𝐺𝑛) = (𝐺‘(𝑗 + 1)))
73 oveq2 7432 . . . . . . . . . . . 12 (𝑛 = (𝑗 + 1) → (2↑𝑛) = (2↑(𝑗 + 1)))
7473fveq2d 6905 . . . . . . . . . . . 12 (𝑛 = (𝑗 + 1) → (𝐹‘(2↑𝑛)) = (𝐹‘(2↑(𝑗 + 1))))
7573, 74oveq12d 7442 . . . . . . . . . . 11 (𝑛 = (𝑗 + 1) → ((2↑𝑛) · (𝐹‘(2↑𝑛))) = ((2↑(𝑗 + 1)) · (𝐹‘(2↑(𝑗 + 1)))))
7672, 75eqeq12d 2742 . . . . . . . . . 10 (𝑛 = (𝑗 + 1) → ((𝐺𝑛) = ((2↑𝑛) · (𝐹‘(2↑𝑛))) ↔ (𝐺‘(𝑗 + 1)) = ((2↑(𝑗 + 1)) · (𝐹‘(2↑(𝑗 + 1))))))
7759adantr 479 . . . . . . . . . 10 ((𝜑𝑗 ∈ ℕ) → ∀𝑛 ∈ ℕ0 (𝐺𝑛) = ((2↑𝑛) · (𝐹‘(2↑𝑛))))
78 peano2nn 12276 . . . . . . . . . . . 12 (𝑗 ∈ ℕ → (𝑗 + 1) ∈ ℕ)
7978adantl 480 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ℕ) → (𝑗 + 1) ∈ ℕ)
8079nnnn0d 12584 . . . . . . . . . 10 ((𝜑𝑗 ∈ ℕ) → (𝑗 + 1) ∈ ℕ0)
8176, 77, 80rspcdva 3609 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ) → (𝐺‘(𝑗 + 1)) = ((2↑(𝑗 + 1)) · (𝐹‘(2↑(𝑗 + 1)))))
82 nnnn0 12531 . . . . . . . . . . . . 13 (𝑗 ∈ ℕ → 𝑗 ∈ ℕ0)
8382adantl 480 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ) → 𝑗 ∈ ℕ0)
84 expp1 14088 . . . . . . . . . . . 12 ((2 ∈ ℂ ∧ 𝑗 ∈ ℕ0) → (2↑(𝑗 + 1)) = ((2↑𝑗) · 2))
853, 83, 84sylancr 585 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ℕ) → (2↑(𝑗 + 1)) = ((2↑𝑗) · 2))
86 nnexpcl 14094 . . . . . . . . . . . . . . 15 ((2 ∈ ℕ ∧ 𝑗 ∈ ℕ0) → (2↑𝑗) ∈ ℕ)
8740, 82, 86sylancr 585 . . . . . . . . . . . . . 14 (𝑗 ∈ ℕ → (2↑𝑗) ∈ ℕ)
8887adantl 480 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ ℕ) → (2↑𝑗) ∈ ℕ)
8988nncnd 12280 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ) → (2↑𝑗) ∈ ℂ)
90 mulcom 11244 . . . . . . . . . . . 12 (((2↑𝑗) ∈ ℂ ∧ 2 ∈ ℂ) → ((2↑𝑗) · 2) = (2 · (2↑𝑗)))
9189, 3, 90sylancl 584 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ℕ) → ((2↑𝑗) · 2) = (2 · (2↑𝑗)))
9285, 91eqtrd 2766 . . . . . . . . . 10 ((𝜑𝑗 ∈ ℕ) → (2↑(𝑗 + 1)) = (2 · (2↑𝑗)))
9392oveq1d 7439 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ) → ((2↑(𝑗 + 1)) · (𝐹‘(2↑(𝑗 + 1)))) = ((2 · (2↑𝑗)) · (𝐹‘(2↑(𝑗 + 1)))))
943a1i 11 . . . . . . . . . 10 ((𝜑𝑗 ∈ ℕ) → 2 ∈ ℂ)
95 fveq2 6901 . . . . . . . . . . . . 13 (𝑘 = (2↑(𝑗 + 1)) → (𝐹𝑘) = (𝐹‘(2↑(𝑗 + 1))))
9695eleq1d 2811 . . . . . . . . . . . 12 (𝑘 = (2↑(𝑗 + 1)) → ((𝐹𝑘) ∈ ℝ ↔ (𝐹‘(2↑(𝑗 + 1))) ∈ ℝ))
9739adantr 479 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ) → ∀𝑘 ∈ ℕ (𝐹𝑘) ∈ ℝ)
98 nnexpcl 14094 . . . . . . . . . . . . 13 ((2 ∈ ℕ ∧ (𝑗 + 1) ∈ ℕ0) → (2↑(𝑗 + 1)) ∈ ℕ)
9940, 80, 98sylancr 585 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ) → (2↑(𝑗 + 1)) ∈ ℕ)
10096, 97, 99rspcdva 3609 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ℕ) → (𝐹‘(2↑(𝑗 + 1))) ∈ ℝ)
101100recnd 11292 . . . . . . . . . 10 ((𝜑𝑗 ∈ ℕ) → (𝐹‘(2↑(𝑗 + 1))) ∈ ℂ)
10294, 89, 101mulassd 11287 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ) → ((2 · (2↑𝑗)) · (𝐹‘(2↑(𝑗 + 1)))) = (2 · ((2↑𝑗) · (𝐹‘(2↑(𝑗 + 1))))))
10381, 93, 1023eqtrd 2770 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ) → (𝐺‘(𝑗 + 1)) = (2 · ((2↑𝑗) · (𝐹‘(2↑(𝑗 + 1))))))
10488nnnn0d 12584 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ ℕ) → (2↑𝑗) ∈ ℕ0)
105 hashfz1 14363 . . . . . . . . . . . . . . 15 ((2↑𝑗) ∈ ℕ0 → (♯‘(1...(2↑𝑗))) = (2↑𝑗))
106104, 105syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ ℕ) → (♯‘(1...(2↑𝑗))) = (2↑𝑗))
107106, 89eqeltrd 2826 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ ℕ) → (♯‘(1...(2↑𝑗))) ∈ ℂ)
108 fzfid 13993 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ ℕ) → (((2↑𝑗) + 1)...(2↑(𝑗 + 1))) ∈ Fin)
109 hashcl 14373 . . . . . . . . . . . . . . 15 ((((2↑𝑗) + 1)...(2↑(𝑗 + 1))) ∈ Fin → (♯‘(((2↑𝑗) + 1)...(2↑(𝑗 + 1)))) ∈ ℕ0)
110108, 109syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ ℕ) → (♯‘(((2↑𝑗) + 1)...(2↑(𝑗 + 1)))) ∈ ℕ0)
111110nn0cnd 12586 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ ℕ) → (♯‘(((2↑𝑗) + 1)...(2↑(𝑗 + 1)))) ∈ ℂ)
112 simpr 483 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ ℕ) → 𝑗 ∈ ℕ)
113112nnzd 12637 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ ℕ) → 𝑗 ∈ ℤ)
114 uzid 12889 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ ℤ → 𝑗 ∈ (ℤ𝑗))
115 peano2uz 12937 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (ℤ𝑗) → (𝑗 + 1) ∈ (ℤ𝑗))
116 2re 12338 . . . . . . . . . . . . . . . . . . 19 2 ∈ ℝ
117 1le2 12473 . . . . . . . . . . . . . . . . . . 19 1 ≤ 2
118 leexp2a 14191 . . . . . . . . . . . . . . . . . . 19 ((2 ∈ ℝ ∧ 1 ≤ 2 ∧ (𝑗 + 1) ∈ (ℤ𝑗)) → (2↑𝑗) ≤ (2↑(𝑗 + 1)))
119116, 117, 118mp3an12 1448 . . . . . . . . . . . . . . . . . 18 ((𝑗 + 1) ∈ (ℤ𝑗) → (2↑𝑗) ≤ (2↑(𝑗 + 1)))
120113, 114, 115, 1194syl 19 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ ℕ) → (2↑𝑗) ≤ (2↑(𝑗 + 1)))
12188, 64eleqtrdi 2836 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ ℕ) → (2↑𝑗) ∈ (ℤ‘1))
12299nnzd 12637 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ ℕ) → (2↑(𝑗 + 1)) ∈ ℤ)
123 elfz5 13547 . . . . . . . . . . . . . . . . . 18 (((2↑𝑗) ∈ (ℤ‘1) ∧ (2↑(𝑗 + 1)) ∈ ℤ) → ((2↑𝑗) ∈ (1...(2↑(𝑗 + 1))) ↔ (2↑𝑗) ≤ (2↑(𝑗 + 1))))
124121, 122, 123syl2anc 582 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ ℕ) → ((2↑𝑗) ∈ (1...(2↑(𝑗 + 1))) ↔ (2↑𝑗) ≤ (2↑(𝑗 + 1))))
125120, 124mpbird 256 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ ℕ) → (2↑𝑗) ∈ (1...(2↑(𝑗 + 1))))
126 fzsplit 13581 . . . . . . . . . . . . . . . 16 ((2↑𝑗) ∈ (1...(2↑(𝑗 + 1))) → (1...(2↑(𝑗 + 1))) = ((1...(2↑𝑗)) ∪ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))))
127125, 126syl 17 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ ℕ) → (1...(2↑(𝑗 + 1))) = ((1...(2↑𝑗)) ∪ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))))
128127fveq2d 6905 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ ℕ) → (♯‘(1...(2↑(𝑗 + 1)))) = (♯‘((1...(2↑𝑗)) ∪ (((2↑𝑗) + 1)...(2↑(𝑗 + 1))))))
12989times2d 12508 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ ℕ) → ((2↑𝑗) · 2) = ((2↑𝑗) + (2↑𝑗)))
13085, 129eqtrd 2766 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ ℕ) → (2↑(𝑗 + 1)) = ((2↑𝑗) + (2↑𝑗)))
13199nnnn0d 12584 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ ℕ) → (2↑(𝑗 + 1)) ∈ ℕ0)
132 hashfz1 14363 . . . . . . . . . . . . . . . 16 ((2↑(𝑗 + 1)) ∈ ℕ0 → (♯‘(1...(2↑(𝑗 + 1)))) = (2↑(𝑗 + 1)))
133131, 132syl 17 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ ℕ) → (♯‘(1...(2↑(𝑗 + 1)))) = (2↑(𝑗 + 1)))
134106oveq1d 7439 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ ℕ) → ((♯‘(1...(2↑𝑗))) + (2↑𝑗)) = ((2↑𝑗) + (2↑𝑗)))
135130, 133, 1343eqtr4d 2776 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ ℕ) → (♯‘(1...(2↑(𝑗 + 1)))) = ((♯‘(1...(2↑𝑗))) + (2↑𝑗)))
136 fzfid 13993 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ ℕ) → (1...(2↑𝑗)) ∈ Fin)
13788nnred 12279 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ ℕ) → (2↑𝑗) ∈ ℝ)
138137ltp1d 12196 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ ℕ) → (2↑𝑗) < ((2↑𝑗) + 1))
139 fzdisj 13582 . . . . . . . . . . . . . . . 16 ((2↑𝑗) < ((2↑𝑗) + 1) → ((1...(2↑𝑗)) ∩ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))) = ∅)
140138, 139syl 17 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ ℕ) → ((1...(2↑𝑗)) ∩ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))) = ∅)
141 hashun 14399 . . . . . . . . . . . . . . 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))))))
142136, 108, 140, 141syl3anc 1368 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ ℕ) → (♯‘((1...(2↑𝑗)) ∪ (((2↑𝑗) + 1)...(2↑(𝑗 + 1))))) = ((♯‘(1...(2↑𝑗))) + (♯‘(((2↑𝑗) + 1)...(2↑(𝑗 + 1))))))
143128, 135, 1423eqtr3d 2774 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ ℕ) → ((♯‘(1...(2↑𝑗))) + (2↑𝑗)) = ((♯‘(1...(2↑𝑗))) + (♯‘(((2↑𝑗) + 1)...(2↑(𝑗 + 1))))))
144107, 89, 111, 143addcanad 11469 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ) → (2↑𝑗) = (♯‘(((2↑𝑗) + 1)...(2↑(𝑗 + 1)))))
145144oveq1d 7439 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ℕ) → ((2↑𝑗) · (𝐹‘(2↑(𝑗 + 1)))) = ((♯‘(((2↑𝑗) + 1)...(2↑(𝑗 + 1)))) · (𝐹‘(2↑(𝑗 + 1)))))
146 fsumconst 15794 . . . . . . . . . . . 12 (((((2↑𝑗) + 1)...(2↑(𝑗 + 1))) ∈ Fin ∧ (𝐹‘(2↑(𝑗 + 1))) ∈ ℂ) → Σ𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))(𝐹‘(2↑(𝑗 + 1))) = ((♯‘(((2↑𝑗) + 1)...(2↑(𝑗 + 1)))) · (𝐹‘(2↑(𝑗 + 1)))))
147108, 101, 146syl2anc 582 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ℕ) → Σ𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))(𝐹‘(2↑(𝑗 + 1))) = ((♯‘(((2↑𝑗) + 1)...(2↑(𝑗 + 1)))) · (𝐹‘(2↑(𝑗 + 1)))))
148145, 147eqtr4d 2769 . . . . . . . . . 10 ((𝜑𝑗 ∈ ℕ) → ((2↑𝑗) · (𝐹‘(2↑(𝑗 + 1)))) = Σ𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))(𝐹‘(2↑(𝑗 + 1))))
149100adantr 479 . . . . . . . . . . 11 (((𝜑𝑗 ∈ ℕ) ∧ 𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))) → (𝐹‘(2↑(𝑗 + 1))) ∈ ℝ)
150 simpl 481 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ) → 𝜑)
151 peano2nn 12276 . . . . . . . . . . . . . 14 ((2↑𝑗) ∈ ℕ → ((2↑𝑗) + 1) ∈ ℕ)
15288, 151syl 17 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ ℕ) → ((2↑𝑗) + 1) ∈ ℕ)
153 elfzuz 13551 . . . . . . . . . . . . 13 (𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1))) → 𝑘 ∈ (ℤ‘((2↑𝑗) + 1)))
154 eluznn 12954 . . . . . . . . . . . . 13 ((((2↑𝑗) + 1) ∈ ℕ ∧ 𝑘 ∈ (ℤ‘((2↑𝑗) + 1))) → 𝑘 ∈ ℕ)
155152, 153, 154syl2an 594 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ ℕ) ∧ 𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))) → 𝑘 ∈ ℕ)
156150, 155, 38syl2an2r 683 . . . . . . . . . . 11 (((𝜑𝑗 ∈ ℕ) ∧ 𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))) → (𝐹𝑘) ∈ ℝ)
157 elfzuz3 13552 . . . . . . . . . . . . . . 15 (𝑛 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1))) → (2↑(𝑗 + 1)) ∈ (ℤ𝑛))
158157adantl 480 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ ℕ) ∧ 𝑛 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))) → (2↑(𝑗 + 1)) ∈ (ℤ𝑛))
159 simplll 773 . . . . . . . . . . . . . . 15 ((((𝜑𝑗 ∈ ℕ) ∧ 𝑛 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))) ∧ 𝑘 ∈ (𝑛...(2↑(𝑗 + 1)))) → 𝜑)
160 elfzuz 13551 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1))) → 𝑛 ∈ (ℤ‘((2↑𝑗) + 1)))
161 eluznn 12954 . . . . . . . . . . . . . . . . 17 ((((2↑𝑗) + 1) ∈ ℕ ∧ 𝑛 ∈ (ℤ‘((2↑𝑗) + 1))) → 𝑛 ∈ ℕ)
162152, 160, 161syl2an 594 . . . . . . . . . . . . . . . 16 (((𝜑𝑗 ∈ ℕ) ∧ 𝑛 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))) → 𝑛 ∈ ℕ)
163 elfzuz 13551 . . . . . . . . . . . . . . . 16 (𝑘 ∈ (𝑛...(2↑(𝑗 + 1))) → 𝑘 ∈ (ℤ𝑛))
164 eluznn 12954 . . . . . . . . . . . . . . . 16 ((𝑛 ∈ ℕ ∧ 𝑘 ∈ (ℤ𝑛)) → 𝑘 ∈ ℕ)
165162, 163, 164syl2an 594 . . . . . . . . . . . . . . 15 ((((𝜑𝑗 ∈ ℕ) ∧ 𝑛 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))) ∧ 𝑘 ∈ (𝑛...(2↑(𝑗 + 1)))) → 𝑘 ∈ ℕ)
166159, 165, 38syl2anc 582 . . . . . . . . . . . . . 14 ((((𝜑𝑗 ∈ ℕ) ∧ 𝑛 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))) ∧ 𝑘 ∈ (𝑛...(2↑(𝑗 + 1)))) → (𝐹𝑘) ∈ ℝ)
167 simplll 773 . . . . . . . . . . . . . . 15 ((((𝜑𝑗 ∈ ℕ) ∧ 𝑛 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))) ∧ 𝑘 ∈ (𝑛...((2↑(𝑗 + 1)) − 1))) → 𝜑)
168 elfzuz 13551 . . . . . . . . . . . . . . . 16 (𝑘 ∈ (𝑛...((2↑(𝑗 + 1)) − 1)) → 𝑘 ∈ (ℤ𝑛))
169162, 168, 164syl2an 594 . . . . . . . . . . . . . . 15 ((((𝜑𝑗 ∈ ℕ) ∧ 𝑛 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))) ∧ 𝑘 ∈ (𝑛...((2↑(𝑗 + 1)) − 1))) → 𝑘 ∈ ℕ)
170 climcnds.3 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ ℕ) → (𝐹‘(𝑘 + 1)) ≤ (𝐹𝑘))
171167, 169, 170syl2anc 582 . . . . . . . . . . . . . 14 ((((𝜑𝑗 ∈ ℕ) ∧ 𝑛 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))) ∧ 𝑘 ∈ (𝑛...((2↑(𝑗 + 1)) − 1))) → (𝐹‘(𝑘 + 1)) ≤ (𝐹𝑘))
172158, 166, 171monoord2 14053 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ ℕ) ∧ 𝑛 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))) → (𝐹‘(2↑(𝑗 + 1))) ≤ (𝐹𝑛))
173172ralrimiva 3136 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ) → ∀𝑛 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))(𝐹‘(2↑(𝑗 + 1))) ≤ (𝐹𝑛))
174 fveq2 6901 . . . . . . . . . . . . . 14 (𝑛 = 𝑘 → (𝐹𝑛) = (𝐹𝑘))
175174breq2d 5165 . . . . . . . . . . . . 13 (𝑛 = 𝑘 → ((𝐹‘(2↑(𝑗 + 1))) ≤ (𝐹𝑛) ↔ (𝐹‘(2↑(𝑗 + 1))) ≤ (𝐹𝑘)))
176175rspccva 3607 . . . . . . . . . . . 12 ((∀𝑛 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))(𝐹‘(2↑(𝑗 + 1))) ≤ (𝐹𝑛) ∧ 𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))) → (𝐹‘(2↑(𝑗 + 1))) ≤ (𝐹𝑘))
177173, 176sylan 578 . . . . . . . . . . 11 (((𝜑𝑗 ∈ ℕ) ∧ 𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))) → (𝐹‘(2↑(𝑗 + 1))) ≤ (𝐹𝑘))
178108, 149, 156, 177fsumle 15803 . . . . . . . . . 10 ((𝜑𝑗 ∈ ℕ) → Σ𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))(𝐹‘(2↑(𝑗 + 1))) ≤ Σ𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))(𝐹𝑘))
179148, 178eqbrtrd 5175 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ) → ((2↑𝑗) · (𝐹‘(2↑(𝑗 + 1)))) ≤ Σ𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))(𝐹𝑘))
180137, 100remulcld 11294 . . . . . . . . . 10 ((𝜑𝑗 ∈ ℕ) → ((2↑𝑗) · (𝐹‘(2↑(𝑗 + 1)))) ∈ ℝ)
181108, 156fsumrecl 15738 . . . . . . . . . 10 ((𝜑𝑗 ∈ ℕ) → Σ𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))(𝐹𝑘) ∈ ℝ)
182 2rp 13033 . . . . . . . . . . 11 2 ∈ ℝ+
183182a1i 11 . . . . . . . . . 10 ((𝜑𝑗 ∈ ℕ) → 2 ∈ ℝ+)
184180, 181, 183lemul2d 13114 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ) → (((2↑𝑗) · (𝐹‘(2↑(𝑗 + 1)))) ≤ Σ𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))(𝐹𝑘) ↔ (2 · ((2↑𝑗) · (𝐹‘(2↑(𝑗 + 1))))) ≤ (2 · Σ𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))(𝐹𝑘))))
185179, 184mpbid 231 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ) → (2 · ((2↑𝑗) · (𝐹‘(2↑(𝑗 + 1))))) ≤ (2 · Σ𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))(𝐹𝑘)))
186103, 185eqbrtrd 5175 . . . . . . 7 ((𝜑𝑗 ∈ ℕ) → (𝐺‘(𝑗 + 1)) ≤ (2 · Σ𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))(𝐹𝑘)))
187 1zzd 12645 . . . . . . . . . 10 (𝜑 → 1 ∈ ℤ)
188 nnnn0 12531 . . . . . . . . . . 11 (𝑛 ∈ ℕ → 𝑛 ∈ ℕ0)
189 simpr 483 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ0) → 𝑛 ∈ ℕ0)
190 nnexpcl 14094 . . . . . . . . . . . . . . 15 ((2 ∈ ℕ ∧ 𝑛 ∈ ℕ0) → (2↑𝑛) ∈ ℕ)
19140, 189, 190sylancr 585 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ ℕ0) → (2↑𝑛) ∈ ℕ)
192191nnred 12279 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ ℕ0) → (2↑𝑛) ∈ ℝ)
193 fveq2 6901 . . . . . . . . . . . . . . 15 (𝑘 = (2↑𝑛) → (𝐹𝑘) = (𝐹‘(2↑𝑛)))
194193eleq1d 2811 . . . . . . . . . . . . . 14 (𝑘 = (2↑𝑛) → ((𝐹𝑘) ∈ ℝ ↔ (𝐹‘(2↑𝑛)) ∈ ℝ))
19539adantr 479 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ ℕ0) → ∀𝑘 ∈ ℕ (𝐹𝑘) ∈ ℝ)
196194, 195, 191rspcdva 3609 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ ℕ0) → (𝐹‘(2↑𝑛)) ∈ ℝ)
197192, 196remulcld 11294 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ0) → ((2↑𝑛) · (𝐹‘(2↑𝑛))) ∈ ℝ)
19858, 197eqeltrd 2826 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ0) → (𝐺𝑛) ∈ ℝ)
199188, 198sylan2 591 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → (𝐺𝑛) ∈ ℝ)
20064, 187, 199serfre 14051 . . . . . . . . 9 (𝜑 → seq1( + , 𝐺):ℕ⟶ℝ)
201200ffvelcdmda 7098 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ) → (seq1( + , 𝐺)‘𝑗) ∈ ℝ)
20272eleq1d 2811 . . . . . . . . 9 (𝑛 = (𝑗 + 1) → ((𝐺𝑛) ∈ ℝ ↔ (𝐺‘(𝑗 + 1)) ∈ ℝ))
203199ralrimiva 3136 . . . . . . . . . 10 (𝜑 → ∀𝑛 ∈ ℕ (𝐺𝑛) ∈ ℝ)
204203adantr 479 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ) → ∀𝑛 ∈ ℕ (𝐺𝑛) ∈ ℝ)
205202, 204, 79rspcdva 3609 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ) → (𝐺‘(𝑗 + 1)) ∈ ℝ)
20664, 187, 38serfre 14051 . . . . . . . . . 10 (𝜑 → seq1( + , 𝐹):ℕ⟶ℝ)
207 ffvelcdm 7095 . . . . . . . . . 10 ((seq1( + , 𝐹):ℕ⟶ℝ ∧ (2↑𝑗) ∈ ℕ) → (seq1( + , 𝐹)‘(2↑𝑗)) ∈ ℝ)
208206, 87, 207syl2an 594 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ) → (seq1( + , 𝐹)‘(2↑𝑗)) ∈ ℝ)
209 remulcl 11243 . . . . . . . . 9 ((2 ∈ ℝ ∧ (seq1( + , 𝐹)‘(2↑𝑗)) ∈ ℝ) → (2 · (seq1( + , 𝐹)‘(2↑𝑗))) ∈ ℝ)
210116, 208, 209sylancr 585 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ) → (2 · (seq1( + , 𝐹)‘(2↑𝑗))) ∈ ℝ)
211 remulcl 11243 . . . . . . . . 9 ((2 ∈ ℝ ∧ Σ𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))(𝐹𝑘) ∈ ℝ) → (2 · Σ𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))(𝐹𝑘)) ∈ ℝ)
212116, 181, 211sylancr 585 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ) → (2 · Σ𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))(𝐹𝑘)) ∈ ℝ)
213 le2add 11746 . . . . . . . 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)))(𝐹𝑘)))))
214201, 205, 210, 212, 213syl22anc 837 . . . . . . 7 ((𝜑𝑗 ∈ ℕ) → (((seq1( + , 𝐺)‘𝑗) ≤ (2 · (seq1( + , 𝐹)‘(2↑𝑗))) ∧ (𝐺‘(𝑗 + 1)) ≤ (2 · Σ𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))(𝐹𝑘))) → ((seq1( + , 𝐺)‘𝑗) + (𝐺‘(𝑗 + 1))) ≤ ((2 · (seq1( + , 𝐹)‘(2↑𝑗))) + (2 · Σ𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))(𝐹𝑘)))))
215186, 214mpan2d 692 . . . . . 6 ((𝜑𝑗 ∈ ℕ) → ((seq1( + , 𝐺)‘𝑗) ≤ (2 · (seq1( + , 𝐹)‘(2↑𝑗))) → ((seq1( + , 𝐺)‘𝑗) + (𝐺‘(𝑗 + 1))) ≤ ((2 · (seq1( + , 𝐹)‘(2↑𝑗))) + (2 · Σ𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))(𝐹𝑘)))))
216112, 64eleqtrdi 2836 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ) → 𝑗 ∈ (ℤ‘1))
217 seqp1 14036 . . . . . . . 8 (𝑗 ∈ (ℤ‘1) → (seq1( + , 𝐺)‘(𝑗 + 1)) = ((seq1( + , 𝐺)‘𝑗) + (𝐺‘(𝑗 + 1))))
218216, 217syl 17 . . . . . . 7 ((𝜑𝑗 ∈ ℕ) → (seq1( + , 𝐺)‘(𝑗 + 1)) = ((seq1( + , 𝐺)‘𝑗) + (𝐺‘(𝑗 + 1))))
219 fzfid 13993 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ℕ) → (1...(2↑(𝑗 + 1))) ∈ Fin)
220 elfznn 13584 . . . . . . . . . . . 12 (𝑘 ∈ (1...(2↑(𝑗 + 1))) → 𝑘 ∈ ℕ)
22138recnd 11292 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ) → (𝐹𝑘) ∈ ℂ)
222150, 220, 221syl2an 594 . . . . . . . . . . 11 (((𝜑𝑗 ∈ ℕ) ∧ 𝑘 ∈ (1...(2↑(𝑗 + 1)))) → (𝐹𝑘) ∈ ℂ)
223140, 127, 219, 222fsumsplit 15745 . . . . . . . . . 10 ((𝜑𝑗 ∈ ℕ) → Σ𝑘 ∈ (1...(2↑(𝑗 + 1)))(𝐹𝑘) = (Σ𝑘 ∈ (1...(2↑𝑗))(𝐹𝑘) + Σ𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))(𝐹𝑘)))
224 eqidd 2727 . . . . . . . . . . 11 (((𝜑𝑗 ∈ ℕ) ∧ 𝑘 ∈ (1...(2↑(𝑗 + 1)))) → (𝐹𝑘) = (𝐹𝑘))
22599, 64eleqtrdi 2836 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ℕ) → (2↑(𝑗 + 1)) ∈ (ℤ‘1))
226224, 225, 222fsumser 15734 . . . . . . . . . 10 ((𝜑𝑗 ∈ ℕ) → Σ𝑘 ∈ (1...(2↑(𝑗 + 1)))(𝐹𝑘) = (seq1( + , 𝐹)‘(2↑(𝑗 + 1))))
227 eqidd 2727 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ ℕ) ∧ 𝑘 ∈ (1...(2↑𝑗))) → (𝐹𝑘) = (𝐹𝑘))
228 elfznn 13584 . . . . . . . . . . . . 13 (𝑘 ∈ (1...(2↑𝑗)) → 𝑘 ∈ ℕ)
229150, 228, 221syl2an 594 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ ℕ) ∧ 𝑘 ∈ (1...(2↑𝑗))) → (𝐹𝑘) ∈ ℂ)
230227, 121, 229fsumser 15734 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ℕ) → Σ𝑘 ∈ (1...(2↑𝑗))(𝐹𝑘) = (seq1( + , 𝐹)‘(2↑𝑗)))
231230oveq1d 7439 . . . . . . . . . 10 ((𝜑𝑗 ∈ ℕ) → (Σ𝑘 ∈ (1...(2↑𝑗))(𝐹𝑘) + Σ𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))(𝐹𝑘)) = ((seq1( + , 𝐹)‘(2↑𝑗)) + Σ𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))(𝐹𝑘)))
232223, 226, 2313eqtr3d 2774 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ) → (seq1( + , 𝐹)‘(2↑(𝑗 + 1))) = ((seq1( + , 𝐹)‘(2↑𝑗)) + Σ𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))(𝐹𝑘)))
233232oveq2d 7440 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ) → (2 · (seq1( + , 𝐹)‘(2↑(𝑗 + 1)))) = (2 · ((seq1( + , 𝐹)‘(2↑𝑗)) + Σ𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))(𝐹𝑘))))
234208recnd 11292 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ) → (seq1( + , 𝐹)‘(2↑𝑗)) ∈ ℂ)
235181recnd 11292 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ) → Σ𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))(𝐹𝑘) ∈ ℂ)
23694, 234, 235adddid 11288 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ) → (2 · ((seq1( + , 𝐹)‘(2↑𝑗)) + Σ𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))(𝐹𝑘))) = ((2 · (seq1( + , 𝐹)‘(2↑𝑗))) + (2 · Σ𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))(𝐹𝑘))))
237233, 236eqtrd 2766 . . . . . . 7 ((𝜑𝑗 ∈ ℕ) → (2 · (seq1( + , 𝐹)‘(2↑(𝑗 + 1)))) = ((2 · (seq1( + , 𝐹)‘(2↑𝑗))) + (2 · Σ𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))(𝐹𝑘))))
238218, 237breq12d 5166 . . . . . 6 ((𝜑𝑗 ∈ ℕ) → ((seq1( + , 𝐺)‘(𝑗 + 1)) ≤ (2 · (seq1( + , 𝐹)‘(2↑(𝑗 + 1)))) ↔ ((seq1( + , 𝐺)‘𝑗) + (𝐺‘(𝑗 + 1))) ≤ ((2 · (seq1( + , 𝐹)‘(2↑𝑗))) + (2 · Σ𝑘 ∈ (((2↑𝑗) + 1)...(2↑(𝑗 + 1)))(𝐹𝑘)))))
239215, 238sylibrd 258 . . . . 5 ((𝜑𝑗 ∈ ℕ) → ((seq1( + , 𝐺)‘𝑗) ≤ (2 · (seq1( + , 𝐹)‘(2↑𝑗))) → (seq1( + , 𝐺)‘(𝑗 + 1)) ≤ (2 · (seq1( + , 𝐹)‘(2↑(𝑗 + 1))))))
240239expcom 412 . . . 4 (𝑗 ∈ ℕ → (𝜑 → ((seq1( + , 𝐺)‘𝑗) ≤ (2 · (seq1( + , 𝐹)‘(2↑𝑗))) → (seq1( + , 𝐺)‘(𝑗 + 1)) ≤ (2 · (seq1( + , 𝐹)‘(2↑(𝑗 + 1)))))))
241240a2d 29 . . 3 (𝑗 ∈ ℕ → ((𝜑 → (seq1( + , 𝐺)‘𝑗) ≤ (2 · (seq1( + , 𝐹)‘(2↑𝑗)))) → (𝜑 → (seq1( + , 𝐺)‘(𝑗 + 1)) ≤ (2 · (seq1( + , 𝐹)‘(2↑(𝑗 + 1)))))))
24210, 16, 22, 28, 71, 241nnind 12282 . 2 (𝑁 ∈ ℕ → (𝜑 → (seq1( + , 𝐺)‘𝑁) ≤ (2 · (seq1( + , 𝐹)‘(2↑𝑁)))))
243242impcom 406 1 ((𝜑𝑁 ∈ ℕ) → (seq1( + , 𝐺)‘𝑁) ≤ (2 · (seq1( + , 𝐹)‘(2↑𝑁))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 394   = wceq 1534  wcel 2099  wral 3051  cun 3945  cin 3946  c0 4325   class class class wbr 5153  wf 6550  cfv 6554  (class class class)co 7424  Fincfn 8974  cc 11156  cr 11157  0cc0 11158  1c1 11159   + caddc 11161   · cmul 11163   < clt 11298  cle 11299  cmin 11494  cn 12264  2c2 12319  0cn0 12524  cz 12610  cuz 12874  +crp 13028  ...cfz 13538  seqcseq 14021  cexp 14081  chash 14347  Σcsu 15690
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2697  ax-rep 5290  ax-sep 5304  ax-nul 5311  ax-pow 5369  ax-pr 5433  ax-un 7746  ax-inf2 9684  ax-cnex 11214  ax-resscn 11215  ax-1cn 11216  ax-icn 11217  ax-addcl 11218  ax-addrcl 11219  ax-mulcl 11220  ax-mulrcl 11221  ax-mulcom 11222  ax-addass 11223  ax-mulass 11224  ax-distr 11225  ax-i2m1 11226  ax-1ne0 11227  ax-1rid 11228  ax-rnegex 11229  ax-rrecex 11230  ax-cnre 11231  ax-pre-lttri 11232  ax-pre-lttrn 11233  ax-pre-ltadd 11234  ax-pre-mulgt0 11235  ax-pre-sup 11236
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2704  df-cleq 2718  df-clel 2803  df-nfc 2878  df-ne 2931  df-nel 3037  df-ral 3052  df-rex 3061  df-rmo 3364  df-reu 3365  df-rab 3420  df-v 3464  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3967  df-nul 4326  df-if 4534  df-pw 4609  df-sn 4634  df-pr 4636  df-op 4640  df-uni 4914  df-int 4955  df-iun 5003  df-br 5154  df-opab 5216  df-mpt 5237  df-tr 5271  df-id 5580  df-eprel 5586  df-po 5594  df-so 5595  df-fr 5637  df-se 5638  df-we 5639  df-xp 5688  df-rel 5689  df-cnv 5690  df-co 5691  df-dm 5692  df-rn 5693  df-res 5694  df-ima 5695  df-pred 6312  df-ord 6379  df-on 6380  df-lim 6381  df-suc 6382  df-iota 6506  df-fun 6556  df-fn 6557  df-f 6558  df-f1 6559  df-fo 6560  df-f1o 6561  df-fv 6562  df-isom 6563  df-riota 7380  df-ov 7427  df-oprab 7428  df-mpo 7429  df-om 7877  df-1st 8003  df-2nd 8004  df-frecs 8296  df-wrecs 8327  df-recs 8401  df-rdg 8440  df-1o 8496  df-oadd 8500  df-er 8734  df-en 8975  df-dom 8976  df-sdom 8977  df-fin 8978  df-sup 9485  df-oi 9553  df-dju 9944  df-card 9982  df-pnf 11300  df-mnf 11301  df-xr 11302  df-ltxr 11303  df-le 11304  df-sub 11496  df-neg 11497  df-div 11922  df-nn 12265  df-2 12327  df-3 12328  df-n0 12525  df-z 12611  df-uz 12875  df-rp 13029  df-ico 13384  df-fz 13539  df-fzo 13682  df-seq 14022  df-exp 14082  df-hash 14348  df-cj 15104  df-re 15105  df-im 15106  df-sqrt 15240  df-abs 15241  df-clim 15490  df-sum 15691
This theorem is referenced by:  climcnds  15855
  Copyright terms: Public domain W3C validator