Step | Hyp | Ref
| Expression |
1 | | pntlem1.m |
. . 3
โข ๐ =
((โโ((logโ๐) / (logโ๐พ))) + 1) |
2 | | pntlem1.x |
. . . . . . . . 9
โข (๐ โ (๐ โ โ+ โง ๐ < ๐)) |
3 | 2 | simpld 496 |
. . . . . . . 8
โข (๐ โ ๐ โ
โ+) |
4 | 3 | rpred 12964 |
. . . . . . 7
โข (๐ โ ๐ โ โ) |
5 | | 1red 11163 |
. . . . . . . 8
โข (๐ โ 1 โ
โ) |
6 | | pntlem1.y |
. . . . . . . . . 10
โข (๐ โ (๐ โ โ+ โง 1 โค
๐)) |
7 | 6 | simpld 496 |
. . . . . . . . 9
โข (๐ โ ๐ โ
โ+) |
8 | 7 | rpred 12964 |
. . . . . . . 8
โข (๐ โ ๐ โ โ) |
9 | 6 | simprd 497 |
. . . . . . . 8
โข (๐ โ 1 โค ๐) |
10 | 2 | simprd 497 |
. . . . . . . 8
โข (๐ โ ๐ < ๐) |
11 | 5, 8, 4, 9, 10 | lelttrd 11320 |
. . . . . . 7
โข (๐ โ 1 < ๐) |
12 | 4, 11 | rplogcld 26000 |
. . . . . 6
โข (๐ โ (logโ๐) โ
โ+) |
13 | | pntlem1.r |
. . . . . . . . . 10
โข ๐
= (๐ โ โ+ โฆ
((ฯโ๐) โ
๐)) |
14 | | pntlem1.a |
. . . . . . . . . 10
โข (๐ โ ๐ด โ
โ+) |
15 | | pntlem1.b |
. . . . . . . . . 10
โข (๐ โ ๐ต โ
โ+) |
16 | | pntlem1.l |
. . . . . . . . . 10
โข (๐ โ ๐ฟ โ (0(,)1)) |
17 | | pntlem1.d |
. . . . . . . . . 10
โข ๐ท = (๐ด + 1) |
18 | | pntlem1.f |
. . . . . . . . . 10
โข ๐น = ((1 โ (1 / ๐ท)) ยท ((๐ฟ / (;32 ยท ๐ต)) / (๐ทโ2))) |
19 | | pntlem1.u |
. . . . . . . . . 10
โข (๐ โ ๐ โ
โ+) |
20 | | pntlem1.u2 |
. . . . . . . . . 10
โข (๐ โ ๐ โค ๐ด) |
21 | | pntlem1.e |
. . . . . . . . . 10
โข ๐ธ = (๐ / ๐ท) |
22 | | pntlem1.k |
. . . . . . . . . 10
โข ๐พ = (expโ(๐ต / ๐ธ)) |
23 | 13, 14, 15, 16, 17, 18, 19, 20, 21, 22 | pntlemc 26959 |
. . . . . . . . 9
โข (๐ โ (๐ธ โ โ+ โง ๐พ โ โ+
โง (๐ธ โ (0(,)1)
โง 1 < ๐พ โง (๐ โ ๐ธ) โ
โ+))) |
24 | 23 | simp2d 1144 |
. . . . . . . 8
โข (๐ โ ๐พ โ
โ+) |
25 | 24 | rpred 12964 |
. . . . . . 7
โข (๐ โ ๐พ โ โ) |
26 | 23 | simp3d 1145 |
. . . . . . . 8
โข (๐ โ (๐ธ โ (0(,)1) โง 1 < ๐พ โง (๐ โ ๐ธ) โ
โ+)) |
27 | 26 | simp2d 1144 |
. . . . . . 7
โข (๐ โ 1 < ๐พ) |
28 | 25, 27 | rplogcld 26000 |
. . . . . 6
โข (๐ โ (logโ๐พ) โ
โ+) |
29 | 12, 28 | rpdivcld 12981 |
. . . . 5
โข (๐ โ ((logโ๐) / (logโ๐พ)) โ
โ+) |
30 | 29 | rprege0d 12971 |
. . . 4
โข (๐ โ (((logโ๐) / (logโ๐พ)) โ โ โง 0 โค
((logโ๐) /
(logโ๐พ)))) |
31 | | flge0nn0 13732 |
. . . 4
โข
((((logโ๐) /
(logโ๐พ)) โ
โ โง 0 โค ((logโ๐) / (logโ๐พ))) โ (โโ((logโ๐) / (logโ๐พ))) โ
โ0) |
32 | | nn0p1nn 12459 |
. . . 4
โข
((โโ((logโ๐) / (logโ๐พ))) โ โ0 โ
((โโ((logโ๐) / (logโ๐พ))) + 1) โ โ) |
33 | 30, 31, 32 | 3syl 18 |
. . 3
โข (๐ โ
((โโ((logโ๐) / (logโ๐พ))) + 1) โ โ) |
34 | 1, 33 | eqeltrid 2842 |
. 2
โข (๐ โ ๐ โ โ) |
35 | 34 | nnzd 12533 |
. . 3
โข (๐ โ ๐ โ โค) |
36 | | pntlem1.n |
. . . 4
โข ๐ =
(โโ(((logโ๐) / (logโ๐พ)) / 2)) |
37 | | pntlem1.c |
. . . . . . . . . 10
โข (๐ โ ๐ถ โ
โ+) |
38 | | pntlem1.w |
. . . . . . . . . 10
โข ๐ = (((๐ + (4 / (๐ฟ ยท ๐ธ)))โ2) + (((๐ ยท (๐พโ2))โ4) + (expโ(((;32 ยท ๐ต) / ((๐ โ ๐ธ) ยท (๐ฟ ยท (๐ธโ2)))) ยท ((๐ ยท 3) + ๐ถ))))) |
39 | | pntlem1.z |
. . . . . . . . . 10
โข (๐ โ ๐ โ (๐[,)+โ)) |
40 | 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 6, 2, 37, 38, 39 | pntlemb 26961 |
. . . . . . . . 9
โข (๐ โ (๐ โ โ+ โง (1 <
๐ โง e โค
(โโ๐) โง
(โโ๐) โค
(๐ / ๐)) โง ((4 / (๐ฟ ยท ๐ธ)) โค (โโ๐) โง (((logโ๐) / (logโ๐พ)) + 2) โค (((logโ๐) / (logโ๐พ)) / 4) โง ((๐ ยท 3) + ๐ถ) โค (((๐ โ ๐ธ) ยท ((๐ฟ ยท (๐ธโ2)) / (;32 ยท ๐ต))) ยท (logโ๐))))) |
41 | 40 | simp1d 1143 |
. . . . . . . 8
โข (๐ โ ๐ โ
โ+) |
42 | 41 | relogcld 25994 |
. . . . . . 7
โข (๐ โ (logโ๐) โ
โ) |
43 | 42, 28 | rerpdivcld 12995 |
. . . . . 6
โข (๐ โ ((logโ๐) / (logโ๐พ)) โ โ) |
44 | 43 | rehalfcld 12407 |
. . . . 5
โข (๐ โ (((logโ๐) / (logโ๐พ)) / 2) โ โ) |
45 | 44 | flcld 13710 |
. . . 4
โข (๐ โ
(โโ(((logโ๐) / (logโ๐พ)) / 2)) โ โค) |
46 | 36, 45 | eqeltrid 2842 |
. . 3
โข (๐ โ ๐ โ โค) |
47 | | 0red 11165 |
. . . . 5
โข (๐ โ 0 โ
โ) |
48 | | 4nn 12243 |
. . . . . 6
โข 4 โ
โ |
49 | | nndivre 12201 |
. . . . . 6
โข
((((logโ๐) /
(logโ๐พ)) โ
โ โง 4 โ โ) โ (((logโ๐) / (logโ๐พ)) / 4) โ โ) |
50 | 43, 48, 49 | sylancl 587 |
. . . . 5
โข (๐ โ (((logโ๐) / (logโ๐พ)) / 4) โ โ) |
51 | 46 | zred 12614 |
. . . . . 6
โข (๐ โ ๐ โ โ) |
52 | 34 | nnred 12175 |
. . . . . 6
โข (๐ โ ๐ โ โ) |
53 | 51, 52 | resubcld 11590 |
. . . . 5
โข (๐ โ (๐ โ ๐) โ โ) |
54 | 41 | rpred 12964 |
. . . . . . . . 9
โข (๐ โ ๐ โ โ) |
55 | 40 | simp2d 1144 |
. . . . . . . . . 10
โข (๐ โ (1 < ๐ โง e โค (โโ๐) โง (โโ๐) โค (๐ / ๐))) |
56 | 55 | simp1d 1143 |
. . . . . . . . 9
โข (๐ โ 1 < ๐) |
57 | 54, 56 | rplogcld 26000 |
. . . . . . . 8
โข (๐ โ (logโ๐) โ
โ+) |
58 | 57, 28 | rpdivcld 12981 |
. . . . . . 7
โข (๐ โ ((logโ๐) / (logโ๐พ)) โ
โ+) |
59 | | 4re 12244 |
. . . . . . . 8
โข 4 โ
โ |
60 | | 4pos 12267 |
. . . . . . . 8
โข 0 <
4 |
61 | 59, 60 | elrpii 12925 |
. . . . . . 7
โข 4 โ
โ+ |
62 | | rpdivcl 12947 |
. . . . . . 7
โข
((((logโ๐) /
(logโ๐พ)) โ
โ+ โง 4 โ โ+) โ
(((logโ๐) /
(logโ๐พ)) / 4) โ
โ+) |
63 | 58, 61, 62 | sylancl 587 |
. . . . . 6
โข (๐ โ (((logโ๐) / (logโ๐พ)) / 4) โ
โ+) |
64 | 63 | rpge0d 12968 |
. . . . 5
โข (๐ โ 0 โค (((logโ๐) / (logโ๐พ)) / 4)) |
65 | 50 | recnd 11190 |
. . . . . . . . 9
โข (๐ โ (((logโ๐) / (logโ๐พ)) / 4) โ โ) |
66 | 34 | nncnd 12176 |
. . . . . . . . 9
โข (๐ โ ๐ โ โ) |
67 | | 1cnd 11157 |
. . . . . . . . 9
โข (๐ โ 1 โ
โ) |
68 | 65, 66, 67 | addassd 11184 |
. . . . . . . 8
โข (๐ โ (((((logโ๐) / (logโ๐พ)) / 4) + ๐) + 1) = ((((logโ๐) / (logโ๐พ)) / 4) + (๐ + 1))) |
69 | 52, 5 | readdcld 11191 |
. . . . . . . . . 10
โข (๐ โ (๐ + 1) โ โ) |
70 | 50, 69 | readdcld 11191 |
. . . . . . . . 9
โข (๐ โ ((((logโ๐) / (logโ๐พ)) / 4) + (๐ + 1)) โ โ) |
71 | | peano2re 11335 |
. . . . . . . . . 10
โข (๐ โ โ โ (๐ + 1) โ
โ) |
72 | 51, 71 | syl 17 |
. . . . . . . . 9
โข (๐ โ (๐ + 1) โ โ) |
73 | 29 | rpred 12964 |
. . . . . . . . . . . . 13
โข (๐ โ ((logโ๐) / (logโ๐พ)) โ โ) |
74 | | 2re 12234 |
. . . . . . . . . . . . . 14
โข 2 โ
โ |
75 | 74 | a1i 11 |
. . . . . . . . . . . . 13
โข (๐ โ 2 โ
โ) |
76 | 73, 75 | readdcld 11191 |
. . . . . . . . . . . 12
โข (๐ โ (((logโ๐) / (logโ๐พ)) + 2) โ โ) |
77 | | reflcl 13708 |
. . . . . . . . . . . . . . . . 17
โข
(((logโ๐) /
(logโ๐พ)) โ
โ โ (โโ((logโ๐) / (logโ๐พ))) โ โ) |
78 | 73, 77 | syl 17 |
. . . . . . . . . . . . . . . 16
โข (๐ โ
(โโ((logโ๐) / (logโ๐พ))) โ โ) |
79 | 78 | recnd 11190 |
. . . . . . . . . . . . . . 15
โข (๐ โ
(โโ((logโ๐) / (logโ๐พ))) โ โ) |
80 | 79, 67, 67 | addassd 11184 |
. . . . . . . . . . . . . 14
โข (๐ โ
(((โโ((logโ๐) / (logโ๐พ))) + 1) + 1) =
((โโ((logโ๐) / (logโ๐พ))) + (1 + 1))) |
81 | 1 | oveq1i 7372 |
. . . . . . . . . . . . . 14
โข (๐ + 1) =
(((โโ((logโ๐) / (logโ๐พ))) + 1) + 1) |
82 | | df-2 12223 |
. . . . . . . . . . . . . . 15
โข 2 = (1 +
1) |
83 | 82 | oveq2i 7373 |
. . . . . . . . . . . . . 14
โข
((โโ((logโ๐) / (logโ๐พ))) + 2) = ((โโ((logโ๐) / (logโ๐พ))) + (1 + 1)) |
84 | 80, 81, 83 | 3eqtr4g 2802 |
. . . . . . . . . . . . 13
โข (๐ โ (๐ + 1) = ((โโ((logโ๐) / (logโ๐พ))) + 2)) |
85 | | flle 13711 |
. . . . . . . . . . . . . . 15
โข
(((logโ๐) /
(logโ๐พ)) โ
โ โ (โโ((logโ๐) / (logโ๐พ))) โค ((logโ๐) / (logโ๐พ))) |
86 | 73, 85 | syl 17 |
. . . . . . . . . . . . . 14
โข (๐ โ
(โโ((logโ๐) / (logโ๐พ))) โค ((logโ๐) / (logโ๐พ))) |
87 | 78, 73, 75, 86 | leadd1dd 11776 |
. . . . . . . . . . . . 13
โข (๐ โ
((โโ((logโ๐) / (logโ๐พ))) + 2) โค (((logโ๐) / (logโ๐พ)) + 2)) |
88 | 84, 87 | eqbrtrd 5132 |
. . . . . . . . . . . 12
โข (๐ โ (๐ + 1) โค (((logโ๐) / (logโ๐พ)) + 2)) |
89 | 40 | simp3d 1145 |
. . . . . . . . . . . . 13
โข (๐ โ ((4 / (๐ฟ ยท ๐ธ)) โค (โโ๐) โง (((logโ๐) / (logโ๐พ)) + 2) โค (((logโ๐) / (logโ๐พ)) / 4) โง ((๐ ยท 3) + ๐ถ) โค (((๐ โ ๐ธ) ยท ((๐ฟ ยท (๐ธโ2)) / (;32 ยท ๐ต))) ยท (logโ๐)))) |
90 | 89 | simp2d 1144 |
. . . . . . . . . . . 12
โข (๐ โ (((logโ๐) / (logโ๐พ)) + 2) โค (((logโ๐) / (logโ๐พ)) / 4)) |
91 | 69, 76, 50, 88, 90 | letrd 11319 |
. . . . . . . . . . 11
โข (๐ โ (๐ + 1) โค (((logโ๐) / (logโ๐พ)) / 4)) |
92 | 69, 50, 50, 91 | leadd2dd 11777 |
. . . . . . . . . 10
โข (๐ โ ((((logโ๐) / (logโ๐พ)) / 4) + (๐ + 1)) โค ((((logโ๐) / (logโ๐พ)) / 4) + (((logโ๐) / (logโ๐พ)) / 4))) |
93 | 43 | recnd 11190 |
. . . . . . . . . . . . . 14
โข (๐ โ ((logโ๐) / (logโ๐พ)) โ โ) |
94 | | 2cnd 12238 |
. . . . . . . . . . . . . 14
โข (๐ โ 2 โ
โ) |
95 | | 2ne0 12264 |
. . . . . . . . . . . . . . 15
โข 2 โ
0 |
96 | 95 | a1i 11 |
. . . . . . . . . . . . . 14
โข (๐ โ 2 โ 0) |
97 | 93, 94, 94, 96, 96 | divdiv1d 11969 |
. . . . . . . . . . . . 13
โข (๐ โ ((((logโ๐) / (logโ๐พ)) / 2) / 2) = (((logโ๐) / (logโ๐พ)) / (2 ยท 2))) |
98 | | 2t2e4 12324 |
. . . . . . . . . . . . . 14
โข (2
ยท 2) = 4 |
99 | 98 | oveq2i 7373 |
. . . . . . . . . . . . 13
โข
(((logโ๐) /
(logโ๐พ)) / (2
ยท 2)) = (((logโ๐) / (logโ๐พ)) / 4) |
100 | 97, 99 | eqtrdi 2793 |
. . . . . . . . . . . 12
โข (๐ โ ((((logโ๐) / (logโ๐พ)) / 2) / 2) = (((logโ๐) / (logโ๐พ)) / 4)) |
101 | 100 | oveq2d 7378 |
. . . . . . . . . . 11
โข (๐ โ (2 ยท
((((logโ๐) /
(logโ๐พ)) / 2) / 2)) =
(2 ยท (((logโ๐)
/ (logโ๐พ)) /
4))) |
102 | 44 | recnd 11190 |
. . . . . . . . . . . 12
โข (๐ โ (((logโ๐) / (logโ๐พ)) / 2) โ โ) |
103 | 102, 94, 96 | divcan2d 11940 |
. . . . . . . . . . 11
โข (๐ โ (2 ยท
((((logโ๐) /
(logโ๐พ)) / 2) / 2)) =
(((logโ๐) /
(logโ๐พ)) /
2)) |
104 | 65 | 2timesd 12403 |
. . . . . . . . . . 11
โข (๐ โ (2 ยท
(((logโ๐) /
(logโ๐พ)) / 4)) =
((((logโ๐) /
(logโ๐พ)) / 4) +
(((logโ๐) /
(logโ๐พ)) /
4))) |
105 | 101, 103,
104 | 3eqtr3d 2785 |
. . . . . . . . . 10
โข (๐ โ (((logโ๐) / (logโ๐พ)) / 2) = ((((logโ๐) / (logโ๐พ)) / 4) + (((logโ๐) / (logโ๐พ)) / 4))) |
106 | 92, 105 | breqtrrd 5138 |
. . . . . . . . 9
โข (๐ โ ((((logโ๐) / (logโ๐พ)) / 4) + (๐ + 1)) โค (((logโ๐) / (logโ๐พ)) / 2)) |
107 | | fllep1 13713 |
. . . . . . . . . . 11
โข
((((logโ๐) /
(logโ๐พ)) / 2) โ
โ โ (((logโ๐) / (logโ๐พ)) / 2) โค
((โโ(((logโ๐) / (logโ๐พ)) / 2)) + 1)) |
108 | 44, 107 | syl 17 |
. . . . . . . . . 10
โข (๐ โ (((logโ๐) / (logโ๐พ)) / 2) โค
((โโ(((logโ๐) / (logโ๐พ)) / 2)) + 1)) |
109 | 36 | oveq1i 7372 |
. . . . . . . . . 10
โข (๐ + 1) =
((โโ(((logโ๐) / (logโ๐พ)) / 2)) + 1) |
110 | 108, 109 | breqtrrdi 5152 |
. . . . . . . . 9
โข (๐ โ (((logโ๐) / (logโ๐พ)) / 2) โค (๐ + 1)) |
111 | 70, 44, 72, 106, 110 | letrd 11319 |
. . . . . . . 8
โข (๐ โ ((((logโ๐) / (logโ๐พ)) / 4) + (๐ + 1)) โค (๐ + 1)) |
112 | 68, 111 | eqbrtrd 5132 |
. . . . . . 7
โข (๐ โ (((((logโ๐) / (logโ๐พ)) / 4) + ๐) + 1) โค (๐ + 1)) |
113 | 50, 52 | readdcld 11191 |
. . . . . . . 8
โข (๐ โ ((((logโ๐) / (logโ๐พ)) / 4) + ๐) โ โ) |
114 | 113, 51, 5 | leadd1d 11756 |
. . . . . . 7
โข (๐ โ (((((logโ๐) / (logโ๐พ)) / 4) + ๐) โค ๐ โ (((((logโ๐) / (logโ๐พ)) / 4) + ๐) + 1) โค (๐ + 1))) |
115 | 112, 114 | mpbird 257 |
. . . . . 6
โข (๐ โ ((((logโ๐) / (logโ๐พ)) / 4) + ๐) โค ๐) |
116 | | leaddsub 11638 |
. . . . . . 7
โข
(((((logโ๐) /
(logโ๐พ)) / 4) โ
โ โง ๐ โ
โ โง ๐ โ
โ) โ (((((logโ๐) / (logโ๐พ)) / 4) + ๐) โค ๐ โ (((logโ๐) / (logโ๐พ)) / 4) โค (๐ โ ๐))) |
117 | 50, 52, 51, 116 | syl3anc 1372 |
. . . . . 6
โข (๐ โ (((((logโ๐) / (logโ๐พ)) / 4) + ๐) โค ๐ โ (((logโ๐) / (logโ๐พ)) / 4) โค (๐ โ ๐))) |
118 | 115, 117 | mpbid 231 |
. . . . 5
โข (๐ โ (((logโ๐) / (logโ๐พ)) / 4) โค (๐ โ ๐)) |
119 | 47, 50, 53, 64, 118 | letrd 11319 |
. . . 4
โข (๐ โ 0 โค (๐ โ ๐)) |
120 | 51, 52 | subge0d 11752 |
. . . 4
โข (๐ โ (0 โค (๐ โ ๐) โ ๐ โค ๐)) |
121 | 119, 120 | mpbid 231 |
. . 3
โข (๐ โ ๐ โค ๐) |
122 | | eluz2 12776 |
. . 3
โข (๐ โ
(โคโฅโ๐) โ (๐ โ โค โง ๐ โ โค โง ๐ โค ๐)) |
123 | 35, 46, 121, 122 | syl3anbrc 1344 |
. 2
โข (๐ โ ๐ โ (โคโฅโ๐)) |
124 | 34, 123, 118 | 3jca 1129 |
1
โข (๐ โ (๐ โ โ โง ๐ โ (โคโฅโ๐) โง (((logโ๐) / (logโ๐พ)) / 4) โค (๐ โ ๐))) |