Theorem log2tlbnd 26923

Description: Bound the error term in the series of log2cnv 26922. (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 13908	. . . 4 ⊢ (𝑁 ∈ ℕ0 → (0...(𝑁 − 1)) ∈ Fin)
2		elfznn0 13548	. . . . 5 ⊢ (𝑛 ∈ (0...(𝑁 − 1)) → 𝑛 ∈ ℕ0)
3		2re 12231	. . . . . . 7 ⊢ 2 ∈ ℝ
4		3nn 12236	. . . . . . . . 9 ⊢ 3 ∈ ℕ
5		2nn0 12430	. . . . . . . . . . 11 ⊢ 2 ∈ ℕ0
6		simpr 484	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → 𝑛 ∈ ℕ0)
7		nn0mulcl 12449	. . . . . . . . . . 11 ⊢ ((2 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → (2 · 𝑛) ∈ ℕ0)
8	5, 6, 7	sylancr 588	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → (2 · 𝑛) ∈ ℕ0)
9		nn0p1nn 12452	. . . . . . . . . 10 ⊢ ((2 · 𝑛) ∈ ℕ0 → ((2 · 𝑛) + 1) ∈ ℕ)
10	8, 9	syl 17	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → ((2 · 𝑛) + 1) ∈ ℕ)
11		nnmulcl 12181	. . . . . . . . 9 ⊢ ((3 ∈ ℕ ∧ ((2 · 𝑛) + 1) ∈ ℕ) → (3 · ((2 · 𝑛) + 1)) ∈ ℕ)
12	4, 10, 11	sylancr 588	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → (3 · ((2 · 𝑛) + 1)) ∈ ℕ)
13		9nn 12255	. . . . . . . . 9 ⊢ 9 ∈ ℕ
14		nnexpcl 14009	. . . . . . . . 9 ⊢ ((9 ∈ ℕ ∧ 𝑛 ∈ ℕ0) → (9↑𝑛) ∈ ℕ)
15	13, 6, 14	sylancr 588	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → (9↑𝑛) ∈ ℕ)
16	12, 15	nnmulcld 12210	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)) ∈ ℕ)
17		nndivre 12198	. . . . . . 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 11172	. . . . 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 15668	. . 3 ⊢ (𝑁 ∈ ℕ0 → Σ𝑛 ∈ (0...(𝑁 − 1))(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) ∈ ℂ)
22		eqid 2737	. . . . 5 ⊢ (ℤ≥‘𝑁) = (ℤ≥‘𝑁)
23		nn0z 12524	. . . . 5 ⊢ (𝑁 ∈ ℕ0 → 𝑁 ∈ ℤ)
24		eluznn0 12842	. . . . . 6 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → 𝑛 ∈ ℕ0)
25		oveq2 7376	. . . . . . . . . . 11 ⊢ (𝑘 = 𝑛 → (2 · 𝑘) = (2 · 𝑛))
26	25	oveq1d 7383	. . . . . . . . . 10 ⊢ (𝑘 = 𝑛 → ((2 · 𝑘) + 1) = ((2 · 𝑛) + 1))
27	26	oveq2d 7384	. . . . . . . . 9 ⊢ (𝑘 = 𝑛 → (3 · ((2 · 𝑘) + 1)) = (3 · ((2 · 𝑛) + 1)))
28		oveq2 7376	. . . . . . . . 9 ⊢ (𝑘 = 𝑛 → (9↑𝑘) = (9↑𝑛))
29	27, 28	oveq12d 7386	. . . . . . . 8 ⊢ (𝑘 = 𝑛 → ((3 · ((2 · 𝑘) + 1)) · (9↑𝑘)) = ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))
30	29	oveq2d 7384	. . . . . . 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 7401	. . . . . . 7 ⊢ (2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) ∈ V
33	30, 31, 32	fvmpt 6949	. . . . . 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 26922	. . . . . . 7 ⊢ seq0( + , (𝑘 ∈ ℕ0 ↦ (2 / ((3 · ((2 · 𝑘) + 1)) · (9↑𝑘))))) ⇝ (log‘2)
37		seqex 13938	. . . . . . . 8 ⊢ seq0( + , (𝑘 ∈ ℕ0 ↦ (2 / ((3 · ((2 · 𝑘) + 1)) · (9↑𝑘))))) ∈ V
38		fvex 6855	. . . . . . . 8 ⊢ (log‘2) ∈ V
39	37, 38	breldm 5865	. . . . . . 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 12801	. . . . . . 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 15592	. . . . . 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 15700	. . . 4 ⊢ (𝑁 ∈ ℕ0 → Σ𝑛 ∈ (ℤ≥‘𝑁)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) ∈ ℝ)
48	47	recnd 11172	. . 3 ⊢ (𝑁 ∈ ℕ0 → Σ𝑛 ∈ (ℤ≥‘𝑁)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) ∈ ℂ)
49		0zd 12512	. . . . 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 15692	. . . 4 ⊢ (𝑁 ∈ ℕ0 → Σ𝑛 ∈ ℕ0 (2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) = (log‘2))
52	41, 22, 42, 43, 19, 40	isumsplit 15775	. . . 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 11562	. 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 12259	. . . . . . 7 ⊢ 0 ≤ 2
57	56	a1i 11	. . . . . 6 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → 0 ≤ 2)
58	16	nnred 12172	. . . . . 6 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)) ∈ ℝ)
59	16	nngt0d 12206	. . . . . 6 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → 0 < ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))
60		divge0 12023	. . . . . 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 15701	. . 3 ⊢ (𝑁 ∈ ℕ0 → 0 ≤ Σ𝑛 ∈ (ℤ≥‘𝑁)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))))
64		oveq2 7376	. . . . . . . . . 10 ⊢ (𝑘 = 𝑛 → ((1 / 9)↑𝑘) = ((1 / 9)↑𝑛))
65	64	oveq2d 7384	. . . . . . . . 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 7401	. . . . . . . . 9 ⊢ ((2 / (3 · ((2 · 𝑁) + 1))) · ((1 / 9)↑𝑛)) ∈ V
68	65, 66, 67	fvmpt 6949	. . . . . . . 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 12257	. . . . . . . . . . 11 ⊢ 9 ∈ ℂ
71	70	a1i 11	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → 9 ∈ ℂ)
72	13	nnne0i 12197	. . . . . . . . . . 11 ⊢ 9 ≠ 0
73	72	a1i 11	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → 9 ≠ 0)
74		nn0z 12524	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ℕ0 → 𝑛 ∈ ℤ)
75	74	adantl 481	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → 𝑛 ∈ ℤ)
76	71, 73, 75	exprecd 14089	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → ((1 / 9)↑𝑛) = (1 / (9↑𝑛)))
77	76	oveq2d 7384	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → ((2 / (3 · ((2 · 𝑁) + 1))) · ((1 / 9)↑𝑛)) = ((2 / (3 · ((2 · 𝑁) + 1))) · (1 / (9↑𝑛))))
78		nn0mulcl 12449	. . . . . . . . . . . . . . 15 ⊢ ((2 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (2 · 𝑁) ∈ ℕ0)
79	5, 78	mpan 691	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ ℕ0 → (2 · 𝑁) ∈ ℕ0)
80		nn0p1nn 12452	. . . . . . . . . . . . . 14 ⊢ ((2 · 𝑁) ∈ ℕ0 → ((2 · 𝑁) + 1) ∈ ℕ)
81	79, 80	syl 17	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ ℕ0 → ((2 · 𝑁) + 1) ∈ ℕ)
82		nnmulcl 12181	. . . . . . . . . . . . 13 ⊢ ((3 ∈ ℕ ∧ ((2 · 𝑁) + 1) ∈ ℕ) → (3 · ((2 · 𝑁) + 1)) ∈ ℕ)
83	4, 81, 82	sylancr 588	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℕ0 → (3 · ((2 · 𝑁) + 1)) ∈ ℕ)
84		nndivre 12198	. . . . . . . . . . . 12 ⊢ ((2 ∈ ℝ ∧ (3 · ((2 · 𝑁) + 1)) ∈ ℕ) → (2 / (3 · ((2 · 𝑁) + 1))) ∈ ℝ)
85	3, 83, 84	sylancr 588	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℕ0 → (2 / (3 · ((2 · 𝑁) + 1))) ∈ ℝ)
86	85	recnd 11172	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ0 → (2 / (3 · ((2 · 𝑁) + 1))) ∈ ℂ)
87	86	adantr 480	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → (2 / (3 · ((2 · 𝑁) + 1))) ∈ ℂ)
88	15	nncnd 12173	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → (9↑𝑛) ∈ ℂ)
89	15	nnne0d 12207	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → (9↑𝑛) ≠ 0)
90	87, 88, 89	divrecd 11932	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → ((2 / (3 · ((2 · 𝑁) + 1))) / (9↑𝑛)) = ((2 / (3 · ((2 · 𝑁) + 1))) · (1 / (9↑𝑛))))
91		2cnd 12235	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → 2 ∈ ℂ)
92	83	adantr 480	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → (3 · ((2 · 𝑁) + 1)) ∈ ℕ)
93	92	nncnd 12173	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → (3 · ((2 · 𝑁) + 1)) ∈ ℂ)
94	92	nnne0d 12207	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → (3 · ((2 · 𝑁) + 1)) ≠ 0)
95	91, 93, 88, 94, 89	divdiv1d 11960	. . . . . . . 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 12210	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → ((3 · ((2 · 𝑁) + 1)) · (9↑𝑛)) ∈ ℕ)
100		nndivre 12198	. . . . . . 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 12475	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (2 · 𝑁) ∈ ℝ)
105	5, 24, 7	sylancr 588	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (2 · 𝑛) ∈ ℕ0)
106	105	nn0red 12475	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (2 · 𝑛) ∈ ℝ)
107		1red 11145	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → 1 ∈ ℝ)
108		eluzle 12776	. . . . . . . . . . 11 ⊢ (𝑛 ∈ (ℤ≥‘𝑁) → 𝑁 ≤ 𝑛)
109	108	adantl 481	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → 𝑁 ≤ 𝑛)
110		nn0re 12422	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℕ0 → 𝑁 ∈ ℝ)
111	110	adantr 480	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → 𝑁 ∈ ℝ)
112	24	nn0red 12475	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → 𝑛 ∈ ℝ)
113	3	a1i 11	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → 2 ∈ ℝ)
114		2pos 12260	. . . . . . . . . . . 12 ⊢ 0 < 2
115	114	a1i 11	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → 0 < 2)
116		lemul2 12006	. . . . . . . . . . 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 11763	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → ((2 · 𝑁) + 1) ≤ ((2 · 𝑛) + 1))
120	81	adantr 480	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → ((2 · 𝑁) + 1) ∈ ℕ)
121	120	nnred 12172	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → ((2 · 𝑁) + 1) ∈ ℝ)
122	24, 10	syldan 592	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → ((2 · 𝑛) + 1) ∈ ℕ)
123	122	nnred 12172	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → ((2 · 𝑛) + 1) ∈ ℝ)
124		3re 12237	. . . . . . . . . 10 ⊢ 3 ∈ ℝ
125	124	a1i 11	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → 3 ∈ ℝ)
126		3pos 12262	. . . . . . . . . 10 ⊢ 0 < 3
127	126	a1i 11	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → 0 < 3)
128		lemul2 12006	. . . . . . . . 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 12172	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (3 · ((2 · 𝑁) + 1)) ∈ ℝ)
133	24, 12	syldan 592	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (3 · ((2 · 𝑛) + 1)) ∈ ℕ)
134	133	nnred 12172	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (3 · ((2 · 𝑛) + 1)) ∈ ℝ)
135	13, 24, 14	sylancr 588	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (9↑𝑛) ∈ ℕ)
136	135	nnred 12172	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (9↑𝑛) ∈ ℝ)
137	135	nngt0d 12206	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → 0 < (9↑𝑛))
138		lemul1 12005	. . . . . . . 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 12172	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → ((3 · ((2 · 𝑁) + 1)) · (9↑𝑛)) ∈ ℝ)
143	141	nngt0d 12206	. . . . . . 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 12044	. . . . . . 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 12256	. . . . . . . . . . . 12 ⊢ 9 ∈ ℝ
150	149, 72	rereccli 11918	. . . . . . . . . . 11 ⊢ (1 / 9) ∈ ℝ
151	150	recni 11158	. . . . . . . . . 10 ⊢ (1 / 9) ∈ ℂ
152	151	a1i 11	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ0 → (1 / 9) ∈ ℂ)
153		0re 11146	. . . . . . . . . . . . 13 ⊢ 0 ∈ ℝ
154		9pos 12270	. . . . . . . . . . . . . 14 ⊢ 0 < 9
155	149, 154	recgt0ii 12060	. . . . . . . . . . . . 13 ⊢ 0 < (1 / 9)
156	153, 150, 155	ltleii 11268	. . . . . . . . . . . 12 ⊢ 0 ≤ (1 / 9)
157		absid 15231	. . . . . . . . . . . 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 12358	. . . . . . . . . . . . 13 ⊢ 1 < 9
160		recgt1i 12051	. . . . . . . . . . . . 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 5121	. . . . . . . . . 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 7401	. . . . . . . . . . 11 ⊢ ((1 / 9)↑𝑛) ∈ V
167	64, 165, 166	fvmpt 6949	. . . . . . . . . 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 15806	. . . . . . . 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 14089	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ0 → ((1 / 9)↑𝑁) = (1 / (9↑𝑁)))
173	70, 72	dividi 11886	. . . . . . . . . . . . 13 ⊢ (9 / 9) = 1
174	173	oveq1i 7378	. . . . . . . . . . . 12 ⊢ ((9 / 9) − (1 / 9)) = (1 − (1 / 9))
175		ax-1cn 11096	. . . . . . . . . . . . . 14 ⊢ 1 ∈ ℂ
176	70, 72	pm3.2i 470	. . . . . . . . . . . . . 14 ⊢ (9 ∈ ℂ ∧ 9 ≠ 0)
177		divsubdir 11847	. . . . . . . . . . . . . 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 12286	. . . . . . . . . . . . . 14 ⊢ (9 − 1) = 8
180	179	oveq1i 7378	. . . . . . . . . . . . 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 7386	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ0 → (((1 / 9)↑𝑁) / (1 − (1 / 9))) = ((1 / (9↑𝑁)) / (8 / 9)))
185	175	a1i 11	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ0 → 1 ∈ ℂ)
186		nnexpcl 14009	. . . . . . . . . . . 12 ⊢ ((9 ∈ ℕ ∧ 𝑁 ∈ ℕ0) → (9↑𝑁) ∈ ℕ)
187	13, 186	mpan 691	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℕ0 → (9↑𝑁) ∈ ℕ)
188	187	nncnd 12173	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ0 → (9↑𝑁) ∈ ℂ)
189		8cn 12254	. . . . . . . . . . . 12 ⊢ 8 ∈ ℂ
190	189, 70, 72	divcli 11895	. . . . . . . . . . 11 ⊢ (8 / 9) ∈ ℂ
191	190	a1i 11	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ0 → (8 / 9) ∈ ℂ)
192	187	nnne0d 12207	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ0 → (9↑𝑁) ≠ 0)
193		8nn 12252	. . . . . . . . . . . . 13 ⊢ 8 ∈ ℕ
194	193	nnne0i 12197	. . . . . . . . . . . 12 ⊢ 8 ≠ 0
195	189, 70, 194, 72	divne0i 11901	. . . . . . . . . . 11 ⊢ (8 / 9) ≠ 0
196	195	a1i 11	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ0 → (8 / 9) ≠ 0)
197	185, 188, 191, 192, 196	divdiv32d 11954	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ0 → ((1 / (9↑𝑁)) / (8 / 9)) = ((1 / (8 / 9)) / (9↑𝑁)))
198		recdiv 11859	. . . . . . . . . . . 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 7378	. . . . . . . . . 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 11960	. . . . . . . . . 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 5126	. . . . . . 7 ⊢ (𝑁 ∈ ℕ0 → seq𝑁( + , (𝑘 ∈ ℕ0 ↦ ((1 / 9)↑𝑘))) ⇝ (9 / (8 · (9↑𝑁))))
207		expcl 14014	. . . . . . . . 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 7384	. . . . . . . 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 15593	. . . . . 6 ⊢ (𝑁 ∈ ℕ0 → seq𝑁( + , (𝑘 ∈ ℕ0 ↦ ((2 / (3 · ((2 · 𝑁) + 1))) · ((1 / 9)↑𝑘)))) ⇝ ((2 / (3 · ((2 · 𝑁) + 1))) · (9 / (8 · (9↑𝑁)))))
214		seqex 13938	. . . . . . 7 ⊢ seq𝑁( + , (𝑘 ∈ ℕ0 ↦ ((2 / (3 · ((2 · 𝑁) + 1))) · ((1 / 9)↑𝑘)))) ∈ V
215		ovex 7401	. . . . . . 7 ⊢ ((2 / (3 · ((2 · 𝑁) + 1))) · (9 / (8 · (9↑𝑁)))) ∈ V
216	214, 215	breldm 5865	. . . . . 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 15779	. . . 4 ⊢ (𝑁 ∈ ℕ0 → Σ𝑛 ∈ (ℤ≥‘𝑁)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) ≤ Σ𝑛 ∈ (ℤ≥‘𝑁)(2 / ((3 · ((2 · 𝑁) + 1)) · (9↑𝑛))))
219	102	recnd 11172	. . . . 5 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (2 / ((3 · ((2 · 𝑁) + 1)) · (9↑𝑛))) ∈ ℂ)
220		3cn 12238	. . . . . . . . . . . 12 ⊢ 3 ∈ ℂ
221		4cn 12242	. . . . . . . . . . . 12 ⊢ 4 ∈ ℂ
222		2cn 12232	. . . . . . . . . . . 12 ⊢ 2 ∈ ℂ
223		4ne0 12265	. . . . . . . . . . . 12 ⊢ 4 ≠ 0
224		3ne0 12263	. . . . . . . . . . . 12 ⊢ 3 ≠ 0
225		2ne0 12261	. . . . . . . . . . . 12 ⊢ 2 ≠ 0
226	220, 221, 222, 220, 223, 224, 225	divdivdivi 11916	. . . . . . . . . . 11 ⊢ ((3 / 4) / (2 / 3)) = ((3 · 3) / (4 · 2))
227		3t3e9 12319	. . . . . . . . . . . 12 ⊢ (3 · 3) = 9
228		4t2e8 12320	. . . . . . . . . . . 12 ⊢ (4 · 2) = 8
229	227, 228	oveq12i 7380	. . . . . . . . . . 11 ⊢ ((3 · 3) / (4 · 2)) = (9 / 8)
230	226, 229	eqtri 2760	. . . . . . . . . 10 ⊢ ((3 / 4) / (2 / 3)) = (9 / 8)
231	230	oveq2i 7379	. . . . . . . . 9 ⊢ ((2 / 3) · ((3 / 4) / (2 / 3))) = ((2 / 3) · (9 / 8))
232	220, 221, 223	divcli 11895	. . . . . . . . . 10 ⊢ (3 / 4) ∈ ℂ
233	222, 220, 224	divcli 11895	. . . . . . . . . 10 ⊢ (2 / 3) ∈ ℂ
234	222, 220, 225, 224	divne0i 11901	. . . . . . . . . 10 ⊢ (2 / 3) ≠ 0
235	232, 233, 234	divcan2i 11896	. . . . . . . . 9 ⊢ ((2 / 3) · ((3 / 4) / (2 / 3))) = (3 / 4)
236	231, 235	eqtr3i 2762	. . . . . . . 8 ⊢ ((2 / 3) · (9 / 8)) = (3 / 4)
237	236	oveq1i 7378	. . . . . . 7 ⊢ (((2 / 3) · (9 / 8)) / (((2 · 𝑁) + 1) · (9↑𝑁))) = ((3 / 4) / (((2 · 𝑁) + 1) · (9↑𝑁)))
238		2cnd 12235	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ0 → 2 ∈ ℂ)
239	220	a1i 11	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ0 → 3 ∈ ℂ)
240	81	nncnd 12173	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ0 → ((2 · 𝑁) + 1) ∈ ℂ)
241	224	a1i 11	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ0 → 3 ≠ 0)
242	81	nnne0d 12207	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ0 → ((2 · 𝑁) + 1) ≠ 0)
243	238, 239, 240, 241, 242	divdiv1d 11960	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ0 → ((2 / 3) / ((2 · 𝑁) + 1)) = (2 / (3 · ((2 · 𝑁) + 1))))
244	243, 203	oveq12d 7386	. . . . . . . 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 11895	. . . . . . . . . 10 ⊢ (9 / 8) ∈ ℂ
247	246	a1i 11	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ0 → (9 / 8) ∈ ℂ)
248	245, 240, 247, 188, 242, 192	divmuldivd 11970	. . . . . . . 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 11167	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ0 → ((4 · ((2 · 𝑁) + 1)) · (9↑𝑁)) = (4 · (((2 · 𝑁) + 1) · (9↑𝑁))))
252	251	oveq2d 7384	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ0 → (3 / ((4 · ((2 · 𝑁) + 1)) · (9↑𝑁))) = (3 / (4 · (((2 · 𝑁) + 1) · (9↑𝑁)))))
253	81, 187	nnmulcld 12210	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ0 → (((2 · 𝑁) + 1) · (9↑𝑁)) ∈ ℕ)
254	253	nncnd 12173	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ0 → (((2 · 𝑁) + 1) · (9↑𝑁)) ∈ ℂ)
255	223	a1i 11	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ0 → 4 ≠ 0)
256	253	nnne0d 12207	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ0 → (((2 · 𝑁) + 1) · (9↑𝑁)) ≠ 0)
257	239, 250, 254, 255, 256	divdiv1d 11960	. . . . . . . 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 5126	. . . . 5 ⊢ (𝑁 ∈ ℕ0 → seq𝑁( + , (𝑘 ∈ ℕ0 ↦ ((2 / (3 · ((2 · 𝑁) + 1))) · ((1 / 9)↑𝑘)))) ⇝ (3 / ((4 · ((2 · 𝑁) + 1)) · (9↑𝑁))))
261	22, 23, 98, 219, 260	isumclim 15692	. . . 4 ⊢ (𝑁 ∈ ℕ0 → Σ𝑛 ∈ (ℤ≥‘𝑁)(2 / ((3 · ((2 · 𝑁) + 1)) · (9↑𝑛))) = (3 / ((4 · ((2 · 𝑁) + 1)) · (9↑𝑁))))
262	218, 261	breqtrd 5126	. . 3 ⊢ (𝑁 ∈ ℕ0 → Σ𝑛 ∈ (ℤ≥‘𝑁)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) ≤ (3 / ((4 · ((2 · 𝑁) + 1)) · (9↑𝑁))))
263		4nn 12240	. . . . . . 7 ⊢ 4 ∈ ℕ
264		nnmulcl 12181	. . . . . . 7 ⊢ ((4 ∈ ℕ ∧ ((2 · 𝑁) + 1) ∈ ℕ) → (4 · ((2 · 𝑁) + 1)) ∈ ℕ)
265	263, 81, 264	sylancr 588	. . . . . 6 ⊢ (𝑁 ∈ ℕ0 → (4 · ((2 · 𝑁) + 1)) ∈ ℕ)
266	265, 187	nnmulcld 12210	. . . . 5 ⊢ (𝑁 ∈ ℕ0 → ((4 · ((2 · 𝑁) + 1)) · (9↑𝑁)) ∈ ℕ)
267		nndivre 12198	. . . . 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 13339	. . . 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 5100   ↦ cmpt 5181  dom cdm 5632  ‘cfv 6500  (class class class)co 7368  ℂcc 11036  ℝcr 11037  0cc0 11038  1c1 11039   + caddc 11041   · cmul 11043   < clt 11178   ≤ cle 11179   − cmin 11376   / cdiv 11806  ℕcn 12157  2c2 12212  3c3 12213  4c4 12214  8c8 12218  9c9 12219  ℕ₀cn0 12413  ℤcz 12500  ℤ_≥cuz 12763  [,]cicc 13276  ...cfz 13435  seqcseq 13936  ↑cexp 13996  abscabs 15169   ⇝ cli 15419  Σcsu 15621  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 5226  ax-sep 5243  ax-nul 5253  ax-pow 5312  ax-pr 5379  ax-un 7690  ax-inf2 9562  ax-cnex 11094  ax-resscn 11095  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-addrcl 11099  ax-mulcl 11100  ax-mulrcl 11101  ax-mulcom 11102  ax-addass 11103  ax-mulass 11104  ax-distr 11105  ax-i2m1 11106  ax-1ne0 11107  ax-1rid 11108  ax-rnegex 11109  ax-rrecex 11110  ax-cnre 11111  ax-pre-lttri 11112  ax-pre-lttrn 11113  ax-pre-ltadd 11114  ax-pre-mulgt0 11115  ax-pre-sup 11116  ax-addf 11117

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 3352  df-reu 3353  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-tp 4587  df-op 4589  df-uni 4866  df-int 4905  df-iun 4950  df-iin 4951  df-br 5101  df-opab 5163  df-mpt 5182  df-tr 5208  df-id 5527  df-eprel 5532  df-po 5540  df-so 5541  df-fr 5585  df-se 5586  df-we 5587  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-pred 6267  df-ord 6328  df-on 6329  df-lim 6330  df-suc 6331  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-isom 6509  df-riota 7325  df-ov 7371  df-oprab 7372  df-mpo 7373  df-of 7632  df-om 7819  df-1st 7943  df-2nd 7944  df-supp 8113  df-frecs 8233  df-wrecs 8264  df-recs 8313  df-rdg 8351  df-1o 8407  df-2o 8408  df-oadd 8411  df-er 8645  df-map 8777  df-pm 8778  df-ixp 8848  df-en 8896  df-dom 8897  df-sdom 8898  df-fin 8899  df-fsupp 9277  df-fi 9326  df-sup 9357  df-inf 9358  df-oi 9427  df-card 9863  df-pnf 11180  df-mnf 11181  df-xr 11182  df-ltxr 11183  df-le 11184  df-sub 11378  df-neg 11379  df-div 11807  df-nn 12158  df-2 12220  df-3 12221  df-4 12222  df-5 12223  df-6 12224  df-7 12225  df-8 12226  df-9 12227  df-n0 12414  df-xnn0 12487  df-z 12501  df-dec 12620  df-uz 12764  df-q 12874  df-rp 12918  df-xneg 13038  df-xadd 13039  df-xmul 13040  df-ioo 13277  df-ioc 13278  df-ico 13279  df-icc 13280  df-fz 13436  df-fzo 13583  df-fl 13724  df-mod 13802  df-seq 13937  df-exp 13997  df-fac 14209  df-bc 14238  df-hash 14266  df-shft 15002  df-cj 15034  df-re 15035  df-im 15036  df-sqrt 15170  df-abs 15171  df-limsup 15406  df-clim 15423  df-rlim 15424  df-sum 15622  df-ef 16002  df-sin 16004  df-cos 16005  df-tan 16006  df-pi 16007  df-dvds 16192  df-struct 17086  df-sets 17103  df-slot 17121  df-ndx 17133  df-base 17149  df-ress 17170  df-plusg 17202  df-mulr 17203  df-starv 17204  df-sca 17205  df-vsca 17206  df-ip 17207  df-tset 17208  df-ple 17209  df-ds 17211  df-unif 17212  df-hom 17213  df-cco 17214  df-rest 17354  df-topn 17355  df-0g 17373  df-gsum 17374  df-topgen 17375  df-pt 17376  df-prds 17379  df-xrs 17435  df-qtop 17440  df-imas 17441  df-xps 17443  df-mre 17517  df-mrc 17518  df-acs 17520  df-mgm 18577  df-sgrp 18656  df-mnd 18672  df-submnd 18721  df-mulg 19010  df-cntz 19258  df-cmn 19723  df-psmet 21313  df-xmet 21314  df-met 21315  df-bl 21316  df-mopn 21317  df-fbas 21318  df-fg 21319  df-cnfld 21322  df-top 22850  df-topon 22867  df-topsp 22889  df-bases 22902  df-cld 22975  df-ntr 22976  df-cls 22977  df-nei 23054  df-lp 23092  df-perf 23093  df-cn 23183  df-cnp 23184  df-haus 23271  df-cmp 23343  df-tx 23518  df-hmeo 23711  df-fil 23802  df-fm 23894  df-flim 23895  df-flf 23896  df-xms 24276  df-ms 24277  df-tms 24278  df-cncf 24839  df-limc 25835  df-dv 25836  df-ulm 26354  df-log 26533  df-atan 26845

This theorem is referenced by:  log2ub  26927