climcndslem1 - Metamath Proof Explorer

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

Theorem climcndslem1 14581

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

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

**Assertion**
Ref	Expression
climcndslem1	⊢ ((𝜑 ∧ 𝑁 ∈ ℕ₀) → (seq1( + , 𝐹)‘((2↑(𝑁 + 1)) − 1)) ≤ (seq0( + , 𝐺)‘𝑁))

Distinct variable groups: 𝑘,𝑛,𝐹 𝑘,𝐺,𝑛 𝜑,𝑘,𝑛 Allowed substitution hints: 𝑁(𝑘,𝑛)

Proof of Theorem climcndslem1 Dummy variables 𝑗 𝑥 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		oveq1 6657	. . . . . . . . . . 11 ⊢ (𝑥 = 0 → (𝑥 + 1) = (0 + 1))
2		0p1e1 11132	. . . . . . . . . . 11 ⊢ (0 + 1) = 1
3	1, 2	syl6eq 2672	. . . . . . . . . 10 ⊢ (𝑥 = 0 → (𝑥 + 1) = 1)
4	3	oveq2d 6666	. . . . . . . . 9 ⊢ (𝑥 = 0 → (2↑(𝑥 + 1)) = (2↑1))
5		2cn 11091	. . . . . . . . . . 11 ⊢ 2 ∈ ℂ
6		exp1 12866	. . . . . . . . . . 11 ⊢ (2 ∈ ℂ → (2↑1) = 2)
7	5, 6	ax-mp 5	. . . . . . . . . 10 ⊢ (2↑1) = 2
8		df-2 11079	. . . . . . . . . 10 ⊢ 2 = (1 + 1)
9	7, 8	eqtri 2644	. . . . . . . . 9 ⊢ (2↑1) = (1 + 1)
10	4, 9	syl6eq 2672	. . . . . . . 8 ⊢ (𝑥 = 0 → (2↑(𝑥 + 1)) = (1 + 1))
11	10	oveq1d 6665	. . . . . . 7 ⊢ (𝑥 = 0 → ((2↑(𝑥 + 1)) − 1) = ((1 + 1) − 1))
12		ax-1cn 9994	. . . . . . . 8 ⊢ 1 ∈ ℂ
13	12, 12	pncan3oi 10297	. . . . . . 7 ⊢ ((1 + 1) − 1) = 1
14	11, 13	syl6eq 2672	. . . . . 6 ⊢ (𝑥 = 0 → ((2↑(𝑥 + 1)) − 1) = 1)
15	14	fveq2d 6195	. . . . 5 ⊢ (𝑥 = 0 → (seq1( + , 𝐹)‘((2↑(𝑥 + 1)) − 1)) = (seq1( + , 𝐹)‘1))
16		fveq2 6191	. . . . 5 ⊢ (𝑥 = 0 → (seq0( + , 𝐺)‘𝑥) = (seq0( + , 𝐺)‘0))
17	15, 16	breq12d 4666	. . . 4 ⊢ (𝑥 = 0 → ((seq1( + , 𝐹)‘((2↑(𝑥 + 1)) − 1)) ≤ (seq0( + , 𝐺)‘𝑥) ↔ (seq1( + , 𝐹)‘1) ≤ (seq0( + , 𝐺)‘0)))
18	17	imbi2d 330	. . 3 ⊢ (𝑥 = 0 → ((𝜑 → (seq1( + , 𝐹)‘((2↑(𝑥 + 1)) − 1)) ≤ (seq0( + , 𝐺)‘𝑥)) ↔ (𝜑 → (seq1( + , 𝐹)‘1) ≤ (seq0( + , 𝐺)‘0))))
19		oveq1 6657	. . . . . . . 8 ⊢ (𝑥 = 𝑗 → (𝑥 + 1) = (𝑗 + 1))
20	19	oveq2d 6666	. . . . . . 7 ⊢ (𝑥 = 𝑗 → (2↑(𝑥 + 1)) = (2↑(𝑗 + 1)))
21	20	oveq1d 6665	. . . . . 6 ⊢ (𝑥 = 𝑗 → ((2↑(𝑥 + 1)) − 1) = ((2↑(𝑗 + 1)) − 1))
22	21	fveq2d 6195	. . . . 5 ⊢ (𝑥 = 𝑗 → (seq1( + , 𝐹)‘((2↑(𝑥 + 1)) − 1)) = (seq1( + , 𝐹)‘((2↑(𝑗 + 1)) − 1)))
23		fveq2 6191	. . . . 5 ⊢ (𝑥 = 𝑗 → (seq0( + , 𝐺)‘𝑥) = (seq0( + , 𝐺)‘𝑗))
24	22, 23	breq12d 4666	. . . 4 ⊢ (𝑥 = 𝑗 → ((seq1( + , 𝐹)‘((2↑(𝑥 + 1)) − 1)) ≤ (seq0( + , 𝐺)‘𝑥) ↔ (seq1( + , 𝐹)‘((2↑(𝑗 + 1)) − 1)) ≤ (seq0( + , 𝐺)‘𝑗)))
25	24	imbi2d 330	. . 3 ⊢ (𝑥 = 𝑗 → ((𝜑 → (seq1( + , 𝐹)‘((2↑(𝑥 + 1)) − 1)) ≤ (seq0( + , 𝐺)‘𝑥)) ↔ (𝜑 → (seq1( + , 𝐹)‘((2↑(𝑗 + 1)) − 1)) ≤ (seq0( + , 𝐺)‘𝑗))))
26		oveq1 6657	. . . . . . . 8 ⊢ (𝑥 = (𝑗 + 1) → (𝑥 + 1) = ((𝑗 + 1) + 1))
27	26	oveq2d 6666	. . . . . . 7 ⊢ (𝑥 = (𝑗 + 1) → (2↑(𝑥 + 1)) = (2↑((𝑗 + 1) + 1)))
28	27	oveq1d 6665	. . . . . 6 ⊢ (𝑥 = (𝑗 + 1) → ((2↑(𝑥 + 1)) − 1) = ((2↑((𝑗 + 1) + 1)) − 1))
29	28	fveq2d 6195	. . . . 5 ⊢ (𝑥 = (𝑗 + 1) → (seq1( + , 𝐹)‘((2↑(𝑥 + 1)) − 1)) = (seq1( + , 𝐹)‘((2↑((𝑗 + 1) + 1)) − 1)))
30		fveq2 6191	. . . . 5 ⊢ (𝑥 = (𝑗 + 1) → (seq0( + , 𝐺)‘𝑥) = (seq0( + , 𝐺)‘(𝑗 + 1)))
31	29, 30	breq12d 4666	. . . 4 ⊢ (𝑥 = (𝑗 + 1) → ((seq1( + , 𝐹)‘((2↑(𝑥 + 1)) − 1)) ≤ (seq0( + , 𝐺)‘𝑥) ↔ (seq1( + , 𝐹)‘((2↑((𝑗 + 1) + 1)) − 1)) ≤ (seq0( + , 𝐺)‘(𝑗 + 1))))
32	31	imbi2d 330	. . 3 ⊢ (𝑥 = (𝑗 + 1) → ((𝜑 → (seq1( + , 𝐹)‘((2↑(𝑥 + 1)) − 1)) ≤ (seq0( + , 𝐺)‘𝑥)) ↔ (𝜑 → (seq1( + , 𝐹)‘((2↑((𝑗 + 1) + 1)) − 1)) ≤ (seq0( + , 𝐺)‘(𝑗 + 1)))))
33		oveq1 6657	. . . . . . . 8 ⊢ (𝑥 = 𝑁 → (𝑥 + 1) = (𝑁 + 1))
34	33	oveq2d 6666	. . . . . . 7 ⊢ (𝑥 = 𝑁 → (2↑(𝑥 + 1)) = (2↑(𝑁 + 1)))
35	34	oveq1d 6665	. . . . . 6 ⊢ (𝑥 = 𝑁 → ((2↑(𝑥 + 1)) − 1) = ((2↑(𝑁 + 1)) − 1))
36	35	fveq2d 6195	. . . . 5 ⊢ (𝑥 = 𝑁 → (seq1( + , 𝐹)‘((2↑(𝑥 + 1)) − 1)) = (seq1( + , 𝐹)‘((2↑(𝑁 + 1)) − 1)))
37		fveq2 6191	. . . . 5 ⊢ (𝑥 = 𝑁 → (seq0( + , 𝐺)‘𝑥) = (seq0( + , 𝐺)‘𝑁))
38	36, 37	breq12d 4666	. . . 4 ⊢ (𝑥 = 𝑁 → ((seq1( + , 𝐹)‘((2↑(𝑥 + 1)) − 1)) ≤ (seq0( + , 𝐺)‘𝑥) ↔ (seq1( + , 𝐹)‘((2↑(𝑁 + 1)) − 1)) ≤ (seq0( + , 𝐺)‘𝑁)))
39	38	imbi2d 330	. . 3 ⊢ (𝑥 = 𝑁 → ((𝜑 → (seq1( + , 𝐹)‘((2↑(𝑥 + 1)) − 1)) ≤ (seq0( + , 𝐺)‘𝑥)) ↔ (𝜑 → (seq1( + , 𝐹)‘((2↑(𝑁 + 1)) − 1)) ≤ (seq0( + , 𝐺)‘𝑁))))
40		1nn 11031	. . . . . . 7 ⊢ 1 ∈ ℕ
41		climcnds.1	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) ∈ ℝ)
42	41	ralrimiva 2966	. . . . . . 7 ⊢ (𝜑 → ∀𝑘 ∈ ℕ (𝐹‘𝑘) ∈ ℝ)
43		fveq2 6191	. . . . . . . . 9 ⊢ (𝑘 = 1 → (𝐹‘𝑘) = (𝐹‘1))
44	43	eleq1d 2686	. . . . . . . 8 ⊢ (𝑘 = 1 → ((𝐹‘𝑘) ∈ ℝ ↔ (𝐹‘1) ∈ ℝ))
45	44	rspcv 3305	. . . . . . 7 ⊢ (1 ∈ ℕ → (∀𝑘 ∈ ℕ (𝐹‘𝑘) ∈ ℝ → (𝐹‘1) ∈ ℝ))
46	40, 42, 45	mpsyl 68	. . . . . 6 ⊢ (𝜑 → (𝐹‘1) ∈ ℝ)
47	46	leidd 10594	. . . . 5 ⊢ (𝜑 → (𝐹‘1) ≤ (𝐹‘1))
48	46	recnd 10068	. . . . . 6 ⊢ (𝜑 → (𝐹‘1) ∈ ℂ)
49	48	mulid2d 10058	. . . . 5 ⊢ (𝜑 → (1 · (𝐹‘1)) = (𝐹‘1))
50	47, 49	breqtrrd 4681	. . . 4 ⊢ (𝜑 → (𝐹‘1) ≤ (1 · (𝐹‘1)))
51		1z 11407	. . . . 5 ⊢ 1 ∈ ℤ
52		eqidd 2623	. . . . 5 ⊢ (𝜑 → (𝐹‘1) = (𝐹‘1))
53	51, 52	seq1i 12815	. . . 4 ⊢ (𝜑 → (seq1( + , 𝐹)‘1) = (𝐹‘1))
54		0z 11388	. . . . 5 ⊢ 0 ∈ ℤ
55		0nn0 11307	. . . . . 6 ⊢ 0 ∈ ℕ₀
56		climcnds.4	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → (𝐺‘𝑛) = ((2↑𝑛) · (𝐹‘(2↑𝑛))))
57	56	ralrimiva 2966	. . . . . 6 ⊢ (𝜑 → ∀𝑛 ∈ ℕ₀ (𝐺‘𝑛) = ((2↑𝑛) · (𝐹‘(2↑𝑛))))
58		fveq2 6191	. . . . . . . 8 ⊢ (𝑛 = 0 → (𝐺‘𝑛) = (𝐺‘0))
59		oveq2 6658	. . . . . . . . . 10 ⊢ (𝑛 = 0 → (2↑𝑛) = (2↑0))
60		exp0 12864	. . . . . . . . . . 11 ⊢ (2 ∈ ℂ → (2↑0) = 1)
61	5, 60	ax-mp 5	. . . . . . . . . 10 ⊢ (2↑0) = 1
62	59, 61	syl6eq 2672	. . . . . . . . 9 ⊢ (𝑛 = 0 → (2↑𝑛) = 1)
63	62	fveq2d 6195	. . . . . . . . 9 ⊢ (𝑛 = 0 → (𝐹‘(2↑𝑛)) = (𝐹‘1))
64	62, 63	oveq12d 6668	. . . . . . . 8 ⊢ (𝑛 = 0 → ((2↑𝑛) · (𝐹‘(2↑𝑛))) = (1 · (𝐹‘1)))
65	58, 64	eqeq12d 2637	. . . . . . 7 ⊢ (𝑛 = 0 → ((𝐺‘𝑛) = ((2↑𝑛) · (𝐹‘(2↑𝑛))) ↔ (𝐺‘0) = (1 · (𝐹‘1))))
66	65	rspcv 3305	. . . . . 6 ⊢ (0 ∈ ℕ₀ → (∀𝑛 ∈ ℕ₀ (𝐺‘𝑛) = ((2↑𝑛) · (𝐹‘(2↑𝑛))) → (𝐺‘0) = (1 · (𝐹‘1))))
67	55, 57, 66	mpsyl 68	. . . . 5 ⊢ (𝜑 → (𝐺‘0) = (1 · (𝐹‘1)))
68	54, 67	seq1i 12815	. . . 4 ⊢ (𝜑 → (seq0( + , 𝐺)‘0) = (1 · (𝐹‘1)))
69	50, 53, 68	3brtr4d 4685	. . 3 ⊢ (𝜑 → (seq1( + , 𝐹)‘1) ≤ (seq0( + , 𝐺)‘0))
70		fzfid 12772	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → ((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1)) ∈ Fin)
71		simpl 473	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → 𝜑)
72	71	adantr 481	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ₀) ∧ 𝑘 ∈ ((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1))) → 𝜑)
73		2nn 11185	. . . . . . . . . . . 12 ⊢ 2 ∈ ℕ
74		peano2nn0 11333	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ ℕ₀ → (𝑗 + 1) ∈ ℕ₀)
75	74	adantl 482	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → (𝑗 + 1) ∈ ℕ₀)
76		nnexpcl 12873	. . . . . . . . . . . 12 ⊢ ((2 ∈ ℕ ∧ (𝑗 + 1) ∈ ℕ₀) → (2↑(𝑗 + 1)) ∈ ℕ)
77	73, 75, 76	sylancr 695	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → (2↑(𝑗 + 1)) ∈ ℕ)
78		elfzuz 12338	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1)) → 𝑘 ∈ (ℤ_≥‘(2↑(𝑗 + 1))))
79		eluznn 11758	. . . . . . . . . . 11 ⊢ (((2↑(𝑗 + 1)) ∈ ℕ ∧ 𝑘 ∈ (ℤ_≥‘(2↑(𝑗 + 1)))) → 𝑘 ∈ ℕ)
80	77, 78, 79	syl2an 494	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ₀) ∧ 𝑘 ∈ ((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1))) → 𝑘 ∈ ℕ)
81	72, 80, 41	syl2anc 693	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ₀) ∧ 𝑘 ∈ ((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1))) → (𝐹‘𝑘) ∈ ℝ)
82	42	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → ∀𝑘 ∈ ℕ (𝐹‘𝑘) ∈ ℝ)
83		fveq2 6191	. . . . . . . . . . . . 13 ⊢ (𝑘 = (2↑(𝑗 + 1)) → (𝐹‘𝑘) = (𝐹‘(2↑(𝑗 + 1))))
84	83	eleq1d 2686	. . . . . . . . . . . 12 ⊢ (𝑘 = (2↑(𝑗 + 1)) → ((𝐹‘𝑘) ∈ ℝ ↔ (𝐹‘(2↑(𝑗 + 1))) ∈ ℝ))
85	84	rspcv 3305	. . . . . . . . . . 11 ⊢ ((2↑(𝑗 + 1)) ∈ ℕ → (∀𝑘 ∈ ℕ (𝐹‘𝑘) ∈ ℝ → (𝐹‘(2↑(𝑗 + 1))) ∈ ℝ))
86	77, 82, 85	sylc 65	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → (𝐹‘(2↑(𝑗 + 1))) ∈ ℝ)
87	86	adantr 481	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ₀) ∧ 𝑘 ∈ ((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1))) → (𝐹‘(2↑(𝑗 + 1))) ∈ ℝ)
88		simpr 477	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ₀) ∧ 𝑛 ∈ (ℤ_≥‘(2↑(𝑗 + 1)))) → 𝑛 ∈ (ℤ_≥‘(2↑(𝑗 + 1))))
89		simplll 798	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ₀) ∧ 𝑛 ∈ (ℤ_≥‘(2↑(𝑗 + 1)))) ∧ 𝑘 ∈ ((2↑(𝑗 + 1))...𝑛)) → 𝜑)
90	77	adantr 481	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ₀) ∧ 𝑛 ∈ (ℤ_≥‘(2↑(𝑗 + 1)))) → (2↑(𝑗 + 1)) ∈ ℕ)
91		elfzuz 12338	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ ((2↑(𝑗 + 1))...𝑛) → 𝑘 ∈ (ℤ_≥‘(2↑(𝑗 + 1))))
92	90, 91, 79	syl2an 494	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ₀) ∧ 𝑛 ∈ (ℤ_≥‘(2↑(𝑗 + 1)))) ∧ 𝑘 ∈ ((2↑(𝑗 + 1))...𝑛)) → 𝑘 ∈ ℕ)
93	89, 92, 41	syl2anc 693	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ₀) ∧ 𝑛 ∈ (ℤ_≥‘(2↑(𝑗 + 1)))) ∧ 𝑘 ∈ ((2↑(𝑗 + 1))...𝑛)) → (𝐹‘𝑘) ∈ ℝ)
94		simplll 798	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ₀) ∧ 𝑛 ∈ (ℤ_≥‘(2↑(𝑗 + 1)))) ∧ 𝑘 ∈ ((2↑(𝑗 + 1))...(𝑛 − 1))) → 𝜑)
95		elfzuz 12338	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ ((2↑(𝑗 + 1))...(𝑛 − 1)) → 𝑘 ∈ (ℤ_≥‘(2↑(𝑗 + 1))))
96	90, 95, 79	syl2an 494	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ₀) ∧ 𝑛 ∈ (ℤ_≥‘(2↑(𝑗 + 1)))) ∧ 𝑘 ∈ ((2↑(𝑗 + 1))...(𝑛 − 1))) → 𝑘 ∈ ℕ)
97		climcnds.3	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘(𝑘 + 1)) ≤ (𝐹‘𝑘))
98	94, 96, 97	syl2anc 693	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ₀) ∧ 𝑛 ∈ (ℤ_≥‘(2↑(𝑗 + 1)))) ∧ 𝑘 ∈ ((2↑(𝑗 + 1))...(𝑛 − 1))) → (𝐹‘(𝑘 + 1)) ≤ (𝐹‘𝑘))
99	88, 93, 98	monoord2 12832	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ₀) ∧ 𝑛 ∈ (ℤ_≥‘(2↑(𝑗 + 1)))) → (𝐹‘𝑛) ≤ (𝐹‘(2↑(𝑗 + 1))))
100	99	ralrimiva 2966	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → ∀𝑛 ∈ (ℤ_≥‘(2↑(𝑗 + 1)))(𝐹‘𝑛) ≤ (𝐹‘(2↑(𝑗 + 1))))
101		fveq2 6191	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝑘 → (𝐹‘𝑛) = (𝐹‘𝑘))
102	101	breq1d 4663	. . . . . . . . . . 11 ⊢ (𝑛 = 𝑘 → ((𝐹‘𝑛) ≤ (𝐹‘(2↑(𝑗 + 1))) ↔ (𝐹‘𝑘) ≤ (𝐹‘(2↑(𝑗 + 1)))))
103	102	rspccva 3308	. . . . . . . . . 10 ⊢ ((∀𝑛 ∈ (ℤ_≥‘(2↑(𝑗 + 1)))(𝐹‘𝑛) ≤ (𝐹‘(2↑(𝑗 + 1))) ∧ 𝑘 ∈ (ℤ_≥‘(2↑(𝑗 + 1)))) → (𝐹‘𝑘) ≤ (𝐹‘(2↑(𝑗 + 1))))
104	100, 78, 103	syl2an 494	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ₀) ∧ 𝑘 ∈ ((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1))) → (𝐹‘𝑘) ≤ (𝐹‘(2↑(𝑗 + 1))))
105	70, 81, 87, 104	fsumle 14531	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → Σ𝑘 ∈ ((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1))(𝐹‘𝑘) ≤ Σ𝑘 ∈ ((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1))(𝐹‘(2↑(𝑗 + 1))))
106		fzfid 12772	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → (1...((2↑(𝑗 + 1)) − 1)) ∈ Fin)
107		hashcl 13147	. . . . . . . . . . . . 13 ⊢ ((1...((2↑(𝑗 + 1)) − 1)) ∈ Fin → (#‘(1...((2↑(𝑗 + 1)) − 1))) ∈ ℕ₀)
108	106, 107	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → (#‘(1...((2↑(𝑗 + 1)) − 1))) ∈ ℕ₀)
109	108	nn0cnd 11353	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → (#‘(1...((2↑(𝑗 + 1)) − 1))) ∈ ℂ)
110	77	nnred 11035	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → (2↑(𝑗 + 1)) ∈ ℝ)
111	110	recnd 10068	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → (2↑(𝑗 + 1)) ∈ ℂ)
112		hashcl 13147	. . . . . . . . . . . . 13 ⊢ (((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1)) ∈ Fin → (#‘((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1))) ∈ ℕ₀)
113	70, 112	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → (#‘((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1))) ∈ ℕ₀)
114	113	nn0cnd 11353	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → (#‘((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1))) ∈ ℂ)
115		2z 11409	. . . . . . . . . . . . . . . . . . . 20 ⊢ 2 ∈ ℤ
116		zexpcl 12875	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((2 ∈ ℤ ∧ (𝑗 + 1) ∈ ℕ₀) → (2↑(𝑗 + 1)) ∈ ℤ)
117	115, 75, 116	sylancr 695	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → (2↑(𝑗 + 1)) ∈ ℤ)
118		nn0p1nn 11332	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑗 ∈ ℕ₀ → (𝑗 + 1) ∈ ℕ)
119	118	adantl 482	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → (𝑗 + 1) ∈ ℕ)
120		nnuz 11723	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ℕ = (ℤ_≥‘1)
121	119, 120	syl6eleq 2711	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → (𝑗 + 1) ∈ (ℤ_≥‘1))
122		2re 11090	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 2 ∈ ℝ
123		1le2 11241	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 1 ≤ 2
124		leexp2a 12916	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((2 ∈ ℝ ∧ 1 ≤ 2 ∧ (𝑗 + 1) ∈ (ℤ_≥‘1)) → (2↑1) ≤ (2↑(𝑗 + 1)))
125	122, 123, 124	mp3an12 1414	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑗 + 1) ∈ (ℤ_≥‘1) → (2↑1) ≤ (2↑(𝑗 + 1)))
126	121, 125	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → (2↑1) ≤ (2↑(𝑗 + 1)))
127	7, 126	syl5eqbrr 4689	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → 2 ≤ (2↑(𝑗 + 1)))
128	115	eluz1i 11695	. . . . . . . . . . . . . . . . . . 19 ⊢ ((2↑(𝑗 + 1)) ∈ (ℤ_≥‘2) ↔ ((2↑(𝑗 + 1)) ∈ ℤ ∧ 2 ≤ (2↑(𝑗 + 1))))
129	117, 127, 128	sylanbrc 698	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → (2↑(𝑗 + 1)) ∈ (ℤ_≥‘2))
130		uz2m1nn 11763	. . . . . . . . . . . . . . . . . 18 ⊢ ((2↑(𝑗 + 1)) ∈ (ℤ_≥‘2) → ((2↑(𝑗 + 1)) − 1) ∈ ℕ)
131	129, 130	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → ((2↑(𝑗 + 1)) − 1) ∈ ℕ)
132	131, 120	syl6eleq 2711	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → ((2↑(𝑗 + 1)) − 1) ∈ (ℤ_≥‘1))
133		peano2zm 11420	. . . . . . . . . . . . . . . . . 18 ⊢ ((2↑(𝑗 + 1)) ∈ ℤ → ((2↑(𝑗 + 1)) − 1) ∈ ℤ)
134	117, 133	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → ((2↑(𝑗 + 1)) − 1) ∈ ℤ)
135		peano2nn0 11333	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑗 + 1) ∈ ℕ₀ → ((𝑗 + 1) + 1) ∈ ℕ₀)
136	75, 135	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → ((𝑗 + 1) + 1) ∈ ℕ₀)
137		zexpcl 12875	. . . . . . . . . . . . . . . . . . 19 ⊢ ((2 ∈ ℤ ∧ ((𝑗 + 1) + 1) ∈ ℕ₀) → (2↑((𝑗 + 1) + 1)) ∈ ℤ)
138	115, 136, 137	sylancr 695	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → (2↑((𝑗 + 1) + 1)) ∈ ℤ)
139		peano2zm 11420	. . . . . . . . . . . . . . . . . 18 ⊢ ((2↑((𝑗 + 1) + 1)) ∈ ℤ → ((2↑((𝑗 + 1) + 1)) − 1) ∈ ℤ)
140	138, 139	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → ((2↑((𝑗 + 1) + 1)) − 1) ∈ ℤ)
141	117	zred 11482	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → (2↑(𝑗 + 1)) ∈ ℝ)
142	138	zred 11482	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → (2↑((𝑗 + 1) + 1)) ∈ ℝ)
143		1red 10055	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → 1 ∈ ℝ)
144	75	nn0zd 11480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → (𝑗 + 1) ∈ ℤ)
145		uzid 11702	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑗 + 1) ∈ ℤ → (𝑗 + 1) ∈ (ℤ_≥‘(𝑗 + 1)))
146		peano2uz 11741	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑗 + 1) ∈ (ℤ_≥‘(𝑗 + 1)) → ((𝑗 + 1) + 1) ∈ (ℤ_≥‘(𝑗 + 1)))
147		leexp2a 12916	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((2 ∈ ℝ ∧ 1 ≤ 2 ∧ ((𝑗 + 1) + 1) ∈ (ℤ_≥‘(𝑗 + 1))) → (2↑(𝑗 + 1)) ≤ (2↑((𝑗 + 1) + 1)))
148	122, 123, 147	mp3an12 1414	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑗 + 1) + 1) ∈ (ℤ_≥‘(𝑗 + 1)) → (2↑(𝑗 + 1)) ≤ (2↑((𝑗 + 1) + 1)))
149	144, 145, 146, 148	4syl 19	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → (2↑(𝑗 + 1)) ≤ (2↑((𝑗 + 1) + 1)))
150	141, 142, 143, 149	lesub1dd 10643	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → ((2↑(𝑗 + 1)) − 1) ≤ ((2↑((𝑗 + 1) + 1)) − 1))
151		eluz2 11693	. . . . . . . . . . . . . . . . 17 ⊢ (((2↑((𝑗 + 1) + 1)) − 1) ∈ (ℤ_≥‘((2↑(𝑗 + 1)) − 1)) ↔ (((2↑(𝑗 + 1)) − 1) ∈ ℤ ∧ ((2↑((𝑗 + 1) + 1)) − 1) ∈ ℤ ∧ ((2↑(𝑗 + 1)) − 1) ≤ ((2↑((𝑗 + 1) + 1)) − 1)))
152	134, 140, 150, 151	syl3anbrc 1246	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → ((2↑((𝑗 + 1) + 1)) − 1) ∈ (ℤ_≥‘((2↑(𝑗 + 1)) − 1)))
153		elfzuzb 12336	. . . . . . . . . . . . . . . 16 ⊢ (((2↑(𝑗 + 1)) − 1) ∈ (1...((2↑((𝑗 + 1) + 1)) − 1)) ↔ (((2↑(𝑗 + 1)) − 1) ∈ (ℤ_≥‘1) ∧ ((2↑((𝑗 + 1) + 1)) − 1) ∈ (ℤ_≥‘((2↑(𝑗 + 1)) − 1))))
154	132, 152, 153	sylanbrc 698	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → ((2↑(𝑗 + 1)) − 1) ∈ (1...((2↑((𝑗 + 1) + 1)) − 1)))
155		fzsplit 12367	. . . . . . . . . . . . . . 15 ⊢ (((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))))
156	154, 155	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → (1...((2↑((𝑗 + 1) + 1)) − 1)) = ((1...((2↑(𝑗 + 1)) − 1)) ∪ ((((2↑(𝑗 + 1)) − 1) + 1)...((2↑((𝑗 + 1) + 1)) − 1))))
157		npcan 10290	. . . . . . . . . . . . . . . . 17 ⊢ (((2↑(𝑗 + 1)) ∈ ℂ ∧ 1 ∈ ℂ) → (((2↑(𝑗 + 1)) − 1) + 1) = (2↑(𝑗 + 1)))
158	111, 12, 157	sylancl 694	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → (((2↑(𝑗 + 1)) − 1) + 1) = (2↑(𝑗 + 1)))
159	158	oveq1d 6665	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → ((((2↑(𝑗 + 1)) − 1) + 1)...((2↑((𝑗 + 1) + 1)) − 1)) = ((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1)))
160	159	uneq2d 3767	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → ((1...((2↑(𝑗 + 1)) − 1)) ∪ ((((2↑(𝑗 + 1)) − 1) + 1)...((2↑((𝑗 + 1) + 1)) − 1))) = ((1...((2↑(𝑗 + 1)) − 1)) ∪ ((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1))))
161	156, 160	eqtrd 2656	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → (1...((2↑((𝑗 + 1) + 1)) − 1)) = ((1...((2↑(𝑗 + 1)) − 1)) ∪ ((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1))))
162	161	fveq2d 6195	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → (#‘(1...((2↑((𝑗 + 1) + 1)) − 1))) = (#‘((1...((2↑(𝑗 + 1)) − 1)) ∪ ((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1)))))
163		expp1 12867	. . . . . . . . . . . . . . . . 17 ⊢ ((2 ∈ ℂ ∧ (𝑗 + 1) ∈ ℕ₀) → (2↑((𝑗 + 1) + 1)) = ((2↑(𝑗 + 1)) · 2))
164	5, 75, 163	sylancr 695	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → (2↑((𝑗 + 1) + 1)) = ((2↑(𝑗 + 1)) · 2))
165	111	times2d 11276	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → ((2↑(𝑗 + 1)) · 2) = ((2↑(𝑗 + 1)) + (2↑(𝑗 + 1))))
166	164, 165	eqtrd 2656	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → (2↑((𝑗 + 1) + 1)) = ((2↑(𝑗 + 1)) + (2↑(𝑗 + 1))))
167	166	oveq1d 6665	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → ((2↑((𝑗 + 1) + 1)) − 1) = (((2↑(𝑗 + 1)) + (2↑(𝑗 + 1))) − 1))
168		1cnd 10056	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → 1 ∈ ℂ)
169	111, 111, 168	addsubd 10413	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → (((2↑(𝑗 + 1)) + (2↑(𝑗 + 1))) − 1) = (((2↑(𝑗 + 1)) − 1) + (2↑(𝑗 + 1))))
170	167, 169	eqtrd 2656	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → ((2↑((𝑗 + 1) + 1)) − 1) = (((2↑(𝑗 + 1)) − 1) + (2↑(𝑗 + 1))))
171		uztrn 11704	. . . . . . . . . . . . . . . . 17 ⊢ ((((2↑((𝑗 + 1) + 1)) − 1) ∈ (ℤ_≥‘((2↑(𝑗 + 1)) − 1)) ∧ ((2↑(𝑗 + 1)) − 1) ∈ (ℤ_≥‘1)) → ((2↑((𝑗 + 1) + 1)) − 1) ∈ (ℤ_≥‘1))
172	152, 132, 171	syl2anc 693	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → ((2↑((𝑗 + 1) + 1)) − 1) ∈ (ℤ_≥‘1))
173	172, 120	syl6eleqr 2712	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → ((2↑((𝑗 + 1) + 1)) − 1) ∈ ℕ)
174	173	nnnn0d 11351	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → ((2↑((𝑗 + 1) + 1)) − 1) ∈ ℕ₀)
175		hashfz1 13134	. . . . . . . . . . . . . 14 ⊢ (((2↑((𝑗 + 1) + 1)) − 1) ∈ ℕ₀ → (#‘(1...((2↑((𝑗 + 1) + 1)) − 1))) = ((2↑((𝑗 + 1) + 1)) − 1))
176	174, 175	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → (#‘(1...((2↑((𝑗 + 1) + 1)) − 1))) = ((2↑((𝑗 + 1) + 1)) − 1))
177	131	nnnn0d 11351	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → ((2↑(𝑗 + 1)) − 1) ∈ ℕ₀)
178		hashfz1 13134	. . . . . . . . . . . . . . 15 ⊢ (((2↑(𝑗 + 1)) − 1) ∈ ℕ₀ → (#‘(1...((2↑(𝑗 + 1)) − 1))) = ((2↑(𝑗 + 1)) − 1))
179	177, 178	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → (#‘(1...((2↑(𝑗 + 1)) − 1))) = ((2↑(𝑗 + 1)) − 1))
180	179	oveq1d 6665	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → ((#‘(1...((2↑(𝑗 + 1)) − 1))) + (2↑(𝑗 + 1))) = (((2↑(𝑗 + 1)) − 1) + (2↑(𝑗 + 1))))
181	170, 176, 180	3eqtr4d 2666	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → (#‘(1...((2↑((𝑗 + 1) + 1)) − 1))) = ((#‘(1...((2↑(𝑗 + 1)) − 1))) + (2↑(𝑗 + 1))))
182	110	ltm1d 10956	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → ((2↑(𝑗 + 1)) − 1) < (2↑(𝑗 + 1)))
183		fzdisj 12368	. . . . . . . . . . . . . 14 ⊢ (((2↑(𝑗 + 1)) − 1) < (2↑(𝑗 + 1)) → ((1...((2↑(𝑗 + 1)) − 1)) ∩ ((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1))) = ∅)
184	182, 183	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → ((1...((2↑(𝑗 + 1)) − 1)) ∩ ((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1))) = ∅)
185		hashun 13171	. . . . . . . . . . . . 13 ⊢ (((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)))))
186	106, 70, 184, 185	syl3anc 1326	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → (#‘((1...((2↑(𝑗 + 1)) − 1)) ∪ ((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1)))) = ((#‘(1...((2↑(𝑗 + 1)) − 1))) + (#‘((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1)))))
187	162, 181, 186	3eqtr3d 2664	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → ((#‘(1...((2↑(𝑗 + 1)) − 1))) + (2↑(𝑗 + 1))) = ((#‘(1...((2↑(𝑗 + 1)) − 1))) + (#‘((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1)))))
188	109, 111, 114, 187	addcanad 10241	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → (2↑(𝑗 + 1)) = (#‘((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1))))
189	188	oveq1d 6665	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → ((2↑(𝑗 + 1)) · (𝐹‘(2↑(𝑗 + 1)))) = ((#‘((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1))) · (𝐹‘(2↑(𝑗 + 1)))))
190	57	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → ∀𝑛 ∈ ℕ₀ (𝐺‘𝑛) = ((2↑𝑛) · (𝐹‘(2↑𝑛))))
191		fveq2 6191	. . . . . . . . . . . 12 ⊢ (𝑛 = (𝑗 + 1) → (𝐺‘𝑛) = (𝐺‘(𝑗 + 1)))
192		oveq2 6658	. . . . . . . . . . . . 13 ⊢ (𝑛 = (𝑗 + 1) → (2↑𝑛) = (2↑(𝑗 + 1)))
193	192	fveq2d 6195	. . . . . . . . . . . . 13 ⊢ (𝑛 = (𝑗 + 1) → (𝐹‘(2↑𝑛)) = (𝐹‘(2↑(𝑗 + 1))))
194	192, 193	oveq12d 6668	. . . . . . . . . . . 12 ⊢ (𝑛 = (𝑗 + 1) → ((2↑𝑛) · (𝐹‘(2↑𝑛))) = ((2↑(𝑗 + 1)) · (𝐹‘(2↑(𝑗 + 1)))))
195	191, 194	eqeq12d 2637	. . . . . . . . . . 11 ⊢ (𝑛 = (𝑗 + 1) → ((𝐺‘𝑛) = ((2↑𝑛) · (𝐹‘(2↑𝑛))) ↔ (𝐺‘(𝑗 + 1)) = ((2↑(𝑗 + 1)) · (𝐹‘(2↑(𝑗 + 1))))))
196	195	rspcv 3305	. . . . . . . . . 10 ⊢ ((𝑗 + 1) ∈ ℕ₀ → (∀𝑛 ∈ ℕ₀ (𝐺‘𝑛) = ((2↑𝑛) · (𝐹‘(2↑𝑛))) → (𝐺‘(𝑗 + 1)) = ((2↑(𝑗 + 1)) · (𝐹‘(2↑(𝑗 + 1))))))
197	75, 190, 196	sylc 65	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → (𝐺‘(𝑗 + 1)) = ((2↑(𝑗 + 1)) · (𝐹‘(2↑(𝑗 + 1)))))
198	86	recnd 10068	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → (𝐹‘(2↑(𝑗 + 1))) ∈ ℂ)
199		fsumconst 14522	. . . . . . . . . 10 ⊢ ((((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)))))
200	70, 198, 199	syl2anc 693	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → Σ𝑘 ∈ ((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1))(𝐹‘(2↑(𝑗 + 1))) = ((#‘((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1))) · (𝐹‘(2↑(𝑗 + 1)))))
201	189, 197, 200	3eqtr4d 2666	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → (𝐺‘(𝑗 + 1)) = Σ𝑘 ∈ ((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1))(𝐹‘(2↑(𝑗 + 1))))
202	105, 201	breqtrrd 4681	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → Σ𝑘 ∈ ((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1))(𝐹‘𝑘) ≤ (𝐺‘(𝑗 + 1)))
203		elfznn 12370	. . . . . . . . . 10 ⊢ (𝑘 ∈ (1...((2↑(𝑗 + 1)) − 1)) → 𝑘 ∈ ℕ)
204	71, 203, 41	syl2an 494	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ₀) ∧ 𝑘 ∈ (1...((2↑(𝑗 + 1)) − 1))) → (𝐹‘𝑘) ∈ ℝ)
205	106, 204	fsumrecl 14465	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → Σ𝑘 ∈ (1...((2↑(𝑗 + 1)) − 1))(𝐹‘𝑘) ∈ ℝ)
206	70, 81	fsumrecl 14465	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → Σ𝑘 ∈ ((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1))(𝐹‘𝑘) ∈ ℝ)
207		nn0uz 11722	. . . . . . . . . 10 ⊢ ℕ₀ = (ℤ_≥‘0)
208		0zd 11389	. . . . . . . . . 10 ⊢ (𝜑 → 0 ∈ ℤ)
209		simpr 477	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → 𝑛 ∈ ℕ₀)
210		nnexpcl 12873	. . . . . . . . . . . . . 14 ⊢ ((2 ∈ ℕ ∧ 𝑛 ∈ ℕ₀) → (2↑𝑛) ∈ ℕ)
211	73, 209, 210	sylancr 695	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → (2↑𝑛) ∈ ℕ)
212	211	nnred 11035	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → (2↑𝑛) ∈ ℝ)
213	42	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → ∀𝑘 ∈ ℕ (𝐹‘𝑘) ∈ ℝ)
214		fveq2 6191	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = (2↑𝑛) → (𝐹‘𝑘) = (𝐹‘(2↑𝑛)))
215	214	eleq1d 2686	. . . . . . . . . . . . . 14 ⊢ (𝑘 = (2↑𝑛) → ((𝐹‘𝑘) ∈ ℝ ↔ (𝐹‘(2↑𝑛)) ∈ ℝ))
216	215	rspcv 3305	. . . . . . . . . . . . 13 ⊢ ((2↑𝑛) ∈ ℕ → (∀𝑘 ∈ ℕ (𝐹‘𝑘) ∈ ℝ → (𝐹‘(2↑𝑛)) ∈ ℝ))
217	211, 213, 216	sylc 65	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → (𝐹‘(2↑𝑛)) ∈ ℝ)
218	212, 217	remulcld 10070	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → ((2↑𝑛) · (𝐹‘(2↑𝑛))) ∈ ℝ)
219	56, 218	eqeltrd 2701	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → (𝐺‘𝑛) ∈ ℝ)
220	207, 208, 219	serfre 12830	. . . . . . . . 9 ⊢ (𝜑 → seq0( + , 𝐺):ℕ₀⟶ℝ)
221	220	ffvelrnda 6359	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → (seq0( + , 𝐺)‘𝑗) ∈ ℝ)
222	141, 86	remulcld 10070	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → ((2↑(𝑗 + 1)) · (𝐹‘(2↑(𝑗 + 1)))) ∈ ℝ)
223	197, 222	eqeltrd 2701	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → (𝐺‘(𝑗 + 1)) ∈ ℝ)
224		le2add 10510	. . . . . . . 8 ⊢ (((Σ𝑘 ∈ (1...((2↑(𝑗 + 1)) − 1))(𝐹‘𝑘) ∈ ℝ ∧ Σ𝑘 ∈ ((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1))(𝐹‘𝑘) ∈ ℝ) ∧ ((seq0( + , 𝐺)‘𝑗) ∈ ℝ ∧ (𝐺‘(𝑗 + 1)) ∈ ℝ)) → ((Σ𝑘 ∈ (1...((2↑(𝑗 + 1)) − 1))(𝐹‘𝑘) ≤ (seq0( + , 𝐺)‘𝑗) ∧ Σ𝑘 ∈ ((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1))(𝐹‘𝑘) ≤ (𝐺‘(𝑗 + 1))) → (Σ𝑘 ∈ (1...((2↑(𝑗 + 1)) − 1))(𝐹‘𝑘) + Σ𝑘 ∈ ((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1))(𝐹‘𝑘)) ≤ ((seq0( + , 𝐺)‘𝑗) + (𝐺‘(𝑗 + 1)))))
225	205, 206, 221, 223, 224	syl22anc 1327	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → ((Σ𝑘 ∈ (1...((2↑(𝑗 + 1)) − 1))(𝐹‘𝑘) ≤ (seq0( + , 𝐺)‘𝑗) ∧ Σ𝑘 ∈ ((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1))(𝐹‘𝑘) ≤ (𝐺‘(𝑗 + 1))) → (Σ𝑘 ∈ (1...((2↑(𝑗 + 1)) − 1))(𝐹‘𝑘) + Σ𝑘 ∈ ((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1))(𝐹‘𝑘)) ≤ ((seq0( + , 𝐺)‘𝑗) + (𝐺‘(𝑗 + 1)))))
226	202, 225	mpan2d 710	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → (Σ𝑘 ∈ (1...((2↑(𝑗 + 1)) − 1))(𝐹‘𝑘) ≤ (seq0( + , 𝐺)‘𝑗) → (Σ𝑘 ∈ (1...((2↑(𝑗 + 1)) − 1))(𝐹‘𝑘) + Σ𝑘 ∈ ((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1))(𝐹‘𝑘)) ≤ ((seq0( + , 𝐺)‘𝑗) + (𝐺‘(𝑗 + 1)))))
227		eqidd 2623	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ₀) ∧ 𝑘 ∈ (1...((2↑(𝑗 + 1)) − 1))) → (𝐹‘𝑘) = (𝐹‘𝑘))
228	41	recnd 10068	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) ∈ ℂ)
229	71, 203, 228	syl2an 494	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ₀) ∧ 𝑘 ∈ (1...((2↑(𝑗 + 1)) − 1))) → (𝐹‘𝑘) ∈ ℂ)
230	227, 132, 229	fsumser 14461	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → Σ𝑘 ∈ (1...((2↑(𝑗 + 1)) − 1))(𝐹‘𝑘) = (seq1( + , 𝐹)‘((2↑(𝑗 + 1)) − 1)))
231	230	eqcomd 2628	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → (seq1( + , 𝐹)‘((2↑(𝑗 + 1)) − 1)) = Σ𝑘 ∈ (1...((2↑(𝑗 + 1)) − 1))(𝐹‘𝑘))
232	231	breq1d 4663	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → ((seq1( + , 𝐹)‘((2↑(𝑗 + 1)) − 1)) ≤ (seq0( + , 𝐺)‘𝑗) ↔ Σ𝑘 ∈ (1...((2↑(𝑗 + 1)) − 1))(𝐹‘𝑘) ≤ (seq0( + , 𝐺)‘𝑗)))
233		eqidd 2623	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ₀) ∧ 𝑘 ∈ (1...((2↑((𝑗 + 1) + 1)) − 1))) → (𝐹‘𝑘) = (𝐹‘𝑘))
234		elfznn 12370	. . . . . . . . . 10 ⊢ (𝑘 ∈ (1...((2↑((𝑗 + 1) + 1)) − 1)) → 𝑘 ∈ ℕ)
235	71, 234, 228	syl2an 494	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ₀) ∧ 𝑘 ∈ (1...((2↑((𝑗 + 1) + 1)) − 1))) → (𝐹‘𝑘) ∈ ℂ)
236	233, 172, 235	fsumser 14461	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → Σ𝑘 ∈ (1...((2↑((𝑗 + 1) + 1)) − 1))(𝐹‘𝑘) = (seq1( + , 𝐹)‘((2↑((𝑗 + 1) + 1)) − 1)))
237		fzfid 12772	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → (1...((2↑((𝑗 + 1) + 1)) − 1)) ∈ Fin)
238	184, 161, 237, 235	fsumsplit 14471	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → Σ𝑘 ∈ (1...((2↑((𝑗 + 1) + 1)) − 1))(𝐹‘𝑘) = (Σ𝑘 ∈ (1...((2↑(𝑗 + 1)) − 1))(𝐹‘𝑘) + Σ𝑘 ∈ ((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1))(𝐹‘𝑘)))
239	236, 238	eqtr3d 2658	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → (seq1( + , 𝐹)‘((2↑((𝑗 + 1) + 1)) − 1)) = (Σ𝑘 ∈ (1...((2↑(𝑗 + 1)) − 1))(𝐹‘𝑘) + Σ𝑘 ∈ ((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1))(𝐹‘𝑘)))
240		simpr 477	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → 𝑗 ∈ ℕ₀)
241	240, 207	syl6eleq 2711	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → 𝑗 ∈ (ℤ_≥‘0))
242		seqp1 12816	. . . . . . . 8 ⊢ (𝑗 ∈ (ℤ_≥‘0) → (seq0( + , 𝐺)‘(𝑗 + 1)) = ((seq0( + , 𝐺)‘𝑗) + (𝐺‘(𝑗 + 1))))
243	241, 242	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → (seq0( + , 𝐺)‘(𝑗 + 1)) = ((seq0( + , 𝐺)‘𝑗) + (𝐺‘(𝑗 + 1))))
244	239, 243	breq12d 4666	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → ((seq1( + , 𝐹)‘((2↑((𝑗 + 1) + 1)) − 1)) ≤ (seq0( + , 𝐺)‘(𝑗 + 1)) ↔ (Σ𝑘 ∈ (1...((2↑(𝑗 + 1)) − 1))(𝐹‘𝑘) + Σ𝑘 ∈ ((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1))(𝐹‘𝑘)) ≤ ((seq0( + , 𝐺)‘𝑗) + (𝐺‘(𝑗 + 1)))))
245	226, 232, 244	3imtr4d 283	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → ((seq1( + , 𝐹)‘((2↑(𝑗 + 1)) − 1)) ≤ (seq0( + , 𝐺)‘𝑗) → (seq1( + , 𝐹)‘((2↑((𝑗 + 1) + 1)) − 1)) ≤ (seq0( + , 𝐺)‘(𝑗 + 1))))
246	245	expcom 451	. . . 4 ⊢ (𝑗 ∈ ℕ₀ → (𝜑 → ((seq1( + , 𝐹)‘((2↑(𝑗 + 1)) − 1)) ≤ (seq0( + , 𝐺)‘𝑗) → (seq1( + , 𝐹)‘((2↑((𝑗 + 1) + 1)) − 1)) ≤ (seq0( + , 𝐺)‘(𝑗 + 1)))))
247	246	a2d 29	. . 3 ⊢ (𝑗 ∈ ℕ₀ → ((𝜑 → (seq1( + , 𝐹)‘((2↑(𝑗 + 1)) − 1)) ≤ (seq0( + , 𝐺)‘𝑗)) → (𝜑 → (seq1( + , 𝐹)‘((2↑((𝑗 + 1) + 1)) − 1)) ≤ (seq0( + , 𝐺)‘(𝑗 + 1)))))
248	18, 25, 32, 39, 69, 247	nn0ind 11472	. 2 ⊢ (𝑁 ∈ ℕ₀ → (𝜑 → (seq1( + , 𝐹)‘((2↑(𝑁 + 1)) − 1)) ≤ (seq0( + , 𝐺)‘𝑁)))
249	248	impcom 446	1 ⊢ ((𝜑 ∧ 𝑁 ∈ ℕ₀) → (seq1( + , 𝐹)‘((2↑(𝑁 + 1)) − 1)) ≤ (seq0( + , 𝐺)‘𝑁))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 384 = wceq 1483 ∈ wcel 1990 ∀wral 2912 ∪ cun 3572 ∩ cin 3573 ∅c0 3915 class class class wbr 4653 ‘cfv 5888 (class class class)co 6650 Fincfn 7955 ℂcc 9934 ℝcr 9935 0cc0 9936 1c1 9937 + caddc 9939 · cmul 9941 < clt 10074 ≤ cle 10075 − cmin 10266 ℕcn 11020 2c2 11070 ℕ₀cn0 11292 ℤcz 11377 ℤ_≥cuz 11687 ...cfz 12326 seqcseq 12801 ↑cexp 12860 #chash 13117 Σcsu 14416

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-rep 4771 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949 ax-inf2 8538 ax-cnex 9992 ax-resscn 9993 ax-1cn 9994 ax-icn 9995 ax-addcl 9996 ax-addrcl 9997 ax-mulcl 9998 ax-mulrcl 9999 ax-mulcom 10000 ax-addass 10001 ax-mulass 10002 ax-distr 10003 ax-i2m1 10004 ax-1ne0 10005 ax-1rid 10006 ax-rnegex 10007 ax-rrecex 10008 ax-cnre 10009 ax-pre-lttri 10010 ax-pre-lttrn 10011 ax-pre-ltadd 10012 ax-pre-mulgt0 10013 ax-pre-sup 10014

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-fal 1489 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-nel 2898 df-ral 2917 df-rex 2918 df-reu 2919 df-rmo 2920 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-pss 3590 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-tp 4182 df-op 4184 df-uni 4437 df-int 4476 df-iun 4522 df-br 4654 df-opab 4713 df-mpt 4730 df-tr 4753 df-id 5024 df-eprel 5029 df-po 5035 df-so 5036 df-fr 5073 df-se 5074 df-we 5075 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-pred 5680 df-ord 5726 df-on 5727 df-lim 5728 df-suc 5729 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-isom 5897 df-riota 6611 df-ov 6653 df-oprab 6654 df-mpt2 6655 df-om 7066 df-1st 7168 df-2nd 7169 df-wrecs 7407 df-recs 7468 df-rdg 7506 df-1o 7560 df-oadd 7564 df-er 7742 df-en 7956 df-dom 7957 df-sdom 7958 df-fin 7959 df-sup 8348 df-oi 8415 df-card 8765 df-cda 8990 df-pnf 10076 df-mnf 10077 df-xr 10078 df-ltxr 10079 df-le 10080 df-sub 10268 df-neg 10269 df-div 10685 df-nn 11021 df-2 11079 df-3 11080 df-n0 11293 df-z 11378 df-uz 11688 df-rp 11833 df-ico 12181 df-fz 12327 df-fzo 12466 df-seq 12802 df-exp 12861 df-hash 13118 df-cj 13839 df-re 13840 df-im 13841 df-sqrt 13975 df-abs 13976 df-clim 14219 df-sum 14417

This theorem is referenced by: climcnds 14583

W3C validator