log2tlbnd

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

		Ref	Expression
	Assertion	log2tlbnd	$⊢ N \in ℕ_{0} \to \log 2 - \sum_{n = 0}^{N - 1} (\frac{2}{3 (2 n + 1) 9^{n}}) \in [0, \frac{3}{4 (2 \cdot N + 1) 9^{N}}]$

Proof

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

Metamath Proof Explorer

Theorem log2tlbnd

Proof