Step | Hyp | Ref
| Expression |
1 | | pntlem1.r |
. . . . . . . . . . . . 13
โข ๐
= (๐ โ โ+ โฆ
((ฯโ๐) โ
๐)) |
2 | | pntlem1.a |
. . . . . . . . . . . . 13
โข (๐ โ ๐ด โ
โ+) |
3 | | pntlem1.b |
. . . . . . . . . . . . 13
โข (๐ โ ๐ต โ
โ+) |
4 | | pntlem1.l |
. . . . . . . . . . . . 13
โข (๐ โ ๐ฟ โ (0(,)1)) |
5 | | pntlem1.d |
. . . . . . . . . . . . 13
โข ๐ท = (๐ด + 1) |
6 | | pntlem1.f |
. . . . . . . . . . . . 13
โข ๐น = ((1 โ (1 / ๐ท)) ยท ((๐ฟ / (;32 ยท ๐ต)) / (๐ทโ2))) |
7 | 1, 2, 3, 4, 5, 6 | pntlemd 26958 |
. . . . . . . . . . . 12
โข (๐ โ (๐ฟ โ โ+ โง ๐ท โ โ+
โง ๐น โ
โ+)) |
8 | 7 | simp1d 1143 |
. . . . . . . . . . 11
โข (๐ โ ๐ฟ โ
โ+) |
9 | | pntlem1.u |
. . . . . . . . . . . . 13
โข (๐ โ ๐ โ
โ+) |
10 | | pntlem1.u2 |
. . . . . . . . . . . . 13
โข (๐ โ ๐ โค ๐ด) |
11 | | pntlem1.e |
. . . . . . . . . . . . 13
โข ๐ธ = (๐ / ๐ท) |
12 | | pntlem1.k |
. . . . . . . . . . . . 13
โข ๐พ = (expโ(๐ต / ๐ธ)) |
13 | 1, 2, 3, 4, 5, 6, 9, 10, 11, 12 | pntlemc 26959 |
. . . . . . . . . . . 12
โข (๐ โ (๐ธ โ โ+ โง ๐พ โ โ+
โง (๐ธ โ (0(,)1)
โง 1 < ๐พ โง (๐ โ ๐ธ) โ
โ+))) |
14 | 13 | simp1d 1143 |
. . . . . . . . . . 11
โข (๐ โ ๐ธ โ
โ+) |
15 | 8, 14 | rpmulcld 12978 |
. . . . . . . . . 10
โข (๐ โ (๐ฟ ยท ๐ธ) โ
โ+) |
16 | | 4re 12242 |
. . . . . . . . . . 11
โข 4 โ
โ |
17 | | 4pos 12265 |
. . . . . . . . . . 11
โข 0 <
4 |
18 | 16, 17 | elrpii 12923 |
. . . . . . . . . 10
โข 4 โ
โ+ |
19 | | rpdivcl 12945 |
. . . . . . . . . 10
โข (((๐ฟ ยท ๐ธ) โ โ+ โง 4 โ
โ+) โ ((๐ฟ ยท ๐ธ) / 4) โ
โ+) |
20 | 15, 18, 19 | sylancl 587 |
. . . . . . . . 9
โข (๐ โ ((๐ฟ ยท ๐ธ) / 4) โ
โ+) |
21 | 20 | rpred 12962 |
. . . . . . . 8
โข (๐ โ ((๐ฟ ยท ๐ธ) / 4) โ โ) |
22 | | pntlem1.y |
. . . . . . . . . . . 12
โข (๐ โ (๐ โ โ+ โง 1 โค
๐)) |
23 | | pntlem1.x |
. . . . . . . . . . . 12
โข (๐ โ (๐ โ โ+ โง ๐ < ๐)) |
24 | | pntlem1.c |
. . . . . . . . . . . 12
โข (๐ โ ๐ถ โ
โ+) |
25 | | pntlem1.w |
. . . . . . . . . . . 12
โข ๐ = (((๐ + (4 / (๐ฟ ยท ๐ธ)))โ2) + (((๐ ยท (๐พโ2))โ4) + (expโ(((;32 ยท ๐ต) / ((๐ โ ๐ธ) ยท (๐ฟ ยท (๐ธโ2)))) ยท ((๐ ยท 3) + ๐ถ))))) |
26 | | pntlem1.z |
. . . . . . . . . . . 12
โข (๐ โ ๐ โ (๐[,)+โ)) |
27 | 1, 2, 3, 4, 5, 6, 9, 10, 11, 12, 22, 23, 24, 25, 26 | pntlemb 26961 |
. . . . . . . . . . 11
โข (๐ โ (๐ โ โ+ โง (1 <
๐ โง e โค
(โโ๐) โง
(โโ๐) โค
(๐ / ๐)) โง ((4 / (๐ฟ ยท ๐ธ)) โค (โโ๐) โง (((logโ๐) / (logโ๐พ)) + 2) โค (((logโ๐) / (logโ๐พ)) / 4) โง ((๐ ยท 3) + ๐ถ) โค (((๐ โ ๐ธ) ยท ((๐ฟ ยท (๐ธโ2)) / (;32 ยท ๐ต))) ยท (logโ๐))))) |
28 | 27 | simp1d 1143 |
. . . . . . . . . 10
โข (๐ โ ๐ โ
โ+) |
29 | | pntlem1.v |
. . . . . . . . . 10
โข (๐ โ ๐ โ
โ+) |
30 | 28, 29 | rpdivcld 12979 |
. . . . . . . . 9
โข (๐ โ (๐ / ๐) โ
โ+) |
31 | 30 | rpred 12962 |
. . . . . . . 8
โข (๐ โ (๐ / ๐) โ โ) |
32 | 21, 31 | remulcld 11190 |
. . . . . . 7
โข (๐ โ (((๐ฟ ยท ๐ธ) / 4) ยท (๐ / ๐)) โ โ) |
33 | | pntlem1.i |
. . . . . . . . . 10
โข ๐ผ = (((โโ(๐ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐))) + 1)...(โโ(๐ / ๐))) |
34 | | fzfid 13884 |
. . . . . . . . . 10
โข (๐ โ (((โโ(๐ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐))) + 1)...(โโ(๐ / ๐))) โ Fin) |
35 | 33, 34 | eqeltrid 2838 |
. . . . . . . . 9
โข (๐ โ ๐ผ โ Fin) |
36 | | hashcl 14262 |
. . . . . . . . 9
โข (๐ผ โ Fin โ
(โฏโ๐ผ) โ
โ0) |
37 | 35, 36 | syl 17 |
. . . . . . . 8
โข (๐ โ (โฏโ๐ผ) โ
โ0) |
38 | 37 | nn0red 12479 |
. . . . . . 7
โข (๐ โ (โฏโ๐ผ) โ
โ) |
39 | 32 | recnd 11188 |
. . . . . . . . . . . 12
โข (๐ โ (((๐ฟ ยท ๐ธ) / 4) ยท (๐ / ๐)) โ โ) |
40 | | 1rp 12924 |
. . . . . . . . . . . . . . . . . 18
โข 1 โ
โ+ |
41 | | rpaddcl 12942 |
. . . . . . . . . . . . . . . . . 18
โข ((1
โ โ+ โง (๐ฟ ยท ๐ธ) โ โ+) โ (1 +
(๐ฟ ยท ๐ธ)) โ
โ+) |
42 | 40, 15, 41 | sylancr 588 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ (1 + (๐ฟ ยท ๐ธ)) โ
โ+) |
43 | 42, 29 | rpmulcld 12978 |
. . . . . . . . . . . . . . . 16
โข (๐ โ ((1 + (๐ฟ ยท ๐ธ)) ยท ๐) โ
โ+) |
44 | 28, 43 | rpdivcld 12979 |
. . . . . . . . . . . . . . 15
โข (๐ โ (๐ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐)) โ
โ+) |
45 | 44 | rpred 12962 |
. . . . . . . . . . . . . 14
โข (๐ โ (๐ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐)) โ โ) |
46 | | reflcl 13707 |
. . . . . . . . . . . . . 14
โข ((๐ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐)) โ โ โ
(โโ(๐ / ((1 +
(๐ฟ ยท ๐ธ)) ยท ๐))) โ โ) |
47 | 45, 46 | syl 17 |
. . . . . . . . . . . . 13
โข (๐ โ (โโ(๐ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐))) โ โ) |
48 | 47 | recnd 11188 |
. . . . . . . . . . . 12
โข (๐ โ (โโ(๐ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐))) โ โ) |
49 | | 1cnd 11155 |
. . . . . . . . . . . 12
โข (๐ โ 1 โ
โ) |
50 | 39, 48, 49 | add32d 11387 |
. . . . . . . . . . 11
โข (๐ โ (((((๐ฟ ยท ๐ธ) / 4) ยท (๐ / ๐)) + (โโ(๐ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐)))) + 1) = (((((๐ฟ ยท ๐ธ) / 4) ยท (๐ / ๐)) + 1) + (โโ(๐ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐))))) |
51 | | peano2re 11333 |
. . . . . . . . . . . . . 14
โข ((((๐ฟ ยท ๐ธ) / 4) ยท (๐ / ๐)) โ โ โ ((((๐ฟ ยท ๐ธ) / 4) ยท (๐ / ๐)) + 1) โ โ) |
52 | 32, 51 | syl 17 |
. . . . . . . . . . . . 13
โข (๐ โ ((((๐ฟ ยท ๐ธ) / 4) ยท (๐ / ๐)) + 1) โ โ) |
53 | 52, 47 | readdcld 11189 |
. . . . . . . . . . . 12
โข (๐ โ (((((๐ฟ ยท ๐ธ) / 4) ยท (๐ / ๐)) + 1) + (โโ(๐ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐)))) โ โ) |
54 | | reflcl 13707 |
. . . . . . . . . . . . . 14
โข ((๐ / ๐) โ โ โ
(โโ(๐ / ๐)) โ
โ) |
55 | 31, 54 | syl 17 |
. . . . . . . . . . . . 13
โข (๐ โ (โโ(๐ / ๐)) โ โ) |
56 | | peano2re 11333 |
. . . . . . . . . . . . 13
โข
((โโ(๐ /
๐)) โ โ โ
((โโ(๐ / ๐)) + 1) โ
โ) |
57 | 55, 56 | syl 17 |
. . . . . . . . . . . 12
โข (๐ โ ((โโ(๐ / ๐)) + 1) โ โ) |
58 | 15 | rphalfcld 12974 |
. . . . . . . . . . . . . . . 16
โข (๐ โ ((๐ฟ ยท ๐ธ) / 2) โ
โ+) |
59 | 58, 30 | rpmulcld 12978 |
. . . . . . . . . . . . . . 15
โข (๐ โ (((๐ฟ ยท ๐ธ) / 2) ยท (๐ / ๐)) โ
โ+) |
60 | 59 | rpred 12962 |
. . . . . . . . . . . . . 14
โข (๐ โ (((๐ฟ ยท ๐ธ) / 2) ยท (๐ / ๐)) โ โ) |
61 | 60, 45 | readdcld 11189 |
. . . . . . . . . . . . 13
โข (๐ โ ((((๐ฟ ยท ๐ธ) / 2) ยท (๐ / ๐)) + (๐ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐))) โ โ) |
62 | | rpdivcl 12945 |
. . . . . . . . . . . . . . . . . . . 20
โข ((4
โ โ+ โง (๐ฟ ยท ๐ธ) โ โ+) โ (4 /
(๐ฟ ยท ๐ธ)) โ
โ+) |
63 | 18, 15, 62 | sylancr 588 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ (4 / (๐ฟ ยท ๐ธ)) โ
โ+) |
64 | 63 | rpred 12962 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ (4 / (๐ฟ ยท ๐ธ)) โ โ) |
65 | 28 | rpsqrtcld 15302 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ (โโ๐) โ
โ+) |
66 | 65 | rpred 12962 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ (โโ๐) โ
โ) |
67 | 27 | simp3d 1145 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ ((4 / (๐ฟ ยท ๐ธ)) โค (โโ๐) โง (((logโ๐) / (logโ๐พ)) + 2) โค (((logโ๐) / (logโ๐พ)) / 4) โง ((๐ ยท 3) + ๐ถ) โค (((๐ โ ๐ธ) ยท ((๐ฟ ยท (๐ธโ2)) / (;32 ยท ๐ต))) ยท (logโ๐)))) |
68 | 67 | simp1d 1143 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ (4 / (๐ฟ ยท ๐ธ)) โค (โโ๐)) |
69 | 43 | rpred 12962 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (๐ โ ((1 + (๐ฟ ยท ๐ธ)) ยท ๐) โ โ) |
70 | 13 | simp2d 1144 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข (๐ โ ๐พ โ
โ+) |
71 | | pntlem1.j |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข (๐ โ ๐ฝ โ (๐..^๐)) |
72 | | elfzoelz 13578 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข (๐ฝ โ (๐..^๐) โ ๐ฝ โ โค) |
73 | 71, 72 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข (๐ โ ๐ฝ โ โค) |
74 | 73 | peano2zd 12615 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข (๐ โ (๐ฝ + 1) โ โค) |
75 | 70, 74 | rpexpcld 14156 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (๐ โ (๐พโ(๐ฝ + 1)) โ
โ+) |
76 | 75 | rpred 12962 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (๐ โ (๐พโ(๐ฝ + 1)) โ โ) |
77 | | pntlem1.V |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข (๐ โ (((๐พโ๐ฝ) < ๐ โง ((1 + (๐ฟ ยท ๐ธ)) ยท ๐) < (๐พ ยท (๐พโ๐ฝ))) โง โ๐ข โ (๐[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐))(absโ((๐
โ๐ข) / ๐ข)) โค ๐ธ)) |
78 | 77 | simplrd 769 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข (๐ โ ((1 + (๐ฟ ยท ๐ธ)) ยท ๐) < (๐พ ยท (๐พโ๐ฝ))) |
79 | 70 | rpcnd 12964 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข (๐ โ ๐พ โ โ) |
80 | 70, 73 | rpexpcld 14156 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
โข (๐ โ (๐พโ๐ฝ) โ
โ+) |
81 | 80 | rpcnd 12964 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข (๐ โ (๐พโ๐ฝ) โ โ) |
82 | 79, 81 | mulcomd 11181 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข (๐ โ (๐พ ยท (๐พโ๐ฝ)) = ((๐พโ๐ฝ) ยท ๐พ)) |
83 | | pntlem1.m |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
โข ๐ =
((โโ((logโ๐) / (logโ๐พ))) + 1) |
84 | | pntlem1.n |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
โข ๐ =
(โโ(((logโ๐) / (logโ๐พ)) / 2)) |
85 | 1, 2, 3, 4, 5, 6, 9, 10, 11, 12, 22, 23, 24, 25, 26, 83, 84 | pntlemg 26962 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
โข (๐ โ (๐ โ โ โง ๐ โ (โคโฅโ๐) โง (((logโ๐) / (logโ๐พ)) / 4) โค (๐ โ ๐))) |
86 | 85 | simp1d 1143 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
โข (๐ โ ๐ โ โ) |
87 | | elfzouz 13582 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
โข (๐ฝ โ (๐..^๐) โ ๐ฝ โ (โคโฅโ๐)) |
88 | 71, 87 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
โข (๐ โ ๐ฝ โ (โคโฅโ๐)) |
89 | | eluznn 12848 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
โข ((๐ โ โ โง ๐ฝ โ
(โคโฅโ๐)) โ ๐ฝ โ โ) |
90 | 86, 88, 89 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
โข (๐ โ ๐ฝ โ โ) |
91 | 90 | nnnn0d 12478 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข (๐ โ ๐ฝ โ
โ0) |
92 | 79, 91 | expp1d 14058 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข (๐ โ (๐พโ(๐ฝ + 1)) = ((๐พโ๐ฝ) ยท ๐พ)) |
93 | 82, 92 | eqtr4d 2776 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข (๐ โ (๐พ ยท (๐พโ๐ฝ)) = (๐พโ(๐ฝ + 1))) |
94 | 78, 93 | breqtrd 5132 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (๐ โ ((1 + (๐ฟ ยท ๐ธ)) ยท ๐) < (๐พโ(๐ฝ + 1))) |
95 | 69, 76, 94 | ltled 11308 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (๐ โ ((1 + (๐ฟ ยท ๐ธ)) ยท ๐) โค (๐พโ(๐ฝ + 1))) |
96 | | fzofzp1 13675 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข (๐ฝ โ (๐..^๐) โ (๐ฝ + 1) โ (๐...๐)) |
97 | 71, 96 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข (๐ โ (๐ฝ + 1) โ (๐...๐)) |
98 | 1, 2, 3, 4, 5, 6, 9, 10, 11, 12, 22, 23, 24, 25, 26, 83, 84 | pntlemh 26963 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข ((๐ โง (๐ฝ + 1) โ (๐...๐)) โ (๐ < (๐พโ(๐ฝ + 1)) โง (๐พโ(๐ฝ + 1)) โค (โโ๐))) |
99 | 97, 98 | mpdan 686 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (๐ โ (๐ < (๐พโ(๐ฝ + 1)) โง (๐พโ(๐ฝ + 1)) โค (โโ๐))) |
100 | 99 | simprd 497 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (๐ โ (๐พโ(๐ฝ + 1)) โค (โโ๐)) |
101 | 69, 76, 66, 95, 100 | letrd 11317 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ โ ((1 + (๐ฟ ยท ๐ธ)) ยท ๐) โค (โโ๐)) |
102 | 69, 66, 65 | lemul2d 13006 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ โ (((1 + (๐ฟ ยท ๐ธ)) ยท ๐) โค (โโ๐) โ ((โโ๐) ยท ((1 + (๐ฟ ยท ๐ธ)) ยท ๐)) โค ((โโ๐) ยท (โโ๐)))) |
103 | 101, 102 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ โ ((โโ๐) ยท ((1 + (๐ฟ ยท ๐ธ)) ยท ๐)) โค ((โโ๐) ยท (โโ๐))) |
104 | 28 | rprege0d 12969 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ โ (๐ โ โ โง 0 โค ๐)) |
105 | | remsqsqrt 15147 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((๐ โ โ โง 0 โค
๐) โ
((โโ๐) ยท
(โโ๐)) = ๐) |
106 | 104, 105 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ โ ((โโ๐) ยท (โโ๐)) = ๐) |
107 | 103, 106 | breqtrd 5132 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ โ ((โโ๐) ยท ((1 + (๐ฟ ยท ๐ธ)) ยท ๐)) โค ๐) |
108 | 28 | rpred 12962 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ โ ๐ โ โ) |
109 | 66, 108, 43 | lemuldivd 13011 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ โ (((โโ๐) ยท ((1 + (๐ฟ ยท ๐ธ)) ยท ๐)) โค ๐ โ (โโ๐) โค (๐ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐)))) |
110 | 107, 109 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ (โโ๐) โค (๐ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐))) |
111 | 29 | rpcnd 12964 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (๐ โ ๐ โ โ) |
112 | 111 | mulid2d 11178 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ โ (1 ยท ๐) = ๐) |
113 | | 1red 11161 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (๐ โ 1 โ
โ) |
114 | 42 | rpred 12962 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (๐ โ (1 + (๐ฟ ยท ๐ธ)) โ โ) |
115 | | 1re 11160 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข 1 โ
โ |
116 | | ltaddrp 12957 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข ((1
โ โ โง (๐ฟ
ยท ๐ธ) โ
โ+) โ 1 < (1 + (๐ฟ ยท ๐ธ))) |
117 | 115, 15, 116 | sylancr 588 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (๐ โ 1 < (1 + (๐ฟ ยท ๐ธ))) |
118 | 113, 114,
29, 117 | ltmul1dd 13017 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ โ (1 ยท ๐) < ((1 + (๐ฟ ยท ๐ธ)) ยท ๐)) |
119 | 112, 118 | eqbrtrrd 5130 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ โ ๐ < ((1 + (๐ฟ ยท ๐ธ)) ยท ๐)) |
120 | 29, 43, 28 | ltdiv2d 12985 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ โ (๐ < ((1 + (๐ฟ ยท ๐ธ)) ยท ๐) โ (๐ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐)) < (๐ / ๐))) |
121 | 119, 120 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ โ (๐ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐)) < (๐ / ๐)) |
122 | 45, 31, 121 | ltled 11308 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ (๐ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐)) โค (๐ / ๐)) |
123 | 66, 45, 31, 110, 122 | letrd 11317 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ (โโ๐) โค (๐ / ๐)) |
124 | 64, 66, 31, 68, 123 | letrd 11317 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ (4 / (๐ฟ ยท ๐ธ)) โค (๐ / ๐)) |
125 | 64, 31, 31, 124 | leadd2dd 11775 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ ((๐ / ๐) + (4 / (๐ฟ ยท ๐ธ))) โค ((๐ / ๐) + (๐ / ๐))) |
126 | 30 | rpcnd 12964 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ (๐ / ๐) โ โ) |
127 | 126 | 2timesd 12401 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ (2 ยท (๐ / ๐)) = ((๐ / ๐) + (๐ / ๐))) |
128 | 125, 127 | breqtrrd 5134 |
. . . . . . . . . . . . . . . 16
โข (๐ โ ((๐ / ๐) + (4 / (๐ฟ ยท ๐ธ))) โค (2 ยท (๐ / ๐))) |
129 | 31, 64 | readdcld 11189 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ ((๐ / ๐) + (4 / (๐ฟ ยท ๐ธ))) โ โ) |
130 | | 2re 12232 |
. . . . . . . . . . . . . . . . . 18
โข 2 โ
โ |
131 | | remulcl 11141 |
. . . . . . . . . . . . . . . . . 18
โข ((2
โ โ โง (๐ /
๐) โ โ) โ
(2 ยท (๐ / ๐)) โ
โ) |
132 | 130, 31, 131 | sylancr 588 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ (2 ยท (๐ / ๐)) โ โ) |
133 | 129, 132,
20 | lemul2d 13006 |
. . . . . . . . . . . . . . . 16
โข (๐ โ (((๐ / ๐) + (4 / (๐ฟ ยท ๐ธ))) โค (2 ยท (๐ / ๐)) โ (((๐ฟ ยท ๐ธ) / 4) ยท ((๐ / ๐) + (4 / (๐ฟ ยท ๐ธ)))) โค (((๐ฟ ยท ๐ธ) / 4) ยท (2 ยท (๐ / ๐))))) |
134 | 128, 133 | mpbid 231 |
. . . . . . . . . . . . . . 15
โข (๐ โ (((๐ฟ ยท ๐ธ) / 4) ยท ((๐ / ๐) + (4 / (๐ฟ ยท ๐ธ)))) โค (((๐ฟ ยท ๐ธ) / 4) ยท (2 ยท (๐ / ๐)))) |
135 | 20 | rpcnd 12964 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ ((๐ฟ ยท ๐ธ) / 4) โ โ) |
136 | 63 | rpcnd 12964 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ (4 / (๐ฟ ยท ๐ธ)) โ โ) |
137 | 135, 126,
136 | adddid 11184 |
. . . . . . . . . . . . . . . 16
โข (๐ โ (((๐ฟ ยท ๐ธ) / 4) ยท ((๐ / ๐) + (4 / (๐ฟ ยท ๐ธ)))) = ((((๐ฟ ยท ๐ธ) / 4) ยท (๐ / ๐)) + (((๐ฟ ยท ๐ธ) / 4) ยท (4 / (๐ฟ ยท ๐ธ))))) |
138 | 15 | rpcnne0d 12971 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ ((๐ฟ ยท ๐ธ) โ โ โง (๐ฟ ยท ๐ธ) โ 0)) |
139 | | rpcnne0 12938 |
. . . . . . . . . . . . . . . . . . 19
โข (4 โ
โ+ โ (4 โ โ โง 4 โ 0)) |
140 | 18, 139 | mp1i 13 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ (4 โ โ โง 4
โ 0)) |
141 | | divcan6 11867 |
. . . . . . . . . . . . . . . . . 18
โข ((((๐ฟ ยท ๐ธ) โ โ โง (๐ฟ ยท ๐ธ) โ 0) โง (4 โ โ โง 4
โ 0)) โ (((๐ฟ
ยท ๐ธ) / 4) ยท
(4 / (๐ฟ ยท ๐ธ))) = 1) |
142 | 138, 140,
141 | syl2anc 585 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ (((๐ฟ ยท ๐ธ) / 4) ยท (4 / (๐ฟ ยท ๐ธ))) = 1) |
143 | 142 | oveq2d 7374 |
. . . . . . . . . . . . . . . 16
โข (๐ โ ((((๐ฟ ยท ๐ธ) / 4) ยท (๐ / ๐)) + (((๐ฟ ยท ๐ธ) / 4) ยท (4 / (๐ฟ ยท ๐ธ)))) = ((((๐ฟ ยท ๐ธ) / 4) ยท (๐ / ๐)) + 1)) |
144 | 137, 143 | eqtrd 2773 |
. . . . . . . . . . . . . . 15
โข (๐ โ (((๐ฟ ยท ๐ธ) / 4) ยท ((๐ / ๐) + (4 / (๐ฟ ยท ๐ธ)))) = ((((๐ฟ ยท ๐ธ) / 4) ยท (๐ / ๐)) + 1)) |
145 | | 2cnd 12236 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ 2 โ
โ) |
146 | 135, 145,
126 | mulassd 11183 |
. . . . . . . . . . . . . . . 16
โข (๐ โ ((((๐ฟ ยท ๐ธ) / 4) ยท 2) ยท (๐ / ๐)) = (((๐ฟ ยท ๐ธ) / 4) ยท (2 ยท (๐ / ๐)))) |
147 | 15 | rpcnd 12964 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ โ (๐ฟ ยท ๐ธ) โ โ) |
148 | | 2rp 12925 |
. . . . . . . . . . . . . . . . . . . . . 22
โข 2 โ
โ+ |
149 | | rpcnne0 12938 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (2 โ
โ+ โ (2 โ โ โง 2 โ 0)) |
150 | 148, 149 | mp1i 13 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ โ (2 โ โ โง 2
โ 0)) |
151 | | divdiv1 11871 |
. . . . . . . . . . . . . . . . . . . . 21
โข (((๐ฟ ยท ๐ธ) โ โ โง (2 โ โ
โง 2 โ 0) โง (2 โ โ โง 2 โ 0)) โ (((๐ฟ ยท ๐ธ) / 2) / 2) = ((๐ฟ ยท ๐ธ) / (2 ยท 2))) |
152 | 147, 150,
150, 151 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ (((๐ฟ ยท ๐ธ) / 2) / 2) = ((๐ฟ ยท ๐ธ) / (2 ยท 2))) |
153 | | 2t2e4 12322 |
. . . . . . . . . . . . . . . . . . . . 21
โข (2
ยท 2) = 4 |
154 | 153 | oveq2i 7369 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ฟ ยท ๐ธ) / (2 ยท 2)) = ((๐ฟ ยท ๐ธ) / 4) |
155 | 152, 154 | eqtr2di 2790 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ ((๐ฟ ยท ๐ธ) / 4) = (((๐ฟ ยท ๐ธ) / 2) / 2)) |
156 | 155 | oveq1d 7373 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ (((๐ฟ ยท ๐ธ) / 4) ยท 2) = ((((๐ฟ ยท ๐ธ) / 2) / 2) ยท 2)) |
157 | 147 | halfcld 12403 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ ((๐ฟ ยท ๐ธ) / 2) โ โ) |
158 | 150 | simprd 497 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ 2 โ 0) |
159 | 157, 145,
158 | divcan1d 11937 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ ((((๐ฟ ยท ๐ธ) / 2) / 2) ยท 2) = ((๐ฟ ยท ๐ธ) / 2)) |
160 | 156, 159 | eqtrd 2773 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ (((๐ฟ ยท ๐ธ) / 4) ยท 2) = ((๐ฟ ยท ๐ธ) / 2)) |
161 | 160 | oveq1d 7373 |
. . . . . . . . . . . . . . . 16
โข (๐ โ ((((๐ฟ ยท ๐ธ) / 4) ยท 2) ยท (๐ / ๐)) = (((๐ฟ ยท ๐ธ) / 2) ยท (๐ / ๐))) |
162 | 146, 161 | eqtr3d 2775 |
. . . . . . . . . . . . . . 15
โข (๐ โ (((๐ฟ ยท ๐ธ) / 4) ยท (2 ยท (๐ / ๐))) = (((๐ฟ ยท ๐ธ) / 2) ยท (๐ / ๐))) |
163 | 134, 144,
162 | 3brtr3d 5137 |
. . . . . . . . . . . . . 14
โข (๐ โ ((((๐ฟ ยท ๐ธ) / 4) ยท (๐ / ๐)) + 1) โค (((๐ฟ ยท ๐ธ) / 2) ยท (๐ / ๐))) |
164 | | flle 13710 |
. . . . . . . . . . . . . . 15
โข ((๐ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐)) โ โ โ
(โโ(๐ / ((1 +
(๐ฟ ยท ๐ธ)) ยท ๐))) โค (๐ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐))) |
165 | 45, 164 | syl 17 |
. . . . . . . . . . . . . 14
โข (๐ โ (โโ(๐ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐))) โค (๐ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐))) |
166 | 52, 47, 60, 45, 163, 165 | le2addd 11779 |
. . . . . . . . . . . . 13
โข (๐ โ (((((๐ฟ ยท ๐ธ) / 4) ยท (๐ / ๐)) + 1) + (โโ(๐ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐)))) โค ((((๐ฟ ยท ๐ธ) / 2) ยท (๐ / ๐)) + (๐ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐)))) |
167 | 58 | rpred 12962 |
. . . . . . . . . . . . . . . 16
โข (๐ โ ((๐ฟ ยท ๐ธ) / 2) โ โ) |
168 | 42 | rprecred 12973 |
. . . . . . . . . . . . . . . 16
โข (๐ โ (1 / (1 + (๐ฟ ยท ๐ธ))) โ โ) |
169 | 167, 168 | readdcld 11189 |
. . . . . . . . . . . . . . 15
โข (๐ โ (((๐ฟ ยท ๐ธ) / 2) + (1 / (1 + (๐ฟ ยท ๐ธ)))) โ โ) |
170 | 15 | rpred 12962 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ (๐ฟ ยท ๐ธ) โ โ) |
171 | 14 | rpred 12962 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ โ ๐ธ โ โ) |
172 | 8 | rpred 12962 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ โ ๐ฟ โ โ) |
173 | | eliooord 13329 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (๐ฟ โ (0(,)1) โ (0 <
๐ฟ โง ๐ฟ < 1)) |
174 | 4, 173 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (๐ โ (0 < ๐ฟ โง ๐ฟ < 1)) |
175 | 174 | simprd 497 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ โ ๐ฟ < 1) |
176 | 172, 113,
14, 175 | ltmul1dd 13017 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ โ (๐ฟ ยท ๐ธ) < (1 ยท ๐ธ)) |
177 | 14 | rpcnd 12964 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ โ ๐ธ โ โ) |
178 | 177 | mulid2d 11178 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ โ (1 ยท ๐ธ) = ๐ธ) |
179 | 176, 178 | breqtrd 5132 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ โ (๐ฟ ยท ๐ธ) < ๐ธ) |
180 | 13 | simp3d 1145 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (๐ โ (๐ธ โ (0(,)1) โง 1 < ๐พ โง (๐ โ ๐ธ) โ
โ+)) |
181 | 180 | simp1d 1143 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ โ ๐ธ โ (0(,)1)) |
182 | | eliooord 13329 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ธ โ (0(,)1) โ (0 <
๐ธ โง ๐ธ < 1)) |
183 | 181, 182 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ โ (0 < ๐ธ โง ๐ธ < 1)) |
184 | 183 | simprd 497 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ โ ๐ธ < 1) |
185 | 170, 171,
113, 179, 184 | lttrd 11321 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ (๐ฟ ยท ๐ธ) < 1) |
186 | 170, 113,
113, 185 | ltadd2dd 11319 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ (1 + (๐ฟ ยท ๐ธ)) < (1 + 1)) |
187 | | df-2 12221 |
. . . . . . . . . . . . . . . . . . 19
โข 2 = (1 +
1) |
188 | 186, 187 | breqtrrdi 5148 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ (1 + (๐ฟ ยท ๐ธ)) < 2) |
189 | 42 | rpregt0d 12968 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ ((1 + (๐ฟ ยท ๐ธ)) โ โ โง 0 < (1 + (๐ฟ ยท ๐ธ)))) |
190 | 130 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ 2 โ
โ) |
191 | | 2pos 12261 |
. . . . . . . . . . . . . . . . . . . 20
โข 0 <
2 |
192 | 191 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ 0 < 2) |
193 | 15 | rpregt0d 12968 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ ((๐ฟ ยท ๐ธ) โ โ โง 0 < (๐ฟ ยท ๐ธ))) |
194 | | ltdiv2 12046 |
. . . . . . . . . . . . . . . . . . 19
โข ((((1 +
(๐ฟ ยท ๐ธ)) โ โ โง 0 <
(1 + (๐ฟ ยท ๐ธ))) โง (2 โ โ
โง 0 < 2) โง ((๐ฟ
ยท ๐ธ) โ โ
โง 0 < (๐ฟ ยท
๐ธ))) โ ((1 + (๐ฟ ยท ๐ธ)) < 2 โ ((๐ฟ ยท ๐ธ) / 2) < ((๐ฟ ยท ๐ธ) / (1 + (๐ฟ ยท ๐ธ))))) |
195 | 189, 190,
192, 193, 194 | syl121anc 1376 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ ((1 + (๐ฟ ยท ๐ธ)) < 2 โ ((๐ฟ ยท ๐ธ) / 2) < ((๐ฟ ยท ๐ธ) / (1 + (๐ฟ ยท ๐ธ))))) |
196 | 188, 195 | mpbid 231 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ ((๐ฟ ยท ๐ธ) / 2) < ((๐ฟ ยท ๐ธ) / (1 + (๐ฟ ยท ๐ธ)))) |
197 | 42 | rpcnd 12964 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ (1 + (๐ฟ ยท ๐ธ)) โ โ) |
198 | 42 | rpcnne0d 12971 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ ((1 + (๐ฟ ยท ๐ธ)) โ โ โง (1 + (๐ฟ ยท ๐ธ)) โ 0)) |
199 | | divsubdir 11854 |
. . . . . . . . . . . . . . . . . . 19
โข (((1 +
(๐ฟ ยท ๐ธ)) โ โ โง 1 โ
โ โง ((1 + (๐ฟ
ยท ๐ธ)) โ โ
โง (1 + (๐ฟ ยท
๐ธ)) โ 0)) โ (((1 +
(๐ฟ ยท ๐ธ)) โ 1) / (1 + (๐ฟ ยท ๐ธ))) = (((1 + (๐ฟ ยท ๐ธ)) / (1 + (๐ฟ ยท ๐ธ))) โ (1 / (1 + (๐ฟ ยท ๐ธ))))) |
200 | 197, 49, 198, 199 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ (((1 + (๐ฟ ยท ๐ธ)) โ 1) / (1 + (๐ฟ ยท ๐ธ))) = (((1 + (๐ฟ ยท ๐ธ)) / (1 + (๐ฟ ยท ๐ธ))) โ (1 / (1 + (๐ฟ ยท ๐ธ))))) |
201 | | ax-1cn 11114 |
. . . . . . . . . . . . . . . . . . . 20
โข 1 โ
โ |
202 | | pncan2 11413 |
. . . . . . . . . . . . . . . . . . . 20
โข ((1
โ โ โง (๐ฟ
ยท ๐ธ) โ โ)
โ ((1 + (๐ฟ ยท
๐ธ)) โ 1) = (๐ฟ ยท ๐ธ)) |
203 | 201, 147,
202 | sylancr 588 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ ((1 + (๐ฟ ยท ๐ธ)) โ 1) = (๐ฟ ยท ๐ธ)) |
204 | 203 | oveq1d 7373 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ (((1 + (๐ฟ ยท ๐ธ)) โ 1) / (1 + (๐ฟ ยท ๐ธ))) = ((๐ฟ ยท ๐ธ) / (1 + (๐ฟ ยท ๐ธ)))) |
205 | | divid 11847 |
. . . . . . . . . . . . . . . . . . . 20
โข (((1 +
(๐ฟ ยท ๐ธ)) โ โ โง (1 +
(๐ฟ ยท ๐ธ)) โ 0) โ ((1 + (๐ฟ ยท ๐ธ)) / (1 + (๐ฟ ยท ๐ธ))) = 1) |
206 | 198, 205 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ ((1 + (๐ฟ ยท ๐ธ)) / (1 + (๐ฟ ยท ๐ธ))) = 1) |
207 | 206 | oveq1d 7373 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ (((1 + (๐ฟ ยท ๐ธ)) / (1 + (๐ฟ ยท ๐ธ))) โ (1 / (1 + (๐ฟ ยท ๐ธ)))) = (1 โ (1 / (1 + (๐ฟ ยท ๐ธ))))) |
208 | 200, 204,
207 | 3eqtr3d 2781 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ ((๐ฟ ยท ๐ธ) / (1 + (๐ฟ ยท ๐ธ))) = (1 โ (1 / (1 + (๐ฟ ยท ๐ธ))))) |
209 | 196, 208 | breqtrd 5132 |
. . . . . . . . . . . . . . . 16
โข (๐ โ ((๐ฟ ยท ๐ธ) / 2) < (1 โ (1 / (1 + (๐ฟ ยท ๐ธ))))) |
210 | 167, 168,
113 | ltaddsubd 11760 |
. . . . . . . . . . . . . . . 16
โข (๐ โ ((((๐ฟ ยท ๐ธ) / 2) + (1 / (1 + (๐ฟ ยท ๐ธ)))) < 1 โ ((๐ฟ ยท ๐ธ) / 2) < (1 โ (1 / (1 + (๐ฟ ยท ๐ธ)))))) |
211 | 209, 210 | mpbird 257 |
. . . . . . . . . . . . . . 15
โข (๐ โ (((๐ฟ ยท ๐ธ) / 2) + (1 / (1 + (๐ฟ ยท ๐ธ)))) < 1) |
212 | 169, 113,
30, 211 | ltmul1dd 13017 |
. . . . . . . . . . . . . 14
โข (๐ โ ((((๐ฟ ยท ๐ธ) / 2) + (1 / (1 + (๐ฟ ยท ๐ธ)))) ยท (๐ / ๐)) < (1 ยท (๐ / ๐))) |
213 | | reccl 11825 |
. . . . . . . . . . . . . . . . 17
โข (((1 +
(๐ฟ ยท ๐ธ)) โ โ โง (1 +
(๐ฟ ยท ๐ธ)) โ 0) โ (1 / (1 +
(๐ฟ ยท ๐ธ))) โ
โ) |
214 | 198, 213 | syl 17 |
. . . . . . . . . . . . . . . 16
โข (๐ โ (1 / (1 + (๐ฟ ยท ๐ธ))) โ โ) |
215 | 157, 214,
126 | adddird 11185 |
. . . . . . . . . . . . . . 15
โข (๐ โ ((((๐ฟ ยท ๐ธ) / 2) + (1 / (1 + (๐ฟ ยท ๐ธ)))) ยท (๐ / ๐)) = ((((๐ฟ ยท ๐ธ) / 2) ยท (๐ / ๐)) + ((1 / (1 + (๐ฟ ยท ๐ธ))) ยท (๐ / ๐)))) |
216 | 197, 111 | mulcomd 11181 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ ((1 + (๐ฟ ยท ๐ธ)) ยท ๐) = (๐ ยท (1 + (๐ฟ ยท ๐ธ)))) |
217 | 216 | oveq2d 7374 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ (๐ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐)) = (๐ / (๐ ยท (1 + (๐ฟ ยท ๐ธ))))) |
218 | 28 | rpcnd 12964 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ ๐ โ โ) |
219 | 29 | rpcnne0d 12971 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ (๐ โ โ โง ๐ โ 0)) |
220 | | divdiv1 11871 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โ โ โง (๐ โ โ โง ๐ โ 0) โง ((1 + (๐ฟ ยท ๐ธ)) โ โ โง (1 + (๐ฟ ยท ๐ธ)) โ 0)) โ ((๐ / ๐) / (1 + (๐ฟ ยท ๐ธ))) = (๐ / (๐ ยท (1 + (๐ฟ ยท ๐ธ))))) |
221 | 218, 219,
198, 220 | syl3anc 1372 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ ((๐ / ๐) / (1 + (๐ฟ ยท ๐ธ))) = (๐ / (๐ ยท (1 + (๐ฟ ยท ๐ธ))))) |
222 | 42 | rpne0d 12967 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ (1 + (๐ฟ ยท ๐ธ)) โ 0) |
223 | 126, 197,
222 | divrec2d 11940 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ ((๐ / ๐) / (1 + (๐ฟ ยท ๐ธ))) = ((1 / (1 + (๐ฟ ยท ๐ธ))) ยท (๐ / ๐))) |
224 | 217, 221,
223 | 3eqtr2d 2779 |
. . . . . . . . . . . . . . . 16
โข (๐ โ (๐ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐)) = ((1 / (1 + (๐ฟ ยท ๐ธ))) ยท (๐ / ๐))) |
225 | 224 | oveq2d 7374 |
. . . . . . . . . . . . . . 15
โข (๐ โ ((((๐ฟ ยท ๐ธ) / 2) ยท (๐ / ๐)) + (๐ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐))) = ((((๐ฟ ยท ๐ธ) / 2) ยท (๐ / ๐)) + ((1 / (1 + (๐ฟ ยท ๐ธ))) ยท (๐ / ๐)))) |
226 | 215, 225 | eqtr4d 2776 |
. . . . . . . . . . . . . 14
โข (๐ โ ((((๐ฟ ยท ๐ธ) / 2) + (1 / (1 + (๐ฟ ยท ๐ธ)))) ยท (๐ / ๐)) = ((((๐ฟ ยท ๐ธ) / 2) ยท (๐ / ๐)) + (๐ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐)))) |
227 | 126 | mulid2d 11178 |
. . . . . . . . . . . . . 14
โข (๐ โ (1 ยท (๐ / ๐)) = (๐ / ๐)) |
228 | 212, 226,
227 | 3brtr3d 5137 |
. . . . . . . . . . . . 13
โข (๐ โ ((((๐ฟ ยท ๐ธ) / 2) ยท (๐ / ๐)) + (๐ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐))) < (๐ / ๐)) |
229 | 53, 61, 31, 166, 228 | lelttrd 11318 |
. . . . . . . . . . . 12
โข (๐ โ (((((๐ฟ ยท ๐ธ) / 4) ยท (๐ / ๐)) + 1) + (โโ(๐ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐)))) < (๐ / ๐)) |
230 | | fllep1 13712 |
. . . . . . . . . . . . 13
โข ((๐ / ๐) โ โ โ (๐ / ๐) โค ((โโ(๐ / ๐)) + 1)) |
231 | 31, 230 | syl 17 |
. . . . . . . . . . . 12
โข (๐ โ (๐ / ๐) โค ((โโ(๐ / ๐)) + 1)) |
232 | 53, 31, 57, 229, 231 | ltletrd 11320 |
. . . . . . . . . . 11
โข (๐ โ (((((๐ฟ ยท ๐ธ) / 4) ยท (๐ / ๐)) + 1) + (โโ(๐ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐)))) < ((โโ(๐ / ๐)) + 1)) |
233 | 50, 232 | eqbrtrd 5128 |
. . . . . . . . . 10
โข (๐ โ (((((๐ฟ ยท ๐ธ) / 4) ยท (๐ / ๐)) + (โโ(๐ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐)))) + 1) < ((โโ(๐ / ๐)) + 1)) |
234 | 32, 47 | readdcld 11189 |
. . . . . . . . . . 11
โข (๐ โ ((((๐ฟ ยท ๐ธ) / 4) ยท (๐ / ๐)) + (โโ(๐ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐)))) โ โ) |
235 | 234, 55, 113 | ltadd1d 11753 |
. . . . . . . . . 10
โข (๐ โ (((((๐ฟ ยท ๐ธ) / 4) ยท (๐ / ๐)) + (โโ(๐ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐)))) < (โโ(๐ / ๐)) โ (((((๐ฟ ยท ๐ธ) / 4) ยท (๐ / ๐)) + (โโ(๐ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐)))) + 1) < ((โโ(๐ / ๐)) + 1))) |
236 | 233, 235 | mpbird 257 |
. . . . . . . . 9
โข (๐ โ ((((๐ฟ ยท ๐ธ) / 4) ยท (๐ / ๐)) + (โโ(๐ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐)))) < (โโ(๐ / ๐))) |
237 | 32, 47, 55 | ltaddsubd 11760 |
. . . . . . . . 9
โข (๐ โ (((((๐ฟ ยท ๐ธ) / 4) ยท (๐ / ๐)) + (โโ(๐ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐)))) < (โโ(๐ / ๐)) โ (((๐ฟ ยท ๐ธ) / 4) ยท (๐ / ๐)) < ((โโ(๐ / ๐)) โ (โโ(๐ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐)))))) |
238 | 236, 237 | mpbid 231 |
. . . . . . . 8
โข (๐ โ (((๐ฟ ยท ๐ธ) / 4) ยท (๐ / ๐)) < ((โโ(๐ / ๐)) โ (โโ(๐ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐))))) |
239 | 31 | flcld 13709 |
. . . . . . . . . . . 12
โข (๐ โ (โโ(๐ / ๐)) โ โค) |
240 | | fzval3 13647 |
. . . . . . . . . . . 12
โข
((โโ(๐ /
๐)) โ โค โ
(((โโ(๐ / ((1 +
(๐ฟ ยท ๐ธ)) ยท ๐))) + 1)...(โโ(๐ / ๐))) = (((โโ(๐ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐))) + 1)..^((โโ(๐ / ๐)) + 1))) |
241 | 239, 240 | syl 17 |
. . . . . . . . . . 11
โข (๐ โ (((โโ(๐ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐))) + 1)...(โโ(๐ / ๐))) = (((โโ(๐ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐))) + 1)..^((โโ(๐ / ๐)) + 1))) |
242 | 33, 241 | eqtrid 2785 |
. . . . . . . . . 10
โข (๐ โ ๐ผ = (((โโ(๐ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐))) + 1)..^((โโ(๐ / ๐)) + 1))) |
243 | 242 | fveq2d 6847 |
. . . . . . . . 9
โข (๐ โ (โฏโ๐ผ) =
(โฏโ(((โโ(๐ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐))) + 1)..^((โโ(๐ / ๐)) + 1)))) |
244 | | flword2 13724 |
. . . . . . . . . . . 12
โข (((๐ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐)) โ โ โง (๐ / ๐) โ โ โง (๐ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐)) โค (๐ / ๐)) โ (โโ(๐ / ๐)) โ
(โคโฅโ(โโ(๐ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐))))) |
245 | 45, 31, 122, 244 | syl3anc 1372 |
. . . . . . . . . . 11
โข (๐ โ (โโ(๐ / ๐)) โ
(โคโฅโ(โโ(๐ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐))))) |
246 | | eluzp1p1 12796 |
. . . . . . . . . . 11
โข
((โโ(๐ /
๐)) โ
(โคโฅโ(โโ(๐ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐)))) โ ((โโ(๐ / ๐)) + 1) โ
(โคโฅโ((โโ(๐ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐))) + 1))) |
247 | 245, 246 | syl 17 |
. . . . . . . . . 10
โข (๐ โ ((โโ(๐ / ๐)) + 1) โ
(โคโฅโ((โโ(๐ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐))) + 1))) |
248 | | hashfzo 14335 |
. . . . . . . . . 10
โข
(((โโ(๐
/ ๐)) + 1) โ
(โคโฅโ((โโ(๐ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐))) + 1)) โ
(โฏโ(((โโ(๐ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐))) + 1)..^((โโ(๐ / ๐)) + 1))) = (((โโ(๐ / ๐)) + 1) โ ((โโ(๐ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐))) + 1))) |
249 | 247, 248 | syl 17 |
. . . . . . . . 9
โข (๐ โ
(โฏโ(((โโ(๐ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐))) + 1)..^((โโ(๐ / ๐)) + 1))) = (((โโ(๐ / ๐)) + 1) โ ((โโ(๐ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐))) + 1))) |
250 | 55 | recnd 11188 |
. . . . . . . . . 10
โข (๐ โ (โโ(๐ / ๐)) โ โ) |
251 | 250, 48, 49 | pnpcan2d 11555 |
. . . . . . . . 9
โข (๐ โ (((โโ(๐ / ๐)) + 1) โ ((โโ(๐ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐))) + 1)) = ((โโ(๐ / ๐)) โ (โโ(๐ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐))))) |
252 | 243, 249,
251 | 3eqtrd 2777 |
. . . . . . . 8
โข (๐ โ (โฏโ๐ผ) = ((โโ(๐ / ๐)) โ (โโ(๐ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐))))) |
253 | 238, 252 | breqtrrd 5134 |
. . . . . . 7
โข (๐ โ (((๐ฟ ยท ๐ธ) / 4) ยท (๐ / ๐)) < (โฏโ๐ผ)) |
254 | 32, 38, 253 | ltled 11308 |
. . . . . 6
โข (๐ โ (((๐ฟ ยท ๐ธ) / 4) ยท (๐ / ๐)) โค (โฏโ๐ผ)) |
255 | 21, 38, 30 | lemuldivd 13011 |
. . . . . 6
โข (๐ โ ((((๐ฟ ยท ๐ธ) / 4) ยท (๐ / ๐)) โค (โฏโ๐ผ) โ ((๐ฟ ยท ๐ธ) / 4) โค ((โฏโ๐ผ) / (๐ / ๐)))) |
256 | 254, 255 | mpbid 231 |
. . . . 5
โข (๐ โ ((๐ฟ ยท ๐ธ) / 4) โค ((โฏโ๐ผ) / (๐ / ๐))) |
257 | 29 | rpred 12962 |
. . . . . . . . . . . . . . 15
โข (๐ โ ๐ โ โ) |
258 | 69, 76, 66, 94, 100 | ltletrd 11320 |
. . . . . . . . . . . . . . . 16
โข (๐ โ ((1 + (๐ฟ ยท ๐ธ)) ยท ๐) < (โโ๐)) |
259 | 257, 69, 66, 119, 258 | lttrd 11321 |
. . . . . . . . . . . . . . 15
โข (๐ โ ๐ < (โโ๐)) |
260 | 257, 66, 259 | ltled 11308 |
. . . . . . . . . . . . . 14
โข (๐ โ ๐ โค (โโ๐)) |
261 | 29 | rprege0d 12969 |
. . . . . . . . . . . . . . 15
โข (๐ โ (๐ โ โ โง 0 โค ๐)) |
262 | 65 | rprege0d 12969 |
. . . . . . . . . . . . . . 15
โข (๐ โ ((โโ๐) โ โ โง 0 โค
(โโ๐))) |
263 | | le2sq 14045 |
. . . . . . . . . . . . . . 15
โข (((๐ โ โ โง 0 โค
๐) โง
((โโ๐) โ
โ โง 0 โค (โโ๐))) โ (๐ โค (โโ๐) โ (๐โ2) โค ((โโ๐)โ2))) |
264 | 261, 262,
263 | syl2anc 585 |
. . . . . . . . . . . . . 14
โข (๐ โ (๐ โค (โโ๐) โ (๐โ2) โค ((โโ๐)โ2))) |
265 | 260, 264 | mpbid 231 |
. . . . . . . . . . . . 13
โข (๐ โ (๐โ2) โค ((โโ๐)โ2)) |
266 | | resqrtth 15146 |
. . . . . . . . . . . . . 14
โข ((๐ โ โ โง 0 โค
๐) โ
((โโ๐)โ2)
= ๐) |
267 | 104, 266 | syl 17 |
. . . . . . . . . . . . 13
โข (๐ โ ((โโ๐)โ2) = ๐) |
268 | 265, 267 | breqtrd 5132 |
. . . . . . . . . . . 12
โข (๐ โ (๐โ2) โค ๐) |
269 | | 2z 12540 |
. . . . . . . . . . . . . . 15
โข 2 โ
โค |
270 | | rpexpcl 13992 |
. . . . . . . . . . . . . . 15
โข ((๐ โ โ+
โง 2 โ โค) โ (๐โ2) โ
โ+) |
271 | 29, 269, 270 | sylancl 587 |
. . . . . . . . . . . . . 14
โข (๐ โ (๐โ2) โ
โ+) |
272 | 271 | rpred 12962 |
. . . . . . . . . . . . 13
โข (๐ โ (๐โ2) โ โ) |
273 | 272, 108,
28 | lemul2d 13006 |
. . . . . . . . . . . 12
โข (๐ โ ((๐โ2) โค ๐ โ (๐ ยท (๐โ2)) โค (๐ ยท ๐))) |
274 | 268, 273 | mpbid 231 |
. . . . . . . . . . 11
โข (๐ โ (๐ ยท (๐โ2)) โค (๐ ยท ๐)) |
275 | 218 | sqvald 14054 |
. . . . . . . . . . 11
โข (๐ โ (๐โ2) = (๐ ยท ๐)) |
276 | 274, 275 | breqtrrd 5134 |
. . . . . . . . . 10
โข (๐ โ (๐ ยท (๐โ2)) โค (๐โ2)) |
277 | 108 | resqcld 14036 |
. . . . . . . . . . 11
โข (๐ โ (๐โ2) โ โ) |
278 | 108, 277,
271 | lemuldivd 13011 |
. . . . . . . . . 10
โข (๐ โ ((๐ ยท (๐โ2)) โค (๐โ2) โ ๐ โค ((๐โ2) / (๐โ2)))) |
279 | 276, 278 | mpbid 231 |
. . . . . . . . 9
โข (๐ โ ๐ โค ((๐โ2) / (๐โ2))) |
280 | 29 | rpne0d 12967 |
. . . . . . . . . 10
โข (๐ โ ๐ โ 0) |
281 | 218, 111,
280 | sqdivd 14070 |
. . . . . . . . 9
โข (๐ โ ((๐ / ๐)โ2) = ((๐โ2) / (๐โ2))) |
282 | 279, 281 | breqtrrd 5134 |
. . . . . . . 8
โข (๐ โ ๐ โค ((๐ / ๐)โ2)) |
283 | | rpexpcl 13992 |
. . . . . . . . . 10
โข (((๐ / ๐) โ โ+ โง 2 โ
โค) โ ((๐ / ๐)โ2) โ
โ+) |
284 | 30, 269, 283 | sylancl 587 |
. . . . . . . . 9
โข (๐ โ ((๐ / ๐)โ2) โ
โ+) |
285 | 28, 284 | logled 25998 |
. . . . . . . 8
โข (๐ โ (๐ โค ((๐ / ๐)โ2) โ (logโ๐) โค (logโ((๐ / ๐)โ2)))) |
286 | 282, 285 | mpbid 231 |
. . . . . . 7
โข (๐ โ (logโ๐) โค (logโ((๐ / ๐)โ2))) |
287 | | relogexp 25967 |
. . . . . . . 8
โข (((๐ / ๐) โ โ+ โง 2 โ
โค) โ (logโ((๐ / ๐)โ2)) = (2 ยท (logโ(๐ / ๐)))) |
288 | 30, 269, 287 | sylancl 587 |
. . . . . . 7
โข (๐ โ (logโ((๐ / ๐)โ2)) = (2 ยท (logโ(๐ / ๐)))) |
289 | 286, 288 | breqtrd 5132 |
. . . . . 6
โข (๐ โ (logโ๐) โค (2 ยท
(logโ(๐ / ๐)))) |
290 | 28 | relogcld 25994 |
. . . . . . 7
โข (๐ โ (logโ๐) โ
โ) |
291 | 30 | relogcld 25994 |
. . . . . . 7
โข (๐ โ (logโ(๐ / ๐)) โ โ) |
292 | | ledivmul 12036 |
. . . . . . 7
โข
(((logโ๐)
โ โ โง (logโ(๐ / ๐)) โ โ โง (2 โ โ
โง 0 < 2)) โ (((logโ๐) / 2) โค (logโ(๐ / ๐)) โ (logโ๐) โค (2 ยท (logโ(๐ / ๐))))) |
293 | 290, 291,
190, 192, 292 | syl112anc 1375 |
. . . . . 6
โข (๐ โ (((logโ๐) / 2) โค (logโ(๐ / ๐)) โ (logโ๐) โค (2 ยท (logโ(๐ / ๐))))) |
294 | 289, 293 | mpbird 257 |
. . . . 5
โข (๐ โ ((logโ๐) / 2) โค (logโ(๐ / ๐))) |
295 | 20 | rprege0d 12969 |
. . . . . 6
โข (๐ โ (((๐ฟ ยท ๐ธ) / 4) โ โ โง 0 โค ((๐ฟ ยท ๐ธ) / 4))) |
296 | 38, 30 | rerpdivcld 12993 |
. . . . . 6
โข (๐ โ ((โฏโ๐ผ) / (๐ / ๐)) โ โ) |
297 | 27 | simp2d 1144 |
. . . . . . . . . 10
โข (๐ โ (1 < ๐ โง e โค (โโ๐) โง (โโ๐) โค (๐ / ๐))) |
298 | 297 | simp1d 1143 |
. . . . . . . . 9
โข (๐ โ 1 < ๐) |
299 | 108, 298 | rplogcld 26000 |
. . . . . . . 8
โข (๐ โ (logโ๐) โ
โ+) |
300 | 299 | rphalfcld 12974 |
. . . . . . 7
โข (๐ โ ((logโ๐) / 2) โ
โ+) |
301 | 300 | rprege0d 12969 |
. . . . . 6
โข (๐ โ (((logโ๐) / 2) โ โ โง 0
โค ((logโ๐) /
2))) |
302 | | lemul12a 12018 |
. . . . . 6
โข
((((((๐ฟ ยท
๐ธ) / 4) โ โ
โง 0 โค ((๐ฟ ยท
๐ธ) / 4)) โง
((โฏโ๐ผ) / (๐ / ๐)) โ โ) โง ((((logโ๐) / 2) โ โ โง 0
โค ((logโ๐) / 2))
โง (logโ(๐ / ๐)) โ โ)) โ
((((๐ฟ ยท ๐ธ) / 4) โค
((โฏโ๐ผ) / (๐ / ๐)) โง ((logโ๐) / 2) โค (logโ(๐ / ๐))) โ (((๐ฟ ยท ๐ธ) / 4) ยท ((logโ๐) / 2)) โค
(((โฏโ๐ผ) /
(๐ / ๐)) ยท (logโ(๐ / ๐))))) |
303 | 295, 296,
301, 291, 302 | syl22anc 838 |
. . . . 5
โข (๐ โ ((((๐ฟ ยท ๐ธ) / 4) โค ((โฏโ๐ผ) / (๐ / ๐)) โง ((logโ๐) / 2) โค (logโ(๐ / ๐))) โ (((๐ฟ ยท ๐ธ) / 4) ยท ((logโ๐) / 2)) โค
(((โฏโ๐ผ) /
(๐ / ๐)) ยท (logโ(๐ / ๐))))) |
304 | 256, 294,
303 | mp2and 698 |
. . . 4
โข (๐ โ (((๐ฟ ยท ๐ธ) / 4) ยท ((logโ๐) / 2)) โค
(((โฏโ๐ผ) /
(๐ / ๐)) ยท (logโ(๐ / ๐)))) |
305 | 299 | rpcnd 12964 |
. . . . . 6
โข (๐ โ (logโ๐) โ
โ) |
306 | | 8nn 12253 |
. . . . . . . 8
โข 8 โ
โ |
307 | | nnrp 12931 |
. . . . . . . 8
โข (8 โ
โ โ 8 โ โ+) |
308 | 306, 307 | ax-mp 5 |
. . . . . . 7
โข 8 โ
โ+ |
309 | | rpcnne0 12938 |
. . . . . . 7
โข (8 โ
โ+ โ (8 โ โ โง 8 โ 0)) |
310 | 308, 309 | mp1i 13 |
. . . . . 6
โข (๐ โ (8 โ โ โง 8
โ 0)) |
311 | | div23 11837 |
. . . . . 6
โข (((๐ฟ ยท ๐ธ) โ โ โง (logโ๐) โ โ โง (8 โ
โ โง 8 โ 0)) โ (((๐ฟ ยท ๐ธ) ยท (logโ๐)) / 8) = (((๐ฟ ยท ๐ธ) / 8) ยท (logโ๐))) |
312 | 147, 305,
310, 311 | syl3anc 1372 |
. . . . 5
โข (๐ โ (((๐ฟ ยท ๐ธ) ยท (logโ๐)) / 8) = (((๐ฟ ยท ๐ธ) / 8) ยท (logโ๐))) |
313 | | divmuldiv 11860 |
. . . . . . 7
โข ((((๐ฟ ยท ๐ธ) โ โ โง (logโ๐) โ โ) โง ((4
โ โ โง 4 โ 0) โง (2 โ โ โง 2 โ 0))) โ
(((๐ฟ ยท ๐ธ) / 4) ยท
((logโ๐) / 2)) =
(((๐ฟ ยท ๐ธ) ยท (logโ๐)) / (4 ยท
2))) |
314 | 147, 305,
140, 150, 313 | syl22anc 838 |
. . . . . 6
โข (๐ โ (((๐ฟ ยท ๐ธ) / 4) ยท ((logโ๐) / 2)) = (((๐ฟ ยท ๐ธ) ยท (logโ๐)) / (4 ยท 2))) |
315 | | 4t2e8 12326 |
. . . . . . 7
โข (4
ยท 2) = 8 |
316 | 315 | oveq2i 7369 |
. . . . . 6
โข (((๐ฟ ยท ๐ธ) ยท (logโ๐)) / (4 ยท 2)) = (((๐ฟ ยท ๐ธ) ยท (logโ๐)) / 8) |
317 | 314, 316 | eqtr2di 2790 |
. . . . 5
โข (๐ โ (((๐ฟ ยท ๐ธ) ยท (logโ๐)) / 8) = (((๐ฟ ยท ๐ธ) / 4) ยท ((logโ๐) / 2))) |
318 | 312, 317 | eqtr3d 2775 |
. . . 4
โข (๐ โ (((๐ฟ ยท ๐ธ) / 8) ยท (logโ๐)) = (((๐ฟ ยท ๐ธ) / 4) ยท ((logโ๐) / 2))) |
319 | 38 | recnd 11188 |
. . . . 5
โข (๐ โ (โฏโ๐ผ) โ
โ) |
320 | 291 | recnd 11188 |
. . . . 5
โข (๐ โ (logโ(๐ / ๐)) โ โ) |
321 | 30 | rpcnne0d 12971 |
. . . . 5
โข (๐ โ ((๐ / ๐) โ โ โง (๐ / ๐) โ 0)) |
322 | | divass 11836 |
. . . . . 6
โข
(((โฏโ๐ผ)
โ โ โง (logโ(๐ / ๐)) โ โ โง ((๐ / ๐) โ โ โง (๐ / ๐) โ 0)) โ (((โฏโ๐ผ) ยท (logโ(๐ / ๐))) / (๐ / ๐)) = ((โฏโ๐ผ) ยท ((logโ(๐ / ๐)) / (๐ / ๐)))) |
323 | | div23 11837 |
. . . . . 6
โข
(((โฏโ๐ผ)
โ โ โง (logโ(๐ / ๐)) โ โ โง ((๐ / ๐) โ โ โง (๐ / ๐) โ 0)) โ (((โฏโ๐ผ) ยท (logโ(๐ / ๐))) / (๐ / ๐)) = (((โฏโ๐ผ) / (๐ / ๐)) ยท (logโ(๐ / ๐)))) |
324 | 322, 323 | eqtr3d 2775 |
. . . . 5
โข
(((โฏโ๐ผ)
โ โ โง (logโ(๐ / ๐)) โ โ โง ((๐ / ๐) โ โ โง (๐ / ๐) โ 0)) โ ((โฏโ๐ผ) ยท ((logโ(๐ / ๐)) / (๐ / ๐))) = (((โฏโ๐ผ) / (๐ / ๐)) ยท (logโ(๐ / ๐)))) |
325 | 319, 320,
321, 324 | syl3anc 1372 |
. . . 4
โข (๐ โ ((โฏโ๐ผ) ยท ((logโ(๐ / ๐)) / (๐ / ๐))) = (((โฏโ๐ผ) / (๐ / ๐)) ยท (logโ(๐ / ๐)))) |
326 | 304, 318,
325 | 3brtr4d 5138 |
. . 3
โข (๐ โ (((๐ฟ ยท ๐ธ) / 8) ยท (logโ๐)) โค ((โฏโ๐ผ) ยท ((logโ(๐ / ๐)) / (๐ / ๐)))) |
327 | | rpdivcl 12945 |
. . . . . . 7
โข (((๐ฟ ยท ๐ธ) โ โ+ โง 8 โ
โ+) โ ((๐ฟ ยท ๐ธ) / 8) โ
โ+) |
328 | 15, 308, 327 | sylancl 587 |
. . . . . 6
โข (๐ โ ((๐ฟ ยท ๐ธ) / 8) โ
โ+) |
329 | 328, 299 | rpmulcld 12978 |
. . . . 5
โข (๐ โ (((๐ฟ ยท ๐ธ) / 8) ยท (logโ๐)) โ
โ+) |
330 | 329 | rpred 12962 |
. . . 4
โข (๐ โ (((๐ฟ ยท ๐ธ) / 8) ยท (logโ๐)) โ โ) |
331 | 291, 30 | rerpdivcld 12993 |
. . . . 5
โข (๐ โ ((logโ(๐ / ๐)) / (๐ / ๐)) โ โ) |
332 | 38, 331 | remulcld 11190 |
. . . 4
โข (๐ โ ((โฏโ๐ผ) ยท ((logโ(๐ / ๐)) / (๐ / ๐))) โ โ) |
333 | 180 | simp3d 1145 |
. . . 4
โข (๐ โ (๐ โ ๐ธ) โ
โ+) |
334 | 330, 332,
333 | lemul2d 13006 |
. . 3
โข (๐ โ ((((๐ฟ ยท ๐ธ) / 8) ยท (logโ๐)) โค ((โฏโ๐ผ) ยท ((logโ(๐ / ๐)) / (๐ / ๐))) โ ((๐ โ ๐ธ) ยท (((๐ฟ ยท ๐ธ) / 8) ยท (logโ๐))) โค ((๐ โ ๐ธ) ยท ((โฏโ๐ผ) ยท ((logโ(๐ / ๐)) / (๐ / ๐)))))) |
335 | 326, 334 | mpbid 231 |
. 2
โข (๐ โ ((๐ โ ๐ธ) ยท (((๐ฟ ยท ๐ธ) / 8) ยท (logโ๐))) โค ((๐ โ ๐ธ) ยท ((โฏโ๐ผ) ยท ((logโ(๐ / ๐)) / (๐ / ๐))))) |
336 | 333 | rpcnd 12964 |
. . 3
โข (๐ โ (๐ โ ๐ธ) โ โ) |
337 | 331 | recnd 11188 |
. . 3
โข (๐ โ ((logโ(๐ / ๐)) / (๐ / ๐)) โ โ) |
338 | 336, 319,
337 | mul12d 11369 |
. 2
โข (๐ โ ((๐ โ ๐ธ) ยท ((โฏโ๐ผ) ยท ((logโ(๐ / ๐)) / (๐ / ๐)))) = ((โฏโ๐ผ) ยท ((๐ โ ๐ธ) ยท ((logโ(๐ / ๐)) / (๐ / ๐))))) |
339 | 335, 338 | breqtrd 5132 |
1
โข (๐ โ ((๐ โ ๐ธ) ยท (((๐ฟ ยท ๐ธ) / 8) ยท (logโ๐))) โค ((โฏโ๐ผ) ยท ((๐ โ ๐ธ) ยท ((logโ(๐ / ๐)) / (๐ / ๐))))) |