Step | Hyp | Ref
| Expression |
1 | | pntpbnd1a.1 |
. . . . . . 7
β’ (π β π β β) |
2 | 1 | nnrpd 12960 |
. . . . . 6
β’ (π β π β
β+) |
3 | | pntpbnd.r |
. . . . . . . 8
β’ π
= (π β β+ β¦
((Οβπ) β
π)) |
4 | 3 | pntrf 26927 |
. . . . . . 7
β’ π
:β+βΆβ |
5 | 4 | ffvelcdmi 7035 |
. . . . . 6
β’ (π β β+
β (π
βπ) β
β) |
6 | 2, 5 | syl 17 |
. . . . 5
β’ (π β (π
βπ) β β) |
7 | 6, 2 | rerpdivcld 12993 |
. . . 4
β’ (π β ((π
βπ) / π) β β) |
8 | 7 | recnd 11188 |
. . 3
β’ (π β ((π
βπ) / π) β β) |
9 | 8 | abscld 15327 |
. 2
β’ (π β (absβ((π
βπ) / π)) β β) |
10 | 2 | relogcld 25994 |
. . 3
β’ (π β (logβπ) β
β) |
11 | 10, 2 | rerpdivcld 12993 |
. 2
β’ (π β ((logβπ) / π) β β) |
12 | | ioossre 13331 |
. . 3
β’ (0(,)1)
β β |
13 | | pntpbnd1.e |
. . 3
β’ (π β πΈ β (0(,)1)) |
14 | 12, 13 | sselid 3943 |
. 2
β’ (π β πΈ β β) |
15 | 6 | recnd 11188 |
. . . . 5
β’ (π β (π
βπ) β β) |
16 | 1 | nnred 12173 |
. . . . . 6
β’ (π β π β β) |
17 | 16 | recnd 11188 |
. . . . 5
β’ (π β π β β) |
18 | 1 | nnne0d 12208 |
. . . . 5
β’ (π β π β 0) |
19 | 15, 17, 18 | absdivd 15346 |
. . . 4
β’ (π β (absβ((π
βπ) / π)) = ((absβ(π
βπ)) / (absβπ))) |
20 | 1 | nnnn0d 12478 |
. . . . . . 7
β’ (π β π β
β0) |
21 | 20 | nn0ge0d 12481 |
. . . . . 6
β’ (π β 0 β€ π) |
22 | 16, 21 | absidd 15313 |
. . . . 5
β’ (π β (absβπ) = π) |
23 | 22 | oveq2d 7374 |
. . . 4
β’ (π β ((absβ(π
βπ)) / (absβπ)) = ((absβ(π
βπ)) / π)) |
24 | 19, 23 | eqtrd 2773 |
. . 3
β’ (π β (absβ((π
βπ) / π)) = ((absβ(π
βπ)) / π)) |
25 | 15 | abscld 15327 |
. . . 4
β’ (π β (absβ(π
βπ)) β β) |
26 | 1 | peano2nnd 12175 |
. . . . . . . . 9
β’ (π β (π + 1) β β) |
27 | | vmacl 26483 |
. . . . . . . . 9
β’ ((π + 1) β β β
(Ξβ(π + 1))
β β) |
28 | 26, 27 | syl 17 |
. . . . . . . 8
β’ (π β (Ξβ(π + 1)) β
β) |
29 | | peano2rem 11473 |
. . . . . . . 8
β’
((Ξβ(π
+ 1)) β β β ((Ξβ(π + 1)) β 1) β
β) |
30 | 28, 29 | syl 17 |
. . . . . . 7
β’ (π β ((Ξβ(π + 1)) β 1) β
β) |
31 | 30 | recnd 11188 |
. . . . . 6
β’ (π β ((Ξβ(π + 1)) β 1) β
β) |
32 | 31 | abscld 15327 |
. . . . 5
β’ (π β
(absβ((Ξβ(π + 1)) β 1)) β
β) |
33 | | pntpbnd1a.3 |
. . . . . 6
β’ (π β (absβ(π
βπ)) β€ (absβ((π
β(π + 1)) β (π
βπ)))) |
34 | 26 | nnrpd 12960 |
. . . . . . . . . 10
β’ (π β (π + 1) β
β+) |
35 | 3 | pntrval 26926 |
. . . . . . . . . 10
β’ ((π + 1) β β+
β (π
β(π + 1)) = ((Οβ(π + 1)) β (π + 1))) |
36 | 34, 35 | syl 17 |
. . . . . . . . 9
β’ (π β (π
β(π + 1)) = ((Οβ(π + 1)) β (π + 1))) |
37 | 3 | pntrval 26926 |
. . . . . . . . . 10
β’ (π β β+
β (π
βπ) = ((Οβπ) β π)) |
38 | 2, 37 | syl 17 |
. . . . . . . . 9
β’ (π β (π
βπ) = ((Οβπ) β π)) |
39 | 36, 38 | oveq12d 7376 |
. . . . . . . 8
β’ (π β ((π
β(π + 1)) β (π
βπ)) = (((Οβ(π + 1)) β (π + 1)) β ((Οβπ) β π))) |
40 | | peano2re 11333 |
. . . . . . . . . . . 12
β’ (π β β β (π + 1) β
β) |
41 | 16, 40 | syl 17 |
. . . . . . . . . . 11
β’ (π β (π + 1) β β) |
42 | | chpcl 26489 |
. . . . . . . . . . 11
β’ ((π + 1) β β β
(Οβ(π + 1))
β β) |
43 | 41, 42 | syl 17 |
. . . . . . . . . 10
β’ (π β (Οβ(π + 1)) β
β) |
44 | 43 | recnd 11188 |
. . . . . . . . 9
β’ (π β (Οβ(π + 1)) β
β) |
45 | 41 | recnd 11188 |
. . . . . . . . 9
β’ (π β (π + 1) β β) |
46 | | chpcl 26489 |
. . . . . . . . . . 11
β’ (π β β β
(Οβπ) β
β) |
47 | 16, 46 | syl 17 |
. . . . . . . . . 10
β’ (π β (Οβπ) β
β) |
48 | 47 | recnd 11188 |
. . . . . . . . 9
β’ (π β (Οβπ) β
β) |
49 | 44, 45, 48, 17 | sub4d 11566 |
. . . . . . . 8
β’ (π β (((Οβ(π + 1)) β (π + 1)) β
((Οβπ) β
π)) = (((Οβ(π + 1)) β
(Οβπ)) β
((π + 1) β π))) |
50 | 28 | recnd 11188 |
. . . . . . . . . 10
β’ (π β (Ξβ(π + 1)) β
β) |
51 | | chpp1 26520 |
. . . . . . . . . . 11
β’ (π β β0
β (Οβ(π +
1)) = ((Οβπ) +
(Ξβ(π +
1)))) |
52 | 20, 51 | syl 17 |
. . . . . . . . . 10
β’ (π β (Οβ(π + 1)) = ((Οβπ) + (Ξβ(π + 1)))) |
53 | 48, 50, 52 | mvrladdd 11573 |
. . . . . . . . 9
β’ (π β ((Οβ(π + 1)) β
(Οβπ)) =
(Ξβ(π +
1))) |
54 | | ax-1cn 11114 |
. . . . . . . . . 10
β’ 1 β
β |
55 | | pncan2 11413 |
. . . . . . . . . 10
β’ ((π β β β§ 1 β
β) β ((π + 1)
β π) =
1) |
56 | 17, 54, 55 | sylancl 587 |
. . . . . . . . 9
β’ (π β ((π + 1) β π) = 1) |
57 | 53, 56 | oveq12d 7376 |
. . . . . . . 8
β’ (π β (((Οβ(π + 1)) β
(Οβπ)) β
((π + 1) β π)) = ((Ξβ(π + 1)) β
1)) |
58 | 39, 49, 57 | 3eqtrd 2777 |
. . . . . . 7
β’ (π β ((π
β(π + 1)) β (π
βπ)) = ((Ξβ(π + 1)) β 1)) |
59 | 58 | fveq2d 6847 |
. . . . . 6
β’ (π β (absβ((π
β(π + 1)) β (π
βπ))) = (absβ((Ξβ(π + 1)) β
1))) |
60 | 33, 59 | breqtrd 5132 |
. . . . 5
β’ (π β (absβ(π
βπ)) β€ (absβ((Ξβ(π + 1)) β
1))) |
61 | | 1red 11161 |
. . . . . . . 8
β’ (π β 1 β
β) |
62 | 61, 10 | resubcld 11588 |
. . . . . . 7
β’ (π β (1 β
(logβπ)) β
β) |
63 | | 0red 11163 |
. . . . . . 7
β’ (π β 0 β
β) |
64 | | 2re 12232 |
. . . . . . . . . . 11
β’ 2 β
β |
65 | | eliooord 13329 |
. . . . . . . . . . . . . 14
β’ (πΈ β (0(,)1) β (0 <
πΈ β§ πΈ < 1)) |
66 | 13, 65 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β (0 < πΈ β§ πΈ < 1)) |
67 | 66 | simpld 496 |
. . . . . . . . . . . 12
β’ (π β 0 < πΈ) |
68 | 14, 67 | elrpd 12959 |
. . . . . . . . . . 11
β’ (π β πΈ β
β+) |
69 | | rerpdivcl 12950 |
. . . . . . . . . . 11
β’ ((2
β β β§ πΈ
β β+) β (2 / πΈ) β β) |
70 | 64, 68, 69 | sylancr 588 |
. . . . . . . . . 10
β’ (π β (2 / πΈ) β β) |
71 | 64 | a1i 11 |
. . . . . . . . . . 11
β’ (π β 2 β
β) |
72 | | 1lt2 12329 |
. . . . . . . . . . . 12
β’ 1 <
2 |
73 | 72 | a1i 11 |
. . . . . . . . . . 11
β’ (π β 1 < 2) |
74 | | 2cn 12233 |
. . . . . . . . . . . . 13
β’ 2 β
β |
75 | 74 | div1i 11888 |
. . . . . . . . . . . 12
β’ (2 / 1) =
2 |
76 | 66 | simprd 497 |
. . . . . . . . . . . . 13
β’ (π β πΈ < 1) |
77 | | 0lt1 11682 |
. . . . . . . . . . . . . . 15
β’ 0 <
1 |
78 | 77 | a1i 11 |
. . . . . . . . . . . . . 14
β’ (π β 0 < 1) |
79 | | 2pos 12261 |
. . . . . . . . . . . . . . 15
β’ 0 <
2 |
80 | 79 | a1i 11 |
. . . . . . . . . . . . . 14
β’ (π β 0 < 2) |
81 | | ltdiv2 12046 |
. . . . . . . . . . . . . 14
β’ (((πΈ β β β§ 0 <
πΈ) β§ (1 β β
β§ 0 < 1) β§ (2 β β β§ 0 < 2)) β (πΈ < 1 β (2 / 1) < (2 /
πΈ))) |
82 | 14, 67, 61, 78, 71, 80, 81 | syl222anc 1387 |
. . . . . . . . . . . . 13
β’ (π β (πΈ < 1 β (2 / 1) < (2 / πΈ))) |
83 | 76, 82 | mpbid 231 |
. . . . . . . . . . . 12
β’ (π β (2 / 1) < (2 / πΈ)) |
84 | 75, 83 | eqbrtrrid 5142 |
. . . . . . . . . . 11
β’ (π β 2 < (2 / πΈ)) |
85 | 61, 71, 70, 73, 84 | lttrd 11321 |
. . . . . . . . . 10
β’ (π β 1 < (2 / πΈ)) |
86 | | pntpbnd1.x |
. . . . . . . . . . . . 13
β’ π = (expβ(2 / πΈ)) |
87 | 70 | rpefcld 15992 |
. . . . . . . . . . . . . . . 16
β’ (π β (expβ(2 / πΈ)) β
β+) |
88 | 86, 87 | eqeltrid 2838 |
. . . . . . . . . . . . . . 15
β’ (π β π β
β+) |
89 | 88 | rpred 12962 |
. . . . . . . . . . . . . 14
β’ (π β π β β) |
90 | | pntpbnd1.y |
. . . . . . . . . . . . . . . 16
β’ (π β π β (π(,)+β)) |
91 | 88 | rpxrd 12963 |
. . . . . . . . . . . . . . . . 17
β’ (π β π β
β*) |
92 | | elioopnf 13366 |
. . . . . . . . . . . . . . . . 17
β’ (π β β*
β (π β (π(,)+β) β (π β β β§ π < π))) |
93 | 91, 92 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (π β (π β (π(,)+β) β (π β β β§ π < π))) |
94 | 90, 93 | mpbid 231 |
. . . . . . . . . . . . . . 15
β’ (π β (π β β β§ π < π)) |
95 | 94 | simpld 496 |
. . . . . . . . . . . . . 14
β’ (π β π β β) |
96 | 94 | simprd 497 |
. . . . . . . . . . . . . 14
β’ (π β π < π) |
97 | | pntpbnd1a.2 |
. . . . . . . . . . . . . . 15
β’ (π β (π < π β§ π β€ (πΎ Β· π))) |
98 | 97 | simpld 496 |
. . . . . . . . . . . . . 14
β’ (π β π < π) |
99 | 89, 95, 16, 96, 98 | lttrd 11321 |
. . . . . . . . . . . . 13
β’ (π β π < π) |
100 | 86, 99 | eqbrtrrid 5142 |
. . . . . . . . . . . 12
β’ (π β (expβ(2 / πΈ)) < π) |
101 | 2 | reeflogd 25995 |
. . . . . . . . . . . 12
β’ (π β
(expβ(logβπ)) =
π) |
102 | 100, 101 | breqtrrd 5134 |
. . . . . . . . . . 11
β’ (π β (expβ(2 / πΈ)) <
(expβ(logβπ))) |
103 | | eflt 16004 |
. . . . . . . . . . . 12
β’ (((2 /
πΈ) β β β§
(logβπ) β
β) β ((2 / πΈ)
< (logβπ) β
(expβ(2 / πΈ)) <
(expβ(logβπ)))) |
104 | 70, 10, 103 | syl2anc 585 |
. . . . . . . . . . 11
β’ (π β ((2 / πΈ) < (logβπ) β (expβ(2 / πΈ)) < (expβ(logβπ)))) |
105 | 102, 104 | mpbird 257 |
. . . . . . . . . 10
β’ (π β (2 / πΈ) < (logβπ)) |
106 | 61, 70, 10, 85, 105 | lttrd 11321 |
. . . . . . . . 9
β’ (π β 1 < (logβπ)) |
107 | 61, 10, 106 | ltled 11308 |
. . . . . . . 8
β’ (π β 1 β€ (logβπ)) |
108 | | 1re 11160 |
. . . . . . . . 9
β’ 1 β
β |
109 | | suble0 11674 |
. . . . . . . . 9
β’ ((1
β β β§ (logβπ) β β) β ((1 β
(logβπ)) β€ 0
β 1 β€ (logβπ))) |
110 | 108, 10, 109 | sylancr 588 |
. . . . . . . 8
β’ (π β ((1 β
(logβπ)) β€ 0
β 1 β€ (logβπ))) |
111 | 107, 110 | mpbird 257 |
. . . . . . 7
β’ (π β (1 β
(logβπ)) β€
0) |
112 | | vmage0 26486 |
. . . . . . . 8
β’ ((π + 1) β β β 0
β€ (Ξβ(π +
1))) |
113 | 26, 112 | syl 17 |
. . . . . . 7
β’ (π β 0 β€
(Ξβ(π +
1))) |
114 | 62, 63, 28, 111, 113 | letrd 11317 |
. . . . . 6
β’ (π β (1 β
(logβπ)) β€
(Ξβ(π +
1))) |
115 | 34 | relogcld 25994 |
. . . . . . 7
β’ (π β (logβ(π + 1)) β
β) |
116 | | readdcl 11139 |
. . . . . . . 8
β’ ((1
β β β§ (logβπ) β β) β (1 +
(logβπ)) β
β) |
117 | 108, 10, 116 | sylancr 588 |
. . . . . . 7
β’ (π β (1 + (logβπ)) β
β) |
118 | | vmalelog 26569 |
. . . . . . . 8
β’ ((π + 1) β β β
(Ξβ(π + 1))
β€ (logβ(π +
1))) |
119 | 26, 118 | syl 17 |
. . . . . . 7
β’ (π β (Ξβ(π + 1)) β€ (logβ(π + 1))) |
120 | 71, 16 | remulcld 11190 |
. . . . . . . . . 10
β’ (π β (2 Β· π) β
β) |
121 | | epr 16095 |
. . . . . . . . . . . 12
β’ e β
β+ |
122 | | rpmulcl 12943 |
. . . . . . . . . . . 12
β’ ((e
β β+ β§ π β β+) β (e
Β· π) β
β+) |
123 | 121, 2, 122 | sylancr 588 |
. . . . . . . . . . 11
β’ (π β (e Β· π) β
β+) |
124 | 123 | rpred 12962 |
. . . . . . . . . 10
β’ (π β (e Β· π) β
β) |
125 | 1 | nnge1d 12206 |
. . . . . . . . . . . 12
β’ (π β 1 β€ π) |
126 | 61, 16, 16, 125 | leadd2dd 11775 |
. . . . . . . . . . 11
β’ (π β (π + 1) β€ (π + π)) |
127 | 17 | 2timesd 12401 |
. . . . . . . . . . 11
β’ (π β (2 Β· π) = (π + π)) |
128 | 126, 127 | breqtrrd 5134 |
. . . . . . . . . 10
β’ (π β (π + 1) β€ (2 Β· π)) |
129 | | ere 15976 |
. . . . . . . . . . . . 13
β’ e β
β |
130 | | egt2lt3 16093 |
. . . . . . . . . . . . . 14
β’ (2 < e
β§ e < 3) |
131 | 130 | simpli 485 |
. . . . . . . . . . . . 13
β’ 2 <
e |
132 | 64, 129, 131 | ltleii 11283 |
. . . . . . . . . . . 12
β’ 2 β€
e |
133 | 132 | a1i 11 |
. . . . . . . . . . 11
β’ (π β 2 β€ e) |
134 | 129 | a1i 11 |
. . . . . . . . . . . 12
β’ (π β e β
β) |
135 | 1 | nngt0d 12207 |
. . . . . . . . . . . 12
β’ (π β 0 < π) |
136 | | lemul1 12012 |
. . . . . . . . . . . 12
β’ ((2
β β β§ e β β β§ (π β β β§ 0 < π)) β (2 β€ e β (2
Β· π) β€ (e
Β· π))) |
137 | 71, 134, 16, 135, 136 | syl112anc 1375 |
. . . . . . . . . . 11
β’ (π β (2 β€ e β (2
Β· π) β€ (e
Β· π))) |
138 | 133, 137 | mpbid 231 |
. . . . . . . . . 10
β’ (π β (2 Β· π) β€ (e Β· π)) |
139 | 41, 120, 124, 128, 138 | letrd 11317 |
. . . . . . . . 9
β’ (π β (π + 1) β€ (e Β· π)) |
140 | 34, 123 | logled 25998 |
. . . . . . . . 9
β’ (π β ((π + 1) β€ (e Β· π) β (logβ(π + 1)) β€ (logβ(e Β· π)))) |
141 | 139, 140 | mpbid 231 |
. . . . . . . 8
β’ (π β (logβ(π + 1)) β€ (logβ(e
Β· π))) |
142 | | relogmul 25963 |
. . . . . . . . . 10
β’ ((e
β β+ β§ π β β+) β
(logβ(e Β· π))
= ((logβe) + (logβπ))) |
143 | 121, 2, 142 | sylancr 588 |
. . . . . . . . 9
β’ (π β (logβ(e Β·
π)) = ((logβe) +
(logβπ))) |
144 | | loge 25958 |
. . . . . . . . . 10
β’
(logβe) = 1 |
145 | 144 | oveq1i 7368 |
. . . . . . . . 9
β’
((logβe) + (logβπ)) = (1 + (logβπ)) |
146 | 143, 145 | eqtrdi 2789 |
. . . . . . . 8
β’ (π β (logβ(e Β·
π)) = (1 + (logβπ))) |
147 | 141, 146 | breqtrd 5132 |
. . . . . . 7
β’ (π β (logβ(π + 1)) β€ (1 +
(logβπ))) |
148 | 28, 115, 117, 119, 147 | letrd 11317 |
. . . . . 6
β’ (π β (Ξβ(π + 1)) β€ (1 +
(logβπ))) |
149 | 28, 61, 10 | absdifled 15325 |
. . . . . 6
β’ (π β
((absβ((Ξβ(π + 1)) β 1)) β€ (logβπ) β ((1 β
(logβπ)) β€
(Ξβ(π + 1))
β§ (Ξβ(π +
1)) β€ (1 + (logβπ))))) |
150 | 114, 148,
149 | mpbir2and 712 |
. . . . 5
β’ (π β
(absβ((Ξβ(π + 1)) β 1)) β€ (logβπ)) |
151 | 25, 32, 10, 60, 150 | letrd 11317 |
. . . 4
β’ (π β (absβ(π
βπ)) β€ (logβπ)) |
152 | 25, 10, 2, 151 | lediv1dd 13020 |
. . 3
β’ (π β ((absβ(π
βπ)) / π) β€ ((logβπ) / π)) |
153 | 24, 152 | eqbrtrd 5128 |
. 2
β’ (π β (absβ((π
βπ) / π)) β€ ((logβπ) / π)) |
154 | 88 | relogcld 25994 |
. . . . 5
β’ (π β (logβπ) β
β) |
155 | 154, 88 | rerpdivcld 12993 |
. . . 4
β’ (π β ((logβπ) / π) β β) |
156 | 61, 70, 85 | ltled 11308 |
. . . . . . . 8
β’ (π β 1 β€ (2 / πΈ)) |
157 | | efle 16005 |
. . . . . . . . 9
β’ ((1
β β β§ (2 / πΈ) β β) β (1 β€ (2 / πΈ) β (expβ1) β€
(expβ(2 / πΈ)))) |
158 | 108, 70, 157 | sylancr 588 |
. . . . . . . 8
β’ (π β (1 β€ (2 / πΈ) β (expβ1) β€
(expβ(2 / πΈ)))) |
159 | 156, 158 | mpbid 231 |
. . . . . . 7
β’ (π β (expβ1) β€
(expβ(2 / πΈ))) |
160 | | df-e 15956 |
. . . . . . 7
β’ e =
(expβ1) |
161 | 159, 160,
86 | 3brtr4g 5140 |
. . . . . 6
β’ (π β e β€ π) |
162 | 144, 107 | eqbrtrid 5141 |
. . . . . . 7
β’ (π β (logβe) β€
(logβπ)) |
163 | | logleb 25974 |
. . . . . . . 8
β’ ((e
β β+ β§ π β β+) β (e β€
π β (logβe) β€
(logβπ))) |
164 | 121, 2, 163 | sylancr 588 |
. . . . . . 7
β’ (π β (e β€ π β (logβe) β€ (logβπ))) |
165 | 162, 164 | mpbird 257 |
. . . . . 6
β’ (π β e β€ π) |
166 | | logdivlt 25992 |
. . . . . 6
β’ (((π β β β§ e β€
π) β§ (π β β β§ e β€ π)) β (π < π β ((logβπ) / π) < ((logβπ) / π))) |
167 | 89, 161, 16, 165, 166 | syl22anc 838 |
. . . . 5
β’ (π β (π < π β ((logβπ) / π) < ((logβπ) / π))) |
168 | 99, 167 | mpbid 231 |
. . . 4
β’ (π β ((logβπ) / π) < ((logβπ) / π)) |
169 | 86 | fveq2i 6846 |
. . . . . . 7
β’
(logβπ) =
(logβ(expβ(2 / πΈ))) |
170 | 70 | relogefd 25999 |
. . . . . . 7
β’ (π β (logβ(expβ(2 /
πΈ))) = (2 / πΈ)) |
171 | 169, 170 | eqtrid 2785 |
. . . . . 6
β’ (π β (logβπ) = (2 / πΈ)) |
172 | 171 | oveq1d 7373 |
. . . . 5
β’ (π β ((logβπ) / π) = ((2 / πΈ) / π)) |
173 | | 2rp 12925 |
. . . . . . . . . . . . 13
β’ 2 β
β+ |
174 | | rpdivcl 12945 |
. . . . . . . . . . . . 13
β’ ((2
β β+ β§ πΈ β β+) β (2 /
πΈ) β
β+) |
175 | 173, 68, 174 | sylancr 588 |
. . . . . . . . . . . 12
β’ (π β (2 / πΈ) β
β+) |
176 | 175 | rpcnd 12964 |
. . . . . . . . . . 11
β’ (π β (2 / πΈ) β β) |
177 | 176 | sqvald 14054 |
. . . . . . . . . 10
β’ (π β ((2 / πΈ)β2) = ((2 / πΈ) Β· (2 / πΈ))) |
178 | | 2cnd 12236 |
. . . . . . . . . . 11
β’ (π β 2 β
β) |
179 | 68 | rpcnne0d 12971 |
. . . . . . . . . . 11
β’ (π β (πΈ β β β§ πΈ β 0)) |
180 | | div12 11840 |
. . . . . . . . . . 11
β’ (((2 /
πΈ) β β β§ 2
β β β§ (πΈ
β β β§ πΈ β
0)) β ((2 / πΈ)
Β· (2 / πΈ)) = (2
Β· ((2 / πΈ) / πΈ))) |
181 | 176, 178,
179, 180 | syl3anc 1372 |
. . . . . . . . . 10
β’ (π β ((2 / πΈ) Β· (2 / πΈ)) = (2 Β· ((2 / πΈ) / πΈ))) |
182 | 177, 181 | eqtrd 2773 |
. . . . . . . . 9
β’ (π β ((2 / πΈ)β2) = (2 Β· ((2 / πΈ) / πΈ))) |
183 | 182 | oveq1d 7373 |
. . . . . . . 8
β’ (π β (((2 / πΈ)β2) / 2) = ((2 Β· ((2 / πΈ) / πΈ)) / 2)) |
184 | 175, 68 | rpdivcld 12979 |
. . . . . . . . . 10
β’ (π β ((2 / πΈ) / πΈ) β
β+) |
185 | 184 | rpcnd 12964 |
. . . . . . . . 9
β’ (π β ((2 / πΈ) / πΈ) β β) |
186 | | 2ne0 12262 |
. . . . . . . . . 10
β’ 2 β
0 |
187 | 186 | a1i 11 |
. . . . . . . . 9
β’ (π β 2 β 0) |
188 | 185, 178,
187 | divcan3d 11941 |
. . . . . . . 8
β’ (π β ((2 Β· ((2 / πΈ) / πΈ)) / 2) = ((2 / πΈ) / πΈ)) |
189 | 183, 188 | eqtrd 2773 |
. . . . . . 7
β’ (π β (((2 / πΈ)β2) / 2) = ((2 / πΈ) / πΈ)) |
190 | 70 | resqcld 14036 |
. . . . . . . . 9
β’ (π β ((2 / πΈ)β2) β β) |
191 | 190 | rehalfcld 12405 |
. . . . . . . 8
β’ (π β (((2 / πΈ)β2) / 2) β
β) |
192 | | 1rp 12924 |
. . . . . . . . . . 11
β’ 1 β
β+ |
193 | | rpaddcl 12942 |
. . . . . . . . . . 11
β’ ((1
β β+ β§ (2 / πΈ) β β+) β (1 + (2
/ πΈ)) β
β+) |
194 | 192, 175,
193 | sylancr 588 |
. . . . . . . . . 10
β’ (π β (1 + (2 / πΈ)) β
β+) |
195 | 194 | rpred 12962 |
. . . . . . . . 9
β’ (π β (1 + (2 / πΈ)) β
β) |
196 | 195, 191 | readdcld 11189 |
. . . . . . . 8
β’ (π β ((1 + (2 / πΈ)) + (((2 / πΈ)β2) / 2)) β
β) |
197 | 191, 194 | ltaddrp2d 12996 |
. . . . . . . 8
β’ (π β (((2 / πΈ)β2) / 2) < ((1 + (2 / πΈ)) + (((2 / πΈ)β2) / 2))) |
198 | | efgt1p2 16001 |
. . . . . . . . . 10
β’ ((2 /
πΈ) β
β+ β ((1 + (2 / πΈ)) + (((2 / πΈ)β2) / 2)) < (expβ(2 / πΈ))) |
199 | 175, 198 | syl 17 |
. . . . . . . . 9
β’ (π β ((1 + (2 / πΈ)) + (((2 / πΈ)β2) / 2)) < (expβ(2 / πΈ))) |
200 | 199, 86 | breqtrrdi 5148 |
. . . . . . . 8
β’ (π β ((1 + (2 / πΈ)) + (((2 / πΈ)β2) / 2)) < π) |
201 | 191, 196,
89, 197, 200 | lttrd 11321 |
. . . . . . 7
β’ (π β (((2 / πΈ)β2) / 2) < π) |
202 | 189, 201 | eqbrtrrd 5130 |
. . . . . 6
β’ (π β ((2 / πΈ) / πΈ) < π) |
203 | 70, 68, 88, 202 | ltdiv23d 13029 |
. . . . 5
β’ (π β ((2 / πΈ) / π) < πΈ) |
204 | 172, 203 | eqbrtrd 5128 |
. . . 4
β’ (π β ((logβπ) / π) < πΈ) |
205 | 11, 155, 14, 168, 204 | lttrd 11321 |
. . 3
β’ (π β ((logβπ) / π) < πΈ) |
206 | 11, 14, 205 | ltled 11308 |
. 2
β’ (π β ((logβπ) / π) β€ πΈ) |
207 | 9, 11, 14, 153, 206 | letrd 11317 |
1
β’ (π β (absβ((π
βπ) / π)) β€ πΈ) |