Metamath Proof Explorer

Theorem climcndslem1

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

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

Proof

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