This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )