Step | Hyp | Ref
| Expression |
1 | | pntlem1.z |
. . . . 5
โข (๐ โ ๐ โ (๐[,)+โ)) |
2 | | pntlem1.r |
. . . . . . . 8
โข ๐
= (๐ โ โ+ โฆ
((ฯโ๐) โ
๐)) |
3 | | pntlem1.a |
. . . . . . . 8
โข (๐ โ ๐ด โ
โ+) |
4 | | pntlem1.b |
. . . . . . . 8
โข (๐ โ ๐ต โ
โ+) |
5 | | pntlem1.l |
. . . . . . . 8
โข (๐ โ ๐ฟ โ (0(,)1)) |
6 | | pntlem1.d |
. . . . . . . 8
โข ๐ท = (๐ด + 1) |
7 | | pntlem1.f |
. . . . . . . 8
โข ๐น = ((1 โ (1 / ๐ท)) ยท ((๐ฟ / (;32 ยท ๐ต)) / (๐ทโ2))) |
8 | | pntlem1.u |
. . . . . . . 8
โข (๐ โ ๐ โ
โ+) |
9 | | pntlem1.u2 |
. . . . . . . 8
โข (๐ โ ๐ โค ๐ด) |
10 | | pntlem1.e |
. . . . . . . 8
โข ๐ธ = (๐ / ๐ท) |
11 | | pntlem1.k |
. . . . . . . 8
โข ๐พ = (expโ(๐ต / ๐ธ)) |
12 | | pntlem1.y |
. . . . . . . 8
โข (๐ โ (๐ โ โ+ โง 1 โค
๐)) |
13 | | pntlem1.x |
. . . . . . . 8
โข (๐ โ (๐ โ โ+ โง ๐ < ๐)) |
14 | | pntlem1.c |
. . . . . . . 8
โข (๐ โ ๐ถ โ
โ+) |
15 | | pntlem1.w |
. . . . . . . 8
โข ๐ = (((๐ + (4 / (๐ฟ ยท ๐ธ)))โ2) + (((๐ ยท (๐พโ2))โ4) + (expโ(((;32 ยท ๐ต) / ((๐ โ ๐ธ) ยท (๐ฟ ยท (๐ธโ2)))) ยท ((๐ ยท 3) + ๐ถ))))) |
16 | 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15 | pntlema 26960 |
. . . . . . 7
โข (๐ โ ๐ โ
โ+) |
17 | 16 | rpred 12964 |
. . . . . 6
โข (๐ โ ๐ โ โ) |
18 | | pnfxr 11216 |
. . . . . 6
โข +โ
โ โ* |
19 | | elico2 13335 |
. . . . . 6
โข ((๐ โ โ โง +โ
โ โ*) โ (๐ โ (๐[,)+โ) โ (๐ โ โ โง ๐ โค ๐ โง ๐ < +โ))) |
20 | 17, 18, 19 | sylancl 587 |
. . . . 5
โข (๐ โ (๐ โ (๐[,)+โ) โ (๐ โ โ โง ๐ โค ๐ โง ๐ < +โ))) |
21 | 1, 20 | mpbid 231 |
. . . 4
โข (๐ โ (๐ โ โ โง ๐ โค ๐ โง ๐ < +โ)) |
22 | 21 | simp1d 1143 |
. . 3
โข (๐ โ ๐ โ โ) |
23 | 21 | simp2d 1144 |
. . 3
โข (๐ โ ๐ โค ๐) |
24 | 22, 16, 23 | rpgecld 13003 |
. 2
โข (๐ โ ๐ โ
โ+) |
25 | | 1re 11162 |
. . . . . . 7
โข 1 โ
โ |
26 | 25 | a1i 11 |
. . . . . 6
โข (๐ โ 1 โ
โ) |
27 | | ere 15978 |
. . . . . . 7
โข e โ
โ |
28 | 27 | a1i 11 |
. . . . . 6
โข (๐ โ e โ
โ) |
29 | 24 | rpsqrtcld 15303 |
. . . . . . 7
โข (๐ โ (โโ๐) โ
โ+) |
30 | 29 | rpred 12964 |
. . . . . 6
โข (๐ โ (โโ๐) โ
โ) |
31 | | 1lt2 12331 |
. . . . . . . 8
โข 1 <
2 |
32 | | egt2lt3 16095 |
. . . . . . . . 9
โข (2 < e
โง e < 3) |
33 | 32 | simpli 485 |
. . . . . . . 8
โข 2 <
e |
34 | | 2re 12234 |
. . . . . . . . 9
โข 2 โ
โ |
35 | 25, 34, 27 | lttri 11288 |
. . . . . . . 8
โข ((1 <
2 โง 2 < e) โ 1 < e) |
36 | 31, 33, 35 | mp2an 691 |
. . . . . . 7
โข 1 <
e |
37 | 36 | a1i 11 |
. . . . . 6
โข (๐ โ 1 < e) |
38 | | 4re 12244 |
. . . . . . . 8
โข 4 โ
โ |
39 | 38 | a1i 11 |
. . . . . . 7
โข (๐ โ 4 โ
โ) |
40 | 32 | simpri 487 |
. . . . . . . . 9
โข e <
3 |
41 | | 3lt4 12334 |
. . . . . . . . 9
โข 3 <
4 |
42 | | 3re 12240 |
. . . . . . . . . 10
โข 3 โ
โ |
43 | 27, 42, 38 | lttri 11288 |
. . . . . . . . 9
โข ((e <
3 โง 3 < 4) โ e < 4) |
44 | 40, 41, 43 | mp2an 691 |
. . . . . . . 8
โข e <
4 |
45 | 44 | a1i 11 |
. . . . . . 7
โข (๐ โ e < 4) |
46 | | 4nn 12243 |
. . . . . . . . . . 11
โข 4 โ
โ |
47 | | nnrp 12933 |
. . . . . . . . . . 11
โข (4 โ
โ โ 4 โ โ+) |
48 | 46, 47 | ax-mp 5 |
. . . . . . . . . 10
โข 4 โ
โ+ |
49 | 2, 3, 4, 5, 6, 7 | pntlemd 26958 |
. . . . . . . . . . . 12
โข (๐ โ (๐ฟ โ โ+ โง ๐ท โ โ+
โง ๐น โ
โ+)) |
50 | 49 | simp1d 1143 |
. . . . . . . . . . 11
โข (๐ โ ๐ฟ โ
โ+) |
51 | 2, 3, 4, 5, 6, 7, 8, 9, 10, 11 | pntlemc 26959 |
. . . . . . . . . . . 12
โข (๐ โ (๐ธ โ โ+ โง ๐พ โ โ+
โง (๐ธ โ (0(,)1)
โง 1 < ๐พ โง (๐ โ ๐ธ) โ
โ+))) |
52 | 51 | simp1d 1143 |
. . . . . . . . . . 11
โข (๐ โ ๐ธ โ
โ+) |
53 | 50, 52 | rpmulcld 12980 |
. . . . . . . . . 10
โข (๐ โ (๐ฟ ยท ๐ธ) โ
โ+) |
54 | | rpdivcl 12947 |
. . . . . . . . . 10
โข ((4
โ โ+ โง (๐ฟ ยท ๐ธ) โ โ+) โ (4 /
(๐ฟ ยท ๐ธ)) โ
โ+) |
55 | 48, 53, 54 | sylancr 588 |
. . . . . . . . 9
โข (๐ โ (4 / (๐ฟ ยท ๐ธ)) โ
โ+) |
56 | 55 | rpred 12964 |
. . . . . . . 8
โข (๐ โ (4 / (๐ฟ ยท ๐ธ)) โ โ) |
57 | 53 | rpred 12964 |
. . . . . . . . . . . 12
โข (๐ โ (๐ฟ ยท ๐ธ) โ โ) |
58 | 52 | rpred 12964 |
. . . . . . . . . . . 12
โข (๐ โ ๐ธ โ โ) |
59 | 50 | rpred 12964 |
. . . . . . . . . . . . . 14
โข (๐ โ ๐ฟ โ โ) |
60 | | eliooord 13330 |
. . . . . . . . . . . . . . . 16
โข (๐ฟ โ (0(,)1) โ (0 <
๐ฟ โง ๐ฟ < 1)) |
61 | 5, 60 | syl 17 |
. . . . . . . . . . . . . . 15
โข (๐ โ (0 < ๐ฟ โง ๐ฟ < 1)) |
62 | 61 | simprd 497 |
. . . . . . . . . . . . . 14
โข (๐ โ ๐ฟ < 1) |
63 | 59, 26, 52, 62 | ltmul1dd 13019 |
. . . . . . . . . . . . 13
โข (๐ โ (๐ฟ ยท ๐ธ) < (1 ยท ๐ธ)) |
64 | 52 | rpcnd 12966 |
. . . . . . . . . . . . . 14
โข (๐ โ ๐ธ โ โ) |
65 | 64 | mulid2d 11180 |
. . . . . . . . . . . . 13
โข (๐ โ (1 ยท ๐ธ) = ๐ธ) |
66 | 63, 65 | breqtrd 5136 |
. . . . . . . . . . . 12
โข (๐ โ (๐ฟ ยท ๐ธ) < ๐ธ) |
67 | 51 | simp3d 1145 |
. . . . . . . . . . . . . . 15
โข (๐ โ (๐ธ โ (0(,)1) โง 1 < ๐พ โง (๐ โ ๐ธ) โ
โ+)) |
68 | 67 | simp1d 1143 |
. . . . . . . . . . . . . 14
โข (๐ โ ๐ธ โ (0(,)1)) |
69 | | eliooord 13330 |
. . . . . . . . . . . . . 14
โข (๐ธ โ (0(,)1) โ (0 <
๐ธ โง ๐ธ < 1)) |
70 | 68, 69 | syl 17 |
. . . . . . . . . . . . 13
โข (๐ โ (0 < ๐ธ โง ๐ธ < 1)) |
71 | 70 | simprd 497 |
. . . . . . . . . . . 12
โข (๐ โ ๐ธ < 1) |
72 | 57, 58, 26, 66, 71 | lttrd 11323 |
. . . . . . . . . . 11
โข (๐ โ (๐ฟ ยท ๐ธ) < 1) |
73 | | 4pos 12267 |
. . . . . . . . . . . . 13
โข 0 <
4 |
74 | 39, 73 | jctir 522 |
. . . . . . . . . . . 12
โข (๐ โ (4 โ โ โง 0
< 4)) |
75 | | ltmul2 12013 |
. . . . . . . . . . . 12
โข (((๐ฟ ยท ๐ธ) โ โ โง 1 โ โ
โง (4 โ โ โง 0 < 4)) โ ((๐ฟ ยท ๐ธ) < 1 โ (4 ยท (๐ฟ ยท ๐ธ)) < (4 ยท 1))) |
76 | 57, 26, 74, 75 | syl3anc 1372 |
. . . . . . . . . . 11
โข (๐ โ ((๐ฟ ยท ๐ธ) < 1 โ (4 ยท (๐ฟ ยท ๐ธ)) < (4 ยท 1))) |
77 | 72, 76 | mpbid 231 |
. . . . . . . . . 10
โข (๐ โ (4 ยท (๐ฟ ยท ๐ธ)) < (4 ยท 1)) |
78 | | 4cn 12245 |
. . . . . . . . . . 11
โข 4 โ
โ |
79 | 78 | mulid1i 11166 |
. . . . . . . . . 10
โข (4
ยท 1) = 4 |
80 | 77, 79 | breqtrdi 5151 |
. . . . . . . . 9
โข (๐ โ (4 ยท (๐ฟ ยท ๐ธ)) < 4) |
81 | 39, 39, 53 | ltmuldivd 13011 |
. . . . . . . . 9
โข (๐ โ ((4 ยท (๐ฟ ยท ๐ธ)) < 4 โ 4 < (4 / (๐ฟ ยท ๐ธ)))) |
82 | 80, 81 | mpbid 231 |
. . . . . . . 8
โข (๐ โ 4 < (4 / (๐ฟ ยท ๐ธ))) |
83 | 12 | simpld 496 |
. . . . . . . . . . 11
โข (๐ โ ๐ โ
โ+) |
84 | 83, 55 | rpaddcld 12979 |
. . . . . . . . . 10
โข (๐ โ (๐ + (4 / (๐ฟ ยท ๐ธ))) โ
โ+) |
85 | 84 | rpred 12964 |
. . . . . . . . 9
โข (๐ โ (๐ + (4 / (๐ฟ ยท ๐ธ))) โ โ) |
86 | 56, 83 | ltaddrp2d 12998 |
. . . . . . . . 9
โข (๐ โ (4 / (๐ฟ ยท ๐ธ)) < (๐ + (4 / (๐ฟ ยท ๐ธ)))) |
87 | 85 | resqcld 14037 |
. . . . . . . . . . . 12
โข (๐ โ ((๐ + (4 / (๐ฟ ยท ๐ธ)))โ2) โ โ) |
88 | 13 | simpld 496 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ ๐ โ
โ+) |
89 | 51 | simp2d 1144 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ ๐พ โ
โ+) |
90 | | 2z 12542 |
. . . . . . . . . . . . . . . . . 18
โข 2 โ
โค |
91 | | rpexpcl 13993 |
. . . . . . . . . . . . . . . . . 18
โข ((๐พ โ โ+
โง 2 โ โค) โ (๐พโ2) โ
โ+) |
92 | 89, 90, 91 | sylancl 587 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ (๐พโ2) โ
โ+) |
93 | 88, 92 | rpmulcld 12980 |
. . . . . . . . . . . . . . . 16
โข (๐ โ (๐ ยท (๐พโ2)) โ
โ+) |
94 | | 4z 12544 |
. . . . . . . . . . . . . . . 16
โข 4 โ
โค |
95 | | rpexpcl 13993 |
. . . . . . . . . . . . . . . 16
โข (((๐ ยท (๐พโ2)) โ โ+ โง 4
โ โค) โ ((๐
ยท (๐พโ2))โ4) โ
โ+) |
96 | 93, 94, 95 | sylancl 587 |
. . . . . . . . . . . . . . 15
โข (๐ โ ((๐ ยท (๐พโ2))โ4) โ
โ+) |
97 | | 3nn0 12438 |
. . . . . . . . . . . . . . . . . . . . . 22
โข 3 โ
โ0 |
98 | | 2nn 12233 |
. . . . . . . . . . . . . . . . . . . . . 22
โข 2 โ
โ |
99 | 97, 98 | decnncl 12645 |
. . . . . . . . . . . . . . . . . . . . 21
โข ;32 โ โ |
100 | | nnrp 12933 |
. . . . . . . . . . . . . . . . . . . . 21
โข (;32 โ โ โ ;32 โ
โ+) |
101 | 99, 100 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . 20
โข ;32 โ
โ+ |
102 | | rpmulcl 12945 |
. . . . . . . . . . . . . . . . . . . 20
โข ((;32 โ โ+ โง
๐ต โ
โ+) โ (;32
ยท ๐ต) โ
โ+) |
103 | 101, 4, 102 | sylancr 588 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ (;32 ยท ๐ต) โ
โ+) |
104 | 67 | simp3d 1145 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ (๐ โ ๐ธ) โ
โ+) |
105 | | rpexpcl 13993 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((๐ธ โ โ+
โง 2 โ โค) โ (๐ธโ2) โ
โ+) |
106 | 52, 90, 105 | sylancl 587 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ โ (๐ธโ2) โ
โ+) |
107 | 50, 106 | rpmulcld 12980 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ (๐ฟ ยท (๐ธโ2)) โ
โ+) |
108 | 104, 107 | rpmulcld 12980 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ ((๐ โ ๐ธ) ยท (๐ฟ ยท (๐ธโ2))) โ
โ+) |
109 | 103, 108 | rpdivcld 12981 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ ((;32 ยท ๐ต) / ((๐ โ ๐ธ) ยท (๐ฟ ยท (๐ธโ2)))) โ
โ+) |
110 | | 3rp 12928 |
. . . . . . . . . . . . . . . . . . . 20
โข 3 โ
โ+ |
111 | | rpmulcl 12945 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โ โ+
โง 3 โ โ+) โ (๐ ยท 3) โ
โ+) |
112 | 8, 110, 111 | sylancl 587 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ (๐ ยท 3) โ
โ+) |
113 | 112, 14 | rpaddcld 12979 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ ((๐ ยท 3) + ๐ถ) โ
โ+) |
114 | 109, 113 | rpmulcld 12980 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ (((;32 ยท ๐ต) / ((๐ โ ๐ธ) ยท (๐ฟ ยท (๐ธโ2)))) ยท ((๐ ยท 3) + ๐ถ)) โ
โ+) |
115 | 114 | rpred 12964 |
. . . . . . . . . . . . . . . 16
โข (๐ โ (((;32 ยท ๐ต) / ((๐ โ ๐ธ) ยท (๐ฟ ยท (๐ธโ2)))) ยท ((๐ ยท 3) + ๐ถ)) โ โ) |
116 | 115 | rpefcld 15994 |
. . . . . . . . . . . . . . 15
โข (๐ โ (expโ(((;32 ยท ๐ต) / ((๐ โ ๐ธ) ยท (๐ฟ ยท (๐ธโ2)))) ยท ((๐ ยท 3) + ๐ถ))) โ
โ+) |
117 | 96, 116 | rpaddcld 12979 |
. . . . . . . . . . . . . 14
โข (๐ โ (((๐ ยท (๐พโ2))โ4) + (expโ(((;32 ยท ๐ต) / ((๐ โ ๐ธ) ยท (๐ฟ ยท (๐ธโ2)))) ยท ((๐ ยท 3) + ๐ถ)))) โ
โ+) |
118 | 87, 117 | ltaddrpd 12997 |
. . . . . . . . . . . . 13
โข (๐ โ ((๐ + (4 / (๐ฟ ยท ๐ธ)))โ2) < (((๐ + (4 / (๐ฟ ยท ๐ธ)))โ2) + (((๐ ยท (๐พโ2))โ4) + (expโ(((;32 ยท ๐ต) / ((๐ โ ๐ธ) ยท (๐ฟ ยท (๐ธโ2)))) ยท ((๐ ยท 3) + ๐ถ)))))) |
119 | 118, 15 | breqtrrdi 5152 |
. . . . . . . . . . . 12
โข (๐ โ ((๐ + (4 / (๐ฟ ยท ๐ธ)))โ2) < ๐) |
120 | 87, 17, 22, 119, 23 | ltletrd 11322 |
. . . . . . . . . . 11
โข (๐ โ ((๐ + (4 / (๐ฟ ยท ๐ธ)))โ2) < ๐) |
121 | 24 | rprege0d 12971 |
. . . . . . . . . . . 12
โข (๐ โ (๐ โ โ โง 0 โค ๐)) |
122 | | resqrtth 15147 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง 0 โค
๐) โ
((โโ๐)โ2)
= ๐) |
123 | 121, 122 | syl 17 |
. . . . . . . . . . 11
โข (๐ โ ((โโ๐)โ2) = ๐) |
124 | 120, 123 | breqtrrd 5138 |
. . . . . . . . . 10
โข (๐ โ ((๐ + (4 / (๐ฟ ยท ๐ธ)))โ2) < ((โโ๐)โ2)) |
125 | 84 | rprege0d 12971 |
. . . . . . . . . . 11
โข (๐ โ ((๐ + (4 / (๐ฟ ยท ๐ธ))) โ โ โง 0 โค (๐ + (4 / (๐ฟ ยท ๐ธ))))) |
126 | 29 | rprege0d 12971 |
. . . . . . . . . . 11
โข (๐ โ ((โโ๐) โ โ โง 0 โค
(โโ๐))) |
127 | | lt2sq 14045 |
. . . . . . . . . . 11
โข ((((๐ + (4 / (๐ฟ ยท ๐ธ))) โ โ โง 0 โค (๐ + (4 / (๐ฟ ยท ๐ธ)))) โง ((โโ๐) โ โ โง 0 โค
(โโ๐))) โ
((๐ + (4 / (๐ฟ ยท ๐ธ))) < (โโ๐) โ ((๐ + (4 / (๐ฟ ยท ๐ธ)))โ2) < ((โโ๐)โ2))) |
128 | 125, 126,
127 | syl2anc 585 |
. . . . . . . . . 10
โข (๐ โ ((๐ + (4 / (๐ฟ ยท ๐ธ))) < (โโ๐) โ ((๐ + (4 / (๐ฟ ยท ๐ธ)))โ2) < ((โโ๐)โ2))) |
129 | 124, 128 | mpbird 257 |
. . . . . . . . 9
โข (๐ โ (๐ + (4 / (๐ฟ ยท ๐ธ))) < (โโ๐)) |
130 | 56, 85, 30, 86, 129 | lttrd 11323 |
. . . . . . . 8
โข (๐ โ (4 / (๐ฟ ยท ๐ธ)) < (โโ๐)) |
131 | 39, 56, 30, 82, 130 | lttrd 11323 |
. . . . . . 7
โข (๐ โ 4 <
(โโ๐)) |
132 | 28, 39, 30, 45, 131 | lttrd 11323 |
. . . . . 6
โข (๐ โ e <
(โโ๐)) |
133 | 26, 28, 30, 37, 132 | lttrd 11323 |
. . . . 5
โข (๐ โ 1 <
(โโ๐)) |
134 | | 0le1 11685 |
. . . . . . 7
โข 0 โค
1 |
135 | 134 | a1i 11 |
. . . . . 6
โข (๐ โ 0 โค 1) |
136 | | lt2sq 14045 |
. . . . . 6
โข (((1
โ โ โง 0 โค 1) โง ((โโ๐) โ โ โง 0 โค
(โโ๐))) โ
(1 < (โโ๐)
โ (1โ2) < ((โโ๐)โ2))) |
137 | 26, 135, 126, 136 | syl21anc 837 |
. . . . 5
โข (๐ โ (1 <
(โโ๐) โ
(1โ2) < ((โโ๐)โ2))) |
138 | 133, 137 | mpbid 231 |
. . . 4
โข (๐ โ (1โ2) <
((โโ๐)โ2)) |
139 | | sq1 14106 |
. . . . 5
โข
(1โ2) = 1 |
140 | 139 | a1i 11 |
. . . 4
โข (๐ โ (1โ2) =
1) |
141 | 138, 140,
123 | 3brtr3d 5141 |
. . 3
โข (๐ โ 1 < ๐) |
142 | 28, 30, 132 | ltled 11310 |
. . 3
โข (๐ โ e โค
(โโ๐)) |
143 | 22, 83 | rerpdivcld 12995 |
. . . 4
โข (๐ โ (๐ / ๐) โ โ) |
144 | 83 | rpred 12964 |
. . . . . . 7
โข (๐ โ ๐ โ โ) |
145 | 144, 55 | ltaddrpd 12997 |
. . . . . . . 8
โข (๐ โ ๐ < (๐ + (4 / (๐ฟ ยท ๐ธ)))) |
146 | 144, 85, 30, 145, 129 | lttrd 11323 |
. . . . . . 7
โข (๐ โ ๐ < (โโ๐)) |
147 | 144, 30, 29, 146 | ltmul2dd 13020 |
. . . . . 6
โข (๐ โ ((โโ๐) ยท ๐) < ((โโ๐) ยท (โโ๐))) |
148 | | remsqsqrt 15148 |
. . . . . . 7
โข ((๐ โ โ โง 0 โค
๐) โ
((โโ๐) ยท
(โโ๐)) = ๐) |
149 | 121, 148 | syl 17 |
. . . . . 6
โข (๐ โ ((โโ๐) ยท (โโ๐)) = ๐) |
150 | 147, 149 | breqtrd 5136 |
. . . . 5
โข (๐ โ ((โโ๐) ยท ๐) < ๐) |
151 | 30, 22, 83 | ltmuldivd 13011 |
. . . . 5
โข (๐ โ (((โโ๐) ยท ๐) < ๐ โ (โโ๐) < (๐ / ๐))) |
152 | 150, 151 | mpbid 231 |
. . . 4
โข (๐ โ (โโ๐) < (๐ / ๐)) |
153 | 30, 143, 152 | ltled 11310 |
. . 3
โข (๐ โ (โโ๐) โค (๐ / ๐)) |
154 | 141, 142,
153 | 3jca 1129 |
. 2
โข (๐ โ (1 < ๐ โง e โค (โโ๐) โง (โโ๐) โค (๐ / ๐))) |
155 | 56, 30, 130 | ltled 11310 |
. . 3
โข (๐ โ (4 / (๐ฟ ยท ๐ธ)) โค (โโ๐)) |
156 | 88 | relogcld 25994 |
. . . . . 6
โข (๐ โ (logโ๐) โ
โ) |
157 | 89 | rpred 12964 |
. . . . . . 7
โข (๐ โ ๐พ โ โ) |
158 | 67 | simp2d 1144 |
. . . . . . 7
โข (๐ โ 1 < ๐พ) |
159 | 157, 158 | rplogcld 26000 |
. . . . . 6
โข (๐ โ (logโ๐พ) โ
โ+) |
160 | 156, 159 | rerpdivcld 12995 |
. . . . 5
โข (๐ โ ((logโ๐) / (logโ๐พ)) โ โ) |
161 | | readdcl 11141 |
. . . . 5
โข
((((logโ๐) /
(logโ๐พ)) โ
โ โง 2 โ โ) โ (((logโ๐) / (logโ๐พ)) + 2) โ โ) |
162 | 160, 34, 161 | sylancl 587 |
. . . 4
โข (๐ โ (((logโ๐) / (logโ๐พ)) + 2) โ โ) |
163 | 24 | relogcld 25994 |
. . . . . 6
โข (๐ โ (logโ๐) โ
โ) |
164 | 163, 159 | rerpdivcld 12995 |
. . . . 5
โข (๐ โ ((logโ๐) / (logโ๐พ)) โ โ) |
165 | | nndivre 12201 |
. . . . 5
โข
((((logโ๐) /
(logโ๐พ)) โ
โ โง 4 โ โ) โ (((logโ๐) / (logโ๐พ)) / 4) โ โ) |
166 | 164, 46, 165 | sylancl 587 |
. . . 4
โข (๐ โ (((logโ๐) / (logโ๐พ)) / 4) โ โ) |
167 | 93 | relogcld 25994 |
. . . . . 6
โข (๐ โ (logโ(๐ ยท (๐พโ2))) โ โ) |
168 | | nndivre 12201 |
. . . . . . 7
โข
(((logโ๐)
โ โ โง 4 โ โ) โ ((logโ๐) / 4) โ โ) |
169 | 163, 46, 168 | sylancl 587 |
. . . . . 6
โข (๐ โ ((logโ๐) / 4) โ
โ) |
170 | | relogexp 25967 |
. . . . . . . . 9
โข (((๐ ยท (๐พโ2)) โ โ+ โง 4
โ โค) โ (logโ((๐ ยท (๐พโ2))โ4)) = (4 ยท
(logโ(๐ ยท
(๐พโ2))))) |
171 | 93, 94, 170 | sylancl 587 |
. . . . . . . 8
โข (๐ โ (logโ((๐ ยท (๐พโ2))โ4)) = (4 ยท
(logโ(๐ ยท
(๐พโ2))))) |
172 | 96 | rpred 12964 |
. . . . . . . . . 10
โข (๐ โ ((๐ ยท (๐พโ2))โ4) โ
โ) |
173 | 117 | rpred 12964 |
. . . . . . . . . 10
โข (๐ โ (((๐ ยท (๐พโ2))โ4) + (expโ(((;32 ยท ๐ต) / ((๐ โ ๐ธ) ยท (๐ฟ ยท (๐ธโ2)))) ยท ((๐ ยท 3) + ๐ถ)))) โ โ) |
174 | 172, 116 | ltaddrpd 12997 |
. . . . . . . . . 10
โข (๐ โ ((๐ ยท (๐พโ2))โ4) < (((๐ ยท (๐พโ2))โ4) + (expโ(((;32 ยท ๐ต) / ((๐ โ ๐ธ) ยท (๐ฟ ยท (๐ธโ2)))) ยท ((๐ ยท 3) + ๐ถ))))) |
175 | | rpexpcl 13993 |
. . . . . . . . . . . . . 14
โข (((๐ + (4 / (๐ฟ ยท ๐ธ))) โ โ+ โง 2
โ โค) โ ((๐
+ (4 / (๐ฟ ยท ๐ธ)))โ2) โ
โ+) |
176 | 84, 90, 175 | sylancl 587 |
. . . . . . . . . . . . 13
โข (๐ โ ((๐ + (4 / (๐ฟ ยท ๐ธ)))โ2) โ
โ+) |
177 | 173, 176 | ltaddrpd 12997 |
. . . . . . . . . . . 12
โข (๐ โ (((๐ ยท (๐พโ2))โ4) + (expโ(((;32 ยท ๐ต) / ((๐ โ ๐ธ) ยท (๐ฟ ยท (๐ธโ2)))) ยท ((๐ ยท 3) + ๐ถ)))) < ((((๐ ยท (๐พโ2))โ4) + (expโ(((;32 ยท ๐ต) / ((๐ โ ๐ธ) ยท (๐ฟ ยท (๐ธโ2)))) ยท ((๐ ยท 3) + ๐ถ)))) + ((๐ + (4 / (๐ฟ ยท ๐ธ)))โ2))) |
178 | 87 | recnd 11190 |
. . . . . . . . . . . . . 14
โข (๐ โ ((๐ + (4 / (๐ฟ ยท ๐ธ)))โ2) โ โ) |
179 | 117 | rpcnd 12966 |
. . . . . . . . . . . . . 14
โข (๐ โ (((๐ ยท (๐พโ2))โ4) + (expโ(((;32 ยท ๐ต) / ((๐ โ ๐ธ) ยท (๐ฟ ยท (๐ธโ2)))) ยท ((๐ ยท 3) + ๐ถ)))) โ โ) |
180 | 178, 179 | addcomd 11364 |
. . . . . . . . . . . . 13
โข (๐ โ (((๐ + (4 / (๐ฟ ยท ๐ธ)))โ2) + (((๐ ยท (๐พโ2))โ4) + (expโ(((;32 ยท ๐ต) / ((๐ โ ๐ธ) ยท (๐ฟ ยท (๐ธโ2)))) ยท ((๐ ยท 3) + ๐ถ))))) = ((((๐ ยท (๐พโ2))โ4) + (expโ(((;32 ยท ๐ต) / ((๐ โ ๐ธ) ยท (๐ฟ ยท (๐ธโ2)))) ยท ((๐ ยท 3) + ๐ถ)))) + ((๐ + (4 / (๐ฟ ยท ๐ธ)))โ2))) |
181 | 15, 180 | eqtrid 2789 |
. . . . . . . . . . . 12
โข (๐ โ ๐ = ((((๐ ยท (๐พโ2))โ4) + (expโ(((;32 ยท ๐ต) / ((๐ โ ๐ธ) ยท (๐ฟ ยท (๐ธโ2)))) ยท ((๐ ยท 3) + ๐ถ)))) + ((๐ + (4 / (๐ฟ ยท ๐ธ)))โ2))) |
182 | 177, 181 | breqtrrd 5138 |
. . . . . . . . . . 11
โข (๐ โ (((๐ ยท (๐พโ2))โ4) + (expโ(((;32 ยท ๐ต) / ((๐ โ ๐ธ) ยท (๐ฟ ยท (๐ธโ2)))) ยท ((๐ ยท 3) + ๐ถ)))) < ๐) |
183 | 173, 17, 22, 182, 23 | ltletrd 11322 |
. . . . . . . . . 10
โข (๐ โ (((๐ ยท (๐พโ2))โ4) + (expโ(((;32 ยท ๐ต) / ((๐ โ ๐ธ) ยท (๐ฟ ยท (๐ธโ2)))) ยท ((๐ ยท 3) + ๐ถ)))) < ๐) |
184 | 172, 173,
22, 174, 183 | lttrd 11323 |
. . . . . . . . 9
โข (๐ โ ((๐ ยท (๐พโ2))โ4) < ๐) |
185 | | logltb 25971 |
. . . . . . . . . 10
โข ((((๐ ยท (๐พโ2))โ4) โ โ+
โง ๐ โ
โ+) โ (((๐ ยท (๐พโ2))โ4) < ๐ โ (logโ((๐ ยท (๐พโ2))โ4)) < (logโ๐))) |
186 | 96, 24, 185 | syl2anc 585 |
. . . . . . . . 9
โข (๐ โ (((๐ ยท (๐พโ2))โ4) < ๐ โ (logโ((๐ ยท (๐พโ2))โ4)) < (logโ๐))) |
187 | 184, 186 | mpbid 231 |
. . . . . . . 8
โข (๐ โ (logโ((๐ ยท (๐พโ2))โ4)) < (logโ๐)) |
188 | 171, 187 | eqbrtrrd 5134 |
. . . . . . 7
โข (๐ โ (4 ยท
(logโ(๐ ยท
(๐พโ2)))) <
(logโ๐)) |
189 | | ltmuldiv2 12036 |
. . . . . . . 8
โข
(((logโ(๐
ยท (๐พโ2)))
โ โ โง (logโ๐) โ โ โง (4 โ โ
โง 0 < 4)) โ ((4 ยท (logโ(๐ ยท (๐พโ2)))) < (logโ๐) โ (logโ(๐ ยท (๐พโ2))) < ((logโ๐) / 4))) |
190 | 167, 163,
74, 189 | syl3anc 1372 |
. . . . . . 7
โข (๐ โ ((4 ยท
(logโ(๐ ยท
(๐พโ2)))) <
(logโ๐) โ
(logโ(๐ ยท
(๐พโ2))) <
((logโ๐) /
4))) |
191 | 188, 190 | mpbid 231 |
. . . . . 6
โข (๐ โ (logโ(๐ ยท (๐พโ2))) < ((logโ๐) / 4)) |
192 | 167, 169,
159, 191 | ltdiv1dd 13021 |
. . . . 5
โข (๐ โ ((logโ(๐ ยท (๐พโ2))) / (logโ๐พ)) < (((logโ๐) / 4) / (logโ๐พ))) |
193 | 88, 92 | relogmuld 25996 |
. . . . . . . 8
โข (๐ โ (logโ(๐ ยท (๐พโ2))) = ((logโ๐) + (logโ(๐พโ2)))) |
194 | | relogexp 25967 |
. . . . . . . . . 10
โข ((๐พ โ โ+
โง 2 โ โค) โ (logโ(๐พโ2)) = (2 ยท (logโ๐พ))) |
195 | 89, 90, 194 | sylancl 587 |
. . . . . . . . 9
โข (๐ โ (logโ(๐พโ2)) = (2 ยท
(logโ๐พ))) |
196 | 195 | oveq2d 7378 |
. . . . . . . 8
โข (๐ โ ((logโ๐) + (logโ(๐พโ2))) = ((logโ๐) + (2 ยท (logโ๐พ)))) |
197 | 193, 196 | eqtrd 2777 |
. . . . . . 7
โข (๐ โ (logโ(๐ ยท (๐พโ2))) = ((logโ๐) + (2 ยท (logโ๐พ)))) |
198 | 197 | oveq1d 7377 |
. . . . . 6
โข (๐ โ ((logโ(๐ ยท (๐พโ2))) / (logโ๐พ)) = (((logโ๐) + (2 ยท (logโ๐พ))) / (logโ๐พ))) |
199 | 156 | recnd 11190 |
. . . . . . 7
โข (๐ โ (logโ๐) โ
โ) |
200 | | 2cnd 12238 |
. . . . . . . 8
โข (๐ โ 2 โ
โ) |
201 | 159 | rpcnd 12966 |
. . . . . . . 8
โข (๐ โ (logโ๐พ) โ
โ) |
202 | 200, 201 | mulcld 11182 |
. . . . . . 7
โข (๐ โ (2 ยท
(logโ๐พ)) โ
โ) |
203 | 159 | rpcnne0d 12973 |
. . . . . . 7
โข (๐ โ ((logโ๐พ) โ โ โง
(logโ๐พ) โ
0)) |
204 | | divdir 11845 |
. . . . . . 7
โข
(((logโ๐)
โ โ โง (2 ยท (logโ๐พ)) โ โ โง ((logโ๐พ) โ โ โง
(logโ๐พ) โ 0))
โ (((logโ๐) + (2
ยท (logโ๐พ))) /
(logโ๐พ)) =
(((logโ๐) /
(logโ๐พ)) + ((2
ยท (logโ๐พ)) /
(logโ๐พ)))) |
205 | 199, 202,
203, 204 | syl3anc 1372 |
. . . . . 6
โข (๐ โ (((logโ๐) + (2 ยท (logโ๐พ))) / (logโ๐พ)) = (((logโ๐) / (logโ๐พ)) + ((2 ยท (logโ๐พ)) / (logโ๐พ)))) |
206 | 203 | simprd 497 |
. . . . . . . 8
โข (๐ โ (logโ๐พ) โ 0) |
207 | 200, 201,
206 | divcan4d 11944 |
. . . . . . 7
โข (๐ โ ((2 ยท
(logโ๐พ)) /
(logโ๐พ)) =
2) |
208 | 207 | oveq2d 7378 |
. . . . . 6
โข (๐ โ (((logโ๐) / (logโ๐พ)) + ((2 ยท (logโ๐พ)) / (logโ๐พ))) = (((logโ๐) / (logโ๐พ)) + 2)) |
209 | 198, 205,
208 | 3eqtrd 2781 |
. . . . 5
โข (๐ โ ((logโ(๐ ยท (๐พโ2))) / (logโ๐พ)) = (((logโ๐) / (logโ๐พ)) + 2)) |
210 | 163 | recnd 11190 |
. . . . . 6
โข (๐ โ (logโ๐) โ
โ) |
211 | | rpcnne0 12940 |
. . . . . . 7
โข (4 โ
โ+ โ (4 โ โ โง 4 โ 0)) |
212 | 48, 211 | mp1i 13 |
. . . . . 6
โข (๐ โ (4 โ โ โง 4
โ 0)) |
213 | | divdiv32 11870 |
. . . . . 6
โข
(((logโ๐)
โ โ โง (4 โ โ โง 4 โ 0) โง ((logโ๐พ) โ โ โง
(logโ๐พ) โ 0))
โ (((logโ๐) / 4)
/ (logโ๐พ)) =
(((logโ๐) /
(logโ๐พ)) /
4)) |
214 | 210, 212,
203, 213 | syl3anc 1372 |
. . . . 5
โข (๐ โ (((logโ๐) / 4) / (logโ๐พ)) = (((logโ๐) / (logโ๐พ)) / 4)) |
215 | 192, 209,
214 | 3brtr3d 5141 |
. . . 4
โข (๐ โ (((logโ๐) / (logโ๐พ)) + 2) < (((logโ๐) / (logโ๐พ)) / 4)) |
216 | 162, 166,
215 | ltled 11310 |
. . 3
โข (๐ โ (((logโ๐) / (logโ๐พ)) + 2) โค (((logโ๐) / (logโ๐พ)) / 4)) |
217 | 113 | rpred 12964 |
. . . . 5
โข (๐ โ ((๐ ยท 3) + ๐ถ) โ โ) |
218 | 108, 103 | rpdivcld 12981 |
. . . . . . 7
โข (๐ โ (((๐ โ ๐ธ) ยท (๐ฟ ยท (๐ธโ2))) / (;32 ยท ๐ต)) โ
โ+) |
219 | 218 | rpred 12964 |
. . . . . 6
โข (๐ โ (((๐ โ ๐ธ) ยท (๐ฟ ยท (๐ธโ2))) / (;32 ยท ๐ต)) โ โ) |
220 | 219, 163 | remulcld 11192 |
. . . . 5
โข (๐ โ ((((๐ โ ๐ธ) ยท (๐ฟ ยท (๐ธโ2))) / (;32 ยท ๐ต)) ยท (logโ๐)) โ โ) |
221 | 113 | rpcnd 12966 |
. . . . . . . . 9
โข (๐ โ ((๐ ยท 3) + ๐ถ) โ โ) |
222 | 108 | rpcnne0d 12973 |
. . . . . . . . 9
โข (๐ โ (((๐ โ ๐ธ) ยท (๐ฟ ยท (๐ธโ2))) โ โ โง ((๐ โ ๐ธ) ยท (๐ฟ ยท (๐ธโ2))) โ 0)) |
223 | 103 | rpcnne0d 12973 |
. . . . . . . . 9
โข (๐ โ ((;32 ยท ๐ต) โ โ โง (;32 ยท ๐ต) โ 0)) |
224 | | divdiv2 11874 |
. . . . . . . . 9
โข ((((๐ ยท 3) + ๐ถ) โ โ โง (((๐ โ ๐ธ) ยท (๐ฟ ยท (๐ธโ2))) โ โ โง ((๐ โ ๐ธ) ยท (๐ฟ ยท (๐ธโ2))) โ 0) โง ((;32 ยท ๐ต) โ โ โง (;32 ยท ๐ต) โ 0)) โ (((๐ ยท 3) + ๐ถ) / (((๐ โ ๐ธ) ยท (๐ฟ ยท (๐ธโ2))) / (;32 ยท ๐ต))) = ((((๐ ยท 3) + ๐ถ) ยท (;32 ยท ๐ต)) / ((๐ โ ๐ธ) ยท (๐ฟ ยท (๐ธโ2))))) |
225 | 221, 222,
223, 224 | syl3anc 1372 |
. . . . . . . 8
โข (๐ โ (((๐ ยท 3) + ๐ถ) / (((๐ โ ๐ธ) ยท (๐ฟ ยท (๐ธโ2))) / (;32 ยท ๐ต))) = ((((๐ ยท 3) + ๐ถ) ยท (;32 ยท ๐ต)) / ((๐ โ ๐ธ) ยท (๐ฟ ยท (๐ธโ2))))) |
226 | 103 | rpcnd 12966 |
. . . . . . . . . 10
โข (๐ โ (;32 ยท ๐ต) โ โ) |
227 | 221, 226 | mulcomd 11183 |
. . . . . . . . 9
โข (๐ โ (((๐ ยท 3) + ๐ถ) ยท (;32 ยท ๐ต)) = ((;32 ยท ๐ต) ยท ((๐ ยท 3) + ๐ถ))) |
228 | 227 | oveq1d 7377 |
. . . . . . . 8
โข (๐ โ ((((๐ ยท 3) + ๐ถ) ยท (;32 ยท ๐ต)) / ((๐ โ ๐ธ) ยท (๐ฟ ยท (๐ธโ2)))) = (((;32 ยท ๐ต) ยท ((๐ ยท 3) + ๐ถ)) / ((๐ โ ๐ธ) ยท (๐ฟ ยท (๐ธโ2))))) |
229 | | div23 11839 |
. . . . . . . . 9
โข (((;32 ยท ๐ต) โ โ โง ((๐ ยท 3) + ๐ถ) โ โ โง (((๐ โ ๐ธ) ยท (๐ฟ ยท (๐ธโ2))) โ โ โง ((๐ โ ๐ธ) ยท (๐ฟ ยท (๐ธโ2))) โ 0)) โ (((;32 ยท ๐ต) ยท ((๐ ยท 3) + ๐ถ)) / ((๐ โ ๐ธ) ยท (๐ฟ ยท (๐ธโ2)))) = (((;32 ยท ๐ต) / ((๐ โ ๐ธ) ยท (๐ฟ ยท (๐ธโ2)))) ยท ((๐ ยท 3) + ๐ถ))) |
230 | 226, 221,
222, 229 | syl3anc 1372 |
. . . . . . . 8
โข (๐ โ (((;32 ยท ๐ต) ยท ((๐ ยท 3) + ๐ถ)) / ((๐ โ ๐ธ) ยท (๐ฟ ยท (๐ธโ2)))) = (((;32 ยท ๐ต) / ((๐ โ ๐ธ) ยท (๐ฟ ยท (๐ธโ2)))) ยท ((๐ ยท 3) + ๐ถ))) |
231 | 225, 228,
230 | 3eqtrd 2781 |
. . . . . . 7
โข (๐ โ (((๐ ยท 3) + ๐ถ) / (((๐ โ ๐ธ) ยท (๐ฟ ยท (๐ธโ2))) / (;32 ยท ๐ต))) = (((;32 ยท ๐ต) / ((๐ โ ๐ธ) ยท (๐ฟ ยท (๐ธโ2)))) ยท ((๐ ยท 3) + ๐ถ))) |
232 | 115 | reefcld 15977 |
. . . . . . . . . 10
โข (๐ โ (expโ(((;32 ยท ๐ต) / ((๐ โ ๐ธ) ยท (๐ฟ ยท (๐ธโ2)))) ยท ((๐ ยท 3) + ๐ถ))) โ โ) |
233 | 232, 96 | ltaddrp2d 12998 |
. . . . . . . . . 10
โข (๐ โ (expโ(((;32 ยท ๐ต) / ((๐ โ ๐ธ) ยท (๐ฟ ยท (๐ธโ2)))) ยท ((๐ ยท 3) + ๐ถ))) < (((๐ ยท (๐พโ2))โ4) + (expโ(((;32 ยท ๐ต) / ((๐ โ ๐ธ) ยท (๐ฟ ยท (๐ธโ2)))) ยท ((๐ ยท 3) + ๐ถ))))) |
234 | 232, 173,
22, 233, 183 | lttrd 11323 |
. . . . . . . . 9
โข (๐ โ (expโ(((;32 ยท ๐ต) / ((๐ โ ๐ธ) ยท (๐ฟ ยท (๐ธโ2)))) ยท ((๐ ยท 3) + ๐ถ))) < ๐) |
235 | 24 | reeflogd 25995 |
. . . . . . . . 9
โข (๐ โ
(expโ(logโ๐)) =
๐) |
236 | 234, 235 | breqtrrd 5138 |
. . . . . . . 8
โข (๐ โ (expโ(((;32 ยท ๐ต) / ((๐ โ ๐ธ) ยท (๐ฟ ยท (๐ธโ2)))) ยท ((๐ ยท 3) + ๐ถ))) < (expโ(logโ๐))) |
237 | | eflt 16006 |
. . . . . . . . 9
โข
(((((;32 ยท ๐ต) / ((๐ โ ๐ธ) ยท (๐ฟ ยท (๐ธโ2)))) ยท ((๐ ยท 3) + ๐ถ)) โ โ โง (logโ๐) โ โ) โ
((((;32 ยท ๐ต) / ((๐ โ ๐ธ) ยท (๐ฟ ยท (๐ธโ2)))) ยท ((๐ ยท 3) + ๐ถ)) < (logโ๐) โ (expโ(((;32 ยท ๐ต) / ((๐ โ ๐ธ) ยท (๐ฟ ยท (๐ธโ2)))) ยท ((๐ ยท 3) + ๐ถ))) < (expโ(logโ๐)))) |
238 | 115, 163,
237 | syl2anc 585 |
. . . . . . . 8
โข (๐ โ ((((;32 ยท ๐ต) / ((๐ โ ๐ธ) ยท (๐ฟ ยท (๐ธโ2)))) ยท ((๐ ยท 3) + ๐ถ)) < (logโ๐) โ (expโ(((;32 ยท ๐ต) / ((๐ โ ๐ธ) ยท (๐ฟ ยท (๐ธโ2)))) ยท ((๐ ยท 3) + ๐ถ))) < (expโ(logโ๐)))) |
239 | 236, 238 | mpbird 257 |
. . . . . . 7
โข (๐ โ (((;32 ยท ๐ต) / ((๐ โ ๐ธ) ยท (๐ฟ ยท (๐ธโ2)))) ยท ((๐ ยท 3) + ๐ถ)) < (logโ๐)) |
240 | 231, 239 | eqbrtrd 5132 |
. . . . . 6
โข (๐ โ (((๐ ยท 3) + ๐ถ) / (((๐ โ ๐ธ) ยท (๐ฟ ยท (๐ธโ2))) / (;32 ยท ๐ต))) < (logโ๐)) |
241 | 217, 163,
218 | ltdivmuld 13015 |
. . . . . 6
โข (๐ โ ((((๐ ยท 3) + ๐ถ) / (((๐ โ ๐ธ) ยท (๐ฟ ยท (๐ธโ2))) / (;32 ยท ๐ต))) < (logโ๐) โ ((๐ ยท 3) + ๐ถ) < ((((๐ โ ๐ธ) ยท (๐ฟ ยท (๐ธโ2))) / (;32 ยท ๐ต)) ยท (logโ๐)))) |
242 | 240, 241 | mpbid 231 |
. . . . 5
โข (๐ โ ((๐ ยท 3) + ๐ถ) < ((((๐ โ ๐ธ) ยท (๐ฟ ยท (๐ธโ2))) / (;32 ยท ๐ต)) ยท (logโ๐))) |
243 | 217, 220,
242 | ltled 11310 |
. . . 4
โข (๐ โ ((๐ ยท 3) + ๐ถ) โค ((((๐ โ ๐ธ) ยท (๐ฟ ยท (๐ธโ2))) / (;32 ยท ๐ต)) ยท (logโ๐))) |
244 | 104 | rpcnd 12966 |
. . . . . 6
โข (๐ โ (๐ โ ๐ธ) โ โ) |
245 | 107 | rpcnd 12966 |
. . . . . 6
โข (๐ โ (๐ฟ ยท (๐ธโ2)) โ โ) |
246 | | divass 11838 |
. . . . . 6
โข (((๐ โ ๐ธ) โ โ โง (๐ฟ ยท (๐ธโ2)) โ โ โง ((;32 ยท ๐ต) โ โ โง (;32 ยท ๐ต) โ 0)) โ (((๐ โ ๐ธ) ยท (๐ฟ ยท (๐ธโ2))) / (;32 ยท ๐ต)) = ((๐ โ ๐ธ) ยท ((๐ฟ ยท (๐ธโ2)) / (;32 ยท ๐ต)))) |
247 | 244, 245,
223, 246 | syl3anc 1372 |
. . . . 5
โข (๐ โ (((๐ โ ๐ธ) ยท (๐ฟ ยท (๐ธโ2))) / (;32 ยท ๐ต)) = ((๐ โ ๐ธ) ยท ((๐ฟ ยท (๐ธโ2)) / (;32 ยท ๐ต)))) |
248 | 247 | oveq1d 7377 |
. . . 4
โข (๐ โ ((((๐ โ ๐ธ) ยท (๐ฟ ยท (๐ธโ2))) / (;32 ยท ๐ต)) ยท (logโ๐)) = (((๐ โ ๐ธ) ยท ((๐ฟ ยท (๐ธโ2)) / (;32 ยท ๐ต))) ยท (logโ๐))) |
249 | 243, 248 | breqtrd 5136 |
. . 3
โข (๐ โ ((๐ ยท 3) + ๐ถ) โค (((๐ โ ๐ธ) ยท ((๐ฟ ยท (๐ธโ2)) / (;32 ยท ๐ต))) ยท (logโ๐))) |
250 | 155, 216,
249 | 3jca 1129 |
. 2
โข (๐ โ ((4 / (๐ฟ ยท ๐ธ)) โค (โโ๐) โง (((logโ๐) / (logโ๐พ)) + 2) โค (((logโ๐) / (logโ๐พ)) / 4) โง ((๐ ยท 3) + ๐ถ) โค (((๐ โ ๐ธ) ยท ((๐ฟ ยท (๐ธโ2)) / (;32 ยท ๐ต))) ยท (logโ๐)))) |
251 | 24, 154, 250 | 3jca 1129 |
1
โข (๐ โ (๐ โ โ+ โง (1 <
๐ โง e โค
(โโ๐) โง
(โโ๐) โค
(๐ / ๐)) โง ((4 / (๐ฟ ยท ๐ธ)) โค (โโ๐) โง (((logโ๐) / (logโ๐พ)) + 2) โค (((logโ๐) / (logโ๐พ)) / 4) โง ((๐ ยท 3) + ๐ถ) โค (((๐ โ ๐ธ) ยท ((๐ฟ ยท (๐ธโ2)) / (;32 ยท ๐ต))) ยท (logโ๐))))) |