Theorem log2tlbnd

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

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

Proof

Step	Hyp	Ref	Expression
1		fzfid	⊢ ( 𝑁 ∈ ℕ0 → ( 0 ... ( 𝑁 − 1 ) ) ∈ Fin )
2		elfznn0	⊢ ( 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) → 𝑛 ∈ ℕ0 )
3		2re	⊢ 2 ∈ ℝ
4		3nn	⊢ 3 ∈ ℕ
5		2nn0	⊢ 2 ∈ ℕ0
6		simpr	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) → 𝑛 ∈ ℕ0 )
7		nn0mulcl	⊢ ( ( 2 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) → ( 2 · 𝑛 ) ∈ ℕ0 )
8	5 6 7	sylancr	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) → ( 2 · 𝑛 ) ∈ ℕ0 )
9		nn0p1nn	⊢ ( ( 2 · 𝑛 ) ∈ ℕ0 → ( ( 2 · 𝑛 ) + 1 ) ∈ ℕ )
10	8 9	syl	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) → ( ( 2 · 𝑛 ) + 1 ) ∈ ℕ )
11		nnmulcl	⊢ ( ( 3 ∈ ℕ ∧ ( ( 2 · 𝑛 ) + 1 ) ∈ ℕ ) → ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) ∈ ℕ )
12	4 10 11	sylancr	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) → ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) ∈ ℕ )
13		9nn	⊢ 9 ∈ ℕ
14		nnexpcl	⊢ ( ( 9 ∈ ℕ ∧ 𝑛 ∈ ℕ0 ) → ( 9 ↑ 𝑛 ) ∈ ℕ )
15	13 6 14	sylancr	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) → ( 9 ↑ 𝑛 ) ∈ ℕ )
16	12 15	nnmulcld	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) → ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ∈ ℕ )
17		nndivre	⊢ ( ( 2 ∈ ℝ ∧ ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ∈ ℕ ) → ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) ∈ ℝ )
18	3 16 17	sylancr	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) → ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) ∈ ℝ )
19	18	recnd	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) → ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) ∈ ℂ )
20	2 19	sylan2	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) ∈ ℂ )
21	1 20	fsumcl	⊢ ( 𝑁 ∈ ℕ0 → Σ 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) ∈ ℂ )
22		eqid	⊢ ( ℤ≥ ‘ 𝑁 ) = ( ℤ≥ ‘ 𝑁 )
23		nn0z	⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℤ )
24		eluznn0	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑛 ∈ ℕ0 )
25		oveq2	⊢ ( 𝑘 = 𝑛 → ( 2 · 𝑘 ) = ( 2 · 𝑛 ) )
26	25	oveq1d	⊢ ( 𝑘 = 𝑛 → ( ( 2 · 𝑘 ) + 1 ) = ( ( 2 · 𝑛 ) + 1 ) )
27	26	oveq2d	⊢ ( 𝑘 = 𝑛 → ( 3 · ( ( 2 · 𝑘 ) + 1 ) ) = ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) )
28		oveq2	⊢ ( 𝑘 = 𝑛 → ( 9 ↑ 𝑘 ) = ( 9 ↑ 𝑛 ) )
29	27 28	oveq12d	⊢ ( 𝑘 = 𝑛 → ( ( 3 · ( ( 2 · 𝑘 ) + 1 ) ) · ( 9 ↑ 𝑘 ) ) = ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) )
30	29	oveq2d	⊢ ( 𝑘 = 𝑛 → ( 2 / ( ( 3 · ( ( 2 · 𝑘 ) + 1 ) ) · ( 9 ↑ 𝑘 ) ) ) = ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) )
31		eqid	⊢ ( 𝑘 ∈ ℕ0 ↦ ( 2 / ( ( 3 · ( ( 2 · 𝑘 ) + 1 ) ) · ( 9 ↑ 𝑘 ) ) ) ) = ( 𝑘 ∈ ℕ0 ↦ ( 2 / ( ( 3 · ( ( 2 · 𝑘 ) + 1 ) ) · ( 9 ↑ 𝑘 ) ) ) )
32		ovex	⊢ ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) ∈ V
33	30 31 32	fvmpt	⊢ ( 𝑛 ∈ ℕ0 → ( ( 𝑘 ∈ ℕ0 ↦ ( 2 / ( ( 3 · ( ( 2 · 𝑘 ) + 1 ) ) · ( 9 ↑ 𝑘 ) ) ) ) ‘ 𝑛 ) = ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) )
34	24 33	syl	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( ( 𝑘 ∈ ℕ0 ↦ ( 2 / ( ( 3 · ( ( 2 · 𝑘 ) + 1 ) ) · ( 9 ↑ 𝑘 ) ) ) ) ‘ 𝑛 ) = ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) )
35	24 18	syldan	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) ∈ ℝ )
36	31	log2cnv	⊢ seq 0 ( + , ( 𝑘 ∈ ℕ0 ↦ ( 2 / ( ( 3 · ( ( 2 · 𝑘 ) + 1 ) ) · ( 9 ↑ 𝑘 ) ) ) ) ) ⇝ ( log ‘ 2 )
37		seqex	⊢ seq 0 ( + , ( 𝑘 ∈ ℕ0 ↦ ( 2 / ( ( 3 · ( ( 2 · 𝑘 ) + 1 ) ) · ( 9 ↑ 𝑘 ) ) ) ) ) ∈ V
38		fvex	⊢ ( log ‘ 2 ) ∈ V
39	37 38	breldm	⊢ ( seq 0 ( + , ( 𝑘 ∈ ℕ0 ↦ ( 2 / ( ( 3 · ( ( 2 · 𝑘 ) + 1 ) ) · ( 9 ↑ 𝑘 ) ) ) ) ) ⇝ ( log ‘ 2 ) → seq 0 ( + , ( 𝑘 ∈ ℕ0 ↦ ( 2 / ( ( 3 · ( ( 2 · 𝑘 ) + 1 ) ) · ( 9 ↑ 𝑘 ) ) ) ) ) ∈ dom ⇝ )
40	36 39	mp1i	⊢ ( 𝑁 ∈ ℕ0 → seq 0 ( + , ( 𝑘 ∈ ℕ0 ↦ ( 2 / ( ( 3 · ( ( 2 · 𝑘 ) + 1 ) ) · ( 9 ↑ 𝑘 ) ) ) ) ) ∈ dom ⇝ )
41		nn0uz	⊢ ℕ0 = ( ℤ≥ ‘ 0 )
42		id	⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℕ0 )
43	33	adantl	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑘 ∈ ℕ0 ↦ ( 2 / ( ( 3 · ( ( 2 · 𝑘 ) + 1 ) ) · ( 9 ↑ 𝑘 ) ) ) ) ‘ 𝑛 ) = ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) )
44	43 19	eqeltrd	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑘 ∈ ℕ0 ↦ ( 2 / ( ( 3 · ( ( 2 · 𝑘 ) + 1 ) ) · ( 9 ↑ 𝑘 ) ) ) ) ‘ 𝑛 ) ∈ ℂ )
45	41 42 44	iserex	⊢ ( 𝑁 ∈ ℕ0 → ( seq 0 ( + , ( 𝑘 ∈ ℕ0 ↦ ( 2 / ( ( 3 · ( ( 2 · 𝑘 ) + 1 ) ) · ( 9 ↑ 𝑘 ) ) ) ) ) ∈ dom ⇝ ↔ seq 𝑁 ( + , ( 𝑘 ∈ ℕ0 ↦ ( 2 / ( ( 3 · ( ( 2 · 𝑘 ) + 1 ) ) · ( 9 ↑ 𝑘 ) ) ) ) ) ∈ dom ⇝ ) )
46	40 45	mpbid	⊢ ( 𝑁 ∈ ℕ0 → seq 𝑁 ( + , ( 𝑘 ∈ ℕ0 ↦ ( 2 / ( ( 3 · ( ( 2 · 𝑘 ) + 1 ) ) · ( 9 ↑ 𝑘 ) ) ) ) ) ∈ dom ⇝ )
47	22 23 34 35 46	isumrecl	⊢ ( 𝑁 ∈ ℕ0 → Σ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) ∈ ℝ )
48	47	recnd	⊢ ( 𝑁 ∈ ℕ0 → Σ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) ∈ ℂ )
49		0zd	⊢ ( 𝑁 ∈ ℕ0 → 0 ∈ ℤ )
50	36	a1i	⊢ ( 𝑁 ∈ ℕ0 → seq 0 ( + , ( 𝑘 ∈ ℕ0 ↦ ( 2 / ( ( 3 · ( ( 2 · 𝑘 ) + 1 ) ) · ( 9 ↑ 𝑘 ) ) ) ) ) ⇝ ( log ‘ 2 ) )
51	41 49 43 19 50	isumclim	⊢ ( 𝑁 ∈ ℕ0 → Σ 𝑛 ∈ ℕ0 ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) = ( log ‘ 2 ) )
52	41 22 42 43 19 40	isumsplit	⊢ ( 𝑁 ∈ ℕ0 → Σ 𝑛 ∈ ℕ0 ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) = ( Σ 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) + Σ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) ) )
53	51 52	eqtr3d	⊢ ( 𝑁 ∈ ℕ0 → ( log ‘ 2 ) = ( Σ 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) + Σ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) ) )
54	21 48 53	mvrladdd	⊢ ( 𝑁 ∈ ℕ0 → ( ( log ‘ 2 ) − Σ 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) ) = Σ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) )
55	3	a1i	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) → 2 ∈ ℝ )
56		0le2	⊢ 0 ≤ 2
57	56	a1i	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) → 0 ≤ 2 )
58	16	nnred	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) → ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ∈ ℝ )
59	16	nngt0d	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) → 0 < ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) )
60		divge0	⊢ ( ( ( 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	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) → 0 ≤ ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) )
62	24 61	syldan	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 0 ≤ ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) )
63	22 23 34 35 46 62	isumge0	⊢ ( 𝑁 ∈ ℕ0 → 0 ≤ Σ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) )
64		oveq2	⊢ ( 𝑘 = 𝑛 → ( ( 1 / 9 ) ↑ 𝑘 ) = ( ( 1 / 9 ) ↑ 𝑛 ) )
65	64	oveq2d	⊢ ( 𝑘 = 𝑛 → ( ( 2 / ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) ) · ( ( 1 / 9 ) ↑ 𝑘 ) ) = ( ( 2 / ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) ) · ( ( 1 / 9 ) ↑ 𝑛 ) ) )
66		eqid	⊢ ( 𝑘 ∈ ℕ0 ↦ ( ( 2 / ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) ) · ( ( 1 / 9 ) ↑ 𝑘 ) ) ) = ( 𝑘 ∈ ℕ0 ↦ ( ( 2 / ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) ) · ( ( 1 / 9 ) ↑ 𝑘 ) ) )
67		ovex	⊢ ( ( 2 / ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) ) · ( ( 1 / 9 ) ↑ 𝑛 ) ) ∈ V
68	65 66 67	fvmpt	⊢ ( 𝑛 ∈ ℕ0 → ( ( 𝑘 ∈ ℕ0 ↦ ( ( 2 / ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) ) · ( ( 1 / 9 ) ↑ 𝑘 ) ) ) ‘ 𝑛 ) = ( ( 2 / ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) ) · ( ( 1 / 9 ) ↑ 𝑛 ) ) )
69	68	adantl	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑘 ∈ ℕ0 ↦ ( ( 2 / ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) ) · ( ( 1 / 9 ) ↑ 𝑘 ) ) ) ‘ 𝑛 ) = ( ( 2 / ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) ) · ( ( 1 / 9 ) ↑ 𝑛 ) ) )
70		9cn	⊢ 9 ∈ ℂ
71	70	a1i	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) → 9 ∈ ℂ )
72	13	nnne0i	⊢ 9 ≠ 0
73	72	a1i	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) → 9 ≠ 0 )
74		nn0z	⊢ ( 𝑛 ∈ ℕ0 → 𝑛 ∈ ℤ )
75	74	adantl	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) → 𝑛 ∈ ℤ )
76	71 73 75	exprecd	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) → ( ( 1 / 9 ) ↑ 𝑛 ) = ( 1 / ( 9 ↑ 𝑛 ) ) )
77	76	oveq2d	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) → ( ( 2 / ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) ) · ( ( 1 / 9 ) ↑ 𝑛 ) ) = ( ( 2 / ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) ) · ( 1 / ( 9 ↑ 𝑛 ) ) ) )
78		nn0mulcl	⊢ ( ( 2 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( 2 · 𝑁 ) ∈ ℕ0 )
79	5 78	mpan	⊢ ( 𝑁 ∈ ℕ0 → ( 2 · 𝑁 ) ∈ ℕ0 )
80		nn0p1nn	⊢ ( ( 2 · 𝑁 ) ∈ ℕ0 → ( ( 2 · 𝑁 ) + 1 ) ∈ ℕ )
81	79 80	syl	⊢ ( 𝑁 ∈ ℕ0 → ( ( 2 · 𝑁 ) + 1 ) ∈ ℕ )
82		nnmulcl	⊢ ( ( 3 ∈ ℕ ∧ ( ( 2 · 𝑁 ) + 1 ) ∈ ℕ ) → ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) ∈ ℕ )
83	4 81 82	sylancr	⊢ ( 𝑁 ∈ ℕ0 → ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) ∈ ℕ )
84		nndivre	⊢ ( ( 2 ∈ ℝ ∧ ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) ∈ ℕ ) → ( 2 / ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) ) ∈ ℝ )
85	3 83 84	sylancr	⊢ ( 𝑁 ∈ ℕ0 → ( 2 / ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) ) ∈ ℝ )
86	85	recnd	⊢ ( 𝑁 ∈ ℕ0 → ( 2 / ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) ) ∈ ℂ )
87	86	adantr	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) → ( 2 / ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) ) ∈ ℂ )
88	15	nncnd	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) → ( 9 ↑ 𝑛 ) ∈ ℂ )
89	15	nnne0d	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) → ( 9 ↑ 𝑛 ) ≠ 0 )
90	87 88 89	divrecd	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) → ( ( 2 / ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) ) / ( 9 ↑ 𝑛 ) ) = ( ( 2 / ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) ) · ( 1 / ( 9 ↑ 𝑛 ) ) ) )
91		2cnd	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) → 2 ∈ ℂ )
92	83	adantr	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) → ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) ∈ ℕ )
93	92	nncnd	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) → ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) ∈ ℂ )
94	92	nnne0d	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) → ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) ≠ 0 )
95	91 93 88 94 89	divdiv1d	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) → ( ( 2 / ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) ) / ( 9 ↑ 𝑛 ) ) = ( 2 / ( ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) )
96	77 90 95	3eqtr2d	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) → ( ( 2 / ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) ) · ( ( 1 / 9 ) ↑ 𝑛 ) ) = ( 2 / ( ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) )
97	69 96	eqtrd	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑘 ∈ ℕ0 ↦ ( ( 2 / ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) ) · ( ( 1 / 9 ) ↑ 𝑘 ) ) ) ‘ 𝑛 ) = ( 2 / ( ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) )
98	24 97	syldan	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( ( 𝑘 ∈ ℕ0 ↦ ( ( 2 / ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) ) · ( ( 1 / 9 ) ↑ 𝑘 ) ) ) ‘ 𝑛 ) = ( 2 / ( ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) )
99	92 15	nnmulcld	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) → ( ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ∈ ℕ )
100		nndivre	⊢ ( ( 2 ∈ ℝ ∧ ( ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ∈ ℕ ) → ( 2 / ( ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) ∈ ℝ )
101	3 99 100	sylancr	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) → ( 2 / ( ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) ∈ ℝ )
102	24 101	syldan	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 2 / ( ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) ∈ ℝ )
103	79	adantr	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 2 · 𝑁 ) ∈ ℕ0 )
104	103	nn0red	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 2 · 𝑁 ) ∈ ℝ )
105	5 24 7	sylancr	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 2 · 𝑛 ) ∈ ℕ0 )
106	105	nn0red	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 2 · 𝑛 ) ∈ ℝ )
107		1red	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 1 ∈ ℝ )
108		eluzle	⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) → 𝑁 ≤ 𝑛 )
109	108	adantl	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑁 ≤ 𝑛 )
110		nn0re	⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℝ )
111	110	adantr	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑁 ∈ ℝ )
112	24	nn0red	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑛 ∈ ℝ )
113	3	a1i	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 2 ∈ ℝ )
114		2pos	⊢ 0 < 2
115	114	a1i	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 0 < 2 )
116		lemul2	⊢ ( ( 𝑁 ∈ ℝ ∧ 𝑛 ∈ ℝ ∧ ( 2 ∈ ℝ ∧ 0 < 2 ) ) → ( 𝑁 ≤ 𝑛 ↔ ( 2 · 𝑁 ) ≤ ( 2 · 𝑛 ) ) )
117	111 112 113 115 116	syl112anc	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 𝑁 ≤ 𝑛 ↔ ( 2 · 𝑁 ) ≤ ( 2 · 𝑛 ) ) )
118	109 117	mpbid	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 2 · 𝑁 ) ≤ ( 2 · 𝑛 ) )
119	104 106 107 118	leadd1dd	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( ( 2 · 𝑁 ) + 1 ) ≤ ( ( 2 · 𝑛 ) + 1 ) )
120	81	adantr	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( ( 2 · 𝑁 ) + 1 ) ∈ ℕ )
121	120	nnred	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( ( 2 · 𝑁 ) + 1 ) ∈ ℝ )
122	24 10	syldan	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( ( 2 · 𝑛 ) + 1 ) ∈ ℕ )
123	122	nnred	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( ( 2 · 𝑛 ) + 1 ) ∈ ℝ )
124		3re	⊢ 3 ∈ ℝ
125	124	a1i	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 3 ∈ ℝ )
126		3pos	⊢ 0 < 3
127	126	a1i	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 0 < 3 )
128		lemul2	⊢ ( ( ( ( 2 · 𝑁 ) + 1 ) ∈ ℝ ∧ ( ( 2 · 𝑛 ) + 1 ) ∈ ℝ ∧ ( 3 ∈ ℝ ∧ 0 < 3 ) ) → ( ( ( 2 · 𝑁 ) + 1 ) ≤ ( ( 2 · 𝑛 ) + 1 ) ↔ ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) ≤ ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) ) )
129	121 123 125 127 128	syl112anc	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( ( ( 2 · 𝑁 ) + 1 ) ≤ ( ( 2 · 𝑛 ) + 1 ) ↔ ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) ≤ ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) ) )
130	119 129	mpbid	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) ≤ ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) )
131	83	adantr	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) ∈ ℕ )
132	131	nnred	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) ∈ ℝ )
133	24 12	syldan	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) ∈ ℕ )
134	133	nnred	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) ∈ ℝ )
135	13 24 14	sylancr	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 9 ↑ 𝑛 ) ∈ ℕ )
136	135	nnred	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 9 ↑ 𝑛 ) ∈ ℝ )
137	135	nngt0d	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 0 < ( 9 ↑ 𝑛 ) )
138		lemul1	⊢ ( ( ( 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	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) ≤ ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) ↔ ( ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ≤ ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) )
140	130 139	mpbid	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ≤ ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) )
141	24 99	syldan	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ∈ ℕ )
142	141	nnred	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ∈ ℝ )
143	141	nngt0d	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 0 < ( ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) )
144	24 58	syldan	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ∈ ℝ )
145	24 59	syldan	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 0 < ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) )
146		lediv2	⊢ ( ( ( ( ( 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	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( ( ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ≤ ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ↔ ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) ≤ ( 2 / ( ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) ) )
148	140 147	mpbid	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) ≤ ( 2 / ( ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) )
149		9re	⊢ 9 ∈ ℝ
150	149 72	rereccli	⊢ ( 1 / 9 ) ∈ ℝ
151	150	recni	⊢ ( 1 / 9 ) ∈ ℂ
152	151	a1i	⊢ ( 𝑁 ∈ ℕ0 → ( 1 / 9 ) ∈ ℂ )
153		0re	⊢ 0 ∈ ℝ
154		9pos	⊢ 0 < 9
155	149 154	recgt0ii	⊢ 0 < ( 1 / 9 )
156	153 150 155	ltleii	⊢ 0 ≤ ( 1 / 9 )
157		absid	⊢ ( ( ( 1 / 9 ) ∈ ℝ ∧ 0 ≤ ( 1 / 9 ) ) → ( abs ‘ ( 1 / 9 ) ) = ( 1 / 9 ) )
158	150 156 157	mp2an	⊢ ( abs ‘ ( 1 / 9 ) ) = ( 1 / 9 )
159		1lt9	⊢ 1 < 9
160		recgt1i	⊢ ( ( 9 ∈ ℝ ∧ 1 < 9 ) → ( 0 < ( 1 / 9 ) ∧ ( 1 / 9 ) < 1 ) )
161	149 159 160	mp2an	⊢ ( 0 < ( 1 / 9 ) ∧ ( 1 / 9 ) < 1 )
162	161	simpri	⊢ ( 1 / 9 ) < 1
163	158 162	eqbrtri	⊢ ( abs ‘ ( 1 / 9 ) ) < 1
164	163	a1i	⊢ ( 𝑁 ∈ ℕ0 → ( abs ‘ ( 1 / 9 ) ) < 1 )
165		eqid	⊢ ( 𝑘 ∈ ℕ0 ↦ ( ( 1 / 9 ) ↑ 𝑘 ) ) = ( 𝑘 ∈ ℕ0 ↦ ( ( 1 / 9 ) ↑ 𝑘 ) )
166		ovex	⊢ ( ( 1 / 9 ) ↑ 𝑛 ) ∈ V
167	64 165 166	fvmpt	⊢ ( 𝑛 ∈ ℕ0 → ( ( 𝑘 ∈ ℕ0 ↦ ( ( 1 / 9 ) ↑ 𝑘 ) ) ‘ 𝑛 ) = ( ( 1 / 9 ) ↑ 𝑛 ) )
168	24 167	syl	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( ( 𝑘 ∈ ℕ0 ↦ ( ( 1 / 9 ) ↑ 𝑘 ) ) ‘ 𝑛 ) = ( ( 1 / 9 ) ↑ 𝑛 ) )
169	152 164 42 168	geolim2	⊢ ( 𝑁 ∈ ℕ0 → seq 𝑁 ( + , ( 𝑘 ∈ ℕ0 ↦ ( ( 1 / 9 ) ↑ 𝑘 ) ) ) ⇝ ( ( ( 1 / 9 ) ↑ 𝑁 ) / ( 1 − ( 1 / 9 ) ) ) )
170	70	a1i	⊢ ( 𝑁 ∈ ℕ0 → 9 ∈ ℂ )
171	72	a1i	⊢ ( 𝑁 ∈ ℕ0 → 9 ≠ 0 )
172	170 171 23	exprecd	⊢ ( 𝑁 ∈ ℕ0 → ( ( 1 / 9 ) ↑ 𝑁 ) = ( 1 / ( 9 ↑ 𝑁 ) ) )
173	70 72	dividi	⊢ ( 9 / 9 ) = 1
174	173	oveq1i	⊢ ( ( 9 / 9 ) − ( 1 / 9 ) ) = ( 1 − ( 1 / 9 ) )
175		ax-1cn	⊢ 1 ∈ ℂ
176	70 72	pm3.2i	⊢ ( 9 ∈ ℂ ∧ 9 ≠ 0 )
177		divsubdir	⊢ ( ( 9 ∈ ℂ ∧ 1 ∈ ℂ ∧ ( 9 ∈ ℂ ∧ 9 ≠ 0 ) ) → ( ( 9 − 1 ) / 9 ) = ( ( 9 / 9 ) − ( 1 / 9 ) ) )
178	70 175 176 177	mp3an	⊢ ( ( 9 − 1 ) / 9 ) = ( ( 9 / 9 ) − ( 1 / 9 ) )
179		9m1e8	⊢ ( 9 − 1 ) = 8
180	179	oveq1i	⊢ ( ( 9 − 1 ) / 9 ) = ( 8 / 9 )
181	178 180	eqtr3i	⊢ ( ( 9 / 9 ) − ( 1 / 9 ) ) = ( 8 / 9 )
182	174 181	eqtr3i	⊢ ( 1 − ( 1 / 9 ) ) = ( 8 / 9 )
183	182	a1i	⊢ ( 𝑁 ∈ ℕ0 → ( 1 − ( 1 / 9 ) ) = ( 8 / 9 ) )
184	172 183	oveq12d	⊢ ( 𝑁 ∈ ℕ0 → ( ( ( 1 / 9 ) ↑ 𝑁 ) / ( 1 − ( 1 / 9 ) ) ) = ( ( 1 / ( 9 ↑ 𝑁 ) ) / ( 8 / 9 ) ) )
185	175	a1i	⊢ ( 𝑁 ∈ ℕ0 → 1 ∈ ℂ )
186		nnexpcl	⊢ ( ( 9 ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( 9 ↑ 𝑁 ) ∈ ℕ )
187	13 186	mpan	⊢ ( 𝑁 ∈ ℕ0 → ( 9 ↑ 𝑁 ) ∈ ℕ )
188	187	nncnd	⊢ ( 𝑁 ∈ ℕ0 → ( 9 ↑ 𝑁 ) ∈ ℂ )
189		8cn	⊢ 8 ∈ ℂ
190	189 70 72	divcli	⊢ ( 8 / 9 ) ∈ ℂ
191	190	a1i	⊢ ( 𝑁 ∈ ℕ0 → ( 8 / 9 ) ∈ ℂ )
192	187	nnne0d	⊢ ( 𝑁 ∈ ℕ0 → ( 9 ↑ 𝑁 ) ≠ 0 )
193		8nn	⊢ 8 ∈ ℕ
194	193	nnne0i	⊢ 8 ≠ 0
195	189 70 194 72	divne0i	⊢ ( 8 / 9 ) ≠ 0
196	195	a1i	⊢ ( 𝑁 ∈ ℕ0 → ( 8 / 9 ) ≠ 0 )
197	185 188 191 192 196	divdiv32d	⊢ ( 𝑁 ∈ ℕ0 → ( ( 1 / ( 9 ↑ 𝑁 ) ) / ( 8 / 9 ) ) = ( ( 1 / ( 8 / 9 ) ) / ( 9 ↑ 𝑁 ) ) )
198		recdiv	⊢ ( ( ( 8 ∈ ℂ ∧ 8 ≠ 0 ) ∧ ( 9 ∈ ℂ ∧ 9 ≠ 0 ) ) → ( 1 / ( 8 / 9 ) ) = ( 9 / 8 ) )
199	189 194 70 72 198	mp4an	⊢ ( 1 / ( 8 / 9 ) ) = ( 9 / 8 )
200	199	oveq1i	⊢ ( ( 1 / ( 8 / 9 ) ) / ( 9 ↑ 𝑁 ) ) = ( ( 9 / 8 ) / ( 9 ↑ 𝑁 ) )
201	189	a1i	⊢ ( 𝑁 ∈ ℕ0 → 8 ∈ ℂ )
202	194	a1i	⊢ ( 𝑁 ∈ ℕ0 → 8 ≠ 0 )
203	170 201 188 202 192	divdiv1d	⊢ ( 𝑁 ∈ ℕ0 → ( ( 9 / 8 ) / ( 9 ↑ 𝑁 ) ) = ( 9 / ( 8 · ( 9 ↑ 𝑁 ) ) ) )
204	200 203	syl5eq	⊢ ( 𝑁 ∈ ℕ0 → ( ( 1 / ( 8 / 9 ) ) / ( 9 ↑ 𝑁 ) ) = ( 9 / ( 8 · ( 9 ↑ 𝑁 ) ) ) )
205	184 197 204	3eqtrd	⊢ ( 𝑁 ∈ ℕ0 → ( ( ( 1 / 9 ) ↑ 𝑁 ) / ( 1 − ( 1 / 9 ) ) ) = ( 9 / ( 8 · ( 9 ↑ 𝑁 ) ) ) )
206	169 205	breqtrd	⊢ ( 𝑁 ∈ ℕ0 → seq 𝑁 ( + , ( 𝑘 ∈ ℕ0 ↦ ( ( 1 / 9 ) ↑ 𝑘 ) ) ) ⇝ ( 9 / ( 8 · ( 9 ↑ 𝑁 ) ) ) )
207		expcl	⊢ ( ( ( 1 / 9 ) ∈ ℂ ∧ 𝑛 ∈ ℕ0 ) → ( ( 1 / 9 ) ↑ 𝑛 ) ∈ ℂ )
208	151 24 207	sylancr	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( ( 1 / 9 ) ↑ 𝑛 ) ∈ ℂ )
209	168 208	eqeltrd	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( ( 𝑘 ∈ ℕ0 ↦ ( ( 1 / 9 ) ↑ 𝑘 ) ) ‘ 𝑛 ) ∈ ℂ )
210	24 68	syl	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( ( 𝑘 ∈ ℕ0 ↦ ( ( 2 / ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) ) · ( ( 1 / 9 ) ↑ 𝑘 ) ) ) ‘ 𝑛 ) = ( ( 2 / ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) ) · ( ( 1 / 9 ) ↑ 𝑛 ) ) )
211	168	oveq2d	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( ( 2 / ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) ) · ( ( 𝑘 ∈ ℕ0 ↦ ( ( 1 / 9 ) ↑ 𝑘 ) ) ‘ 𝑛 ) ) = ( ( 2 / ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) ) · ( ( 1 / 9 ) ↑ 𝑛 ) ) )
212	210 211	eqtr4d	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( ( 𝑘 ∈ ℕ0 ↦ ( ( 2 / ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) ) · ( ( 1 / 9 ) ↑ 𝑘 ) ) ) ‘ 𝑛 ) = ( ( 2 / ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) ) · ( ( 𝑘 ∈ ℕ0 ↦ ( ( 1 / 9 ) ↑ 𝑘 ) ) ‘ 𝑛 ) ) )
213	22 23 86 206 209 212	isermulc2	⊢ ( 𝑁 ∈ ℕ0 → seq 𝑁 ( + , ( 𝑘 ∈ ℕ0 ↦ ( ( 2 / ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) ) · ( ( 1 / 9 ) ↑ 𝑘 ) ) ) ) ⇝ ( ( 2 / ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) ) · ( 9 / ( 8 · ( 9 ↑ 𝑁 ) ) ) ) )
214		seqex	⊢ seq 𝑁 ( + , ( 𝑘 ∈ ℕ0 ↦ ( ( 2 / ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) ) · ( ( 1 / 9 ) ↑ 𝑘 ) ) ) ) ∈ V
215		ovex	⊢ ( ( 2 / ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) ) · ( 9 / ( 8 · ( 9 ↑ 𝑁 ) ) ) ) ∈ V
216	214 215	breldm	⊢ ( 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	⊢ ( 𝑁 ∈ ℕ0 → seq 𝑁 ( + , ( 𝑘 ∈ ℕ0 ↦ ( ( 2 / ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) ) · ( ( 1 / 9 ) ↑ 𝑘 ) ) ) ) ∈ dom ⇝ )
218	22 23 34 35 98 102 148 46 217	isumle	⊢ ( 𝑁 ∈ ℕ0 → Σ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) ≤ Σ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ( 2 / ( ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) )
219	102	recnd	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 2 / ( ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) ∈ ℂ )
220		3cn	⊢ 3 ∈ ℂ
221		4cn	⊢ 4 ∈ ℂ
222		2cn	⊢ 2 ∈ ℂ
223		4ne0	⊢ 4 ≠ 0
224		3ne0	⊢ 3 ≠ 0
225		2ne0	⊢ 2 ≠ 0
226	220 221 222 220 223 224 225	divdivdivi	⊢ ( ( 3 / 4 ) / ( 2 / 3 ) ) = ( ( 3 · 3 ) / ( 4 · 2 ) )
227		3t3e9	⊢ ( 3 · 3 ) = 9
228		4t2e8	⊢ ( 4 · 2 ) = 8
229	227 228	oveq12i	⊢ ( ( 3 · 3 ) / ( 4 · 2 ) ) = ( 9 / 8 )
230	226 229	eqtri	⊢ ( ( 3 / 4 ) / ( 2 / 3 ) ) = ( 9 / 8 )
231	230	oveq2i	⊢ ( ( 2 / 3 ) · ( ( 3 / 4 ) / ( 2 / 3 ) ) ) = ( ( 2 / 3 ) · ( 9 / 8 ) )
232	220 221 223	divcli	⊢ ( 3 / 4 ) ∈ ℂ
233	222 220 224	divcli	⊢ ( 2 / 3 ) ∈ ℂ
234	222 220 225 224	divne0i	⊢ ( 2 / 3 ) ≠ 0
235	232 233 234	divcan2i	⊢ ( ( 2 / 3 ) · ( ( 3 / 4 ) / ( 2 / 3 ) ) ) = ( 3 / 4 )
236	231 235	eqtr3i	⊢ ( ( 2 / 3 ) · ( 9 / 8 ) ) = ( 3 / 4 )
237	236	oveq1i	⊢ ( ( ( 2 / 3 ) · ( 9 / 8 ) ) / ( ( ( 2 · 𝑁 ) + 1 ) · ( 9 ↑ 𝑁 ) ) ) = ( ( 3 / 4 ) / ( ( ( 2 · 𝑁 ) + 1 ) · ( 9 ↑ 𝑁 ) ) )
238		2cnd	⊢ ( 𝑁 ∈ ℕ0 → 2 ∈ ℂ )
239	220	a1i	⊢ ( 𝑁 ∈ ℕ0 → 3 ∈ ℂ )
240	81	nncnd	⊢ ( 𝑁 ∈ ℕ0 → ( ( 2 · 𝑁 ) + 1 ) ∈ ℂ )
241	224	a1i	⊢ ( 𝑁 ∈ ℕ0 → 3 ≠ 0 )
242	81	nnne0d	⊢ ( 𝑁 ∈ ℕ0 → ( ( 2 · 𝑁 ) + 1 ) ≠ 0 )
243	238 239 240 241 242	divdiv1d	⊢ ( 𝑁 ∈ ℕ0 → ( ( 2 / 3 ) / ( ( 2 · 𝑁 ) + 1 ) ) = ( 2 / ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) ) )
244	243 203	oveq12d	⊢ ( 𝑁 ∈ ℕ0 → ( ( ( 2 / 3 ) / ( ( 2 · 𝑁 ) + 1 ) ) · ( ( 9 / 8 ) / ( 9 ↑ 𝑁 ) ) ) = ( ( 2 / ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) ) · ( 9 / ( 8 · ( 9 ↑ 𝑁 ) ) ) ) )
245	233	a1i	⊢ ( 𝑁 ∈ ℕ0 → ( 2 / 3 ) ∈ ℂ )
246	70 189 194	divcli	⊢ ( 9 / 8 ) ∈ ℂ
247	246	a1i	⊢ ( 𝑁 ∈ ℕ0 → ( 9 / 8 ) ∈ ℂ )
248	245 240 247 188 242 192	divmuldivd	⊢ ( 𝑁 ∈ ℕ0 → ( ( ( 2 / 3 ) / ( ( 2 · 𝑁 ) + 1 ) ) · ( ( 9 / 8 ) / ( 9 ↑ 𝑁 ) ) ) = ( ( ( 2 / 3 ) · ( 9 / 8 ) ) / ( ( ( 2 · 𝑁 ) + 1 ) · ( 9 ↑ 𝑁 ) ) ) )
249	244 248	eqtr3d	⊢ ( 𝑁 ∈ ℕ0 → ( ( 2 / ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) ) · ( 9 / ( 8 · ( 9 ↑ 𝑁 ) ) ) ) = ( ( ( 2 / 3 ) · ( 9 / 8 ) ) / ( ( ( 2 · 𝑁 ) + 1 ) · ( 9 ↑ 𝑁 ) ) ) )
250	221	a1i	⊢ ( 𝑁 ∈ ℕ0 → 4 ∈ ℂ )
251	250 240 188	mulassd	⊢ ( 𝑁 ∈ ℕ0 → ( ( 4 · ( ( 2 · 𝑁 ) + 1 ) ) · ( 9 ↑ 𝑁 ) ) = ( 4 · ( ( ( 2 · 𝑁 ) + 1 ) · ( 9 ↑ 𝑁 ) ) ) )
252	251	oveq2d	⊢ ( 𝑁 ∈ ℕ0 → ( 3 / ( ( 4 · ( ( 2 · 𝑁 ) + 1 ) ) · ( 9 ↑ 𝑁 ) ) ) = ( 3 / ( 4 · ( ( ( 2 · 𝑁 ) + 1 ) · ( 9 ↑ 𝑁 ) ) ) ) )
253	81 187	nnmulcld	⊢ ( 𝑁 ∈ ℕ0 → ( ( ( 2 · 𝑁 ) + 1 ) · ( 9 ↑ 𝑁 ) ) ∈ ℕ )
254	253	nncnd	⊢ ( 𝑁 ∈ ℕ0 → ( ( ( 2 · 𝑁 ) + 1 ) · ( 9 ↑ 𝑁 ) ) ∈ ℂ )
255	223	a1i	⊢ ( 𝑁 ∈ ℕ0 → 4 ≠ 0 )
256	253	nnne0d	⊢ ( 𝑁 ∈ ℕ0 → ( ( ( 2 · 𝑁 ) + 1 ) · ( 9 ↑ 𝑁 ) ) ≠ 0 )
257	239 250 254 255 256	divdiv1d	⊢ ( 𝑁 ∈ ℕ0 → ( ( 3 / 4 ) / ( ( ( 2 · 𝑁 ) + 1 ) · ( 9 ↑ 𝑁 ) ) ) = ( 3 / ( 4 · ( ( ( 2 · 𝑁 ) + 1 ) · ( 9 ↑ 𝑁 ) ) ) ) )
258	252 257	eqtr4d	⊢ ( 𝑁 ∈ ℕ0 → ( 3 / ( ( 4 · ( ( 2 · 𝑁 ) + 1 ) ) · ( 9 ↑ 𝑁 ) ) ) = ( ( 3 / 4 ) / ( ( ( 2 · 𝑁 ) + 1 ) · ( 9 ↑ 𝑁 ) ) ) )
259	237 249 258	3eqtr4a	⊢ ( 𝑁 ∈ ℕ0 → ( ( 2 / ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) ) · ( 9 / ( 8 · ( 9 ↑ 𝑁 ) ) ) ) = ( 3 / ( ( 4 · ( ( 2 · 𝑁 ) + 1 ) ) · ( 9 ↑ 𝑁 ) ) ) )
260	213 259	breqtrd	⊢ ( 𝑁 ∈ ℕ0 → seq 𝑁 ( + , ( 𝑘 ∈ ℕ0 ↦ ( ( 2 / ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) ) · ( ( 1 / 9 ) ↑ 𝑘 ) ) ) ) ⇝ ( 3 / ( ( 4 · ( ( 2 · 𝑁 ) + 1 ) ) · ( 9 ↑ 𝑁 ) ) ) )
261	22 23 98 219 260	isumclim	⊢ ( 𝑁 ∈ ℕ0 → Σ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ( 2 / ( ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) = ( 3 / ( ( 4 · ( ( 2 · 𝑁 ) + 1 ) ) · ( 9 ↑ 𝑁 ) ) ) )
262	218 261	breqtrd	⊢ ( 𝑁 ∈ ℕ0 → Σ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) ≤ ( 3 / ( ( 4 · ( ( 2 · 𝑁 ) + 1 ) ) · ( 9 ↑ 𝑁 ) ) ) )
263		4nn	⊢ 4 ∈ ℕ
264		nnmulcl	⊢ ( ( 4 ∈ ℕ ∧ ( ( 2 · 𝑁 ) + 1 ) ∈ ℕ ) → ( 4 · ( ( 2 · 𝑁 ) + 1 ) ) ∈ ℕ )
265	263 81 264	sylancr	⊢ ( 𝑁 ∈ ℕ0 → ( 4 · ( ( 2 · 𝑁 ) + 1 ) ) ∈ ℕ )
266	265 187	nnmulcld	⊢ ( 𝑁 ∈ ℕ0 → ( ( 4 · ( ( 2 · 𝑁 ) + 1 ) ) · ( 9 ↑ 𝑁 ) ) ∈ ℕ )
267		nndivre	⊢ ( ( 3 ∈ ℝ ∧ ( ( 4 · ( ( 2 · 𝑁 ) + 1 ) ) · ( 9 ↑ 𝑁 ) ) ∈ ℕ ) → ( 3 / ( ( 4 · ( ( 2 · 𝑁 ) + 1 ) ) · ( 9 ↑ 𝑁 ) ) ) ∈ ℝ )
268	124 266 267	sylancr	⊢ ( 𝑁 ∈ ℕ0 → ( 3 / ( ( 4 · ( ( 2 · 𝑁 ) + 1 ) ) · ( 9 ↑ 𝑁 ) ) ) ∈ ℝ )
269		elicc2	⊢ ( ( 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	⊢ ( 𝑁 ∈ ℕ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	⊢ ( 𝑁 ∈ ℕ0 → Σ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) ∈ ( 0 [,] ( 3 / ( ( 4 · ( ( 2 · 𝑁 ) + 1 ) ) · ( 9 ↑ 𝑁 ) ) ) ) )
272	54 271	eqeltrd	⊢ ( 𝑁 ∈ ℕ0 → ( ( log ‘ 2 ) − Σ 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) ) ∈ ( 0 [,] ( 3 / ( ( 4 · ( ( 2 · 𝑁 ) + 1 ) ) · ( 9 ↑ 𝑁 ) ) ) ) )