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 14962

Description: Lemma for climcnds 14964: 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 6917	. . . . . . . . . . 11 ⊢ (𝑥 = 0 → (𝑥 + 1) = (0 + 1))
2		0p1e1 11487	. . . . . . . . . . 11 ⊢ (0 + 1) = 1
3	1, 2	syl6eq 2877	. . . . . . . . . 10 ⊢ (𝑥 = 0 → (𝑥 + 1) = 1)
4	3	oveq2d 6926	. . . . . . . . 9 ⊢ (𝑥 = 0 → (2↑(𝑥 + 1)) = (2↑1))
5		2cn 11433	. . . . . . . . . . 11 ⊢ 2 ∈ ℂ
6		exp1 13167	. . . . . . . . . . 11 ⊢ (2 ∈ ℂ → (2↑1) = 2)
7	5, 6	ax-mp 5	. . . . . . . . . 10 ⊢ (2↑1) = 2
8		df-2 11421	. . . . . . . . . 10 ⊢ 2 = (1 + 1)
9	7, 8	eqtri 2849	. . . . . . . . 9 ⊢ (2↑1) = (1 + 1)
10	4, 9	syl6eq 2877	. . . . . . . 8 ⊢ (𝑥 = 0 → (2↑(𝑥 + 1)) = (1 + 1))
11	10	oveq1d 6925	. . . . . . 7 ⊢ (𝑥 = 0 → ((2↑(𝑥 + 1)) − 1) = ((1 + 1) − 1))
12		ax-1cn 10317	. . . . . . . 8 ⊢ 1 ∈ ℂ
13	12, 12	pncan3oi 10625	. . . . . . 7 ⊢ ((1 + 1) − 1) = 1
14	11, 13	syl6eq 2877	. . . . . 6 ⊢ (𝑥 = 0 → ((2↑(𝑥 + 1)) − 1) = 1)
15	14	fveq2d 6441	. . . . 5 ⊢ (𝑥 = 0 → (seq1( + , 𝐹)‘((2↑(𝑥 + 1)) − 1)) = (seq1( + , 𝐹)‘1))
16		fveq2 6437	. . . . 5 ⊢ (𝑥 = 0 → (seq0( + , 𝐺)‘𝑥) = (seq0( + , 𝐺)‘0))
17	15, 16	breq12d 4888	. . . 4 ⊢ (𝑥 = 0 → ((seq1( + , 𝐹)‘((2↑(𝑥 + 1)) − 1)) ≤ (seq0( + , 𝐺)‘𝑥) ↔ (seq1( + , 𝐹)‘1) ≤ (seq0( + , 𝐺)‘0)))
18	17	imbi2d 332	. . 3 ⊢ (𝑥 = 0 → ((𝜑 → (seq1( + , 𝐹)‘((2↑(𝑥 + 1)) − 1)) ≤ (seq0( + , 𝐺)‘𝑥)) ↔ (𝜑 → (seq1( + , 𝐹)‘1) ≤ (seq0( + , 𝐺)‘0))))
19		oveq1 6917	. . . . . . 7 ⊢ (𝑥 = 𝑗 → (𝑥 + 1) = (𝑗 + 1))
20	19	oveq2d 6926	. . . . . 6 ⊢ (𝑥 = 𝑗 → (2↑(𝑥 + 1)) = (2↑(𝑗 + 1)))
21	20	fvoveq1d 6932	. . . . 5 ⊢ (𝑥 = 𝑗 → (seq1( + , 𝐹)‘((2↑(𝑥 + 1)) − 1)) = (seq1( + , 𝐹)‘((2↑(𝑗 + 1)) − 1)))
22		fveq2 6437	. . . . 5 ⊢ (𝑥 = 𝑗 → (seq0( + , 𝐺)‘𝑥) = (seq0( + , 𝐺)‘𝑗))
23	21, 22	breq12d 4888	. . . 4 ⊢ (𝑥 = 𝑗 → ((seq1( + , 𝐹)‘((2↑(𝑥 + 1)) − 1)) ≤ (seq0( + , 𝐺)‘𝑥) ↔ (seq1( + , 𝐹)‘((2↑(𝑗 + 1)) − 1)) ≤ (seq0( + , 𝐺)‘𝑗)))
24	23	imbi2d 332	. . 3 ⊢ (𝑥 = 𝑗 → ((𝜑 → (seq1( + , 𝐹)‘((2↑(𝑥 + 1)) − 1)) ≤ (seq0( + , 𝐺)‘𝑥)) ↔ (𝜑 → (seq1( + , 𝐹)‘((2↑(𝑗 + 1)) − 1)) ≤ (seq0( + , 𝐺)‘𝑗))))
25		oveq1 6917	. . . . . . 7 ⊢ (𝑥 = (𝑗 + 1) → (𝑥 + 1) = ((𝑗 + 1) + 1))
26	25	oveq2d 6926	. . . . . 6 ⊢ (𝑥 = (𝑗 + 1) → (2↑(𝑥 + 1)) = (2↑((𝑗 + 1) + 1)))
27	26	fvoveq1d 6932	. . . . 5 ⊢ (𝑥 = (𝑗 + 1) → (seq1( + , 𝐹)‘((2↑(𝑥 + 1)) − 1)) = (seq1( + , 𝐹)‘((2↑((𝑗 + 1) + 1)) − 1)))
28		fveq2 6437	. . . . 5 ⊢ (𝑥 = (𝑗 + 1) → (seq0( + , 𝐺)‘𝑥) = (seq0( + , 𝐺)‘(𝑗 + 1)))
29	27, 28	breq12d 4888	. . . 4 ⊢ (𝑥 = (𝑗 + 1) → ((seq1( + , 𝐹)‘((2↑(𝑥 + 1)) − 1)) ≤ (seq0( + , 𝐺)‘𝑥) ↔ (seq1( + , 𝐹)‘((2↑((𝑗 + 1) + 1)) − 1)) ≤ (seq0( + , 𝐺)‘(𝑗 + 1))))
30	29	imbi2d 332	. . 3 ⊢ (𝑥 = (𝑗 + 1) → ((𝜑 → (seq1( + , 𝐹)‘((2↑(𝑥 + 1)) − 1)) ≤ (seq0( + , 𝐺)‘𝑥)) ↔ (𝜑 → (seq1( + , 𝐹)‘((2↑((𝑗 + 1) + 1)) − 1)) ≤ (seq0( + , 𝐺)‘(𝑗 + 1)))))
31		oveq1 6917	. . . . . . 7 ⊢ (𝑥 = 𝑁 → (𝑥 + 1) = (𝑁 + 1))
32	31	oveq2d 6926	. . . . . 6 ⊢ (𝑥 = 𝑁 → (2↑(𝑥 + 1)) = (2↑(𝑁 + 1)))
33	32	fvoveq1d 6932	. . . . 5 ⊢ (𝑥 = 𝑁 → (seq1( + , 𝐹)‘((2↑(𝑥 + 1)) − 1)) = (seq1( + , 𝐹)‘((2↑(𝑁 + 1)) − 1)))
34		fveq2 6437	. . . . 5 ⊢ (𝑥 = 𝑁 → (seq0( + , 𝐺)‘𝑥) = (seq0( + , 𝐺)‘𝑁))
35	33, 34	breq12d 4888	. . . 4 ⊢ (𝑥 = 𝑁 → ((seq1( + , 𝐹)‘((2↑(𝑥 + 1)) − 1)) ≤ (seq0( + , 𝐺)‘𝑥) ↔ (seq1( + , 𝐹)‘((2↑(𝑁 + 1)) − 1)) ≤ (seq0( + , 𝐺)‘𝑁)))
36	35	imbi2d 332	. . 3 ⊢ (𝑥 = 𝑁 → ((𝜑 → (seq1( + , 𝐹)‘((2↑(𝑥 + 1)) − 1)) ≤ (seq0( + , 𝐺)‘𝑥)) ↔ (𝜑 → (seq1( + , 𝐹)‘((2↑(𝑁 + 1)) − 1)) ≤ (seq0( + , 𝐺)‘𝑁))))
37		fveq2 6437	. . . . . . . 8 ⊢ (𝑘 = 1 → (𝐹‘𝑘) = (𝐹‘1))
38	37	eleq1d 2891	. . . . . . 7 ⊢ (𝑘 = 1 → ((𝐹‘𝑘) ∈ ℝ ↔ (𝐹‘1) ∈ ℝ))
39		climcnds.1	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) ∈ ℝ)
40	39	ralrimiva 3175	. . . . . . 7 ⊢ (𝜑 → ∀𝑘 ∈ ℕ (𝐹‘𝑘) ∈ ℝ)
41		1nn 11370	. . . . . . . 8 ⊢ 1 ∈ ℕ
42	41	a1i 11	. . . . . . 7 ⊢ (𝜑 → 1 ∈ ℕ)
43	38, 40, 42	rspcdva 3532	. . . . . 6 ⊢ (𝜑 → (𝐹‘1) ∈ ℝ)
44	43	leidd 10925	. . . . 5 ⊢ (𝜑 → (𝐹‘1) ≤ (𝐹‘1))
45	43	recnd 10392	. . . . . 6 ⊢ (𝜑 → (𝐹‘1) ∈ ℂ)
46	45	mulid2d 10382	. . . . 5 ⊢ (𝜑 → (1 · (𝐹‘1)) = (𝐹‘1))
47	44, 46	breqtrrd 4903	. . . 4 ⊢ (𝜑 → (𝐹‘1) ≤ (1 · (𝐹‘1)))
48		1z 11742	. . . . 5 ⊢ 1 ∈ ℤ
49		eqidd 2826	. . . . 5 ⊢ (𝜑 → (𝐹‘1) = (𝐹‘1))
50	48, 49	seq1i 13116	. . . 4 ⊢ (𝜑 → (seq1( + , 𝐹)‘1) = (𝐹‘1))
51		0z 11722	. . . . 5 ⊢ 0 ∈ ℤ
52		fveq2 6437	. . . . . . 7 ⊢ (𝑛 = 0 → (𝐺‘𝑛) = (𝐺‘0))
53		oveq2 6918	. . . . . . . . 9 ⊢ (𝑛 = 0 → (2↑𝑛) = (2↑0))
54		exp0 13165	. . . . . . . . . 10 ⊢ (2 ∈ ℂ → (2↑0) = 1)
55	5, 54	ax-mp 5	. . . . . . . . 9 ⊢ (2↑0) = 1
56	53, 55	syl6eq 2877	. . . . . . . 8 ⊢ (𝑛 = 0 → (2↑𝑛) = 1)
57	56	fveq2d 6441	. . . . . . . 8 ⊢ (𝑛 = 0 → (𝐹‘(2↑𝑛)) = (𝐹‘1))
58	56, 57	oveq12d 6928	. . . . . . 7 ⊢ (𝑛 = 0 → ((2↑𝑛) · (𝐹‘(2↑𝑛))) = (1 · (𝐹‘1)))
59	52, 58	eqeq12d 2840	. . . . . 6 ⊢ (𝑛 = 0 → ((𝐺‘𝑛) = ((2↑𝑛) · (𝐹‘(2↑𝑛))) ↔ (𝐺‘0) = (1 · (𝐹‘1))))
60		climcnds.4	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → (𝐺‘𝑛) = ((2↑𝑛) · (𝐹‘(2↑𝑛))))
61	60	ralrimiva 3175	. . . . . 6 ⊢ (𝜑 → ∀𝑛 ∈ ℕ₀ (𝐺‘𝑛) = ((2↑𝑛) · (𝐹‘(2↑𝑛))))
62		0nn0 11642	. . . . . . 7 ⊢ 0 ∈ ℕ₀
63	62	a1i 11	. . . . . 6 ⊢ (𝜑 → 0 ∈ ℕ₀)
64	59, 61, 63	rspcdva 3532	. . . . 5 ⊢ (𝜑 → (𝐺‘0) = (1 · (𝐹‘1)))
65	51, 64	seq1i 13116	. . . 4 ⊢ (𝜑 → (seq0( + , 𝐺)‘0) = (1 · (𝐹‘1)))
66	47, 50, 65	3brtr4d 4907	. . 3 ⊢ (𝜑 → (seq1( + , 𝐹)‘1) ≤ (seq0( + , 𝐺)‘0))
67		fzfid 13074	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → ((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1)) ∈ Fin)
68		simpl 476	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → 𝜑)
69	68	adantr 474	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ₀) ∧ 𝑘 ∈ ((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1))) → 𝜑)
70		2nn 11431	. . . . . . . . . . . 12 ⊢ 2 ∈ ℕ
71		peano2nn0 11667	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ ℕ₀ → (𝑗 + 1) ∈ ℕ₀)
72	71	adantl 475	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → (𝑗 + 1) ∈ ℕ₀)
73		nnexpcl 13174	. . . . . . . . . . . 12 ⊢ ((2 ∈ ℕ ∧ (𝑗 + 1) ∈ ℕ₀) → (2↑(𝑗 + 1)) ∈ ℕ)
74	70, 72, 73	sylancr 581	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → (2↑(𝑗 + 1)) ∈ ℕ)
75		elfzuz 12638	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1)) → 𝑘 ∈ (ℤ_≥‘(2↑(𝑗 + 1))))
76		eluznn 12048	. . . . . . . . . . 11 ⊢ (((2↑(𝑗 + 1)) ∈ ℕ ∧ 𝑘 ∈ (ℤ_≥‘(2↑(𝑗 + 1)))) → 𝑘 ∈ ℕ)
77	74, 75, 76	syl2an 589	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ₀) ∧ 𝑘 ∈ ((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1))) → 𝑘 ∈ ℕ)
78	69, 77, 39	syl2anc 579	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ₀) ∧ 𝑘 ∈ ((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1))) → (𝐹‘𝑘) ∈ ℝ)
79		fveq2 6437	. . . . . . . . . . . 12 ⊢ (𝑘 = (2↑(𝑗 + 1)) → (𝐹‘𝑘) = (𝐹‘(2↑(𝑗 + 1))))
80	79	eleq1d 2891	. . . . . . . . . . 11 ⊢ (𝑘 = (2↑(𝑗 + 1)) → ((𝐹‘𝑘) ∈ ℝ ↔ (𝐹‘(2↑(𝑗 + 1))) ∈ ℝ))
81	40	adantr 474	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → ∀𝑘 ∈ ℕ (𝐹‘𝑘) ∈ ℝ)
82	80, 81, 74	rspcdva 3532	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → (𝐹‘(2↑(𝑗 + 1))) ∈ ℝ)
83	82	adantr 474	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ₀) ∧ 𝑘 ∈ ((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1))) → (𝐹‘(2↑(𝑗 + 1))) ∈ ℝ)
84		simpr 479	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ₀) ∧ 𝑛 ∈ (ℤ_≥‘(2↑(𝑗 + 1)))) → 𝑛 ∈ (ℤ_≥‘(2↑(𝑗 + 1))))
85		simplll 791	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ₀) ∧ 𝑛 ∈ (ℤ_≥‘(2↑(𝑗 + 1)))) ∧ 𝑘 ∈ ((2↑(𝑗 + 1))...𝑛)) → 𝜑)
86	74	adantr 474	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ₀) ∧ 𝑛 ∈ (ℤ_≥‘(2↑(𝑗 + 1)))) → (2↑(𝑗 + 1)) ∈ ℕ)
87		elfzuz 12638	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ ((2↑(𝑗 + 1))...𝑛) → 𝑘 ∈ (ℤ_≥‘(2↑(𝑗 + 1))))
88	86, 87, 76	syl2an 589	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ₀) ∧ 𝑛 ∈ (ℤ_≥‘(2↑(𝑗 + 1)))) ∧ 𝑘 ∈ ((2↑(𝑗 + 1))...𝑛)) → 𝑘 ∈ ℕ)
89	85, 88, 39	syl2anc 579	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ₀) ∧ 𝑛 ∈ (ℤ_≥‘(2↑(𝑗 + 1)))) ∧ 𝑘 ∈ ((2↑(𝑗 + 1))...𝑛)) → (𝐹‘𝑘) ∈ ℝ)
90		simplll 791	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ₀) ∧ 𝑛 ∈ (ℤ_≥‘(2↑(𝑗 + 1)))) ∧ 𝑘 ∈ ((2↑(𝑗 + 1))...(𝑛 − 1))) → 𝜑)
91		elfzuz 12638	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ ((2↑(𝑗 + 1))...(𝑛 − 1)) → 𝑘 ∈ (ℤ_≥‘(2↑(𝑗 + 1))))
92	86, 91, 76	syl2an 589	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ₀) ∧ 𝑛 ∈ (ℤ_≥‘(2↑(𝑗 + 1)))) ∧ 𝑘 ∈ ((2↑(𝑗 + 1))...(𝑛 − 1))) → 𝑘 ∈ ℕ)
93		climcnds.3	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘(𝑘 + 1)) ≤ (𝐹‘𝑘))
94	90, 92, 93	syl2anc 579	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ₀) ∧ 𝑛 ∈ (ℤ_≥‘(2↑(𝑗 + 1)))) ∧ 𝑘 ∈ ((2↑(𝑗 + 1))...(𝑛 − 1))) → (𝐹‘(𝑘 + 1)) ≤ (𝐹‘𝑘))
95	84, 89, 94	monoord2 13133	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ₀) ∧ 𝑛 ∈ (ℤ_≥‘(2↑(𝑗 + 1)))) → (𝐹‘𝑛) ≤ (𝐹‘(2↑(𝑗 + 1))))
96	95	ralrimiva 3175	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → ∀𝑛 ∈ (ℤ_≥‘(2↑(𝑗 + 1)))(𝐹‘𝑛) ≤ (𝐹‘(2↑(𝑗 + 1))))
97		fveq2 6437	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝑘 → (𝐹‘𝑛) = (𝐹‘𝑘))
98	97	breq1d 4885	. . . . . . . . . . 11 ⊢ (𝑛 = 𝑘 → ((𝐹‘𝑛) ≤ (𝐹‘(2↑(𝑗 + 1))) ↔ (𝐹‘𝑘) ≤ (𝐹‘(2↑(𝑗 + 1)))))
99	98	rspccva 3525	. . . . . . . . . 10 ⊢ ((∀𝑛 ∈ (ℤ_≥‘(2↑(𝑗 + 1)))(𝐹‘𝑛) ≤ (𝐹‘(2↑(𝑗 + 1))) ∧ 𝑘 ∈ (ℤ_≥‘(2↑(𝑗 + 1)))) → (𝐹‘𝑘) ≤ (𝐹‘(2↑(𝑗 + 1))))
100	96, 75, 99	syl2an 589	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ₀) ∧ 𝑘 ∈ ((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1))) → (𝐹‘𝑘) ≤ (𝐹‘(2↑(𝑗 + 1))))
101	67, 78, 83, 100	fsumle 14912	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → Σ𝑘 ∈ ((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1))(𝐹‘𝑘) ≤ Σ𝑘 ∈ ((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1))(𝐹‘(2↑(𝑗 + 1))))
102		fzfid 13074	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → (1...((2↑(𝑗 + 1)) − 1)) ∈ Fin)
103		hashcl 13444	. . . . . . . . . . . . 13 ⊢ ((1...((2↑(𝑗 + 1)) − 1)) ∈ Fin → (♯‘(1...((2↑(𝑗 + 1)) − 1))) ∈ ℕ₀)
104	102, 103	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → (♯‘(1...((2↑(𝑗 + 1)) − 1))) ∈ ℕ₀)
105	104	nn0cnd 11687	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → (♯‘(1...((2↑(𝑗 + 1)) − 1))) ∈ ℂ)
106	74	nnred 11374	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → (2↑(𝑗 + 1)) ∈ ℝ)
107	106	recnd 10392	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → (2↑(𝑗 + 1)) ∈ ℂ)
108		hashcl 13444	. . . . . . . . . . . . 13 ⊢ (((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1)) ∈ Fin → (♯‘((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1))) ∈ ℕ₀)
109	67, 108	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → (♯‘((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1))) ∈ ℕ₀)
110	109	nn0cnd 11687	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → (♯‘((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1))) ∈ ℂ)
111		2z 11744	. . . . . . . . . . . . . . . . . . . 20 ⊢ 2 ∈ ℤ
112		zexpcl 13176	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((2 ∈ ℤ ∧ (𝑗 + 1) ∈ ℕ₀) → (2↑(𝑗 + 1)) ∈ ℤ)
113	111, 72, 112	sylancr 581	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → (2↑(𝑗 + 1)) ∈ ℤ)
114		nn0p1nn 11666	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑗 ∈ ℕ₀ → (𝑗 + 1) ∈ ℕ)
115	114	adantl 475	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → (𝑗 + 1) ∈ ℕ)
116		nnuz 12012	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ℕ = (ℤ_≥‘1)
117	115, 116	syl6eleq 2916	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → (𝑗 + 1) ∈ (ℤ_≥‘1))
118		2re 11432	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 2 ∈ ℝ
119		1le2 11574	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 1 ≤ 2
120		leexp2a 13217	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((2 ∈ ℝ ∧ 1 ≤ 2 ∧ (𝑗 + 1) ∈ (ℤ_≥‘1)) → (2↑1) ≤ (2↑(𝑗 + 1)))
121	118, 119, 120	mp3an12 1579	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑗 + 1) ∈ (ℤ_≥‘1) → (2↑1) ≤ (2↑(𝑗 + 1)))
122	117, 121	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → (2↑1) ≤ (2↑(𝑗 + 1)))
123	7, 122	syl5eqbrr 4911	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → 2 ≤ (2↑(𝑗 + 1)))
124	111	eluz1i 11983	. . . . . . . . . . . . . . . . . . 19 ⊢ ((2↑(𝑗 + 1)) ∈ (ℤ_≥‘2) ↔ ((2↑(𝑗 + 1)) ∈ ℤ ∧ 2 ≤ (2↑(𝑗 + 1))))
125	113, 123, 124	sylanbrc 578	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → (2↑(𝑗 + 1)) ∈ (ℤ_≥‘2))
126		uz2m1nn 12053	. . . . . . . . . . . . . . . . . 18 ⊢ ((2↑(𝑗 + 1)) ∈ (ℤ_≥‘2) → ((2↑(𝑗 + 1)) − 1) ∈ ℕ)
127	125, 126	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → ((2↑(𝑗 + 1)) − 1) ∈ ℕ)
128	127, 116	syl6eleq 2916	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → ((2↑(𝑗 + 1)) − 1) ∈ (ℤ_≥‘1))
129		peano2zm 11755	. . . . . . . . . . . . . . . . . 18 ⊢ ((2↑(𝑗 + 1)) ∈ ℤ → ((2↑(𝑗 + 1)) − 1) ∈ ℤ)
130	113, 129	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → ((2↑(𝑗 + 1)) − 1) ∈ ℤ)
131		peano2nn0 11667	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑗 + 1) ∈ ℕ₀ → ((𝑗 + 1) + 1) ∈ ℕ₀)
132	72, 131	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → ((𝑗 + 1) + 1) ∈ ℕ₀)
133		zexpcl 13176	. . . . . . . . . . . . . . . . . . 19 ⊢ ((2 ∈ ℤ ∧ ((𝑗 + 1) + 1) ∈ ℕ₀) → (2↑((𝑗 + 1) + 1)) ∈ ℤ)
134	111, 132, 133	sylancr 581	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → (2↑((𝑗 + 1) + 1)) ∈ ℤ)
135		peano2zm 11755	. . . . . . . . . . . . . . . . . 18 ⊢ ((2↑((𝑗 + 1) + 1)) ∈ ℤ → ((2↑((𝑗 + 1) + 1)) − 1) ∈ ℤ)
136	134, 135	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → ((2↑((𝑗 + 1) + 1)) − 1) ∈ ℤ)
137	113	zred 11817	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → (2↑(𝑗 + 1)) ∈ ℝ)
138	134	zred 11817	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → (2↑((𝑗 + 1) + 1)) ∈ ℝ)
139		1red 10364	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → 1 ∈ ℝ)
140	72	nn0zd 11815	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → (𝑗 + 1) ∈ ℤ)
141		uzid 11990	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑗 + 1) ∈ ℤ → (𝑗 + 1) ∈ (ℤ_≥‘(𝑗 + 1)))
142		peano2uz 12030	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑗 + 1) ∈ (ℤ_≥‘(𝑗 + 1)) → ((𝑗 + 1) + 1) ∈ (ℤ_≥‘(𝑗 + 1)))
143		leexp2a 13217	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((2 ∈ ℝ ∧ 1 ≤ 2 ∧ ((𝑗 + 1) + 1) ∈ (ℤ_≥‘(𝑗 + 1))) → (2↑(𝑗 + 1)) ≤ (2↑((𝑗 + 1) + 1)))
144	118, 119, 143	mp3an12 1579	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑗 + 1) + 1) ∈ (ℤ_≥‘(𝑗 + 1)) → (2↑(𝑗 + 1)) ≤ (2↑((𝑗 + 1) + 1)))
145	140, 141, 142, 144	4syl 19	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → (2↑(𝑗 + 1)) ≤ (2↑((𝑗 + 1) + 1)))
146	137, 138, 139, 145	lesub1dd 10975	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → ((2↑(𝑗 + 1)) − 1) ≤ ((2↑((𝑗 + 1) + 1)) − 1))
147		eluz2 11981	. . . . . . . . . . . . . . . . 17 ⊢ (((2↑((𝑗 + 1) + 1)) − 1) ∈ (ℤ_≥‘((2↑(𝑗 + 1)) − 1)) ↔ (((2↑(𝑗 + 1)) − 1) ∈ ℤ ∧ ((2↑((𝑗 + 1) + 1)) − 1) ∈ ℤ ∧ ((2↑(𝑗 + 1)) − 1) ≤ ((2↑((𝑗 + 1) + 1)) − 1)))
148	130, 136, 146, 147	syl3anbrc 1447	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → ((2↑((𝑗 + 1) + 1)) − 1) ∈ (ℤ_≥‘((2↑(𝑗 + 1)) − 1)))
149		elfzuzb 12636	. . . . . . . . . . . . . . . 16 ⊢ (((2↑(𝑗 + 1)) − 1) ∈ (1...((2↑((𝑗 + 1) + 1)) − 1)) ↔ (((2↑(𝑗 + 1)) − 1) ∈ (ℤ_≥‘1) ∧ ((2↑((𝑗 + 1) + 1)) − 1) ∈ (ℤ_≥‘((2↑(𝑗 + 1)) − 1))))
150	128, 148, 149	sylanbrc 578	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → ((2↑(𝑗 + 1)) − 1) ∈ (1...((2↑((𝑗 + 1) + 1)) − 1)))
151		fzsplit 12667	. . . . . . . . . . . . . . 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))))
152	150, 151	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → (1...((2↑((𝑗 + 1) + 1)) − 1)) = ((1...((2↑(𝑗 + 1)) − 1)) ∪ ((((2↑(𝑗 + 1)) − 1) + 1)...((2↑((𝑗 + 1) + 1)) − 1))))
153		npcan 10618	. . . . . . . . . . . . . . . . 17 ⊢ (((2↑(𝑗 + 1)) ∈ ℂ ∧ 1 ∈ ℂ) → (((2↑(𝑗 + 1)) − 1) + 1) = (2↑(𝑗 + 1)))
154	107, 12, 153	sylancl 580	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → (((2↑(𝑗 + 1)) − 1) + 1) = (2↑(𝑗 + 1)))
155	154	oveq1d 6925	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → ((((2↑(𝑗 + 1)) − 1) + 1)...((2↑((𝑗 + 1) + 1)) − 1)) = ((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1)))
156	155	uneq2d 3996	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → ((1...((2↑(𝑗 + 1)) − 1)) ∪ ((((2↑(𝑗 + 1)) − 1) + 1)...((2↑((𝑗 + 1) + 1)) − 1))) = ((1...((2↑(𝑗 + 1)) − 1)) ∪ ((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1))))
157	152, 156	eqtrd 2861	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → (1...((2↑((𝑗 + 1) + 1)) − 1)) = ((1...((2↑(𝑗 + 1)) − 1)) ∪ ((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1))))
158	157	fveq2d 6441	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → (♯‘(1...((2↑((𝑗 + 1) + 1)) − 1))) = (♯‘((1...((2↑(𝑗 + 1)) − 1)) ∪ ((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1)))))
159		expp1 13168	. . . . . . . . . . . . . . . . 17 ⊢ ((2 ∈ ℂ ∧ (𝑗 + 1) ∈ ℕ₀) → (2↑((𝑗 + 1) + 1)) = ((2↑(𝑗 + 1)) · 2))
160	5, 72, 159	sylancr 581	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → (2↑((𝑗 + 1) + 1)) = ((2↑(𝑗 + 1)) · 2))
161	107	times2d 11609	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → ((2↑(𝑗 + 1)) · 2) = ((2↑(𝑗 + 1)) + (2↑(𝑗 + 1))))
162	160, 161	eqtrd 2861	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → (2↑((𝑗 + 1) + 1)) = ((2↑(𝑗 + 1)) + (2↑(𝑗 + 1))))
163	162	oveq1d 6925	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → ((2↑((𝑗 + 1) + 1)) − 1) = (((2↑(𝑗 + 1)) + (2↑(𝑗 + 1))) − 1))
164		1cnd 10358	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → 1 ∈ ℂ)
165	107, 107, 164	addsubd 10741	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → (((2↑(𝑗 + 1)) + (2↑(𝑗 + 1))) − 1) = (((2↑(𝑗 + 1)) − 1) + (2↑(𝑗 + 1))))
166	163, 165	eqtrd 2861	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → ((2↑((𝑗 + 1) + 1)) − 1) = (((2↑(𝑗 + 1)) − 1) + (2↑(𝑗 + 1))))
167		uztrn 11992	. . . . . . . . . . . . . . . . 17 ⊢ ((((2↑((𝑗 + 1) + 1)) − 1) ∈ (ℤ_≥‘((2↑(𝑗 + 1)) − 1)) ∧ ((2↑(𝑗 + 1)) − 1) ∈ (ℤ_≥‘1)) → ((2↑((𝑗 + 1) + 1)) − 1) ∈ (ℤ_≥‘1))
168	148, 128, 167	syl2anc 579	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → ((2↑((𝑗 + 1) + 1)) − 1) ∈ (ℤ_≥‘1))
169	168, 116	syl6eleqr 2917	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → ((2↑((𝑗 + 1) + 1)) − 1) ∈ ℕ)
170	169	nnnn0d 11685	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → ((2↑((𝑗 + 1) + 1)) − 1) ∈ ℕ₀)
171		hashfz1 13433	. . . . . . . . . . . . . 14 ⊢ (((2↑((𝑗 + 1) + 1)) − 1) ∈ ℕ₀ → (♯‘(1...((2↑((𝑗 + 1) + 1)) − 1))) = ((2↑((𝑗 + 1) + 1)) − 1))
172	170, 171	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → (♯‘(1...((2↑((𝑗 + 1) + 1)) − 1))) = ((2↑((𝑗 + 1) + 1)) − 1))
173	127	nnnn0d 11685	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → ((2↑(𝑗 + 1)) − 1) ∈ ℕ₀)
174		hashfz1 13433	. . . . . . . . . . . . . . 15 ⊢ (((2↑(𝑗 + 1)) − 1) ∈ ℕ₀ → (♯‘(1...((2↑(𝑗 + 1)) − 1))) = ((2↑(𝑗 + 1)) − 1))
175	173, 174	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → (♯‘(1...((2↑(𝑗 + 1)) − 1))) = ((2↑(𝑗 + 1)) − 1))
176	175	oveq1d 6925	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → ((♯‘(1...((2↑(𝑗 + 1)) − 1))) + (2↑(𝑗 + 1))) = (((2↑(𝑗 + 1)) − 1) + (2↑(𝑗 + 1))))
177	166, 172, 176	3eqtr4d 2871	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → (♯‘(1...((2↑((𝑗 + 1) + 1)) − 1))) = ((♯‘(1...((2↑(𝑗 + 1)) − 1))) + (2↑(𝑗 + 1))))
178	106	ltm1d 11293	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → ((2↑(𝑗 + 1)) − 1) < (2↑(𝑗 + 1)))
179		fzdisj 12668	. . . . . . . . . . . . . 14 ⊢ (((2↑(𝑗 + 1)) − 1) < (2↑(𝑗 + 1)) → ((1...((2↑(𝑗 + 1)) − 1)) ∩ ((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1))) = ∅)
180	178, 179	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → ((1...((2↑(𝑗 + 1)) − 1)) ∩ ((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1))) = ∅)
181		hashun 13468	. . . . . . . . . . . . 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)))))
182	102, 67, 180, 181	syl3anc 1494	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → (♯‘((1...((2↑(𝑗 + 1)) − 1)) ∪ ((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1)))) = ((♯‘(1...((2↑(𝑗 + 1)) − 1))) + (♯‘((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1)))))
183	158, 177, 182	3eqtr3d 2869	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → ((♯‘(1...((2↑(𝑗 + 1)) − 1))) + (2↑(𝑗 + 1))) = ((♯‘(1...((2↑(𝑗 + 1)) − 1))) + (♯‘((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1)))))
184	105, 107, 110, 183	addcanad 10567	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → (2↑(𝑗 + 1)) = (♯‘((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1))))
185	184	oveq1d 6925	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → ((2↑(𝑗 + 1)) · (𝐹‘(2↑(𝑗 + 1)))) = ((♯‘((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1))) · (𝐹‘(2↑(𝑗 + 1)))))
186		fveq2 6437	. . . . . . . . . . 11 ⊢ (𝑛 = (𝑗 + 1) → (𝐺‘𝑛) = (𝐺‘(𝑗 + 1)))
187		oveq2 6918	. . . . . . . . . . . 12 ⊢ (𝑛 = (𝑗 + 1) → (2↑𝑛) = (2↑(𝑗 + 1)))
188	187	fveq2d 6441	. . . . . . . . . . . 12 ⊢ (𝑛 = (𝑗 + 1) → (𝐹‘(2↑𝑛)) = (𝐹‘(2↑(𝑗 + 1))))
189	187, 188	oveq12d 6928	. . . . . . . . . . 11 ⊢ (𝑛 = (𝑗 + 1) → ((2↑𝑛) · (𝐹‘(2↑𝑛))) = ((2↑(𝑗 + 1)) · (𝐹‘(2↑(𝑗 + 1)))))
190	186, 189	eqeq12d 2840	. . . . . . . . . 10 ⊢ (𝑛 = (𝑗 + 1) → ((𝐺‘𝑛) = ((2↑𝑛) · (𝐹‘(2↑𝑛))) ↔ (𝐺‘(𝑗 + 1)) = ((2↑(𝑗 + 1)) · (𝐹‘(2↑(𝑗 + 1))))))
191	61	adantr 474	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → ∀𝑛 ∈ ℕ₀ (𝐺‘𝑛) = ((2↑𝑛) · (𝐹‘(2↑𝑛))))
192	190, 191, 72	rspcdva 3532	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → (𝐺‘(𝑗 + 1)) = ((2↑(𝑗 + 1)) · (𝐹‘(2↑(𝑗 + 1)))))
193	82	recnd 10392	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → (𝐹‘(2↑(𝑗 + 1))) ∈ ℂ)
194		fsumconst 14903	. . . . . . . . . 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)))))
195	67, 193, 194	syl2anc 579	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → Σ𝑘 ∈ ((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1))(𝐹‘(2↑(𝑗 + 1))) = ((♯‘((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1))) · (𝐹‘(2↑(𝑗 + 1)))))
196	185, 192, 195	3eqtr4d 2871	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → (𝐺‘(𝑗 + 1)) = Σ𝑘 ∈ ((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1))(𝐹‘(2↑(𝑗 + 1))))
197	101, 196	breqtrrd 4903	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → Σ𝑘 ∈ ((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1))(𝐹‘𝑘) ≤ (𝐺‘(𝑗 + 1)))
198		elfznn 12670	. . . . . . . . . 10 ⊢ (𝑘 ∈ (1...((2↑(𝑗 + 1)) − 1)) → 𝑘 ∈ ℕ)
199	68, 198, 39	syl2an 589	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ₀) ∧ 𝑘 ∈ (1...((2↑(𝑗 + 1)) − 1))) → (𝐹‘𝑘) ∈ ℝ)
200	102, 199	fsumrecl 14849	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → Σ𝑘 ∈ (1...((2↑(𝑗 + 1)) − 1))(𝐹‘𝑘) ∈ ℝ)
201	67, 78	fsumrecl 14849	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → Σ𝑘 ∈ ((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1))(𝐹‘𝑘) ∈ ℝ)
202		nn0uz 12011	. . . . . . . . . 10 ⊢ ℕ₀ = (ℤ_≥‘0)
203		0zd 11723	. . . . . . . . . 10 ⊢ (𝜑 → 0 ∈ ℤ)
204		simpr 479	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → 𝑛 ∈ ℕ₀)
205		nnexpcl 13174	. . . . . . . . . . . . . 14 ⊢ ((2 ∈ ℕ ∧ 𝑛 ∈ ℕ₀) → (2↑𝑛) ∈ ℕ)
206	70, 204, 205	sylancr 581	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → (2↑𝑛) ∈ ℕ)
207	206	nnred 11374	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → (2↑𝑛) ∈ ℝ)
208		fveq2 6437	. . . . . . . . . . . . . 14 ⊢ (𝑘 = (2↑𝑛) → (𝐹‘𝑘) = (𝐹‘(2↑𝑛)))
209	208	eleq1d 2891	. . . . . . . . . . . . 13 ⊢ (𝑘 = (2↑𝑛) → ((𝐹‘𝑘) ∈ ℝ ↔ (𝐹‘(2↑𝑛)) ∈ ℝ))
210	40	adantr 474	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → ∀𝑘 ∈ ℕ (𝐹‘𝑘) ∈ ℝ)
211	209, 210, 206	rspcdva 3532	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → (𝐹‘(2↑𝑛)) ∈ ℝ)
212	207, 211	remulcld 10394	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → ((2↑𝑛) · (𝐹‘(2↑𝑛))) ∈ ℝ)
213	60, 212	eqeltrd 2906	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → (𝐺‘𝑛) ∈ ℝ)
214	202, 203, 213	serfre 13131	. . . . . . . . 9 ⊢ (𝜑 → seq0( + , 𝐺):ℕ₀⟶ℝ)
215	214	ffvelrnda 6613	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → (seq0( + , 𝐺)‘𝑗) ∈ ℝ)
216	137, 82	remulcld 10394	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → ((2↑(𝑗 + 1)) · (𝐹‘(2↑(𝑗 + 1)))) ∈ ℝ)
217	192, 216	eqeltrd 2906	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → (𝐺‘(𝑗 + 1)) ∈ ℝ)
218		le2add 10841	. . . . . . . 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)))))
219	200, 201, 215, 217, 218	syl22anc 872	. . . . . . 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)))))
220	197, 219	mpan2d 685	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → (Σ𝑘 ∈ (1...((2↑(𝑗 + 1)) − 1))(𝐹‘𝑘) ≤ (seq0( + , 𝐺)‘𝑗) → (Σ𝑘 ∈ (1...((2↑(𝑗 + 1)) − 1))(𝐹‘𝑘) + Σ𝑘 ∈ ((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1))(𝐹‘𝑘)) ≤ ((seq0( + , 𝐺)‘𝑗) + (𝐺‘(𝑗 + 1)))))
221		eqidd 2826	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ₀) ∧ 𝑘 ∈ (1...((2↑(𝑗 + 1)) − 1))) → (𝐹‘𝑘) = (𝐹‘𝑘))
222	39	recnd 10392	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) ∈ ℂ)
223	68, 198, 222	syl2an 589	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ₀) ∧ 𝑘 ∈ (1...((2↑(𝑗 + 1)) − 1))) → (𝐹‘𝑘) ∈ ℂ)
224	221, 128, 223	fsumser 14845	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → Σ𝑘 ∈ (1...((2↑(𝑗 + 1)) − 1))(𝐹‘𝑘) = (seq1( + , 𝐹)‘((2↑(𝑗 + 1)) − 1)))
225	224	eqcomd 2831	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → (seq1( + , 𝐹)‘((2↑(𝑗 + 1)) − 1)) = Σ𝑘 ∈ (1...((2↑(𝑗 + 1)) − 1))(𝐹‘𝑘))
226	225	breq1d 4885	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → ((seq1( + , 𝐹)‘((2↑(𝑗 + 1)) − 1)) ≤ (seq0( + , 𝐺)‘𝑗) ↔ Σ𝑘 ∈ (1...((2↑(𝑗 + 1)) − 1))(𝐹‘𝑘) ≤ (seq0( + , 𝐺)‘𝑗)))
227		eqidd 2826	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ₀) ∧ 𝑘 ∈ (1...((2↑((𝑗 + 1) + 1)) − 1))) → (𝐹‘𝑘) = (𝐹‘𝑘))
228		elfznn 12670	. . . . . . . . . 10 ⊢ (𝑘 ∈ (1...((2↑((𝑗 + 1) + 1)) − 1)) → 𝑘 ∈ ℕ)
229	68, 228, 222	syl2an 589	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ₀) ∧ 𝑘 ∈ (1...((2↑((𝑗 + 1) + 1)) − 1))) → (𝐹‘𝑘) ∈ ℂ)
230	227, 168, 229	fsumser 14845	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → Σ𝑘 ∈ (1...((2↑((𝑗 + 1) + 1)) − 1))(𝐹‘𝑘) = (seq1( + , 𝐹)‘((2↑((𝑗 + 1) + 1)) − 1)))
231		fzfid 13074	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → (1...((2↑((𝑗 + 1) + 1)) − 1)) ∈ Fin)
232	180, 157, 231, 229	fsumsplit 14855	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → Σ𝑘 ∈ (1...((2↑((𝑗 + 1) + 1)) − 1))(𝐹‘𝑘) = (Σ𝑘 ∈ (1...((2↑(𝑗 + 1)) − 1))(𝐹‘𝑘) + Σ𝑘 ∈ ((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1))(𝐹‘𝑘)))
233	230, 232	eqtr3d 2863	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → (seq1( + , 𝐹)‘((2↑((𝑗 + 1) + 1)) − 1)) = (Σ𝑘 ∈ (1...((2↑(𝑗 + 1)) − 1))(𝐹‘𝑘) + Σ𝑘 ∈ ((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1))(𝐹‘𝑘)))
234		simpr 479	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → 𝑗 ∈ ℕ₀)
235	234, 202	syl6eleq 2916	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → 𝑗 ∈ (ℤ_≥‘0))
236		seqp1 13117	. . . . . . . 8 ⊢ (𝑗 ∈ (ℤ_≥‘0) → (seq0( + , 𝐺)‘(𝑗 + 1)) = ((seq0( + , 𝐺)‘𝑗) + (𝐺‘(𝑗 + 1))))
237	235, 236	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → (seq0( + , 𝐺)‘(𝑗 + 1)) = ((seq0( + , 𝐺)‘𝑗) + (𝐺‘(𝑗 + 1))))
238	233, 237	breq12d 4888	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → ((seq1( + , 𝐹)‘((2↑((𝑗 + 1) + 1)) − 1)) ≤ (seq0( + , 𝐺)‘(𝑗 + 1)) ↔ (Σ𝑘 ∈ (1...((2↑(𝑗 + 1)) − 1))(𝐹‘𝑘) + Σ𝑘 ∈ ((2↑(𝑗 + 1))...((2↑((𝑗 + 1) + 1)) − 1))(𝐹‘𝑘)) ≤ ((seq0( + , 𝐺)‘𝑗) + (𝐺‘(𝑗 + 1)))))
239	220, 226, 238	3imtr4d 286	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → ((seq1( + , 𝐹)‘((2↑(𝑗 + 1)) − 1)) ≤ (seq0( + , 𝐺)‘𝑗) → (seq1( + , 𝐹)‘((2↑((𝑗 + 1) + 1)) − 1)) ≤ (seq0( + , 𝐺)‘(𝑗 + 1))))
240	239	expcom 404	. . . 4 ⊢ (𝑗 ∈ ℕ₀ → (𝜑 → ((seq1( + , 𝐹)‘((2↑(𝑗 + 1)) − 1)) ≤ (seq0( + , 𝐺)‘𝑗) → (seq1( + , 𝐹)‘((2↑((𝑗 + 1) + 1)) − 1)) ≤ (seq0( + , 𝐺)‘(𝑗 + 1)))))
241	240	a2d 29	. . 3 ⊢ (𝑗 ∈ ℕ₀ → ((𝜑 → (seq1( + , 𝐹)‘((2↑(𝑗 + 1)) − 1)) ≤ (seq0( + , 𝐺)‘𝑗)) → (𝜑 → (seq1( + , 𝐹)‘((2↑((𝑗 + 1) + 1)) − 1)) ≤ (seq0( + , 𝐺)‘(𝑗 + 1)))))
242	18, 24, 30, 36, 66, 241	nn0ind 11807	. 2 ⊢ (𝑁 ∈ ℕ₀ → (𝜑 → (seq1( + , 𝐹)‘((2↑(𝑁 + 1)) − 1)) ≤ (seq0( + , 𝐺)‘𝑁)))
243	242	impcom 398	1 ⊢ ((𝜑 ∧ 𝑁 ∈ ℕ₀) → (seq1( + , 𝐹)‘((2↑(𝑁 + 1)) − 1)) ≤ (seq0( + , 𝐺)‘𝑁))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 386 = wceq 1656 ∈ wcel 2164 ∀wral 3117 ∪ cun 3796 ∩ cin 3797 ∅c0 4146 class class class wbr 4875 ‘cfv 6127 (class class class)co 6910 Fincfn 8228 ℂcc 10257 ℝcr 10258 0cc0 10259 1c1 10260 + caddc 10262 · cmul 10264 < clt 10398 ≤ cle 10399 − cmin 10592 ℕcn 11357 2c2 11413 ℕ₀cn0 11625 ℤcz 11711 ℤ_≥cuz 11975 ...cfz 12626 seqcseq 13102 ↑cexp 13161 ♯chash 13417 Σcsu 14800

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1894 ax-4 1908 ax-5 2009 ax-6 2075 ax-7 2112 ax-8 2166 ax-9 2173 ax-10 2192 ax-11 2207 ax-12 2220 ax-13 2389 ax-ext 2803 ax-rep 4996 ax-sep 5007 ax-nul 5015 ax-pow 5067 ax-pr 5129 ax-un 7214 ax-inf2 8822 ax-cnex 10315 ax-resscn 10316 ax-1cn 10317 ax-icn 10318 ax-addcl 10319 ax-addrcl 10320 ax-mulcl 10321 ax-mulrcl 10322 ax-mulcom 10323 ax-addass 10324 ax-mulass 10325 ax-distr 10326 ax-i2m1 10327 ax-1ne0 10328 ax-1rid 10329 ax-rnegex 10330 ax-rrecex 10331 ax-cnre 10332 ax-pre-lttri 10333 ax-pre-lttrn 10334 ax-pre-ltadd 10335 ax-pre-mulgt0 10336 ax-pre-sup 10337

This theorem depends on definitions: df-bi 199 df-an 387 df-or 879 df-3or 1112 df-3an 1113 df-tru 1660 df-fal 1670 df-ex 1879 df-nf 1883 df-sb 2068 df-mo 2605 df-eu 2640 df-clab 2812 df-cleq 2818 df-clel 2821 df-nfc 2958 df-ne 3000 df-nel 3103 df-ral 3122 df-rex 3123 df-reu 3124 df-rmo 3125 df-rab 3126 df-v 3416 df-sbc 3663 df-csb 3758 df-dif 3801 df-un 3803 df-in 3805 df-ss 3812 df-pss 3814 df-nul 4147 df-if 4309 df-pw 4382 df-sn 4400 df-pr 4402 df-tp 4404 df-op 4406 df-uni 4661 df-int 4700 df-iun 4744 df-br 4876 df-opab 4938 df-mpt 4955 df-tr 4978 df-id 5252 df-eprel 5257 df-po 5265 df-so 5266 df-fr 5305 df-se 5306 df-we 5307 df-xp 5352 df-rel 5353 df-cnv 5354 df-co 5355 df-dm 5356 df-rn 5357 df-res 5358 df-ima 5359 df-pred 5924 df-ord 5970 df-on 5971 df-lim 5972 df-suc 5973 df-iota 6090 df-fun 6129 df-fn 6130 df-f 6131 df-f1 6132 df-fo 6133 df-f1o 6134 df-fv 6135 df-isom 6136 df-riota 6871 df-ov 6913 df-oprab 6914 df-mpt2 6915 df-om 7332 df-1st 7433 df-2nd 7434 df-wrecs 7677 df-recs 7739 df-rdg 7777 df-1o 7831 df-oadd 7835 df-er 8014 df-en 8229 df-dom 8230 df-sdom 8231 df-fin 8232 df-sup 8623 df-oi 8691 df-card 9085 df-cda 9312 df-pnf 10400 df-mnf 10401 df-xr 10402 df-ltxr 10403 df-le 10404 df-sub 10594 df-neg 10595 df-div 11017 df-nn 11358 df-2 11421 df-3 11422 df-n0 11626 df-z 11712 df-uz 11976 df-rp 12120 df-ico 12476 df-fz 12627 df-fzo 12768 df-seq 13103 df-exp 13162 df-hash 13418 df-cj 14223 df-re 14224 df-im 14225 df-sqrt 14359 df-abs 14360 df-clim 14603 df-sum 14801

This theorem is referenced by: climcnds 14964

W3C validator