Theorem 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=\left(n\in \mathbb{N}⟼2{\left(\frac{1}{2}\right)}^n\right)$$
	erelem1.2	$$⊢G=\left(n\in {\mathbb{N}}_0⟼\frac{1}{n!}\right)$$
Assertion	ege2le3	$$⊢\left(2\le \mathrm{e}\wedge \mathrm{e}\le 3\right)$$

Proof

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