Theorem log2tlbnd 26000

Description: Bound the error term in the series of log2cnv 25999. (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 13621	. . . 4 ⊢ (𝑁 ∈ ℕ0 → (0...(𝑁 − 1)) ∈ Fin)
2		elfznn0 13278	. . . . 5 ⊢ (𝑛 ∈ (0...(𝑁 − 1)) → 𝑛 ∈ ℕ0)
3		2re 11977	. . . . . . 7 ⊢ 2 ∈ ℝ
4		3nn 11982	. . . . . . . . 9 ⊢ 3 ∈ ℕ
5		2nn0 12180	. . . . . . . . . . 11 ⊢ 2 ∈ ℕ0
6		simpr 484	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → 𝑛 ∈ ℕ0)
7		nn0mulcl 12199	. . . . . . . . . . 11 ⊢ ((2 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → (2 · 𝑛) ∈ ℕ0)
8	5, 6, 7	sylancr 586	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → (2 · 𝑛) ∈ ℕ0)
9		nn0p1nn 12202	. . . . . . . . . 10 ⊢ ((2 · 𝑛) ∈ ℕ0 → ((2 · 𝑛) + 1) ∈ ℕ)
10	8, 9	syl 17	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → ((2 · 𝑛) + 1) ∈ ℕ)
11		nnmulcl 11927	. . . . . . . . 9 ⊢ ((3 ∈ ℕ ∧ ((2 · 𝑛) + 1) ∈ ℕ) → (3 · ((2 · 𝑛) + 1)) ∈ ℕ)
12	4, 10, 11	sylancr 586	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → (3 · ((2 · 𝑛) + 1)) ∈ ℕ)
13		9nn 12001	. . . . . . . . 9 ⊢ 9 ∈ ℕ
14		nnexpcl 13723	. . . . . . . . 9 ⊢ ((9 ∈ ℕ ∧ 𝑛 ∈ ℕ0) → (9↑𝑛) ∈ ℕ)
15	13, 6, 14	sylancr 586	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → (9↑𝑛) ∈ ℕ)
16	12, 15	nnmulcld 11956	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)) ∈ ℕ)
17		nndivre 11944	. . . . . . 7 ⊢ ((2 ∈ ℝ ∧ ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)) ∈ ℕ) → (2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) ∈ ℝ)
18	3, 16, 17	sylancr 586	. . . . . 6 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → (2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) ∈ ℝ)
19	18	recnd 10934	. . . . 5 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → (2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) ∈ ℂ)
20	2, 19	sylan2 592	. . . 4 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (0...(𝑁 − 1))) → (2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) ∈ ℂ)
21	1, 20	fsumcl 15373	. . 3 ⊢ (𝑁 ∈ ℕ0 → Σ𝑛 ∈ (0...(𝑁 − 1))(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) ∈ ℂ)
22		eqid 2738	. . . . 5 ⊢ (ℤ≥‘𝑁) = (ℤ≥‘𝑁)
23		nn0z 12273	. . . . 5 ⊢ (𝑁 ∈ ℕ0 → 𝑁 ∈ ℤ)
24		eluznn0 12586	. . . . . 6 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → 𝑛 ∈ ℕ0)
25		oveq2 7263	. . . . . . . . . . 11 ⊢ (𝑘 = 𝑛 → (2 · 𝑘) = (2 · 𝑛))
26	25	oveq1d 7270	. . . . . . . . . 10 ⊢ (𝑘 = 𝑛 → ((2 · 𝑘) + 1) = ((2 · 𝑛) + 1))
27	26	oveq2d 7271	. . . . . . . . 9 ⊢ (𝑘 = 𝑛 → (3 · ((2 · 𝑘) + 1)) = (3 · ((2 · 𝑛) + 1)))
28		oveq2 7263	. . . . . . . . 9 ⊢ (𝑘 = 𝑛 → (9↑𝑘) = (9↑𝑛))
29	27, 28	oveq12d 7273	. . . . . . . 8 ⊢ (𝑘 = 𝑛 → ((3 · ((2 · 𝑘) + 1)) · (9↑𝑘)) = ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))
30	29	oveq2d 7271	. . . . . . 7 ⊢ (𝑘 = 𝑛 → (2 / ((3 · ((2 · 𝑘) + 1)) · (9↑𝑘))) = (2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))))
31		eqid 2738	. . . . . . 7 ⊢ (𝑘 ∈ ℕ0 ↦ (2 / ((3 · ((2 · 𝑘) + 1)) · (9↑𝑘)))) = (𝑘 ∈ ℕ0 ↦ (2 / ((3 · ((2 · 𝑘) + 1)) · (9↑𝑘))))
32		ovex 7288	. . . . . . 7 ⊢ (2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) ∈ V
33	30, 31, 32	fvmpt 6857	. . . . . 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 590	. . . . 5 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) ∈ ℝ)
36	31	log2cnv 25999	. . . . . . 7 ⊢ seq0( + , (𝑘 ∈ ℕ0 ↦ (2 / ((3 · ((2 · 𝑘) + 1)) · (9↑𝑘))))) ⇝ (log‘2)
37		seqex 13651	. . . . . . . 8 ⊢ seq0( + , (𝑘 ∈ ℕ0 ↦ (2 / ((3 · ((2 · 𝑘) + 1)) · (9↑𝑘))))) ∈ V
38		fvex 6769	. . . . . . . 8 ⊢ (log‘2) ∈ V
39	37, 38	breldm 5806	. . . . . . 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 12549	. . . . . . 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 2839	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → ((𝑘 ∈ ℕ0 ↦ (2 / ((3 · ((2 · 𝑘) + 1)) · (9↑𝑘))))‘𝑛) ∈ ℂ)
45	41, 42, 44	iserex 15296	. . . . . 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 15405	. . . 4 ⊢ (𝑁 ∈ ℕ0 → Σ𝑛 ∈ (ℤ≥‘𝑁)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) ∈ ℝ)
48	47	recnd 10934	. . 3 ⊢ (𝑁 ∈ ℕ0 → Σ𝑛 ∈ (ℤ≥‘𝑁)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) ∈ ℂ)
49		0zd 12261	. . . . 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 15397	. . . 4 ⊢ (𝑁 ∈ ℕ0 → Σ𝑛 ∈ ℕ0 (2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) = (log‘2))
52	41, 22, 42, 43, 19, 40	isumsplit 15480	. . . 4 ⊢ (𝑁 ∈ ℕ0 → Σ𝑛 ∈ ℕ0 (2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) = (Σ𝑛 ∈ (0...(𝑁 − 1))(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) + Σ𝑛 ∈ (ℤ≥‘𝑁)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))))
53	51, 52	eqtr3d 2780	. . 3 ⊢ (𝑁 ∈ ℕ0 → (log‘2) = (Σ𝑛 ∈ (0...(𝑁 − 1))(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) + Σ𝑛 ∈ (ℤ≥‘𝑁)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))))
54	21, 48, 53	mvrladdd 11318	. 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 12005	. . . . . . 7 ⊢ 0 ≤ 2
57	56	a1i 11	. . . . . 6 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → 0 ≤ 2)
58	16	nnred 11918	. . . . . 6 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)) ∈ ℝ)
59	16	nngt0d 11952	. . . . . 6 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → 0 < ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))
60		divge0 11774	. . . . . 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 835	. . . . 5 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → 0 ≤ (2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))))
62	24, 61	syldan 590	. . . 4 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → 0 ≤ (2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))))
63	22, 23, 34, 35, 46, 62	isumge0 15406	. . 3 ⊢ (𝑁 ∈ ℕ0 → 0 ≤ Σ𝑛 ∈ (ℤ≥‘𝑁)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))))
64		oveq2 7263	. . . . . . . . . 10 ⊢ (𝑘 = 𝑛 → ((1 / 9)↑𝑘) = ((1 / 9)↑𝑛))
65	64	oveq2d 7271	. . . . . . . . 9 ⊢ (𝑘 = 𝑛 → ((2 / (3 · ((2 · 𝑁) + 1))) · ((1 / 9)↑𝑘)) = ((2 / (3 · ((2 · 𝑁) + 1))) · ((1 / 9)↑𝑛)))
66		eqid 2738	. . . . . . . . 9 ⊢ (𝑘 ∈ ℕ0 ↦ ((2 / (3 · ((2 · 𝑁) + 1))) · ((1 / 9)↑𝑘))) = (𝑘 ∈ ℕ0 ↦ ((2 / (3 · ((2 · 𝑁) + 1))) · ((1 / 9)↑𝑘)))
67		ovex 7288	. . . . . . . . 9 ⊢ ((2 / (3 · ((2 · 𝑁) + 1))) · ((1 / 9)↑𝑛)) ∈ V
68	65, 66, 67	fvmpt 6857	. . . . . . . 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 12003	. . . . . . . . . . 11 ⊢ 9 ∈ ℂ
71	70	a1i 11	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → 9 ∈ ℂ)
72	13	nnne0i 11943	. . . . . . . . . . 11 ⊢ 9 ≠ 0
73	72	a1i 11	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → 9 ≠ 0)
74		nn0z 12273	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ℕ0 → 𝑛 ∈ ℤ)
75	74	adantl 481	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → 𝑛 ∈ ℤ)
76	71, 73, 75	exprecd 13800	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → ((1 / 9)↑𝑛) = (1 / (9↑𝑛)))
77	76	oveq2d 7271	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → ((2 / (3 · ((2 · 𝑁) + 1))) · ((1 / 9)↑𝑛)) = ((2 / (3 · ((2 · 𝑁) + 1))) · (1 / (9↑𝑛))))
78		nn0mulcl 12199	. . . . . . . . . . . . . . 15 ⊢ ((2 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (2 · 𝑁) ∈ ℕ0)
79	5, 78	mpan 686	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ ℕ0 → (2 · 𝑁) ∈ ℕ0)
80		nn0p1nn 12202	. . . . . . . . . . . . . 14 ⊢ ((2 · 𝑁) ∈ ℕ0 → ((2 · 𝑁) + 1) ∈ ℕ)
81	79, 80	syl 17	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ ℕ0 → ((2 · 𝑁) + 1) ∈ ℕ)
82		nnmulcl 11927	. . . . . . . . . . . . 13 ⊢ ((3 ∈ ℕ ∧ ((2 · 𝑁) + 1) ∈ ℕ) → (3 · ((2 · 𝑁) + 1)) ∈ ℕ)
83	4, 81, 82	sylancr 586	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℕ0 → (3 · ((2 · 𝑁) + 1)) ∈ ℕ)
84		nndivre 11944	. . . . . . . . . . . 12 ⊢ ((2 ∈ ℝ ∧ (3 · ((2 · 𝑁) + 1)) ∈ ℕ) → (2 / (3 · ((2 · 𝑁) + 1))) ∈ ℝ)
85	3, 83, 84	sylancr 586	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℕ0 → (2 / (3 · ((2 · 𝑁) + 1))) ∈ ℝ)
86	85	recnd 10934	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ0 → (2 / (3 · ((2 · 𝑁) + 1))) ∈ ℂ)
87	86	adantr 480	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → (2 / (3 · ((2 · 𝑁) + 1))) ∈ ℂ)
88	15	nncnd 11919	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → (9↑𝑛) ∈ ℂ)
89	15	nnne0d 11953	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → (9↑𝑛) ≠ 0)
90	87, 88, 89	divrecd 11684	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → ((2 / (3 · ((2 · 𝑁) + 1))) / (9↑𝑛)) = ((2 / (3 · ((2 · 𝑁) + 1))) · (1 / (9↑𝑛))))
91		2cnd 11981	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → 2 ∈ ℂ)
92	83	adantr 480	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → (3 · ((2 · 𝑁) + 1)) ∈ ℕ)
93	92	nncnd 11919	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → (3 · ((2 · 𝑁) + 1)) ∈ ℂ)
94	92	nnne0d 11953	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → (3 · ((2 · 𝑁) + 1)) ≠ 0)
95	91, 93, 88, 94, 89	divdiv1d 11712	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → ((2 / (3 · ((2 · 𝑁) + 1))) / (9↑𝑛)) = (2 / ((3 · ((2 · 𝑁) + 1)) · (9↑𝑛))))
96	77, 90, 95	3eqtr2d 2784	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → ((2 / (3 · ((2 · 𝑁) + 1))) · ((1 / 9)↑𝑛)) = (2 / ((3 · ((2 · 𝑁) + 1)) · (9↑𝑛))))
97	69, 96	eqtrd 2778	. . . . . 6 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → ((𝑘 ∈ ℕ0 ↦ ((2 / (3 · ((2 · 𝑁) + 1))) · ((1 / 9)↑𝑘)))‘𝑛) = (2 / ((3 · ((2 · 𝑁) + 1)) · (9↑𝑛))))
98	24, 97	syldan 590	. . . . 5 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → ((𝑘 ∈ ℕ0 ↦ ((2 / (3 · ((2 · 𝑁) + 1))) · ((1 / 9)↑𝑘)))‘𝑛) = (2 / ((3 · ((2 · 𝑁) + 1)) · (9↑𝑛))))
99	92, 15	nnmulcld 11956	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → ((3 · ((2 · 𝑁) + 1)) · (9↑𝑛)) ∈ ℕ)
100		nndivre 11944	. . . . . . 7 ⊢ ((2 ∈ ℝ ∧ ((3 · ((2 · 𝑁) + 1)) · (9↑𝑛)) ∈ ℕ) → (2 / ((3 · ((2 · 𝑁) + 1)) · (9↑𝑛))) ∈ ℝ)
101	3, 99, 100	sylancr 586	. . . . . 6 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → (2 / ((3 · ((2 · 𝑁) + 1)) · (9↑𝑛))) ∈ ℝ)
102	24, 101	syldan 590	. . . . 5 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (2 / ((3 · ((2 · 𝑁) + 1)) · (9↑𝑛))) ∈ ℝ)
103	79	adantr 480	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (2 · 𝑁) ∈ ℕ0)
104	103	nn0red 12224	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (2 · 𝑁) ∈ ℝ)
105	5, 24, 7	sylancr 586	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (2 · 𝑛) ∈ ℕ0)
106	105	nn0red 12224	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (2 · 𝑛) ∈ ℝ)
107		1red 10907	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → 1 ∈ ℝ)
108		eluzle 12524	. . . . . . . . . . 11 ⊢ (𝑛 ∈ (ℤ≥‘𝑁) → 𝑁 ≤ 𝑛)
109	108	adantl 481	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → 𝑁 ≤ 𝑛)
110		nn0re 12172	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℕ0 → 𝑁 ∈ ℝ)
111	110	adantr 480	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → 𝑁 ∈ ℝ)
112	24	nn0red 12224	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → 𝑛 ∈ ℝ)
113	3	a1i 11	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → 2 ∈ ℝ)
114		2pos 12006	. . . . . . . . . . . 12 ⊢ 0 < 2
115	114	a1i 11	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → 0 < 2)
116		lemul2 11758	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℝ ∧ 𝑛 ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → (𝑁 ≤ 𝑛 ↔ (2 · 𝑁) ≤ (2 · 𝑛)))
117	111, 112, 113, 115, 116	syl112anc 1372	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (𝑁 ≤ 𝑛 ↔ (2 · 𝑁) ≤ (2 · 𝑛)))
118	109, 117	mpbid 231	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (2 · 𝑁) ≤ (2 · 𝑛))
119	104, 106, 107, 118	leadd1dd 11519	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → ((2 · 𝑁) + 1) ≤ ((2 · 𝑛) + 1))
120	81	adantr 480	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → ((2 · 𝑁) + 1) ∈ ℕ)
121	120	nnred 11918	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → ((2 · 𝑁) + 1) ∈ ℝ)
122	24, 10	syldan 590	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → ((2 · 𝑛) + 1) ∈ ℕ)
123	122	nnred 11918	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → ((2 · 𝑛) + 1) ∈ ℝ)
124		3re 11983	. . . . . . . . . 10 ⊢ 3 ∈ ℝ
125	124	a1i 11	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → 3 ∈ ℝ)
126		3pos 12008	. . . . . . . . . 10 ⊢ 0 < 3
127	126	a1i 11	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → 0 < 3)
128		lemul2 11758	. . . . . . . . 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 1372	. . . . . . . 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 480	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (3 · ((2 · 𝑁) + 1)) ∈ ℕ)
132	131	nnred 11918	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (3 · ((2 · 𝑁) + 1)) ∈ ℝ)
133	24, 12	syldan 590	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (3 · ((2 · 𝑛) + 1)) ∈ ℕ)
134	133	nnred 11918	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (3 · ((2 · 𝑛) + 1)) ∈ ℝ)
135	13, 24, 14	sylancr 586	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (9↑𝑛) ∈ ℕ)
136	135	nnred 11918	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (9↑𝑛) ∈ ℝ)
137	135	nngt0d 11952	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → 0 < (9↑𝑛))
138		lemul1 11757	. . . . . . . 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 1372	. . . . . . 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 590	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → ((3 · ((2 · 𝑁) + 1)) · (9↑𝑛)) ∈ ℕ)
142	141	nnred 11918	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → ((3 · ((2 · 𝑁) + 1)) · (9↑𝑛)) ∈ ℝ)
143	141	nngt0d 11952	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → 0 < ((3 · ((2 · 𝑁) + 1)) · (9↑𝑛)))
144	24, 58	syldan 590	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)) ∈ ℝ)
145	24, 59	syldan 590	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → 0 < ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))
146		lediv2 11795	. . . . . . 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 1384	. . . . . 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 12002	. . . . . . . . . . . 12 ⊢ 9 ∈ ℝ
150	149, 72	rereccli 11670	. . . . . . . . . . 11 ⊢ (1 / 9) ∈ ℝ
151	150	recni 10920	. . . . . . . . . 10 ⊢ (1 / 9) ∈ ℂ
152	151	a1i 11	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ0 → (1 / 9) ∈ ℂ)
153		0re 10908	. . . . . . . . . . . . 13 ⊢ 0 ∈ ℝ
154		9pos 12016	. . . . . . . . . . . . . 14 ⊢ 0 < 9
155	149, 154	recgt0ii 11811	. . . . . . . . . . . . 13 ⊢ 0 < (1 / 9)
156	153, 150, 155	ltleii 11028	. . . . . . . . . . . 12 ⊢ 0 ≤ (1 / 9)
157		absid 14936	. . . . . . . . . . . 12 ⊢ (((1 / 9) ∈ ℝ ∧ 0 ≤ (1 / 9)) → (abs‘(1 / 9)) = (1 / 9))
158	150, 156, 157	mp2an 688	. . . . . . . . . . 11 ⊢ (abs‘(1 / 9)) = (1 / 9)
159		1lt9 12109	. . . . . . . . . . . . 13 ⊢ 1 < 9
160		recgt1i 11802	. . . . . . . . . . . . 13 ⊢ ((9 ∈ ℝ ∧ 1 < 9) → (0 < (1 / 9) ∧ (1 / 9) < 1))
161	149, 159, 160	mp2an 688	. . . . . . . . . . . 12 ⊢ (0 < (1 / 9) ∧ (1 / 9) < 1)
162	161	simpri 485	. . . . . . . . . . 11 ⊢ (1 / 9) < 1
163	158, 162	eqbrtri 5091	. . . . . . . . . 10 ⊢ (abs‘(1 / 9)) < 1
164	163	a1i 11	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ0 → (abs‘(1 / 9)) < 1)
165		eqid 2738	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℕ0 ↦ ((1 / 9)↑𝑘)) = (𝑘 ∈ ℕ0 ↦ ((1 / 9)↑𝑘))
166		ovex 7288	. . . . . . . . . . 11 ⊢ ((1 / 9)↑𝑛) ∈ V
167	64, 165, 166	fvmpt 6857	. . . . . . . . . 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 15511	. . . . . . . 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 13800	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ0 → ((1 / 9)↑𝑁) = (1 / (9↑𝑁)))
173	70, 72	dividi 11638	. . . . . . . . . . . . 13 ⊢ (9 / 9) = 1
174	173	oveq1i 7265	. . . . . . . . . . . 12 ⊢ ((9 / 9) − (1 / 9)) = (1 − (1 / 9))
175		ax-1cn 10860	. . . . . . . . . . . . . 14 ⊢ 1 ∈ ℂ
176	70, 72	pm3.2i 470	. . . . . . . . . . . . . 14 ⊢ (9 ∈ ℂ ∧ 9 ≠ 0)
177		divsubdir 11599	. . . . . . . . . . . . . 14 ⊢ ((9 ∈ ℂ ∧ 1 ∈ ℂ ∧ (9 ∈ ℂ ∧ 9 ≠ 0)) → ((9 − 1) / 9) = ((9 / 9) − (1 / 9)))
178	70, 175, 176, 177	mp3an 1459	. . . . . . . . . . . . 13 ⊢ ((9 − 1) / 9) = ((9 / 9) − (1 / 9))
179		9m1e8 12037	. . . . . . . . . . . . . 14 ⊢ (9 − 1) = 8
180	179	oveq1i 7265	. . . . . . . . . . . . 13 ⊢ ((9 − 1) / 9) = (8 / 9)
181	178, 180	eqtr3i 2768	. . . . . . . . . . . 12 ⊢ ((9 / 9) − (1 / 9)) = (8 / 9)
182	174, 181	eqtr3i 2768	. . . . . . . . . . 11 ⊢ (1 − (1 / 9)) = (8 / 9)
183	182	a1i 11	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ0 → (1 − (1 / 9)) = (8 / 9))
184	172, 183	oveq12d 7273	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ0 → (((1 / 9)↑𝑁) / (1 − (1 / 9))) = ((1 / (9↑𝑁)) / (8 / 9)))
185	175	a1i 11	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ0 → 1 ∈ ℂ)
186		nnexpcl 13723	. . . . . . . . . . . 12 ⊢ ((9 ∈ ℕ ∧ 𝑁 ∈ ℕ0) → (9↑𝑁) ∈ ℕ)
187	13, 186	mpan 686	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℕ0 → (9↑𝑁) ∈ ℕ)
188	187	nncnd 11919	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ0 → (9↑𝑁) ∈ ℂ)
189		8cn 12000	. . . . . . . . . . . 12 ⊢ 8 ∈ ℂ
190	189, 70, 72	divcli 11647	. . . . . . . . . . 11 ⊢ (8 / 9) ∈ ℂ
191	190	a1i 11	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ0 → (8 / 9) ∈ ℂ)
192	187	nnne0d 11953	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ0 → (9↑𝑁) ≠ 0)
193		8nn 11998	. . . . . . . . . . . . 13 ⊢ 8 ∈ ℕ
194	193	nnne0i 11943	. . . . . . . . . . . 12 ⊢ 8 ≠ 0
195	189, 70, 194, 72	divne0i 11653	. . . . . . . . . . 11 ⊢ (8 / 9) ≠ 0
196	195	a1i 11	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ0 → (8 / 9) ≠ 0)
197	185, 188, 191, 192, 196	divdiv32d 11706	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ0 → ((1 / (9↑𝑁)) / (8 / 9)) = ((1 / (8 / 9)) / (9↑𝑁)))
198		recdiv 11611	. . . . . . . . . . . 12 ⊢ (((8 ∈ ℂ ∧ 8 ≠ 0) ∧ (9 ∈ ℂ ∧ 9 ≠ 0)) → (1 / (8 / 9)) = (9 / 8))
199	189, 194, 70, 72, 198	mp4an 689	. . . . . . . . . . 11 ⊢ (1 / (8 / 9)) = (9 / 8)
200	199	oveq1i 7265	. . . . . . . . . 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 11712	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ0 → ((9 / 8) / (9↑𝑁)) = (9 / (8 · (9↑𝑁))))
204	200, 203	syl5eq 2791	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ0 → ((1 / (8 / 9)) / (9↑𝑁)) = (9 / (8 · (9↑𝑁))))
205	184, 197, 204	3eqtrd 2782	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ0 → (((1 / 9)↑𝑁) / (1 − (1 / 9))) = (9 / (8 · (9↑𝑁))))
206	169, 205	breqtrd 5096	. . . . . . 7 ⊢ (𝑁 ∈ ℕ0 → seq𝑁( + , (𝑘 ∈ ℕ0 ↦ ((1 / 9)↑𝑘))) ⇝ (9 / (8 · (9↑𝑁))))
207		expcl 13728	. . . . . . . . 9 ⊢ (((1 / 9) ∈ ℂ ∧ 𝑛 ∈ ℕ0) → ((1 / 9)↑𝑛) ∈ ℂ)
208	151, 24, 207	sylancr 586	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → ((1 / 9)↑𝑛) ∈ ℂ)
209	168, 208	eqeltrd 2839	. . . . . . 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 7271	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → ((2 / (3 · ((2 · 𝑁) + 1))) · ((𝑘 ∈ ℕ0 ↦ ((1 / 9)↑𝑘))‘𝑛)) = ((2 / (3 · ((2 · 𝑁) + 1))) · ((1 / 9)↑𝑛)))
212	210, 211	eqtr4d 2781	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → ((𝑘 ∈ ℕ0 ↦ ((2 / (3 · ((2 · 𝑁) + 1))) · ((1 / 9)↑𝑘)))‘𝑛) = ((2 / (3 · ((2 · 𝑁) + 1))) · ((𝑘 ∈ ℕ0 ↦ ((1 / 9)↑𝑘))‘𝑛)))
213	22, 23, 86, 206, 209, 212	isermulc2 15297	. . . . . 6 ⊢ (𝑁 ∈ ℕ0 → seq𝑁( + , (𝑘 ∈ ℕ0 ↦ ((2 / (3 · ((2 · 𝑁) + 1))) · ((1 / 9)↑𝑘)))) ⇝ ((2 / (3 · ((2 · 𝑁) + 1))) · (9 / (8 · (9↑𝑁)))))
214		seqex 13651	. . . . . . 7 ⊢ seq𝑁( + , (𝑘 ∈ ℕ0 ↦ ((2 / (3 · ((2 · 𝑁) + 1))) · ((1 / 9)↑𝑘)))) ∈ V
215		ovex 7288	. . . . . . 7 ⊢ ((2 / (3 · ((2 · 𝑁) + 1))) · (9 / (8 · (9↑𝑁)))) ∈ V
216	214, 215	breldm 5806	. . . . . 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 15484	. . . 4 ⊢ (𝑁 ∈ ℕ0 → Σ𝑛 ∈ (ℤ≥‘𝑁)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) ≤ Σ𝑛 ∈ (ℤ≥‘𝑁)(2 / ((3 · ((2 · 𝑁) + 1)) · (9↑𝑛))))
219	102	recnd 10934	. . . . 5 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (2 / ((3 · ((2 · 𝑁) + 1)) · (9↑𝑛))) ∈ ℂ)
220		3cn 11984	. . . . . . . . . . . 12 ⊢ 3 ∈ ℂ
221		4cn 11988	. . . . . . . . . . . 12 ⊢ 4 ∈ ℂ
222		2cn 11978	. . . . . . . . . . . 12 ⊢ 2 ∈ ℂ
223		4ne0 12011	. . . . . . . . . . . 12 ⊢ 4 ≠ 0
224		3ne0 12009	. . . . . . . . . . . 12 ⊢ 3 ≠ 0
225		2ne0 12007	. . . . . . . . . . . 12 ⊢ 2 ≠ 0
226	220, 221, 222, 220, 223, 224, 225	divdivdivi 11668	. . . . . . . . . . 11 ⊢ ((3 / 4) / (2 / 3)) = ((3 · 3) / (4 · 2))
227		3t3e9 12070	. . . . . . . . . . . 12 ⊢ (3 · 3) = 9
228		4t2e8 12071	. . . . . . . . . . . 12 ⊢ (4 · 2) = 8
229	227, 228	oveq12i 7267	. . . . . . . . . . 11 ⊢ ((3 · 3) / (4 · 2)) = (9 / 8)
230	226, 229	eqtri 2766	. . . . . . . . . 10 ⊢ ((3 / 4) / (2 / 3)) = (9 / 8)
231	230	oveq2i 7266	. . . . . . . . 9 ⊢ ((2 / 3) · ((3 / 4) / (2 / 3))) = ((2 / 3) · (9 / 8))
232	220, 221, 223	divcli 11647	. . . . . . . . . 10 ⊢ (3 / 4) ∈ ℂ
233	222, 220, 224	divcli 11647	. . . . . . . . . 10 ⊢ (2 / 3) ∈ ℂ
234	222, 220, 225, 224	divne0i 11653	. . . . . . . . . 10 ⊢ (2 / 3) ≠ 0
235	232, 233, 234	divcan2i 11648	. . . . . . . . 9 ⊢ ((2 / 3) · ((3 / 4) / (2 / 3))) = (3 / 4)
236	231, 235	eqtr3i 2768	. . . . . . . 8 ⊢ ((2 / 3) · (9 / 8)) = (3 / 4)
237	236	oveq1i 7265	. . . . . . 7 ⊢ (((2 / 3) · (9 / 8)) / (((2 · 𝑁) + 1) · (9↑𝑁))) = ((3 / 4) / (((2 · 𝑁) + 1) · (9↑𝑁)))
238		2cnd 11981	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ0 → 2 ∈ ℂ)
239	220	a1i 11	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ0 → 3 ∈ ℂ)
240	81	nncnd 11919	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ0 → ((2 · 𝑁) + 1) ∈ ℂ)
241	224	a1i 11	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ0 → 3 ≠ 0)
242	81	nnne0d 11953	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ0 → ((2 · 𝑁) + 1) ≠ 0)
243	238, 239, 240, 241, 242	divdiv1d 11712	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ0 → ((2 / 3) / ((2 · 𝑁) + 1)) = (2 / (3 · ((2 · 𝑁) + 1))))
244	243, 203	oveq12d 7273	. . . . . . . 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 11647	. . . . . . . . . 10 ⊢ (9 / 8) ∈ ℂ
247	246	a1i 11	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ0 → (9 / 8) ∈ ℂ)
248	245, 240, 247, 188, 242, 192	divmuldivd 11722	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ0 → (((2 / 3) / ((2 · 𝑁) + 1)) · ((9 / 8) / (9↑𝑁))) = (((2 / 3) · (9 / 8)) / (((2 · 𝑁) + 1) · (9↑𝑁))))
249	244, 248	eqtr3d 2780	. . . . . . 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 10929	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ0 → ((4 · ((2 · 𝑁) + 1)) · (9↑𝑁)) = (4 · (((2 · 𝑁) + 1) · (9↑𝑁))))
252	251	oveq2d 7271	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ0 → (3 / ((4 · ((2 · 𝑁) + 1)) · (9↑𝑁))) = (3 / (4 · (((2 · 𝑁) + 1) · (9↑𝑁)))))
253	81, 187	nnmulcld 11956	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ0 → (((2 · 𝑁) + 1) · (9↑𝑁)) ∈ ℕ)
254	253	nncnd 11919	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ0 → (((2 · 𝑁) + 1) · (9↑𝑁)) ∈ ℂ)
255	223	a1i 11	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ0 → 4 ≠ 0)
256	253	nnne0d 11953	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ0 → (((2 · 𝑁) + 1) · (9↑𝑁)) ≠ 0)
257	239, 250, 254, 255, 256	divdiv1d 11712	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ0 → ((3 / 4) / (((2 · 𝑁) + 1) · (9↑𝑁))) = (3 / (4 · (((2 · 𝑁) + 1) · (9↑𝑁)))))
258	252, 257	eqtr4d 2781	. . . . . . 7 ⊢ (𝑁 ∈ ℕ0 → (3 / ((4 · ((2 · 𝑁) + 1)) · (9↑𝑁))) = ((3 / 4) / (((2 · 𝑁) + 1) · (9↑𝑁))))
259	237, 249, 258	3eqtr4a 2805	. . . . . 6 ⊢ (𝑁 ∈ ℕ0 → ((2 / (3 · ((2 · 𝑁) + 1))) · (9 / (8 · (9↑𝑁)))) = (3 / ((4 · ((2 · 𝑁) + 1)) · (9↑𝑁))))
260	213, 259	breqtrd 5096	. . . . 5 ⊢ (𝑁 ∈ ℕ0 → seq𝑁( + , (𝑘 ∈ ℕ0 ↦ ((2 / (3 · ((2 · 𝑁) + 1))) · ((1 / 9)↑𝑘)))) ⇝ (3 / ((4 · ((2 · 𝑁) + 1)) · (9↑𝑁))))
261	22, 23, 98, 219, 260	isumclim 15397	. . . 4 ⊢ (𝑁 ∈ ℕ0 → Σ𝑛 ∈ (ℤ≥‘𝑁)(2 / ((3 · ((2 · 𝑁) + 1)) · (9↑𝑛))) = (3 / ((4 · ((2 · 𝑁) + 1)) · (9↑𝑁))))
262	218, 261	breqtrd 5096	. . 3 ⊢ (𝑁 ∈ ℕ0 → Σ𝑛 ∈ (ℤ≥‘𝑁)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) ≤ (3 / ((4 · ((2 · 𝑁) + 1)) · (9↑𝑁))))
263		4nn 11986	. . . . . . 7 ⊢ 4 ∈ ℕ
264		nnmulcl 11927	. . . . . . 7 ⊢ ((4 ∈ ℕ ∧ ((2 · 𝑁) + 1) ∈ ℕ) → (4 · ((2 · 𝑁) + 1)) ∈ ℕ)
265	263, 81, 264	sylancr 586	. . . . . 6 ⊢ (𝑁 ∈ ℕ0 → (4 · ((2 · 𝑁) + 1)) ∈ ℕ)
266	265, 187	nnmulcld 11956	. . . . 5 ⊢ (𝑁 ∈ ℕ0 → ((4 · ((2 · 𝑁) + 1)) · (9↑𝑁)) ∈ ℕ)
267		nndivre 11944	. . . . 5 ⊢ ((3 ∈ ℝ ∧ ((4 · ((2 · 𝑁) + 1)) · (9↑𝑁)) ∈ ℕ) → (3 / ((4 · ((2 · 𝑁) + 1)) · (9↑𝑁))) ∈ ℝ)
268	124, 266, 267	sylancr 586	. . . 4 ⊢ (𝑁 ∈ ℕ0 → (3 / ((4 · ((2 · 𝑁) + 1)) · (9↑𝑁))) ∈ ℝ)
269		elicc2 13073	. . . 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 586	. . 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 1340	. 2 ⊢ (𝑁 ∈ ℕ0 → Σ𝑛 ∈ (ℤ≥‘𝑁)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) ∈ (0[,](3 / ((4 · ((2 · 𝑁) + 1)) · (9↑𝑁)))))
272	54, 271	eqeltrd 2839	1 ⊢ (𝑁 ∈ ℕ0 → ((log‘2) − Σ𝑛 ∈ (0...(𝑁 − 1))(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))) ∈ (0[,](3 / ((4 · ((2 · 𝑁) + 1)) · (9↑𝑁)))))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   ∧ w3a 1085   = wceq 1539   ∈ wcel 2108   ≠ wne 2942   class class class wbr 5070   ↦ cmpt 5153  dom cdm 5580  ‘cfv 6418  (class class class)co 7255  ℂcc 10800  ℝcr 10801  0cc0 10802  1c1 10803   + caddc 10805   · cmul 10807   < clt 10940   ≤ cle 10941   − cmin 11135   / cdiv 11562  ℕcn 11903  2c2 11958  3c3 11959  4c4 11960  8c8 11964  9c9 11965  ℕ₀cn0 12163  ℤcz 12249  ℤ_≥cuz 12511  [,]cicc 13011  ...cfz 13168  seqcseq 13649  ↑cexp 13710  abscabs 14873   ⇝ cli 15121  Σcsu 15325  logclog 25615

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-rep 5205  ax-sep 5218  ax-nul 5225  ax-pow 5283  ax-pr 5347  ax-un 7566  ax-inf2 9329  ax-cnex 10858  ax-resscn 10859  ax-1cn 10860  ax-icn 10861  ax-addcl 10862  ax-addrcl 10863  ax-mulcl 10864  ax-mulrcl 10865  ax-mulcom 10866  ax-addass 10867  ax-mulass 10868  ax-distr 10869  ax-i2m1 10870  ax-1ne0 10871  ax-1rid 10872  ax-rnegex 10873  ax-rrecex 10874  ax-cnre 10875  ax-pre-lttri 10876  ax-pre-lttrn 10877  ax-pre-ltadd 10878  ax-pre-mulgt0 10879  ax-pre-sup 10880  ax-addf 10881  ax-mulf 10882

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-nel 3049  df-ral 3068  df-rex 3069  df-reu 3070  df-rmo 3071  df-rab 3072  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3902  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-tp 4563  df-op 4565  df-uni 4837  df-int 4877  df-iun 4923  df-iin 4924  df-br 5071  df-opab 5133  df-mpt 5154  df-tr 5188  df-id 5480  df-eprel 5486  df-po 5494  df-so 5495  df-fr 5535  df-se 5536  df-we 5537  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-pred 6191  df-ord 6254  df-on 6255  df-lim 6256  df-suc 6257  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-f1 6423  df-fo 6424  df-f1o 6425  df-fv 6426  df-isom 6427  df-riota 7212  df-ov 7258  df-oprab 7259  df-mpo 7260  df-of 7511  df-om 7688  df-1st 7804  df-2nd 7805  df-supp 7949  df-frecs 8068  df-wrecs 8099  df-recs 8173  df-rdg 8212  df-1o 8267  df-2o 8268  df-oadd 8271  df-er 8456  df-map 8575  df-pm 8576  df-ixp 8644  df-en 8692  df-dom 8693  df-sdom 8694  df-fin 8695  df-fsupp 9059  df-fi 9100  df-sup 9131  df-inf 9132  df-oi 9199  df-card 9628  df-pnf 10942  df-mnf 10943  df-xr 10944  df-ltxr 10945  df-le 10946  df-sub 11137  df-neg 11138  df-div 11563  df-nn 11904  df-2 11966  df-3 11967  df-4 11968  df-5 11969  df-6 11970  df-7 11971  df-8 11972  df-9 11973  df-n0 12164  df-xnn0 12236  df-z 12250  df-dec 12367  df-uz 12512  df-q 12618  df-rp 12660  df-xneg 12777  df-xadd 12778  df-xmul 12779  df-ioo 13012  df-ioc 13013  df-ico 13014  df-icc 13015  df-fz 13169  df-fzo 13312  df-fl 13440  df-mod 13518  df-seq 13650  df-exp 13711  df-fac 13916  df-bc 13945  df-hash 13973  df-shft 14706  df-cj 14738  df-re 14739  df-im 14740  df-sqrt 14874  df-abs 14875  df-limsup 15108  df-clim 15125  df-rlim 15126  df-sum 15326  df-ef 15705  df-sin 15707  df-cos 15708  df-tan 15709  df-pi 15710  df-dvds 15892  df-struct 16776  df-sets 16793  df-slot 16811  df-ndx 16823  df-base 16841  df-ress 16868  df-plusg 16901  df-mulr 16902  df-starv 16903  df-sca 16904  df-vsca 16905  df-ip 16906  df-tset 16907  df-ple 16908  df-ds 16910  df-unif 16911  df-hom 16912  df-cco 16913  df-rest 17050  df-topn 17051  df-0g 17069  df-gsum 17070  df-topgen 17071  df-pt 17072  df-prds 17075  df-xrs 17130  df-qtop 17135  df-imas 17136  df-xps 17138  df-mre 17212  df-mrc 17213  df-acs 17215  df-mgm 18241  df-sgrp 18290  df-mnd 18301  df-submnd 18346  df-mulg 18616  df-cntz 18838  df-cmn 19303  df-psmet 20502  df-xmet 20503  df-met 20504  df-bl 20505  df-mopn 20506  df-fbas 20507  df-fg 20508  df-cnfld 20511  df-top 21951  df-topon 21968  df-topsp 21990  df-bases 22004  df-cld 22078  df-ntr 22079  df-cls 22080  df-nei 22157  df-lp 22195  df-perf 22196  df-cn 22286  df-cnp 22287  df-haus 22374  df-cmp 22446  df-tx 22621  df-hmeo 22814  df-fil 22905  df-fm 22997  df-flim 22998  df-flf 22999  df-xms 23381  df-ms 23382  df-tms 23383  df-cncf 23947  df-limc 24935  df-dv 24936  df-ulm 25441  df-log 25617  df-atan 25922

This theorem is referenced by:  log2ub  26004