Step | Hyp | Ref
| Expression |
1 | | pntlem1.r |
. . . . . . 7
โข ๐
= (๐ โ โ+ โฆ
((ฯโ๐) โ
๐)) |
2 | | pntlem1.a |
. . . . . . 7
โข (๐ โ ๐ด โ
โ+) |
3 | | pntlem1.b |
. . . . . . 7
โข (๐ โ ๐ต โ
โ+) |
4 | | pntlem1.l |
. . . . . . 7
โข (๐ โ ๐ฟ โ (0(,)1)) |
5 | | pntlem1.d |
. . . . . . 7
โข ๐ท = (๐ด + 1) |
6 | | pntlem1.f |
. . . . . . 7
โข ๐น = ((1 โ (1 / ๐ท)) ยท ((๐ฟ / (;32 ยท ๐ต)) / (๐ทโ2))) |
7 | | pntlem1.u |
. . . . . . 7
โข (๐ โ ๐ โ
โ+) |
8 | | pntlem1.u2 |
. . . . . . 7
โข (๐ โ ๐ โค ๐ด) |
9 | | pntlem1.e |
. . . . . . 7
โข ๐ธ = (๐ / ๐ท) |
10 | | pntlem1.k |
. . . . . . 7
โข ๐พ = (expโ(๐ต / ๐ธ)) |
11 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10 | pntlemc 26959 |
. . . . . 6
โข (๐ โ (๐ธ โ โ+ โง ๐พ โ โ+
โง (๐ธ โ (0(,)1)
โง 1 < ๐พ โง (๐ โ ๐ธ) โ
โ+))) |
12 | 11 | simp3d 1145 |
. . . . 5
โข (๐ โ (๐ธ โ (0(,)1) โง 1 < ๐พ โง (๐ โ ๐ธ) โ
โ+)) |
13 | 12 | simp3d 1145 |
. . . 4
โข (๐ โ (๐ โ ๐ธ) โ
โ+) |
14 | 1, 2, 3, 4, 5, 6 | pntlemd 26958 |
. . . . . . . 8
โข (๐ โ (๐ฟ โ โ+ โง ๐ท โ โ+
โง ๐น โ
โ+)) |
15 | 14 | simp1d 1143 |
. . . . . . 7
โข (๐ โ ๐ฟ โ
โ+) |
16 | 11 | simp1d 1143 |
. . . . . . 7
โข (๐ โ ๐ธ โ
โ+) |
17 | 15, 16 | rpmulcld 12978 |
. . . . . 6
โข (๐ โ (๐ฟ ยท ๐ธ) โ
โ+) |
18 | | 8nn 12253 |
. . . . . . 7
โข 8 โ
โ |
19 | | nnrp 12931 |
. . . . . . 7
โข (8 โ
โ โ 8 โ โ+) |
20 | 18, 19 | ax-mp 5 |
. . . . . 6
โข 8 โ
โ+ |
21 | | rpdivcl 12945 |
. . . . . 6
โข (((๐ฟ ยท ๐ธ) โ โ+ โง 8 โ
โ+) โ ((๐ฟ ยท ๐ธ) / 8) โ
โ+) |
22 | 17, 20, 21 | sylancl 587 |
. . . . 5
โข (๐ โ ((๐ฟ ยท ๐ธ) / 8) โ
โ+) |
23 | | pntlem1.y |
. . . . . . . . 9
โข (๐ โ (๐ โ โ+ โง 1 โค
๐)) |
24 | | pntlem1.x |
. . . . . . . . 9
โข (๐ โ (๐ โ โ+ โง ๐ < ๐)) |
25 | | pntlem1.c |
. . . . . . . . 9
โข (๐ โ ๐ถ โ
โ+) |
26 | | pntlem1.w |
. . . . . . . . 9
โข ๐ = (((๐ + (4 / (๐ฟ ยท ๐ธ)))โ2) + (((๐ ยท (๐พโ2))โ4) + (expโ(((;32 ยท ๐ต) / ((๐ โ ๐ธ) ยท (๐ฟ ยท (๐ธโ2)))) ยท ((๐ ยท 3) + ๐ถ))))) |
27 | | pntlem1.z |
. . . . . . . . 9
โข (๐ โ ๐ โ (๐[,)+โ)) |
28 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
23, 24, 25, 26, 27 | pntlemb 26961 |
. . . . . . . 8
โข (๐ โ (๐ โ โ+ โง (1 <
๐ โง e โค
(โโ๐) โง
(โโ๐) โค
(๐ / ๐)) โง ((4 / (๐ฟ ยท ๐ธ)) โค (โโ๐) โง (((logโ๐) / (logโ๐พ)) + 2) โค (((logโ๐) / (logโ๐พ)) / 4) โง ((๐ ยท 3) + ๐ถ) โค (((๐ โ ๐ธ) ยท ((๐ฟ ยท (๐ธโ2)) / (;32 ยท ๐ต))) ยท (logโ๐))))) |
29 | 28 | simp1d 1143 |
. . . . . . 7
โข (๐ โ ๐ โ
โ+) |
30 | 29 | rpred 12962 |
. . . . . 6
โข (๐ โ ๐ โ โ) |
31 | 28 | simp2d 1144 |
. . . . . . 7
โข (๐ โ (1 < ๐ โง e โค (โโ๐) โง (โโ๐) โค (๐ / ๐))) |
32 | 31 | simp1d 1143 |
. . . . . 6
โข (๐ โ 1 < ๐) |
33 | 30, 32 | rplogcld 26000 |
. . . . 5
โข (๐ โ (logโ๐) โ
โ+) |
34 | 22, 33 | rpmulcld 12978 |
. . . 4
โข (๐ โ (((๐ฟ ยท ๐ธ) / 8) ยท (logโ๐)) โ
โ+) |
35 | 13, 34 | rpmulcld 12978 |
. . 3
โข (๐ โ ((๐ โ ๐ธ) ยท (((๐ฟ ยท ๐ธ) / 8) ยท (logโ๐))) โ
โ+) |
36 | 35 | rpred 12962 |
. 2
โข (๐ โ ((๐ โ ๐ธ) ยท (((๐ฟ ยท ๐ธ) / 8) ยท (logโ๐))) โ โ) |
37 | | pntlem1.i |
. . . . . 6
โข ๐ผ = (((โโ(๐ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐))) + 1)...(โโ(๐ / ๐))) |
38 | | fzfid 13884 |
. . . . . 6
โข (๐ โ (((โโ(๐ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐))) + 1)...(โโ(๐ / ๐))) โ Fin) |
39 | 37, 38 | eqeltrid 2838 |
. . . . 5
โข (๐ โ ๐ผ โ Fin) |
40 | | hashcl 14262 |
. . . . 5
โข (๐ผ โ Fin โ
(โฏโ๐ผ) โ
โ0) |
41 | 39, 40 | syl 17 |
. . . 4
โข (๐ โ (โฏโ๐ผ) โ
โ0) |
42 | 41 | nn0red 12479 |
. . 3
โข (๐ โ (โฏโ๐ผ) โ
โ) |
43 | 13 | rpred 12962 |
. . . 4
โข (๐ โ (๐ โ ๐ธ) โ โ) |
44 | | pntlem1.v |
. . . . . . 7
โข (๐ โ ๐ โ
โ+) |
45 | 29, 44 | rpdivcld 12979 |
. . . . . 6
โข (๐ โ (๐ / ๐) โ
โ+) |
46 | 45 | relogcld 25994 |
. . . . 5
โข (๐ โ (logโ(๐ / ๐)) โ โ) |
47 | 46, 45 | rerpdivcld 12993 |
. . . 4
โข (๐ โ ((logโ(๐ / ๐)) / (๐ / ๐)) โ โ) |
48 | 43, 47 | remulcld 11190 |
. . 3
โข (๐ โ ((๐ โ ๐ธ) ยท ((logโ(๐ / ๐)) / (๐ / ๐))) โ โ) |
49 | 42, 48 | remulcld 11190 |
. 2
โข (๐ โ ((โฏโ๐ผ) ยท ((๐ โ ๐ธ) ยท ((logโ(๐ / ๐)) / (๐ / ๐)))) โ โ) |
50 | | pntlem1.o |
. . . 4
โข ๐ = (((โโ(๐ / (๐พโ(๐ฝ + 1)))) + 1)...(โโ(๐ / (๐พโ๐ฝ)))) |
51 | | fzfid 13884 |
. . . 4
โข (๐ โ (((โโ(๐ / (๐พโ(๐ฝ + 1)))) + 1)...(โโ(๐ / (๐พโ๐ฝ)))) โ Fin) |
52 | 50, 51 | eqeltrid 2838 |
. . 3
โข (๐ โ ๐ โ Fin) |
53 | 7 | rpred 12962 |
. . . . . . 7
โข (๐ โ ๐ โ โ) |
54 | 53 | adantr 482 |
. . . . . 6
โข ((๐ โง ๐ โ ๐) โ ๐ โ โ) |
55 | 11 | simp2d 1144 |
. . . . . . . . . . 11
โข (๐ โ ๐พ โ
โ+) |
56 | | pntlem1.j |
. . . . . . . . . . . . 13
โข (๐ โ ๐ฝ โ (๐..^๐)) |
57 | | elfzoelz 13578 |
. . . . . . . . . . . . 13
โข (๐ฝ โ (๐..^๐) โ ๐ฝ โ โค) |
58 | 56, 57 | syl 17 |
. . . . . . . . . . . 12
โข (๐ โ ๐ฝ โ โค) |
59 | 58 | peano2zd 12615 |
. . . . . . . . . . 11
โข (๐ โ (๐ฝ + 1) โ โค) |
60 | 55, 59 | rpexpcld 14156 |
. . . . . . . . . 10
โข (๐ โ (๐พโ(๐ฝ + 1)) โ
โ+) |
61 | 29, 60 | rpdivcld 12979 |
. . . . . . . . 9
โข (๐ โ (๐ / (๐พโ(๐ฝ + 1))) โ
โ+) |
62 | 61 | rprege0d 12969 |
. . . . . . . 8
โข (๐ โ ((๐ / (๐พโ(๐ฝ + 1))) โ โ โง 0 โค (๐ / (๐พโ(๐ฝ + 1))))) |
63 | | flge0nn0 13731 |
. . . . . . . 8
โข (((๐ / (๐พโ(๐ฝ + 1))) โ โ โง 0 โค (๐ / (๐พโ(๐ฝ + 1)))) โ (โโ(๐ / (๐พโ(๐ฝ + 1)))) โ
โ0) |
64 | | nn0p1nn 12457 |
. . . . . . . 8
โข
((โโ(๐ /
(๐พโ(๐ฝ + 1)))) โ โ0 โ
((โโ(๐ / (๐พโ(๐ฝ + 1)))) + 1) โ
โ) |
65 | 62, 63, 64 | 3syl 18 |
. . . . . . 7
โข (๐ โ ((โโ(๐ / (๐พโ(๐ฝ + 1)))) + 1) โ
โ) |
66 | | elfzuz 13443 |
. . . . . . . 8
โข (๐ โ (((โโ(๐ / (๐พโ(๐ฝ + 1)))) + 1)...(โโ(๐ / (๐พโ๐ฝ)))) โ ๐ โ
(โคโฅโ((โโ(๐ / (๐พโ(๐ฝ + 1)))) + 1))) |
67 | 66, 50 | eleq2s 2852 |
. . . . . . 7
โข (๐ โ ๐ โ ๐ โ
(โคโฅโ((โโ(๐ / (๐พโ(๐ฝ + 1)))) + 1))) |
68 | | eluznn 12848 |
. . . . . . 7
โข
((((โโ(๐
/ (๐พโ(๐ฝ + 1)))) + 1) โ โ
โง ๐ โ
(โคโฅโ((โโ(๐ / (๐พโ(๐ฝ + 1)))) + 1))) โ ๐ โ โ) |
69 | 65, 67, 68 | syl2an 597 |
. . . . . 6
โข ((๐ โง ๐ โ ๐) โ ๐ โ โ) |
70 | 54, 69 | nndivred 12212 |
. . . . 5
โข ((๐ โง ๐ โ ๐) โ (๐ / ๐) โ โ) |
71 | 29 | adantr 482 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ ๐) โ ๐ โ
โ+) |
72 | 69 | nnrpd 12960 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ ๐) โ ๐ โ โ+) |
73 | 71, 72 | rpdivcld 12979 |
. . . . . . . . 9
โข ((๐ โง ๐ โ ๐) โ (๐ / ๐) โ
โ+) |
74 | 1 | pntrf 26927 |
. . . . . . . . . 10
โข ๐
:โ+โถโ |
75 | 74 | ffvelcdmi 7035 |
. . . . . . . . 9
โข ((๐ / ๐) โ โ+ โ (๐
โ(๐ / ๐)) โ โ) |
76 | 73, 75 | syl 17 |
. . . . . . . 8
โข ((๐ โง ๐ โ ๐) โ (๐
โ(๐ / ๐)) โ โ) |
77 | 76, 71 | rerpdivcld 12993 |
. . . . . . 7
โข ((๐ โง ๐ โ ๐) โ ((๐
โ(๐ / ๐)) / ๐) โ โ) |
78 | 77 | recnd 11188 |
. . . . . 6
โข ((๐ โง ๐ โ ๐) โ ((๐
โ(๐ / ๐)) / ๐) โ โ) |
79 | 78 | abscld 15327 |
. . . . 5
โข ((๐ โง ๐ โ ๐) โ (absโ((๐
โ(๐ / ๐)) / ๐)) โ โ) |
80 | 70, 79 | resubcld 11588 |
. . . 4
โข ((๐ โง ๐ โ ๐) โ ((๐ / ๐) โ (absโ((๐
โ(๐ / ๐)) / ๐))) โ โ) |
81 | 72 | relogcld 25994 |
. . . 4
โข ((๐ โง ๐ โ ๐) โ (logโ๐) โ โ) |
82 | 80, 81 | remulcld 11190 |
. . 3
โข ((๐ โง ๐ โ ๐) โ (((๐ / ๐) โ (absโ((๐
โ(๐ / ๐)) / ๐))) ยท (logโ๐)) โ โ) |
83 | 52, 82 | fsumrecl 15624 |
. 2
โข (๐ โ ฮฃ๐ โ ๐ (((๐ / ๐) โ (absโ((๐
โ(๐ / ๐)) / ๐))) ยท (logโ๐)) โ โ) |
84 | | pntlem1.m |
. . 3
โข ๐ =
((โโ((logโ๐) / (logโ๐พ))) + 1) |
85 | | pntlem1.n |
. . 3
โข ๐ =
(โโ(((logโ๐) / (logโ๐พ)) / 2)) |
86 | | pntlem1.U |
. . 3
โข (๐ โ โ๐ง โ (๐[,)+โ)(absโ((๐
โ๐ง) / ๐ง)) โค ๐) |
87 | | pntlem1.K |
. . 3
โข (๐ โ โ๐ฆ โ (๐(,)+โ)โ๐ง โ โ+ ((๐ฆ < ๐ง โง ((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง) < (๐พ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง))(absโ((๐
โ๐ข) / ๐ข)) โค ๐ธ)) |
88 | | pntlem1.V |
. . 3
โข (๐ โ (((๐พโ๐ฝ) < ๐ โง ((1 + (๐ฟ ยท ๐ธ)) ยท ๐) < (๐พ ยท (๐พโ๐ฝ))) โง โ๐ข โ (๐[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐))(absโ((๐
โ๐ข) / ๐ข)) โค ๐ธ)) |
89 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
23, 24, 25, 26, 27, 84, 85, 86, 87, 50, 44, 88, 56, 37 | pntlemr 26966 |
. 2
โข (๐ โ ((๐ โ ๐ธ) ยท (((๐ฟ ยท ๐ธ) / 8) ยท (logโ๐))) โค ((โฏโ๐ผ) ยท ((๐ โ ๐ธ) ยท ((logโ(๐ / ๐)) / (๐ / ๐))))) |
90 | 48 | recnd 11188 |
. . . . 5
โข (๐ โ ((๐ โ ๐ธ) ยท ((logโ(๐ / ๐)) / (๐ / ๐))) โ โ) |
91 | | fsumconst 15680 |
. . . . 5
โข ((๐ผ โ Fin โง ((๐ โ ๐ธ) ยท ((logโ(๐ / ๐)) / (๐ / ๐))) โ โ) โ ฮฃ๐ โ ๐ผ ((๐ โ ๐ธ) ยท ((logโ(๐ / ๐)) / (๐ / ๐))) = ((โฏโ๐ผ) ยท ((๐ โ ๐ธ) ยท ((logโ(๐ / ๐)) / (๐ / ๐))))) |
92 | 39, 90, 91 | syl2anc 585 |
. . . 4
โข (๐ โ ฮฃ๐ โ ๐ผ ((๐ โ ๐ธ) ยท ((logโ(๐ / ๐)) / (๐ / ๐))) = ((โฏโ๐ผ) ยท ((๐ โ ๐ธ) ยท ((logโ(๐ / ๐)) / (๐ / ๐))))) |
93 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
23, 24, 25, 26, 27, 84, 85, 86, 87, 50, 44, 88, 56, 37 | pntlemq 26965 |
. . . . 5
โข (๐ โ ๐ผ โ ๐) |
94 | 90 | ralrimivw 3144 |
. . . . 5
โข (๐ โ โ๐ โ ๐ผ ((๐ โ ๐ธ) ยท ((logโ(๐ / ๐)) / (๐ / ๐))) โ โ) |
95 | 52 | olcd 873 |
. . . . 5
โข (๐ โ (๐ โ (โคโฅโ1)
โจ ๐ โ
Fin)) |
96 | | sumss2 15616 |
. . . . 5
โข (((๐ผ โ ๐ โง โ๐ โ ๐ผ ((๐ โ ๐ธ) ยท ((logโ(๐ / ๐)) / (๐ / ๐))) โ โ) โง (๐ โ (โคโฅโ1)
โจ ๐ โ Fin)) โ
ฮฃ๐ โ ๐ผ ((๐ โ ๐ธ) ยท ((logโ(๐ / ๐)) / (๐ / ๐))) = ฮฃ๐ โ ๐ if(๐ โ ๐ผ, ((๐ โ ๐ธ) ยท ((logโ(๐ / ๐)) / (๐ / ๐))), 0)) |
97 | 93, 94, 95, 96 | syl21anc 837 |
. . . 4
โข (๐ โ ฮฃ๐ โ ๐ผ ((๐ โ ๐ธ) ยท ((logโ(๐ / ๐)) / (๐ / ๐))) = ฮฃ๐ โ ๐ if(๐ โ ๐ผ, ((๐ โ ๐ธ) ยท ((logโ(๐ / ๐)) / (๐ / ๐))), 0)) |
98 | 92, 97 | eqtr3d 2775 |
. . 3
โข (๐ โ ((โฏโ๐ผ) ยท ((๐ โ ๐ธ) ยท ((logโ(๐ / ๐)) / (๐ / ๐)))) = ฮฃ๐ โ ๐ if(๐ โ ๐ผ, ((๐ โ ๐ธ) ยท ((logโ(๐ / ๐)) / (๐ / ๐))), 0)) |
99 | 48 | adantr 482 |
. . . . . 6
โข ((๐ โง ๐ โ ๐ผ) โ ((๐ โ ๐ธ) ยท ((logโ(๐ / ๐)) / (๐ / ๐))) โ โ) |
100 | 99 | adantlr 714 |
. . . . 5
โข (((๐ โง ๐ โ ๐) โง ๐ โ ๐ผ) โ ((๐ โ ๐ธ) ยท ((logโ(๐ / ๐)) / (๐ / ๐))) โ โ) |
101 | | 0red 11163 |
. . . . 5
โข (((๐ โง ๐ โ ๐) โง ยฌ ๐ โ ๐ผ) โ 0 โ โ) |
102 | 100, 101 | ifclda 4522 |
. . . 4
โข ((๐ โง ๐ โ ๐) โ if(๐ โ ๐ผ, ((๐ โ ๐ธ) ยท ((logโ(๐ / ๐)) / (๐ / ๐))), 0) โ โ) |
103 | | breq1 5109 |
. . . . 5
โข (((๐ โ ๐ธ) ยท ((logโ(๐ / ๐)) / (๐ / ๐))) = if(๐ โ ๐ผ, ((๐ โ ๐ธ) ยท ((logโ(๐ / ๐)) / (๐ / ๐))), 0) โ (((๐ โ ๐ธ) ยท ((logโ(๐ / ๐)) / (๐ / ๐))) โค (((๐ / ๐) โ (absโ((๐
โ(๐ / ๐)) / ๐))) ยท (logโ๐)) โ if(๐ โ ๐ผ, ((๐ โ ๐ธ) ยท ((logโ(๐ / ๐)) / (๐ / ๐))), 0) โค (((๐ / ๐) โ (absโ((๐
โ(๐ / ๐)) / ๐))) ยท (logโ๐)))) |
104 | | breq1 5109 |
. . . . 5
โข (0 =
if(๐ โ ๐ผ, ((๐ โ ๐ธ) ยท ((logโ(๐ / ๐)) / (๐ / ๐))), 0) โ (0 โค (((๐ / ๐) โ (absโ((๐
โ(๐ / ๐)) / ๐))) ยท (logโ๐)) โ if(๐ โ ๐ผ, ((๐ โ ๐ธ) ยท ((logโ(๐ / ๐)) / (๐ / ๐))), 0) โค (((๐ / ๐) โ (absโ((๐
โ(๐ / ๐)) / ๐))) ยท (logโ๐)))) |
105 | 13 | rpregt0d 12968 |
. . . . . . . . . 10
โข (๐ โ ((๐ โ ๐ธ) โ โ โง 0 < (๐ โ ๐ธ))) |
106 | 105 | adantr 482 |
. . . . . . . . 9
โข ((๐ โง ๐ โ ๐ผ) โ ((๐ โ ๐ธ) โ โ โง 0 < (๐ โ ๐ธ))) |
107 | 106 | simpld 496 |
. . . . . . . 8
โข ((๐ โง ๐ โ ๐ผ) โ (๐ โ ๐ธ) โ โ) |
108 | | 1rp 12924 |
. . . . . . . . . . . . . . . . 17
โข 1 โ
โ+ |
109 | | rpaddcl 12942 |
. . . . . . . . . . . . . . . . 17
โข ((1
โ โ+ โง (๐ฟ ยท ๐ธ) โ โ+) โ (1 +
(๐ฟ ยท ๐ธ)) โ
โ+) |
110 | 108, 17, 109 | sylancr 588 |
. . . . . . . . . . . . . . . 16
โข (๐ โ (1 + (๐ฟ ยท ๐ธ)) โ
โ+) |
111 | 110, 44 | rpmulcld 12978 |
. . . . . . . . . . . . . . 15
โข (๐ โ ((1 + (๐ฟ ยท ๐ธ)) ยท ๐) โ
โ+) |
112 | 29, 111 | rpdivcld 12979 |
. . . . . . . . . . . . . 14
โข (๐ โ (๐ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐)) โ
โ+) |
113 | 112 | rprege0d 12969 |
. . . . . . . . . . . . 13
โข (๐ โ ((๐ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐)) โ โ โง 0 โค (๐ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐)))) |
114 | | flge0nn0 13731 |
. . . . . . . . . . . . 13
โข (((๐ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐)) โ โ โง 0 โค (๐ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐))) โ (โโ(๐ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐))) โ
โ0) |
115 | | nn0p1nn 12457 |
. . . . . . . . . . . . 13
โข
((โโ(๐ /
((1 + (๐ฟ ยท ๐ธ)) ยท ๐))) โ โ0 โ
((โโ(๐ / ((1 +
(๐ฟ ยท ๐ธ)) ยท ๐))) + 1) โ โ) |
116 | 113, 114,
115 | 3syl 18 |
. . . . . . . . . . . 12
โข (๐ โ ((โโ(๐ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐))) + 1) โ โ) |
117 | | elfzuz 13443 |
. . . . . . . . . . . . 13
โข (๐ โ (((โโ(๐ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐))) + 1)...(โโ(๐ / ๐))) โ ๐ โ
(โคโฅโ((โโ(๐ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐))) + 1))) |
118 | 117, 37 | eleq2s 2852 |
. . . . . . . . . . . 12
โข (๐ โ ๐ผ โ ๐ โ
(โคโฅโ((โโ(๐ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐))) + 1))) |
119 | | eluznn 12848 |
. . . . . . . . . . . 12
โข
((((โโ(๐
/ ((1 + (๐ฟ ยท ๐ธ)) ยท ๐))) + 1) โ โ โง ๐ โ
(โคโฅโ((โโ(๐ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐))) + 1))) โ ๐ โ โ) |
120 | 116, 118,
119 | syl2an 597 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ ๐ผ) โ ๐ โ โ) |
121 | 120 | nnrpd 12960 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ ๐ผ) โ ๐ โ โ+) |
122 | 121 | relogcld 25994 |
. . . . . . . . 9
โข ((๐ โง ๐ โ ๐ผ) โ (logโ๐) โ โ) |
123 | 122, 120 | nndivred 12212 |
. . . . . . . 8
โข ((๐ โง ๐ โ ๐ผ) โ ((logโ๐) / ๐) โ โ) |
124 | 107, 123 | remulcld 11190 |
. . . . . . 7
โข ((๐ โง ๐ โ ๐ผ) โ ((๐ โ ๐ธ) ยท ((logโ๐) / ๐)) โ โ) |
125 | 93 | sselda 3945 |
. . . . . . . 8
โข ((๐ โง ๐ โ ๐ผ) โ ๐ โ ๐) |
126 | 125, 82 | syldan 592 |
. . . . . . 7
โข ((๐ โง ๐ โ ๐ผ) โ (((๐ / ๐) โ (absโ((๐
โ(๐ / ๐)) / ๐))) ยท (logโ๐)) โ โ) |
127 | | simpr 486 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ ๐ผ) โ ๐ โ ๐ผ) |
128 | 127, 37 | eleqtrdi 2844 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ ๐ผ) โ ๐ โ (((โโ(๐ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐))) + 1)...(โโ(๐ / ๐)))) |
129 | | elfzle2 13451 |
. . . . . . . . . . 11
โข (๐ โ (((โโ(๐ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐))) + 1)...(โโ(๐ / ๐))) โ ๐ โค (โโ(๐ / ๐))) |
130 | 128, 129 | syl 17 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ ๐ผ) โ ๐ โค (โโ(๐ / ๐))) |
131 | 45 | rpred 12962 |
. . . . . . . . . . . 12
โข (๐ โ (๐ / ๐) โ โ) |
132 | 131 | adantr 482 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ ๐ผ) โ (๐ / ๐) โ โ) |
133 | 128 | elfzelzd 13448 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ ๐ผ) โ ๐ โ โค) |
134 | | flge 13716 |
. . . . . . . . . . 11
โข (((๐ / ๐) โ โ โง ๐ โ โค) โ (๐ โค (๐ / ๐) โ ๐ โค (โโ(๐ / ๐)))) |
135 | 132, 133,
134 | syl2anc 585 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ ๐ผ) โ (๐ โค (๐ / ๐) โ ๐ โค (โโ(๐ / ๐)))) |
136 | 130, 135 | mpbird 257 |
. . . . . . . . 9
โข ((๐ โง ๐ โ ๐ผ) โ ๐ โค (๐ / ๐)) |
137 | 120 | nnred 12173 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ ๐ผ) โ ๐ โ โ) |
138 | | ere 15976 |
. . . . . . . . . . . 12
โข e โ
โ |
139 | 138 | a1i 11 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ ๐ผ) โ e โ โ) |
140 | 112 | rpred 12962 |
. . . . . . . . . . . 12
โข (๐ โ (๐ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐)) โ โ) |
141 | 140 | adantr 482 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ ๐ผ) โ (๐ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐)) โ โ) |
142 | 138 | a1i 11 |
. . . . . . . . . . . . 13
โข (๐ โ e โ
โ) |
143 | 29 | rpsqrtcld 15302 |
. . . . . . . . . . . . . 14
โข (๐ โ (โโ๐) โ
โ+) |
144 | 143 | rpred 12962 |
. . . . . . . . . . . . 13
โข (๐ โ (โโ๐) โ
โ) |
145 | 31 | simp2d 1144 |
. . . . . . . . . . . . 13
โข (๐ โ e โค
(โโ๐)) |
146 | 111 | rpred 12962 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ ((1 + (๐ฟ ยท ๐ธ)) ยท ๐) โ โ) |
147 | 60 | rpred 12962 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ (๐พโ(๐ฝ + 1)) โ โ) |
148 | 88 | simpld 496 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ ((๐พโ๐ฝ) < ๐ โง ((1 + (๐ฟ ยท ๐ธ)) ยท ๐) < (๐พ ยท (๐พโ๐ฝ)))) |
149 | 148 | simprd 497 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ ((1 + (๐ฟ ยท ๐ธ)) ยท ๐) < (๐พ ยท (๐พโ๐ฝ))) |
150 | 55 | rpcnd 12964 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ โ ๐พ โ โ) |
151 | 55, 58 | rpexpcld 14156 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ โ (๐พโ๐ฝ) โ
โ+) |
152 | 151 | rpcnd 12964 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ โ (๐พโ๐ฝ) โ โ) |
153 | 150, 152 | mulcomd 11181 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ (๐พ ยท (๐พโ๐ฝ)) = ((๐พโ๐ฝ) ยท ๐พ)) |
154 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
23, 24, 25, 26, 27, 84, 85 | pntlemg 26962 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (๐ โ (๐ โ โ โง ๐ โ (โคโฅโ๐) โง (((logโ๐) / (logโ๐พ)) / 4) โค (๐ โ ๐))) |
155 | 154 | simp1d 1143 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ โ ๐ โ โ) |
156 | | elfzouz 13582 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (๐ฝ โ (๐..^๐) โ ๐ฝ โ (โคโฅโ๐)) |
157 | 56, 156 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ โ ๐ฝ โ (โคโฅโ๐)) |
158 | | eluznn 12848 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((๐ โ โ โง ๐ฝ โ
(โคโฅโ๐)) โ ๐ฝ โ โ) |
159 | 155, 157,
158 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ โ ๐ฝ โ โ) |
160 | 159 | nnnn0d 12478 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ โ ๐ฝ โ
โ0) |
161 | 150, 160 | expp1d 14058 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ (๐พโ(๐ฝ + 1)) = ((๐พโ๐ฝ) ยท ๐พ)) |
162 | 153, 161 | eqtr4d 2776 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ (๐พ ยท (๐พโ๐ฝ)) = (๐พโ(๐ฝ + 1))) |
163 | 149, 162 | breqtrd 5132 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ ((1 + (๐ฟ ยท ๐ธ)) ยท ๐) < (๐พโ(๐ฝ + 1))) |
164 | 146, 147,
163 | ltled 11308 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ ((1 + (๐ฟ ยท ๐ธ)) ยท ๐) โค (๐พโ(๐ฝ + 1))) |
165 | | fzofzp1 13675 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ฝ โ (๐..^๐) โ (๐ฝ + 1) โ (๐...๐)) |
166 | 56, 165 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ (๐ฝ + 1) โ (๐...๐)) |
167 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
23, 24, 25, 26, 27, 84, 85 | pntlemh 26963 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง (๐ฝ + 1) โ (๐...๐)) โ (๐ < (๐พโ(๐ฝ + 1)) โง (๐พโ(๐ฝ + 1)) โค (โโ๐))) |
168 | 166, 167 | mpdan 686 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ (๐ < (๐พโ(๐ฝ + 1)) โง (๐พโ(๐ฝ + 1)) โค (โโ๐))) |
169 | 168 | simprd 497 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ (๐พโ(๐ฝ + 1)) โค (โโ๐)) |
170 | 146, 147,
144, 164, 169 | letrd 11317 |
. . . . . . . . . . . . . . . 16
โข (๐ โ ((1 + (๐ฟ ยท ๐ธ)) ยท ๐) โค (โโ๐)) |
171 | 146, 144,
143 | lemul2d 13006 |
. . . . . . . . . . . . . . . 16
โข (๐ โ (((1 + (๐ฟ ยท ๐ธ)) ยท ๐) โค (โโ๐) โ ((โโ๐) ยท ((1 + (๐ฟ ยท ๐ธ)) ยท ๐)) โค ((โโ๐) ยท (โโ๐)))) |
172 | 170, 171 | mpbid 231 |
. . . . . . . . . . . . . . 15
โข (๐ โ ((โโ๐) ยท ((1 + (๐ฟ ยท ๐ธ)) ยท ๐)) โค ((โโ๐) ยท (โโ๐))) |
173 | 29 | rprege0d 12969 |
. . . . . . . . . . . . . . . 16
โข (๐ โ (๐ โ โ โง 0 โค ๐)) |
174 | | remsqsqrt 15147 |
. . . . . . . . . . . . . . . 16
โข ((๐ โ โ โง 0 โค
๐) โ
((โโ๐) ยท
(โโ๐)) = ๐) |
175 | 173, 174 | syl 17 |
. . . . . . . . . . . . . . 15
โข (๐ โ ((โโ๐) ยท (โโ๐)) = ๐) |
176 | 172, 175 | breqtrd 5132 |
. . . . . . . . . . . . . 14
โข (๐ โ ((โโ๐) ยท ((1 + (๐ฟ ยท ๐ธ)) ยท ๐)) โค ๐) |
177 | 144, 30, 111 | lemuldivd 13011 |
. . . . . . . . . . . . . 14
โข (๐ โ (((โโ๐) ยท ((1 + (๐ฟ ยท ๐ธ)) ยท ๐)) โค ๐ โ (โโ๐) โค (๐ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐)))) |
178 | 176, 177 | mpbid 231 |
. . . . . . . . . . . . 13
โข (๐ โ (โโ๐) โค (๐ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐))) |
179 | 142, 144,
140, 145, 178 | letrd 11317 |
. . . . . . . . . . . 12
โข (๐ โ e โค (๐ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐))) |
180 | 179 | adantr 482 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ ๐ผ) โ e โค (๐ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐))) |
181 | | reflcl 13707 |
. . . . . . . . . . . . . 14
โข ((๐ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐)) โ โ โ
(โโ(๐ / ((1 +
(๐ฟ ยท ๐ธ)) ยท ๐))) โ โ) |
182 | | peano2re 11333 |
. . . . . . . . . . . . . 14
โข
((โโ(๐ /
((1 + (๐ฟ ยท ๐ธ)) ยท ๐))) โ โ โ
((โโ(๐ / ((1 +
(๐ฟ ยท ๐ธ)) ยท ๐))) + 1) โ โ) |
183 | 140, 181,
182 | 3syl 18 |
. . . . . . . . . . . . 13
โข (๐ โ ((โโ(๐ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐))) + 1) โ โ) |
184 | 183 | adantr 482 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ ๐ผ) โ ((โโ(๐ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐))) + 1) โ โ) |
185 | | fllep1 13712 |
. . . . . . . . . . . . 13
โข ((๐ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐)) โ โ โ (๐ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐)) โค ((โโ(๐ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐))) + 1)) |
186 | 141, 185 | syl 17 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ ๐ผ) โ (๐ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐)) โค ((โโ(๐ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐))) + 1)) |
187 | | elfzle1 13450 |
. . . . . . . . . . . . 13
โข (๐ โ (((โโ(๐ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐))) + 1)...(โโ(๐ / ๐))) โ ((โโ(๐ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐))) + 1) โค ๐) |
188 | 128, 187 | syl 17 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ ๐ผ) โ ((โโ(๐ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐))) + 1) โค ๐) |
189 | 141, 184,
137, 186, 188 | letrd 11317 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ ๐ผ) โ (๐ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐)) โค ๐) |
190 | 139, 141,
137, 180, 189 | letrd 11317 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ ๐ผ) โ e โค ๐) |
191 | 139, 137,
132, 190, 136 | letrd 11317 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ ๐ผ) โ e โค (๐ / ๐)) |
192 | | logdivle 25993 |
. . . . . . . . . 10
โข (((๐ โ โ โง e โค
๐) โง ((๐ / ๐) โ โ โง e โค (๐ / ๐))) โ (๐ โค (๐ / ๐) โ ((logโ(๐ / ๐)) / (๐ / ๐)) โค ((logโ๐) / ๐))) |
193 | 137, 190,
132, 191, 192 | syl22anc 838 |
. . . . . . . . 9
โข ((๐ โง ๐ โ ๐ผ) โ (๐ โค (๐ / ๐) โ ((logโ(๐ / ๐)) / (๐ / ๐)) โค ((logโ๐) / ๐))) |
194 | 136, 193 | mpbid 231 |
. . . . . . . 8
โข ((๐ โง ๐ โ ๐ผ) โ ((logโ(๐ / ๐)) / (๐ / ๐)) โค ((logโ๐) / ๐)) |
195 | 47 | adantr 482 |
. . . . . . . . 9
โข ((๐ โง ๐ โ ๐ผ) โ ((logโ(๐ / ๐)) / (๐ / ๐)) โ โ) |
196 | | lemul2 12013 |
. . . . . . . . 9
โข
((((logโ(๐ /
๐)) / (๐ / ๐)) โ โ โง ((logโ๐) / ๐) โ โ โง ((๐ โ ๐ธ) โ โ โง 0 < (๐ โ ๐ธ))) โ (((logโ(๐ / ๐)) / (๐ / ๐)) โค ((logโ๐) / ๐) โ ((๐ โ ๐ธ) ยท ((logโ(๐ / ๐)) / (๐ / ๐))) โค ((๐ โ ๐ธ) ยท ((logโ๐) / ๐)))) |
197 | 195, 123,
106, 196 | syl3anc 1372 |
. . . . . . . 8
โข ((๐ โง ๐ โ ๐ผ) โ (((logโ(๐ / ๐)) / (๐ / ๐)) โค ((logโ๐) / ๐) โ ((๐ โ ๐ธ) ยท ((logโ(๐ / ๐)) / (๐ / ๐))) โค ((๐ โ ๐ธ) ยท ((logโ๐) / ๐)))) |
198 | 194, 197 | mpbid 231 |
. . . . . . 7
โข ((๐ โง ๐ โ ๐ผ) โ ((๐ โ ๐ธ) ยท ((logโ(๐ / ๐)) / (๐ / ๐))) โค ((๐ โ ๐ธ) ยท ((logโ๐) / ๐))) |
199 | 13 | rpcnd 12964 |
. . . . . . . . . . 11
โข (๐ โ (๐ โ ๐ธ) โ โ) |
200 | 199 | adantr 482 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ ๐ผ) โ (๐ โ ๐ธ) โ โ) |
201 | 122 | recnd 11188 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ ๐ผ) โ (logโ๐) โ โ) |
202 | 121 | rpcnne0d 12971 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ ๐ผ) โ (๐ โ โ โง ๐ โ 0)) |
203 | | div23 11837 |
. . . . . . . . . 10
โข (((๐ โ ๐ธ) โ โ โง (logโ๐) โ โ โง (๐ โ โ โง ๐ โ 0)) โ (((๐ โ ๐ธ) ยท (logโ๐)) / ๐) = (((๐ โ ๐ธ) / ๐) ยท (logโ๐))) |
204 | 200, 201,
202, 203 | syl3anc 1372 |
. . . . . . . . 9
โข ((๐ โง ๐ โ ๐ผ) โ (((๐ โ ๐ธ) ยท (logโ๐)) / ๐) = (((๐ โ ๐ธ) / ๐) ยท (logโ๐))) |
205 | | divass 11836 |
. . . . . . . . . 10
โข (((๐ โ ๐ธ) โ โ โง (logโ๐) โ โ โง (๐ โ โ โง ๐ โ 0)) โ (((๐ โ ๐ธ) ยท (logโ๐)) / ๐) = ((๐ โ ๐ธ) ยท ((logโ๐) / ๐))) |
206 | 200, 201,
202, 205 | syl3anc 1372 |
. . . . . . . . 9
โข ((๐ โง ๐ โ ๐ผ) โ (((๐ โ ๐ธ) ยท (logโ๐)) / ๐) = ((๐ โ ๐ธ) ยท ((logโ๐) / ๐))) |
207 | 204, 206 | eqtr3d 2775 |
. . . . . . . 8
โข ((๐ โง ๐ โ ๐ผ) โ (((๐ โ ๐ธ) / ๐) ยท (logโ๐)) = ((๐ โ ๐ธ) ยท ((logโ๐) / ๐))) |
208 | 43 | adantr 482 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ ๐ผ) โ (๐ โ ๐ธ) โ โ) |
209 | 208, 120 | nndivred 12212 |
. . . . . . . . 9
โข ((๐ โง ๐ โ ๐ผ) โ ((๐ โ ๐ธ) / ๐) โ โ) |
210 | 125, 80 | syldan 592 |
. . . . . . . . 9
โข ((๐ โง ๐ โ ๐ผ) โ ((๐ / ๐) โ (absโ((๐
โ(๐ / ๐)) / ๐))) โ โ) |
211 | | log1 25957 |
. . . . . . . . . 10
โข
(logโ1) = 0 |
212 | 120 | nnge1d 12206 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ ๐ผ) โ 1 โค ๐) |
213 | | logleb 25974 |
. . . . . . . . . . . 12
โข ((1
โ โ+ โง ๐ โ โ+) โ (1 โค
๐ โ (logโ1) โค
(logโ๐))) |
214 | 108, 121,
213 | sylancr 588 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ ๐ผ) โ (1 โค ๐ โ (logโ1) โค (logโ๐))) |
215 | 212, 214 | mpbid 231 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ ๐ผ) โ (logโ1) โค (logโ๐)) |
216 | 211, 215 | eqbrtrrid 5142 |
. . . . . . . . 9
โข ((๐ โง ๐ โ ๐ผ) โ 0 โค (logโ๐)) |
217 | 7 | rpcnd 12964 |
. . . . . . . . . . . 12
โข (๐ โ ๐ โ โ) |
218 | 217 | adantr 482 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ ๐ผ) โ ๐ โ โ) |
219 | 16 | rpred 12962 |
. . . . . . . . . . . . 13
โข (๐ โ ๐ธ โ โ) |
220 | 219 | adantr 482 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ ๐ผ) โ ๐ธ โ โ) |
221 | 220 | recnd 11188 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ ๐ผ) โ ๐ธ โ โ) |
222 | | divsubdir 11854 |
. . . . . . . . . . 11
โข ((๐ โ โ โง ๐ธ โ โ โง (๐ โ โ โง ๐ โ 0)) โ ((๐ โ ๐ธ) / ๐) = ((๐ / ๐) โ (๐ธ / ๐))) |
223 | 218, 221,
202, 222 | syl3anc 1372 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ ๐ผ) โ ((๐ โ ๐ธ) / ๐) = ((๐ / ๐) โ (๐ธ / ๐))) |
224 | 125, 79 | syldan 592 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ ๐ผ) โ (absโ((๐
โ(๐ / ๐)) / ๐)) โ โ) |
225 | 220, 120 | nndivred 12212 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ ๐ผ) โ (๐ธ / ๐) โ โ) |
226 | 125, 70 | syldan 592 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ ๐ผ) โ (๐ / ๐) โ โ) |
227 | 125, 76 | syldan 592 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง ๐ โ ๐ผ) โ (๐
โ(๐ / ๐)) โ โ) |
228 | 227 | recnd 11188 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง ๐ โ ๐ผ) โ (๐
โ(๐ / ๐)) โ โ) |
229 | 29 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง ๐ โ ๐ผ) โ ๐ โ
โ+) |
230 | 229 | rpcnne0d 12971 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง ๐ โ ๐ผ) โ (๐ โ โ โง ๐ โ 0)) |
231 | | divdiv2 11872 |
. . . . . . . . . . . . . . . . 17
โข (((๐
โ(๐ / ๐)) โ โ โง (๐ โ โ โง ๐ โ 0) โง (๐ โ โ โง ๐ โ 0)) โ ((๐
โ(๐ / ๐)) / (๐ / ๐)) = (((๐
โ(๐ / ๐)) ยท ๐) / ๐)) |
232 | 228, 230,
202, 231 | syl3anc 1372 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ โ ๐ผ) โ ((๐
โ(๐ / ๐)) / (๐ / ๐)) = (((๐
โ(๐ / ๐)) ยท ๐) / ๐)) |
233 | 121 | rpcnd 12964 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง ๐ โ ๐ผ) โ ๐ โ โ) |
234 | | div23 11837 |
. . . . . . . . . . . . . . . . 17
โข (((๐
โ(๐ / ๐)) โ โ โง ๐ โ โ โง (๐ โ โ โง ๐ โ 0)) โ (((๐
โ(๐ / ๐)) ยท ๐) / ๐) = (((๐
โ(๐ / ๐)) / ๐) ยท ๐)) |
235 | 228, 233,
230, 234 | syl3anc 1372 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ โ ๐ผ) โ (((๐
โ(๐ / ๐)) ยท ๐) / ๐) = (((๐
โ(๐ / ๐)) / ๐) ยท ๐)) |
236 | 232, 235 | eqtrd 2773 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ โ ๐ผ) โ ((๐
โ(๐ / ๐)) / (๐ / ๐)) = (((๐
โ(๐ / ๐)) / ๐) ยท ๐)) |
237 | 236 | fveq2d 6847 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ โ ๐ผ) โ (absโ((๐
โ(๐ / ๐)) / (๐ / ๐))) = (absโ(((๐
โ(๐ / ๐)) / ๐) ยท ๐))) |
238 | 125, 78 | syldan 592 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ โ ๐ผ) โ ((๐
โ(๐ / ๐)) / ๐) โ โ) |
239 | 238, 233 | absmuld 15345 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ โ ๐ผ) โ (absโ(((๐
โ(๐ / ๐)) / ๐) ยท ๐)) = ((absโ((๐
โ(๐ / ๐)) / ๐)) ยท (absโ๐))) |
240 | 121 | rprege0d 12969 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ โ ๐ผ) โ (๐ โ โ โง 0 โค ๐)) |
241 | | absid 15187 |
. . . . . . . . . . . . . . . 16
โข ((๐ โ โ โง 0 โค
๐) โ (absโ๐) = ๐) |
242 | 240, 241 | syl 17 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ โ ๐ผ) โ (absโ๐) = ๐) |
243 | 242 | oveq2d 7374 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ โ ๐ผ) โ ((absโ((๐
โ(๐ / ๐)) / ๐)) ยท (absโ๐)) = ((absโ((๐
โ(๐ / ๐)) / ๐)) ยท ๐)) |
244 | 237, 239,
243 | 3eqtrd 2777 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ โ ๐ผ) โ (absโ((๐
โ(๐ / ๐)) / (๐ / ๐))) = ((absโ((๐
โ(๐ / ๐)) / ๐)) ยท ๐)) |
245 | | fveq2 6843 |
. . . . . . . . . . . . . . . . 17
โข (๐ข = (๐ / ๐) โ (๐
โ๐ข) = (๐
โ(๐ / ๐))) |
246 | | id 22 |
. . . . . . . . . . . . . . . . 17
โข (๐ข = (๐ / ๐) โ ๐ข = (๐ / ๐)) |
247 | 245, 246 | oveq12d 7376 |
. . . . . . . . . . . . . . . 16
โข (๐ข = (๐ / ๐) โ ((๐
โ๐ข) / ๐ข) = ((๐
โ(๐ / ๐)) / (๐ / ๐))) |
248 | 247 | fveq2d 6847 |
. . . . . . . . . . . . . . 15
โข (๐ข = (๐ / ๐) โ (absโ((๐
โ๐ข) / ๐ข)) = (absโ((๐
โ(๐ / ๐)) / (๐ / ๐)))) |
249 | 248 | breq1d 5116 |
. . . . . . . . . . . . . 14
โข (๐ข = (๐ / ๐) โ ((absโ((๐
โ๐ข) / ๐ข)) โค ๐ธ โ (absโ((๐
โ(๐ / ๐)) / (๐ / ๐))) โค ๐ธ)) |
250 | 88 | simprd 497 |
. . . . . . . . . . . . . . 15
โข (๐ โ โ๐ข โ (๐[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐))(absโ((๐
โ๐ข) / ๐ข)) โค ๐ธ) |
251 | 250 | adantr 482 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ โ ๐ผ) โ โ๐ข โ (๐[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐))(absโ((๐
โ๐ข) / ๐ข)) โค ๐ธ) |
252 | 30 | adantr 482 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ โ ๐ผ) โ ๐ โ โ) |
253 | 252, 120 | nndivred 12212 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ โ ๐ผ) โ (๐ / ๐) โ โ) |
254 | 44 | rpregt0d 12968 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ (๐ โ โ โง 0 < ๐)) |
255 | 254 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง ๐ โ ๐ผ) โ (๐ โ โ โง 0 < ๐)) |
256 | | lemuldiv2 12041 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โ โ โง ๐ โ โ โง (๐ โ โ โง 0 <
๐)) โ ((๐ ยท ๐) โค ๐ โ ๐ โค (๐ / ๐))) |
257 | 137, 252,
255, 256 | syl3anc 1372 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง ๐ โ ๐ผ) โ ((๐ ยท ๐) โค ๐ โ ๐ โค (๐ / ๐))) |
258 | 136, 257 | mpbird 257 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ โ ๐ผ) โ (๐ ยท ๐) โค ๐) |
259 | 255 | simpld 496 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง ๐ โ ๐ผ) โ ๐ โ โ) |
260 | 259, 252,
121 | lemuldivd 13011 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ โ ๐ผ) โ ((๐ ยท ๐) โค ๐ โ ๐ โค (๐ / ๐))) |
261 | 258, 260 | mpbid 231 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ โ ๐ผ) โ ๐ โค (๐ / ๐)) |
262 | 111 | rpregt0d 12968 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ (((1 + (๐ฟ ยท ๐ธ)) ยท ๐) โ โ โง 0 < ((1 + (๐ฟ ยท ๐ธ)) ยท ๐))) |
263 | 262 | adantr 482 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง ๐ โ ๐ผ) โ (((1 + (๐ฟ ยท ๐ธ)) ยท ๐) โ โ โง 0 < ((1 + (๐ฟ ยท ๐ธ)) ยท ๐))) |
264 | 121 | rpregt0d 12968 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง ๐ โ ๐ผ) โ (๐ โ โ โง 0 < ๐)) |
265 | | lediv23 12052 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โ โ โง (((1 +
(๐ฟ ยท ๐ธ)) ยท ๐) โ โ โง 0 < ((1 + (๐ฟ ยท ๐ธ)) ยท ๐)) โง (๐ โ โ โง 0 < ๐)) โ ((๐ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐)) โค ๐ โ (๐ / ๐) โค ((1 + (๐ฟ ยท ๐ธ)) ยท ๐))) |
266 | 252, 263,
264, 265 | syl3anc 1372 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ โ ๐ผ) โ ((๐ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐)) โค ๐ โ (๐ / ๐) โค ((1 + (๐ฟ ยท ๐ธ)) ยท ๐))) |
267 | 189, 266 | mpbid 231 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ โ ๐ผ) โ (๐ / ๐) โค ((1 + (๐ฟ ยท ๐ธ)) ยท ๐)) |
268 | 44 | rpred 12962 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ ๐ โ โ) |
269 | 268 | adantr 482 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ โ ๐ผ) โ ๐ โ โ) |
270 | 146 | adantr 482 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ โ ๐ผ) โ ((1 + (๐ฟ ยท ๐ธ)) ยท ๐) โ โ) |
271 | | elicc2 13335 |
. . . . . . . . . . . . . . . 16
โข ((๐ โ โ โง ((1 +
(๐ฟ ยท ๐ธ)) ยท ๐) โ โ) โ ((๐ / ๐) โ (๐[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐)) โ ((๐ / ๐) โ โ โง ๐ โค (๐ / ๐) โง (๐ / ๐) โค ((1 + (๐ฟ ยท ๐ธ)) ยท ๐)))) |
272 | 269, 270,
271 | syl2anc 585 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ โ ๐ผ) โ ((๐ / ๐) โ (๐[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐)) โ ((๐ / ๐) โ โ โง ๐ โค (๐ / ๐) โง (๐ / ๐) โค ((1 + (๐ฟ ยท ๐ธ)) ยท ๐)))) |
273 | 253, 261,
267, 272 | mpbir3and 1343 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ โ ๐ผ) โ (๐ / ๐) โ (๐[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐))) |
274 | 249, 251,
273 | rspcdva 3581 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ โ ๐ผ) โ (absโ((๐
โ(๐ / ๐)) / (๐ / ๐))) โค ๐ธ) |
275 | 244, 274 | eqbrtrrd 5130 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ ๐ผ) โ ((absโ((๐
โ(๐ / ๐)) / ๐)) ยท ๐) โค ๐ธ) |
276 | 224, 220,
121 | lemuldivd 13011 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ ๐ผ) โ (((absโ((๐
โ(๐ / ๐)) / ๐)) ยท ๐) โค ๐ธ โ (absโ((๐
โ(๐ / ๐)) / ๐)) โค (๐ธ / ๐))) |
277 | 275, 276 | mpbid 231 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ ๐ผ) โ (absโ((๐
โ(๐ / ๐)) / ๐)) โค (๐ธ / ๐)) |
278 | 224, 225,
226, 277 | lesub2dd 11777 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ ๐ผ) โ ((๐ / ๐) โ (๐ธ / ๐)) โค ((๐ / ๐) โ (absโ((๐
โ(๐ / ๐)) / ๐)))) |
279 | 223, 278 | eqbrtrd 5128 |
. . . . . . . . 9
โข ((๐ โง ๐ โ ๐ผ) โ ((๐ โ ๐ธ) / ๐) โค ((๐ / ๐) โ (absโ((๐
โ(๐ / ๐)) / ๐)))) |
280 | 209, 210,
122, 216, 279 | lemul1ad 12099 |
. . . . . . . 8
โข ((๐ โง ๐ โ ๐ผ) โ (((๐ โ ๐ธ) / ๐) ยท (logโ๐)) โค (((๐ / ๐) โ (absโ((๐
โ(๐ / ๐)) / ๐))) ยท (logโ๐))) |
281 | 207, 280 | eqbrtrrd 5130 |
. . . . . . 7
โข ((๐ โง ๐ โ ๐ผ) โ ((๐ โ ๐ธ) ยท ((logโ๐) / ๐)) โค (((๐ / ๐) โ (absโ((๐
โ(๐ / ๐)) / ๐))) ยท (logโ๐))) |
282 | 99, 124, 126, 198, 281 | letrd 11317 |
. . . . . 6
โข ((๐ โง ๐ โ ๐ผ) โ ((๐ โ ๐ธ) ยท ((logโ(๐ / ๐)) / (๐ / ๐))) โค (((๐ / ๐) โ (absโ((๐
โ(๐ / ๐)) / ๐))) ยท (logโ๐))) |
283 | 282 | adantlr 714 |
. . . . 5
โข (((๐ โง ๐ โ ๐) โง ๐ โ ๐ผ) โ ((๐ โ ๐ธ) ยท ((logโ(๐ / ๐)) / (๐ / ๐))) โค (((๐ / ๐) โ (absโ((๐
โ(๐ / ๐)) / ๐))) ยท (logโ๐))) |
284 | 69 | nnred 12173 |
. . . . . . . . 9
โข ((๐ โง ๐ โ ๐) โ ๐ โ โ) |
285 | 29, 151 | rpdivcld 12979 |
. . . . . . . . . . 11
โข (๐ โ (๐ / (๐พโ๐ฝ)) โ
โ+) |
286 | 285 | rpred 12962 |
. . . . . . . . . 10
โข (๐ โ (๐ / (๐พโ๐ฝ)) โ โ) |
287 | 286 | adantr 482 |
. . . . . . . . 9
โข ((๐ โง ๐ โ ๐) โ (๐ / (๐พโ๐ฝ)) โ โ) |
288 | 23 | simpld 496 |
. . . . . . . . . . . 12
โข (๐ โ ๐ โ
โ+) |
289 | 29, 288 | rpdivcld 12979 |
. . . . . . . . . . 11
โข (๐ โ (๐ / ๐) โ
โ+) |
290 | 289 | rpred 12962 |
. . . . . . . . . 10
โข (๐ โ (๐ / ๐) โ โ) |
291 | 290 | adantr 482 |
. . . . . . . . 9
โข ((๐ โง ๐ โ ๐) โ (๐ / ๐) โ โ) |
292 | | simpr 486 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ ๐) โ ๐ โ ๐) |
293 | 292, 50 | eleqtrdi 2844 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ ๐) โ ๐ โ (((โโ(๐ / (๐พโ(๐ฝ + 1)))) + 1)...(โโ(๐ / (๐พโ๐ฝ))))) |
294 | | elfzle2 13451 |
. . . . . . . . . . 11
โข (๐ โ (((โโ(๐ / (๐พโ(๐ฝ + 1)))) + 1)...(โโ(๐ / (๐พโ๐ฝ)))) โ ๐ โค (โโ(๐ / (๐พโ๐ฝ)))) |
295 | 293, 294 | syl 17 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ ๐) โ ๐ โค (โโ(๐ / (๐พโ๐ฝ)))) |
296 | 69 | nnzd 12531 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ ๐) โ ๐ โ โค) |
297 | | flge 13716 |
. . . . . . . . . . 11
โข (((๐ / (๐พโ๐ฝ)) โ โ โง ๐ โ โค) โ (๐ โค (๐ / (๐พโ๐ฝ)) โ ๐ โค (โโ(๐ / (๐พโ๐ฝ))))) |
298 | 287, 296,
297 | syl2anc 585 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ ๐) โ (๐ โค (๐ / (๐พโ๐ฝ)) โ ๐ โค (โโ(๐ / (๐พโ๐ฝ))))) |
299 | 295, 298 | mpbird 257 |
. . . . . . . . 9
โข ((๐ โง ๐ โ ๐) โ ๐ โค (๐ / (๐พโ๐ฝ))) |
300 | 288 | rpred 12962 |
. . . . . . . . . . . 12
โข (๐ โ ๐ โ โ) |
301 | 24 | simpld 496 |
. . . . . . . . . . . . 13
โข (๐ โ ๐ โ
โ+) |
302 | 301 | rpred 12962 |
. . . . . . . . . . . 12
โข (๐ โ ๐ โ โ) |
303 | 151 | rpred 12962 |
. . . . . . . . . . . 12
โข (๐ โ (๐พโ๐ฝ) โ โ) |
304 | 24 | simprd 497 |
. . . . . . . . . . . . 13
โข (๐ โ ๐ < ๐) |
305 | 300, 302,
304 | ltled 11308 |
. . . . . . . . . . . 12
โข (๐ โ ๐ โค ๐) |
306 | | elfzofz 13594 |
. . . . . . . . . . . . . . . 16
โข (๐ฝ โ (๐..^๐) โ ๐ฝ โ (๐...๐)) |
307 | 56, 306 | syl 17 |
. . . . . . . . . . . . . . 15
โข (๐ โ ๐ฝ โ (๐...๐)) |
308 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
23, 24, 25, 26, 27, 84, 85 | pntlemh 26963 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ฝ โ (๐...๐)) โ (๐ < (๐พโ๐ฝ) โง (๐พโ๐ฝ) โค (โโ๐))) |
309 | 307, 308 | mpdan 686 |
. . . . . . . . . . . . . 14
โข (๐ โ (๐ < (๐พโ๐ฝ) โง (๐พโ๐ฝ) โค (โโ๐))) |
310 | 309 | simpld 496 |
. . . . . . . . . . . . 13
โข (๐ โ ๐ < (๐พโ๐ฝ)) |
311 | 302, 303,
310 | ltled 11308 |
. . . . . . . . . . . 12
โข (๐ โ ๐ โค (๐พโ๐ฝ)) |
312 | 300, 302,
303, 305, 311 | letrd 11317 |
. . . . . . . . . . 11
โข (๐ โ ๐ โค (๐พโ๐ฝ)) |
313 | 288, 151,
29 | lediv2d 12986 |
. . . . . . . . . . 11
โข (๐ โ (๐ โค (๐พโ๐ฝ) โ (๐ / (๐พโ๐ฝ)) โค (๐ / ๐))) |
314 | 312, 313 | mpbid 231 |
. . . . . . . . . 10
โข (๐ โ (๐ / (๐พโ๐ฝ)) โค (๐ / ๐)) |
315 | 314 | adantr 482 |
. . . . . . . . 9
โข ((๐ โง ๐ โ ๐) โ (๐ / (๐พโ๐ฝ)) โค (๐ / ๐)) |
316 | 284, 287,
291, 299, 315 | letrd 11317 |
. . . . . . . 8
โข ((๐ โง ๐ โ ๐) โ ๐ โค (๐ / ๐)) |
317 | 69, 316 | jca 513 |
. . . . . . 7
โข ((๐ โง ๐ โ ๐) โ (๐ โ โ โง ๐ โค (๐ / ๐))) |
318 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
23, 24, 25, 26, 27, 84, 85, 86 | pntlemn 26964 |
. . . . . . 7
โข ((๐ โง (๐ โ โ โง ๐ โค (๐ / ๐))) โ 0 โค (((๐ / ๐) โ (absโ((๐
โ(๐ / ๐)) / ๐))) ยท (logโ๐))) |
319 | 317, 318 | syldan 592 |
. . . . . 6
โข ((๐ โง ๐ โ ๐) โ 0 โค (((๐ / ๐) โ (absโ((๐
โ(๐ / ๐)) / ๐))) ยท (logโ๐))) |
320 | 319 | adantr 482 |
. . . . 5
โข (((๐ โง ๐ โ ๐) โง ยฌ ๐ โ ๐ผ) โ 0 โค (((๐ / ๐) โ (absโ((๐
โ(๐ / ๐)) / ๐))) ยท (logโ๐))) |
321 | 103, 104,
283, 320 | ifbothda 4525 |
. . . 4
โข ((๐ โง ๐ โ ๐) โ if(๐ โ ๐ผ, ((๐ โ ๐ธ) ยท ((logโ(๐ / ๐)) / (๐ / ๐))), 0) โค (((๐ / ๐) โ (absโ((๐
โ(๐ / ๐)) / ๐))) ยท (logโ๐))) |
322 | 52, 102, 82, 321 | fsumle 15689 |
. . 3
โข (๐ โ ฮฃ๐ โ ๐ if(๐ โ ๐ผ, ((๐ โ ๐ธ) ยท ((logโ(๐ / ๐)) / (๐ / ๐))), 0) โค ฮฃ๐ โ ๐ (((๐ / ๐) โ (absโ((๐
โ(๐ / ๐)) / ๐))) ยท (logโ๐))) |
323 | 98, 322 | eqbrtrd 5128 |
. 2
โข (๐ โ ((โฏโ๐ผ) ยท ((๐ โ ๐ธ) ยท ((logโ(๐ / ๐)) / (๐ / ๐)))) โค ฮฃ๐ โ ๐ (((๐ / ๐) โ (absโ((๐
โ(๐ / ๐)) / ๐))) ยท (logโ๐))) |
324 | 36, 49, 83, 89, 323 | letrd 11317 |
1
โข (๐ โ ((๐ โ ๐ธ) ยท (((๐ฟ ยท ๐ธ) / 8) ยท (logโ๐))) โค ฮฃ๐ โ ๐ (((๐ / ๐) โ (absโ((๐
โ(๐ / ๐)) / ๐))) ยท (logโ๐))) |