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	⊢ 𝐹 = ( 𝑛 ∈ ℕ ↦ ( 2 · ( ( 1 / 2 ) ↑ 𝑛 ) ) )
	erelem1.2	⊢ 𝐺 = ( 𝑛 ∈ ℕ0 ↦ ( 1 / ( ! ‘ 𝑛 ) ) )
Assertion	ege2le3	⊢ ( 2 ≤ e ∧ e ≤ 3 )

Proof

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