This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem climcndslem2

Description: Lemma for climcnds : bound the condensed series by the original series. (Contributed by Mario Carneiro, 18-Jul-2014) (Proof shortened by AV, 10-Jul-2022)

Ref Expression
Hypotheses climcnds.1 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
climcnds.2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 0 ≤ ( 𝐹 ‘ 𝑘 ) )
climcnds.3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝐹 ‘ ( 𝑘 + 1 ) ) ≤ ( 𝐹 ‘ 𝑘 ) )
climcnds.4 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( 𝐺 ‘ 𝑛 ) = ( ( 2 ↑ 𝑛 ) · ( 𝐹 ‘ ( 2 ↑ 𝑛 ) ) ) )
Assertion climcndslem2 ( ( 𝜑 ∧ 𝑁 ∈ ℕ ) → ( seq 1 ( + , 𝐺 ) ‘ 𝑁 ) ≤ ( 2 · ( seq 1 ( + , 𝐹 ) ‘ ( 2 ↑ 𝑁 ) ) ) )

Proof

Step Hyp Ref Expression
1 climcnds.1 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
2 climcnds.2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 0 ≤ ( 𝐹 ‘ 𝑘 ) )
3 climcnds.3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝐹 ‘ ( 𝑘 + 1 ) ) ≤ ( 𝐹 ‘ 𝑘 ) )
4 climcnds.4 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( 𝐺 ‘ 𝑛 ) = ( ( 2 ↑ 𝑛 ) · ( 𝐹 ‘ ( 2 ↑ 𝑛 ) ) ) )
5 fveq2 ⊢ ( 𝑥 = 1 → ( seq 1 ( + , 𝐺 ) ‘ 𝑥 ) = ( seq 1 ( + , 𝐺 ) ‘ 1 ) )
6 oveq2 ⊢ ( 𝑥 = 1 → ( 2 ↑ 𝑥 ) = ( 2 ↑ 1 ) )
7 2cn ⊢ 2 ∈ ℂ
8 exp1 ⊢ ( 2 ∈ ℂ → ( 2 ↑ 1 ) = 2 )
9 7 8 ax-mp ⊢ ( 2 ↑ 1 ) = 2
10 6 9 eqtrdi ⊢ ( 𝑥 = 1 → ( 2 ↑ 𝑥 ) = 2 )
11 10 fveq2d ⊢ ( 𝑥 = 1 → ( seq 1 ( + , 𝐹 ) ‘ ( 2 ↑ 𝑥 ) ) = ( seq 1 ( + , 𝐹 ) ‘ 2 ) )
12 11 oveq2d ⊢ ( 𝑥 = 1 → ( 2 · ( seq 1 ( + , 𝐹 ) ‘ ( 2 ↑ 𝑥 ) ) ) = ( 2 · ( seq 1 ( + , 𝐹 ) ‘ 2 ) ) )
13 5 12 breq12d ⊢ ( 𝑥 = 1 → ( ( seq 1 ( + , 𝐺 ) ‘ 𝑥 ) ≤ ( 2 · ( seq 1 ( + , 𝐹 ) ‘ ( 2 ↑ 𝑥 ) ) ) ↔ ( seq 1 ( + , 𝐺 ) ‘ 1 ) ≤ ( 2 · ( seq 1 ( + , 𝐹 ) ‘ 2 ) ) ) )
14 13 imbi2d ⊢ ( 𝑥 = 1 → ( ( 𝜑 → ( seq 1 ( + , 𝐺 ) ‘ 𝑥 ) ≤ ( 2 · ( seq 1 ( + , 𝐹 ) ‘ ( 2 ↑ 𝑥 ) ) ) ) ↔ ( 𝜑 → ( seq 1 ( + , 𝐺 ) ‘ 1 ) ≤ ( 2 · ( seq 1 ( + , 𝐹 ) ‘ 2 ) ) ) ) )
15 fveq2 ⊢ ( 𝑥 = 𝑗 → ( seq 1 ( + , 𝐺 ) ‘ 𝑥 ) = ( seq 1 ( + , 𝐺 ) ‘ 𝑗 ) )
16 oveq2 ⊢ ( 𝑥 = 𝑗 → ( 2 ↑ 𝑥 ) = ( 2 ↑ 𝑗 ) )
17 16 fveq2d ⊢ ( 𝑥 = 𝑗 → ( seq 1 ( + , 𝐹 ) ‘ ( 2 ↑ 𝑥 ) ) = ( seq 1 ( + , 𝐹 ) ‘ ( 2 ↑ 𝑗 ) ) )
18 17 oveq2d ⊢ ( 𝑥 = 𝑗 → ( 2 · ( seq 1 ( + , 𝐹 ) ‘ ( 2 ↑ 𝑥 ) ) ) = ( 2 · ( seq 1 ( + , 𝐹 ) ‘ ( 2 ↑ 𝑗 ) ) ) )
19 15 18 breq12d ⊢ ( 𝑥 = 𝑗 → ( ( seq 1 ( + , 𝐺 ) ‘ 𝑥 ) ≤ ( 2 · ( seq 1 ( + , 𝐹 ) ‘ ( 2 ↑ 𝑥 ) ) ) ↔ ( seq 1 ( + , 𝐺 ) ‘ 𝑗 ) ≤ ( 2 · ( seq 1 ( + , 𝐹 ) ‘ ( 2 ↑ 𝑗 ) ) ) ) )
20 19 imbi2d ⊢ ( 𝑥 = 𝑗 → ( ( 𝜑 → ( seq 1 ( + , 𝐺 ) ‘ 𝑥 ) ≤ ( 2 · ( seq 1 ( + , 𝐹 ) ‘ ( 2 ↑ 𝑥 ) ) ) ) ↔ ( 𝜑 → ( seq 1 ( + , 𝐺 ) ‘ 𝑗 ) ≤ ( 2 · ( seq 1 ( + , 𝐹 ) ‘ ( 2 ↑ 𝑗 ) ) ) ) ) )
21 fveq2 ⊢ ( 𝑥 = ( 𝑗 + 1 ) → ( seq 1 ( + , 𝐺 ) ‘ 𝑥 ) = ( seq 1 ( + , 𝐺 ) ‘ ( 𝑗 + 1 ) ) )
22 oveq2 ⊢ ( 𝑥 = ( 𝑗 + 1 ) → ( 2 ↑ 𝑥 ) = ( 2 ↑ ( 𝑗 + 1 ) ) )
23 22 fveq2d ⊢ ( 𝑥 = ( 𝑗 + 1 ) → ( seq 1 ( + , 𝐹 ) ‘ ( 2 ↑ 𝑥 ) ) = ( seq 1 ( + , 𝐹 ) ‘ ( 2 ↑ ( 𝑗 + 1 ) ) ) )
24 23 oveq2d ⊢ ( 𝑥 = ( 𝑗 + 1 ) → ( 2 · ( seq 1 ( + , 𝐹 ) ‘ ( 2 ↑ 𝑥 ) ) ) = ( 2 · ( seq 1 ( + , 𝐹 ) ‘ ( 2 ↑ ( 𝑗 + 1 ) ) ) ) )
25 21 24 breq12d ⊢ ( 𝑥 = ( 𝑗 + 1 ) → ( ( seq 1 ( + , 𝐺 ) ‘ 𝑥 ) ≤ ( 2 · ( seq 1 ( + , 𝐹 ) ‘ ( 2 ↑ 𝑥 ) ) ) ↔ ( seq 1 ( + , 𝐺 ) ‘ ( 𝑗 + 1 ) ) ≤ ( 2 · ( seq 1 ( + , 𝐹 ) ‘ ( 2 ↑ ( 𝑗 + 1 ) ) ) ) ) )
26 25 imbi2d ⊢ ( 𝑥 = ( 𝑗 + 1 ) → ( ( 𝜑 → ( seq 1 ( + , 𝐺 ) ‘ 𝑥 ) ≤ ( 2 · ( seq 1 ( + , 𝐹 ) ‘ ( 2 ↑ 𝑥 ) ) ) ) ↔ ( 𝜑 → ( seq 1 ( + , 𝐺 ) ‘ ( 𝑗 + 1 ) ) ≤ ( 2 · ( seq 1 ( + , 𝐹 ) ‘ ( 2 ↑ ( 𝑗 + 1 ) ) ) ) ) ) )
27 fveq2 ⊢ ( 𝑥 = 𝑁 → ( seq 1 ( + , 𝐺 ) ‘ 𝑥 ) = ( seq 1 ( + , 𝐺 ) ‘ 𝑁 ) )
28 oveq2 ⊢ ( 𝑥 = 𝑁 → ( 2 ↑ 𝑥 ) = ( 2 ↑ 𝑁 ) )
29 28 fveq2d ⊢ ( 𝑥 = 𝑁 → ( seq 1 ( + , 𝐹 ) ‘ ( 2 ↑ 𝑥 ) ) = ( seq 1 ( + , 𝐹 ) ‘ ( 2 ↑ 𝑁 ) ) )
30 29 oveq2d ⊢ ( 𝑥 = 𝑁 → ( 2 · ( seq 1 ( + , 𝐹 ) ‘ ( 2 ↑ 𝑥 ) ) ) = ( 2 · ( seq 1 ( + , 𝐹 ) ‘ ( 2 ↑ 𝑁 ) ) ) )
31 27 30 breq12d ⊢ ( 𝑥 = 𝑁 → ( ( seq 1 ( + , 𝐺 ) ‘ 𝑥 ) ≤ ( 2 · ( seq 1 ( + , 𝐹 ) ‘ ( 2 ↑ 𝑥 ) ) ) ↔ ( seq 1 ( + , 𝐺 ) ‘ 𝑁 ) ≤ ( 2 · ( seq 1 ( + , 𝐹 ) ‘ ( 2 ↑ 𝑁 ) ) ) ) )
32 31 imbi2d ⊢ ( 𝑥 = 𝑁 → ( ( 𝜑 → ( seq 1 ( + , 𝐺 ) ‘ 𝑥 ) ≤ ( 2 · ( seq 1 ( + , 𝐹 ) ‘ ( 2 ↑ 𝑥 ) ) ) ) ↔ ( 𝜑 → ( seq 1 ( + , 𝐺 ) ‘ 𝑁 ) ≤ ( 2 · ( seq 1 ( + , 𝐹 ) ‘ ( 2 ↑ 𝑁 ) ) ) ) ) )
33 fveq2 ⊢ ( 𝑘 = 1 → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 1 ) )
34 33 breq2d ⊢ ( 𝑘 = 1 → ( 0 ≤ ( 𝐹 ‘ 𝑘 ) ↔ 0 ≤ ( 𝐹 ‘ 1 ) ) )
35 2 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ ℕ 0 ≤ ( 𝐹 ‘ 𝑘 ) )
36 1nn ⊢ 1 ∈ ℕ
37 36 a1i ⊢ ( 𝜑 → 1 ∈ ℕ )
38 34 35 37 rspcdva ⊢ ( 𝜑 → 0 ≤ ( 𝐹 ‘ 1 ) )
39 fveq2 ⊢ ( 𝑘 = 2 → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 2 ) )
40 39 eleq1d ⊢ ( 𝑘 = 2 → ( ( 𝐹 ‘ 𝑘 ) ∈ ℝ ↔ ( 𝐹 ‘ 2 ) ∈ ℝ ) )
41 1 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
42 2nn ⊢ 2 ∈ ℕ
43 42 a1i ⊢ ( 𝜑 → 2 ∈ ℕ )
44 40 41 43 rspcdva ⊢ ( 𝜑 → ( 𝐹 ‘ 2 ) ∈ ℝ )
45 33 eleq1d ⊢ ( 𝑘 = 1 → ( ( 𝐹 ‘ 𝑘 ) ∈ ℝ ↔ ( 𝐹 ‘ 1 ) ∈ ℝ ) )
46 45 41 37 rspcdva ⊢ ( 𝜑 → ( 𝐹 ‘ 1 ) ∈ ℝ )
47 44 46 addge02d ⊢ ( 𝜑 → ( 0 ≤ ( 𝐹 ‘ 1 ) ↔ ( 𝐹 ‘ 2 ) ≤ ( ( 𝐹 ‘ 1 ) + ( 𝐹 ‘ 2 ) ) ) )
48 38 47 mpbid ⊢ ( 𝜑 → ( 𝐹 ‘ 2 ) ≤ ( ( 𝐹 ‘ 1 ) + ( 𝐹 ‘ 2 ) ) )
49 46 44 readdcld ⊢ ( 𝜑 → ( ( 𝐹 ‘ 1 ) + ( 𝐹 ‘ 2 ) ) ∈ ℝ )
50 43 nnrpd ⊢ ( 𝜑 → 2 ∈ ℝ+ )
51 44 49 50 lemul2d ⊢ ( 𝜑 → ( ( 𝐹 ‘ 2 ) ≤ ( ( 𝐹 ‘ 1 ) + ( 𝐹 ‘ 2 ) ) ↔ ( 2 · ( 𝐹 ‘ 2 ) ) ≤ ( 2 · ( ( 𝐹 ‘ 1 ) + ( 𝐹 ‘ 2 ) ) ) ) )
52 48 51 mpbid ⊢ ( 𝜑 → ( 2 · ( 𝐹 ‘ 2 ) ) ≤ ( 2 · ( ( 𝐹 ‘ 1 ) + ( 𝐹 ‘ 2 ) ) ) )
53 1z ⊢ 1 ∈ ℤ
54 fveq2 ⊢ ( 𝑛 = 1 → ( 𝐺 ‘ 𝑛 ) = ( 𝐺 ‘ 1 ) )
55 oveq2 ⊢ ( 𝑛 = 1 → ( 2 ↑ 𝑛 ) = ( 2 ↑ 1 ) )
56 55 9 eqtrdi ⊢ ( 𝑛 = 1 → ( 2 ↑ 𝑛 ) = 2 )
57 56 fveq2d ⊢ ( 𝑛 = 1 → ( 𝐹 ‘ ( 2 ↑ 𝑛 ) ) = ( 𝐹 ‘ 2 ) )
58 56 57 oveq12d ⊢ ( 𝑛 = 1 → ( ( 2 ↑ 𝑛 ) · ( 𝐹 ‘ ( 2 ↑ 𝑛 ) ) ) = ( 2 · ( 𝐹 ‘ 2 ) ) )
59 54 58 eqeq12d ⊢ ( 𝑛 = 1 → ( ( 𝐺 ‘ 𝑛 ) = ( ( 2 ↑ 𝑛 ) · ( 𝐹 ‘ ( 2 ↑ 𝑛 ) ) ) ↔ ( 𝐺 ‘ 1 ) = ( 2 · ( 𝐹 ‘ 2 ) ) ) )
60 4 ralrimiva ⊢ ( 𝜑 → ∀ 𝑛 ∈ ℕ0 ( 𝐺 ‘ 𝑛 ) = ( ( 2 ↑ 𝑛 ) · ( 𝐹 ‘ ( 2 ↑ 𝑛 ) ) ) )
61 1nn0 ⊢ 1 ∈ ℕ0
62 61 a1i ⊢ ( 𝜑 → 1 ∈ ℕ0 )
63 59 60 62 rspcdva ⊢ ( 𝜑 → ( 𝐺 ‘ 1 ) = ( 2 · ( 𝐹 ‘ 2 ) ) )
64 53 63 seq1i ⊢ ( 𝜑 → ( seq 1 ( + , 𝐺 ) ‘ 1 ) = ( 2 · ( 𝐹 ‘ 2 ) ) )
65 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
66 df-2 ⊢ 2 = ( 1 + 1 )
67 eqidd ⊢ ( 𝜑 → ( 𝐹 ‘ 1 ) = ( 𝐹 ‘ 1 ) )
68 53 67 seq1i ⊢ ( 𝜑 → ( seq 1 ( + , 𝐹 ) ‘ 1 ) = ( 𝐹 ‘ 1 ) )
69 eqidd ⊢ ( 𝜑 → ( 𝐹 ‘ 2 ) = ( 𝐹 ‘ 2 ) )
70 65 37 66 68 69 seqp1d ⊢ ( 𝜑 → ( seq 1 ( + , 𝐹 ) ‘ 2 ) = ( ( 𝐹 ‘ 1 ) + ( 𝐹 ‘ 2 ) ) )
71 70 oveq2d ⊢ ( 𝜑 → ( 2 · ( seq 1 ( + , 𝐹 ) ‘ 2 ) ) = ( 2 · ( ( 𝐹 ‘ 1 ) + ( 𝐹 ‘ 2 ) ) ) )
72 52 64 71 3brtr4d ⊢ ( 𝜑 → ( seq 1 ( + , 𝐺 ) ‘ 1 ) ≤ ( 2 · ( seq 1 ( + , 𝐹 ) ‘ 2 ) ) )
73 fveq2 ⊢ ( 𝑛 = ( 𝑗 + 1 ) → ( 𝐺 ‘ 𝑛 ) = ( 𝐺 ‘ ( 𝑗 + 1 ) ) )
74 oveq2 ⊢ ( 𝑛 = ( 𝑗 + 1 ) → ( 2 ↑ 𝑛 ) = ( 2 ↑ ( 𝑗 + 1 ) ) )
75 74 fveq2d ⊢ ( 𝑛 = ( 𝑗 + 1 ) → ( 𝐹 ‘ ( 2 ↑ 𝑛 ) ) = ( 𝐹 ‘ ( 2 ↑ ( 𝑗 + 1 ) ) ) )
76 74 75 oveq12d ⊢ ( 𝑛 = ( 𝑗 + 1 ) → ( ( 2 ↑ 𝑛 ) · ( 𝐹 ‘ ( 2 ↑ 𝑛 ) ) ) = ( ( 2 ↑ ( 𝑗 + 1 ) ) · ( 𝐹 ‘ ( 2 ↑ ( 𝑗 + 1 ) ) ) ) )
77 73 76 eqeq12d ⊢ ( 𝑛 = ( 𝑗 + 1 ) → ( ( 𝐺 ‘ 𝑛 ) = ( ( 2 ↑ 𝑛 ) · ( 𝐹 ‘ ( 2 ↑ 𝑛 ) ) ) ↔ ( 𝐺 ‘ ( 𝑗 + 1 ) ) = ( ( 2 ↑ ( 𝑗 + 1 ) ) · ( 𝐹 ‘ ( 2 ↑ ( 𝑗 + 1 ) ) ) ) ) )
78 60 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ∀ 𝑛 ∈ ℕ0 ( 𝐺 ‘ 𝑛 ) = ( ( 2 ↑ 𝑛 ) · ( 𝐹 ‘ ( 2 ↑ 𝑛 ) ) ) )
79 peano2nn ⊢ ( 𝑗 ∈ ℕ → ( 𝑗 + 1 ) ∈ ℕ )
80 79 adantl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝑗 + 1 ) ∈ ℕ )
81 80 nnnn0d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝑗 + 1 ) ∈ ℕ0 )
82 77 78 81 rspcdva ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝐺 ‘ ( 𝑗 + 1 ) ) = ( ( 2 ↑ ( 𝑗 + 1 ) ) · ( 𝐹 ‘ ( 2 ↑ ( 𝑗 + 1 ) ) ) ) )
83 nnnn0 ⊢ ( 𝑗 ∈ ℕ → 𝑗 ∈ ℕ0 )
84 83 adantl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → 𝑗 ∈ ℕ0 )
85 expp1 ⊢ ( ( 2 ∈ ℂ ∧ 𝑗 ∈ ℕ0 ) → ( 2 ↑ ( 𝑗 + 1 ) ) = ( ( 2 ↑ 𝑗 ) · 2 ) )
86 7 84 85 sylancr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 2 ↑ ( 𝑗 + 1 ) ) = ( ( 2 ↑ 𝑗 ) · 2 ) )
87 nnexpcl ⊢ ( ( 2 ∈ ℕ ∧ 𝑗 ∈ ℕ0 ) → ( 2 ↑ 𝑗 ) ∈ ℕ )
88 42 83 87 sylancr ⊢ ( 𝑗 ∈ ℕ → ( 2 ↑ 𝑗 ) ∈ ℕ )
89 88 adantl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 2 ↑ 𝑗 ) ∈ ℕ )
90 89 nncnd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 2 ↑ 𝑗 ) ∈ ℂ )
91 mulcom ⊢ ( ( ( 2 ↑ 𝑗 ) ∈ ℂ ∧ 2 ∈ ℂ ) → ( ( 2 ↑ 𝑗 ) · 2 ) = ( 2 · ( 2 ↑ 𝑗 ) ) )
92 90 7 91 sylancl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( 2 ↑ 𝑗 ) · 2 ) = ( 2 · ( 2 ↑ 𝑗 ) ) )
93 86 92 eqtrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 2 ↑ ( 𝑗 + 1 ) ) = ( 2 · ( 2 ↑ 𝑗 ) ) )
94 93 oveq1d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( 2 ↑ ( 𝑗 + 1 ) ) · ( 𝐹 ‘ ( 2 ↑ ( 𝑗 + 1 ) ) ) ) = ( ( 2 · ( 2 ↑ 𝑗 ) ) · ( 𝐹 ‘ ( 2 ↑ ( 𝑗 + 1 ) ) ) ) )
95 7 a1i ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → 2 ∈ ℂ )
96 fveq2 ⊢ ( 𝑘 = ( 2 ↑ ( 𝑗 + 1 ) ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ ( 2 ↑ ( 𝑗 + 1 ) ) ) )
97 96 eleq1d ⊢ ( 𝑘 = ( 2 ↑ ( 𝑗 + 1 ) ) → ( ( 𝐹 ‘ 𝑘 ) ∈ ℝ ↔ ( 𝐹 ‘ ( 2 ↑ ( 𝑗 + 1 ) ) ) ∈ ℝ ) )
98 41 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ∀ 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
99 nnexpcl ⊢ ( ( 2 ∈ ℕ ∧ ( 𝑗 + 1 ) ∈ ℕ0 ) → ( 2 ↑ ( 𝑗 + 1 ) ) ∈ ℕ )
100 42 81 99 sylancr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 2 ↑ ( 𝑗 + 1 ) ) ∈ ℕ )
101 97 98 100 rspcdva ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝐹 ‘ ( 2 ↑ ( 𝑗 + 1 ) ) ) ∈ ℝ )
102 101 recnd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝐹 ‘ ( 2 ↑ ( 𝑗 + 1 ) ) ) ∈ ℂ )
103 95 90 102 mulassd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( 2 · ( 2 ↑ 𝑗 ) ) · ( 𝐹 ‘ ( 2 ↑ ( 𝑗 + 1 ) ) ) ) = ( 2 · ( ( 2 ↑ 𝑗 ) · ( 𝐹 ‘ ( 2 ↑ ( 𝑗 + 1 ) ) ) ) ) )
104 82 94 103 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝐺 ‘ ( 𝑗 + 1 ) ) = ( 2 · ( ( 2 ↑ 𝑗 ) · ( 𝐹 ‘ ( 2 ↑ ( 𝑗 + 1 ) ) ) ) ) )
105 89 nnnn0d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 2 ↑ 𝑗 ) ∈ ℕ0 )
106 hashfz1 ⊢ ( ( 2 ↑ 𝑗 ) ∈ ℕ0 → ( ♯ ‘ ( 1 ... ( 2 ↑ 𝑗 ) ) ) = ( 2 ↑ 𝑗 ) )
107 105 106 syl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ♯ ‘ ( 1 ... ( 2 ↑ 𝑗 ) ) ) = ( 2 ↑ 𝑗 ) )
108 107 90 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ♯ ‘ ( 1 ... ( 2 ↑ 𝑗 ) ) ) ∈ ℂ )
109 fzfid ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( ( 2 ↑ 𝑗 ) + 1 ) ... ( 2 ↑ ( 𝑗 + 1 ) ) ) ∈ Fin )
110 hashcl ⊢ ( ( ( ( 2 ↑ 𝑗 ) + 1 ) ... ( 2 ↑ ( 𝑗 + 1 ) ) ) ∈ Fin → ( ♯ ‘ ( ( ( 2 ↑ 𝑗 ) + 1 ) ... ( 2 ↑ ( 𝑗 + 1 ) ) ) ) ∈ ℕ0 )
111 109 110 syl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ♯ ‘ ( ( ( 2 ↑ 𝑗 ) + 1 ) ... ( 2 ↑ ( 𝑗 + 1 ) ) ) ) ∈ ℕ0 )
112 111 nn0cnd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ♯ ‘ ( ( ( 2 ↑ 𝑗 ) + 1 ) ... ( 2 ↑ ( 𝑗 + 1 ) ) ) ) ∈ ℂ )
113 simpr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → 𝑗 ∈ ℕ )
114 113 nnzd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → 𝑗 ∈ ℤ )
115 uzid ⊢ ( 𝑗 ∈ ℤ → 𝑗 ∈ ( ℤ≥ ‘ 𝑗 ) )
116 peano2uz ⊢ ( 𝑗 ∈ ( ℤ≥ ‘ 𝑗 ) → ( 𝑗 + 1 ) ∈ ( ℤ≥ ‘ 𝑗 ) )
117 2re ⊢ 2 ∈ ℝ
118 1le2 ⊢ 1 ≤ 2
119 leexp2a ⊢ ( ( 2 ∈ ℝ ∧ 1 ≤ 2 ∧ ( 𝑗 + 1 ) ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( 2 ↑ 𝑗 ) ≤ ( 2 ↑ ( 𝑗 + 1 ) ) )
120 117 118 119 mp3an12 ⊢ ( ( 𝑗 + 1 ) ∈ ( ℤ≥ ‘ 𝑗 ) → ( 2 ↑ 𝑗 ) ≤ ( 2 ↑ ( 𝑗 + 1 ) ) )
121 114 115 116 120 4syl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 2 ↑ 𝑗 ) ≤ ( 2 ↑ ( 𝑗 + 1 ) ) )
122 89 65 eleqtrdi ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 2 ↑ 𝑗 ) ∈ ( ℤ≥ ‘ 1 ) )
123 100 nnzd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 2 ↑ ( 𝑗 + 1 ) ) ∈ ℤ )
124 elfz5 ⊢ ( ( ( 2 ↑ 𝑗 ) ∈ ( ℤ≥ ‘ 1 ) ∧ ( 2 ↑ ( 𝑗 + 1 ) ) ∈ ℤ ) → ( ( 2 ↑ 𝑗 ) ∈ ( 1 ... ( 2 ↑ ( 𝑗 + 1 ) ) ) ↔ ( 2 ↑ 𝑗 ) ≤ ( 2 ↑ ( 𝑗 + 1 ) ) ) )
125 122 123 124 syl2anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( 2 ↑ 𝑗 ) ∈ ( 1 ... ( 2 ↑ ( 𝑗 + 1 ) ) ) ↔ ( 2 ↑ 𝑗 ) ≤ ( 2 ↑ ( 𝑗 + 1 ) ) ) )
126 121 125 mpbird ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 2 ↑ 𝑗 ) ∈ ( 1 ... ( 2 ↑ ( 𝑗 + 1 ) ) ) )
127 fzsplit ⊢ ( ( 2 ↑ 𝑗 ) ∈ ( 1 ... ( 2 ↑ ( 𝑗 + 1 ) ) ) → ( 1 ... ( 2 ↑ ( 𝑗 + 1 ) ) ) = ( ( 1 ... ( 2 ↑ 𝑗 ) ) ∪ ( ( ( 2 ↑ 𝑗 ) + 1 ) ... ( 2 ↑ ( 𝑗 + 1 ) ) ) ) )
128 126 127 syl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 1 ... ( 2 ↑ ( 𝑗 + 1 ) ) ) = ( ( 1 ... ( 2 ↑ 𝑗 ) ) ∪ ( ( ( 2 ↑ 𝑗 ) + 1 ) ... ( 2 ↑ ( 𝑗 + 1 ) ) ) ) )
129 128 fveq2d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ♯ ‘ ( 1 ... ( 2 ↑ ( 𝑗 + 1 ) ) ) ) = ( ♯ ‘ ( ( 1 ... ( 2 ↑ 𝑗 ) ) ∪ ( ( ( 2 ↑ 𝑗 ) + 1 ) ... ( 2 ↑ ( 𝑗 + 1 ) ) ) ) ) )
130 90 times2d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( 2 ↑ 𝑗 ) · 2 ) = ( ( 2 ↑ 𝑗 ) + ( 2 ↑ 𝑗 ) ) )
131 86 130 eqtrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 2 ↑ ( 𝑗 + 1 ) ) = ( ( 2 ↑ 𝑗 ) + ( 2 ↑ 𝑗 ) ) )
132 100 nnnn0d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 2 ↑ ( 𝑗 + 1 ) ) ∈ ℕ0 )
133 hashfz1 ⊢ ( ( 2 ↑ ( 𝑗 + 1 ) ) ∈ ℕ0 → ( ♯ ‘ ( 1 ... ( 2 ↑ ( 𝑗 + 1 ) ) ) ) = ( 2 ↑ ( 𝑗 + 1 ) ) )
134 132 133 syl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ♯ ‘ ( 1 ... ( 2 ↑ ( 𝑗 + 1 ) ) ) ) = ( 2 ↑ ( 𝑗 + 1 ) ) )
135 107 oveq1d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( ♯ ‘ ( 1 ... ( 2 ↑ 𝑗 ) ) ) + ( 2 ↑ 𝑗 ) ) = ( ( 2 ↑ 𝑗 ) + ( 2 ↑ 𝑗 ) ) )
136 131 134 135 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ♯ ‘ ( 1 ... ( 2 ↑ ( 𝑗 + 1 ) ) ) ) = ( ( ♯ ‘ ( 1 ... ( 2 ↑ 𝑗 ) ) ) + ( 2 ↑ 𝑗 ) ) )
137 fzfid ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 1 ... ( 2 ↑ 𝑗 ) ) ∈ Fin )
138 89 nnred ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 2 ↑ 𝑗 ) ∈ ℝ )
139 138 ltp1d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 2 ↑ 𝑗 ) < ( ( 2 ↑ 𝑗 ) + 1 ) )
140 fzdisj ⊢ ( ( 2 ↑ 𝑗 ) < ( ( 2 ↑ 𝑗 ) + 1 ) → ( ( 1 ... ( 2 ↑ 𝑗 ) ) ∩ ( ( ( 2 ↑ 𝑗 ) + 1 ) ... ( 2 ↑ ( 𝑗 + 1 ) ) ) ) = ∅ )
141 139 140 syl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( 1 ... ( 2 ↑ 𝑗 ) ) ∩ ( ( ( 2 ↑ 𝑗 ) + 1 ) ... ( 2 ↑ ( 𝑗 + 1 ) ) ) ) = ∅ )
142 hashun ⊢ ( ( ( 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 ) ) ) ) ) )
143 137 109 141 142 syl3anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ♯ ‘ ( ( 1 ... ( 2 ↑ 𝑗 ) ) ∪ ( ( ( 2 ↑ 𝑗 ) + 1 ) ... ( 2 ↑ ( 𝑗 + 1 ) ) ) ) ) = ( ( ♯ ‘ ( 1 ... ( 2 ↑ 𝑗 ) ) ) + ( ♯ ‘ ( ( ( 2 ↑ 𝑗 ) + 1 ) ... ( 2 ↑ ( 𝑗 + 1 ) ) ) ) ) )
144 129 136 143 3eqtr3d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( ♯ ‘ ( 1 ... ( 2 ↑ 𝑗 ) ) ) + ( 2 ↑ 𝑗 ) ) = ( ( ♯ ‘ ( 1 ... ( 2 ↑ 𝑗 ) ) ) + ( ♯ ‘ ( ( ( 2 ↑ 𝑗 ) + 1 ) ... ( 2 ↑ ( 𝑗 + 1 ) ) ) ) ) )
145 108 90 112 144 addcanad ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 2 ↑ 𝑗 ) = ( ♯ ‘ ( ( ( 2 ↑ 𝑗 ) + 1 ) ... ( 2 ↑ ( 𝑗 + 1 ) ) ) ) )
146 145 oveq1d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( 2 ↑ 𝑗 ) · ( 𝐹 ‘ ( 2 ↑ ( 𝑗 + 1 ) ) ) ) = ( ( ♯ ‘ ( ( ( 2 ↑ 𝑗 ) + 1 ) ... ( 2 ↑ ( 𝑗 + 1 ) ) ) ) · ( 𝐹 ‘ ( 2 ↑ ( 𝑗 + 1 ) ) ) ) )
147 fsumconst ⊢ ( ( ( ( ( 2 ↑ 𝑗 ) + 1 ) ... ( 2 ↑ ( 𝑗 + 1 ) ) ) ∈ Fin ∧ ( 𝐹 ‘ ( 2 ↑ ( 𝑗 + 1 ) ) ) ∈ ℂ ) → Σ 𝑘 ∈ ( ( ( 2 ↑ 𝑗 ) + 1 ) ... ( 2 ↑ ( 𝑗 + 1 ) ) ) ( 𝐹 ‘ ( 2 ↑ ( 𝑗 + 1 ) ) ) = ( ( ♯ ‘ ( ( ( 2 ↑ 𝑗 ) + 1 ) ... ( 2 ↑ ( 𝑗 + 1 ) ) ) ) · ( 𝐹 ‘ ( 2 ↑ ( 𝑗 + 1 ) ) ) ) )
148 109 102 147 syl2anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → Σ 𝑘 ∈ ( ( ( 2 ↑ 𝑗 ) + 1 ) ... ( 2 ↑ ( 𝑗 + 1 ) ) ) ( 𝐹 ‘ ( 2 ↑ ( 𝑗 + 1 ) ) ) = ( ( ♯ ‘ ( ( ( 2 ↑ 𝑗 ) + 1 ) ... ( 2 ↑ ( 𝑗 + 1 ) ) ) ) · ( 𝐹 ‘ ( 2 ↑ ( 𝑗 + 1 ) ) ) ) )
149 146 148 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( 2 ↑ 𝑗 ) · ( 𝐹 ‘ ( 2 ↑ ( 𝑗 + 1 ) ) ) ) = Σ 𝑘 ∈ ( ( ( 2 ↑ 𝑗 ) + 1 ) ... ( 2 ↑ ( 𝑗 + 1 ) ) ) ( 𝐹 ‘ ( 2 ↑ ( 𝑗 + 1 ) ) ) )
150 101 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ ( ( ( 2 ↑ 𝑗 ) + 1 ) ... ( 2 ↑ ( 𝑗 + 1 ) ) ) ) → ( 𝐹 ‘ ( 2 ↑ ( 𝑗 + 1 ) ) ) ∈ ℝ )
151 simpl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → 𝜑 )
152 peano2nn ⊢ ( ( 2 ↑ 𝑗 ) ∈ ℕ → ( ( 2 ↑ 𝑗 ) + 1 ) ∈ ℕ )
153 89 152 syl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( 2 ↑ 𝑗 ) + 1 ) ∈ ℕ )
154 elfzuz ⊢ ( 𝑘 ∈ ( ( ( 2 ↑ 𝑗 ) + 1 ) ... ( 2 ↑ ( 𝑗 + 1 ) ) ) → 𝑘 ∈ ( ℤ≥ ‘ ( ( 2 ↑ 𝑗 ) + 1 ) ) )
155 eluznn ⊢ ( ( ( ( 2 ↑ 𝑗 ) + 1 ) ∈ ℕ ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ( 2 ↑ 𝑗 ) + 1 ) ) ) → 𝑘 ∈ ℕ )
156 153 154 155 syl2an ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ ( ( ( 2 ↑ 𝑗 ) + 1 ) ... ( 2 ↑ ( 𝑗 + 1 ) ) ) ) → 𝑘 ∈ ℕ )
157 151 156 1 syl2an2r ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ ( ( ( 2 ↑ 𝑗 ) + 1 ) ... ( 2 ↑ ( 𝑗 + 1 ) ) ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
158 elfzuz3 ⊢ ( 𝑛 ∈ ( ( ( 2 ↑ 𝑗 ) + 1 ) ... ( 2 ↑ ( 𝑗 + 1 ) ) ) → ( 2 ↑ ( 𝑗 + 1 ) ) ∈ ( ℤ≥ ‘ 𝑛 ) )
159 158 adantl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( ( ( 2 ↑ 𝑗 ) + 1 ) ... ( 2 ↑ ( 𝑗 + 1 ) ) ) ) → ( 2 ↑ ( 𝑗 + 1 ) ) ∈ ( ℤ≥ ‘ 𝑛 ) )
160 simplll ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( ( ( 2 ↑ 𝑗 ) + 1 ) ... ( 2 ↑ ( 𝑗 + 1 ) ) ) ) ∧ 𝑘 ∈ ( 𝑛 ... ( 2 ↑ ( 𝑗 + 1 ) ) ) ) → 𝜑 )
161 elfzuz ⊢ ( 𝑛 ∈ ( ( ( 2 ↑ 𝑗 ) + 1 ) ... ( 2 ↑ ( 𝑗 + 1 ) ) ) → 𝑛 ∈ ( ℤ≥ ‘ ( ( 2 ↑ 𝑗 ) + 1 ) ) )
162 eluznn ⊢ ( ( ( ( 2 ↑ 𝑗 ) + 1 ) ∈ ℕ ∧ 𝑛 ∈ ( ℤ≥ ‘ ( ( 2 ↑ 𝑗 ) + 1 ) ) ) → 𝑛 ∈ ℕ )
163 153 161 162 syl2an ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( ( ( 2 ↑ 𝑗 ) + 1 ) ... ( 2 ↑ ( 𝑗 + 1 ) ) ) ) → 𝑛 ∈ ℕ )
164 elfzuz ⊢ ( 𝑘 ∈ ( 𝑛 ... ( 2 ↑ ( 𝑗 + 1 ) ) ) → 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) )
165 eluznn ⊢ ( ( 𝑛 ∈ ℕ ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) ) → 𝑘 ∈ ℕ )
166 163 164 165 syl2an ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( ( ( 2 ↑ 𝑗 ) + 1 ) ... ( 2 ↑ ( 𝑗 + 1 ) ) ) ) ∧ 𝑘 ∈ ( 𝑛 ... ( 2 ↑ ( 𝑗 + 1 ) ) ) ) → 𝑘 ∈ ℕ )
167 160 166 1 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( ( ( 2 ↑ 𝑗 ) + 1 ) ... ( 2 ↑ ( 𝑗 + 1 ) ) ) ) ∧ 𝑘 ∈ ( 𝑛 ... ( 2 ↑ ( 𝑗 + 1 ) ) ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
168 simplll ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( ( ( 2 ↑ 𝑗 ) + 1 ) ... ( 2 ↑ ( 𝑗 + 1 ) ) ) ) ∧ 𝑘 ∈ ( 𝑛 ... ( ( 2 ↑ ( 𝑗 + 1 ) ) − 1 ) ) ) → 𝜑 )
169 elfzuz ⊢ ( 𝑘 ∈ ( 𝑛 ... ( ( 2 ↑ ( 𝑗 + 1 ) ) − 1 ) ) → 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) )
170 163 169 165 syl2an ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( ( ( 2 ↑ 𝑗 ) + 1 ) ... ( 2 ↑ ( 𝑗 + 1 ) ) ) ) ∧ 𝑘 ∈ ( 𝑛 ... ( ( 2 ↑ ( 𝑗 + 1 ) ) − 1 ) ) ) → 𝑘 ∈ ℕ )
171 168 170 3 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( ( ( 2 ↑ 𝑗 ) + 1 ) ... ( 2 ↑ ( 𝑗 + 1 ) ) ) ) ∧ 𝑘 ∈ ( 𝑛 ... ( ( 2 ↑ ( 𝑗 + 1 ) ) − 1 ) ) ) → ( 𝐹 ‘ ( 𝑘 + 1 ) ) ≤ ( 𝐹 ‘ 𝑘 ) )
172 159 167 171 monoord2 ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( ( ( 2 ↑ 𝑗 ) + 1 ) ... ( 2 ↑ ( 𝑗 + 1 ) ) ) ) → ( 𝐹 ‘ ( 2 ↑ ( 𝑗 + 1 ) ) ) ≤ ( 𝐹 ‘ 𝑛 ) )
173 172 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ∀ 𝑛 ∈ ( ( ( 2 ↑ 𝑗 ) + 1 ) ... ( 2 ↑ ( 𝑗 + 1 ) ) ) ( 𝐹 ‘ ( 2 ↑ ( 𝑗 + 1 ) ) ) ≤ ( 𝐹 ‘ 𝑛 ) )
174 fveq2 ⊢ ( 𝑛 = 𝑘 → ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ 𝑘 ) )
175 174 breq2d ⊢ ( 𝑛 = 𝑘 → ( ( 𝐹 ‘ ( 2 ↑ ( 𝑗 + 1 ) ) ) ≤ ( 𝐹 ‘ 𝑛 ) ↔ ( 𝐹 ‘ ( 2 ↑ ( 𝑗 + 1 ) ) ) ≤ ( 𝐹 ‘ 𝑘 ) ) )
176 175 rspccva ⊢ ( ( ∀ 𝑛 ∈ ( ( ( 2 ↑ 𝑗 ) + 1 ) ... ( 2 ↑ ( 𝑗 + 1 ) ) ) ( 𝐹 ‘ ( 2 ↑ ( 𝑗 + 1 ) ) ) ≤ ( 𝐹 ‘ 𝑛 ) ∧ 𝑘 ∈ ( ( ( 2 ↑ 𝑗 ) + 1 ) ... ( 2 ↑ ( 𝑗 + 1 ) ) ) ) → ( 𝐹 ‘ ( 2 ↑ ( 𝑗 + 1 ) ) ) ≤ ( 𝐹 ‘ 𝑘 ) )
177 173 176 sylan ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ ( ( ( 2 ↑ 𝑗 ) + 1 ) ... ( 2 ↑ ( 𝑗 + 1 ) ) ) ) → ( 𝐹 ‘ ( 2 ↑ ( 𝑗 + 1 ) ) ) ≤ ( 𝐹 ‘ 𝑘 ) )
178 109 150 157 177 fsumle ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → Σ 𝑘 ∈ ( ( ( 2 ↑ 𝑗 ) + 1 ) ... ( 2 ↑ ( 𝑗 + 1 ) ) ) ( 𝐹 ‘ ( 2 ↑ ( 𝑗 + 1 ) ) ) ≤ Σ 𝑘 ∈ ( ( ( 2 ↑ 𝑗 ) + 1 ) ... ( 2 ↑ ( 𝑗 + 1 ) ) ) ( 𝐹 ‘ 𝑘 ) )
179 149 178 eqbrtrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( 2 ↑ 𝑗 ) · ( 𝐹 ‘ ( 2 ↑ ( 𝑗 + 1 ) ) ) ) ≤ Σ 𝑘 ∈ ( ( ( 2 ↑ 𝑗 ) + 1 ) ... ( 2 ↑ ( 𝑗 + 1 ) ) ) ( 𝐹 ‘ 𝑘 ) )
180 138 101 remulcld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( 2 ↑ 𝑗 ) · ( 𝐹 ‘ ( 2 ↑ ( 𝑗 + 1 ) ) ) ) ∈ ℝ )
181 109 157 fsumrecl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → Σ 𝑘 ∈ ( ( ( 2 ↑ 𝑗 ) + 1 ) ... ( 2 ↑ ( 𝑗 + 1 ) ) ) ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
182 2rp ⊢ 2 ∈ ℝ+
183 182 a1i ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → 2 ∈ ℝ+ )
184 180 181 183 lemul2d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( ( 2 ↑ 𝑗 ) · ( 𝐹 ‘ ( 2 ↑ ( 𝑗 + 1 ) ) ) ) ≤ Σ 𝑘 ∈ ( ( ( 2 ↑ 𝑗 ) + 1 ) ... ( 2 ↑ ( 𝑗 + 1 ) ) ) ( 𝐹 ‘ 𝑘 ) ↔ ( 2 · ( ( 2 ↑ 𝑗 ) · ( 𝐹 ‘ ( 2 ↑ ( 𝑗 + 1 ) ) ) ) ) ≤ ( 2 · Σ 𝑘 ∈ ( ( ( 2 ↑ 𝑗 ) + 1 ) ... ( 2 ↑ ( 𝑗 + 1 ) ) ) ( 𝐹 ‘ 𝑘 ) ) ) )
185 179 184 mpbid ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 2 · ( ( 2 ↑ 𝑗 ) · ( 𝐹 ‘ ( 2 ↑ ( 𝑗 + 1 ) ) ) ) ) ≤ ( 2 · Σ 𝑘 ∈ ( ( ( 2 ↑ 𝑗 ) + 1 ) ... ( 2 ↑ ( 𝑗 + 1 ) ) ) ( 𝐹 ‘ 𝑘 ) ) )
186 104 185 eqbrtrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝐺 ‘ ( 𝑗 + 1 ) ) ≤ ( 2 · Σ 𝑘 ∈ ( ( ( 2 ↑ 𝑗 ) + 1 ) ... ( 2 ↑ ( 𝑗 + 1 ) ) ) ( 𝐹 ‘ 𝑘 ) ) )
187 1zzd ⊢ ( 𝜑 → 1 ∈ ℤ )
188 nnnn0 ⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℕ0 )
189 simpr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → 𝑛 ∈ ℕ0 )
190 nnexpcl ⊢ ( ( 2 ∈ ℕ ∧ 𝑛 ∈ ℕ0 ) → ( 2 ↑ 𝑛 ) ∈ ℕ )
191 42 189 190 sylancr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( 2 ↑ 𝑛 ) ∈ ℕ )
192 191 nnred ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( 2 ↑ 𝑛 ) ∈ ℝ )
193 fveq2 ⊢ ( 𝑘 = ( 2 ↑ 𝑛 ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ ( 2 ↑ 𝑛 ) ) )
194 193 eleq1d ⊢ ( 𝑘 = ( 2 ↑ 𝑛 ) → ( ( 𝐹 ‘ 𝑘 ) ∈ ℝ ↔ ( 𝐹 ‘ ( 2 ↑ 𝑛 ) ) ∈ ℝ ) )
195 41 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ∀ 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
196 194 195 191 rspcdva ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( 𝐹 ‘ ( 2 ↑ 𝑛 ) ) ∈ ℝ )
197 192 196 remulcld ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( ( 2 ↑ 𝑛 ) · ( 𝐹 ‘ ( 2 ↑ 𝑛 ) ) ) ∈ ℝ )
198 4 197 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( 𝐺 ‘ 𝑛 ) ∈ ℝ )
199 188 198 sylan2 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐺 ‘ 𝑛 ) ∈ ℝ )
200 65 187 199 serfre ⊢ ( 𝜑 → seq 1 ( + , 𝐺 ) : ℕ ⟶ ℝ )
201 200 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( seq 1 ( + , 𝐺 ) ‘ 𝑗 ) ∈ ℝ )
202 73 eleq1d ⊢ ( 𝑛 = ( 𝑗 + 1 ) → ( ( 𝐺 ‘ 𝑛 ) ∈ ℝ ↔ ( 𝐺 ‘ ( 𝑗 + 1 ) ) ∈ ℝ ) )
203 199 ralrimiva ⊢ ( 𝜑 → ∀ 𝑛 ∈ ℕ ( 𝐺 ‘ 𝑛 ) ∈ ℝ )
204 203 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ∀ 𝑛 ∈ ℕ ( 𝐺 ‘ 𝑛 ) ∈ ℝ )
205 202 204 80 rspcdva ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝐺 ‘ ( 𝑗 + 1 ) ) ∈ ℝ )
206 65 187 1 serfre ⊢ ( 𝜑 → seq 1 ( + , 𝐹 ) : ℕ ⟶ ℝ )
207 ffvelcdm ⊢ ( ( seq 1 ( + , 𝐹 ) : ℕ ⟶ ℝ ∧ ( 2 ↑ 𝑗 ) ∈ ℕ ) → ( seq 1 ( + , 𝐹 ) ‘ ( 2 ↑ 𝑗 ) ) ∈ ℝ )
208 206 88 207 syl2an ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( seq 1 ( + , 𝐹 ) ‘ ( 2 ↑ 𝑗 ) ) ∈ ℝ )
209 remulcl ⊢ ( ( 2 ∈ ℝ ∧ ( seq 1 ( + , 𝐹 ) ‘ ( 2 ↑ 𝑗 ) ) ∈ ℝ ) → ( 2 · ( seq 1 ( + , 𝐹 ) ‘ ( 2 ↑ 𝑗 ) ) ) ∈ ℝ )
210 117 208 209 sylancr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 2 · ( seq 1 ( + , 𝐹 ) ‘ ( 2 ↑ 𝑗 ) ) ) ∈ ℝ )
211 remulcl ⊢ ( ( 2 ∈ ℝ ∧ Σ 𝑘 ∈ ( ( ( 2 ↑ 𝑗 ) + 1 ) ... ( 2 ↑ ( 𝑗 + 1 ) ) ) ( 𝐹 ‘ 𝑘 ) ∈ ℝ ) → ( 2 · Σ 𝑘 ∈ ( ( ( 2 ↑ 𝑗 ) + 1 ) ... ( 2 ↑ ( 𝑗 + 1 ) ) ) ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ )
212 117 181 211 sylancr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 2 · Σ 𝑘 ∈ ( ( ( 2 ↑ 𝑗 ) + 1 ) ... ( 2 ↑ ( 𝑗 + 1 ) ) ) ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ )
213 le2add ⊢ ( ( ( ( seq 1 ( + , 𝐺 ) ‘ 𝑗 ) ∈ ℝ ∧ ( 𝐺 ‘ ( 𝑗 + 1 ) ) ∈ ℝ ) ∧ ( ( 2 · ( seq 1 ( + , 𝐹 ) ‘ ( 2 ↑ 𝑗 ) ) ) ∈ ℝ ∧ ( 2 · Σ 𝑘 ∈ ( ( ( 2 ↑ 𝑗 ) + 1 ) ... ( 2 ↑ ( 𝑗 + 1 ) ) ) ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ) ) → ( ( ( seq 1 ( + , 𝐺 ) ‘ 𝑗 ) ≤ ( 2 · ( seq 1 ( + , 𝐹 ) ‘ ( 2 ↑ 𝑗 ) ) ) ∧ ( 𝐺 ‘ ( 𝑗 + 1 ) ) ≤ ( 2 · Σ 𝑘 ∈ ( ( ( 2 ↑ 𝑗 ) + 1 ) ... ( 2 ↑ ( 𝑗 + 1 ) ) ) ( 𝐹 ‘ 𝑘 ) ) ) → ( ( seq 1 ( + , 𝐺 ) ‘ 𝑗 ) + ( 𝐺 ‘ ( 𝑗 + 1 ) ) ) ≤ ( ( 2 · ( seq 1 ( + , 𝐹 ) ‘ ( 2 ↑ 𝑗 ) ) ) + ( 2 · Σ 𝑘 ∈ ( ( ( 2 ↑ 𝑗 ) + 1 ) ... ( 2 ↑ ( 𝑗 + 1 ) ) ) ( 𝐹 ‘ 𝑘 ) ) ) ) )
214 201 205 210 212 213 syl22anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( ( seq 1 ( + , 𝐺 ) ‘ 𝑗 ) ≤ ( 2 · ( seq 1 ( + , 𝐹 ) ‘ ( 2 ↑ 𝑗 ) ) ) ∧ ( 𝐺 ‘ ( 𝑗 + 1 ) ) ≤ ( 2 · Σ 𝑘 ∈ ( ( ( 2 ↑ 𝑗 ) + 1 ) ... ( 2 ↑ ( 𝑗 + 1 ) ) ) ( 𝐹 ‘ 𝑘 ) ) ) → ( ( seq 1 ( + , 𝐺 ) ‘ 𝑗 ) + ( 𝐺 ‘ ( 𝑗 + 1 ) ) ) ≤ ( ( 2 · ( seq 1 ( + , 𝐹 ) ‘ ( 2 ↑ 𝑗 ) ) ) + ( 2 · Σ 𝑘 ∈ ( ( ( 2 ↑ 𝑗 ) + 1 ) ... ( 2 ↑ ( 𝑗 + 1 ) ) ) ( 𝐹 ‘ 𝑘 ) ) ) ) )
215 186 214 mpan2d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( seq 1 ( + , 𝐺 ) ‘ 𝑗 ) ≤ ( 2 · ( seq 1 ( + , 𝐹 ) ‘ ( 2 ↑ 𝑗 ) ) ) → ( ( seq 1 ( + , 𝐺 ) ‘ 𝑗 ) + ( 𝐺 ‘ ( 𝑗 + 1 ) ) ) ≤ ( ( 2 · ( seq 1 ( + , 𝐹 ) ‘ ( 2 ↑ 𝑗 ) ) ) + ( 2 · Σ 𝑘 ∈ ( ( ( 2 ↑ 𝑗 ) + 1 ) ... ( 2 ↑ ( 𝑗 + 1 ) ) ) ( 𝐹 ‘ 𝑘 ) ) ) ) )
216 113 65 eleqtrdi ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → 𝑗 ∈ ( ℤ≥ ‘ 1 ) )
217 seqp1 ⊢ ( 𝑗 ∈ ( ℤ≥ ‘ 1 ) → ( seq 1 ( + , 𝐺 ) ‘ ( 𝑗 + 1 ) ) = ( ( seq 1 ( + , 𝐺 ) ‘ 𝑗 ) + ( 𝐺 ‘ ( 𝑗 + 1 ) ) ) )
218 216 217 syl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( seq 1 ( + , 𝐺 ) ‘ ( 𝑗 + 1 ) ) = ( ( seq 1 ( + , 𝐺 ) ‘ 𝑗 ) + ( 𝐺 ‘ ( 𝑗 + 1 ) ) ) )
219 fzfid ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 1 ... ( 2 ↑ ( 𝑗 + 1 ) ) ) ∈ Fin )
220 elfznn ⊢ ( 𝑘 ∈ ( 1 ... ( 2 ↑ ( 𝑗 + 1 ) ) ) → 𝑘 ∈ ℕ )
221 1 recnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
222 151 220 221 syl2an ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... ( 2 ↑ ( 𝑗 + 1 ) ) ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
223 141 128 219 222 fsumsplit ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → Σ 𝑘 ∈ ( 1 ... ( 2 ↑ ( 𝑗 + 1 ) ) ) ( 𝐹 ‘ 𝑘 ) = ( Σ 𝑘 ∈ ( 1 ... ( 2 ↑ 𝑗 ) ) ( 𝐹 ‘ 𝑘 ) + Σ 𝑘 ∈ ( ( ( 2 ↑ 𝑗 ) + 1 ) ... ( 2 ↑ ( 𝑗 + 1 ) ) ) ( 𝐹 ‘ 𝑘 ) ) )
224 eqidd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... ( 2 ↑ ( 𝑗 + 1 ) ) ) ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑘 ) )
225 100 65 eleqtrdi ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 2 ↑ ( 𝑗 + 1 ) ) ∈ ( ℤ≥ ‘ 1 ) )
226 224 225 222 fsumser ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → Σ 𝑘 ∈ ( 1 ... ( 2 ↑ ( 𝑗 + 1 ) ) ) ( 𝐹 ‘ 𝑘 ) = ( seq 1 ( + , 𝐹 ) ‘ ( 2 ↑ ( 𝑗 + 1 ) ) ) )
227 eqidd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... ( 2 ↑ 𝑗 ) ) ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑘 ) )
228 elfznn ⊢ ( 𝑘 ∈ ( 1 ... ( 2 ↑ 𝑗 ) ) → 𝑘 ∈ ℕ )
229 151 228 221 syl2an ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... ( 2 ↑ 𝑗 ) ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
230 227 122 229 fsumser ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → Σ 𝑘 ∈ ( 1 ... ( 2 ↑ 𝑗 ) ) ( 𝐹 ‘ 𝑘 ) = ( seq 1 ( + , 𝐹 ) ‘ ( 2 ↑ 𝑗 ) ) )
231 230 oveq1d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( Σ 𝑘 ∈ ( 1 ... ( 2 ↑ 𝑗 ) ) ( 𝐹 ‘ 𝑘 ) + Σ 𝑘 ∈ ( ( ( 2 ↑ 𝑗 ) + 1 ) ... ( 2 ↑ ( 𝑗 + 1 ) ) ) ( 𝐹 ‘ 𝑘 ) ) = ( ( seq 1 ( + , 𝐹 ) ‘ ( 2 ↑ 𝑗 ) ) + Σ 𝑘 ∈ ( ( ( 2 ↑ 𝑗 ) + 1 ) ... ( 2 ↑ ( 𝑗 + 1 ) ) ) ( 𝐹 ‘ 𝑘 ) ) )
232 223 226 231 3eqtr3d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( seq 1 ( + , 𝐹 ) ‘ ( 2 ↑ ( 𝑗 + 1 ) ) ) = ( ( seq 1 ( + , 𝐹 ) ‘ ( 2 ↑ 𝑗 ) ) + Σ 𝑘 ∈ ( ( ( 2 ↑ 𝑗 ) + 1 ) ... ( 2 ↑ ( 𝑗 + 1 ) ) ) ( 𝐹 ‘ 𝑘 ) ) )
233 232 oveq2d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 2 · ( seq 1 ( + , 𝐹 ) ‘ ( 2 ↑ ( 𝑗 + 1 ) ) ) ) = ( 2 · ( ( seq 1 ( + , 𝐹 ) ‘ ( 2 ↑ 𝑗 ) ) + Σ 𝑘 ∈ ( ( ( 2 ↑ 𝑗 ) + 1 ) ... ( 2 ↑ ( 𝑗 + 1 ) ) ) ( 𝐹 ‘ 𝑘 ) ) ) )
234 208 recnd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( seq 1 ( + , 𝐹 ) ‘ ( 2 ↑ 𝑗 ) ) ∈ ℂ )
235 181 recnd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → Σ 𝑘 ∈ ( ( ( 2 ↑ 𝑗 ) + 1 ) ... ( 2 ↑ ( 𝑗 + 1 ) ) ) ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
236 95 234 235 adddid ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 2 · ( ( seq 1 ( + , 𝐹 ) ‘ ( 2 ↑ 𝑗 ) ) + Σ 𝑘 ∈ ( ( ( 2 ↑ 𝑗 ) + 1 ) ... ( 2 ↑ ( 𝑗 + 1 ) ) ) ( 𝐹 ‘ 𝑘 ) ) ) = ( ( 2 · ( seq 1 ( + , 𝐹 ) ‘ ( 2 ↑ 𝑗 ) ) ) + ( 2 · Σ 𝑘 ∈ ( ( ( 2 ↑ 𝑗 ) + 1 ) ... ( 2 ↑ ( 𝑗 + 1 ) ) ) ( 𝐹 ‘ 𝑘 ) ) ) )
237 233 236 eqtrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 2 · ( seq 1 ( + , 𝐹 ) ‘ ( 2 ↑ ( 𝑗 + 1 ) ) ) ) = ( ( 2 · ( seq 1 ( + , 𝐹 ) ‘ ( 2 ↑ 𝑗 ) ) ) + ( 2 · Σ 𝑘 ∈ ( ( ( 2 ↑ 𝑗 ) + 1 ) ... ( 2 ↑ ( 𝑗 + 1 ) ) ) ( 𝐹 ‘ 𝑘 ) ) ) )
238 218 237 breq12d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( seq 1 ( + , 𝐺 ) ‘ ( 𝑗 + 1 ) ) ≤ ( 2 · ( seq 1 ( + , 𝐹 ) ‘ ( 2 ↑ ( 𝑗 + 1 ) ) ) ) ↔ ( ( seq 1 ( + , 𝐺 ) ‘ 𝑗 ) + ( 𝐺 ‘ ( 𝑗 + 1 ) ) ) ≤ ( ( 2 · ( seq 1 ( + , 𝐹 ) ‘ ( 2 ↑ 𝑗 ) ) ) + ( 2 · Σ 𝑘 ∈ ( ( ( 2 ↑ 𝑗 ) + 1 ) ... ( 2 ↑ ( 𝑗 + 1 ) ) ) ( 𝐹 ‘ 𝑘 ) ) ) ) )
239 215 238 sylibrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( seq 1 ( + , 𝐺 ) ‘ 𝑗 ) ≤ ( 2 · ( seq 1 ( + , 𝐹 ) ‘ ( 2 ↑ 𝑗 ) ) ) → ( seq 1 ( + , 𝐺 ) ‘ ( 𝑗 + 1 ) ) ≤ ( 2 · ( seq 1 ( + , 𝐹 ) ‘ ( 2 ↑ ( 𝑗 + 1 ) ) ) ) ) )
240 239 expcom ⊢ ( 𝑗 ∈ ℕ → ( 𝜑 → ( ( seq 1 ( + , 𝐺 ) ‘ 𝑗 ) ≤ ( 2 · ( seq 1 ( + , 𝐹 ) ‘ ( 2 ↑ 𝑗 ) ) ) → ( seq 1 ( + , 𝐺 ) ‘ ( 𝑗 + 1 ) ) ≤ ( 2 · ( seq 1 ( + , 𝐹 ) ‘ ( 2 ↑ ( 𝑗 + 1 ) ) ) ) ) ) )
241 240 a2d ⊢ ( 𝑗 ∈ ℕ → ( ( 𝜑 → ( seq 1 ( + , 𝐺 ) ‘ 𝑗 ) ≤ ( 2 · ( seq 1 ( + , 𝐹 ) ‘ ( 2 ↑ 𝑗 ) ) ) ) → ( 𝜑 → ( seq 1 ( + , 𝐺 ) ‘ ( 𝑗 + 1 ) ) ≤ ( 2 · ( seq 1 ( + , 𝐹 ) ‘ ( 2 ↑ ( 𝑗 + 1 ) ) ) ) ) ) )
242 14 20 26 32 72 241 nnind ⊢ ( 𝑁 ∈ ℕ → ( 𝜑 → ( seq 1 ( + , 𝐺 ) ‘ 𝑁 ) ≤ ( 2 · ( seq 1 ( + , 𝐹 ) ‘ ( 2 ↑ 𝑁 ) ) ) ) )
243 242 impcom ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ℕ ) → ( seq 1 ( + , 𝐺 ) ‘ 𝑁 ) ≤ ( 2 · ( seq 1 ( + , 𝐹 ) ‘ ( 2 ↑ 𝑁 ) ) ) )