Theorem log2tlbnd 26439

Description: Bound the error term in the series of log2cnv 26438. (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 13934	. . . 4 ⊢ (𝑁 ∈ ℕ0 → (0...(𝑁 − 1)) ∈ Fin)
2		elfznn0 13590	. . . . 5 ⊢ (𝑛 ∈ (0...(𝑁 − 1)) → 𝑛 ∈ ℕ0)
3		2re 12282	. . . . . . 7 ⊢ 2 ∈ ℝ
4		3nn 12287	. . . . . . . . 9 ⊢ 3 ∈ ℕ
5		2nn0 12485	. . . . . . . . . . 11 ⊢ 2 ∈ ℕ0
6		simpr 485	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → 𝑛 ∈ ℕ0)
7		nn0mulcl 12504	. . . . . . . . . . 11 ⊢ ((2 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → (2 · 𝑛) ∈ ℕ0)
8	5, 6, 7	sylancr 587	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → (2 · 𝑛) ∈ ℕ0)
9		nn0p1nn 12507	. . . . . . . . . 10 ⊢ ((2 · 𝑛) ∈ ℕ0 → ((2 · 𝑛) + 1) ∈ ℕ)
10	8, 9	syl 17	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → ((2 · 𝑛) + 1) ∈ ℕ)
11		nnmulcl 12232	. . . . . . . . 9 ⊢ ((3 ∈ ℕ ∧ ((2 · 𝑛) + 1) ∈ ℕ) → (3 · ((2 · 𝑛) + 1)) ∈ ℕ)
12	4, 10, 11	sylancr 587	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → (3 · ((2 · 𝑛) + 1)) ∈ ℕ)
13		9nn 12306	. . . . . . . . 9 ⊢ 9 ∈ ℕ
14		nnexpcl 14036	. . . . . . . . 9 ⊢ ((9 ∈ ℕ ∧ 𝑛 ∈ ℕ0) → (9↑𝑛) ∈ ℕ)
15	13, 6, 14	sylancr 587	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → (9↑𝑛) ∈ ℕ)
16	12, 15	nnmulcld 12261	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)) ∈ ℕ)
17		nndivre 12249	. . . . . . 7 ⊢ ((2 ∈ ℝ ∧ ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)) ∈ ℕ) → (2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) ∈ ℝ)
18	3, 16, 17	sylancr 587	. . . . . 6 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → (2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) ∈ ℝ)
19	18	recnd 11238	. . . . 5 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → (2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) ∈ ℂ)
20	2, 19	sylan2 593	. . . 4 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (0...(𝑁 − 1))) → (2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) ∈ ℂ)
21	1, 20	fsumcl 15675	. . 3 ⊢ (𝑁 ∈ ℕ0 → Σ𝑛 ∈ (0...(𝑁 − 1))(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) ∈ ℂ)
22		eqid 2732	. . . . 5 ⊢ (ℤ≥‘𝑁) = (ℤ≥‘𝑁)
23		nn0z 12579	. . . . 5 ⊢ (𝑁 ∈ ℕ0 → 𝑁 ∈ ℤ)
24		eluznn0 12897	. . . . . 6 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → 𝑛 ∈ ℕ0)
25		oveq2 7413	. . . . . . . . . . 11 ⊢ (𝑘 = 𝑛 → (2 · 𝑘) = (2 · 𝑛))
26	25	oveq1d 7420	. . . . . . . . . 10 ⊢ (𝑘 = 𝑛 → ((2 · 𝑘) + 1) = ((2 · 𝑛) + 1))
27	26	oveq2d 7421	. . . . . . . . 9 ⊢ (𝑘 = 𝑛 → (3 · ((2 · 𝑘) + 1)) = (3 · ((2 · 𝑛) + 1)))
28		oveq2 7413	. . . . . . . . 9 ⊢ (𝑘 = 𝑛 → (9↑𝑘) = (9↑𝑛))
29	27, 28	oveq12d 7423	. . . . . . . 8 ⊢ (𝑘 = 𝑛 → ((3 · ((2 · 𝑘) + 1)) · (9↑𝑘)) = ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))
30	29	oveq2d 7421	. . . . . . 7 ⊢ (𝑘 = 𝑛 → (2 / ((3 · ((2 · 𝑘) + 1)) · (9↑𝑘))) = (2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))))
31		eqid 2732	. . . . . . 7 ⊢ (𝑘 ∈ ℕ0 ↦ (2 / ((3 · ((2 · 𝑘) + 1)) · (9↑𝑘)))) = (𝑘 ∈ ℕ0 ↦ (2 / ((3 · ((2 · 𝑘) + 1)) · (9↑𝑘))))
32		ovex 7438	. . . . . . 7 ⊢ (2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) ∈ V
33	30, 31, 32	fvmpt 6995	. . . . . 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 591	. . . . 5 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) ∈ ℝ)
36	31	log2cnv 26438	. . . . . . 7 ⊢ seq0( + , (𝑘 ∈ ℕ0 ↦ (2 / ((3 · ((2 · 𝑘) + 1)) · (9↑𝑘))))) ⇝ (log‘2)
37		seqex 13964	. . . . . . . 8 ⊢ seq0( + , (𝑘 ∈ ℕ0 ↦ (2 / ((3 · ((2 · 𝑘) + 1)) · (9↑𝑘))))) ∈ V
38		fvex 6901	. . . . . . . 8 ⊢ (log‘2) ∈ V
39	37, 38	breldm 5906	. . . . . . 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 12860	. . . . . . 7 ⊢ ℕ0 = (ℤ≥‘0)
42		id 22	. . . . . . 7 ⊢ (𝑁 ∈ ℕ0 → 𝑁 ∈ ℕ0)
43	33	adantl 482	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → ((𝑘 ∈ ℕ0 ↦ (2 / ((3 · ((2 · 𝑘) + 1)) · (9↑𝑘))))‘𝑛) = (2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))))
44	43, 19	eqeltrd 2833	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → ((𝑘 ∈ ℕ0 ↦ (2 / ((3 · ((2 · 𝑘) + 1)) · (9↑𝑘))))‘𝑛) ∈ ℂ)
45	41, 42, 44	iserex 15599	. . . . . 6 ⊢ (𝑁 ∈ ℕ0 → (seq0( + , (𝑘 ∈ ℕ0 ↦ (2 / ((3 · ((2 · 𝑘) + 1)) · (9↑𝑘))))) ∈ dom ⇝ ↔ seq𝑁( + , (𝑘 ∈ ℕ0 ↦ (2 / ((3 · ((2 · 𝑘) + 1)) · (9↑𝑘))))) ∈ dom ⇝ ))
46	40, 45	mpbid 231	. . . . 5 ⊢ (𝑁 ∈ ℕ0 → seq𝑁( + , (𝑘 ∈ ℕ0 ↦ (2 / ((3 · ((2 · 𝑘) + 1)) · (9↑𝑘))))) ∈ dom ⇝ )
47	22, 23, 34, 35, 46	isumrecl 15707	. . . 4 ⊢ (𝑁 ∈ ℕ0 → Σ𝑛 ∈ (ℤ≥‘𝑁)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) ∈ ℝ)
48	47	recnd 11238	. . 3 ⊢ (𝑁 ∈ ℕ0 → Σ𝑛 ∈ (ℤ≥‘𝑁)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) ∈ ℂ)
49		0zd 12566	. . . . 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 15699	. . . 4 ⊢ (𝑁 ∈ ℕ0 → Σ𝑛 ∈ ℕ0 (2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) = (log‘2))
52	41, 22, 42, 43, 19, 40	isumsplit 15782	. . . 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 11623	. 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 12310	. . . . . . 7 ⊢ 0 ≤ 2
57	56	a1i 11	. . . . . 6 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → 0 ≤ 2)
58	16	nnred 12223	. . . . . 6 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)) ∈ ℝ)
59	16	nngt0d 12257	. . . . . 6 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → 0 < ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))
60		divge0 12079	. . . . . 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 837	. . . . 5 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → 0 ≤ (2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))))
62	24, 61	syldan 591	. . . 4 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → 0 ≤ (2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))))
63	22, 23, 34, 35, 46, 62	isumge0 15708	. . 3 ⊢ (𝑁 ∈ ℕ0 → 0 ≤ Σ𝑛 ∈ (ℤ≥‘𝑁)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))))
64		oveq2 7413	. . . . . . . . . 10 ⊢ (𝑘 = 𝑛 → ((1 / 9)↑𝑘) = ((1 / 9)↑𝑛))
65	64	oveq2d 7421	. . . . . . . . 9 ⊢ (𝑘 = 𝑛 → ((2 / (3 · ((2 · 𝑁) + 1))) · ((1 / 9)↑𝑘)) = ((2 / (3 · ((2 · 𝑁) + 1))) · ((1 / 9)↑𝑛)))
66		eqid 2732	. . . . . . . . 9 ⊢ (𝑘 ∈ ℕ0 ↦ ((2 / (3 · ((2 · 𝑁) + 1))) · ((1 / 9)↑𝑘))) = (𝑘 ∈ ℕ0 ↦ ((2 / (3 · ((2 · 𝑁) + 1))) · ((1 / 9)↑𝑘)))
67		ovex 7438	. . . . . . . . 9 ⊢ ((2 / (3 · ((2 · 𝑁) + 1))) · ((1 / 9)↑𝑛)) ∈ V
68	65, 66, 67	fvmpt 6995	. . . . . . . 8 ⊢ (𝑛 ∈ ℕ0 → ((𝑘 ∈ ℕ0 ↦ ((2 / (3 · ((2 · 𝑁) + 1))) · ((1 / 9)↑𝑘)))‘𝑛) = ((2 / (3 · ((2 · 𝑁) + 1))) · ((1 / 9)↑𝑛)))
69	68	adantl 482	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → ((𝑘 ∈ ℕ0 ↦ ((2 / (3 · ((2 · 𝑁) + 1))) · ((1 / 9)↑𝑘)))‘𝑛) = ((2 / (3 · ((2 · 𝑁) + 1))) · ((1 / 9)↑𝑛)))
70		9cn 12308	. . . . . . . . . . 11 ⊢ 9 ∈ ℂ
71	70	a1i 11	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → 9 ∈ ℂ)
72	13	nnne0i 12248	. . . . . . . . . . 11 ⊢ 9 ≠ 0
73	72	a1i 11	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → 9 ≠ 0)
74		nn0z 12579	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ℕ0 → 𝑛 ∈ ℤ)
75	74	adantl 482	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → 𝑛 ∈ ℤ)
76	71, 73, 75	exprecd 14115	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → ((1 / 9)↑𝑛) = (1 / (9↑𝑛)))
77	76	oveq2d 7421	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → ((2 / (3 · ((2 · 𝑁) + 1))) · ((1 / 9)↑𝑛)) = ((2 / (3 · ((2 · 𝑁) + 1))) · (1 / (9↑𝑛))))
78		nn0mulcl 12504	. . . . . . . . . . . . . . 15 ⊢ ((2 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (2 · 𝑁) ∈ ℕ0)
79	5, 78	mpan 688	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ ℕ0 → (2 · 𝑁) ∈ ℕ0)
80		nn0p1nn 12507	. . . . . . . . . . . . . 14 ⊢ ((2 · 𝑁) ∈ ℕ0 → ((2 · 𝑁) + 1) ∈ ℕ)
81	79, 80	syl 17	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ ℕ0 → ((2 · 𝑁) + 1) ∈ ℕ)
82		nnmulcl 12232	. . . . . . . . . . . . 13 ⊢ ((3 ∈ ℕ ∧ ((2 · 𝑁) + 1) ∈ ℕ) → (3 · ((2 · 𝑁) + 1)) ∈ ℕ)
83	4, 81, 82	sylancr 587	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℕ0 → (3 · ((2 · 𝑁) + 1)) ∈ ℕ)
84		nndivre 12249	. . . . . . . . . . . 12 ⊢ ((2 ∈ ℝ ∧ (3 · ((2 · 𝑁) + 1)) ∈ ℕ) → (2 / (3 · ((2 · 𝑁) + 1))) ∈ ℝ)
85	3, 83, 84	sylancr 587	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℕ0 → (2 / (3 · ((2 · 𝑁) + 1))) ∈ ℝ)
86	85	recnd 11238	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ0 → (2 / (3 · ((2 · 𝑁) + 1))) ∈ ℂ)
87	86	adantr 481	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → (2 / (3 · ((2 · 𝑁) + 1))) ∈ ℂ)
88	15	nncnd 12224	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → (9↑𝑛) ∈ ℂ)
89	15	nnne0d 12258	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → (9↑𝑛) ≠ 0)
90	87, 88, 89	divrecd 11989	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → ((2 / (3 · ((2 · 𝑁) + 1))) / (9↑𝑛)) = ((2 / (3 · ((2 · 𝑁) + 1))) · (1 / (9↑𝑛))))
91		2cnd 12286	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → 2 ∈ ℂ)
92	83	adantr 481	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → (3 · ((2 · 𝑁) + 1)) ∈ ℕ)
93	92	nncnd 12224	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → (3 · ((2 · 𝑁) + 1)) ∈ ℂ)
94	92	nnne0d 12258	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → (3 · ((2 · 𝑁) + 1)) ≠ 0)
95	91, 93, 88, 94, 89	divdiv1d 12017	. . . . . . . 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 591	. . . . 5 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → ((𝑘 ∈ ℕ0 ↦ ((2 / (3 · ((2 · 𝑁) + 1))) · ((1 / 9)↑𝑘)))‘𝑛) = (2 / ((3 · ((2 · 𝑁) + 1)) · (9↑𝑛))))
99	92, 15	nnmulcld 12261	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → ((3 · ((2 · 𝑁) + 1)) · (9↑𝑛)) ∈ ℕ)
100		nndivre 12249	. . . . . . 7 ⊢ ((2 ∈ ℝ ∧ ((3 · ((2 · 𝑁) + 1)) · (9↑𝑛)) ∈ ℕ) → (2 / ((3 · ((2 · 𝑁) + 1)) · (9↑𝑛))) ∈ ℝ)
101	3, 99, 100	sylancr 587	. . . . . 6 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → (2 / ((3 · ((2 · 𝑁) + 1)) · (9↑𝑛))) ∈ ℝ)
102	24, 101	syldan 591	. . . . 5 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (2 / ((3 · ((2 · 𝑁) + 1)) · (9↑𝑛))) ∈ ℝ)
103	79	adantr 481	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (2 · 𝑁) ∈ ℕ0)
104	103	nn0red 12529	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (2 · 𝑁) ∈ ℝ)
105	5, 24, 7	sylancr 587	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (2 · 𝑛) ∈ ℕ0)
106	105	nn0red 12529	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (2 · 𝑛) ∈ ℝ)
107		1red 11211	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → 1 ∈ ℝ)
108		eluzle 12831	. . . . . . . . . . 11 ⊢ (𝑛 ∈ (ℤ≥‘𝑁) → 𝑁 ≤ 𝑛)
109	108	adantl 482	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → 𝑁 ≤ 𝑛)
110		nn0re 12477	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℕ0 → 𝑁 ∈ ℝ)
111	110	adantr 481	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → 𝑁 ∈ ℝ)
112	24	nn0red 12529	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → 𝑛 ∈ ℝ)
113	3	a1i 11	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → 2 ∈ ℝ)
114		2pos 12311	. . . . . . . . . . . 12 ⊢ 0 < 2
115	114	a1i 11	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → 0 < 2)
116		lemul2 12063	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℝ ∧ 𝑛 ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → (𝑁 ≤ 𝑛 ↔ (2 · 𝑁) ≤ (2 · 𝑛)))
117	111, 112, 113, 115, 116	syl112anc 1374	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (𝑁 ≤ 𝑛 ↔ (2 · 𝑁) ≤ (2 · 𝑛)))
118	109, 117	mpbid 231	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (2 · 𝑁) ≤ (2 · 𝑛))
119	104, 106, 107, 118	leadd1dd 11824	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → ((2 · 𝑁) + 1) ≤ ((2 · 𝑛) + 1))
120	81	adantr 481	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → ((2 · 𝑁) + 1) ∈ ℕ)
121	120	nnred 12223	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → ((2 · 𝑁) + 1) ∈ ℝ)
122	24, 10	syldan 591	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → ((2 · 𝑛) + 1) ∈ ℕ)
123	122	nnred 12223	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → ((2 · 𝑛) + 1) ∈ ℝ)
124		3re 12288	. . . . . . . . . 10 ⊢ 3 ∈ ℝ
125	124	a1i 11	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → 3 ∈ ℝ)
126		3pos 12313	. . . . . . . . . 10 ⊢ 0 < 3
127	126	a1i 11	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → 0 < 3)
128		lemul2 12063	. . . . . . . . 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 1374	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (((2 · 𝑁) + 1) ≤ ((2 · 𝑛) + 1) ↔ (3 · ((2 · 𝑁) + 1)) ≤ (3 · ((2 · 𝑛) + 1))))
130	119, 129	mpbid 231	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (3 · ((2 · 𝑁) + 1)) ≤ (3 · ((2 · 𝑛) + 1)))
131	83	adantr 481	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (3 · ((2 · 𝑁) + 1)) ∈ ℕ)
132	131	nnred 12223	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (3 · ((2 · 𝑁) + 1)) ∈ ℝ)
133	24, 12	syldan 591	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (3 · ((2 · 𝑛) + 1)) ∈ ℕ)
134	133	nnred 12223	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (3 · ((2 · 𝑛) + 1)) ∈ ℝ)
135	13, 24, 14	sylancr 587	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (9↑𝑛) ∈ ℕ)
136	135	nnred 12223	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (9↑𝑛) ∈ ℝ)
137	135	nngt0d 12257	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → 0 < (9↑𝑛))
138		lemul1 12062	. . . . . . . 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 1374	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → ((3 · ((2 · 𝑁) + 1)) ≤ (3 · ((2 · 𝑛) + 1)) ↔ ((3 · ((2 · 𝑁) + 1)) · (9↑𝑛)) ≤ ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))))
140	130, 139	mpbid 231	. . . . . 6 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → ((3 · ((2 · 𝑁) + 1)) · (9↑𝑛)) ≤ ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))
141	24, 99	syldan 591	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → ((3 · ((2 · 𝑁) + 1)) · (9↑𝑛)) ∈ ℕ)
142	141	nnred 12223	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → ((3 · ((2 · 𝑁) + 1)) · (9↑𝑛)) ∈ ℝ)
143	141	nngt0d 12257	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → 0 < ((3 · ((2 · 𝑁) + 1)) · (9↑𝑛)))
144	24, 58	syldan 591	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)) ∈ ℝ)
145	24, 59	syldan 591	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → 0 < ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))
146		lediv2 12100	. . . . . . 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 1386	. . . . . 6 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (((3 · ((2 · 𝑁) + 1)) · (9↑𝑛)) ≤ ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)) ↔ (2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) ≤ (2 / ((3 · ((2 · 𝑁) + 1)) · (9↑𝑛)))))
148	140, 147	mpbid 231	. . . . 5 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) ≤ (2 / ((3 · ((2 · 𝑁) + 1)) · (9↑𝑛))))
149		9re 12307	. . . . . . . . . . . 12 ⊢ 9 ∈ ℝ
150	149, 72	rereccli 11975	. . . . . . . . . . 11 ⊢ (1 / 9) ∈ ℝ
151	150	recni 11224	. . . . . . . . . 10 ⊢ (1 / 9) ∈ ℂ
152	151	a1i 11	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ0 → (1 / 9) ∈ ℂ)
153		0re 11212	. . . . . . . . . . . . 13 ⊢ 0 ∈ ℝ
154		9pos 12321	. . . . . . . . . . . . . 14 ⊢ 0 < 9
155	149, 154	recgt0ii 12116	. . . . . . . . . . . . 13 ⊢ 0 < (1 / 9)
156	153, 150, 155	ltleii 11333	. . . . . . . . . . . 12 ⊢ 0 ≤ (1 / 9)
157		absid 15239	. . . . . . . . . . . 12 ⊢ (((1 / 9) ∈ ℝ ∧ 0 ≤ (1 / 9)) → (abs‘(1 / 9)) = (1 / 9))
158	150, 156, 157	mp2an 690	. . . . . . . . . . 11 ⊢ (abs‘(1 / 9)) = (1 / 9)
159		1lt9 12414	. . . . . . . . . . . . 13 ⊢ 1 < 9
160		recgt1i 12107	. . . . . . . . . . . . 13 ⊢ ((9 ∈ ℝ ∧ 1 < 9) → (0 < (1 / 9) ∧ (1 / 9) < 1))
161	149, 159, 160	mp2an 690	. . . . . . . . . . . 12 ⊢ (0 < (1 / 9) ∧ (1 / 9) < 1)
162	161	simpri 486	. . . . . . . . . . 11 ⊢ (1 / 9) < 1
163	158, 162	eqbrtri 5168	. . . . . . . . . 10 ⊢ (abs‘(1 / 9)) < 1
164	163	a1i 11	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ0 → (abs‘(1 / 9)) < 1)
165		eqid 2732	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℕ0 ↦ ((1 / 9)↑𝑘)) = (𝑘 ∈ ℕ0 ↦ ((1 / 9)↑𝑘))
166		ovex 7438	. . . . . . . . . . 11 ⊢ ((1 / 9)↑𝑛) ∈ V
167	64, 165, 166	fvmpt 6995	. . . . . . . . . 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 15813	. . . . . . . 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 14115	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ0 → ((1 / 9)↑𝑁) = (1 / (9↑𝑁)))
173	70, 72	dividi 11943	. . . . . . . . . . . . 13 ⊢ (9 / 9) = 1
174	173	oveq1i 7415	. . . . . . . . . . . 12 ⊢ ((9 / 9) − (1 / 9)) = (1 − (1 / 9))
175		ax-1cn 11164	. . . . . . . . . . . . . 14 ⊢ 1 ∈ ℂ
176	70, 72	pm3.2i 471	. . . . . . . . . . . . . 14 ⊢ (9 ∈ ℂ ∧ 9 ≠ 0)
177		divsubdir 11904	. . . . . . . . . . . . . 14 ⊢ ((9 ∈ ℂ ∧ 1 ∈ ℂ ∧ (9 ∈ ℂ ∧ 9 ≠ 0)) → ((9 − 1) / 9) = ((9 / 9) − (1 / 9)))
178	70, 175, 176, 177	mp3an 1461	. . . . . . . . . . . . 13 ⊢ ((9 − 1) / 9) = ((9 / 9) − (1 / 9))
179		9m1e8 12342	. . . . . . . . . . . . . 14 ⊢ (9 − 1) = 8
180	179	oveq1i 7415	. . . . . . . . . . . . 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 7423	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ0 → (((1 / 9)↑𝑁) / (1 − (1 / 9))) = ((1 / (9↑𝑁)) / (8 / 9)))
185	175	a1i 11	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ0 → 1 ∈ ℂ)
186		nnexpcl 14036	. . . . . . . . . . . 12 ⊢ ((9 ∈ ℕ ∧ 𝑁 ∈ ℕ0) → (9↑𝑁) ∈ ℕ)
187	13, 186	mpan 688	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℕ0 → (9↑𝑁) ∈ ℕ)
188	187	nncnd 12224	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ0 → (9↑𝑁) ∈ ℂ)
189		8cn 12305	. . . . . . . . . . . 12 ⊢ 8 ∈ ℂ
190	189, 70, 72	divcli 11952	. . . . . . . . . . 11 ⊢ (8 / 9) ∈ ℂ
191	190	a1i 11	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ0 → (8 / 9) ∈ ℂ)
192	187	nnne0d 12258	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ0 → (9↑𝑁) ≠ 0)
193		8nn 12303	. . . . . . . . . . . . 13 ⊢ 8 ∈ ℕ
194	193	nnne0i 12248	. . . . . . . . . . . 12 ⊢ 8 ≠ 0
195	189, 70, 194, 72	divne0i 11958	. . . . . . . . . . 11 ⊢ (8 / 9) ≠ 0
196	195	a1i 11	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ0 → (8 / 9) ≠ 0)
197	185, 188, 191, 192, 196	divdiv32d 12011	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ0 → ((1 / (9↑𝑁)) / (8 / 9)) = ((1 / (8 / 9)) / (9↑𝑁)))
198		recdiv 11916	. . . . . . . . . . . 12 ⊢ (((8 ∈ ℂ ∧ 8 ≠ 0) ∧ (9 ∈ ℂ ∧ 9 ≠ 0)) → (1 / (8 / 9)) = (9 / 8))
199	189, 194, 70, 72, 198	mp4an 691	. . . . . . . . . . 11 ⊢ (1 / (8 / 9)) = (9 / 8)
200	199	oveq1i 7415	. . . . . . . . . 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 12017	. . . . . . . . . 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 5173	. . . . . . 7 ⊢ (𝑁 ∈ ℕ0 → seq𝑁( + , (𝑘 ∈ ℕ0 ↦ ((1 / 9)↑𝑘))) ⇝ (9 / (8 · (9↑𝑁))))
207		expcl 14041	. . . . . . . . 9 ⊢ (((1 / 9) ∈ ℂ ∧ 𝑛 ∈ ℕ0) → ((1 / 9)↑𝑛) ∈ ℂ)
208	151, 24, 207	sylancr 587	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → ((1 / 9)↑𝑛) ∈ ℂ)
209	168, 208	eqeltrd 2833	. . . . . . 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 7421	. . . . . . . 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 15600	. . . . . 6 ⊢ (𝑁 ∈ ℕ0 → seq𝑁( + , (𝑘 ∈ ℕ0 ↦ ((2 / (3 · ((2 · 𝑁) + 1))) · ((1 / 9)↑𝑘)))) ⇝ ((2 / (3 · ((2 · 𝑁) + 1))) · (9 / (8 · (9↑𝑁)))))
214		seqex 13964	. . . . . . 7 ⊢ seq𝑁( + , (𝑘 ∈ ℕ0 ↦ ((2 / (3 · ((2 · 𝑁) + 1))) · ((1 / 9)↑𝑘)))) ∈ V
215		ovex 7438	. . . . . . 7 ⊢ ((2 / (3 · ((2 · 𝑁) + 1))) · (9 / (8 · (9↑𝑁)))) ∈ V
216	214, 215	breldm 5906	. . . . . 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 15786	. . . 4 ⊢ (𝑁 ∈ ℕ0 → Σ𝑛 ∈ (ℤ≥‘𝑁)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) ≤ Σ𝑛 ∈ (ℤ≥‘𝑁)(2 / ((3 · ((2 · 𝑁) + 1)) · (9↑𝑛))))
219	102	recnd 11238	. . . . 5 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (2 / ((3 · ((2 · 𝑁) + 1)) · (9↑𝑛))) ∈ ℂ)
220		3cn 12289	. . . . . . . . . . . 12 ⊢ 3 ∈ ℂ
221		4cn 12293	. . . . . . . . . . . 12 ⊢ 4 ∈ ℂ
222		2cn 12283	. . . . . . . . . . . 12 ⊢ 2 ∈ ℂ
223		4ne0 12316	. . . . . . . . . . . 12 ⊢ 4 ≠ 0
224		3ne0 12314	. . . . . . . . . . . 12 ⊢ 3 ≠ 0
225		2ne0 12312	. . . . . . . . . . . 12 ⊢ 2 ≠ 0
226	220, 221, 222, 220, 223, 224, 225	divdivdivi 11973	. . . . . . . . . . 11 ⊢ ((3 / 4) / (2 / 3)) = ((3 · 3) / (4 · 2))
227		3t3e9 12375	. . . . . . . . . . . 12 ⊢ (3 · 3) = 9
228		4t2e8 12376	. . . . . . . . . . . 12 ⊢ (4 · 2) = 8
229	227, 228	oveq12i 7417	. . . . . . . . . . 11 ⊢ ((3 · 3) / (4 · 2)) = (9 / 8)
230	226, 229	eqtri 2760	. . . . . . . . . 10 ⊢ ((3 / 4) / (2 / 3)) = (9 / 8)
231	230	oveq2i 7416	. . . . . . . . 9 ⊢ ((2 / 3) · ((3 / 4) / (2 / 3))) = ((2 / 3) · (9 / 8))
232	220, 221, 223	divcli 11952	. . . . . . . . . 10 ⊢ (3 / 4) ∈ ℂ
233	222, 220, 224	divcli 11952	. . . . . . . . . 10 ⊢ (2 / 3) ∈ ℂ
234	222, 220, 225, 224	divne0i 11958	. . . . . . . . . 10 ⊢ (2 / 3) ≠ 0
235	232, 233, 234	divcan2i 11953	. . . . . . . . 9 ⊢ ((2 / 3) · ((3 / 4) / (2 / 3))) = (3 / 4)
236	231, 235	eqtr3i 2762	. . . . . . . 8 ⊢ ((2 / 3) · (9 / 8)) = (3 / 4)
237	236	oveq1i 7415	. . . . . . 7 ⊢ (((2 / 3) · (9 / 8)) / (((2 · 𝑁) + 1) · (9↑𝑁))) = ((3 / 4) / (((2 · 𝑁) + 1) · (9↑𝑁)))
238		2cnd 12286	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ0 → 2 ∈ ℂ)
239	220	a1i 11	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ0 → 3 ∈ ℂ)
240	81	nncnd 12224	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ0 → ((2 · 𝑁) + 1) ∈ ℂ)
241	224	a1i 11	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ0 → 3 ≠ 0)
242	81	nnne0d 12258	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ0 → ((2 · 𝑁) + 1) ≠ 0)
243	238, 239, 240, 241, 242	divdiv1d 12017	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ0 → ((2 / 3) / ((2 · 𝑁) + 1)) = (2 / (3 · ((2 · 𝑁) + 1))))
244	243, 203	oveq12d 7423	. . . . . . . 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 11952	. . . . . . . . . 10 ⊢ (9 / 8) ∈ ℂ
247	246	a1i 11	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ0 → (9 / 8) ∈ ℂ)
248	245, 240, 247, 188, 242, 192	divmuldivd 12027	. . . . . . . 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 11233	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ0 → ((4 · ((2 · 𝑁) + 1)) · (9↑𝑁)) = (4 · (((2 · 𝑁) + 1) · (9↑𝑁))))
252	251	oveq2d 7421	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ0 → (3 / ((4 · ((2 · 𝑁) + 1)) · (9↑𝑁))) = (3 / (4 · (((2 · 𝑁) + 1) · (9↑𝑁)))))
253	81, 187	nnmulcld 12261	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ0 → (((2 · 𝑁) + 1) · (9↑𝑁)) ∈ ℕ)
254	253	nncnd 12224	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ0 → (((2 · 𝑁) + 1) · (9↑𝑁)) ∈ ℂ)
255	223	a1i 11	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ0 → 4 ≠ 0)
256	253	nnne0d 12258	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ0 → (((2 · 𝑁) + 1) · (9↑𝑁)) ≠ 0)
257	239, 250, 254, 255, 256	divdiv1d 12017	. . . . . . . 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 5173	. . . . 5 ⊢ (𝑁 ∈ ℕ0 → seq𝑁( + , (𝑘 ∈ ℕ0 ↦ ((2 / (3 · ((2 · 𝑁) + 1))) · ((1 / 9)↑𝑘)))) ⇝ (3 / ((4 · ((2 · 𝑁) + 1)) · (9↑𝑁))))
261	22, 23, 98, 219, 260	isumclim 15699	. . . 4 ⊢ (𝑁 ∈ ℕ0 → Σ𝑛 ∈ (ℤ≥‘𝑁)(2 / ((3 · ((2 · 𝑁) + 1)) · (9↑𝑛))) = (3 / ((4 · ((2 · 𝑁) + 1)) · (9↑𝑁))))
262	218, 261	breqtrd 5173	. . 3 ⊢ (𝑁 ∈ ℕ0 → Σ𝑛 ∈ (ℤ≥‘𝑁)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) ≤ (3 / ((4 · ((2 · 𝑁) + 1)) · (9↑𝑁))))
263		4nn 12291	. . . . . . 7 ⊢ 4 ∈ ℕ
264		nnmulcl 12232	. . . . . . 7 ⊢ ((4 ∈ ℕ ∧ ((2 · 𝑁) + 1) ∈ ℕ) → (4 · ((2 · 𝑁) + 1)) ∈ ℕ)
265	263, 81, 264	sylancr 587	. . . . . 6 ⊢ (𝑁 ∈ ℕ0 → (4 · ((2 · 𝑁) + 1)) ∈ ℕ)
266	265, 187	nnmulcld 12261	. . . . 5 ⊢ (𝑁 ∈ ℕ0 → ((4 · ((2 · 𝑁) + 1)) · (9↑𝑁)) ∈ ℕ)
267		nndivre 12249	. . . . 5 ⊢ ((3 ∈ ℝ ∧ ((4 · ((2 · 𝑁) + 1)) · (9↑𝑁)) ∈ ℕ) → (3 / ((4 · ((2 · 𝑁) + 1)) · (9↑𝑁))) ∈ ℝ)
268	124, 266, 267	sylancr 587	. . . 4 ⊢ (𝑁 ∈ ℕ0 → (3 / ((4 · ((2 · 𝑁) + 1)) · (9↑𝑁))) ∈ ℝ)
269		elicc2 13385	. . . 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 587	. . 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 1342	. 2 ⊢ (𝑁 ∈ ℕ0 → Σ𝑛 ∈ (ℤ≥‘𝑁)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) ∈ (0[,](3 / ((4 · ((2 · 𝑁) + 1)) · (9↑𝑁)))))
272	54, 271	eqeltrd 2833	1 ⊢ (𝑁 ∈ ℕ0 → ((log‘2) − Σ𝑛 ∈ (0...(𝑁 − 1))(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))) ∈ (0[,](3 / ((4 · ((2 · 𝑁) + 1)) · (9↑𝑁)))))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   ∧ w3a 1087   = wceq 1541   ∈ wcel 2106   ≠ wne 2940   class class class wbr 5147   ↦ cmpt 5230  dom cdm 5675  ‘cfv 6540  (class class class)co 7405  ℂcc 11104  ℝcr 11105  0cc0 11106  1c1 11107   + caddc 11109   · cmul 11111   < clt 11244   ≤ cle 11245   − cmin 11440   / cdiv 11867  ℕcn 12208  2c2 12263  3c3 12264  4c4 12265  8c8 12269  9c9 12270  ℕ₀cn0 12468  ℤcz 12554  ℤ_≥cuz 12818  [,]cicc 13323  ...cfz 13480  seqcseq 13962  ↑cexp 14023  abscabs 15177   ⇝ cli 15424  Σcsu 15628  logclog 26054

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7721  ax-inf2 9632  ax-cnex 11162  ax-resscn 11163  ax-1cn 11164  ax-icn 11165  ax-addcl 11166  ax-addrcl 11167  ax-mulcl 11168  ax-mulrcl 11169  ax-mulcom 11170  ax-addass 11171  ax-mulass 11172  ax-distr 11173  ax-i2m1 11174  ax-1ne0 11175  ax-1rid 11176  ax-rnegex 11177  ax-rrecex 11178  ax-cnre 11179  ax-pre-lttri 11180  ax-pre-lttrn 11181  ax-pre-ltadd 11182  ax-pre-mulgt0 11183  ax-pre-sup 11184  ax-addf 11185  ax-mulf 11186

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3376  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-tp 4632  df-op 4634  df-uni 4908  df-int 4950  df-iun 4998  df-iin 4999  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-se 5631  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6297  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-isom 6549  df-riota 7361  df-ov 7408  df-oprab 7409  df-mpo 7410  df-of 7666  df-om 7852  df-1st 7971  df-2nd 7972  df-supp 8143  df-frecs 8262  df-wrecs 8293  df-recs 8367  df-rdg 8406  df-1o 8462  df-2o 8463  df-oadd 8466  df-er 8699  df-map 8818  df-pm 8819  df-ixp 8888  df-en 8936  df-dom 8937  df-sdom 8938  df-fin 8939  df-fsupp 9358  df-fi 9402  df-sup 9433  df-inf 9434  df-oi 9501  df-card 9930  df-pnf 11246  df-mnf 11247  df-xr 11248  df-ltxr 11249  df-le 11250  df-sub 11442  df-neg 11443  df-div 11868  df-nn 12209  df-2 12271  df-3 12272  df-4 12273  df-5 12274  df-6 12275  df-7 12276  df-8 12277  df-9 12278  df-n0 12469  df-xnn0 12541  df-z 12555  df-dec 12674  df-uz 12819  df-q 12929  df-rp 12971  df-xneg 13088  df-xadd 13089  df-xmul 13090  df-ioo 13324  df-ioc 13325  df-ico 13326  df-icc 13327  df-fz 13481  df-fzo 13624  df-fl 13753  df-mod 13831  df-seq 13963  df-exp 14024  df-fac 14230  df-bc 14259  df-hash 14287  df-shft 15010  df-cj 15042  df-re 15043  df-im 15044  df-sqrt 15178  df-abs 15179  df-limsup 15411  df-clim 15428  df-rlim 15429  df-sum 15629  df-ef 16007  df-sin 16009  df-cos 16010  df-tan 16011  df-pi 16012  df-dvds 16194  df-struct 17076  df-sets 17093  df-slot 17111  df-ndx 17123  df-base 17141  df-ress 17170  df-plusg 17206  df-mulr 17207  df-starv 17208  df-sca 17209  df-vsca 17210  df-ip 17211  df-tset 17212  df-ple 17213  df-ds 17215  df-unif 17216  df-hom 17217  df-cco 17218  df-rest 17364  df-topn 17365  df-0g 17383  df-gsum 17384  df-topgen 17385  df-pt 17386  df-prds 17389  df-xrs 17444  df-qtop 17449  df-imas 17450  df-xps 17452  df-mre 17526  df-mrc 17527  df-acs 17529  df-mgm 18557  df-sgrp 18606  df-mnd 18622  df-submnd 18668  df-mulg 18945  df-cntz 19175  df-cmn 19644  df-psmet 20928  df-xmet 20929  df-met 20930  df-bl 20931  df-mopn 20932  df-fbas 20933  df-fg 20934  df-cnfld 20937  df-top 22387  df-topon 22404  df-topsp 22426  df-bases 22440  df-cld 22514  df-ntr 22515  df-cls 22516  df-nei 22593  df-lp 22631  df-perf 22632  df-cn 22722  df-cnp 22723  df-haus 22810  df-cmp 22882  df-tx 23057  df-hmeo 23250  df-fil 23341  df-fm 23433  df-flim 23434  df-flf 23435  df-xms 23817  df-ms 23818  df-tms 23819  df-cncf 24385  df-limc 25374  df-dv 25375  df-ulm 25880  df-log 26056  df-atan 26361

This theorem is referenced by:  log2ub  26443