Proof of Theorem pntpbnd1a
Step | Hyp | Ref
| Expression |
1 | | pntpbnd1a.1 |
. . . . . . 7
⊢ (𝜑 → 𝑁 ∈ ℕ) |
2 | 1 | nnrpd 11746 |
. . . . . 6
⊢ (𝜑 → 𝑁 ∈
ℝ+) |
3 | | pntpbnd.r |
. . . . . . . 8
⊢ 𝑅 = (𝑎 ∈ ℝ+ ↦
((ψ‘𝑎) −
𝑎)) |
4 | 3 | pntrf 25052 |
. . . . . . 7
⊢ 𝑅:ℝ+⟶ℝ |
5 | 4 | ffvelrni 6266 |
. . . . . 6
⊢ (𝑁 ∈ ℝ+
→ (𝑅‘𝑁) ∈
ℝ) |
6 | 2, 5 | syl 17 |
. . . . 5
⊢ (𝜑 → (𝑅‘𝑁) ∈ ℝ) |
7 | 6, 2 | rerpdivcld 11779 |
. . . 4
⊢ (𝜑 → ((𝑅‘𝑁) / 𝑁) ∈ ℝ) |
8 | 7 | recnd 9947 |
. . 3
⊢ (𝜑 → ((𝑅‘𝑁) / 𝑁) ∈ ℂ) |
9 | 8 | abscld 14023 |
. 2
⊢ (𝜑 → (abs‘((𝑅‘𝑁) / 𝑁)) ∈ ℝ) |
10 | 2 | relogcld 24173 |
. . 3
⊢ (𝜑 → (log‘𝑁) ∈
ℝ) |
11 | 10, 2 | rerpdivcld 11779 |
. 2
⊢ (𝜑 → ((log‘𝑁) / 𝑁) ∈ ℝ) |
12 | | ioossre 12106 |
. . 3
⊢ (0(,)1)
⊆ ℝ |
13 | | pntpbnd1.e |
. . 3
⊢ (𝜑 → 𝐸 ∈ (0(,)1)) |
14 | 12, 13 | sseldi 3566 |
. 2
⊢ (𝜑 → 𝐸 ∈ ℝ) |
15 | 6 | recnd 9947 |
. . . . 5
⊢ (𝜑 → (𝑅‘𝑁) ∈ ℂ) |
16 | 1 | nnred 10912 |
. . . . . 6
⊢ (𝜑 → 𝑁 ∈ ℝ) |
17 | 16 | recnd 9947 |
. . . . 5
⊢ (𝜑 → 𝑁 ∈ ℂ) |
18 | 1 | nnne0d 10942 |
. . . . 5
⊢ (𝜑 → 𝑁 ≠ 0) |
19 | 15, 17, 18 | absdivd 14042 |
. . . 4
⊢ (𝜑 → (abs‘((𝑅‘𝑁) / 𝑁)) = ((abs‘(𝑅‘𝑁)) / (abs‘𝑁))) |
20 | 1 | nnnn0d 11228 |
. . . . . . 7
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
21 | 20 | nn0ge0d 11231 |
. . . . . 6
⊢ (𝜑 → 0 ≤ 𝑁) |
22 | 16, 21 | absidd 14009 |
. . . . 5
⊢ (𝜑 → (abs‘𝑁) = 𝑁) |
23 | 22 | oveq2d 6565 |
. . . 4
⊢ (𝜑 → ((abs‘(𝑅‘𝑁)) / (abs‘𝑁)) = ((abs‘(𝑅‘𝑁)) / 𝑁)) |
24 | 19, 23 | eqtrd 2644 |
. . 3
⊢ (𝜑 → (abs‘((𝑅‘𝑁) / 𝑁)) = ((abs‘(𝑅‘𝑁)) / 𝑁)) |
25 | 15 | abscld 14023 |
. . . 4
⊢ (𝜑 → (abs‘(𝑅‘𝑁)) ∈ ℝ) |
26 | 1 | peano2nnd 10914 |
. . . . . . . . 9
⊢ (𝜑 → (𝑁 + 1) ∈ ℕ) |
27 | | vmacl 24644 |
. . . . . . . . 9
⊢ ((𝑁 + 1) ∈ ℕ →
(Λ‘(𝑁 + 1))
∈ ℝ) |
28 | 26, 27 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (Λ‘(𝑁 + 1)) ∈
ℝ) |
29 | | peano2rem 10227 |
. . . . . . . 8
⊢
((Λ‘(𝑁
+ 1)) ∈ ℝ → ((Λ‘(𝑁 + 1)) − 1) ∈
ℝ) |
30 | 28, 29 | syl 17 |
. . . . . . 7
⊢ (𝜑 → ((Λ‘(𝑁 + 1)) − 1) ∈
ℝ) |
31 | 30 | recnd 9947 |
. . . . . 6
⊢ (𝜑 → ((Λ‘(𝑁 + 1)) − 1) ∈
ℂ) |
32 | 31 | abscld 14023 |
. . . . 5
⊢ (𝜑 →
(abs‘((Λ‘(𝑁 + 1)) − 1)) ∈
ℝ) |
33 | | pntpbnd1a.3 |
. . . . . 6
⊢ (𝜑 → (abs‘(𝑅‘𝑁)) ≤ (abs‘((𝑅‘(𝑁 + 1)) − (𝑅‘𝑁)))) |
34 | 26 | nnrpd 11746 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑁 + 1) ∈
ℝ+) |
35 | 3 | pntrval 25051 |
. . . . . . . . . 10
⊢ ((𝑁 + 1) ∈ ℝ+
→ (𝑅‘(𝑁 + 1)) = ((ψ‘(𝑁 + 1)) − (𝑁 + 1))) |
36 | 34, 35 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (𝑅‘(𝑁 + 1)) = ((ψ‘(𝑁 + 1)) − (𝑁 + 1))) |
37 | 3 | pntrval 25051 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℝ+
→ (𝑅‘𝑁) = ((ψ‘𝑁) − 𝑁)) |
38 | 2, 37 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (𝑅‘𝑁) = ((ψ‘𝑁) − 𝑁)) |
39 | 36, 38 | oveq12d 6567 |
. . . . . . . 8
⊢ (𝜑 → ((𝑅‘(𝑁 + 1)) − (𝑅‘𝑁)) = (((ψ‘(𝑁 + 1)) − (𝑁 + 1)) − ((ψ‘𝑁) − 𝑁))) |
40 | | peano2re 10088 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℝ → (𝑁 + 1) ∈
ℝ) |
41 | 16, 40 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑁 + 1) ∈ ℝ) |
42 | | chpcl 24650 |
. . . . . . . . . . 11
⊢ ((𝑁 + 1) ∈ ℝ →
(ψ‘(𝑁 + 1))
∈ ℝ) |
43 | 41, 42 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (ψ‘(𝑁 + 1)) ∈
ℝ) |
44 | 43 | recnd 9947 |
. . . . . . . . 9
⊢ (𝜑 → (ψ‘(𝑁 + 1)) ∈
ℂ) |
45 | 41 | recnd 9947 |
. . . . . . . . 9
⊢ (𝜑 → (𝑁 + 1) ∈ ℂ) |
46 | | chpcl 24650 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℝ →
(ψ‘𝑁) ∈
ℝ) |
47 | 16, 46 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (ψ‘𝑁) ∈
ℝ) |
48 | 47 | recnd 9947 |
. . . . . . . . 9
⊢ (𝜑 → (ψ‘𝑁) ∈
ℂ) |
49 | 44, 45, 48, 17 | sub4d 10320 |
. . . . . . . 8
⊢ (𝜑 → (((ψ‘(𝑁 + 1)) − (𝑁 + 1)) −
((ψ‘𝑁) −
𝑁)) = (((ψ‘(𝑁 + 1)) −
(ψ‘𝑁)) −
((𝑁 + 1) − 𝑁))) |
50 | | chpp1 24681 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ0
→ (ψ‘(𝑁 +
1)) = ((ψ‘𝑁) +
(Λ‘(𝑁 +
1)))) |
51 | 20, 50 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (ψ‘(𝑁 + 1)) = ((ψ‘𝑁) + (Λ‘(𝑁 + 1)))) |
52 | 51 | oveq1d 6564 |
. . . . . . . . . 10
⊢ (𝜑 → ((ψ‘(𝑁 + 1)) −
(ψ‘𝑁)) =
(((ψ‘𝑁) +
(Λ‘(𝑁 + 1)))
− (ψ‘𝑁))) |
53 | 28 | recnd 9947 |
. . . . . . . . . . 11
⊢ (𝜑 → (Λ‘(𝑁 + 1)) ∈
ℂ) |
54 | 48, 53 | pncan2d 10273 |
. . . . . . . . . 10
⊢ (𝜑 → (((ψ‘𝑁) + (Λ‘(𝑁 + 1))) −
(ψ‘𝑁)) =
(Λ‘(𝑁 +
1))) |
55 | 52, 54 | eqtrd 2644 |
. . . . . . . . 9
⊢ (𝜑 → ((ψ‘(𝑁 + 1)) −
(ψ‘𝑁)) =
(Λ‘(𝑁 +
1))) |
56 | | ax-1cn 9873 |
. . . . . . . . . 10
⊢ 1 ∈
ℂ |
57 | | pncan2 10167 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑁 + 1)
− 𝑁) =
1) |
58 | 17, 56, 57 | sylancl 693 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑁 + 1) − 𝑁) = 1) |
59 | 55, 58 | oveq12d 6567 |
. . . . . . . 8
⊢ (𝜑 → (((ψ‘(𝑁 + 1)) −
(ψ‘𝑁)) −
((𝑁 + 1) − 𝑁)) = ((Λ‘(𝑁 + 1)) −
1)) |
60 | 39, 49, 59 | 3eqtrd 2648 |
. . . . . . 7
⊢ (𝜑 → ((𝑅‘(𝑁 + 1)) − (𝑅‘𝑁)) = ((Λ‘(𝑁 + 1)) − 1)) |
61 | 60 | fveq2d 6107 |
. . . . . 6
⊢ (𝜑 → (abs‘((𝑅‘(𝑁 + 1)) − (𝑅‘𝑁))) = (abs‘((Λ‘(𝑁 + 1)) −
1))) |
62 | 33, 61 | breqtrd 4609 |
. . . . 5
⊢ (𝜑 → (abs‘(𝑅‘𝑁)) ≤ (abs‘((Λ‘(𝑁 + 1)) −
1))) |
63 | | 1red 9934 |
. . . . . . . 8
⊢ (𝜑 → 1 ∈
ℝ) |
64 | 63, 10 | resubcld 10337 |
. . . . . . 7
⊢ (𝜑 → (1 −
(log‘𝑁)) ∈
ℝ) |
65 | | 0red 9920 |
. . . . . . 7
⊢ (𝜑 → 0 ∈
ℝ) |
66 | | 2re 10967 |
. . . . . . . . . . 11
⊢ 2 ∈
ℝ |
67 | | eliooord 12104 |
. . . . . . . . . . . . . 14
⊢ (𝐸 ∈ (0(,)1) → (0 <
𝐸 ∧ 𝐸 < 1)) |
68 | 13, 67 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (0 < 𝐸 ∧ 𝐸 < 1)) |
69 | 68 | simpld 474 |
. . . . . . . . . . . 12
⊢ (𝜑 → 0 < 𝐸) |
70 | 14, 69 | elrpd 11745 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐸 ∈
ℝ+) |
71 | | rerpdivcl 11737 |
. . . . . . . . . . 11
⊢ ((2
∈ ℝ ∧ 𝐸
∈ ℝ+) → (2 / 𝐸) ∈ ℝ) |
72 | 66, 70, 71 | sylancr 694 |
. . . . . . . . . 10
⊢ (𝜑 → (2 / 𝐸) ∈ ℝ) |
73 | 66 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → 2 ∈
ℝ) |
74 | | 1lt2 11071 |
. . . . . . . . . . . 12
⊢ 1 <
2 |
75 | 74 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → 1 < 2) |
76 | | 2cn 10968 |
. . . . . . . . . . . . 13
⊢ 2 ∈
ℂ |
77 | 76 | div1i 10632 |
. . . . . . . . . . . 12
⊢ (2 / 1) =
2 |
78 | 68 | simprd 478 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐸 < 1) |
79 | | 0lt1 10429 |
. . . . . . . . . . . . . . 15
⊢ 0 <
1 |
80 | 79 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 0 < 1) |
81 | | 2pos 10989 |
. . . . . . . . . . . . . . 15
⊢ 0 <
2 |
82 | 81 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 0 < 2) |
83 | | ltdiv2 10788 |
. . . . . . . . . . . . . 14
⊢ (((𝐸 ∈ ℝ ∧ 0 <
𝐸) ∧ (1 ∈ ℝ
∧ 0 < 1) ∧ (2 ∈ ℝ ∧ 0 < 2)) → (𝐸 < 1 ↔ (2 / 1) < (2 /
𝐸))) |
84 | 14, 69, 63, 80, 73, 82, 83 | syl222anc 1334 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐸 < 1 ↔ (2 / 1) < (2 / 𝐸))) |
85 | 78, 84 | mpbid 221 |
. . . . . . . . . . . 12
⊢ (𝜑 → (2 / 1) < (2 / 𝐸)) |
86 | 77, 85 | syl5eqbrr 4619 |
. . . . . . . . . . 11
⊢ (𝜑 → 2 < (2 / 𝐸)) |
87 | 63, 73, 72, 75, 86 | lttrd 10077 |
. . . . . . . . . 10
⊢ (𝜑 → 1 < (2 / 𝐸)) |
88 | | pntpbnd1.x |
. . . . . . . . . . . . 13
⊢ 𝑋 = (exp‘(2 / 𝐸)) |
89 | 72 | rpefcld 14674 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (exp‘(2 / 𝐸)) ∈
ℝ+) |
90 | 88, 89 | syl5eqel 2692 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑋 ∈
ℝ+) |
91 | 90 | rpred 11748 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑋 ∈ ℝ) |
92 | | pntpbnd1.y |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑌 ∈ (𝑋(,)+∞)) |
93 | 90 | rpxrd 11749 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑋 ∈
ℝ*) |
94 | | elioopnf 12138 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑋 ∈ ℝ*
→ (𝑌 ∈ (𝑋(,)+∞) ↔ (𝑌 ∈ ℝ ∧ 𝑋 < 𝑌))) |
95 | 93, 94 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑌 ∈ (𝑋(,)+∞) ↔ (𝑌 ∈ ℝ ∧ 𝑋 < 𝑌))) |
96 | 92, 95 | mpbid 221 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑌 ∈ ℝ ∧ 𝑋 < 𝑌)) |
97 | 96 | simpld 474 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑌 ∈ ℝ) |
98 | 96 | simprd 478 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑋 < 𝑌) |
99 | | pntpbnd1a.2 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑌 < 𝑁 ∧ 𝑁 ≤ (𝐾 · 𝑌))) |
100 | 99 | simpld 474 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑌 < 𝑁) |
101 | 91, 97, 16, 98, 100 | lttrd 10077 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑋 < 𝑁) |
102 | 88, 101 | syl5eqbrr 4619 |
. . . . . . . . . . . 12
⊢ (𝜑 → (exp‘(2 / 𝐸)) < 𝑁) |
103 | 2 | reeflogd 24174 |
. . . . . . . . . . . 12
⊢ (𝜑 →
(exp‘(log‘𝑁)) =
𝑁) |
104 | 102, 103 | breqtrrd 4611 |
. . . . . . . . . . 11
⊢ (𝜑 → (exp‘(2 / 𝐸)) <
(exp‘(log‘𝑁))) |
105 | | eflt 14686 |
. . . . . . . . . . . 12
⊢ (((2 /
𝐸) ∈ ℝ ∧
(log‘𝑁) ∈
ℝ) → ((2 / 𝐸)
< (log‘𝑁) ↔
(exp‘(2 / 𝐸)) <
(exp‘(log‘𝑁)))) |
106 | 72, 10, 105 | syl2anc 691 |
. . . . . . . . . . 11
⊢ (𝜑 → ((2 / 𝐸) < (log‘𝑁) ↔ (exp‘(2 / 𝐸)) < (exp‘(log‘𝑁)))) |
107 | 104, 106 | mpbird 246 |
. . . . . . . . . 10
⊢ (𝜑 → (2 / 𝐸) < (log‘𝑁)) |
108 | 63, 72, 10, 87, 107 | lttrd 10077 |
. . . . . . . . 9
⊢ (𝜑 → 1 < (log‘𝑁)) |
109 | 63, 10, 108 | ltled 10064 |
. . . . . . . 8
⊢ (𝜑 → 1 ≤ (log‘𝑁)) |
110 | | 1re 9918 |
. . . . . . . . 9
⊢ 1 ∈
ℝ |
111 | | suble0 10421 |
. . . . . . . . 9
⊢ ((1
∈ ℝ ∧ (log‘𝑁) ∈ ℝ) → ((1 −
(log‘𝑁)) ≤ 0
↔ 1 ≤ (log‘𝑁))) |
112 | 110, 10, 111 | sylancr 694 |
. . . . . . . 8
⊢ (𝜑 → ((1 −
(log‘𝑁)) ≤ 0
↔ 1 ≤ (log‘𝑁))) |
113 | 109, 112 | mpbird 246 |
. . . . . . 7
⊢ (𝜑 → (1 −
(log‘𝑁)) ≤
0) |
114 | | vmage0 24647 |
. . . . . . . 8
⊢ ((𝑁 + 1) ∈ ℕ → 0
≤ (Λ‘(𝑁 +
1))) |
115 | 26, 114 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 0 ≤
(Λ‘(𝑁 +
1))) |
116 | 64, 65, 28, 113, 115 | letrd 10073 |
. . . . . 6
⊢ (𝜑 → (1 −
(log‘𝑁)) ≤
(Λ‘(𝑁 +
1))) |
117 | 34 | relogcld 24173 |
. . . . . . 7
⊢ (𝜑 → (log‘(𝑁 + 1)) ∈
ℝ) |
118 | | readdcl 9898 |
. . . . . . . 8
⊢ ((1
∈ ℝ ∧ (log‘𝑁) ∈ ℝ) → (1 +
(log‘𝑁)) ∈
ℝ) |
119 | 110, 10, 118 | sylancr 694 |
. . . . . . 7
⊢ (𝜑 → (1 + (log‘𝑁)) ∈
ℝ) |
120 | | vmalelog 24730 |
. . . . . . . 8
⊢ ((𝑁 + 1) ∈ ℕ →
(Λ‘(𝑁 + 1))
≤ (log‘(𝑁 +
1))) |
121 | 26, 120 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (Λ‘(𝑁 + 1)) ≤ (log‘(𝑁 + 1))) |
122 | 73, 16 | remulcld 9949 |
. . . . . . . . . 10
⊢ (𝜑 → (2 · 𝑁) ∈
ℝ) |
123 | | epr 14775 |
. . . . . . . . . . . 12
⊢ e ∈
ℝ+ |
124 | | rpmulcl 11731 |
. . . . . . . . . . . 12
⊢ ((e
∈ ℝ+ ∧ 𝑁 ∈ ℝ+) → (e
· 𝑁) ∈
ℝ+) |
125 | 123, 2, 124 | sylancr 694 |
. . . . . . . . . . 11
⊢ (𝜑 → (e · 𝑁) ∈
ℝ+) |
126 | 125 | rpred 11748 |
. . . . . . . . . 10
⊢ (𝜑 → (e · 𝑁) ∈
ℝ) |
127 | 1 | nnge1d 10940 |
. . . . . . . . . . . 12
⊢ (𝜑 → 1 ≤ 𝑁) |
128 | 63, 16, 16, 127 | leadd2dd 10521 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑁 + 1) ≤ (𝑁 + 𝑁)) |
129 | 17 | 2timesd 11152 |
. . . . . . . . . . 11
⊢ (𝜑 → (2 · 𝑁) = (𝑁 + 𝑁)) |
130 | 128, 129 | breqtrrd 4611 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑁 + 1) ≤ (2 · 𝑁)) |
131 | | ere 14658 |
. . . . . . . . . . . . 13
⊢ e ∈
ℝ |
132 | | egt2lt3 14773 |
. . . . . . . . . . . . . 14
⊢ (2 < e
∧ e < 3) |
133 | 132 | simpli 473 |
. . . . . . . . . . . . 13
⊢ 2 <
e |
134 | 66, 131, 133 | ltleii 10039 |
. . . . . . . . . . . 12
⊢ 2 ≤
e |
135 | 134 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → 2 ≤ e) |
136 | 131 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → e ∈
ℝ) |
137 | 1 | nngt0d 10941 |
. . . . . . . . . . . 12
⊢ (𝜑 → 0 < 𝑁) |
138 | | lemul1 10754 |
. . . . . . . . . . . 12
⊢ ((2
∈ ℝ ∧ e ∈ ℝ ∧ (𝑁 ∈ ℝ ∧ 0 < 𝑁)) → (2 ≤ e ↔ (2
· 𝑁) ≤ (e
· 𝑁))) |
139 | 73, 136, 16, 137, 138 | syl112anc 1322 |
. . . . . . . . . . 11
⊢ (𝜑 → (2 ≤ e ↔ (2
· 𝑁) ≤ (e
· 𝑁))) |
140 | 135, 139 | mpbid 221 |
. . . . . . . . . 10
⊢ (𝜑 → (2 · 𝑁) ≤ (e · 𝑁)) |
141 | 41, 122, 126, 130, 140 | letrd 10073 |
. . . . . . . . 9
⊢ (𝜑 → (𝑁 + 1) ≤ (e · 𝑁)) |
142 | 34, 125 | logled 24177 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑁 + 1) ≤ (e · 𝑁) ↔ (log‘(𝑁 + 1)) ≤ (log‘(e · 𝑁)))) |
143 | 141, 142 | mpbid 221 |
. . . . . . . 8
⊢ (𝜑 → (log‘(𝑁 + 1)) ≤ (log‘(e
· 𝑁))) |
144 | | relogmul 24142 |
. . . . . . . . . 10
⊢ ((e
∈ ℝ+ ∧ 𝑁 ∈ ℝ+) →
(log‘(e · 𝑁))
= ((log‘e) + (log‘𝑁))) |
145 | 123, 2, 144 | sylancr 694 |
. . . . . . . . 9
⊢ (𝜑 → (log‘(e ·
𝑁)) = ((log‘e) +
(log‘𝑁))) |
146 | | loge 24137 |
. . . . . . . . . 10
⊢
(log‘e) = 1 |
147 | 146 | oveq1i 6559 |
. . . . . . . . 9
⊢
((log‘e) + (log‘𝑁)) = (1 + (log‘𝑁)) |
148 | 145, 147 | syl6eq 2660 |
. . . . . . . 8
⊢ (𝜑 → (log‘(e ·
𝑁)) = (1 + (log‘𝑁))) |
149 | 143, 148 | breqtrd 4609 |
. . . . . . 7
⊢ (𝜑 → (log‘(𝑁 + 1)) ≤ (1 +
(log‘𝑁))) |
150 | 28, 117, 119, 121, 149 | letrd 10073 |
. . . . . 6
⊢ (𝜑 → (Λ‘(𝑁 + 1)) ≤ (1 +
(log‘𝑁))) |
151 | 28, 63, 10 | absdifled 14021 |
. . . . . 6
⊢ (𝜑 →
((abs‘((Λ‘(𝑁 + 1)) − 1)) ≤ (log‘𝑁) ↔ ((1 −
(log‘𝑁)) ≤
(Λ‘(𝑁 + 1))
∧ (Λ‘(𝑁 +
1)) ≤ (1 + (log‘𝑁))))) |
152 | 116, 150,
151 | mpbir2and 959 |
. . . . 5
⊢ (𝜑 →
(abs‘((Λ‘(𝑁 + 1)) − 1)) ≤ (log‘𝑁)) |
153 | 25, 32, 10, 62, 152 | letrd 10073 |
. . . 4
⊢ (𝜑 → (abs‘(𝑅‘𝑁)) ≤ (log‘𝑁)) |
154 | 25, 10, 2, 153 | lediv1dd 11806 |
. . 3
⊢ (𝜑 → ((abs‘(𝑅‘𝑁)) / 𝑁) ≤ ((log‘𝑁) / 𝑁)) |
155 | 24, 154 | eqbrtrd 4605 |
. 2
⊢ (𝜑 → (abs‘((𝑅‘𝑁) / 𝑁)) ≤ ((log‘𝑁) / 𝑁)) |
156 | 90 | relogcld 24173 |
. . . . 5
⊢ (𝜑 → (log‘𝑋) ∈
ℝ) |
157 | 156, 90 | rerpdivcld 11779 |
. . . 4
⊢ (𝜑 → ((log‘𝑋) / 𝑋) ∈ ℝ) |
158 | 63, 72, 87 | ltled 10064 |
. . . . . . . 8
⊢ (𝜑 → 1 ≤ (2 / 𝐸)) |
159 | | efle 14687 |
. . . . . . . . 9
⊢ ((1
∈ ℝ ∧ (2 / 𝐸) ∈ ℝ) → (1 ≤ (2 / 𝐸) ↔ (exp‘1) ≤
(exp‘(2 / 𝐸)))) |
160 | 110, 72, 159 | sylancr 694 |
. . . . . . . 8
⊢ (𝜑 → (1 ≤ (2 / 𝐸) ↔ (exp‘1) ≤
(exp‘(2 / 𝐸)))) |
161 | 158, 160 | mpbid 221 |
. . . . . . 7
⊢ (𝜑 → (exp‘1) ≤
(exp‘(2 / 𝐸))) |
162 | | df-e 14638 |
. . . . . . 7
⊢ e =
(exp‘1) |
163 | 161, 162,
88 | 3brtr4g 4617 |
. . . . . 6
⊢ (𝜑 → e ≤ 𝑋) |
164 | 146, 109 | syl5eqbr 4618 |
. . . . . . 7
⊢ (𝜑 → (log‘e) ≤
(log‘𝑁)) |
165 | | logleb 24153 |
. . . . . . . 8
⊢ ((e
∈ ℝ+ ∧ 𝑁 ∈ ℝ+) → (e ≤
𝑁 ↔ (log‘e) ≤
(log‘𝑁))) |
166 | 123, 2, 165 | sylancr 694 |
. . . . . . 7
⊢ (𝜑 → (e ≤ 𝑁 ↔ (log‘e) ≤ (log‘𝑁))) |
167 | 164, 166 | mpbird 246 |
. . . . . 6
⊢ (𝜑 → e ≤ 𝑁) |
168 | | logdivlt 24171 |
. . . . . 6
⊢ (((𝑋 ∈ ℝ ∧ e ≤
𝑋) ∧ (𝑁 ∈ ℝ ∧ e ≤ 𝑁)) → (𝑋 < 𝑁 ↔ ((log‘𝑁) / 𝑁) < ((log‘𝑋) / 𝑋))) |
169 | 91, 163, 16, 167, 168 | syl22anc 1319 |
. . . . 5
⊢ (𝜑 → (𝑋 < 𝑁 ↔ ((log‘𝑁) / 𝑁) < ((log‘𝑋) / 𝑋))) |
170 | 101, 169 | mpbid 221 |
. . . 4
⊢ (𝜑 → ((log‘𝑁) / 𝑁) < ((log‘𝑋) / 𝑋)) |
171 | 88 | fveq2i 6106 |
. . . . . . 7
⊢
(log‘𝑋) =
(log‘(exp‘(2 / 𝐸))) |
172 | 72 | relogefd 24178 |
. . . . . . 7
⊢ (𝜑 → (log‘(exp‘(2 /
𝐸))) = (2 / 𝐸)) |
173 | 171, 172 | syl5eq 2656 |
. . . . . 6
⊢ (𝜑 → (log‘𝑋) = (2 / 𝐸)) |
174 | 173 | oveq1d 6564 |
. . . . 5
⊢ (𝜑 → ((log‘𝑋) / 𝑋) = ((2 / 𝐸) / 𝑋)) |
175 | | 2rp 11713 |
. . . . . . . . . . . . 13
⊢ 2 ∈
ℝ+ |
176 | | rpdivcl 11732 |
. . . . . . . . . . . . 13
⊢ ((2
∈ ℝ+ ∧ 𝐸 ∈ ℝ+) → (2 /
𝐸) ∈
ℝ+) |
177 | 175, 70, 176 | sylancr 694 |
. . . . . . . . . . . 12
⊢ (𝜑 → (2 / 𝐸) ∈
ℝ+) |
178 | 177 | rpcnd 11750 |
. . . . . . . . . . 11
⊢ (𝜑 → (2 / 𝐸) ∈ ℂ) |
179 | 178 | sqvald 12867 |
. . . . . . . . . 10
⊢ (𝜑 → ((2 / 𝐸)↑2) = ((2 / 𝐸) · (2 / 𝐸))) |
180 | | 2cnd 10970 |
. . . . . . . . . . 11
⊢ (𝜑 → 2 ∈
ℂ) |
181 | 70 | rpcnne0d 11757 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐸 ∈ ℂ ∧ 𝐸 ≠ 0)) |
182 | | div12 10586 |
. . . . . . . . . . 11
⊢ (((2 /
𝐸) ∈ ℂ ∧ 2
∈ ℂ ∧ (𝐸
∈ ℂ ∧ 𝐸 ≠
0)) → ((2 / 𝐸)
· (2 / 𝐸)) = (2
· ((2 / 𝐸) / 𝐸))) |
183 | 178, 180,
181, 182 | syl3anc 1318 |
. . . . . . . . . 10
⊢ (𝜑 → ((2 / 𝐸) · (2 / 𝐸)) = (2 · ((2 / 𝐸) / 𝐸))) |
184 | 179, 183 | eqtrd 2644 |
. . . . . . . . 9
⊢ (𝜑 → ((2 / 𝐸)↑2) = (2 · ((2 / 𝐸) / 𝐸))) |
185 | 184 | oveq1d 6564 |
. . . . . . . 8
⊢ (𝜑 → (((2 / 𝐸)↑2) / 2) = ((2 · ((2 / 𝐸) / 𝐸)) / 2)) |
186 | 177, 70 | rpdivcld 11765 |
. . . . . . . . . 10
⊢ (𝜑 → ((2 / 𝐸) / 𝐸) ∈
ℝ+) |
187 | 186 | rpcnd 11750 |
. . . . . . . . 9
⊢ (𝜑 → ((2 / 𝐸) / 𝐸) ∈ ℂ) |
188 | | 2ne0 10990 |
. . . . . . . . . 10
⊢ 2 ≠
0 |
189 | 188 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → 2 ≠ 0) |
190 | 187, 180,
189 | divcan3d 10685 |
. . . . . . . 8
⊢ (𝜑 → ((2 · ((2 / 𝐸) / 𝐸)) / 2) = ((2 / 𝐸) / 𝐸)) |
191 | 185, 190 | eqtrd 2644 |
. . . . . . 7
⊢ (𝜑 → (((2 / 𝐸)↑2) / 2) = ((2 / 𝐸) / 𝐸)) |
192 | 72 | resqcld 12897 |
. . . . . . . . 9
⊢ (𝜑 → ((2 / 𝐸)↑2) ∈ ℝ) |
193 | 192 | rehalfcld 11156 |
. . . . . . . 8
⊢ (𝜑 → (((2 / 𝐸)↑2) / 2) ∈
ℝ) |
194 | | 1rp 11712 |
. . . . . . . . . . 11
⊢ 1 ∈
ℝ+ |
195 | | rpaddcl 11730 |
. . . . . . . . . . 11
⊢ ((1
∈ ℝ+ ∧ (2 / 𝐸) ∈ ℝ+) → (1 + (2
/ 𝐸)) ∈
ℝ+) |
196 | 194, 177,
195 | sylancr 694 |
. . . . . . . . . 10
⊢ (𝜑 → (1 + (2 / 𝐸)) ∈
ℝ+) |
197 | 196 | rpred 11748 |
. . . . . . . . 9
⊢ (𝜑 → (1 + (2 / 𝐸)) ∈
ℝ) |
198 | 197, 193 | readdcld 9948 |
. . . . . . . 8
⊢ (𝜑 → ((1 + (2 / 𝐸)) + (((2 / 𝐸)↑2) / 2)) ∈
ℝ) |
199 | 193, 196 | ltaddrp2d 11782 |
. . . . . . . 8
⊢ (𝜑 → (((2 / 𝐸)↑2) / 2) < ((1 + (2 / 𝐸)) + (((2 / 𝐸)↑2) / 2))) |
200 | | efgt1p2 14683 |
. . . . . . . . . 10
⊢ ((2 /
𝐸) ∈
ℝ+ → ((1 + (2 / 𝐸)) + (((2 / 𝐸)↑2) / 2)) < (exp‘(2 / 𝐸))) |
201 | 177, 200 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → ((1 + (2 / 𝐸)) + (((2 / 𝐸)↑2) / 2)) < (exp‘(2 / 𝐸))) |
202 | 201, 88 | syl6breqr 4625 |
. . . . . . . 8
⊢ (𝜑 → ((1 + (2 / 𝐸)) + (((2 / 𝐸)↑2) / 2)) < 𝑋) |
203 | 193, 198,
91, 199, 202 | lttrd 10077 |
. . . . . . 7
⊢ (𝜑 → (((2 / 𝐸)↑2) / 2) < 𝑋) |
204 | 191, 203 | eqbrtrrd 4607 |
. . . . . 6
⊢ (𝜑 → ((2 / 𝐸) / 𝐸) < 𝑋) |
205 | 72, 70, 90, 204 | ltdiv23d 11813 |
. . . . 5
⊢ (𝜑 → ((2 / 𝐸) / 𝑋) < 𝐸) |
206 | 174, 205 | eqbrtrd 4605 |
. . . 4
⊢ (𝜑 → ((log‘𝑋) / 𝑋) < 𝐸) |
207 | 11, 157, 14, 170, 206 | lttrd 10077 |
. . 3
⊢ (𝜑 → ((log‘𝑁) / 𝑁) < 𝐸) |
208 | 11, 14, 207 | ltled 10064 |
. 2
⊢ (𝜑 → ((log‘𝑁) / 𝑁) ≤ 𝐸) |
209 | 9, 11, 14, 155, 208 | letrd 10073 |
1
⊢ (𝜑 → (abs‘((𝑅‘𝑁) / 𝑁)) ≤ 𝐸) |