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 ( + , 𝐺 ) ‘ 𝑁 ) )