Theorem log2tlbnd 26922

Description: Bound the error term in the series of log2cnv 26921. (Contributed by Mario Carneiro, 7-Apr-2015.)

Assertion

Ref	Expression
log2tlbnd	⊢ (𝑁 ∈ ℕ0 → ((log‘2) − Σ𝑛 ∈ (0...(𝑁 − 1))(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))) ∈ (0[,](3 / ((4 · ((2 · 𝑁) + 1)) · (9↑𝑁)))))

Distinct variable group:   𝑛,𝑁

Proof of Theorem log2tlbnd

Dummy variable 𝑘 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		fzfid 13926	. . . 4 ⊢ (𝑁 ∈ ℕ0 → (0...(𝑁 − 1)) ∈ Fin)
2		elfznn0 13565	. . . . 5 ⊢ (𝑛 ∈ (0...(𝑁 − 1)) → 𝑛 ∈ ℕ0)
3		2re 12246	. . . . . . 7 ⊢ 2 ∈ ℝ
4		3nn 12251	. . . . . . . . 9 ⊢ 3 ∈ ℕ
5		2nn0 12445	. . . . . . . . . . 11 ⊢ 2 ∈ ℕ0
6		simpr 484	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → 𝑛 ∈ ℕ0)
7		nn0mulcl 12464	. . . . . . . . . . 11 ⊢ ((2 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → (2 · 𝑛) ∈ ℕ0)
8	5, 6, 7	sylancr 588	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → (2 · 𝑛) ∈ ℕ0)
9		nn0p1nn 12467	. . . . . . . . . 10 ⊢ ((2 · 𝑛) ∈ ℕ0 → ((2 · 𝑛) + 1) ∈ ℕ)
10	8, 9	syl 17	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → ((2 · 𝑛) + 1) ∈ ℕ)
11		nnmulcl 12189	. . . . . . . . 9 ⊢ ((3 ∈ ℕ ∧ ((2 · 𝑛) + 1) ∈ ℕ) → (3 · ((2 · 𝑛) + 1)) ∈ ℕ)
12	4, 10, 11	sylancr 588	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → (3 · ((2 · 𝑛) + 1)) ∈ ℕ)
13		9nn 12270	. . . . . . . . 9 ⊢ 9 ∈ ℕ
14		nnexpcl 14027	. . . . . . . . 9 ⊢ ((9 ∈ ℕ ∧ 𝑛 ∈ ℕ0) → (9↑𝑛) ∈ ℕ)
15	13, 6, 14	sylancr 588	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → (9↑𝑛) ∈ ℕ)
16	12, 15	nnmulcld 12221	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)) ∈ ℕ)
17		nndivre 12209	. . . . . . 7 ⊢ ((2 ∈ ℝ ∧ ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)) ∈ ℕ) → (2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) ∈ ℝ)
18	3, 16, 17	sylancr 588	. . . . . 6 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → (2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) ∈ ℝ)
19	18	recnd 11164	. . . . 5 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → (2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) ∈ ℂ)
20	2, 19	sylan2 594	. . . 4 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (0...(𝑁 − 1))) → (2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) ∈ ℂ)
21	1, 20	fsumcl 15686	. . 3 ⊢ (𝑁 ∈ ℕ0 → Σ𝑛 ∈ (0...(𝑁 − 1))(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) ∈ ℂ)
22		eqid 2737	. . . . 5 ⊢ (ℤ≥‘𝑁) = (ℤ≥‘𝑁)
23		nn0z 12539	. . . . 5 ⊢ (𝑁 ∈ ℕ0 → 𝑁 ∈ ℤ)
24		eluznn0 12858	. . . . . 6 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → 𝑛 ∈ ℕ0)
25		oveq2 7368	. . . . . . . . . . 11 ⊢ (𝑘 = 𝑛 → (2 · 𝑘) = (2 · 𝑛))
26	25	oveq1d 7375	. . . . . . . . . 10 ⊢ (𝑘 = 𝑛 → ((2 · 𝑘) + 1) = ((2 · 𝑛) + 1))
27	26	oveq2d 7376	. . . . . . . . 9 ⊢ (𝑘 = 𝑛 → (3 · ((2 · 𝑘) + 1)) = (3 · ((2 · 𝑛) + 1)))
28		oveq2 7368	. . . . . . . . 9 ⊢ (𝑘 = 𝑛 → (9↑𝑘) = (9↑𝑛))
29	27, 28	oveq12d 7378	. . . . . . . 8 ⊢ (𝑘 = 𝑛 → ((3 · ((2 · 𝑘) + 1)) · (9↑𝑘)) = ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))
30	29	oveq2d 7376	. . . . . . 7 ⊢ (𝑘 = 𝑛 → (2 / ((3 · ((2 · 𝑘) + 1)) · (9↑𝑘))) = (2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))))
31		eqid 2737	. . . . . . 7 ⊢ (𝑘 ∈ ℕ0 ↦ (2 / ((3 · ((2 · 𝑘) + 1)) · (9↑𝑘)))) = (𝑘 ∈ ℕ0 ↦ (2 / ((3 · ((2 · 𝑘) + 1)) · (9↑𝑘))))
32		ovex 7393	. . . . . . 7 ⊢ (2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) ∈ V
33	30, 31, 32	fvmpt 6941	. . . . . 6 ⊢ (𝑛 ∈ ℕ0 → ((𝑘 ∈ ℕ0 ↦ (2 / ((3 · ((2 · 𝑘) + 1)) · (9↑𝑘))))‘𝑛) = (2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))))
34	24, 33	syl 17	. . . . 5 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → ((𝑘 ∈ ℕ0 ↦ (2 / ((3 · ((2 · 𝑘) + 1)) · (9↑𝑘))))‘𝑛) = (2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))))
35	24, 18	syldan 592	. . . . 5 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) ∈ ℝ)
36	31	log2cnv 26921	. . . . . . 7 ⊢ seq0( + , (𝑘 ∈ ℕ0 ↦ (2 / ((3 · ((2 · 𝑘) + 1)) · (9↑𝑘))))) ⇝ (log‘2)
37		seqex 13956	. . . . . . . 8 ⊢ seq0( + , (𝑘 ∈ ℕ0 ↦ (2 / ((3 · ((2 · 𝑘) + 1)) · (9↑𝑘))))) ∈ V
38		fvex 6847	. . . . . . . 8 ⊢ (log‘2) ∈ V
39	37, 38	breldm 5857	. . . . . . 7 ⊢ (seq0( + , (𝑘 ∈ ℕ0 ↦ (2 / ((3 · ((2 · 𝑘) + 1)) · (9↑𝑘))))) ⇝ (log‘2) → seq0( + , (𝑘 ∈ ℕ0 ↦ (2 / ((3 · ((2 · 𝑘) + 1)) · (9↑𝑘))))) ∈ dom ⇝ )
40	36, 39	mp1i 13	. . . . . 6 ⊢ (𝑁 ∈ ℕ0 → seq0( + , (𝑘 ∈ ℕ0 ↦ (2 / ((3 · ((2 · 𝑘) + 1)) · (9↑𝑘))))) ∈ dom ⇝ )
41		nn0uz 12817	. . . . . . 7 ⊢ ℕ0 = (ℤ≥‘0)
42		id 22	. . . . . . 7 ⊢ (𝑁 ∈ ℕ0 → 𝑁 ∈ ℕ0)
43	33	adantl 481	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → ((𝑘 ∈ ℕ0 ↦ (2 / ((3 · ((2 · 𝑘) + 1)) · (9↑𝑘))))‘𝑛) = (2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))))
44	43, 19	eqeltrd 2837	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → ((𝑘 ∈ ℕ0 ↦ (2 / ((3 · ((2 · 𝑘) + 1)) · (9↑𝑘))))‘𝑛) ∈ ℂ)
45	41, 42, 44	iserex 15610	. . . . . 6 ⊢ (𝑁 ∈ ℕ0 → (seq0( + , (𝑘 ∈ ℕ0 ↦ (2 / ((3 · ((2 · 𝑘) + 1)) · (9↑𝑘))))) ∈ dom ⇝ ↔ seq𝑁( + , (𝑘 ∈ ℕ0 ↦ (2 / ((3 · ((2 · 𝑘) + 1)) · (9↑𝑘))))) ∈ dom ⇝ ))
46	40, 45	mpbid 232	. . . . 5 ⊢ (𝑁 ∈ ℕ0 → seq𝑁( + , (𝑘 ∈ ℕ0 ↦ (2 / ((3 · ((2 · 𝑘) + 1)) · (9↑𝑘))))) ∈ dom ⇝ )
47	22, 23, 34, 35, 46	isumrecl 15718	. . . 4 ⊢ (𝑁 ∈ ℕ0 → Σ𝑛 ∈ (ℤ≥‘𝑁)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) ∈ ℝ)
48	47	recnd 11164	. . 3 ⊢ (𝑁 ∈ ℕ0 → Σ𝑛 ∈ (ℤ≥‘𝑁)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) ∈ ℂ)
49		0zd 12527	. . . . 5 ⊢ (𝑁 ∈ ℕ0 → 0 ∈ ℤ)
50	36	a1i 11	. . . . 5 ⊢ (𝑁 ∈ ℕ0 → seq0( + , (𝑘 ∈ ℕ0 ↦ (2 / ((3 · ((2 · 𝑘) + 1)) · (9↑𝑘))))) ⇝ (log‘2))
51	41, 49, 43, 19, 50	isumclim 15710	. . . 4 ⊢ (𝑁 ∈ ℕ0 → Σ𝑛 ∈ ℕ0 (2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) = (log‘2))
52	41, 22, 42, 43, 19, 40	isumsplit 15796	. . . 4 ⊢ (𝑁 ∈ ℕ0 → Σ𝑛 ∈ ℕ0 (2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) = (Σ𝑛 ∈ (0...(𝑁 − 1))(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) + Σ𝑛 ∈ (ℤ≥‘𝑁)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))))
53	51, 52	eqtr3d 2774	. . 3 ⊢ (𝑁 ∈ ℕ0 → (log‘2) = (Σ𝑛 ∈ (0...(𝑁 − 1))(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) + Σ𝑛 ∈ (ℤ≥‘𝑁)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))))
54	21, 48, 53	mvrladdd 11554	. 2 ⊢ (𝑁 ∈ ℕ0 → ((log‘2) − Σ𝑛 ∈ (0...(𝑁 − 1))(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))) = Σ𝑛 ∈ (ℤ≥‘𝑁)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))))
55	3	a1i 11	. . . . . 6 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → 2 ∈ ℝ)
56		0le2 12274	. . . . . . 7 ⊢ 0 ≤ 2
57	56	a1i 11	. . . . . 6 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → 0 ≤ 2)
58	16	nnred 12180	. . . . . 6 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)) ∈ ℝ)
59	16	nngt0d 12217	. . . . . 6 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → 0 < ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))
60		divge0 12016	. . . . . 6 ⊢ (((2 ∈ ℝ ∧ 0 ≤ 2) ∧ (((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)) ∈ ℝ ∧ 0 < ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))) → 0 ≤ (2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))))
61	55, 57, 58, 59, 60	syl22anc 839	. . . . 5 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → 0 ≤ (2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))))
62	24, 61	syldan 592	. . . 4 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → 0 ≤ (2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))))
63	22, 23, 34, 35, 46, 62	isumge0 15719	. . 3 ⊢ (𝑁 ∈ ℕ0 → 0 ≤ Σ𝑛 ∈ (ℤ≥‘𝑁)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))))
64		oveq2 7368	. . . . . . . . . 10 ⊢ (𝑘 = 𝑛 → ((1 / 9)↑𝑘) = ((1 / 9)↑𝑛))
65	64	oveq2d 7376	. . . . . . . . 9 ⊢ (𝑘 = 𝑛 → ((2 / (3 · ((2 · 𝑁) + 1))) · ((1 / 9)↑𝑘)) = ((2 / (3 · ((2 · 𝑁) + 1))) · ((1 / 9)↑𝑛)))
66		eqid 2737	. . . . . . . . 9 ⊢ (𝑘 ∈ ℕ0 ↦ ((2 / (3 · ((2 · 𝑁) + 1))) · ((1 / 9)↑𝑘))) = (𝑘 ∈ ℕ0 ↦ ((2 / (3 · ((2 · 𝑁) + 1))) · ((1 / 9)↑𝑘)))
67		ovex 7393	. . . . . . . . 9 ⊢ ((2 / (3 · ((2 · 𝑁) + 1))) · ((1 / 9)↑𝑛)) ∈ V
68	65, 66, 67	fvmpt 6941	. . . . . . . 8 ⊢ (𝑛 ∈ ℕ0 → ((𝑘 ∈ ℕ0 ↦ ((2 / (3 · ((2 · 𝑁) + 1))) · ((1 / 9)↑𝑘)))‘𝑛) = ((2 / (3 · ((2 · 𝑁) + 1))) · ((1 / 9)↑𝑛)))
69	68	adantl 481	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → ((𝑘 ∈ ℕ0 ↦ ((2 / (3 · ((2 · 𝑁) + 1))) · ((1 / 9)↑𝑘)))‘𝑛) = ((2 / (3 · ((2 · 𝑁) + 1))) · ((1 / 9)↑𝑛)))
70		9cn 12272	. . . . . . . . . . 11 ⊢ 9 ∈ ℂ
71	70	a1i 11	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → 9 ∈ ℂ)
72	13	nnne0i 12208	. . . . . . . . . . 11 ⊢ 9 ≠ 0
73	72	a1i 11	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → 9 ≠ 0)
74		nn0z 12539	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ℕ0 → 𝑛 ∈ ℤ)
75	74	adantl 481	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → 𝑛 ∈ ℤ)
76	71, 73, 75	exprecd 14107	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → ((1 / 9)↑𝑛) = (1 / (9↑𝑛)))
77	76	oveq2d 7376	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → ((2 / (3 · ((2 · 𝑁) + 1))) · ((1 / 9)↑𝑛)) = ((2 / (3 · ((2 · 𝑁) + 1))) · (1 / (9↑𝑛))))
78		nn0mulcl 12464	. . . . . . . . . . . . . . 15 ⊢ ((2 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (2 · 𝑁) ∈ ℕ0)
79	5, 78	mpan 691	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ ℕ0 → (2 · 𝑁) ∈ ℕ0)
80		nn0p1nn 12467	. . . . . . . . . . . . . 14 ⊢ ((2 · 𝑁) ∈ ℕ0 → ((2 · 𝑁) + 1) ∈ ℕ)
81	79, 80	syl 17	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ ℕ0 → ((2 · 𝑁) + 1) ∈ ℕ)
82		nnmulcl 12189	. . . . . . . . . . . . 13 ⊢ ((3 ∈ ℕ ∧ ((2 · 𝑁) + 1) ∈ ℕ) → (3 · ((2 · 𝑁) + 1)) ∈ ℕ)
83	4, 81, 82	sylancr 588	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℕ0 → (3 · ((2 · 𝑁) + 1)) ∈ ℕ)
84		nndivre 12209	. . . . . . . . . . . 12 ⊢ ((2 ∈ ℝ ∧ (3 · ((2 · 𝑁) + 1)) ∈ ℕ) → (2 / (3 · ((2 · 𝑁) + 1))) ∈ ℝ)
85	3, 83, 84	sylancr 588	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℕ0 → (2 / (3 · ((2 · 𝑁) + 1))) ∈ ℝ)
86	85	recnd 11164	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ0 → (2 / (3 · ((2 · 𝑁) + 1))) ∈ ℂ)
87	86	adantr 480	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → (2 / (3 · ((2 · 𝑁) + 1))) ∈ ℂ)
88	15	nncnd 12181	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → (9↑𝑛) ∈ ℂ)
89	15	nnne0d 12218	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → (9↑𝑛) ≠ 0)
90	87, 88, 89	divrecd 11925	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → ((2 / (3 · ((2 · 𝑁) + 1))) / (9↑𝑛)) = ((2 / (3 · ((2 · 𝑁) + 1))) · (1 / (9↑𝑛))))
91		2cnd 12250	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → 2 ∈ ℂ)
92	83	adantr 480	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → (3 · ((2 · 𝑁) + 1)) ∈ ℕ)
93	92	nncnd 12181	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → (3 · ((2 · 𝑁) + 1)) ∈ ℂ)
94	92	nnne0d 12218	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → (3 · ((2 · 𝑁) + 1)) ≠ 0)
95	91, 93, 88, 94, 89	divdiv1d 11953	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → ((2 / (3 · ((2 · 𝑁) + 1))) / (9↑𝑛)) = (2 / ((3 · ((2 · 𝑁) + 1)) · (9↑𝑛))))
96	77, 90, 95	3eqtr2d 2778	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → ((2 / (3 · ((2 · 𝑁) + 1))) · ((1 / 9)↑𝑛)) = (2 / ((3 · ((2 · 𝑁) + 1)) · (9↑𝑛))))
97	69, 96	eqtrd 2772	. . . . . 6 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → ((𝑘 ∈ ℕ0 ↦ ((2 / (3 · ((2 · 𝑁) + 1))) · ((1 / 9)↑𝑘)))‘𝑛) = (2 / ((3 · ((2 · 𝑁) + 1)) · (9↑𝑛))))
98	24, 97	syldan 592	. . . . 5 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → ((𝑘 ∈ ℕ0 ↦ ((2 / (3 · ((2 · 𝑁) + 1))) · ((1 / 9)↑𝑘)))‘𝑛) = (2 / ((3 · ((2 · 𝑁) + 1)) · (9↑𝑛))))
99	92, 15	nnmulcld 12221	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → ((3 · ((2 · 𝑁) + 1)) · (9↑𝑛)) ∈ ℕ)
100		nndivre 12209	. . . . . . 7 ⊢ ((2 ∈ ℝ ∧ ((3 · ((2 · 𝑁) + 1)) · (9↑𝑛)) ∈ ℕ) → (2 / ((3 · ((2 · 𝑁) + 1)) · (9↑𝑛))) ∈ ℝ)
101	3, 99, 100	sylancr 588	. . . . . 6 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → (2 / ((3 · ((2 · 𝑁) + 1)) · (9↑𝑛))) ∈ ℝ)
102	24, 101	syldan 592	. . . . 5 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (2 / ((3 · ((2 · 𝑁) + 1)) · (9↑𝑛))) ∈ ℝ)
103	79	adantr 480	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (2 · 𝑁) ∈ ℕ0)
104	103	nn0red 12490	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (2 · 𝑁) ∈ ℝ)
105	5, 24, 7	sylancr 588	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (2 · 𝑛) ∈ ℕ0)
106	105	nn0red 12490	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (2 · 𝑛) ∈ ℝ)
107		1red 11136	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → 1 ∈ ℝ)
108		eluzle 12792	. . . . . . . . . . 11 ⊢ (𝑛 ∈ (ℤ≥‘𝑁) → 𝑁 ≤ 𝑛)
109	108	adantl 481	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → 𝑁 ≤ 𝑛)
110		nn0re 12437	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℕ0 → 𝑁 ∈ ℝ)
111	110	adantr 480	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → 𝑁 ∈ ℝ)
112	24	nn0red 12490	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → 𝑛 ∈ ℝ)
113	3	a1i 11	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → 2 ∈ ℝ)
114		2pos 12275	. . . . . . . . . . . 12 ⊢ 0 < 2
115	114	a1i 11	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → 0 < 2)
116		lemul2 11999	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℝ ∧ 𝑛 ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → (𝑁 ≤ 𝑛 ↔ (2 · 𝑁) ≤ (2 · 𝑛)))
117	111, 112, 113, 115, 116	syl112anc 1377	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (𝑁 ≤ 𝑛 ↔ (2 · 𝑁) ≤ (2 · 𝑛)))
118	109, 117	mpbid 232	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (2 · 𝑁) ≤ (2 · 𝑛))
119	104, 106, 107, 118	leadd1dd 11755	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → ((2 · 𝑁) + 1) ≤ ((2 · 𝑛) + 1))
120	81	adantr 480	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → ((2 · 𝑁) + 1) ∈ ℕ)
121	120	nnred 12180	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → ((2 · 𝑁) + 1) ∈ ℝ)
122	24, 10	syldan 592	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → ((2 · 𝑛) + 1) ∈ ℕ)
123	122	nnred 12180	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → ((2 · 𝑛) + 1) ∈ ℝ)
124		3re 12252	. . . . . . . . . 10 ⊢ 3 ∈ ℝ
125	124	a1i 11	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → 3 ∈ ℝ)
126		3pos 12277	. . . . . . . . . 10 ⊢ 0 < 3
127	126	a1i 11	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → 0 < 3)
128		lemul2 11999	. . . . . . . . 9 ⊢ ((((2 · 𝑁) + 1) ∈ ℝ ∧ ((2 · 𝑛) + 1) ∈ ℝ ∧ (3 ∈ ℝ ∧ 0 < 3)) → (((2 · 𝑁) + 1) ≤ ((2 · 𝑛) + 1) ↔ (3 · ((2 · 𝑁) + 1)) ≤ (3 · ((2 · 𝑛) + 1))))
129	121, 123, 125, 127, 128	syl112anc 1377	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (((2 · 𝑁) + 1) ≤ ((2 · 𝑛) + 1) ↔ (3 · ((2 · 𝑁) + 1)) ≤ (3 · ((2 · 𝑛) + 1))))
130	119, 129	mpbid 232	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (3 · ((2 · 𝑁) + 1)) ≤ (3 · ((2 · 𝑛) + 1)))
131	83	adantr 480	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (3 · ((2 · 𝑁) + 1)) ∈ ℕ)
132	131	nnred 12180	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (3 · ((2 · 𝑁) + 1)) ∈ ℝ)
133	24, 12	syldan 592	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (3 · ((2 · 𝑛) + 1)) ∈ ℕ)
134	133	nnred 12180	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (3 · ((2 · 𝑛) + 1)) ∈ ℝ)
135	13, 24, 14	sylancr 588	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (9↑𝑛) ∈ ℕ)
136	135	nnred 12180	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (9↑𝑛) ∈ ℝ)
137	135	nngt0d 12217	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → 0 < (9↑𝑛))
138		lemul1 11998	. . . . . . . 8 ⊢ (((3 · ((2 · 𝑁) + 1)) ∈ ℝ ∧ (3 · ((2 · 𝑛) + 1)) ∈ ℝ ∧ ((9↑𝑛) ∈ ℝ ∧ 0 < (9↑𝑛))) → ((3 · ((2 · 𝑁) + 1)) ≤ (3 · ((2 · 𝑛) + 1)) ↔ ((3 · ((2 · 𝑁) + 1)) · (9↑𝑛)) ≤ ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))))
139	132, 134, 136, 137, 138	syl112anc 1377	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → ((3 · ((2 · 𝑁) + 1)) ≤ (3 · ((2 · 𝑛) + 1)) ↔ ((3 · ((2 · 𝑁) + 1)) · (9↑𝑛)) ≤ ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))))
140	130, 139	mpbid 232	. . . . . 6 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → ((3 · ((2 · 𝑁) + 1)) · (9↑𝑛)) ≤ ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))
141	24, 99	syldan 592	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → ((3 · ((2 · 𝑁) + 1)) · (9↑𝑛)) ∈ ℕ)
142	141	nnred 12180	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → ((3 · ((2 · 𝑁) + 1)) · (9↑𝑛)) ∈ ℝ)
143	141	nngt0d 12217	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → 0 < ((3 · ((2 · 𝑁) + 1)) · (9↑𝑛)))
144	24, 58	syldan 592	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)) ∈ ℝ)
145	24, 59	syldan 592	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → 0 < ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))
146		lediv2 12037	. . . . . . 7 ⊢ (((((3 · ((2 · 𝑁) + 1)) · (9↑𝑛)) ∈ ℝ ∧ 0 < ((3 · ((2 · 𝑁) + 1)) · (9↑𝑛))) ∧ (((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)) ∈ ℝ ∧ 0 < ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) ∧ (2 ∈ ℝ ∧ 0 < 2)) → (((3 · ((2 · 𝑁) + 1)) · (9↑𝑛)) ≤ ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)) ↔ (2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) ≤ (2 / ((3 · ((2 · 𝑁) + 1)) · (9↑𝑛)))))
147	142, 143, 144, 145, 113, 115, 146	syl222anc 1389	. . . . . 6 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (((3 · ((2 · 𝑁) + 1)) · (9↑𝑛)) ≤ ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)) ↔ (2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) ≤ (2 / ((3 · ((2 · 𝑁) + 1)) · (9↑𝑛)))))
148	140, 147	mpbid 232	. . . . 5 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) ≤ (2 / ((3 · ((2 · 𝑁) + 1)) · (9↑𝑛))))
149		9re 12271	. . . . . . . . . . . 12 ⊢ 9 ∈ ℝ
150	149, 72	rereccli 11911	. . . . . . . . . . 11 ⊢ (1 / 9) ∈ ℝ
151	150	recni 11150	. . . . . . . . . 10 ⊢ (1 / 9) ∈ ℂ
152	151	a1i 11	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ0 → (1 / 9) ∈ ℂ)
153		0re 11137	. . . . . . . . . . . . 13 ⊢ 0 ∈ ℝ
154		9pos 12285	. . . . . . . . . . . . . 14 ⊢ 0 < 9
155	149, 154	recgt0ii 12053	. . . . . . . . . . . . 13 ⊢ 0 < (1 / 9)
156	153, 150, 155	ltleii 11260	. . . . . . . . . . . 12 ⊢ 0 ≤ (1 / 9)
157		absid 15249	. . . . . . . . . . . 12 ⊢ (((1 / 9) ∈ ℝ ∧ 0 ≤ (1 / 9)) → (abs‘(1 / 9)) = (1 / 9))
158	150, 156, 157	mp2an 693	. . . . . . . . . . 11 ⊢ (abs‘(1 / 9)) = (1 / 9)
159		1lt9 12373	. . . . . . . . . . . . 13 ⊢ 1 < 9
160		recgt1i 12044	. . . . . . . . . . . . 13 ⊢ ((9 ∈ ℝ ∧ 1 < 9) → (0 < (1 / 9) ∧ (1 / 9) < 1))
161	149, 159, 160	mp2an 693	. . . . . . . . . . . 12 ⊢ (0 < (1 / 9) ∧ (1 / 9) < 1)
162	161	simpri 485	. . . . . . . . . . 11 ⊢ (1 / 9) < 1
163	158, 162	eqbrtri 5107	. . . . . . . . . 10 ⊢ (abs‘(1 / 9)) < 1
164	163	a1i 11	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ0 → (abs‘(1 / 9)) < 1)
165		eqid 2737	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℕ0 ↦ ((1 / 9)↑𝑘)) = (𝑘 ∈ ℕ0 ↦ ((1 / 9)↑𝑘))
166		ovex 7393	. . . . . . . . . . 11 ⊢ ((1 / 9)↑𝑛) ∈ V
167	64, 165, 166	fvmpt 6941	. . . . . . . . . 10 ⊢ (𝑛 ∈ ℕ0 → ((𝑘 ∈ ℕ0 ↦ ((1 / 9)↑𝑘))‘𝑛) = ((1 / 9)↑𝑛))
168	24, 167	syl 17	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → ((𝑘 ∈ ℕ0 ↦ ((1 / 9)↑𝑘))‘𝑛) = ((1 / 9)↑𝑛))
169	152, 164, 42, 168	geolim2 15827	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ0 → seq𝑁( + , (𝑘 ∈ ℕ0 ↦ ((1 / 9)↑𝑘))) ⇝ (((1 / 9)↑𝑁) / (1 − (1 / 9))))
170	70	a1i 11	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℕ0 → 9 ∈ ℂ)
171	72	a1i 11	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℕ0 → 9 ≠ 0)
172	170, 171, 23	exprecd 14107	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ0 → ((1 / 9)↑𝑁) = (1 / (9↑𝑁)))
173	70, 72	dividi 11879	. . . . . . . . . . . . 13 ⊢ (9 / 9) = 1
174	173	oveq1i 7370	. . . . . . . . . . . 12 ⊢ ((9 / 9) − (1 / 9)) = (1 − (1 / 9))
175		ax-1cn 11087	. . . . . . . . . . . . . 14 ⊢ 1 ∈ ℂ
176	70, 72	pm3.2i 470	. . . . . . . . . . . . . 14 ⊢ (9 ∈ ℂ ∧ 9 ≠ 0)
177		divsubdir 11839	. . . . . . . . . . . . . 14 ⊢ ((9 ∈ ℂ ∧ 1 ∈ ℂ ∧ (9 ∈ ℂ ∧ 9 ≠ 0)) → ((9 − 1) / 9) = ((9 / 9) − (1 / 9)))
178	70, 175, 176, 177	mp3an 1464	. . . . . . . . . . . . 13 ⊢ ((9 − 1) / 9) = ((9 / 9) − (1 / 9))
179		9m1e8 12301	. . . . . . . . . . . . . 14 ⊢ (9 − 1) = 8
180	179	oveq1i 7370	. . . . . . . . . . . . 13 ⊢ ((9 − 1) / 9) = (8 / 9)
181	178, 180	eqtr3i 2762	. . . . . . . . . . . 12 ⊢ ((9 / 9) − (1 / 9)) = (8 / 9)
182	174, 181	eqtr3i 2762	. . . . . . . . . . 11 ⊢ (1 − (1 / 9)) = (8 / 9)
183	182	a1i 11	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ0 → (1 − (1 / 9)) = (8 / 9))
184	172, 183	oveq12d 7378	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ0 → (((1 / 9)↑𝑁) / (1 − (1 / 9))) = ((1 / (9↑𝑁)) / (8 / 9)))
185	175	a1i 11	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ0 → 1 ∈ ℂ)
186		nnexpcl 14027	. . . . . . . . . . . 12 ⊢ ((9 ∈ ℕ ∧ 𝑁 ∈ ℕ0) → (9↑𝑁) ∈ ℕ)
187	13, 186	mpan 691	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℕ0 → (9↑𝑁) ∈ ℕ)
188	187	nncnd 12181	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ0 → (9↑𝑁) ∈ ℂ)
189		8cn 12269	. . . . . . . . . . . 12 ⊢ 8 ∈ ℂ
190	189, 70, 72	divcli 11888	. . . . . . . . . . 11 ⊢ (8 / 9) ∈ ℂ
191	190	a1i 11	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ0 → (8 / 9) ∈ ℂ)
192	187	nnne0d 12218	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ0 → (9↑𝑁) ≠ 0)
193		8nn 12267	. . . . . . . . . . . . 13 ⊢ 8 ∈ ℕ
194	193	nnne0i 12208	. . . . . . . . . . . 12 ⊢ 8 ≠ 0
195	189, 70, 194, 72	divne0i 11894	. . . . . . . . . . 11 ⊢ (8 / 9) ≠ 0
196	195	a1i 11	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ0 → (8 / 9) ≠ 0)
197	185, 188, 191, 192, 196	divdiv32d 11947	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ0 → ((1 / (9↑𝑁)) / (8 / 9)) = ((1 / (8 / 9)) / (9↑𝑁)))
198		recdiv 11852	. . . . . . . . . . . 12 ⊢ (((8 ∈ ℂ ∧ 8 ≠ 0) ∧ (9 ∈ ℂ ∧ 9 ≠ 0)) → (1 / (8 / 9)) = (9 / 8))
199	189, 194, 70, 72, 198	mp4an 694	. . . . . . . . . . 11 ⊢ (1 / (8 / 9)) = (9 / 8)
200	199	oveq1i 7370	. . . . . . . . . 10 ⊢ ((1 / (8 / 9)) / (9↑𝑁)) = ((9 / 8) / (9↑𝑁))
201	189	a1i 11	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℕ0 → 8 ∈ ℂ)
202	194	a1i 11	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℕ0 → 8 ≠ 0)
203	170, 201, 188, 202, 192	divdiv1d 11953	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ0 → ((9 / 8) / (9↑𝑁)) = (9 / (8 · (9↑𝑁))))
204	200, 203	eqtrid 2784	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ0 → ((1 / (8 / 9)) / (9↑𝑁)) = (9 / (8 · (9↑𝑁))))
205	184, 197, 204	3eqtrd 2776	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ0 → (((1 / 9)↑𝑁) / (1 − (1 / 9))) = (9 / (8 · (9↑𝑁))))
206	169, 205	breqtrd 5112	. . . . . . 7 ⊢ (𝑁 ∈ ℕ0 → seq𝑁( + , (𝑘 ∈ ℕ0 ↦ ((1 / 9)↑𝑘))) ⇝ (9 / (8 · (9↑𝑁))))
207		expcl 14032	. . . . . . . . 9 ⊢ (((1 / 9) ∈ ℂ ∧ 𝑛 ∈ ℕ0) → ((1 / 9)↑𝑛) ∈ ℂ)
208	151, 24, 207	sylancr 588	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → ((1 / 9)↑𝑛) ∈ ℂ)
209	168, 208	eqeltrd 2837	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → ((𝑘 ∈ ℕ0 ↦ ((1 / 9)↑𝑘))‘𝑛) ∈ ℂ)
210	24, 68	syl 17	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → ((𝑘 ∈ ℕ0 ↦ ((2 / (3 · ((2 · 𝑁) + 1))) · ((1 / 9)↑𝑘)))‘𝑛) = ((2 / (3 · ((2 · 𝑁) + 1))) · ((1 / 9)↑𝑛)))
211	168	oveq2d 7376	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → ((2 / (3 · ((2 · 𝑁) + 1))) · ((𝑘 ∈ ℕ0 ↦ ((1 / 9)↑𝑘))‘𝑛)) = ((2 / (3 · ((2 · 𝑁) + 1))) · ((1 / 9)↑𝑛)))
212	210, 211	eqtr4d 2775	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → ((𝑘 ∈ ℕ0 ↦ ((2 / (3 · ((2 · 𝑁) + 1))) · ((1 / 9)↑𝑘)))‘𝑛) = ((2 / (3 · ((2 · 𝑁) + 1))) · ((𝑘 ∈ ℕ0 ↦ ((1 / 9)↑𝑘))‘𝑛)))
213	22, 23, 86, 206, 209, 212	isermulc2 15611	. . . . . 6 ⊢ (𝑁 ∈ ℕ0 → seq𝑁( + , (𝑘 ∈ ℕ0 ↦ ((2 / (3 · ((2 · 𝑁) + 1))) · ((1 / 9)↑𝑘)))) ⇝ ((2 / (3 · ((2 · 𝑁) + 1))) · (9 / (8 · (9↑𝑁)))))
214		seqex 13956	. . . . . . 7 ⊢ seq𝑁( + , (𝑘 ∈ ℕ0 ↦ ((2 / (3 · ((2 · 𝑁) + 1))) · ((1 / 9)↑𝑘)))) ∈ V
215		ovex 7393	. . . . . . 7 ⊢ ((2 / (3 · ((2 · 𝑁) + 1))) · (9 / (8 · (9↑𝑁)))) ∈ V
216	214, 215	breldm 5857	. . . . . 6 ⊢ (seq𝑁( + , (𝑘 ∈ ℕ0 ↦ ((2 / (3 · ((2 · 𝑁) + 1))) · ((1 / 9)↑𝑘)))) ⇝ ((2 / (3 · ((2 · 𝑁) + 1))) · (9 / (8 · (9↑𝑁)))) → seq𝑁( + , (𝑘 ∈ ℕ0 ↦ ((2 / (3 · ((2 · 𝑁) + 1))) · ((1 / 9)↑𝑘)))) ∈ dom ⇝ )
217	213, 216	syl 17	. . . . 5 ⊢ (𝑁 ∈ ℕ0 → seq𝑁( + , (𝑘 ∈ ℕ0 ↦ ((2 / (3 · ((2 · 𝑁) + 1))) · ((1 / 9)↑𝑘)))) ∈ dom ⇝ )
218	22, 23, 34, 35, 98, 102, 148, 46, 217	isumle 15800	. . . 4 ⊢ (𝑁 ∈ ℕ0 → Σ𝑛 ∈ (ℤ≥‘𝑁)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) ≤ Σ𝑛 ∈ (ℤ≥‘𝑁)(2 / ((3 · ((2 · 𝑁) + 1)) · (9↑𝑛))))
219	102	recnd 11164	. . . . 5 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (2 / ((3 · ((2 · 𝑁) + 1)) · (9↑𝑛))) ∈ ℂ)
220		3cn 12253	. . . . . . . . . . . 12 ⊢ 3 ∈ ℂ
221		4cn 12257	. . . . . . . . . . . 12 ⊢ 4 ∈ ℂ
222		2cn 12247	. . . . . . . . . . . 12 ⊢ 2 ∈ ℂ
223		4ne0 12280	. . . . . . . . . . . 12 ⊢ 4 ≠ 0
224		3ne0 12278	. . . . . . . . . . . 12 ⊢ 3 ≠ 0
225		2ne0 12276	. . . . . . . . . . . 12 ⊢ 2 ≠ 0
226	220, 221, 222, 220, 223, 224, 225	divdivdivi 11909	. . . . . . . . . . 11 ⊢ ((3 / 4) / (2 / 3)) = ((3 · 3) / (4 · 2))
227		3t3e9 12334	. . . . . . . . . . . 12 ⊢ (3 · 3) = 9
228		4t2e8 12335	. . . . . . . . . . . 12 ⊢ (4 · 2) = 8
229	227, 228	oveq12i 7372	. . . . . . . . . . 11 ⊢ ((3 · 3) / (4 · 2)) = (9 / 8)
230	226, 229	eqtri 2760	. . . . . . . . . 10 ⊢ ((3 / 4) / (2 / 3)) = (9 / 8)
231	230	oveq2i 7371	. . . . . . . . 9 ⊢ ((2 / 3) · ((3 / 4) / (2 / 3))) = ((2 / 3) · (9 / 8))
232	220, 221, 223	divcli 11888	. . . . . . . . . 10 ⊢ (3 / 4) ∈ ℂ
233	222, 220, 224	divcli 11888	. . . . . . . . . 10 ⊢ (2 / 3) ∈ ℂ
234	222, 220, 225, 224	divne0i 11894	. . . . . . . . . 10 ⊢ (2 / 3) ≠ 0
235	232, 233, 234	divcan2i 11889	. . . . . . . . 9 ⊢ ((2 / 3) · ((3 / 4) / (2 / 3))) = (3 / 4)
236	231, 235	eqtr3i 2762	. . . . . . . 8 ⊢ ((2 / 3) · (9 / 8)) = (3 / 4)
237	236	oveq1i 7370	. . . . . . 7 ⊢ (((2 / 3) · (9 / 8)) / (((2 · 𝑁) + 1) · (9↑𝑁))) = ((3 / 4) / (((2 · 𝑁) + 1) · (9↑𝑁)))
238		2cnd 12250	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ0 → 2 ∈ ℂ)
239	220	a1i 11	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ0 → 3 ∈ ℂ)
240	81	nncnd 12181	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ0 → ((2 · 𝑁) + 1) ∈ ℂ)
241	224	a1i 11	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ0 → 3 ≠ 0)
242	81	nnne0d 12218	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ0 → ((2 · 𝑁) + 1) ≠ 0)
243	238, 239, 240, 241, 242	divdiv1d 11953	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ0 → ((2 / 3) / ((2 · 𝑁) + 1)) = (2 / (3 · ((2 · 𝑁) + 1))))
244	243, 203	oveq12d 7378	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ0 → (((2 / 3) / ((2 · 𝑁) + 1)) · ((9 / 8) / (9↑𝑁))) = ((2 / (3 · ((2 · 𝑁) + 1))) · (9 / (8 · (9↑𝑁)))))
245	233	a1i 11	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ0 → (2 / 3) ∈ ℂ)
246	70, 189, 194	divcli 11888	. . . . . . . . . 10 ⊢ (9 / 8) ∈ ℂ
247	246	a1i 11	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ0 → (9 / 8) ∈ ℂ)
248	245, 240, 247, 188, 242, 192	divmuldivd 11963	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ0 → (((2 / 3) / ((2 · 𝑁) + 1)) · ((9 / 8) / (9↑𝑁))) = (((2 / 3) · (9 / 8)) / (((2 · 𝑁) + 1) · (9↑𝑁))))
249	244, 248	eqtr3d 2774	. . . . . . 7 ⊢ (𝑁 ∈ ℕ0 → ((2 / (3 · ((2 · 𝑁) + 1))) · (9 / (8 · (9↑𝑁)))) = (((2 / 3) · (9 / 8)) / (((2 · 𝑁) + 1) · (9↑𝑁))))
250	221	a1i 11	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ0 → 4 ∈ ℂ)
251	250, 240, 188	mulassd 11159	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ0 → ((4 · ((2 · 𝑁) + 1)) · (9↑𝑁)) = (4 · (((2 · 𝑁) + 1) · (9↑𝑁))))
252	251	oveq2d 7376	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ0 → (3 / ((4 · ((2 · 𝑁) + 1)) · (9↑𝑁))) = (3 / (4 · (((2 · 𝑁) + 1) · (9↑𝑁)))))
253	81, 187	nnmulcld 12221	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ0 → (((2 · 𝑁) + 1) · (9↑𝑁)) ∈ ℕ)
254	253	nncnd 12181	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ0 → (((2 · 𝑁) + 1) · (9↑𝑁)) ∈ ℂ)
255	223	a1i 11	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ0 → 4 ≠ 0)
256	253	nnne0d 12218	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ0 → (((2 · 𝑁) + 1) · (9↑𝑁)) ≠ 0)
257	239, 250, 254, 255, 256	divdiv1d 11953	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ0 → ((3 / 4) / (((2 · 𝑁) + 1) · (9↑𝑁))) = (3 / (4 · (((2 · 𝑁) + 1) · (9↑𝑁)))))
258	252, 257	eqtr4d 2775	. . . . . . 7 ⊢ (𝑁 ∈ ℕ0 → (3 / ((4 · ((2 · 𝑁) + 1)) · (9↑𝑁))) = ((3 / 4) / (((2 · 𝑁) + 1) · (9↑𝑁))))
259	237, 249, 258	3eqtr4a 2798	. . . . . 6 ⊢ (𝑁 ∈ ℕ0 → ((2 / (3 · ((2 · 𝑁) + 1))) · (9 / (8 · (9↑𝑁)))) = (3 / ((4 · ((2 · 𝑁) + 1)) · (9↑𝑁))))
260	213, 259	breqtrd 5112	. . . . 5 ⊢ (𝑁 ∈ ℕ0 → seq𝑁( + , (𝑘 ∈ ℕ0 ↦ ((2 / (3 · ((2 · 𝑁) + 1))) · ((1 / 9)↑𝑘)))) ⇝ (3 / ((4 · ((2 · 𝑁) + 1)) · (9↑𝑁))))
261	22, 23, 98, 219, 260	isumclim 15710	. . . 4 ⊢ (𝑁 ∈ ℕ0 → Σ𝑛 ∈ (ℤ≥‘𝑁)(2 / ((3 · ((2 · 𝑁) + 1)) · (9↑𝑛))) = (3 / ((4 · ((2 · 𝑁) + 1)) · (9↑𝑁))))
262	218, 261	breqtrd 5112	. . 3 ⊢ (𝑁 ∈ ℕ0 → Σ𝑛 ∈ (ℤ≥‘𝑁)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) ≤ (3 / ((4 · ((2 · 𝑁) + 1)) · (9↑𝑁))))
263		4nn 12255	. . . . . . 7 ⊢ 4 ∈ ℕ
264		nnmulcl 12189	. . . . . . 7 ⊢ ((4 ∈ ℕ ∧ ((2 · 𝑁) + 1) ∈ ℕ) → (4 · ((2 · 𝑁) + 1)) ∈ ℕ)
265	263, 81, 264	sylancr 588	. . . . . 6 ⊢ (𝑁 ∈ ℕ0 → (4 · ((2 · 𝑁) + 1)) ∈ ℕ)
266	265, 187	nnmulcld 12221	. . . . 5 ⊢ (𝑁 ∈ ℕ0 → ((4 · ((2 · 𝑁) + 1)) · (9↑𝑁)) ∈ ℕ)
267		nndivre 12209	. . . . 5 ⊢ ((3 ∈ ℝ ∧ ((4 · ((2 · 𝑁) + 1)) · (9↑𝑁)) ∈ ℕ) → (3 / ((4 · ((2 · 𝑁) + 1)) · (9↑𝑁))) ∈ ℝ)
268	124, 266, 267	sylancr 588	. . . 4 ⊢ (𝑁 ∈ ℕ0 → (3 / ((4 · ((2 · 𝑁) + 1)) · (9↑𝑁))) ∈ ℝ)
269		elicc2 13355	. . . 4 ⊢ ((0 ∈ ℝ ∧ (3 / ((4 · ((2 · 𝑁) + 1)) · (9↑𝑁))) ∈ ℝ) → (Σ𝑛 ∈ (ℤ≥‘𝑁)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) ∈ (0[,](3 / ((4 · ((2 · 𝑁) + 1)) · (9↑𝑁)))) ↔ (Σ𝑛 ∈ (ℤ≥‘𝑁)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) ∈ ℝ ∧ 0 ≤ Σ𝑛 ∈ (ℤ≥‘𝑁)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) ∧ Σ𝑛 ∈ (ℤ≥‘𝑁)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) ≤ (3 / ((4 · ((2 · 𝑁) + 1)) · (9↑𝑁))))))
270	153, 268, 269	sylancr 588	. . 3 ⊢ (𝑁 ∈ ℕ0 → (Σ𝑛 ∈ (ℤ≥‘𝑁)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) ∈ (0[,](3 / ((4 · ((2 · 𝑁) + 1)) · (9↑𝑁)))) ↔ (Σ𝑛 ∈ (ℤ≥‘𝑁)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) ∈ ℝ ∧ 0 ≤ Σ𝑛 ∈ (ℤ≥‘𝑁)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) ∧ Σ𝑛 ∈ (ℤ≥‘𝑁)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) ≤ (3 / ((4 · ((2 · 𝑁) + 1)) · (9↑𝑁))))))
271	47, 63, 262, 270	mpbir3and 1344	. 2 ⊢ (𝑁 ∈ ℕ0 → Σ𝑛 ∈ (ℤ≥‘𝑁)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) ∈ (0[,](3 / ((4 · ((2 · 𝑁) + 1)) · (9↑𝑁)))))
272	54, 271	eqeltrd 2837	1 ⊢ (𝑁 ∈ ℕ0 → ((log‘2) − Σ𝑛 ∈ (0...(𝑁 − 1))(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))) ∈ (0[,](3 / ((4 · ((2 · 𝑁) + 1)) · (9↑𝑁)))))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1087   = wceq 1542   ∈ wcel 2114   ≠ wne 2933   class class class wbr 5086   ↦ cmpt 5167  dom cdm 5624  ‘cfv 6492  (class class class)co 7360  ℂcc 11027  ℝcr 11028  0cc0 11029  1c1 11030   + caddc 11032   · cmul 11034   < clt 11170   ≤ cle 11171   − cmin 11368   / cdiv 11798  ℕcn 12165  2c2 12227  3c3 12228  4c4 12229  8c8 12233  9c9 12234  ℕ₀cn0 12428  ℤcz 12515  ℤ_≥cuz 12779  [,]cicc 13292  ...cfz 13452  seqcseq 13954  ↑cexp 14014  abscabs 15187   ⇝ cli 15437  Σcsu 15639  logclog 26531

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-rep 5212  ax-sep 5231  ax-nul 5241  ax-pow 5302  ax-pr 5370  ax-un 7682  ax-inf2 9553  ax-cnex 11085  ax-resscn 11086  ax-1cn 11087  ax-icn 11088  ax-addcl 11089  ax-addrcl 11090  ax-mulcl 11091  ax-mulrcl 11092  ax-mulcom 11093  ax-addass 11094  ax-mulass 11095  ax-distr 11096  ax-i2m1 11097  ax-1ne0 11098  ax-1rid 11099  ax-rnegex 11100  ax-rrecex 11101  ax-cnre 11102  ax-pre-lttri 11103  ax-pre-lttrn 11104  ax-pre-ltadd 11105  ax-pre-mulgt0 11106  ax-pre-sup 11107  ax-addf 11108

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-rmo 3343  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-tp 4573  df-op 4575  df-uni 4852  df-int 4891  df-iun 4936  df-iin 4937  df-br 5087  df-opab 5149  df-mpt 5168  df-tr 5194  df-id 5519  df-eprel 5524  df-po 5532  df-so 5533  df-fr 5577  df-se 5578  df-we 5579  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-pred 6259  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-isom 6501  df-riota 7317  df-ov 7363  df-oprab 7364  df-mpo 7365  df-of 7624  df-om 7811  df-1st 7935  df-2nd 7936  df-supp 8104  df-frecs 8224  df-wrecs 8255  df-recs 8304  df-rdg 8342  df-1o 8398  df-2o 8399  df-oadd 8402  df-er 8636  df-map 8768  df-pm 8769  df-ixp 8839  df-en 8887  df-dom 8888  df-sdom 8889  df-fin 8890  df-fsupp 9268  df-fi 9317  df-sup 9348  df-inf 9349  df-oi 9418  df-card 9854  df-pnf 11172  df-mnf 11173  df-xr 11174  df-ltxr 11175  df-le 11176  df-sub 11370  df-neg 11371  df-div 11799  df-nn 12166  df-2 12235  df-3 12236  df-4 12237  df-5 12238  df-6 12239  df-7 12240  df-8 12241  df-9 12242  df-n0 12429  df-xnn0 12502  df-z 12516  df-dec 12636  df-uz 12780  df-q 12890  df-rp 12934  df-xneg 13054  df-xadd 13055  df-xmul 13056  df-ioo 13293  df-ioc 13294  df-ico 13295  df-icc 13296  df-fz 13453  df-fzo 13600  df-fl 13742  df-mod 13820  df-seq 13955  df-exp 14015  df-fac 14227  df-bc 14256  df-hash 14284  df-shft 15020  df-cj 15052  df-re 15053  df-im 15054  df-sqrt 15188  df-abs 15189  df-limsup 15424  df-clim 15441  df-rlim 15442  df-sum 15640  df-ef 16023  df-sin 16025  df-cos 16026  df-tan 16027  df-pi 16028  df-dvds 16213  df-struct 17108  df-sets 17125  df-slot 17143  df-ndx 17155  df-base 17171  df-ress 17192  df-plusg 17224  df-mulr 17225  df-starv 17226  df-sca 17227  df-vsca 17228  df-ip 17229  df-tset 17230  df-ple 17231  df-ds 17233  df-unif 17234  df-hom 17235  df-cco 17236  df-rest 17376  df-topn 17377  df-0g 17395  df-gsum 17396  df-topgen 17397  df-pt 17398  df-prds 17401  df-xrs 17457  df-qtop 17462  df-imas 17463  df-xps 17465  df-mre 17539  df-mrc 17540  df-acs 17542  df-mgm 18599  df-sgrp 18678  df-mnd 18694  df-submnd 18743  df-mulg 19035  df-cntz 19283  df-cmn 19748  df-psmet 21336  df-xmet 21337  df-met 21338  df-bl 21339  df-mopn 21340  df-fbas 21341  df-fg 21342  df-cnfld 21345  df-top 22869  df-topon 22886  df-topsp 22908  df-bases 22921  df-cld 22994  df-ntr 22995  df-cls 22996  df-nei 23073  df-lp 23111  df-perf 23112  df-cn 23202  df-cnp 23203  df-haus 23290  df-cmp 23362  df-tx 23537  df-hmeo 23730  df-fil 23821  df-fm 23913  df-flim 23914  df-flf 23915  df-xms 24295  df-ms 24296  df-tms 24297  df-cncf 24855  df-limc 25843  df-dv 25844  df-ulm 26355  df-log 26533  df-atan 26844

This theorem is referenced by:  log2ub  26926