Metamath Proof Explorer

Theorem pntpbnd1a

Description: Lemma for pntpbnd . (Contributed by Mario Carneiro, 11-Apr-2016) Replace reference to OLD theorem. (Revised by Wolf Lammen, 8-Sep-2020)

Ref Expression
Hypotheses pntpbnd.r ⊢ 𝑅 = ( 𝑎 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑎 ) − 𝑎 ) )
pntpbnd1.e ⊢ ( 𝜑 → 𝐸 ∈ ( 0 (,) 1 ) )
pntpbnd1.x ⊢ 𝑋 = ( exp ‘ ( 2 / 𝐸 ) )
pntpbnd1.y ⊢ ( 𝜑 → 𝑌 ∈ ( 𝑋 (,) +∞ ) )
pntpbnd1a.1 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
pntpbnd1a.2 ⊢ ( 𝜑 → ( 𝑌 < 𝑁 ∧ 𝑁 ≤ ( 𝐾 · 𝑌 ) ) )
pntpbnd1a.3 ⊢ ( 𝜑 → ( abs ‘ ( 𝑅 ‘ 𝑁 ) ) ≤ ( abs ‘ ( ( 𝑅 ‘ ( 𝑁 + 1 ) ) − ( 𝑅 ‘ 𝑁 ) ) ) )
Assertion pntpbnd1a ( 𝜑 → ( abs ‘ ( ( 𝑅 ‘ 𝑁 ) / 𝑁 ) ) ≤ 𝐸 )

Proof

Step Hyp Ref Expression
1 pntpbnd.r ⊢ 𝑅 = ( 𝑎 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑎 ) − 𝑎 ) )
2 pntpbnd1.e ⊢ ( 𝜑 → 𝐸 ∈ ( 0 (,) 1 ) )
3 pntpbnd1.x ⊢ 𝑋 = ( exp ‘ ( 2 / 𝐸 ) )
4 pntpbnd1.y ⊢ ( 𝜑 → 𝑌 ∈ ( 𝑋 (,) +∞ ) )
5 pntpbnd1a.1 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
6 pntpbnd1a.2 ⊢ ( 𝜑 → ( 𝑌 < 𝑁 ∧ 𝑁 ≤ ( 𝐾 · 𝑌 ) ) )
7 pntpbnd1a.3 ⊢ ( 𝜑 → ( abs ‘ ( 𝑅 ‘ 𝑁 ) ) ≤ ( abs ‘ ( ( 𝑅 ‘ ( 𝑁 + 1 ) ) − ( 𝑅 ‘ 𝑁 ) ) ) )
8 5 nnrpd ⊢ ( 𝜑 → 𝑁 ∈ ℝ+ )
9 1 pntrf ⊢ 𝑅 : ℝ+ ⟶ ℝ
10 9 ffvelcdmi ⊢ ( 𝑁 ∈ ℝ+ → ( 𝑅 ‘ 𝑁 ) ∈ ℝ )
11 8 10 syl ⊢ ( 𝜑 → ( 𝑅 ‘ 𝑁 ) ∈ ℝ )
12 11 8 rerpdivcld ⊢ ( 𝜑 → ( ( 𝑅 ‘ 𝑁 ) / 𝑁 ) ∈ ℝ )
13 12 recnd ⊢ ( 𝜑 → ( ( 𝑅 ‘ 𝑁 ) / 𝑁 ) ∈ ℂ )
14 13 abscld ⊢ ( 𝜑 → ( abs ‘ ( ( 𝑅 ‘ 𝑁 ) / 𝑁 ) ) ∈ ℝ )
15 8 relogcld ⊢ ( 𝜑 → ( log ‘ 𝑁 ) ∈ ℝ )
16 15 8 rerpdivcld ⊢ ( 𝜑 → ( ( log ‘ 𝑁 ) / 𝑁 ) ∈ ℝ )
17 ioossre ⊢ ( 0 (,) 1 ) ⊆ ℝ
18 17 2 sselid ⊢ ( 𝜑 → 𝐸 ∈ ℝ )
19 11 recnd ⊢ ( 𝜑 → ( 𝑅 ‘ 𝑁 ) ∈ ℂ )
20 5 nnred ⊢ ( 𝜑 → 𝑁 ∈ ℝ )
21 20 recnd ⊢ ( 𝜑 → 𝑁 ∈ ℂ )
22 5 nnne0d ⊢ ( 𝜑 → 𝑁 ≠ 0 )
23 19 21 22 absdivd ⊢ ( 𝜑 → ( abs ‘ ( ( 𝑅 ‘ 𝑁 ) / 𝑁 ) ) = ( ( abs ‘ ( 𝑅 ‘ 𝑁 ) ) / ( abs ‘ 𝑁 ) ) )
24 5 nnnn0d ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
25 24 nn0ge0d ⊢ ( 𝜑 → 0 ≤ 𝑁 )
26 20 25 absidd ⊢ ( 𝜑 → ( abs ‘ 𝑁 ) = 𝑁 )
27 26 oveq2d ⊢ ( 𝜑 → ( ( abs ‘ ( 𝑅 ‘ 𝑁 ) ) / ( abs ‘ 𝑁 ) ) = ( ( abs ‘ ( 𝑅 ‘ 𝑁 ) ) / 𝑁 ) )
28 23 27 eqtrd ⊢ ( 𝜑 → ( abs ‘ ( ( 𝑅 ‘ 𝑁 ) / 𝑁 ) ) = ( ( abs ‘ ( 𝑅 ‘ 𝑁 ) ) / 𝑁 ) )
29 19 abscld ⊢ ( 𝜑 → ( abs ‘ ( 𝑅 ‘ 𝑁 ) ) ∈ ℝ )
30 5 peano2nnd ⊢ ( 𝜑 → ( 𝑁 + 1 ) ∈ ℕ )
31 vmacl ⊢ ( ( 𝑁 + 1 ) ∈ ℕ → ( Λ ‘ ( 𝑁 + 1 ) ) ∈ ℝ )
32 30 31 syl ⊢ ( 𝜑 → ( Λ ‘ ( 𝑁 + 1 ) ) ∈ ℝ )
33 peano2rem ⊢ ( ( Λ ‘ ( 𝑁 + 1 ) ) ∈ ℝ → ( ( Λ ‘ ( 𝑁 + 1 ) ) − 1 ) ∈ ℝ )
34 32 33 syl ⊢ ( 𝜑 → ( ( Λ ‘ ( 𝑁 + 1 ) ) − 1 ) ∈ ℝ )
35 34 recnd ⊢ ( 𝜑 → ( ( Λ ‘ ( 𝑁 + 1 ) ) − 1 ) ∈ ℂ )
36 35 abscld ⊢ ( 𝜑 → ( abs ‘ ( ( Λ ‘ ( 𝑁 + 1 ) ) − 1 ) ) ∈ ℝ )
37 30 nnrpd ⊢ ( 𝜑 → ( 𝑁 + 1 ) ∈ ℝ+ )
38 1 pntrval ⊢ ( ( 𝑁 + 1 ) ∈ ℝ+ → ( 𝑅 ‘ ( 𝑁 + 1 ) ) = ( ( ψ ‘ ( 𝑁 + 1 ) ) − ( 𝑁 + 1 ) ) )
39 37 38 syl ⊢ ( 𝜑 → ( 𝑅 ‘ ( 𝑁 + 1 ) ) = ( ( ψ ‘ ( 𝑁 + 1 ) ) − ( 𝑁 + 1 ) ) )
40 1 pntrval ⊢ ( 𝑁 ∈ ℝ+ → ( 𝑅 ‘ 𝑁 ) = ( ( ψ ‘ 𝑁 ) − 𝑁 ) )
41 8 40 syl ⊢ ( 𝜑 → ( 𝑅 ‘ 𝑁 ) = ( ( ψ ‘ 𝑁 ) − 𝑁 ) )
42 39 41 oveq12d ⊢ ( 𝜑 → ( ( 𝑅 ‘ ( 𝑁 + 1 ) ) − ( 𝑅 ‘ 𝑁 ) ) = ( ( ( ψ ‘ ( 𝑁 + 1 ) ) − ( 𝑁 + 1 ) ) − ( ( ψ ‘ 𝑁 ) − 𝑁 ) ) )
43 peano2re ⊢ ( 𝑁 ∈ ℝ → ( 𝑁 + 1 ) ∈ ℝ )
44 20 43 syl ⊢ ( 𝜑 → ( 𝑁 + 1 ) ∈ ℝ )
45 chpcl ⊢ ( ( 𝑁 + 1 ) ∈ ℝ → ( ψ ‘ ( 𝑁 + 1 ) ) ∈ ℝ )
46 44 45 syl ⊢ ( 𝜑 → ( ψ ‘ ( 𝑁 + 1 ) ) ∈ ℝ )
47 46 recnd ⊢ ( 𝜑 → ( ψ ‘ ( 𝑁 + 1 ) ) ∈ ℂ )
48 44 recnd ⊢ ( 𝜑 → ( 𝑁 + 1 ) ∈ ℂ )
49 chpcl ⊢ ( 𝑁 ∈ ℝ → ( ψ ‘ 𝑁 ) ∈ ℝ )
50 20 49 syl ⊢ ( 𝜑 → ( ψ ‘ 𝑁 ) ∈ ℝ )
51 50 recnd ⊢ ( 𝜑 → ( ψ ‘ 𝑁 ) ∈ ℂ )
52 47 48 51 21 sub4d ⊢ ( 𝜑 → ( ( ( ψ ‘ ( 𝑁 + 1 ) ) − ( 𝑁 + 1 ) ) − ( ( ψ ‘ 𝑁 ) − 𝑁 ) ) = ( ( ( ψ ‘ ( 𝑁 + 1 ) ) − ( ψ ‘ 𝑁 ) ) − ( ( 𝑁 + 1 ) − 𝑁 ) ) )
53 32 recnd ⊢ ( 𝜑 → ( Λ ‘ ( 𝑁 + 1 ) ) ∈ ℂ )
54 chpp1 ⊢ ( 𝑁 ∈ ℕ0 → ( ψ ‘ ( 𝑁 + 1 ) ) = ( ( ψ ‘ 𝑁 ) + ( Λ ‘ ( 𝑁 + 1 ) ) ) )
55 24 54 syl ⊢ ( 𝜑 → ( ψ ‘ ( 𝑁 + 1 ) ) = ( ( ψ ‘ 𝑁 ) + ( Λ ‘ ( 𝑁 + 1 ) ) ) )
56 51 53 55 mvrladdd ⊢ ( 𝜑 → ( ( ψ ‘ ( 𝑁 + 1 ) ) − ( ψ ‘ 𝑁 ) ) = ( Λ ‘ ( 𝑁 + 1 ) ) )
57 ax-1cn ⊢ 1 ∈ ℂ
58 pncan2 ⊢ ( ( 𝑁 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝑁 + 1 ) − 𝑁 ) = 1 )
59 21 57 58 sylancl ⊢ ( 𝜑 → ( ( 𝑁 + 1 ) − 𝑁 ) = 1 )
60 56 59 oveq12d ⊢ ( 𝜑 → ( ( ( ψ ‘ ( 𝑁 + 1 ) ) − ( ψ ‘ 𝑁 ) ) − ( ( 𝑁 + 1 ) − 𝑁 ) ) = ( ( Λ ‘ ( 𝑁 + 1 ) ) − 1 ) )
61 42 52 60 3eqtrd ⊢ ( 𝜑 → ( ( 𝑅 ‘ ( 𝑁 + 1 ) ) − ( 𝑅 ‘ 𝑁 ) ) = ( ( Λ ‘ ( 𝑁 + 1 ) ) − 1 ) )
62 61 fveq2d ⊢ ( 𝜑 → ( abs ‘ ( ( 𝑅 ‘ ( 𝑁 + 1 ) ) − ( 𝑅 ‘ 𝑁 ) ) ) = ( abs ‘ ( ( Λ ‘ ( 𝑁 + 1 ) ) − 1 ) ) )
63 7 62 breqtrd ⊢ ( 𝜑 → ( abs ‘ ( 𝑅 ‘ 𝑁 ) ) ≤ ( abs ‘ ( ( Λ ‘ ( 𝑁 + 1 ) ) − 1 ) ) )
64 1red ⊢ ( 𝜑 → 1 ∈ ℝ )
65 64 15 resubcld ⊢ ( 𝜑 → ( 1 − ( log ‘ 𝑁 ) ) ∈ ℝ )
66 0red ⊢ ( 𝜑 → 0 ∈ ℝ )
67 2re ⊢ 2 ∈ ℝ
68 eliooord ⊢ ( 𝐸 ∈ ( 0 (,) 1 ) → ( 0 < 𝐸 ∧ 𝐸 < 1 ) )
69 2 68 syl ⊢ ( 𝜑 → ( 0 < 𝐸 ∧ 𝐸 < 1 ) )
70 69 simpld ⊢ ( 𝜑 → 0 < 𝐸 )
71 18 70 elrpd ⊢ ( 𝜑 → 𝐸 ∈ ℝ+ )
72 rerpdivcl ⊢ ( ( 2 ∈ ℝ ∧ 𝐸 ∈ ℝ+ ) → ( 2 / 𝐸 ) ∈ ℝ )
73 67 71 72 sylancr ⊢ ( 𝜑 → ( 2 / 𝐸 ) ∈ ℝ )
74 67 a1i ⊢ ( 𝜑 → 2 ∈ ℝ )
75 1lt2 ⊢ 1 < 2
76 75 a1i ⊢ ( 𝜑 → 1 < 2 )
77 2cn ⊢ 2 ∈ ℂ
78 77 div1i ⊢ ( 2 / 1 ) = 2
79 69 simprd ⊢ ( 𝜑 → 𝐸 < 1 )
80 0lt1 ⊢ 0 < 1
81 80 a1i ⊢ ( 𝜑 → 0 < 1 )
82 2pos ⊢ 0 < 2
83 82 a1i ⊢ ( 𝜑 → 0 < 2 )
84 ltdiv2 ⊢ ( ( ( 𝐸 ∈ ℝ ∧ 0 < 𝐸 ) ∧ ( 1 ∈ ℝ ∧ 0 < 1 ) ∧ ( 2 ∈ ℝ ∧ 0 < 2 ) ) → ( 𝐸 < 1 ↔ ( 2 / 1 ) < ( 2 / 𝐸 ) ) )
85 18 70 64 81 74 83 84 syl222anc ⊢ ( 𝜑 → ( 𝐸 < 1 ↔ ( 2 / 1 ) < ( 2 / 𝐸 ) ) )
86 79 85 mpbid ⊢ ( 𝜑 → ( 2 / 1 ) < ( 2 / 𝐸 ) )
87 78 86 eqbrtrrid ⊢ ( 𝜑 → 2 < ( 2 / 𝐸 ) )
88 64 74 73 76 87 lttrd ⊢ ( 𝜑 → 1 < ( 2 / 𝐸 ) )
89 73 rpefcld ⊢ ( 𝜑 → ( exp ‘ ( 2 / 𝐸 ) ) ∈ ℝ+ )
90 3 89 eqeltrid ⊢ ( 𝜑 → 𝑋 ∈ ℝ+ )
91 90 rpred ⊢ ( 𝜑 → 𝑋 ∈ ℝ )
92 90 rpxrd ⊢ ( 𝜑 → 𝑋 ∈ ℝ* )
93 elioopnf ⊢ ( 𝑋 ∈ ℝ* → ( 𝑌 ∈ ( 𝑋 (,) +∞ ) ↔ ( 𝑌 ∈ ℝ ∧ 𝑋 < 𝑌 ) ) )
94 92 93 syl ⊢ ( 𝜑 → ( 𝑌 ∈ ( 𝑋 (,) +∞ ) ↔ ( 𝑌 ∈ ℝ ∧ 𝑋 < 𝑌 ) ) )
95 4 94 mpbid ⊢ ( 𝜑 → ( 𝑌 ∈ ℝ ∧ 𝑋 < 𝑌 ) )
96 95 simpld ⊢ ( 𝜑 → 𝑌 ∈ ℝ )
97 95 simprd ⊢ ( 𝜑 → 𝑋 < 𝑌 )
98 6 simpld ⊢ ( 𝜑 → 𝑌 < 𝑁 )
99 91 96 20 97 98 lttrd ⊢ ( 𝜑 → 𝑋 < 𝑁 )
100 3 99 eqbrtrrid ⊢ ( 𝜑 → ( exp ‘ ( 2 / 𝐸 ) ) < 𝑁 )
101 8 reeflogd ⊢ ( 𝜑 → ( exp ‘ ( log ‘ 𝑁 ) ) = 𝑁 )
102 100 101 breqtrrd ⊢ ( 𝜑 → ( exp ‘ ( 2 / 𝐸 ) ) < ( exp ‘ ( log ‘ 𝑁 ) ) )
103 eflt ⊢ ( ( ( 2 / 𝐸 ) ∈ ℝ ∧ ( log ‘ 𝑁 ) ∈ ℝ ) → ( ( 2 / 𝐸 ) < ( log ‘ 𝑁 ) ↔ ( exp ‘ ( 2 / 𝐸 ) ) < ( exp ‘ ( log ‘ 𝑁 ) ) ) )
104 73 15 103 syl2anc ⊢ ( 𝜑 → ( ( 2 / 𝐸 ) < ( log ‘ 𝑁 ) ↔ ( exp ‘ ( 2 / 𝐸 ) ) < ( exp ‘ ( log ‘ 𝑁 ) ) ) )
105 102 104 mpbird ⊢ ( 𝜑 → ( 2 / 𝐸 ) < ( log ‘ 𝑁 ) )
106 64 73 15 88 105 lttrd ⊢ ( 𝜑 → 1 < ( log ‘ 𝑁 ) )
107 64 15 106 ltled ⊢ ( 𝜑 → 1 ≤ ( log ‘ 𝑁 ) )
108 1re ⊢ 1 ∈ ℝ
109 suble0 ⊢ ( ( 1 ∈ ℝ ∧ ( log ‘ 𝑁 ) ∈ ℝ ) → ( ( 1 − ( log ‘ 𝑁 ) ) ≤ 0 ↔ 1 ≤ ( log ‘ 𝑁 ) ) )
110 108 15 109 sylancr ⊢ ( 𝜑 → ( ( 1 − ( log ‘ 𝑁 ) ) ≤ 0 ↔ 1 ≤ ( log ‘ 𝑁 ) ) )
111 107 110 mpbird ⊢ ( 𝜑 → ( 1 − ( log ‘ 𝑁 ) ) ≤ 0 )
112 vmage0 ⊢ ( ( 𝑁 + 1 ) ∈ ℕ → 0 ≤ ( Λ ‘ ( 𝑁 + 1 ) ) )
113 30 112 syl ⊢ ( 𝜑 → 0 ≤ ( Λ ‘ ( 𝑁 + 1 ) ) )
114 65 66 32 111 113 letrd ⊢ ( 𝜑 → ( 1 − ( log ‘ 𝑁 ) ) ≤ ( Λ ‘ ( 𝑁 + 1 ) ) )
115 37 relogcld ⊢ ( 𝜑 → ( log ‘ ( 𝑁 + 1 ) ) ∈ ℝ )
116 readdcl ⊢ ( ( 1 ∈ ℝ ∧ ( log ‘ 𝑁 ) ∈ ℝ ) → ( 1 + ( log ‘ 𝑁 ) ) ∈ ℝ )
117 108 15 116 sylancr ⊢ ( 𝜑 → ( 1 + ( log ‘ 𝑁 ) ) ∈ ℝ )
118 vmalelog ⊢ ( ( 𝑁 + 1 ) ∈ ℕ → ( Λ ‘ ( 𝑁 + 1 ) ) ≤ ( log ‘ ( 𝑁 + 1 ) ) )
119 30 118 syl ⊢ ( 𝜑 → ( Λ ‘ ( 𝑁 + 1 ) ) ≤ ( log ‘ ( 𝑁 + 1 ) ) )
120 74 20 remulcld ⊢ ( 𝜑 → ( 2 · 𝑁 ) ∈ ℝ )
121 epr ⊢ e ∈ ℝ+
122 rpmulcl ⊢ ( ( e ∈ ℝ+ ∧ 𝑁 ∈ ℝ+ ) → ( e · 𝑁 ) ∈ ℝ+ )
123 121 8 122 sylancr ⊢ ( 𝜑 → ( e · 𝑁 ) ∈ ℝ+ )
124 123 rpred ⊢ ( 𝜑 → ( e · 𝑁 ) ∈ ℝ )
125 5 nnge1d ⊢ ( 𝜑 → 1 ≤ 𝑁 )
126 64 20 20 125 leadd2dd ⊢ ( 𝜑 → ( 𝑁 + 1 ) ≤ ( 𝑁 + 𝑁 ) )
127 21 2timesd ⊢ ( 𝜑 → ( 2 · 𝑁 ) = ( 𝑁 + 𝑁 ) )
128 126 127 breqtrrd ⊢ ( 𝜑 → ( 𝑁 + 1 ) ≤ ( 2 · 𝑁 ) )
129 ere ⊢ e ∈ ℝ
130 egt2lt3 ⊢ ( 2 < e ∧ e < 3 )
131 130 simpli ⊢ 2 < e
132 67 129 131 ltleii ⊢ 2 ≤ e
133 132 a1i ⊢ ( 𝜑 → 2 ≤ e )
134 129 a1i ⊢ ( 𝜑 → e ∈ ℝ )
135 5 nngt0d ⊢ ( 𝜑 → 0 < 𝑁 )
136 lemul1 ⊢ ( ( 2 ∈ ℝ ∧ e ∈ ℝ ∧ ( 𝑁 ∈ ℝ ∧ 0 < 𝑁 ) ) → ( 2 ≤ e ↔ ( 2 · 𝑁 ) ≤ ( e · 𝑁 ) ) )
137 74 134 20 135 136 syl112anc ⊢ ( 𝜑 → ( 2 ≤ e ↔ ( 2 · 𝑁 ) ≤ ( e · 𝑁 ) ) )
138 133 137 mpbid ⊢ ( 𝜑 → ( 2 · 𝑁 ) ≤ ( e · 𝑁 ) )
139 44 120 124 128 138 letrd ⊢ ( 𝜑 → ( 𝑁 + 1 ) ≤ ( e · 𝑁 ) )
140 37 123 logled ⊢ ( 𝜑 → ( ( 𝑁 + 1 ) ≤ ( e · 𝑁 ) ↔ ( log ‘ ( 𝑁 + 1 ) ) ≤ ( log ‘ ( e · 𝑁 ) ) ) )
141 139 140 mpbid ⊢ ( 𝜑 → ( log ‘ ( 𝑁 + 1 ) ) ≤ ( log ‘ ( e · 𝑁 ) ) )
142 relogmul ⊢ ( ( e ∈ ℝ+ ∧ 𝑁 ∈ ℝ+ ) → ( log ‘ ( e · 𝑁 ) ) = ( ( log ‘ e ) + ( log ‘ 𝑁 ) ) )
143 121 8 142 sylancr ⊢ ( 𝜑 → ( log ‘ ( e · 𝑁 ) ) = ( ( log ‘ e ) + ( log ‘ 𝑁 ) ) )
144 loge ⊢ ( log ‘ e ) = 1
145 144 oveq1i ⊢ ( ( log ‘ e ) + ( log ‘ 𝑁 ) ) = ( 1 + ( log ‘ 𝑁 ) )
146 143 145 eqtrdi ⊢ ( 𝜑 → ( log ‘ ( e · 𝑁 ) ) = ( 1 + ( log ‘ 𝑁 ) ) )
147 141 146 breqtrd ⊢ ( 𝜑 → ( log ‘ ( 𝑁 + 1 ) ) ≤ ( 1 + ( log ‘ 𝑁 ) ) )
148 32 115 117 119 147 letrd ⊢ ( 𝜑 → ( Λ ‘ ( 𝑁 + 1 ) ) ≤ ( 1 + ( log ‘ 𝑁 ) ) )
149 32 64 15 absdifled ⊢ ( 𝜑 → ( ( abs ‘ ( ( Λ ‘ ( 𝑁 + 1 ) ) − 1 ) ) ≤ ( log ‘ 𝑁 ) ↔ ( ( 1 − ( log ‘ 𝑁 ) ) ≤ ( Λ ‘ ( 𝑁 + 1 ) ) ∧ ( Λ ‘ ( 𝑁 + 1 ) ) ≤ ( 1 + ( log ‘ 𝑁 ) ) ) ) )
150 114 148 149 mpbir2and ⊢ ( 𝜑 → ( abs ‘ ( ( Λ ‘ ( 𝑁 + 1 ) ) − 1 ) ) ≤ ( log ‘ 𝑁 ) )
151 29 36 15 63 150 letrd ⊢ ( 𝜑 → ( abs ‘ ( 𝑅 ‘ 𝑁 ) ) ≤ ( log ‘ 𝑁 ) )
152 29 15 8 151 lediv1dd ⊢ ( 𝜑 → ( ( abs ‘ ( 𝑅 ‘ 𝑁 ) ) / 𝑁 ) ≤ ( ( log ‘ 𝑁 ) / 𝑁 ) )
153 28 152 eqbrtrd ⊢ ( 𝜑 → ( abs ‘ ( ( 𝑅 ‘ 𝑁 ) / 𝑁 ) ) ≤ ( ( log ‘ 𝑁 ) / 𝑁 ) )
154 90 relogcld ⊢ ( 𝜑 → ( log ‘ 𝑋 ) ∈ ℝ )
155 154 90 rerpdivcld ⊢ ( 𝜑 → ( ( log ‘ 𝑋 ) / 𝑋 ) ∈ ℝ )
156 64 73 88 ltled ⊢ ( 𝜑 → 1 ≤ ( 2 / 𝐸 ) )
157 efle ⊢ ( ( 1 ∈ ℝ ∧ ( 2 / 𝐸 ) ∈ ℝ ) → ( 1 ≤ ( 2 / 𝐸 ) ↔ ( exp ‘ 1 ) ≤ ( exp ‘ ( 2 / 𝐸 ) ) ) )
158 108 73 157 sylancr ⊢ ( 𝜑 → ( 1 ≤ ( 2 / 𝐸 ) ↔ ( exp ‘ 1 ) ≤ ( exp ‘ ( 2 / 𝐸 ) ) ) )
159 156 158 mpbid ⊢ ( 𝜑 → ( exp ‘ 1 ) ≤ ( exp ‘ ( 2 / 𝐸 ) ) )
160 df-e ⊢ e = ( exp ‘ 1 )
161 159 160 3 3brtr4g ⊢ ( 𝜑 → e ≤ 𝑋 )
162 144 107 eqbrtrid ⊢ ( 𝜑 → ( log ‘ e ) ≤ ( log ‘ 𝑁 ) )
163 logleb ⊢ ( ( e ∈ ℝ+ ∧ 𝑁 ∈ ℝ+ ) → ( e ≤ 𝑁 ↔ ( log ‘ e ) ≤ ( log ‘ 𝑁 ) ) )
164 121 8 163 sylancr ⊢ ( 𝜑 → ( e ≤ 𝑁 ↔ ( log ‘ e ) ≤ ( log ‘ 𝑁 ) ) )
165 162 164 mpbird ⊢ ( 𝜑 → e ≤ 𝑁 )
166 logdivlt ⊢ ( ( ( 𝑋 ∈ ℝ ∧ e ≤ 𝑋 ) ∧ ( 𝑁 ∈ ℝ ∧ e ≤ 𝑁 ) ) → ( 𝑋 < 𝑁 ↔ ( ( log ‘ 𝑁 ) / 𝑁 ) < ( ( log ‘ 𝑋 ) / 𝑋 ) ) )
167 91 161 20 165 166 syl22anc ⊢ ( 𝜑 → ( 𝑋 < 𝑁 ↔ ( ( log ‘ 𝑁 ) / 𝑁 ) < ( ( log ‘ 𝑋 ) / 𝑋 ) ) )
168 99 167 mpbid ⊢ ( 𝜑 → ( ( log ‘ 𝑁 ) / 𝑁 ) < ( ( log ‘ 𝑋 ) / 𝑋 ) )
169 3 fveq2i ⊢ ( log ‘ 𝑋 ) = ( log ‘ ( exp ‘ ( 2 / 𝐸 ) ) )
170 73 relogefd ⊢ ( 𝜑 → ( log ‘ ( exp ‘ ( 2 / 𝐸 ) ) ) = ( 2 / 𝐸 ) )
171 169 170 eqtrid ⊢ ( 𝜑 → ( log ‘ 𝑋 ) = ( 2 / 𝐸 ) )
172 171 oveq1d ⊢ ( 𝜑 → ( ( log ‘ 𝑋 ) / 𝑋 ) = ( ( 2 / 𝐸 ) / 𝑋 ) )
173 2rp ⊢ 2 ∈ ℝ+
174 rpdivcl ⊢ ( ( 2 ∈ ℝ+ ∧ 𝐸 ∈ ℝ+ ) → ( 2 / 𝐸 ) ∈ ℝ+ )
175 173 71 174 sylancr ⊢ ( 𝜑 → ( 2 / 𝐸 ) ∈ ℝ+ )
176 175 rpcnd ⊢ ( 𝜑 → ( 2 / 𝐸 ) ∈ ℂ )
177 176 sqvald ⊢ ( 𝜑 → ( ( 2 / 𝐸 ) ↑ 2 ) = ( ( 2 / 𝐸 ) · ( 2 / 𝐸 ) ) )
178 2cnd ⊢ ( 𝜑 → 2 ∈ ℂ )
179 71 rpcnne0d ⊢ ( 𝜑 → ( 𝐸 ∈ ℂ ∧ 𝐸 ≠ 0 ) )
180 div12 ⊢ ( ( ( 2 / 𝐸 ) ∈ ℂ ∧ 2 ∈ ℂ ∧ ( 𝐸 ∈ ℂ ∧ 𝐸 ≠ 0 ) ) → ( ( 2 / 𝐸 ) · ( 2 / 𝐸 ) ) = ( 2 · ( ( 2 / 𝐸 ) / 𝐸 ) ) )
181 176 178 179 180 syl3anc ⊢ ( 𝜑 → ( ( 2 / 𝐸 ) · ( 2 / 𝐸 ) ) = ( 2 · ( ( 2 / 𝐸 ) / 𝐸 ) ) )
182 177 181 eqtrd ⊢ ( 𝜑 → ( ( 2 / 𝐸 ) ↑ 2 ) = ( 2 · ( ( 2 / 𝐸 ) / 𝐸 ) ) )
183 182 oveq1d ⊢ ( 𝜑 → ( ( ( 2 / 𝐸 ) ↑ 2 ) / 2 ) = ( ( 2 · ( ( 2 / 𝐸 ) / 𝐸 ) ) / 2 ) )
184 175 71 rpdivcld ⊢ ( 𝜑 → ( ( 2 / 𝐸 ) / 𝐸 ) ∈ ℝ+ )
185 184 rpcnd ⊢ ( 𝜑 → ( ( 2 / 𝐸 ) / 𝐸 ) ∈ ℂ )
186 2ne0 ⊢ 2 ≠ 0
187 186 a1i ⊢ ( 𝜑 → 2 ≠ 0 )
188 185 178 187 divcan3d ⊢ ( 𝜑 → ( ( 2 · ( ( 2 / 𝐸 ) / 𝐸 ) ) / 2 ) = ( ( 2 / 𝐸 ) / 𝐸 ) )
189 183 188 eqtrd ⊢ ( 𝜑 → ( ( ( 2 / 𝐸 ) ↑ 2 ) / 2 ) = ( ( 2 / 𝐸 ) / 𝐸 ) )
190 73 resqcld ⊢ ( 𝜑 → ( ( 2 / 𝐸 ) ↑ 2 ) ∈ ℝ )
191 190 rehalfcld ⊢ ( 𝜑 → ( ( ( 2 / 𝐸 ) ↑ 2 ) / 2 ) ∈ ℝ )
192 1rp ⊢ 1 ∈ ℝ+
193 rpaddcl ⊢ ( ( 1 ∈ ℝ+ ∧ ( 2 / 𝐸 ) ∈ ℝ+ ) → ( 1 + ( 2 / 𝐸 ) ) ∈ ℝ+ )
194 192 175 193 sylancr ⊢ ( 𝜑 → ( 1 + ( 2 / 𝐸 ) ) ∈ ℝ+ )
195 194 rpred ⊢ ( 𝜑 → ( 1 + ( 2 / 𝐸 ) ) ∈ ℝ )
196 195 191 readdcld ⊢ ( 𝜑 → ( ( 1 + ( 2 / 𝐸 ) ) + ( ( ( 2 / 𝐸 ) ↑ 2 ) / 2 ) ) ∈ ℝ )
197 191 194 ltaddrp2d ⊢ ( 𝜑 → ( ( ( 2 / 𝐸 ) ↑ 2 ) / 2 ) < ( ( 1 + ( 2 / 𝐸 ) ) + ( ( ( 2 / 𝐸 ) ↑ 2 ) / 2 ) ) )
198 efgt1p2 ⊢ ( ( 2 / 𝐸 ) ∈ ℝ+ → ( ( 1 + ( 2 / 𝐸 ) ) + ( ( ( 2 / 𝐸 ) ↑ 2 ) / 2 ) ) < ( exp ‘ ( 2 / 𝐸 ) ) )
199 175 198 syl ⊢ ( 𝜑 → ( ( 1 + ( 2 / 𝐸 ) ) + ( ( ( 2 / 𝐸 ) ↑ 2 ) / 2 ) ) < ( exp ‘ ( 2 / 𝐸 ) ) )
200 199 3 breqtrrdi ⊢ ( 𝜑 → ( ( 1 + ( 2 / 𝐸 ) ) + ( ( ( 2 / 𝐸 ) ↑ 2 ) / 2 ) ) < 𝑋 )
201 191 196 91 197 200 lttrd ⊢ ( 𝜑 → ( ( ( 2 / 𝐸 ) ↑ 2 ) / 2 ) < 𝑋 )
202 189 201 eqbrtrrd ⊢ ( 𝜑 → ( ( 2 / 𝐸 ) / 𝐸 ) < 𝑋 )
203 73 71 90 202 ltdiv23d ⊢ ( 𝜑 → ( ( 2 / 𝐸 ) / 𝑋 ) < 𝐸 )
204 172 203 eqbrtrd ⊢ ( 𝜑 → ( ( log ‘ 𝑋 ) / 𝑋 ) < 𝐸 )
205 16 155 18 168 204 lttrd ⊢ ( 𝜑 → ( ( log ‘ 𝑁 ) / 𝑁 ) < 𝐸 )
206 16 18 205 ltled ⊢ ( 𝜑 → ( ( log ‘ 𝑁 ) / 𝑁 ) ≤ 𝐸 )
207 14 16 18 153 206 letrd ⊢ ( 𝜑 → ( abs ‘ ( ( 𝑅 ‘ 𝑁 ) / 𝑁 ) ) ≤ 𝐸 )