Theorem log2tlbnd 26988

Description: Bound the error term in the series of log2cnv 26987. (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 14014	. . . 4 ⊢ (𝑁 ∈ ℕ0 → (0...(𝑁 − 1)) ∈ Fin)
2		elfznn0 13660	. . . . 5 ⊢ (𝑛 ∈ (0...(𝑁 − 1)) → 𝑛 ∈ ℕ0)
3		2re 12340	. . . . . . 7 ⊢ 2 ∈ ℝ
4		3nn 12345	. . . . . . . . 9 ⊢ 3 ∈ ℕ
5		2nn0 12543	. . . . . . . . . . 11 ⊢ 2 ∈ ℕ0
6		simpr 484	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → 𝑛 ∈ ℕ0)
7		nn0mulcl 12562	. . . . . . . . . . 11 ⊢ ((2 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → (2 · 𝑛) ∈ ℕ0)
8	5, 6, 7	sylancr 587	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → (2 · 𝑛) ∈ ℕ0)
9		nn0p1nn 12565	. . . . . . . . . 10 ⊢ ((2 · 𝑛) ∈ ℕ0 → ((2 · 𝑛) + 1) ∈ ℕ)
10	8, 9	syl 17	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → ((2 · 𝑛) + 1) ∈ ℕ)
11		nnmulcl 12290	. . . . . . . . 9 ⊢ ((3 ∈ ℕ ∧ ((2 · 𝑛) + 1) ∈ ℕ) → (3 · ((2 · 𝑛) + 1)) ∈ ℕ)
12	4, 10, 11	sylancr 587	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → (3 · ((2 · 𝑛) + 1)) ∈ ℕ)
13		9nn 12364	. . . . . . . . 9 ⊢ 9 ∈ ℕ
14		nnexpcl 14115	. . . . . . . . 9 ⊢ ((9 ∈ ℕ ∧ 𝑛 ∈ ℕ0) → (9↑𝑛) ∈ ℕ)
15	13, 6, 14	sylancr 587	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → (9↑𝑛) ∈ ℕ)
16	12, 15	nnmulcld 12319	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)) ∈ ℕ)
17		nndivre 12307	. . . . . . 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 11289	. . . . 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 15769	. . 3 ⊢ (𝑁 ∈ ℕ0 → Σ𝑛 ∈ (0...(𝑁 − 1))(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) ∈ ℂ)
22		eqid 2737	. . . . 5 ⊢ (ℤ≥‘𝑁) = (ℤ≥‘𝑁)
23		nn0z 12638	. . . . 5 ⊢ (𝑁 ∈ ℕ0 → 𝑁 ∈ ℤ)
24		eluznn0 12959	. . . . . 6 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → 𝑛 ∈ ℕ0)
25		oveq2 7439	. . . . . . . . . . 11 ⊢ (𝑘 = 𝑛 → (2 · 𝑘) = (2 · 𝑛))
26	25	oveq1d 7446	. . . . . . . . . 10 ⊢ (𝑘 = 𝑛 → ((2 · 𝑘) + 1) = ((2 · 𝑛) + 1))
27	26	oveq2d 7447	. . . . . . . . 9 ⊢ (𝑘 = 𝑛 → (3 · ((2 · 𝑘) + 1)) = (3 · ((2 · 𝑛) + 1)))
28		oveq2 7439	. . . . . . . . 9 ⊢ (𝑘 = 𝑛 → (9↑𝑘) = (9↑𝑛))
29	27, 28	oveq12d 7449	. . . . . . . 8 ⊢ (𝑘 = 𝑛 → ((3 · ((2 · 𝑘) + 1)) · (9↑𝑘)) = ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))
30	29	oveq2d 7447	. . . . . . 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 7464	. . . . . . 7 ⊢ (2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) ∈ V
33	30, 31, 32	fvmpt 7016	. . . . . 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 26987	. . . . . . 7 ⊢ seq0( + , (𝑘 ∈ ℕ0 ↦ (2 / ((3 · ((2 · 𝑘) + 1)) · (9↑𝑘))))) ⇝ (log‘2)
37		seqex 14044	. . . . . . . 8 ⊢ seq0( + , (𝑘 ∈ ℕ0 ↦ (2 / ((3 · ((2 · 𝑘) + 1)) · (9↑𝑘))))) ∈ V
38		fvex 6919	. . . . . . . 8 ⊢ (log‘2) ∈ V
39	37, 38	breldm 5919	. . . . . . 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 12920	. . . . . . 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 2841	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → ((𝑘 ∈ ℕ0 ↦ (2 / ((3 · ((2 · 𝑘) + 1)) · (9↑𝑘))))‘𝑛) ∈ ℂ)
45	41, 42, 44	iserex 15693	. . . . . 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 15801	. . . 4 ⊢ (𝑁 ∈ ℕ0 → Σ𝑛 ∈ (ℤ≥‘𝑁)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) ∈ ℝ)
48	47	recnd 11289	. . 3 ⊢ (𝑁 ∈ ℕ0 → Σ𝑛 ∈ (ℤ≥‘𝑁)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) ∈ ℂ)
49		0zd 12625	. . . . 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 15793	. . . 4 ⊢ (𝑁 ∈ ℕ0 → Σ𝑛 ∈ ℕ0 (2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) = (log‘2))
52	41, 22, 42, 43, 19, 40	isumsplit 15876	. . . 4 ⊢ (𝑁 ∈ ℕ0 → Σ𝑛 ∈ ℕ0 (2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) = (Σ𝑛 ∈ (0...(𝑁 − 1))(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) + Σ𝑛 ∈ (ℤ≥‘𝑁)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))))
53	51, 52	eqtr3d 2779	. . 3 ⊢ (𝑁 ∈ ℕ0 → (log‘2) = (Σ𝑛 ∈ (0...(𝑁 − 1))(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) + Σ𝑛 ∈ (ℤ≥‘𝑁)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))))
54	21, 48, 53	mvrladdd 11676	. 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 12368	. . . . . . 7 ⊢ 0 ≤ 2
57	56	a1i 11	. . . . . 6 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → 0 ≤ 2)
58	16	nnred 12281	. . . . . 6 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)) ∈ ℝ)
59	16	nngt0d 12315	. . . . . 6 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → 0 < ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))
60		divge0 12137	. . . . . 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 591	. . . 4 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → 0 ≤ (2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))))
63	22, 23, 34, 35, 46, 62	isumge0 15802	. . 3 ⊢ (𝑁 ∈ ℕ0 → 0 ≤ Σ𝑛 ∈ (ℤ≥‘𝑁)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))))
64		oveq2 7439	. . . . . . . . . 10 ⊢ (𝑘 = 𝑛 → ((1 / 9)↑𝑘) = ((1 / 9)↑𝑛))
65	64	oveq2d 7447	. . . . . . . . 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 7464	. . . . . . . . 9 ⊢ ((2 / (3 · ((2 · 𝑁) + 1))) · ((1 / 9)↑𝑛)) ∈ V
68	65, 66, 67	fvmpt 7016	. . . . . . . 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 12366	. . . . . . . . . . 11 ⊢ 9 ∈ ℂ
71	70	a1i 11	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → 9 ∈ ℂ)
72	13	nnne0i 12306	. . . . . . . . . . 11 ⊢ 9 ≠ 0
73	72	a1i 11	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → 9 ≠ 0)
74		nn0z 12638	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ℕ0 → 𝑛 ∈ ℤ)
75	74	adantl 481	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → 𝑛 ∈ ℤ)
76	71, 73, 75	exprecd 14194	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → ((1 / 9)↑𝑛) = (1 / (9↑𝑛)))
77	76	oveq2d 7447	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → ((2 / (3 · ((2 · 𝑁) + 1))) · ((1 / 9)↑𝑛)) = ((2 / (3 · ((2 · 𝑁) + 1))) · (1 / (9↑𝑛))))
78		nn0mulcl 12562	. . . . . . . . . . . . . . 15 ⊢ ((2 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (2 · 𝑁) ∈ ℕ0)
79	5, 78	mpan 690	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ ℕ0 → (2 · 𝑁) ∈ ℕ0)
80		nn0p1nn 12565	. . . . . . . . . . . . . 14 ⊢ ((2 · 𝑁) ∈ ℕ0 → ((2 · 𝑁) + 1) ∈ ℕ)
81	79, 80	syl 17	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ ℕ0 → ((2 · 𝑁) + 1) ∈ ℕ)
82		nnmulcl 12290	. . . . . . . . . . . . 13 ⊢ ((3 ∈ ℕ ∧ ((2 · 𝑁) + 1) ∈ ℕ) → (3 · ((2 · 𝑁) + 1)) ∈ ℕ)
83	4, 81, 82	sylancr 587	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℕ0 → (3 · ((2 · 𝑁) + 1)) ∈ ℕ)
84		nndivre 12307	. . . . . . . . . . . 12 ⊢ ((2 ∈ ℝ ∧ (3 · ((2 · 𝑁) + 1)) ∈ ℕ) → (2 / (3 · ((2 · 𝑁) + 1))) ∈ ℝ)
85	3, 83, 84	sylancr 587	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℕ0 → (2 / (3 · ((2 · 𝑁) + 1))) ∈ ℝ)
86	85	recnd 11289	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ0 → (2 / (3 · ((2 · 𝑁) + 1))) ∈ ℂ)
87	86	adantr 480	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → (2 / (3 · ((2 · 𝑁) + 1))) ∈ ℂ)
88	15	nncnd 12282	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → (9↑𝑛) ∈ ℂ)
89	15	nnne0d 12316	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → (9↑𝑛) ≠ 0)
90	87, 88, 89	divrecd 12046	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → ((2 / (3 · ((2 · 𝑁) + 1))) / (9↑𝑛)) = ((2 / (3 · ((2 · 𝑁) + 1))) · (1 / (9↑𝑛))))
91		2cnd 12344	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → 2 ∈ ℂ)
92	83	adantr 480	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → (3 · ((2 · 𝑁) + 1)) ∈ ℕ)
93	92	nncnd 12282	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → (3 · ((2 · 𝑁) + 1)) ∈ ℂ)
94	92	nnne0d 12316	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → (3 · ((2 · 𝑁) + 1)) ≠ 0)
95	91, 93, 88, 94, 89	divdiv1d 12074	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → ((2 / (3 · ((2 · 𝑁) + 1))) / (9↑𝑛)) = (2 / ((3 · ((2 · 𝑁) + 1)) · (9↑𝑛))))
96	77, 90, 95	3eqtr2d 2783	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → ((2 / (3 · ((2 · 𝑁) + 1))) · ((1 / 9)↑𝑛)) = (2 / ((3 · ((2 · 𝑁) + 1)) · (9↑𝑛))))
97	69, 96	eqtrd 2777	. . . . . 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 12319	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → ((3 · ((2 · 𝑁) + 1)) · (9↑𝑛)) ∈ ℕ)
100		nndivre 12307	. . . . . . 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 480	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (2 · 𝑁) ∈ ℕ0)
104	103	nn0red 12588	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (2 · 𝑁) ∈ ℝ)
105	5, 24, 7	sylancr 587	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (2 · 𝑛) ∈ ℕ0)
106	105	nn0red 12588	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (2 · 𝑛) ∈ ℝ)
107		1red 11262	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → 1 ∈ ℝ)
108		eluzle 12891	. . . . . . . . . . 11 ⊢ (𝑛 ∈ (ℤ≥‘𝑁) → 𝑁 ≤ 𝑛)
109	108	adantl 481	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → 𝑁 ≤ 𝑛)
110		nn0re 12535	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℕ0 → 𝑁 ∈ ℝ)
111	110	adantr 480	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → 𝑁 ∈ ℝ)
112	24	nn0red 12588	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → 𝑛 ∈ ℝ)
113	3	a1i 11	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → 2 ∈ ℝ)
114		2pos 12369	. . . . . . . . . . . 12 ⊢ 0 < 2
115	114	a1i 11	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → 0 < 2)
116		lemul2 12120	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℝ ∧ 𝑛 ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → (𝑁 ≤ 𝑛 ↔ (2 · 𝑁) ≤ (2 · 𝑛)))
117	111, 112, 113, 115, 116	syl112anc 1376	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (𝑁 ≤ 𝑛 ↔ (2 · 𝑁) ≤ (2 · 𝑛)))
118	109, 117	mpbid 232	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (2 · 𝑁) ≤ (2 · 𝑛))
119	104, 106, 107, 118	leadd1dd 11877	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → ((2 · 𝑁) + 1) ≤ ((2 · 𝑛) + 1))
120	81	adantr 480	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → ((2 · 𝑁) + 1) ∈ ℕ)
121	120	nnred 12281	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → ((2 · 𝑁) + 1) ∈ ℝ)
122	24, 10	syldan 591	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → ((2 · 𝑛) + 1) ∈ ℕ)
123	122	nnred 12281	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → ((2 · 𝑛) + 1) ∈ ℝ)
124		3re 12346	. . . . . . . . . 10 ⊢ 3 ∈ ℝ
125	124	a1i 11	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → 3 ∈ ℝ)
126		3pos 12371	. . . . . . . . . 10 ⊢ 0 < 3
127	126	a1i 11	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → 0 < 3)
128		lemul2 12120	. . . . . . . . 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 1376	. . . . . . . 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 12281	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (3 · ((2 · 𝑁) + 1)) ∈ ℝ)
133	24, 12	syldan 591	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (3 · ((2 · 𝑛) + 1)) ∈ ℕ)
134	133	nnred 12281	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (3 · ((2 · 𝑛) + 1)) ∈ ℝ)
135	13, 24, 14	sylancr 587	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (9↑𝑛) ∈ ℕ)
136	135	nnred 12281	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (9↑𝑛) ∈ ℝ)
137	135	nngt0d 12315	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → 0 < (9↑𝑛))
138		lemul1 12119	. . . . . . . 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 1376	. . . . . . 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 591	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → ((3 · ((2 · 𝑁) + 1)) · (9↑𝑛)) ∈ ℕ)
142	141	nnred 12281	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → ((3 · ((2 · 𝑁) + 1)) · (9↑𝑛)) ∈ ℝ)
143	141	nngt0d 12315	. . . . . . 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 12158	. . . . . . 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 1388	. . . . . 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 12365	. . . . . . . . . . . 12 ⊢ 9 ∈ ℝ
150	149, 72	rereccli 12032	. . . . . . . . . . 11 ⊢ (1 / 9) ∈ ℝ
151	150	recni 11275	. . . . . . . . . 10 ⊢ (1 / 9) ∈ ℂ
152	151	a1i 11	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ0 → (1 / 9) ∈ ℂ)
153		0re 11263	. . . . . . . . . . . . 13 ⊢ 0 ∈ ℝ
154		9pos 12379	. . . . . . . . . . . . . 14 ⊢ 0 < 9
155	149, 154	recgt0ii 12174	. . . . . . . . . . . . 13 ⊢ 0 < (1 / 9)
156	153, 150, 155	ltleii 11384	. . . . . . . . . . . 12 ⊢ 0 ≤ (1 / 9)
157		absid 15335	. . . . . . . . . . . 12 ⊢ (((1 / 9) ∈ ℝ ∧ 0 ≤ (1 / 9)) → (abs‘(1 / 9)) = (1 / 9))
158	150, 156, 157	mp2an 692	. . . . . . . . . . 11 ⊢ (abs‘(1 / 9)) = (1 / 9)
159		1lt9 12472	. . . . . . . . . . . . 13 ⊢ 1 < 9
160		recgt1i 12165	. . . . . . . . . . . . 13 ⊢ ((9 ∈ ℝ ∧ 1 < 9) → (0 < (1 / 9) ∧ (1 / 9) < 1))
161	149, 159, 160	mp2an 692	. . . . . . . . . . . 12 ⊢ (0 < (1 / 9) ∧ (1 / 9) < 1)
162	161	simpri 485	. . . . . . . . . . 11 ⊢ (1 / 9) < 1
163	158, 162	eqbrtri 5164	. . . . . . . . . 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 7464	. . . . . . . . . . 11 ⊢ ((1 / 9)↑𝑛) ∈ V
167	64, 165, 166	fvmpt 7016	. . . . . . . . . 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 15907	. . . . . . . 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 14194	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ0 → ((1 / 9)↑𝑁) = (1 / (9↑𝑁)))
173	70, 72	dividi 12000	. . . . . . . . . . . . 13 ⊢ (9 / 9) = 1
174	173	oveq1i 7441	. . . . . . . . . . . 12 ⊢ ((9 / 9) − (1 / 9)) = (1 − (1 / 9))
175		ax-1cn 11213	. . . . . . . . . . . . . 14 ⊢ 1 ∈ ℂ
176	70, 72	pm3.2i 470	. . . . . . . . . . . . . 14 ⊢ (9 ∈ ℂ ∧ 9 ≠ 0)
177		divsubdir 11961	. . . . . . . . . . . . . 14 ⊢ ((9 ∈ ℂ ∧ 1 ∈ ℂ ∧ (9 ∈ ℂ ∧ 9 ≠ 0)) → ((9 − 1) / 9) = ((9 / 9) − (1 / 9)))
178	70, 175, 176, 177	mp3an 1463	. . . . . . . . . . . . 13 ⊢ ((9 − 1) / 9) = ((9 / 9) − (1 / 9))
179		9m1e8 12400	. . . . . . . . . . . . . 14 ⊢ (9 − 1) = 8
180	179	oveq1i 7441	. . . . . . . . . . . . 13 ⊢ ((9 − 1) / 9) = (8 / 9)
181	178, 180	eqtr3i 2767	. . . . . . . . . . . 12 ⊢ ((9 / 9) − (1 / 9)) = (8 / 9)
182	174, 181	eqtr3i 2767	. . . . . . . . . . 11 ⊢ (1 − (1 / 9)) = (8 / 9)
183	182	a1i 11	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ0 → (1 − (1 / 9)) = (8 / 9))
184	172, 183	oveq12d 7449	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ0 → (((1 / 9)↑𝑁) / (1 − (1 / 9))) = ((1 / (9↑𝑁)) / (8 / 9)))
185	175	a1i 11	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ0 → 1 ∈ ℂ)
186		nnexpcl 14115	. . . . . . . . . . . 12 ⊢ ((9 ∈ ℕ ∧ 𝑁 ∈ ℕ0) → (9↑𝑁) ∈ ℕ)
187	13, 186	mpan 690	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℕ0 → (9↑𝑁) ∈ ℕ)
188	187	nncnd 12282	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ0 → (9↑𝑁) ∈ ℂ)
189		8cn 12363	. . . . . . . . . . . 12 ⊢ 8 ∈ ℂ
190	189, 70, 72	divcli 12009	. . . . . . . . . . 11 ⊢ (8 / 9) ∈ ℂ
191	190	a1i 11	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ0 → (8 / 9) ∈ ℂ)
192	187	nnne0d 12316	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ0 → (9↑𝑁) ≠ 0)
193		8nn 12361	. . . . . . . . . . . . 13 ⊢ 8 ∈ ℕ
194	193	nnne0i 12306	. . . . . . . . . . . 12 ⊢ 8 ≠ 0
195	189, 70, 194, 72	divne0i 12015	. . . . . . . . . . 11 ⊢ (8 / 9) ≠ 0
196	195	a1i 11	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ0 → (8 / 9) ≠ 0)
197	185, 188, 191, 192, 196	divdiv32d 12068	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ0 → ((1 / (9↑𝑁)) / (8 / 9)) = ((1 / (8 / 9)) / (9↑𝑁)))
198		recdiv 11973	. . . . . . . . . . . 12 ⊢ (((8 ∈ ℂ ∧ 8 ≠ 0) ∧ (9 ∈ ℂ ∧ 9 ≠ 0)) → (1 / (8 / 9)) = (9 / 8))
199	189, 194, 70, 72, 198	mp4an 693	. . . . . . . . . . 11 ⊢ (1 / (8 / 9)) = (9 / 8)
200	199	oveq1i 7441	. . . . . . . . . 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 12074	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ0 → ((9 / 8) / (9↑𝑁)) = (9 / (8 · (9↑𝑁))))
204	200, 203	eqtrid 2789	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ0 → ((1 / (8 / 9)) / (9↑𝑁)) = (9 / (8 · (9↑𝑁))))
205	184, 197, 204	3eqtrd 2781	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ0 → (((1 / 9)↑𝑁) / (1 − (1 / 9))) = (9 / (8 · (9↑𝑁))))
206	169, 205	breqtrd 5169	. . . . . . 7 ⊢ (𝑁 ∈ ℕ0 → seq𝑁( + , (𝑘 ∈ ℕ0 ↦ ((1 / 9)↑𝑘))) ⇝ (9 / (8 · (9↑𝑁))))
207		expcl 14120	. . . . . . . . 9 ⊢ (((1 / 9) ∈ ℂ ∧ 𝑛 ∈ ℕ0) → ((1 / 9)↑𝑛) ∈ ℂ)
208	151, 24, 207	sylancr 587	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → ((1 / 9)↑𝑛) ∈ ℂ)
209	168, 208	eqeltrd 2841	. . . . . . 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 7447	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → ((2 / (3 · ((2 · 𝑁) + 1))) · ((𝑘 ∈ ℕ0 ↦ ((1 / 9)↑𝑘))‘𝑛)) = ((2 / (3 · ((2 · 𝑁) + 1))) · ((1 / 9)↑𝑛)))
212	210, 211	eqtr4d 2780	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → ((𝑘 ∈ ℕ0 ↦ ((2 / (3 · ((2 · 𝑁) + 1))) · ((1 / 9)↑𝑘)))‘𝑛) = ((2 / (3 · ((2 · 𝑁) + 1))) · ((𝑘 ∈ ℕ0 ↦ ((1 / 9)↑𝑘))‘𝑛)))
213	22, 23, 86, 206, 209, 212	isermulc2 15694	. . . . . 6 ⊢ (𝑁 ∈ ℕ0 → seq𝑁( + , (𝑘 ∈ ℕ0 ↦ ((2 / (3 · ((2 · 𝑁) + 1))) · ((1 / 9)↑𝑘)))) ⇝ ((2 / (3 · ((2 · 𝑁) + 1))) · (9 / (8 · (9↑𝑁)))))
214		seqex 14044	. . . . . . 7 ⊢ seq𝑁( + , (𝑘 ∈ ℕ0 ↦ ((2 / (3 · ((2 · 𝑁) + 1))) · ((1 / 9)↑𝑘)))) ∈ V
215		ovex 7464	. . . . . . 7 ⊢ ((2 / (3 · ((2 · 𝑁) + 1))) · (9 / (8 · (9↑𝑁)))) ∈ V
216	214, 215	breldm 5919	. . . . . 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 15880	. . . 4 ⊢ (𝑁 ∈ ℕ0 → Σ𝑛 ∈ (ℤ≥‘𝑁)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) ≤ Σ𝑛 ∈ (ℤ≥‘𝑁)(2 / ((3 · ((2 · 𝑁) + 1)) · (9↑𝑛))))
219	102	recnd 11289	. . . . 5 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (2 / ((3 · ((2 · 𝑁) + 1)) · (9↑𝑛))) ∈ ℂ)
220		3cn 12347	. . . . . . . . . . . 12 ⊢ 3 ∈ ℂ
221		4cn 12351	. . . . . . . . . . . 12 ⊢ 4 ∈ ℂ
222		2cn 12341	. . . . . . . . . . . 12 ⊢ 2 ∈ ℂ
223		4ne0 12374	. . . . . . . . . . . 12 ⊢ 4 ≠ 0
224		3ne0 12372	. . . . . . . . . . . 12 ⊢ 3 ≠ 0
225		2ne0 12370	. . . . . . . . . . . 12 ⊢ 2 ≠ 0
226	220, 221, 222, 220, 223, 224, 225	divdivdivi 12030	. . . . . . . . . . 11 ⊢ ((3 / 4) / (2 / 3)) = ((3 · 3) / (4 · 2))
227		3t3e9 12433	. . . . . . . . . . . 12 ⊢ (3 · 3) = 9
228		4t2e8 12434	. . . . . . . . . . . 12 ⊢ (4 · 2) = 8
229	227, 228	oveq12i 7443	. . . . . . . . . . 11 ⊢ ((3 · 3) / (4 · 2)) = (9 / 8)
230	226, 229	eqtri 2765	. . . . . . . . . 10 ⊢ ((3 / 4) / (2 / 3)) = (9 / 8)
231	230	oveq2i 7442	. . . . . . . . 9 ⊢ ((2 / 3) · ((3 / 4) / (2 / 3))) = ((2 / 3) · (9 / 8))
232	220, 221, 223	divcli 12009	. . . . . . . . . 10 ⊢ (3 / 4) ∈ ℂ
233	222, 220, 224	divcli 12009	. . . . . . . . . 10 ⊢ (2 / 3) ∈ ℂ
234	222, 220, 225, 224	divne0i 12015	. . . . . . . . . 10 ⊢ (2 / 3) ≠ 0
235	232, 233, 234	divcan2i 12010	. . . . . . . . 9 ⊢ ((2 / 3) · ((3 / 4) / (2 / 3))) = (3 / 4)
236	231, 235	eqtr3i 2767	. . . . . . . 8 ⊢ ((2 / 3) · (9 / 8)) = (3 / 4)
237	236	oveq1i 7441	. . . . . . 7 ⊢ (((2 / 3) · (9 / 8)) / (((2 · 𝑁) + 1) · (9↑𝑁))) = ((3 / 4) / (((2 · 𝑁) + 1) · (9↑𝑁)))
238		2cnd 12344	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ0 → 2 ∈ ℂ)
239	220	a1i 11	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ0 → 3 ∈ ℂ)
240	81	nncnd 12282	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ0 → ((2 · 𝑁) + 1) ∈ ℂ)
241	224	a1i 11	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ0 → 3 ≠ 0)
242	81	nnne0d 12316	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ0 → ((2 · 𝑁) + 1) ≠ 0)
243	238, 239, 240, 241, 242	divdiv1d 12074	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ0 → ((2 / 3) / ((2 · 𝑁) + 1)) = (2 / (3 · ((2 · 𝑁) + 1))))
244	243, 203	oveq12d 7449	. . . . . . . 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 12009	. . . . . . . . . 10 ⊢ (9 / 8) ∈ ℂ
247	246	a1i 11	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ0 → (9 / 8) ∈ ℂ)
248	245, 240, 247, 188, 242, 192	divmuldivd 12084	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ0 → (((2 / 3) / ((2 · 𝑁) + 1)) · ((9 / 8) / (9↑𝑁))) = (((2 / 3) · (9 / 8)) / (((2 · 𝑁) + 1) · (9↑𝑁))))
249	244, 248	eqtr3d 2779	. . . . . . 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 11284	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ0 → ((4 · ((2 · 𝑁) + 1)) · (9↑𝑁)) = (4 · (((2 · 𝑁) + 1) · (9↑𝑁))))
252	251	oveq2d 7447	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ0 → (3 / ((4 · ((2 · 𝑁) + 1)) · (9↑𝑁))) = (3 / (4 · (((2 · 𝑁) + 1) · (9↑𝑁)))))
253	81, 187	nnmulcld 12319	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ0 → (((2 · 𝑁) + 1) · (9↑𝑁)) ∈ ℕ)
254	253	nncnd 12282	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ0 → (((2 · 𝑁) + 1) · (9↑𝑁)) ∈ ℂ)
255	223	a1i 11	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ0 → 4 ≠ 0)
256	253	nnne0d 12316	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ0 → (((2 · 𝑁) + 1) · (9↑𝑁)) ≠ 0)
257	239, 250, 254, 255, 256	divdiv1d 12074	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ0 → ((3 / 4) / (((2 · 𝑁) + 1) · (9↑𝑁))) = (3 / (4 · (((2 · 𝑁) + 1) · (9↑𝑁)))))
258	252, 257	eqtr4d 2780	. . . . . . 7 ⊢ (𝑁 ∈ ℕ0 → (3 / ((4 · ((2 · 𝑁) + 1)) · (9↑𝑁))) = ((3 / 4) / (((2 · 𝑁) + 1) · (9↑𝑁))))
259	237, 249, 258	3eqtr4a 2803	. . . . . 6 ⊢ (𝑁 ∈ ℕ0 → ((2 / (3 · ((2 · 𝑁) + 1))) · (9 / (8 · (9↑𝑁)))) = (3 / ((4 · ((2 · 𝑁) + 1)) · (9↑𝑁))))
260	213, 259	breqtrd 5169	. . . . 5 ⊢ (𝑁 ∈ ℕ0 → seq𝑁( + , (𝑘 ∈ ℕ0 ↦ ((2 / (3 · ((2 · 𝑁) + 1))) · ((1 / 9)↑𝑘)))) ⇝ (3 / ((4 · ((2 · 𝑁) + 1)) · (9↑𝑁))))
261	22, 23, 98, 219, 260	isumclim 15793	. . . 4 ⊢ (𝑁 ∈ ℕ0 → Σ𝑛 ∈ (ℤ≥‘𝑁)(2 / ((3 · ((2 · 𝑁) + 1)) · (9↑𝑛))) = (3 / ((4 · ((2 · 𝑁) + 1)) · (9↑𝑁))))
262	218, 261	breqtrd 5169	. . 3 ⊢ (𝑁 ∈ ℕ0 → Σ𝑛 ∈ (ℤ≥‘𝑁)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) ≤ (3 / ((4 · ((2 · 𝑁) + 1)) · (9↑𝑁))))
263		4nn 12349	. . . . . . 7 ⊢ 4 ∈ ℕ
264		nnmulcl 12290	. . . . . . 7 ⊢ ((4 ∈ ℕ ∧ ((2 · 𝑁) + 1) ∈ ℕ) → (4 · ((2 · 𝑁) + 1)) ∈ ℕ)
265	263, 81, 264	sylancr 587	. . . . . 6 ⊢ (𝑁 ∈ ℕ0 → (4 · ((2 · 𝑁) + 1)) ∈ ℕ)
266	265, 187	nnmulcld 12319	. . . . 5 ⊢ (𝑁 ∈ ℕ0 → ((4 · ((2 · 𝑁) + 1)) · (9↑𝑁)) ∈ ℕ)
267		nndivre 12307	. . . . 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 13452	. . . 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 1343	. 2 ⊢ (𝑁 ∈ ℕ0 → Σ𝑛 ∈ (ℤ≥‘𝑁)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) ∈ (0[,](3 / ((4 · ((2 · 𝑁) + 1)) · (9↑𝑁)))))
272	54, 271	eqeltrd 2841	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 1540   ∈ wcel 2108   ≠ wne 2940   class class class wbr 5143   ↦ cmpt 5225  dom cdm 5685  ‘cfv 6561  (class class class)co 7431  ℂcc 11153  ℝcr 11154  0cc0 11155  1c1 11156   + caddc 11158   · cmul 11160   < clt 11295   ≤ cle 11296   − cmin 11492   / cdiv 11920  ℕcn 12266  2c2 12321  3c3 12322  4c4 12323  8c8 12327  9c9 12328  ℕ₀cn0 12526  ℤcz 12613  ℤ_≥cuz 12878  [,]cicc 13390  ...cfz 13547  seqcseq 14042  ↑cexp 14102  abscabs 15273   ⇝ cli 15520  Σcsu 15722  logclog 26596

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-inf2 9681  ax-cnex 11211  ax-resscn 11212  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-addrcl 11216  ax-mulcl 11217  ax-mulrcl 11218  ax-mulcom 11219  ax-addass 11220  ax-mulass 11221  ax-distr 11222  ax-i2m1 11223  ax-1ne0 11224  ax-1rid 11225  ax-rnegex 11226  ax-rrecex 11227  ax-cnre 11228  ax-pre-lttri 11229  ax-pre-lttrn 11230  ax-pre-ltadd 11231  ax-pre-mulgt0 11232  ax-pre-sup 11233  ax-addf 11234

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3380  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-tp 4631  df-op 4633  df-uni 4908  df-int 4947  df-iun 4993  df-iin 4994  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-se 5638  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-isom 6570  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-of 7697  df-om 7888  df-1st 8014  df-2nd 8015  df-supp 8186  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-1o 8506  df-2o 8507  df-oadd 8510  df-er 8745  df-map 8868  df-pm 8869  df-ixp 8938  df-en 8986  df-dom 8987  df-sdom 8988  df-fin 8989  df-fsupp 9402  df-fi 9451  df-sup 9482  df-inf 9483  df-oi 9550  df-card 9979  df-pnf 11297  df-mnf 11298  df-xr 11299  df-ltxr 11300  df-le 11301  df-sub 11494  df-neg 11495  df-div 11921  df-nn 12267  df-2 12329  df-3 12330  df-4 12331  df-5 12332  df-6 12333  df-7 12334  df-8 12335  df-9 12336  df-n0 12527  df-xnn0 12600  df-z 12614  df-dec 12734  df-uz 12879  df-q 12991  df-rp 13035  df-xneg 13154  df-xadd 13155  df-xmul 13156  df-ioo 13391  df-ioc 13392  df-ico 13393  df-icc 13394  df-fz 13548  df-fzo 13695  df-fl 13832  df-mod 13910  df-seq 14043  df-exp 14103  df-fac 14313  df-bc 14342  df-hash 14370  df-shft 15106  df-cj 15138  df-re 15139  df-im 15140  df-sqrt 15274  df-abs 15275  df-limsup 15507  df-clim 15524  df-rlim 15525  df-sum 15723  df-ef 16103  df-sin 16105  df-cos 16106  df-tan 16107  df-pi 16108  df-dvds 16291  df-struct 17184  df-sets 17201  df-slot 17219  df-ndx 17231  df-base 17248  df-ress 17275  df-plusg 17310  df-mulr 17311  df-starv 17312  df-sca 17313  df-vsca 17314  df-ip 17315  df-tset 17316  df-ple 17317  df-ds 17319  df-unif 17320  df-hom 17321  df-cco 17322  df-rest 17467  df-topn 17468  df-0g 17486  df-gsum 17487  df-topgen 17488  df-pt 17489  df-prds 17492  df-xrs 17547  df-qtop 17552  df-imas 17553  df-xps 17555  df-mre 17629  df-mrc 17630  df-acs 17632  df-mgm 18653  df-sgrp 18732  df-mnd 18748  df-submnd 18797  df-mulg 19086  df-cntz 19335  df-cmn 19800  df-psmet 21356  df-xmet 21357  df-met 21358  df-bl 21359  df-mopn 21360  df-fbas 21361  df-fg 21362  df-cnfld 21365  df-top 22900  df-topon 22917  df-topsp 22939  df-bases 22953  df-cld 23027  df-ntr 23028  df-cls 23029  df-nei 23106  df-lp 23144  df-perf 23145  df-cn 23235  df-cnp 23236  df-haus 23323  df-cmp 23395  df-tx 23570  df-hmeo 23763  df-fil 23854  df-fm 23946  df-flim 23947  df-flf 23948  df-xms 24330  df-ms 24331  df-tms 24332  df-cncf 24904  df-limc 25901  df-dv 25902  df-ulm 26420  df-log 26598  df-atan 26910

This theorem is referenced by:  log2ub  26992