ege2le3

Description: Lemma for egt2lt3 . (Contributed by NM, 20-Mar-2005) (Proof shortened by Mario Carneiro, 28-Apr-2014)

	Ref	Expression
Hypotheses	erelem1.1	$⊢ F = (n \in ℕ ⟼ 2 {(\frac{1}{2})}^{n})$
	erelem1.2	$⊢ G = (n \in ℕ_{0} ⟼ \frac{1}{n!})$
Assertion	ege2le3	$⊢ (2 \leq e \land e \leq 3)$

Proof

Step	Hyp	Ref	Expression
1		erelem1.1	$⊢ F = (n \in ℕ ⟼ 2 {(\frac{1}{2})}^{n})$
2		erelem1.2	$⊢ G = (n \in ℕ_{0} ⟼ \frac{1}{n!})$
3		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
4		0nn0	$⊢ 0 \in ℕ_{0}$
5	4	a1i	$⊢ ⊤ \to 0 \in ℕ_{0}$
6		1e0p1	$⊢ 1 = 0 + 1$
7		0z	$⊢ 0 \in ℤ$
8		fveq2	$⊢ n = 0 \to n! = 0!$
9		fac0	$⊢ 0! = 1$
10	8 9	eqtrdi	$⊢ n = 0 \to n! = 1$
11	10	oveq2d	$⊢ n = 0 \to \frac{1}{n!} = \frac{1}{1}$
12		ax-1cn	$⊢ 1 \in ℂ$
13	12	div1i	$⊢ \frac{1}{1} = 1$
14	11 13	eqtrdi	$⊢ n = 0 \to \frac{1}{n!} = 1$
15		1ex	$⊢ 1 \in V$
16	14 2 15	fvmpt	$⊢ 0 \in ℕ_{0} \to G (0) = 1$
17	4 16	mp1i	$⊢ ⊤ \to G (0) = 1$
18	7 17	seq1i	$⊢ ⊤ \to seq 0 (+ G) (0) = 1$
19		1nn0	$⊢ 1 \in ℕ_{0}$
20		fveq2	$⊢ n = 1 \to n! = 1!$
21		fac1	$⊢ 1! = 1$
22	20 21	eqtrdi	$⊢ n = 1 \to n! = 1$
23	22	oveq2d	$⊢ n = 1 \to \frac{1}{n!} = \frac{1}{1}$
24	23 13	eqtrdi	$⊢ n = 1 \to \frac{1}{n!} = 1$
25	24 2 15	fvmpt	$⊢ 1 \in ℕ_{0} \to G (1) = 1$
26	19 25	mp1i	$⊢ ⊤ \to G (1) = 1$
27	3 5 6 18 26	seqp1d	$⊢ ⊤ \to seq 0 (+ G) (1) = 1 + 1$
28		df-2	$⊢ 2 = 1 + 1$
29	27 28	eqtr4di	$⊢ ⊤ \to seq 0 (+ G) (1) = 2$
30	19	a1i	$⊢ ⊤ \to 1 \in ℕ_{0}$
31		nn0z	$⊢ n \in ℕ_{0} \to n \in ℤ$
32		1exp	$⊢ n \in ℤ \to 1^{n} = 1$
33	31 32	syl	$⊢ n \in ℕ_{0} \to 1^{n} = 1$
34	33	oveq1d	$⊢ n \in ℕ_{0} \to \frac{1^{n}}{n!} = \frac{1}{n!}$
35	34	mpteq2ia	$⊢ (n \in ℕ_{0} ⟼ \frac{1^{n}}{n!}) = (n \in ℕ_{0} ⟼ \frac{1}{n!})$
36	2 35	eqtr4i	$⊢ G = (n \in ℕ_{0} ⟼ \frac{1^{n}}{n!})$
37	36	efcvg	$⊢ 1 \in ℂ \to seq 0 (+ G) ⇝ e^{1}$
38	12 37	mp1i	$⊢ ⊤ \to seq 0 (+ G) ⇝ e^{1}$
39		df-e	$⊢ e = e^{1}$
40	38 39	breqtrrdi	$⊢ ⊤ \to seq 0 (+ G) ⇝ e$
41		fveq2	$⊢ n = k \to n! = k!$
42	41	oveq2d	$⊢ n = k \to \frac{1}{n!} = \frac{1}{k!}$
43		ovex	$⊢ \frac{1}{k!} \in V$
44	42 2 43	fvmpt	$⊢ k \in ℕ_{0} \to G (k) = \frac{1}{k!}$
45	44	adantl	$⊢ (⊤ \land k \in ℕ_{0}) \to G (k) = \frac{1}{k!}$
46		faccl	$⊢ k \in ℕ_{0} \to k! \in ℕ$
47	46	adantl	$⊢ (⊤ \land k \in ℕ_{0}) \to k! \in ℕ$
48	47	nnrecred	$⊢ (⊤ \land k \in ℕ_{0}) \to \frac{1}{k!} \in ℝ$
49	45 48	eqeltrd	$⊢ (⊤ \land k \in ℕ_{0}) \to G (k) \in ℝ$
50	47	nnred	$⊢ (⊤ \land k \in ℕ_{0}) \to k! \in ℝ$
51	47	nngt0d	$⊢ (⊤ \land k \in ℕ_{0}) \to 0 < k!$
52		1re	$⊢ 1 \in ℝ$
53		0le1	$⊢ 0 \leq 1$
54		divge0	$⊢ ((1 \in ℝ \land 0 \leq 1) \land (k! \in ℝ \land 0 < k!)) \to 0 \leq \frac{1}{k!}$
55	52 53 54	mpanl12	$⊢ (k! \in ℝ \land 0 < k!) \to 0 \leq \frac{1}{k!}$
56	50 51 55	syl2anc	$⊢ (⊤ \land k \in ℕ_{0}) \to 0 \leq \frac{1}{k!}$
57	56 45	breqtrrd	$⊢ (⊤ \land k \in ℕ_{0}) \to 0 \leq G (k)$
58	3 30 40 49 57	climserle	$⊢ ⊤ \to seq 0 (+ G) (1) \leq e$
59	29 58	eqbrtrrd	$⊢ ⊤ \to 2 \leq e$
60	59	mptru	$⊢ 2 \leq e$
61		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
62		1zzd	$⊢ ⊤ \to 1 \in ℤ$
63	49	recnd	$⊢ (⊤ \land k \in ℕ_{0}) \to G (k) \in ℂ$
64	3 5 63 40	clim2ser	$⊢ ⊤ \to seq (0 + 1) (+ G) ⇝ (e - seq 0 (+ G) (0))$
65		0p1e1	$⊢ 0 + 1 = 1$
66		seqeq1	$⊢ 0 + 1 = 1 \to seq (0 + 1) (+ G) = seq 1 (+ G)$
67	65 66	ax-mp	$⊢ seq (0 + 1) (+ G) = seq 1 (+ G)$
68	18	mptru	$⊢ seq 0 (+ G) (0) = 1$
69	68	oveq2i	$⊢ e - seq 0 (+ G) (0) = e - 1$
70	64 67 69	3brtr3g	$⊢ ⊤ \to seq 1 (+ G) ⇝ (e - 1)$
71		2cnd	$⊢ ⊤ \to 2 \in ℂ$
72		oveq2	$⊢ n = k \to {(\frac{1}{2})}^{n} = {(\frac{1}{2})}^{k}$
73		eqid	$⊢ (n \in ℕ_{0} ⟼ {(\frac{1}{2})}^{n}) = (n \in ℕ_{0} ⟼ {(\frac{1}{2})}^{n})$
74		ovex	$⊢ {(\frac{1}{2})}^{k} \in V$
75	72 73 74	fvmpt	$⊢ k \in ℕ_{0} \to (n \in ℕ_{0} ⟼ {(\frac{1}{2})}^{n}) (k) = {(\frac{1}{2})}^{k}$
76	75	adantl	$⊢ (⊤ \land k \in ℕ_{0}) \to (n \in ℕ_{0} ⟼ {(\frac{1}{2})}^{n}) (k) = {(\frac{1}{2})}^{k}$
77		halfre	$⊢ \frac{1}{2} \in ℝ$
78		simpr	$⊢ (⊤ \land k \in ℕ_{0}) \to k \in ℕ_{0}$
79		reexpcl	$⊢ (\frac{1}{2} \in ℝ \land k \in ℕ_{0}) \to {(\frac{1}{2})}^{k} \in ℝ$
80	77 78 79	sylancr	$⊢ (⊤ \land k \in ℕ_{0}) \to {(\frac{1}{2})}^{k} \in ℝ$
81	80	recnd	$⊢ (⊤ \land k \in ℕ_{0}) \to {(\frac{1}{2})}^{k} \in ℂ$
82	76 81	eqeltrd	$⊢ (⊤ \land k \in ℕ_{0}) \to (n \in ℕ_{0} ⟼ {(\frac{1}{2})}^{n}) (k) \in ℂ$
83		1lt2	$⊢ 1 < 2$
84		2re	$⊢ 2 \in ℝ$
85		0le2	$⊢ 0 \leq 2$
86		absid	$⊢ (2 \in ℝ \land 0 \leq 2) \to \|2\| = 2$
87	84 85 86	mp2an	$⊢ \|2\| = 2$
88	83 87	breqtrri	$⊢ 1 < \|2\|$
89	88	a1i	$⊢ ⊤ \to 1 < \|2\|$
90	71 89 76	georeclim	$⊢ ⊤ \to seq 0 (+ (n \in ℕ_{0} ⟼ {(\frac{1}{2})}^{n})) ⇝ (\frac{2}{2 - 1})$
91		2m1e1	$⊢ 2 - 1 = 1$
92	91	oveq2i	$⊢ \frac{2}{2 - 1} = \frac{2}{1}$
93		2cn	$⊢ 2 \in ℂ$
94	93	div1i	$⊢ \frac{2}{1} = 2$
95	92 94	eqtri	$⊢ \frac{2}{2 - 1} = 2$
96	90 95	breqtrdi	$⊢ ⊤ \to seq 0 (+ (n \in ℕ_{0} ⟼ {(\frac{1}{2})}^{n})) ⇝ 2$
97	3 5 82 96	clim2ser	$⊢ ⊤ \to seq (0 + 1) (+ (n \in ℕ_{0} ⟼ {(\frac{1}{2})}^{n})) ⇝ (2 - seq 0 (+ (n \in ℕ_{0} ⟼ {(\frac{1}{2})}^{n})) (0))$
98		seqeq1	$⊢ 0 + 1 = 1 \to seq (0 + 1) (+ (n \in ℕ_{0} ⟼ {(\frac{1}{2})}^{n})) = seq 1 (+ (n \in ℕ_{0} ⟼ {(\frac{1}{2})}^{n}))$
99	65 98	ax-mp	$⊢ seq (0 + 1) (+ (n \in ℕ_{0} ⟼ {(\frac{1}{2})}^{n})) = seq 1 (+ (n \in ℕ_{0} ⟼ {(\frac{1}{2})}^{n}))$
100		oveq2	$⊢ n = 0 \to {(\frac{1}{2})}^{n} = {(\frac{1}{2})}^{0}$
101		ovex	$⊢ {(\frac{1}{2})}^{0} \in V$
102	100 73 101	fvmpt	$⊢ 0 \in ℕ_{0} \to (n \in ℕ_{0} ⟼ {(\frac{1}{2})}^{n}) (0) = {(\frac{1}{2})}^{0}$
103	4 102	ax-mp	$⊢ (n \in ℕ_{0} ⟼ {(\frac{1}{2})}^{n}) (0) = {(\frac{1}{2})}^{0}$
104		halfcn	$⊢ \frac{1}{2} \in ℂ$
105		exp0	$⊢ \frac{1}{2} \in ℂ \to {(\frac{1}{2})}^{0} = 1$
106	104 105	ax-mp	$⊢ {(\frac{1}{2})}^{0} = 1$
107	103 106	eqtri	$⊢ (n \in ℕ_{0} ⟼ {(\frac{1}{2})}^{n}) (0) = 1$
108	107	a1i	$⊢ ⊤ \to (n \in ℕ_{0} ⟼ {(\frac{1}{2})}^{n}) (0) = 1$
109	7 108	seq1i	$⊢ ⊤ \to seq 0 (+ (n \in ℕ_{0} ⟼ {(\frac{1}{2})}^{n})) (0) = 1$
110	109	mptru	$⊢ seq 0 (+ (n \in ℕ_{0} ⟼ {(\frac{1}{2})}^{n})) (0) = 1$
111	110	oveq2i	$⊢ 2 - seq 0 (+ (n \in ℕ_{0} ⟼ {(\frac{1}{2})}^{n})) (0) = 2 - 1$
112	111 91	eqtri	$⊢ 2 - seq 0 (+ (n \in ℕ_{0} ⟼ {(\frac{1}{2})}^{n})) (0) = 1$
113	97 99 112	3brtr3g	$⊢ ⊤ \to seq 1 (+ (n \in ℕ_{0} ⟼ {(\frac{1}{2})}^{n})) ⇝ 1$
114		nnnn0	$⊢ k \in ℕ \to k \in ℕ_{0}$
115	114 82	sylan2	$⊢ (⊤ \land k \in ℕ) \to (n \in ℕ_{0} ⟼ {(\frac{1}{2})}^{n}) (k) \in ℂ$
116	72	oveq2d	$⊢ n = k \to 2 {(\frac{1}{2})}^{n} = 2 {(\frac{1}{2})}^{k}$
117		ovex	$⊢ 2 {(\frac{1}{2})}^{k} \in V$
118	116 1 117	fvmpt	$⊢ k \in ℕ \to F (k) = 2 {(\frac{1}{2})}^{k}$
119	118	adantl	$⊢ (⊤ \land k \in ℕ) \to F (k) = 2 {(\frac{1}{2})}^{k}$
120	114 76	sylan2	$⊢ (⊤ \land k \in ℕ) \to (n \in ℕ_{0} ⟼ {(\frac{1}{2})}^{n}) (k) = {(\frac{1}{2})}^{k}$
121	120	oveq2d	$⊢ (⊤ \land k \in ℕ) \to 2 (n \in ℕ_{0} ⟼ {(\frac{1}{2})}^{n}) (k) = 2 {(\frac{1}{2})}^{k}$
122	119 121	eqtr4d	$⊢ (⊤ \land k \in ℕ) \to F (k) = 2 (n \in ℕ_{0} ⟼ {(\frac{1}{2})}^{n}) (k)$
123	61 62 71 113 115 122	isermulc2	$⊢ ⊤ \to seq 1 (+ F) ⇝ 2 \cdot 1$
124		2t1e2	$⊢ 2 \cdot 1 = 2$
125	123 124	breqtrdi	$⊢ ⊤ \to seq 1 (+ F) ⇝ 2$
126	114 49	sylan2	$⊢ (⊤ \land k \in ℕ) \to G (k) \in ℝ$
127		remulcl	$⊢ (2 \in ℝ \land {(\frac{1}{2})}^{k} \in ℝ) \to 2 {(\frac{1}{2})}^{k} \in ℝ$
128	84 80 127	sylancr	$⊢ (⊤ \land k \in ℕ_{0}) \to 2 {(\frac{1}{2})}^{k} \in ℝ$
129	114 128	sylan2	$⊢ (⊤ \land k \in ℕ) \to 2 {(\frac{1}{2})}^{k} \in ℝ$
130	119 129	eqeltrd	$⊢ (⊤ \land k \in ℕ) \to F (k) \in ℝ$
131		faclbnd2	$⊢ k \in ℕ_{0} \to \frac{2^{k}}{2} \leq k!$
132	131	adantl	$⊢ (⊤ \land k \in ℕ_{0}) \to \frac{2^{k}}{2} \leq k!$
133		2nn	$⊢ 2 \in ℕ$
134		nnexpcl	$⊢ (2 \in ℕ \land k \in ℕ_{0}) \to 2^{k} \in ℕ$
135	133 78 134	sylancr	$⊢ (⊤ \land k \in ℕ_{0}) \to 2^{k} \in ℕ$
136	135	nnrpd	$⊢ (⊤ \land k \in ℕ_{0}) \to 2^{k} \in ℝ^{+}$
137	136	rphalfcld	$⊢ (⊤ \land k \in ℕ_{0}) \to \frac{2^{k}}{2} \in ℝ^{+}$
138	47	nnrpd	$⊢ (⊤ \land k \in ℕ_{0}) \to k! \in ℝ^{+}$
139	137 138	lerecd	$⊢ (⊤ \land k \in ℕ_{0}) \to (\frac{2^{k}}{2} \leq k! \leftrightarrow \frac{1}{k!} \leq \frac{1}{\frac{2^{k}}{2}})$
140	132 139	mpbid	$⊢ (⊤ \land k \in ℕ_{0}) \to \frac{1}{k!} \leq \frac{1}{\frac{2^{k}}{2}}$
141		2cnd	$⊢ (⊤ \land k \in ℕ_{0}) \to 2 \in ℂ$
142	135	nncnd	$⊢ (⊤ \land k \in ℕ_{0}) \to 2^{k} \in ℂ$
143	135	nnne0d	$⊢ (⊤ \land k \in ℕ_{0}) \to 2^{k} \neq 0$
144	141 142 143	divrecd	$⊢ (⊤ \land k \in ℕ_{0}) \to \frac{2}{2^{k}} = 2 (\frac{1}{2^{k}})$
145		2ne0	$⊢ 2 \neq 0$
146		recdiv	$⊢ ((2^{k} \in ℂ \land 2^{k} \neq 0) \land (2 \in ℂ \land 2 \neq 0)) \to \frac{1}{\frac{2^{k}}{2}} = \frac{2}{2^{k}}$
147	93 145 146	mpanr12	$⊢ (2^{k} \in ℂ \land 2^{k} \neq 0) \to \frac{1}{\frac{2^{k}}{2}} = \frac{2}{2^{k}}$
148	142 143 147	syl2anc	$⊢ (⊤ \land k \in ℕ_{0}) \to \frac{1}{\frac{2^{k}}{2}} = \frac{2}{2^{k}}$
149	145	a1i	$⊢ (⊤ \land k \in ℕ_{0}) \to 2 \neq 0$
150		nn0z	$⊢ k \in ℕ_{0} \to k \in ℤ$
151	150	adantl	$⊢ (⊤ \land k \in ℕ_{0}) \to k \in ℤ$
152	141 149 151	exprecd	$⊢ (⊤ \land k \in ℕ_{0}) \to {(\frac{1}{2})}^{k} = \frac{1}{2^{k}}$
153	152	oveq2d	$⊢ (⊤ \land k \in ℕ_{0}) \to 2 {(\frac{1}{2})}^{k} = 2 (\frac{1}{2^{k}})$
154	144 148 153	3eqtr4rd	$⊢ (⊤ \land k \in ℕ_{0}) \to 2 {(\frac{1}{2})}^{k} = \frac{1}{\frac{2^{k}}{2}}$
155	140 154	breqtrrd	$⊢ (⊤ \land k \in ℕ_{0}) \to \frac{1}{k!} \leq 2 {(\frac{1}{2})}^{k}$
156	114 155	sylan2	$⊢ (⊤ \land k \in ℕ) \to \frac{1}{k!} \leq 2 {(\frac{1}{2})}^{k}$
157	114 45	sylan2	$⊢ (⊤ \land k \in ℕ) \to G (k) = \frac{1}{k!}$
158	156 157 119	3brtr4d	$⊢ (⊤ \land k \in ℕ) \to G (k) \leq F (k)$
159	61 62 70 125 126 130 158	iserle	$⊢ ⊤ \to e - 1 \leq 2$
160	159	mptru	$⊢ e - 1 \leq 2$
161		ere	$⊢ e \in ℝ$
162	161 52 84	lesubaddi	$⊢ e - 1 \leq 2 \leftrightarrow e \leq 2 + 1$
163	160 162	mpbi	$⊢ e \leq 2 + 1$
164		df-3	$⊢ 3 = 2 + 1$
165	163 164	breqtrri	$⊢ e \leq 3$
166	60 165	pm3.2i	$⊢ (2 \leq e \land e \leq 3)$

Metamath Proof Explorer

Theorem ege2le3

Proof