Step | Hyp | Ref
| Expression |
1 | | bposlem9.4 |
. . 3
โข (๐ โ ;64 < ๐) |
2 | | bposlem7.1 |
. . . 4
โข ๐น = (๐ โ โ โฆ ((((โโ2)
ยท (๐บโ(โโ๐))) + ((9 / 4) ยท (๐บโ(๐ / 2)))) + ((logโ2) / (โโ(2
ยท ๐))))) |
3 | | bposlem7.2 |
. . . 4
โข ๐บ = (๐ฅ โ โ+ โฆ
((logโ๐ฅ) / ๐ฅ)) |
4 | | 6nn0 12296 |
. . . . . 6
โข 6 โ
โ0 |
5 | | 4nn 12098 |
. . . . . 6
โข 4 โ
โ |
6 | 4, 5 | decnncl 12499 |
. . . . 5
โข ;64 โ โ |
7 | 6 | a1i 11 |
. . . 4
โข (๐ โ ;64 โ โ) |
8 | | bposlem9.3 |
. . . 4
โข (๐ โ ๐ โ โ) |
9 | | ere 15839 |
. . . . . . . 8
โข e โ
โ |
10 | | 8re 12111 |
. . . . . . . 8
โข 8 โ
โ |
11 | | egt2lt3 15956 |
. . . . . . . . . 10
โข (2 < e
โง e < 3) |
12 | 11 | simpri 487 |
. . . . . . . . 9
โข e <
3 |
13 | | 3lt8 12211 |
. . . . . . . . 9
โข 3 <
8 |
14 | | 3re 12095 |
. . . . . . . . . 10
โข 3 โ
โ |
15 | 9, 14, 10 | lttri 11143 |
. . . . . . . . 9
โข ((e <
3 โง 3 < 8) โ e < 8) |
16 | 12, 13, 15 | mp2an 690 |
. . . . . . . 8
โข e <
8 |
17 | 9, 10, 16 | ltleii 11140 |
. . . . . . 7
โข e โค
8 |
18 | | 0re 11019 |
. . . . . . . . 9
โข 0 โ
โ |
19 | | epos 15957 |
. . . . . . . . 9
โข 0 <
e |
20 | 18, 9, 19 | ltleii 11140 |
. . . . . . . 8
โข 0 โค
e |
21 | | 8pos 12127 |
. . . . . . . . 9
โข 0 <
8 |
22 | 18, 10, 21 | ltleii 11140 |
. . . . . . . 8
โข 0 โค
8 |
23 | | le2sq 13895 |
. . . . . . . 8
โข (((e
โ โ โง 0 โค e) โง (8 โ โ โง 0 โค 8)) โ
(e โค 8 โ (eโ2) โค (8โ2))) |
24 | 9, 20, 10, 22, 23 | mp4an 691 |
. . . . . . 7
โข (e โค 8
โ (eโ2) โค (8โ2)) |
25 | 17, 24 | mpbi 230 |
. . . . . 6
โข
(eโ2) โค (8โ2) |
26 | 10 | recni 11031 |
. . . . . . . 8
โข 8 โ
โ |
27 | 26 | sqvali 13939 |
. . . . . . 7
โข
(8โ2) = (8 ยท 8) |
28 | | 8t8e64 12600 |
. . . . . . 7
โข (8
ยท 8) = ;64 |
29 | 27, 28 | eqtri 2764 |
. . . . . 6
โข
(8โ2) = ;64 |
30 | 25, 29 | breqtri 5106 |
. . . . 5
โข
(eโ2) โค ;64 |
31 | 30 | a1i 11 |
. . . 4
โข (๐ โ (eโ2) โค ;64) |
32 | 9 | resqcli 13945 |
. . . . . 6
โข
(eโ2) โ โ |
33 | 32 | a1i 11 |
. . . . 5
โข (๐ โ (eโ2) โ
โ) |
34 | 6 | nnrei 12024 |
. . . . . 6
โข ;64 โ โ |
35 | 34 | a1i 11 |
. . . . 5
โข (๐ โ ;64 โ โ) |
36 | 8 | nnred 12030 |
. . . . 5
โข (๐ โ ๐ โ โ) |
37 | | ltle 11105 |
. . . . . . 7
โข ((;64 โ โ โง ๐ โ โ) โ (;64 < ๐ โ ;64 โค ๐)) |
38 | 34, 36, 37 | sylancr 588 |
. . . . . 6
โข (๐ โ (;64 < ๐ โ ;64 โค ๐)) |
39 | 1, 38 | mpd 15 |
. . . . 5
โข (๐ โ ;64 โค ๐) |
40 | 33, 35, 36, 31, 39 | letrd 11174 |
. . . 4
โข (๐ โ (eโ2) โค ๐) |
41 | 2, 3, 7, 8, 31, 40 | bposlem7 26479 |
. . 3
โข (๐ โ (;64 < ๐ โ (๐นโ๐) < (๐นโ;64))) |
42 | 1, 41 | mpd 15 |
. 2
โข (๐ โ (๐นโ๐) < (๐นโ;64)) |
43 | 2, 3 | bposlem8 26480 |
. . . . 5
โข ((๐นโ;64) โ โ โง (๐นโ;64) < (logโ2)) |
44 | 43 | a1i 11 |
. . . 4
โข (๐ โ ((๐นโ;64) โ โ โง (๐นโ;64) < (logโ2))) |
45 | 44 | simpld 496 |
. . 3
โข (๐ โ (๐นโ;64) โ โ) |
46 | | 2fveq3 6805 |
. . . . . . . . 9
โข (๐ = ๐ โ (๐บโ(โโ๐)) = (๐บโ(โโ๐))) |
47 | 46 | oveq2d 7319 |
. . . . . . . 8
โข (๐ = ๐ โ ((โโ2) ยท (๐บโ(โโ๐))) = ((โโ2)
ยท (๐บโ(โโ๐)))) |
48 | | fvoveq1 7326 |
. . . . . . . . 9
โข (๐ = ๐ โ (๐บโ(๐ / 2)) = (๐บโ(๐ / 2))) |
49 | 48 | oveq2d 7319 |
. . . . . . . 8
โข (๐ = ๐ โ ((9 / 4) ยท (๐บโ(๐ / 2))) = ((9 / 4) ยท (๐บโ(๐ / 2)))) |
50 | 47, 49 | oveq12d 7321 |
. . . . . . 7
โข (๐ = ๐ โ (((โโ2) ยท (๐บโ(โโ๐))) + ((9 / 4) ยท (๐บโ(๐ / 2)))) = (((โโ2) ยท
(๐บโ(โโ๐))) + ((9 / 4) ยท (๐บโ(๐ / 2))))) |
51 | | oveq2 7311 |
. . . . . . . . 9
โข (๐ = ๐ โ (2 ยท ๐) = (2 ยท ๐)) |
52 | 51 | fveq2d 6804 |
. . . . . . . 8
โข (๐ = ๐ โ (โโ(2 ยท ๐)) = (โโ(2 ยท
๐))) |
53 | 52 | oveq2d 7319 |
. . . . . . 7
โข (๐ = ๐ โ ((logโ2) / (โโ(2
ยท ๐))) =
((logโ2) / (โโ(2 ยท ๐)))) |
54 | 50, 53 | oveq12d 7321 |
. . . . . 6
โข (๐ = ๐ โ ((((โโ2) ยท (๐บโ(โโ๐))) + ((9 / 4) ยท (๐บโ(๐ / 2)))) + ((logโ2) / (โโ(2
ยท ๐)))) =
((((โโ2) ยท (๐บโ(โโ๐))) + ((9 / 4) ยท (๐บโ(๐ / 2)))) + ((logโ2) /
(โโ(2 ยท ๐))))) |
55 | | ovex 7336 |
. . . . . 6
โข
((((โโ2) ยท (๐บโ(โโ๐))) + ((9 / 4) ยท (๐บโ(๐ / 2)))) + ((logโ2) /
(โโ(2 ยท ๐)))) โ V |
56 | 54, 2, 55 | fvmpt 6903 |
. . . . 5
โข (๐ โ โ โ (๐นโ๐) = ((((โโ2) ยท (๐บโ(โโ๐))) + ((9 / 4) ยท (๐บโ(๐ / 2)))) + ((logโ2) /
(โโ(2 ยท ๐))))) |
57 | 8, 56 | syl 17 |
. . . 4
โข (๐ โ (๐นโ๐) = ((((โโ2) ยท (๐บโ(โโ๐))) + ((9 / 4) ยท (๐บโ(๐ / 2)))) + ((logโ2) /
(โโ(2 ยท ๐))))) |
58 | | sqrt2re 16000 |
. . . . . . 7
โข
(โโ2) โ โ |
59 | 8 | nnrpd 12812 |
. . . . . . . . . 10
โข (๐ โ ๐ โ
โ+) |
60 | 59 | rpsqrtcld 15164 |
. . . . . . . . 9
โข (๐ โ (โโ๐) โ
โ+) |
61 | | fveq2 6800 |
. . . . . . . . . . 11
โข (๐ฅ = (โโ๐) โ (logโ๐ฅ) =
(logโ(โโ๐))) |
62 | | id 22 |
. . . . . . . . . . 11
โข (๐ฅ = (โโ๐) โ ๐ฅ = (โโ๐)) |
63 | 61, 62 | oveq12d 7321 |
. . . . . . . . . 10
โข (๐ฅ = (โโ๐) โ ((logโ๐ฅ) / ๐ฅ) = ((logโ(โโ๐)) / (โโ๐))) |
64 | | ovex 7336 |
. . . . . . . . . 10
โข
((logโ(โโ๐)) / (โโ๐)) โ V |
65 | 63, 3, 64 | fvmpt 6903 |
. . . . . . . . 9
โข
((โโ๐)
โ โ+ โ (๐บโ(โโ๐)) = ((logโ(โโ๐)) / (โโ๐))) |
66 | 60, 65 | syl 17 |
. . . . . . . 8
โข (๐ โ (๐บโ(โโ๐)) = ((logโ(โโ๐)) / (โโ๐))) |
67 | 60 | relogcld 25819 |
. . . . . . . . 9
โข (๐ โ
(logโ(โโ๐)) โ โ) |
68 | 67, 60 | rerpdivcld 12845 |
. . . . . . . 8
โข (๐ โ
((logโ(โโ๐)) / (โโ๐)) โ โ) |
69 | 66, 68 | eqeltrd 2837 |
. . . . . . 7
โข (๐ โ (๐บโ(โโ๐)) โ โ) |
70 | | remulcl 10998 |
. . . . . . 7
โข
(((โโ2) โ โ โง (๐บโ(โโ๐)) โ โ) โ ((โโ2)
ยท (๐บโ(โโ๐))) โ โ) |
71 | 58, 69, 70 | sylancr 588 |
. . . . . 6
โข (๐ โ ((โโ2)
ยท (๐บโ(โโ๐))) โ โ) |
72 | | 9re 12114 |
. . . . . . . 8
โข 9 โ
โ |
73 | | 4re 12099 |
. . . . . . . 8
โข 4 โ
โ |
74 | | 4ne0 12123 |
. . . . . . . 8
โข 4 โ
0 |
75 | 72, 73, 74 | redivcli 11784 |
. . . . . . 7
โข (9 / 4)
โ โ |
76 | 59 | rphalfcld 12826 |
. . . . . . . . 9
โข (๐ โ (๐ / 2) โ
โ+) |
77 | | fveq2 6800 |
. . . . . . . . . . 11
โข (๐ฅ = (๐ / 2) โ (logโ๐ฅ) = (logโ(๐ / 2))) |
78 | | id 22 |
. . . . . . . . . . 11
โข (๐ฅ = (๐ / 2) โ ๐ฅ = (๐ / 2)) |
79 | 77, 78 | oveq12d 7321 |
. . . . . . . . . 10
โข (๐ฅ = (๐ / 2) โ ((logโ๐ฅ) / ๐ฅ) = ((logโ(๐ / 2)) / (๐ / 2))) |
80 | | ovex 7336 |
. . . . . . . . . 10
โข
((logโ(๐ / 2))
/ (๐ / 2)) โ
V |
81 | 79, 3, 80 | fvmpt 6903 |
. . . . . . . . 9
โข ((๐ / 2) โ โ+
โ (๐บโ(๐ / 2)) = ((logโ(๐ / 2)) / (๐ / 2))) |
82 | 76, 81 | syl 17 |
. . . . . . . 8
โข (๐ โ (๐บโ(๐ / 2)) = ((logโ(๐ / 2)) / (๐ / 2))) |
83 | 76 | relogcld 25819 |
. . . . . . . . 9
โข (๐ โ (logโ(๐ / 2)) โ
โ) |
84 | 83, 76 | rerpdivcld 12845 |
. . . . . . . 8
โข (๐ โ ((logโ(๐ / 2)) / (๐ / 2)) โ โ) |
85 | 82, 84 | eqeltrd 2837 |
. . . . . . 7
โข (๐ โ (๐บโ(๐ / 2)) โ โ) |
86 | | remulcl 10998 |
. . . . . . 7
โข (((9 / 4)
โ โ โง (๐บโ(๐ / 2)) โ โ) โ ((9 / 4)
ยท (๐บโ(๐ / 2))) โ
โ) |
87 | 75, 85, 86 | sylancr 588 |
. . . . . 6
โข (๐ โ ((9 / 4) ยท (๐บโ(๐ / 2))) โ โ) |
88 | 71, 87 | readdcld 11046 |
. . . . 5
โข (๐ โ (((โโ2)
ยท (๐บโ(โโ๐))) + ((9 / 4) ยท (๐บโ(๐ / 2)))) โ โ) |
89 | | 2rp 12777 |
. . . . . . 7
โข 2 โ
โ+ |
90 | | relogcl 25772 |
. . . . . . 7
โข (2 โ
โ+ โ (logโ2) โ โ) |
91 | 89, 90 | ax-mp 5 |
. . . . . 6
โข
(logโ2) โ โ |
92 | | rpmulcl 12795 |
. . . . . . . 8
โข ((2
โ โ+ โง ๐ โ โ+) โ (2
ยท ๐) โ
โ+) |
93 | 89, 59, 92 | sylancr 588 |
. . . . . . 7
โข (๐ โ (2 ยท ๐) โ
โ+) |
94 | 93 | rpsqrtcld 15164 |
. . . . . 6
โข (๐ โ (โโ(2 ยท
๐)) โ
โ+) |
95 | | rerpdivcl 12802 |
. . . . . 6
โข
(((logโ2) โ โ โง (โโ(2 ยท ๐)) โ โ+)
โ ((logโ2) / (โโ(2 ยท ๐))) โ โ) |
96 | 91, 94, 95 | sylancr 588 |
. . . . 5
โข (๐ โ ((logโ2) /
(โโ(2 ยท ๐))) โ โ) |
97 | 88, 96 | readdcld 11046 |
. . . 4
โข (๐ โ ((((โโ2)
ยท (๐บโ(โโ๐))) + ((9 / 4) ยท (๐บโ(๐ / 2)))) + ((logโ2) /
(โโ(2 ยท ๐)))) โ โ) |
98 | 57, 97 | eqeltrd 2837 |
. . 3
โข (๐ โ (๐นโ๐) โ โ) |
99 | 91 | a1i 11 |
. . . 4
โข (๐ โ (logโ2) โ
โ) |
100 | 44 | simprd 497 |
. . . 4
โข (๐ โ (๐นโ;64) < (logโ2)) |
101 | | nnrp 12783 |
. . . . . . . . . . 11
โข (4 โ
โ โ 4 โ โ+) |
102 | 5, 101 | ax-mp 5 |
. . . . . . . . . 10
โข 4 โ
โ+ |
103 | | relogcl 25772 |
. . . . . . . . . 10
โข (4 โ
โ+ โ (logโ4) โ โ) |
104 | 102, 103 | ax-mp 5 |
. . . . . . . . 9
โข
(logโ4) โ โ |
105 | | remulcl 10998 |
. . . . . . . . 9
โข ((๐ โ โ โง
(logโ4) โ โ) โ (๐ ยท (logโ4)) โ
โ) |
106 | 36, 104, 105 | sylancl 587 |
. . . . . . . 8
โข (๐ โ (๐ ยท (logโ4)) โ
โ) |
107 | 59 | relogcld 25819 |
. . . . . . . 8
โข (๐ โ (logโ๐) โ
โ) |
108 | 106, 107 | resubcld 11445 |
. . . . . . 7
โข (๐ โ ((๐ ยท (logโ4)) โ
(logโ๐)) โ
โ) |
109 | | rpre 12780 |
. . . . . . . . . . . . 13
โข ((2
ยท ๐) โ
โ+ โ (2 ยท ๐) โ โ) |
110 | | rpge0 12785 |
. . . . . . . . . . . . 13
โข ((2
ยท ๐) โ
โ+ โ 0 โค (2 ยท ๐)) |
111 | 109, 110 | resqrtcld 15170 |
. . . . . . . . . . . 12
โข ((2
ยท ๐) โ
โ+ โ (โโ(2 ยท ๐)) โ โ) |
112 | 93, 111 | syl 17 |
. . . . . . . . . . 11
โข (๐ โ (โโ(2 ยท
๐)) โ
โ) |
113 | | 3nn 12094 |
. . . . . . . . . . 11
โข 3 โ
โ |
114 | | nndivre 12056 |
. . . . . . . . . . 11
โข
(((โโ(2 ยท ๐)) โ โ โง 3 โ โ)
โ ((โโ(2 ยท ๐)) / 3) โ โ) |
115 | 112, 113,
114 | sylancl 587 |
. . . . . . . . . 10
โข (๐ โ ((โโ(2
ยท ๐)) / 3) โ
โ) |
116 | | 2re 12089 |
. . . . . . . . . 10
โข 2 โ
โ |
117 | | readdcl 10996 |
. . . . . . . . . 10
โข
((((โโ(2 ยท ๐)) / 3) โ โ โง 2 โ
โ) โ (((โโ(2 ยท ๐)) / 3) + 2) โ
โ) |
118 | 115, 116,
117 | sylancl 587 |
. . . . . . . . 9
โข (๐ โ (((โโ(2
ยท ๐)) / 3) + 2)
โ โ) |
119 | 93 | relogcld 25819 |
. . . . . . . . 9
โข (๐ โ (logโ(2 ยท
๐)) โ
โ) |
120 | 118, 119 | remulcld 11047 |
. . . . . . . 8
โข (๐ โ ((((โโ(2
ยท ๐)) / 3) + 2)
ยท (logโ(2 ยท ๐))) โ โ) |
121 | | remulcl 10998 |
. . . . . . . . . . . 12
โข ((4
โ โ โง ๐
โ โ) โ (4 ยท ๐) โ โ) |
122 | 73, 36, 121 | sylancr 588 |
. . . . . . . . . . 11
โข (๐ โ (4 ยท ๐) โ
โ) |
123 | | nndivre 12056 |
. . . . . . . . . . 11
โข (((4
ยท ๐) โ โ
โง 3 โ โ) โ ((4 ยท ๐) / 3) โ โ) |
124 | 122, 113,
123 | sylancl 587 |
. . . . . . . . . 10
โข (๐ โ ((4 ยท ๐) / 3) โ
โ) |
125 | | 5re 12102 |
. . . . . . . . . 10
โข 5 โ
โ |
126 | | resubcl 11327 |
. . . . . . . . . 10
โข ((((4
ยท ๐) / 3) โ
โ โง 5 โ โ) โ (((4 ยท ๐) / 3) โ 5) โ
โ) |
127 | 124, 125,
126 | sylancl 587 |
. . . . . . . . 9
โข (๐ โ (((4 ยท ๐) / 3) โ 5) โ
โ) |
128 | | remulcl 10998 |
. . . . . . . . 9
โข (((((4
ยท ๐) / 3) โ 5)
โ โ โง (logโ2) โ โ) โ ((((4 ยท ๐) / 3) โ 5) ยท
(logโ2)) โ โ) |
129 | 127, 91, 128 | sylancl 587 |
. . . . . . . 8
โข (๐ โ ((((4 ยท ๐) / 3) โ 5) ยท
(logโ2)) โ โ) |
130 | 120, 129 | readdcld 11046 |
. . . . . . 7
โข (๐ โ (((((โโ(2
ยท ๐)) / 3) + 2)
ยท (logโ(2 ยท ๐))) + ((((4 ยท ๐) / 3) โ 5) ยท (logโ2)))
โ โ) |
131 | | remulcl 10998 |
. . . . . . . . 9
โข ((((4
ยท ๐) / 3) โ
โ โง (logโ2) โ โ) โ (((4 ยท ๐) / 3) ยท (logโ2))
โ โ) |
132 | 124, 91, 131 | sylancl 587 |
. . . . . . . 8
โข (๐ โ (((4 ยท ๐) / 3) ยท (logโ2))
โ โ) |
133 | 132, 107 | resubcld 11445 |
. . . . . . 7
โข (๐ โ ((((4 ยท ๐) / 3) ยท (logโ2))
โ (logโ๐))
โ โ) |
134 | 8 | nnzd 12467 |
. . . . . . . . . . 11
โข (๐ โ ๐ โ โค) |
135 | | df-5 12081 |
. . . . . . . . . . . 12
โข 5 = (4 +
1) |
136 | 73 | a1i 11 |
. . . . . . . . . . . . . 14
โข (๐ โ 4 โ
โ) |
137 | | 6nn 12104 |
. . . . . . . . . . . . . . . 16
โข 6 โ
โ |
138 | | 4nn0 12294 |
. . . . . . . . . . . . . . . 16
โข 4 โ
โ0 |
139 | | 4lt10 12615 |
. . . . . . . . . . . . . . . 16
โข 4 <
;10 |
140 | 137, 138,
138, 139 | declti 12517 |
. . . . . . . . . . . . . . 15
โข 4 <
;64 |
141 | 140 | a1i 11 |
. . . . . . . . . . . . . 14
โข (๐ โ 4 < ;64) |
142 | 136, 35, 36, 141, 1 | lttrd 11178 |
. . . . . . . . . . . . 13
โข (๐ โ 4 < ๐) |
143 | | 4z 12396 |
. . . . . . . . . . . . . 14
โข 4 โ
โค |
144 | | zltp1le 12412 |
. . . . . . . . . . . . . 14
โข ((4
โ โค โง ๐
โ โค) โ (4 < ๐ โ (4 + 1) โค ๐)) |
145 | 143, 134,
144 | sylancr 588 |
. . . . . . . . . . . . 13
โข (๐ โ (4 < ๐ โ (4 + 1) โค ๐)) |
146 | 142, 145 | mpbid 232 |
. . . . . . . . . . . 12
โข (๐ โ (4 + 1) โค ๐) |
147 | 135, 146 | eqbrtrid 5116 |
. . . . . . . . . . 11
โข (๐ โ 5 โค ๐) |
148 | | 5nn 12101 |
. . . . . . . . . . . . 13
โข 5 โ
โ |
149 | 148 | nnzi 12386 |
. . . . . . . . . . . 12
โข 5 โ
โค |
150 | 149 | eluz1i 12632 |
. . . . . . . . . . 11
โข (๐ โ
(โคโฅโ5) โ (๐ โ โค โง 5 โค ๐)) |
151 | 134, 147,
150 | sylanbrc 584 |
. . . . . . . . . 10
โข (๐ โ ๐ โ
(โคโฅโ5)) |
152 | | bposlem9.5 |
. . . . . . . . . . 11
โข (๐ โ ยฌ โ๐ โ โ (๐ < ๐ โง ๐ โค (2 ยท ๐))) |
153 | | breq2 5085 |
. . . . . . . . . . . . 13
โข (๐ = ๐ โ (๐ < ๐ โ ๐ < ๐)) |
154 | | breq1 5084 |
. . . . . . . . . . . . 13
โข (๐ = ๐ โ (๐ โค (2 ยท ๐) โ ๐ โค (2 ยท ๐))) |
155 | 153, 154 | anbi12d 632 |
. . . . . . . . . . . 12
โข (๐ = ๐ โ ((๐ < ๐ โง ๐ โค (2 ยท ๐)) โ (๐ < ๐ โง ๐ โค (2 ยท ๐)))) |
156 | 155 | cbvrexvw 3223 |
. . . . . . . . . . 11
โข
(โ๐ โ
โ (๐ < ๐ โง ๐ โค (2 ยท ๐)) โ โ๐ โ โ (๐ < ๐ โง ๐ โค (2 ยท ๐))) |
157 | 152, 156 | sylnib 329 |
. . . . . . . . . 10
โข (๐ โ ยฌ โ๐ โ โ (๐ < ๐ โง ๐ โค (2 ยท ๐))) |
158 | | eqid 2736 |
. . . . . . . . . 10
โข (๐ โ โ โฆ if(๐ โ โ, (๐โ(๐ pCnt ((2 ยท ๐)C๐))), 1)) = (๐ โ โ โฆ if(๐ โ โ, (๐โ(๐ pCnt ((2 ยท ๐)C๐))), 1)) |
159 | | eqid 2736 |
. . . . . . . . . 10
โข
(โโ((2 ยท ๐) / 3)) = (โโ((2 ยท ๐) / 3)) |
160 | | eqid 2736 |
. . . . . . . . . 10
โข
(โโ(โโ(2 ยท ๐))) = (โโ(โโ(2
ยท ๐))) |
161 | 151, 157,
158, 159, 160 | bposlem6 26478 |
. . . . . . . . 9
โข (๐ โ ((4โ๐) / ๐) < (((2 ยท ๐)โ๐(((โโ(2
ยท ๐)) / 3) + 2))
ยท (2โ๐(((4 ยท ๐) / 3) โ 5)))) |
162 | | reexplog 25791 |
. . . . . . . . . . . 12
โข ((4
โ โ+ โง ๐ โ โค) โ (4โ๐) = (expโ(๐ ยท
(logโ4)))) |
163 | 102, 134,
162 | sylancr 588 |
. . . . . . . . . . 11
โข (๐ โ (4โ๐) = (expโ(๐ ยท (logโ4)))) |
164 | 59 | reeflogd 25820 |
. . . . . . . . . . . 12
โข (๐ โ
(expโ(logโ๐)) =
๐) |
165 | 164 | eqcomd 2742 |
. . . . . . . . . . 11
โข (๐ โ ๐ = (expโ(logโ๐))) |
166 | 163, 165 | oveq12d 7321 |
. . . . . . . . . 10
โข (๐ โ ((4โ๐) / ๐) = ((expโ(๐ ยท (logโ4))) /
(expโ(logโ๐)))) |
167 | 106 | recnd 11045 |
. . . . . . . . . . 11
โข (๐ โ (๐ ยท (logโ4)) โ
โ) |
168 | 107 | recnd 11045 |
. . . . . . . . . . 11
โข (๐ โ (logโ๐) โ
โ) |
169 | | efsub 15850 |
. . . . . . . . . . 11
โข (((๐ ยท (logโ4)) โ
โ โง (logโ๐)
โ โ) โ (expโ((๐ ยท (logโ4)) โ
(logโ๐))) =
((expโ(๐ ยท
(logโ4))) / (expโ(logโ๐)))) |
170 | 167, 168,
169 | syl2anc 585 |
. . . . . . . . . 10
โข (๐ โ (expโ((๐ ยท (logโ4)) โ
(logโ๐))) =
((expโ(๐ ยท
(logโ4))) / (expโ(logโ๐)))) |
171 | 166, 170 | eqtr4d 2779 |
. . . . . . . . 9
โข (๐ โ ((4โ๐) / ๐) = (expโ((๐ ยท (logโ4)) โ
(logโ๐)))) |
172 | 93 | rpcnd 12816 |
. . . . . . . . . . . 12
โข (๐ โ (2 ยท ๐) โ
โ) |
173 | 93 | rpne0d 12819 |
. . . . . . . . . . . 12
โข (๐ โ (2 ยท ๐) โ 0) |
174 | 118 | recnd 11045 |
. . . . . . . . . . . 12
โข (๐ โ (((โโ(2
ยท ๐)) / 3) + 2)
โ โ) |
175 | 172, 173,
174 | cxpefd 25908 |
. . . . . . . . . . 11
โข (๐ โ ((2 ยท ๐)โ๐(((โโ(2
ยท ๐)) / 3) + 2)) =
(expโ((((โโ(2 ยท ๐)) / 3) + 2) ยท (logโ(2 ยท
๐))))) |
176 | | 2cn 12090 |
. . . . . . . . . . . 12
โข 2 โ
โ |
177 | | 2ne0 12119 |
. . . . . . . . . . . 12
โข 2 โ
0 |
178 | 127 | recnd 11045 |
. . . . . . . . . . . 12
โข (๐ โ (((4 ยท ๐) / 3) โ 5) โ
โ) |
179 | | cxpef 25861 |
. . . . . . . . . . . 12
โข ((2
โ โ โง 2 โ 0 โง (((4 ยท ๐) / 3) โ 5) โ โ) โ
(2โ๐(((4 ยท ๐) / 3) โ 5)) = (expโ((((4
ยท ๐) / 3) โ 5)
ยท (logโ2)))) |
180 | 176, 177,
178, 179 | mp3an12i 1465 |
. . . . . . . . . . 11
โข (๐ โ
(2โ๐(((4 ยท ๐) / 3) โ 5)) = (expโ((((4
ยท ๐) / 3) โ 5)
ยท (logโ2)))) |
181 | 175, 180 | oveq12d 7321 |
. . . . . . . . . 10
โข (๐ โ (((2 ยท ๐)โ๐(((โโ(2
ยท ๐)) / 3) + 2))
ยท (2โ๐(((4 ยท ๐) / 3) โ 5))) =
((expโ((((โโ(2 ยท ๐)) / 3) + 2) ยท (logโ(2 ยท
๐)))) ยท
(expโ((((4 ยท ๐)
/ 3) โ 5) ยท (logโ2))))) |
182 | 120 | recnd 11045 |
. . . . . . . . . . 11
โข (๐ โ ((((โโ(2
ยท ๐)) / 3) + 2)
ยท (logโ(2 ยท ๐))) โ โ) |
183 | 129 | recnd 11045 |
. . . . . . . . . . 11
โข (๐ โ ((((4 ยท ๐) / 3) โ 5) ยท
(logโ2)) โ โ) |
184 | | efadd 15844 |
. . . . . . . . . . 11
โข
((((((โโ(2 ยท ๐)) / 3) + 2) ยท (logโ(2 ยท
๐))) โ โ โง
((((4 ยท ๐) / 3)
โ 5) ยท (logโ2)) โ โ) โ
(expโ(((((โโ(2 ยท ๐)) / 3) + 2) ยท (logโ(2 ยท
๐))) + ((((4 ยท ๐) / 3) โ 5) ยท
(logโ2)))) = ((expโ((((โโ(2 ยท ๐)) / 3) + 2) ยท (logโ(2 ยท
๐)))) ยท
(expโ((((4 ยท ๐) / 3) โ 5) ยท
(logโ2))))) |
185 | 182, 183,
184 | syl2anc 585 |
. . . . . . . . . 10
โข (๐ โ
(expโ(((((โโ(2 ยท ๐)) / 3) + 2) ยท (logโ(2 ยท
๐))) + ((((4 ยท ๐) / 3) โ 5) ยท
(logโ2)))) = ((expโ((((โโ(2 ยท ๐)) / 3) + 2) ยท (logโ(2 ยท
๐)))) ยท
(expโ((((4 ยท ๐) / 3) โ 5) ยท
(logโ2))))) |
186 | 181, 185 | eqtr4d 2779 |
. . . . . . . . 9
โข (๐ โ (((2 ยท ๐)โ๐(((โโ(2
ยท ๐)) / 3) + 2))
ยท (2โ๐(((4 ยท ๐) / 3) โ 5))) =
(expโ(((((โโ(2 ยท ๐)) / 3) + 2) ยท (logโ(2 ยท
๐))) + ((((4 ยท ๐) / 3) โ 5) ยท
(logโ2))))) |
187 | 161, 171,
186 | 3brtr3d 5112 |
. . . . . . . 8
โข (๐ โ (expโ((๐ ยท (logโ4)) โ
(logโ๐))) <
(expโ(((((โโ(2 ยท ๐)) / 3) + 2) ยท (logโ(2 ยท
๐))) + ((((4 ยท ๐) / 3) โ 5) ยท
(logโ2))))) |
188 | | eflt 15867 |
. . . . . . . . 9
โข ((((๐ ยท (logโ4)) โ
(logโ๐)) โ
โ โง (((((โโ(2 ยท ๐)) / 3) + 2) ยท (logโ(2 ยท
๐))) + ((((4 ยท ๐) / 3) โ 5) ยท
(logโ2))) โ โ) โ (((๐ ยท (logโ4)) โ
(logโ๐)) <
(((((โโ(2 ยท ๐)) / 3) + 2) ยท (logโ(2 ยท
๐))) + ((((4 ยท ๐) / 3) โ 5) ยท
(logโ2))) โ (expโ((๐ ยท (logโ4)) โ
(logโ๐))) <
(expโ(((((โโ(2 ยท ๐)) / 3) + 2) ยท (logโ(2 ยท
๐))) + ((((4 ยท ๐) / 3) โ 5) ยท
(logโ2)))))) |
189 | 108, 130,
188 | syl2anc 585 |
. . . . . . . 8
โข (๐ โ (((๐ ยท (logโ4)) โ
(logโ๐)) <
(((((โโ(2 ยท ๐)) / 3) + 2) ยท (logโ(2 ยท
๐))) + ((((4 ยท ๐) / 3) โ 5) ยท
(logโ2))) โ (expโ((๐ ยท (logโ4)) โ
(logโ๐))) <
(expโ(((((โโ(2 ยท ๐)) / 3) + 2) ยท (logโ(2 ยท
๐))) + ((((4 ยท ๐) / 3) โ 5) ยท
(logโ2)))))) |
190 | 187, 189 | mpbird 258 |
. . . . . . 7
โข (๐ โ ((๐ ยท (logโ4)) โ
(logโ๐)) <
(((((โโ(2 ยท ๐)) / 3) + 2) ยท (logโ(2 ยท
๐))) + ((((4 ยท ๐) / 3) โ 5) ยท
(logโ2)))) |
191 | 108, 130,
133, 190 | ltsub1dd 11629 |
. . . . . 6
โข (๐ โ (((๐ ยท (logโ4)) โ
(logโ๐)) โ
((((4 ยท ๐) / 3)
ยท (logโ2)) โ (logโ๐))) < ((((((โโ(2 ยท
๐)) / 3) + 2) ยท
(logโ(2 ยท ๐)))
+ ((((4 ยท ๐) / 3)
โ 5) ยท (logโ2))) โ ((((4 ยท ๐) / 3) ยท (logโ2)) โ
(logโ๐)))) |
192 | 36 | recnd 11045 |
. . . . . . . . . . 11
โข (๐ โ ๐ โ โ) |
193 | | mulcom 10999 |
. . . . . . . . . . 11
โข ((2
โ โ โง ๐
โ โ) โ (2 ยท ๐) = (๐ ยท 2)) |
194 | 176, 192,
193 | sylancr 588 |
. . . . . . . . . 10
โข (๐ โ (2 ยท ๐) = (๐ ยท 2)) |
195 | 194 | oveq1d 7318 |
. . . . . . . . 9
โข (๐ โ ((2 ยท ๐) ยท (logโ2)) =
((๐ ยท 2) ยท
(logโ2))) |
196 | 91 | recni 11031 |
. . . . . . . . . . . 12
โข
(logโ2) โ โ |
197 | | mulass 11001 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง 2 โ
โ โง (logโ2) โ โ) โ ((๐ ยท 2) ยท (logโ2)) =
(๐ ยท (2 ยท
(logโ2)))) |
198 | 176, 196,
197 | mp3an23 1453 |
. . . . . . . . . . 11
โข (๐ โ โ โ ((๐ ยท 2) ยท
(logโ2)) = (๐
ยท (2 ยท (logโ2)))) |
199 | 192, 198 | syl 17 |
. . . . . . . . . 10
โข (๐ โ ((๐ ยท 2) ยท (logโ2)) =
(๐ ยท (2 ยท
(logโ2)))) |
200 | 196 | 2timesi 12153 |
. . . . . . . . . . . 12
โข (2
ยท (logโ2)) = ((logโ2) + (logโ2)) |
201 | | relogmul 25788 |
. . . . . . . . . . . . 13
โข ((2
โ โ+ โง 2 โ โ+) โ
(logโ(2 ยท 2)) = ((logโ2) + (logโ2))) |
202 | 89, 89, 201 | mp2an 690 |
. . . . . . . . . . . 12
โข
(logโ(2 ยท 2)) = ((logโ2) +
(logโ2)) |
203 | | 2t2e4 12179 |
. . . . . . . . . . . . 13
โข (2
ยท 2) = 4 |
204 | 203 | fveq2i 6803 |
. . . . . . . . . . . 12
โข
(logโ(2 ยท 2)) = (logโ4) |
205 | 200, 202,
204 | 3eqtr2i 2770 |
. . . . . . . . . . 11
โข (2
ยท (logโ2)) = (logโ4) |
206 | 205 | oveq2i 7314 |
. . . . . . . . . 10
โข (๐ ยท (2 ยท
(logโ2))) = (๐
ยท (logโ4)) |
207 | 199, 206 | eqtrdi 2792 |
. . . . . . . . 9
โข (๐ โ ((๐ ยท 2) ยท (logโ2)) =
(๐ ยท
(logโ4))) |
208 | 195, 207 | eqtrd 2776 |
. . . . . . . 8
โข (๐ โ ((2 ยท ๐) ยท (logโ2)) =
(๐ ยท
(logโ4))) |
209 | 208 | oveq1d 7318 |
. . . . . . 7
โข (๐ โ (((2 ยท ๐) ยท (logโ2))
โ (((4 ยท ๐) /
3) ยท (logโ2))) = ((๐ ยท (logโ4)) โ (((4
ยท ๐) / 3) ยท
(logโ2)))) |
210 | 124 | recnd 11045 |
. . . . . . . . . 10
โข (๐ โ ((4 ยท ๐) / 3) โ
โ) |
211 | | 3rp 12778 |
. . . . . . . . . . . 12
โข 3 โ
โ+ |
212 | | rpdivcl 12797 |
. . . . . . . . . . . 12
โข (((2
ยท ๐) โ
โ+ โง 3 โ โ+) โ ((2 ยท
๐) / 3) โ
โ+) |
213 | 93, 211, 212 | sylancl 587 |
. . . . . . . . . . 11
โข (๐ โ ((2 ยท ๐) / 3) โ
โ+) |
214 | 213 | rpcnd 12816 |
. . . . . . . . . 10
โข (๐ โ ((2 ยท ๐) / 3) โ
โ) |
215 | | 4p2e6 12168 |
. . . . . . . . . . . . . 14
โข (4 + 2) =
6 |
216 | 215 | oveq1i 7313 |
. . . . . . . . . . . . 13
โข ((4 + 2)
ยท ๐) = (6 ยท
๐) |
217 | | 4cn 12100 |
. . . . . . . . . . . . . 14
โข 4 โ
โ |
218 | | adddir 11008 |
. . . . . . . . . . . . . 14
โข ((4
โ โ โง 2 โ โ โง ๐ โ โ) โ ((4 + 2) ยท
๐) = ((4 ยท ๐) + (2 ยท ๐))) |
219 | 217, 176,
192, 218 | mp3an12i 1465 |
. . . . . . . . . . . . 13
โข (๐ โ ((4 + 2) ยท ๐) = ((4 ยท ๐) + (2 ยท ๐))) |
220 | 216, 219 | eqtr3id 2790 |
. . . . . . . . . . . 12
โข (๐ โ (6 ยท ๐) = ((4 ยท ๐) + (2 ยท ๐))) |
221 | 220 | oveq1d 7318 |
. . . . . . . . . . 11
โข (๐ โ ((6 ยท ๐) / 3) = (((4 ยท ๐) + (2 ยท ๐)) / 3)) |
222 | | 6cn 12106 |
. . . . . . . . . . . . . 14
โข 6 โ
โ |
223 | | 3cn 12096 |
. . . . . . . . . . . . . . 15
โข 3 โ
โ |
224 | | 3ne0 12121 |
. . . . . . . . . . . . . . 15
โข 3 โ
0 |
225 | 223, 224 | pm3.2i 472 |
. . . . . . . . . . . . . 14
โข (3 โ
โ โง 3 โ 0) |
226 | | div23 11694 |
. . . . . . . . . . . . . 14
โข ((6
โ โ โง ๐
โ โ โง (3 โ โ โง 3 โ 0)) โ ((6 ยท
๐) / 3) = ((6 / 3) ยท
๐)) |
227 | 222, 225,
226 | mp3an13 1452 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ ((6
ยท ๐) / 3) = ((6 / 3)
ยท ๐)) |
228 | 192, 227 | syl 17 |
. . . . . . . . . . . 12
โข (๐ โ ((6 ยท ๐) / 3) = ((6 / 3) ยท ๐)) |
229 | | 3t2e6 12181 |
. . . . . . . . . . . . . . 15
โข (3
ยท 2) = 6 |
230 | 229 | oveq1i 7313 |
. . . . . . . . . . . . . 14
โข ((3
ยท 2) / 3) = (6 / 3) |
231 | 176, 223,
224 | divcan3i 11763 |
. . . . . . . . . . . . . 14
โข ((3
ยท 2) / 3) = 2 |
232 | 230, 231 | eqtr3i 2766 |
. . . . . . . . . . . . 13
โข (6 / 3) =
2 |
233 | 232 | oveq1i 7313 |
. . . . . . . . . . . 12
โข ((6 / 3)
ยท ๐) = (2 ยท
๐) |
234 | 228, 233 | eqtrdi 2792 |
. . . . . . . . . . 11
โข (๐ โ ((6 ยท ๐) / 3) = (2 ยท ๐)) |
235 | 122 | recnd 11045 |
. . . . . . . . . . . 12
โข (๐ โ (4 ยท ๐) โ
โ) |
236 | | remulcl 10998 |
. . . . . . . . . . . . . 14
โข ((2
โ โ โง ๐
โ โ) โ (2 ยท ๐) โ โ) |
237 | 116, 36, 236 | sylancr 588 |
. . . . . . . . . . . . 13
โข (๐ โ (2 ยท ๐) โ
โ) |
238 | 237 | recnd 11045 |
. . . . . . . . . . . 12
โข (๐ โ (2 ยท ๐) โ
โ) |
239 | | divdir 11700 |
. . . . . . . . . . . . 13
โข (((4
ยท ๐) โ โ
โง (2 ยท ๐) โ
โ โง (3 โ โ โง 3 โ 0)) โ (((4 ยท ๐) + (2 ยท ๐)) / 3) = (((4 ยท ๐) / 3) + ((2 ยท ๐) / 3))) |
240 | 225, 239 | mp3an3 1450 |
. . . . . . . . . . . 12
โข (((4
ยท ๐) โ โ
โง (2 ยท ๐) โ
โ) โ (((4 ยท ๐) + (2 ยท ๐)) / 3) = (((4 ยท ๐) / 3) + ((2 ยท ๐) / 3))) |
241 | 235, 238,
240 | syl2anc 585 |
. . . . . . . . . . 11
โข (๐ โ (((4 ยท ๐) + (2 ยท ๐)) / 3) = (((4 ยท ๐) / 3) + ((2 ยท ๐) / 3))) |
242 | 221, 234,
241 | 3eqtr3d 2784 |
. . . . . . . . . 10
โข (๐ โ (2 ยท ๐) = (((4 ยท ๐) / 3) + ((2 ยท ๐) / 3))) |
243 | 210, 214,
242 | mvrladdd 11430 |
. . . . . . . . 9
โข (๐ โ ((2 ยท ๐) โ ((4 ยท ๐) / 3)) = ((2 ยท ๐) / 3)) |
244 | 243 | oveq1d 7318 |
. . . . . . . 8
โข (๐ โ (((2 ยท ๐) โ ((4 ยท ๐) / 3)) ยท (logโ2))
= (((2 ยท ๐) / 3)
ยท (logโ2))) |
245 | 99 | recnd 11045 |
. . . . . . . . 9
โข (๐ โ (logโ2) โ
โ) |
246 | 238, 210,
245 | subdird 11474 |
. . . . . . . 8
โข (๐ โ (((2 ยท ๐) โ ((4 ยท ๐) / 3)) ยท (logโ2))
= (((2 ยท ๐) ยท
(logโ2)) โ (((4 ยท ๐) / 3) ยท
(logโ2)))) |
247 | 244, 246 | eqtr3d 2778 |
. . . . . . 7
โข (๐ โ (((2 ยท ๐) / 3) ยท (logโ2)) =
(((2 ยท ๐) ยท
(logโ2)) โ (((4 ยท ๐) / 3) ยท
(logโ2)))) |
248 | 132 | recnd 11045 |
. . . . . . . 8
โข (๐ โ (((4 ยท ๐) / 3) ยท (logโ2))
โ โ) |
249 | 167, 248,
168 | nnncan2d 11409 |
. . . . . . 7
โข (๐ โ (((๐ ยท (logโ4)) โ
(logโ๐)) โ
((((4 ยท ๐) / 3)
ยท (logโ2)) โ (logโ๐))) = ((๐ ยท (logโ4)) โ (((4
ยท ๐) / 3) ยท
(logโ2)))) |
250 | 209, 247,
249 | 3eqtr4d 2786 |
. . . . . 6
โข (๐ โ (((2 ยท ๐) / 3) ยท (logโ2)) =
(((๐ ยท
(logโ4)) โ (logโ๐)) โ ((((4 ยท ๐) / 3) ยท (logโ2)) โ
(logโ๐)))) |
251 | 115 | recnd 11045 |
. . . . . . . . . 10
โข (๐ โ ((โโ(2
ยท ๐)) / 3) โ
โ) |
252 | 176 | a1i 11 |
. . . . . . . . . 10
โข (๐ โ 2 โ
โ) |
253 | 119 | recnd 11045 |
. . . . . . . . . 10
โข (๐ โ (logโ(2 ยท
๐)) โ
โ) |
254 | 251, 252,
253 | adddird 11042 |
. . . . . . . . 9
โข (๐ โ ((((โโ(2
ยท ๐)) / 3) + 2)
ยท (logโ(2 ยท ๐))) = ((((โโ(2 ยท ๐)) / 3) ยท (logโ(2
ยท ๐))) + (2 ยท
(logโ(2 ยท ๐))))) |
255 | | relogmul 25788 |
. . . . . . . . . . . . 13
โข ((2
โ โ+ โง ๐ โ โ+) โ
(logโ(2 ยท ๐))
= ((logโ2) + (logโ๐))) |
256 | 89, 59, 255 | sylancr 588 |
. . . . . . . . . . . 12
โข (๐ โ (logโ(2 ยท
๐)) = ((logโ2) +
(logโ๐))) |
257 | 256 | oveq2d 7319 |
. . . . . . . . . . 11
โข (๐ โ (2 ยท (logโ(2
ยท ๐))) = (2 ยท
((logโ2) + (logโ๐)))) |
258 | 252, 245,
168 | adddid 11041 |
. . . . . . . . . . 11
โข (๐ โ (2 ยท ((logโ2)
+ (logโ๐))) = ((2
ยท (logโ2)) + (2 ยท (logโ๐)))) |
259 | 257, 258 | eqtrd 2776 |
. . . . . . . . . 10
โข (๐ โ (2 ยท (logโ(2
ยท ๐))) = ((2
ยท (logโ2)) + (2 ยท (logโ๐)))) |
260 | 259 | oveq2d 7319 |
. . . . . . . . 9
โข (๐ โ ((((โโ(2
ยท ๐)) / 3) ยท
(logโ(2 ยท ๐)))
+ (2 ยท (logโ(2 ยท ๐)))) = ((((โโ(2 ยท ๐)) / 3) ยท (logโ(2
ยท ๐))) + ((2
ยท (logโ2)) + (2 ยท (logโ๐))))) |
261 | 254, 260 | eqtrd 2776 |
. . . . . . . 8
โข (๐ โ ((((โโ(2
ยท ๐)) / 3) + 2)
ยท (logโ(2 ยท ๐))) = ((((โโ(2 ยท ๐)) / 3) ยท (logโ(2
ยท ๐))) + ((2
ยท (logโ2)) + (2 ยท (logโ๐))))) |
262 | | 5cn 12103 |
. . . . . . . . . . . 12
โข 5 โ
โ |
263 | 262 | a1i 11 |
. . . . . . . . . . 11
โข (๐ โ 5 โ
โ) |
264 | 210, 263,
245 | subdird 11474 |
. . . . . . . . . 10
โข (๐ โ ((((4 ยท ๐) / 3) โ 5) ยท
(logโ2)) = ((((4 ยท ๐) / 3) ยท (logโ2)) โ (5
ยท (logโ2)))) |
265 | 264 | oveq1d 7318 |
. . . . . . . . 9
โข (๐ โ (((((4 ยท ๐) / 3) โ 5) ยท
(logโ2)) โ ((((4 ยท ๐) / 3) ยท (logโ2)) โ
(logโ๐))) = (((((4
ยท ๐) / 3) ยท
(logโ2)) โ (5 ยท (logโ2))) โ ((((4 ยท ๐) / 3) ยท (logโ2))
โ (logโ๐)))) |
266 | 262, 196 | mulcli 11024 |
. . . . . . . . . . 11
โข (5
ยท (logโ2)) โ โ |
267 | 266 | a1i 11 |
. . . . . . . . . 10
โข (๐ โ (5 ยท (logโ2))
โ โ) |
268 | 248, 267,
168 | nnncan1d 11408 |
. . . . . . . . 9
โข (๐ โ (((((4 ยท ๐) / 3) ยท (logโ2))
โ (5 ยท (logโ2))) โ ((((4 ยท ๐) / 3) ยท (logโ2)) โ
(logโ๐))) =
((logโ๐) โ (5
ยท (logโ2)))) |
269 | 265, 268 | eqtrd 2776 |
. . . . . . . 8
โข (๐ โ (((((4 ยท ๐) / 3) โ 5) ยท
(logโ2)) โ ((((4 ยท ๐) / 3) ยท (logโ2)) โ
(logโ๐))) =
((logโ๐) โ (5
ยท (logโ2)))) |
270 | 261, 269 | oveq12d 7321 |
. . . . . . 7
โข (๐ โ (((((โโ(2
ยท ๐)) / 3) + 2)
ยท (logโ(2 ยท ๐))) + (((((4 ยท ๐) / 3) โ 5) ยท (logโ2))
โ ((((4 ยท ๐) /
3) ยท (logโ2)) โ (logโ๐)))) = (((((โโ(2 ยท ๐)) / 3) ยท (logโ(2
ยท ๐))) + ((2
ยท (logโ2)) + (2 ยท (logโ๐)))) + ((logโ๐) โ (5 ยท
(logโ2))))) |
271 | 133 | recnd 11045 |
. . . . . . . 8
โข (๐ โ ((((4 ยท ๐) / 3) ยท (logโ2))
โ (logโ๐))
โ โ) |
272 | 182, 183,
271 | addsubassd 11394 |
. . . . . . 7
โข (๐ โ ((((((โโ(2
ยท ๐)) / 3) + 2)
ยท (logโ(2 ยท ๐))) + ((((4 ยท ๐) / 3) โ 5) ยท (logโ2)))
โ ((((4 ยท ๐) /
3) ยท (logโ2)) โ (logโ๐))) = (((((โโ(2 ยท ๐)) / 3) + 2) ยท
(logโ(2 ยท ๐)))
+ (((((4 ยท ๐) / 3)
โ 5) ยท (logโ2)) โ ((((4 ยท ๐) / 3) ยท (logโ2)) โ
(logโ๐))))) |
273 | 262, 223,
196 | subdiri 11467 |
. . . . . . . . . . . . 13
โข ((5
โ 3) ยท (logโ2)) = ((5 ยท (logโ2)) โ (3
ยท (logโ2))) |
274 | | 3p2e5 12166 |
. . . . . . . . . . . . . . . 16
โข (3 + 2) =
5 |
275 | 274 | oveq1i 7313 |
. . . . . . . . . . . . . . 15
โข ((3 + 2)
โ 3) = (5 โ 3) |
276 | | pncan2 11270 |
. . . . . . . . . . . . . . . 16
โข ((3
โ โ โง 2 โ โ) โ ((3 + 2) โ 3) =
2) |
277 | 223, 176,
276 | mp2an 690 |
. . . . . . . . . . . . . . 15
โข ((3 + 2)
โ 3) = 2 |
278 | 275, 277 | eqtr3i 2766 |
. . . . . . . . . . . . . 14
โข (5
โ 3) = 2 |
279 | 278 | oveq1i 7313 |
. . . . . . . . . . . . 13
โข ((5
โ 3) ยท (logโ2)) = (2 ยท
(logโ2)) |
280 | 273, 279 | eqtr3i 2766 |
. . . . . . . . . . . 12
โข ((5
ยท (logโ2)) โ (3 ยท (logโ2))) = (2 ยท
(logโ2)) |
281 | 280 | a1i 11 |
. . . . . . . . . . 11
โข (๐ โ ((5 ยท
(logโ2)) โ (3 ยท (logโ2))) = (2 ยท
(logโ2))) |
282 | | mulcl 10997 |
. . . . . . . . . . . . 13
โข ((2
โ โ โง (logโ๐) โ โ) โ (2 ยท
(logโ๐)) โ
โ) |
283 | 176, 168,
282 | sylancr 588 |
. . . . . . . . . . . 12
โข (๐ โ (2 ยท
(logโ๐)) โ
โ) |
284 | | df-3 12079 |
. . . . . . . . . . . . . . . 16
โข 3 = (2 +
1) |
285 | 284 | oveq1i 7313 |
. . . . . . . . . . . . . . 15
โข (3
ยท (logโ๐)) =
((2 + 1) ยท (logโ๐)) |
286 | | 1cnd 11012 |
. . . . . . . . . . . . . . . 16
โข (๐ โ 1 โ
โ) |
287 | 252, 286,
168 | adddird 11042 |
. . . . . . . . . . . . . . 15
โข (๐ โ ((2 + 1) ยท
(logโ๐)) = ((2
ยท (logโ๐)) +
(1 ยท (logโ๐)))) |
288 | 285, 287 | eqtrid 2788 |
. . . . . . . . . . . . . 14
โข (๐ โ (3 ยท
(logโ๐)) = ((2
ยท (logโ๐)) +
(1 ยท (logโ๐)))) |
289 | 168 | mulid2d 11035 |
. . . . . . . . . . . . . . 15
โข (๐ โ (1 ยท
(logโ๐)) =
(logโ๐)) |
290 | 289 | oveq2d 7319 |
. . . . . . . . . . . . . 14
โข (๐ โ ((2 ยท
(logโ๐)) + (1
ยท (logโ๐))) =
((2 ยท (logโ๐))
+ (logโ๐))) |
291 | 288, 290 | eqtrd 2776 |
. . . . . . . . . . . . 13
โข (๐ โ (3 ยท
(logโ๐)) = ((2
ยท (logโ๐)) +
(logโ๐))) |
292 | 291 | oveq1d 7318 |
. . . . . . . . . . . 12
โข (๐ โ ((3 ยท
(logโ๐)) โ (5
ยท (logโ2))) = (((2 ยท (logโ๐)) + (logโ๐)) โ (5 ยท
(logโ2)))) |
293 | 283, 168,
267, 292 | assraddsubd 11431 |
. . . . . . . . . . 11
โข (๐ โ ((3 ยท
(logโ๐)) โ (5
ยท (logโ2))) = ((2 ยท (logโ๐)) + ((logโ๐) โ (5 ยท
(logโ2))))) |
294 | 281, 293 | oveq12d 7321 |
. . . . . . . . . 10
โข (๐ โ (((5 ยท
(logโ2)) โ (3 ยท (logโ2))) + ((3 ยท
(logโ๐)) โ (5
ยท (logโ2)))) = ((2 ยท (logโ2)) + ((2 ยท
(logโ๐)) +
((logโ๐) โ (5
ยท (logโ2)))))) |
295 | | relogdiv 25789 |
. . . . . . . . . . . . . 14
โข ((๐ โ โ+
โง 2 โ โ+) โ (logโ(๐ / 2)) = ((logโ๐) โ (logโ2))) |
296 | 59, 89, 295 | sylancl 587 |
. . . . . . . . . . . . 13
โข (๐ โ (logโ(๐ / 2)) = ((logโ๐) โ
(logโ2))) |
297 | 296 | oveq2d 7319 |
. . . . . . . . . . . 12
โข (๐ โ (3 ยท
(logโ(๐ / 2))) = (3
ยท ((logโ๐)
โ (logโ2)))) |
298 | | subdi 11450 |
. . . . . . . . . . . . . 14
โข ((3
โ โ โง (logโ๐) โ โ โง (logโ2) โ
โ) โ (3 ยท ((logโ๐) โ (logโ2))) = ((3 ยท
(logโ๐)) โ (3
ยท (logโ2)))) |
299 | 223, 196,
298 | mp3an13 1452 |
. . . . . . . . . . . . 13
โข
((logโ๐)
โ โ โ (3 ยท ((logโ๐) โ (logโ2))) = ((3 ยท
(logโ๐)) โ (3
ยท (logโ2)))) |
300 | 168, 299 | syl 17 |
. . . . . . . . . . . 12
โข (๐ โ (3 ยท
((logโ๐) โ
(logโ2))) = ((3 ยท (logโ๐)) โ (3 ยท
(logโ2)))) |
301 | 297, 300 | eqtrd 2776 |
. . . . . . . . . . 11
โข (๐ โ (3 ยท
(logโ(๐ / 2))) = ((3
ยท (logโ๐))
โ (3 ยท (logโ2)))) |
302 | | div23 11694 |
. . . . . . . . . . . . . . . . 17
โข ((2
โ โ โง ๐
โ โ โง (3 โ โ โง 3 โ 0)) โ ((2 ยท
๐) / 3) = ((2 / 3) ยท
๐)) |
303 | 176, 225,
302 | mp3an13 1452 |
. . . . . . . . . . . . . . . 16
โข (๐ โ โ โ ((2
ยท ๐) / 3) = ((2 / 3)
ยท ๐)) |
304 | 192, 303 | syl 17 |
. . . . . . . . . . . . . . 15
โข (๐ โ ((2 ยท ๐) / 3) = ((2 / 3) ยท ๐)) |
305 | 223, 176,
223, 176, 177, 177 | divmuldivi 11777 |
. . . . . . . . . . . . . . . . 17
โข ((3 / 2)
ยท (3 / 2)) = ((3 ยท 3) / (2 ยท 2)) |
306 | | 3t3e9 12182 |
. . . . . . . . . . . . . . . . . 18
โข (3
ยท 3) = 9 |
307 | 306, 203 | oveq12i 7315 |
. . . . . . . . . . . . . . . . 17
โข ((3
ยท 3) / (2 ยท 2)) = (9 / 4) |
308 | 305, 307 | eqtr2i 2765 |
. . . . . . . . . . . . . . . 16
โข (9 / 4) =
((3 / 2) ยท (3 / 2)) |
309 | 308 | a1i 11 |
. . . . . . . . . . . . . . 15
โข (๐ โ (9 / 4) = ((3 / 2)
ยท (3 / 2))) |
310 | 304, 309 | oveq12d 7321 |
. . . . . . . . . . . . . 14
โข (๐ โ (((2 ยท ๐) / 3) ยท (9 / 4)) = (((2
/ 3) ยท ๐) ยท
((3 / 2) ยท (3 / 2)))) |
311 | 176, 223,
224 | divcli 11759 |
. . . . . . . . . . . . . . 15
โข (2 / 3)
โ โ |
312 | 223, 176,
177 | divcli 11759 |
. . . . . . . . . . . . . . . 16
โข (3 / 2)
โ โ |
313 | | mul4 11185 |
. . . . . . . . . . . . . . . 16
โข ((((2 /
3) โ โ โง ๐
โ โ) โง ((3 / 2) โ โ โง (3 / 2) โ โ))
โ (((2 / 3) ยท ๐) ยท ((3 / 2) ยท (3 / 2))) =
(((2 / 3) ยท (3 / 2)) ยท (๐ ยท (3 / 2)))) |
314 | 312, 312,
313 | mpanr12 703 |
. . . . . . . . . . . . . . 15
โข (((2 / 3)
โ โ โง ๐
โ โ) โ (((2 / 3) ยท ๐) ยท ((3 / 2) ยท (3 / 2))) =
(((2 / 3) ยท (3 / 2)) ยท (๐ ยท (3 / 2)))) |
315 | 311, 192,
314 | sylancr 588 |
. . . . . . . . . . . . . 14
โข (๐ โ (((2 / 3) ยท ๐) ยท ((3 / 2) ยท (3
/ 2))) = (((2 / 3) ยท (3 / 2)) ยท (๐ ยท (3 / 2)))) |
316 | | divcan6 11724 |
. . . . . . . . . . . . . . . . . 18
โข (((2
โ โ โง 2 โ 0) โง (3 โ โ โง 3 โ 0)) โ
((2 / 3) ยท (3 / 2)) = 1) |
317 | 176, 177,
223, 224, 316 | mp4an 691 |
. . . . . . . . . . . . . . . . 17
โข ((2 / 3)
ยท (3 / 2)) = 1 |
318 | 317 | oveq1i 7313 |
. . . . . . . . . . . . . . . 16
โข (((2 / 3)
ยท (3 / 2)) ยท (๐ ยท (3 / 2))) = (1 ยท (๐ ยท (3 /
2))) |
319 | | mulcl 10997 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โ โ โง (3 / 2)
โ โ) โ (๐
ยท (3 / 2)) โ โ) |
320 | 192, 312,
319 | sylancl 587 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ (๐ ยท (3 / 2)) โ
โ) |
321 | 320 | mulid2d 11035 |
. . . . . . . . . . . . . . . 16
โข (๐ โ (1 ยท (๐ ยท (3 / 2))) = (๐ ยท (3 /
2))) |
322 | 318, 321 | eqtrid 2788 |
. . . . . . . . . . . . . . 15
โข (๐ โ (((2 / 3) ยท (3 /
2)) ยท (๐ ยท (3
/ 2))) = (๐ ยท (3 /
2))) |
323 | | 2cnne0 12225 |
. . . . . . . . . . . . . . . . 17
โข (2 โ
โ โง 2 โ 0) |
324 | | div12 11697 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โ โ โง 3 โ
โ โง (2 โ โ โง 2 โ 0)) โ (๐ ยท (3 / 2)) = (3 ยท (๐ / 2))) |
325 | 223, 323,
324 | mp3an23 1453 |
. . . . . . . . . . . . . . . 16
โข (๐ โ โ โ (๐ ยท (3 / 2)) = (3 ยท
(๐ / 2))) |
326 | 192, 325 | syl 17 |
. . . . . . . . . . . . . . 15
โข (๐ โ (๐ ยท (3 / 2)) = (3 ยท (๐ / 2))) |
327 | 322, 326 | eqtrd 2776 |
. . . . . . . . . . . . . 14
โข (๐ โ (((2 / 3) ยท (3 /
2)) ยท (๐ ยท (3
/ 2))) = (3 ยท (๐ /
2))) |
328 | 310, 315,
327 | 3eqtrd 2780 |
. . . . . . . . . . . . 13
โข (๐ โ (((2 ยท ๐) / 3) ยท (9 / 4)) = (3
ยท (๐ /
2))) |
329 | 328, 82 | oveq12d 7321 |
. . . . . . . . . . . 12
โข (๐ โ ((((2 ยท ๐) / 3) ยท (9 / 4))
ยท (๐บโ(๐ / 2))) = ((3 ยท (๐ / 2)) ยท
((logโ(๐ / 2)) /
(๐ / 2)))) |
330 | 75 | recni 11031 |
. . . . . . . . . . . . . 14
โข (9 / 4)
โ โ |
331 | 330 | a1i 11 |
. . . . . . . . . . . . 13
โข (๐ โ (9 / 4) โ
โ) |
332 | 85 | recnd 11045 |
. . . . . . . . . . . . 13
โข (๐ โ (๐บโ(๐ / 2)) โ โ) |
333 | 214, 331,
332 | mulassd 11040 |
. . . . . . . . . . . 12
โข (๐ โ ((((2 ยท ๐) / 3) ยท (9 / 4))
ยท (๐บโ(๐ / 2))) = (((2 ยท ๐) / 3) ยท ((9 / 4)
ยท (๐บโ(๐ / 2))))) |
334 | 223 | a1i 11 |
. . . . . . . . . . . . . 14
โข (๐ โ 3 โ
โ) |
335 | 76 | rpcnd 12816 |
. . . . . . . . . . . . . 14
โข (๐ โ (๐ / 2) โ โ) |
336 | 83 | recnd 11045 |
. . . . . . . . . . . . . . 15
โข (๐ โ (logโ(๐ / 2)) โ
โ) |
337 | 76 | rpne0d 12819 |
. . . . . . . . . . . . . . 15
โข (๐ โ (๐ / 2) โ 0) |
338 | 336, 335,
337 | divcld 11793 |
. . . . . . . . . . . . . 14
โข (๐ โ ((logโ(๐ / 2)) / (๐ / 2)) โ โ) |
339 | 334, 335,
338 | mulassd 11040 |
. . . . . . . . . . . . 13
โข (๐ โ ((3 ยท (๐ / 2)) ยท
((logโ(๐ / 2)) /
(๐ / 2))) = (3 ยท
((๐ / 2) ยท
((logโ(๐ / 2)) /
(๐ /
2))))) |
340 | 336, 335,
337 | divcan2d 11795 |
. . . . . . . . . . . . . 14
โข (๐ โ ((๐ / 2) ยท ((logโ(๐ / 2)) / (๐ / 2))) = (logโ(๐ / 2))) |
341 | 340 | oveq2d 7319 |
. . . . . . . . . . . . 13
โข (๐ โ (3 ยท ((๐ / 2) ยท
((logโ(๐ / 2)) /
(๐ / 2)))) = (3 ยท
(logโ(๐ /
2)))) |
342 | 339, 341 | eqtrd 2776 |
. . . . . . . . . . . 12
โข (๐ โ ((3 ยท (๐ / 2)) ยท
((logโ(๐ / 2)) /
(๐ / 2))) = (3 ยท
(logโ(๐ /
2)))) |
343 | 329, 333,
342 | 3eqtr3d 2784 |
. . . . . . . . . . 11
โข (๐ โ (((2 ยท ๐) / 3) ยท ((9 / 4)
ยท (๐บโ(๐ / 2)))) = (3 ยท
(logโ(๐ /
2)))) |
344 | 223, 196 | mulcli 11024 |
. . . . . . . . . . . . 13
โข (3
ยท (logโ2)) โ โ |
345 | 344 | a1i 11 |
. . . . . . . . . . . 12
โข (๐ โ (3 ยท (logโ2))
โ โ) |
346 | | mulcl 10997 |
. . . . . . . . . . . . 13
โข ((3
โ โ โง (logโ๐) โ โ) โ (3 ยท
(logโ๐)) โ
โ) |
347 | 223, 168,
346 | sylancr 588 |
. . . . . . . . . . . 12
โข (๐ โ (3 ยท
(logโ๐)) โ
โ) |
348 | 267, 345,
347 | npncan3d 11410 |
. . . . . . . . . . 11
โข (๐ โ (((5 ยท
(logโ2)) โ (3 ยท (logโ2))) + ((3 ยท
(logโ๐)) โ (5
ยท (logโ2)))) = ((3 ยท (logโ๐)) โ (3 ยท
(logโ2)))) |
349 | 301, 343,
348 | 3eqtr4d 2786 |
. . . . . . . . . 10
โข (๐ โ (((2 ยท ๐) / 3) ยท ((9 / 4)
ยท (๐บโ(๐ / 2)))) = (((5 ยท
(logโ2)) โ (3 ยท (logโ2))) + ((3 ยท
(logโ๐)) โ (5
ยท (logโ2))))) |
350 | 116, 91 | remulcli 11033 |
. . . . . . . . . . . . 13
โข (2
ยท (logโ2)) โ โ |
351 | 350 | recni 11031 |
. . . . . . . . . . . 12
โข (2
ยท (logโ2)) โ โ |
352 | 351 | a1i 11 |
. . . . . . . . . . 11
โข (๐ โ (2 ยท (logโ2))
โ โ) |
353 | | subcl 11262 |
. . . . . . . . . . . 12
โข
(((logโ๐)
โ โ โง (5 ยท (logโ2)) โ โ) โ
((logโ๐) โ (5
ยท (logโ2))) โ โ) |
354 | 168, 266,
353 | sylancl 587 |
. . . . . . . . . . 11
โข (๐ โ ((logโ๐) โ (5 ยท
(logโ2))) โ โ) |
355 | 352, 283,
354 | addassd 11039 |
. . . . . . . . . 10
โข (๐ โ (((2 ยท
(logโ2)) + (2 ยท (logโ๐))) + ((logโ๐) โ (5 ยท (logโ2)))) = ((2
ยท (logโ2)) + ((2 ยท (logโ๐)) + ((logโ๐) โ (5 ยท
(logโ2)))))) |
356 | 294, 349,
355 | 3eqtr4d 2786 |
. . . . . . . . 9
โข (๐ โ (((2 ยท ๐) / 3) ยท ((9 / 4)
ยท (๐บโ(๐ / 2)))) = (((2 ยท
(logโ2)) + (2 ยท (logโ๐))) + ((logโ๐) โ (5 ยท
(logโ2))))) |
357 | 356 | oveq2d 7319 |
. . . . . . . 8
โข (๐ โ ((((โโ(2
ยท ๐)) / 3) ยท
(logโ(2 ยท ๐)))
+ (((2 ยท ๐) / 3)
ยท ((9 / 4) ยท (๐บโ(๐ / 2))))) = ((((โโ(2 ยท
๐)) / 3) ยท
(logโ(2 ยท ๐)))
+ (((2 ยท (logโ2)) + (2 ยท (logโ๐))) + ((logโ๐) โ (5 ยท
(logโ2)))))) |
358 | | mulcl 10997 |
. . . . . . . . . . 11
โข
((((โโ(2 ยท ๐)) / 3) โ โ โง (logโ2)
โ โ) โ (((โโ(2 ยท ๐)) / 3) ยท (logโ2)) โ
โ) |
359 | 251, 196,
358 | sylancl 587 |
. . . . . . . . . 10
โข (๐ โ (((โโ(2
ยท ๐)) / 3) ยท
(logโ2)) โ โ) |
360 | 251, 168 | mulcld 11037 |
. . . . . . . . . 10
โข (๐ โ (((โโ(2
ยท ๐)) / 3) ยท
(logโ๐)) โ
โ) |
361 | 87 | recnd 11045 |
. . . . . . . . . . 11
โข (๐ โ ((9 / 4) ยท (๐บโ(๐ / 2))) โ โ) |
362 | 214, 361 | mulcld 11037 |
. . . . . . . . . 10
โข (๐ โ (((2 ยท ๐) / 3) ยท ((9 / 4)
ยท (๐บโ(๐ / 2)))) โ
โ) |
363 | 359, 360,
362 | addassd 11039 |
. . . . . . . . 9
โข (๐ โ (((((โโ(2
ยท ๐)) / 3) ยท
(logโ2)) + (((โโ(2 ยท ๐)) / 3) ยท (logโ๐))) + (((2 ยท ๐) / 3) ยท ((9 / 4)
ยท (๐บโ(๐ / 2))))) = ((((โโ(2
ยท ๐)) / 3) ยท
(logโ2)) + ((((โโ(2 ยท ๐)) / 3) ยท (logโ๐)) + (((2 ยท ๐) / 3) ยท ((9 / 4)
ยท (๐บโ(๐ / 2))))))) |
364 | 256 | oveq2d 7319 |
. . . . . . . . . . 11
โข (๐ โ (((โโ(2
ยท ๐)) / 3) ยท
(logโ(2 ยท ๐)))
= (((โโ(2 ยท ๐)) / 3) ยท ((logโ2) +
(logโ๐)))) |
365 | 251, 245,
168 | adddid 11041 |
. . . . . . . . . . 11
โข (๐ โ (((โโ(2
ยท ๐)) / 3) ยท
((logโ2) + (logโ๐))) = ((((โโ(2 ยท ๐)) / 3) ยท (logโ2))
+ (((โโ(2 ยท ๐)) / 3) ยท (logโ๐)))) |
366 | 364, 365 | eqtrd 2776 |
. . . . . . . . . 10
โข (๐ โ (((โโ(2
ยท ๐)) / 3) ยท
(logโ(2 ยท ๐)))
= ((((โโ(2 ยท ๐)) / 3) ยท (logโ2)) +
(((โโ(2 ยท ๐)) / 3) ยท (logโ๐)))) |
367 | 366 | oveq1d 7318 |
. . . . . . . . 9
โข (๐ โ ((((โโ(2
ยท ๐)) / 3) ยท
(logโ(2 ยท ๐)))
+ (((2 ยท ๐) / 3)
ยท ((9 / 4) ยท (๐บโ(๐ / 2))))) = (((((โโ(2 ยท
๐)) / 3) ยท
(logโ2)) + (((โโ(2 ยท ๐)) / 3) ยท (logโ๐))) + (((2 ยท ๐) / 3) ยท ((9 / 4)
ยท (๐บโ(๐ / 2)))))) |
368 | 57 | oveq2d 7319 |
. . . . . . . . . . 11
โข (๐ โ (((2 ยท ๐) / 3) ยท (๐นโ๐)) = (((2 ยท ๐) / 3) ยท ((((โโ2)
ยท (๐บโ(โโ๐))) + ((9 / 4) ยท (๐บโ(๐ / 2)))) + ((logโ2) /
(โโ(2 ยท ๐)))))) |
369 | 88 | recnd 11045 |
. . . . . . . . . . . 12
โข (๐ โ (((โโ2)
ยท (๐บโ(โโ๐))) + ((9 / 4) ยท (๐บโ(๐ / 2)))) โ โ) |
370 | 96 | recnd 11045 |
. . . . . . . . . . . 12
โข (๐ โ ((logโ2) /
(โโ(2 ยท ๐))) โ โ) |
371 | 214, 369,
370 | adddid 11041 |
. . . . . . . . . . 11
โข (๐ โ (((2 ยท ๐) / 3) ยท
((((โโ2) ยท (๐บโ(โโ๐))) + ((9 / 4) ยท (๐บโ(๐ / 2)))) + ((logโ2) /
(โโ(2 ยท ๐))))) = ((((2 ยท ๐) / 3) ยท (((โโ2) ยท
(๐บโ(โโ๐))) + ((9 / 4) ยท (๐บโ(๐ / 2))))) + (((2 ยท ๐) / 3) ยท ((logโ2) /
(โโ(2 ยท ๐)))))) |
372 | 368, 371 | eqtrd 2776 |
. . . . . . . . . 10
โข (๐ โ (((2 ยท ๐) / 3) ยท (๐นโ๐)) = ((((2 ยท ๐) / 3) ยท (((โโ2) ยท
(๐บโ(โโ๐))) + ((9 / 4) ยท (๐บโ(๐ / 2))))) + (((2 ยท ๐) / 3) ยท ((logโ2) /
(โโ(2 ยท ๐)))))) |
373 | 71 | recnd 11045 |
. . . . . . . . . . . . 13
โข (๐ โ ((โโ2)
ยท (๐บโ(โโ๐))) โ โ) |
374 | 214, 373,
361 | adddid 11041 |
. . . . . . . . . . . 12
โข (๐ โ (((2 ยท ๐) / 3) ยท
(((โโ2) ยท (๐บโ(โโ๐))) + ((9 / 4) ยท (๐บโ(๐ / 2))))) = ((((2 ยท ๐) / 3) ยท ((โโ2) ยท
(๐บโ(โโ๐)))) + (((2 ยท ๐) / 3) ยท ((9 / 4) ยท (๐บโ(๐ / 2)))))) |
375 | 93 | rpge0d 12818 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ 0 โค (2 ยท ๐)) |
376 | | remsqsqrt 15009 |
. . . . . . . . . . . . . . . . . 18
โข (((2
ยท ๐) โ โ
โง 0 โค (2 ยท ๐)) โ ((โโ(2 ยท ๐)) ยท (โโ(2
ยท ๐))) = (2 ยท
๐)) |
377 | 237, 375,
376 | syl2anc 585 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ ((โโ(2
ยท ๐)) ยท
(โโ(2 ยท ๐))) = (2 ยท ๐)) |
378 | 377 | oveq1d 7318 |
. . . . . . . . . . . . . . . 16
โข (๐ โ (((โโ(2
ยท ๐)) ยท
(โโ(2 ยท ๐))) / 3) = ((2 ยท ๐) / 3)) |
379 | 112 | recnd 11045 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ (โโ(2 ยท
๐)) โ
โ) |
380 | 224 | a1i 11 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ 3 โ 0) |
381 | 379, 379,
334, 380 | div23d 11830 |
. . . . . . . . . . . . . . . 16
โข (๐ โ (((โโ(2
ยท ๐)) ยท
(โโ(2 ยท ๐))) / 3) = (((โโ(2 ยท
๐)) / 3) ยท
(โโ(2 ยท ๐)))) |
382 | 378, 381 | eqtr3d 2778 |
. . . . . . . . . . . . . . 15
โข (๐ โ ((2 ยท ๐) / 3) = (((โโ(2
ยท ๐)) / 3) ยท
(โโ(2 ยท ๐)))) |
383 | 382 | oveq1d 7318 |
. . . . . . . . . . . . . 14
โข (๐ โ (((2 ยท ๐) / 3) ยท
((โโ2) ยท (๐บโ(โโ๐)))) = ((((โโ(2 ยท ๐)) / 3) ยท
(โโ(2 ยท ๐))) ยท ((โโ2) ยท
(๐บโ(โโ๐))))) |
384 | 251, 379,
373 | mulassd 11040 |
. . . . . . . . . . . . . 14
โข (๐ โ ((((โโ(2
ยท ๐)) / 3) ยท
(โโ(2 ยท ๐))) ยท ((โโ2) ยท
(๐บโ(โโ๐)))) = (((โโ(2 ยท ๐)) / 3) ยท
((โโ(2 ยท ๐)) ยท ((โโ2) ยท
(๐บโ(โโ๐)))))) |
385 | | 0le2 12117 |
. . . . . . . . . . . . . . . . . . 19
โข 0 โค
2 |
386 | 116, 385 | pm3.2i 472 |
. . . . . . . . . . . . . . . . . 18
โข (2 โ
โ โง 0 โค 2) |
387 | 59 | rprege0d 12821 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ (๐ โ โ โง 0 โค ๐)) |
388 | | sqrtmul 15012 |
. . . . . . . . . . . . . . . . . 18
โข (((2
โ โ โง 0 โค 2) โง (๐ โ โ โง 0 โค ๐)) โ (โโ(2
ยท ๐)) =
((โโ2) ยท (โโ๐))) |
389 | 386, 387,
388 | sylancr 588 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ (โโ(2 ยท
๐)) = ((โโ2)
ยท (โโ๐))) |
390 | 389 | oveq1d 7318 |
. . . . . . . . . . . . . . . 16
โข (๐ โ ((โโ(2
ยท ๐)) ยท
((โโ2) ยท (๐บโ(โโ๐)))) = (((โโ2) ยท
(โโ๐)) ยท
((โโ2) ยท (๐บโ(โโ๐))))) |
391 | 58 | recni 11031 |
. . . . . . . . . . . . . . . . . 18
โข
(โโ2) โ โ |
392 | 391 | a1i 11 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ (โโ2) โ
โ) |
393 | 60 | rpcnd 12816 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ (โโ๐) โ
โ) |
394 | 69 | recnd 11045 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ (๐บโ(โโ๐)) โ โ) |
395 | 392, 393,
392, 394 | mul4d 11229 |
. . . . . . . . . . . . . . . 16
โข (๐ โ (((โโ2)
ยท (โโ๐))
ยท ((โโ2) ยท (๐บโ(โโ๐)))) = (((โโ2) ยท
(โโ2)) ยท ((โโ๐) ยท (๐บโ(โโ๐))))) |
396 | | remsqsqrt 15009 |
. . . . . . . . . . . . . . . . . . . 20
โข ((2
โ โ โง 0 โค 2) โ ((โโ2) ยท
(โโ2)) = 2) |
397 | 116, 385,
396 | mp2an 690 |
. . . . . . . . . . . . . . . . . . 19
โข
((โโ2) ยท (โโ2)) = 2 |
398 | 397 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ ((โโ2)
ยท (โโ2)) = 2) |
399 | 66 | oveq2d 7319 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ ((โโ๐) ยท (๐บโ(โโ๐))) = ((โโ๐) ยท ((logโ(โโ๐)) / (โโ๐)))) |
400 | 67 | recnd 11045 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ
(logโ(โโ๐)) โ โ) |
401 | 60 | rpne0d 12819 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ (โโ๐) โ 0) |
402 | 400, 393,
401 | divcan2d 11795 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ ((โโ๐) ยท
((logโ(โโ๐)) / (โโ๐))) = (logโ(โโ๐))) |
403 | 399, 402 | eqtrd 2776 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ ((โโ๐) ยท (๐บโ(โโ๐))) = (logโ(โโ๐))) |
404 | 398, 403 | oveq12d 7321 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ (((โโ2)
ยท (โโ2)) ยท ((โโ๐) ยท (๐บโ(โโ๐)))) = (2 ยท
(logโ(โโ๐)))) |
405 | 400 | 2timesd 12258 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ (2 ยท
(logโ(โโ๐))) = ((logโ(โโ๐)) +
(logโ(โโ๐)))) |
406 | 60, 60 | relogmuld 25821 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ
(logโ((โโ๐) ยท (โโ๐))) = ((logโ(โโ๐)) +
(logโ(โโ๐)))) |
407 | | remsqsqrt 15009 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โ โ โง 0 โค
๐) โ
((โโ๐) ยท
(โโ๐)) = ๐) |
408 | 387, 407 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ ((โโ๐) ยท (โโ๐)) = ๐) |
409 | 408 | fveq2d 6804 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ
(logโ((โโ๐) ยท (โโ๐))) = (logโ๐)) |
410 | 406, 409 | eqtr3d 2778 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ
((logโ(โโ๐)) + (logโ(โโ๐))) = (logโ๐)) |
411 | 404, 405,
410 | 3eqtrd 2780 |
. . . . . . . . . . . . . . . 16
โข (๐ โ (((โโ2)
ยท (โโ2)) ยท ((โโ๐) ยท (๐บโ(โโ๐)))) = (logโ๐)) |
412 | 390, 395,
411 | 3eqtrd 2780 |
. . . . . . . . . . . . . . 15
โข (๐ โ ((โโ(2
ยท ๐)) ยท
((โโ2) ยท (๐บโ(โโ๐)))) = (logโ๐)) |
413 | 412 | oveq2d 7319 |
. . . . . . . . . . . . . 14
โข (๐ โ (((โโ(2
ยท ๐)) / 3) ยท
((โโ(2 ยท ๐)) ยท ((โโ2) ยท
(๐บโ(โโ๐))))) = (((โโ(2 ยท ๐)) / 3) ยท
(logโ๐))) |
414 | 383, 384,
413 | 3eqtrd 2780 |
. . . . . . . . . . . . 13
โข (๐ โ (((2 ยท ๐) / 3) ยท
((โโ2) ยท (๐บโ(โโ๐)))) = (((โโ(2 ยท ๐)) / 3) ยท
(logโ๐))) |
415 | 414 | oveq1d 7318 |
. . . . . . . . . . . 12
โข (๐ โ ((((2 ยท ๐) / 3) ยท
((โโ2) ยท (๐บโ(โโ๐)))) + (((2 ยท ๐) / 3) ยท ((9 / 4) ยท (๐บโ(๐ / 2))))) = ((((โโ(2 ยท
๐)) / 3) ยท
(logโ๐)) + (((2
ยท ๐) / 3) ยท
((9 / 4) ยท (๐บโ(๐ / 2)))))) |
416 | 374, 415 | eqtrd 2776 |
. . . . . . . . . . 11
โข (๐ โ (((2 ยท ๐) / 3) ยท
(((โโ2) ยท (๐บโ(โโ๐))) + ((9 / 4) ยท (๐บโ(๐ / 2))))) = ((((โโ(2 ยท
๐)) / 3) ยท
(logโ๐)) + (((2
ยท ๐) / 3) ยท
((9 / 4) ยท (๐บโ(๐ / 2)))))) |
417 | 382 | oveq1d 7318 |
. . . . . . . . . . . 12
โข (๐ โ (((2 ยท ๐) / 3) ยท ((logโ2) /
(โโ(2 ยท ๐)))) = ((((โโ(2 ยท ๐)) / 3) ยท
(โโ(2 ยท ๐))) ยท ((logโ2) /
(โโ(2 ยท ๐))))) |
418 | 251, 379,
370 | mulassd 11040 |
. . . . . . . . . . . 12
โข (๐ โ ((((โโ(2
ยท ๐)) / 3) ยท
(โโ(2 ยท ๐))) ยท ((logโ2) /
(โโ(2 ยท ๐)))) = (((โโ(2 ยท ๐)) / 3) ยท
((โโ(2 ยท ๐)) ยท ((logโ2) /
(โโ(2 ยท ๐)))))) |
419 | 94 | rpne0d 12819 |
. . . . . . . . . . . . . 14
โข (๐ โ (โโ(2 ยท
๐)) โ
0) |
420 | 245, 379,
419 | divcan2d 11795 |
. . . . . . . . . . . . 13
โข (๐ โ ((โโ(2
ยท ๐)) ยท
((logโ2) / (โโ(2 ยท ๐)))) = (logโ2)) |
421 | 420 | oveq2d 7319 |
. . . . . . . . . . . 12
โข (๐ โ (((โโ(2
ยท ๐)) / 3) ยท
((โโ(2 ยท ๐)) ยท ((logโ2) /
(โโ(2 ยท ๐))))) = (((โโ(2 ยท ๐)) / 3) ยท
(logโ2))) |
422 | 417, 418,
421 | 3eqtrd 2780 |
. . . . . . . . . . 11
โข (๐ โ (((2 ยท ๐) / 3) ยท ((logโ2) /
(โโ(2 ยท ๐)))) = (((โโ(2 ยท ๐)) / 3) ยท
(logโ2))) |
423 | 416, 422 | oveq12d 7321 |
. . . . . . . . . 10
โข (๐ โ ((((2 ยท ๐) / 3) ยท
(((โโ2) ยท (๐บโ(โโ๐))) + ((9 / 4) ยท (๐บโ(๐ / 2))))) + (((2 ยท ๐) / 3) ยท ((logโ2) /
(โโ(2 ยท ๐))))) = (((((โโ(2 ยท ๐)) / 3) ยท
(logโ๐)) + (((2
ยท ๐) / 3) ยท
((9 / 4) ยท (๐บโ(๐ / 2))))) + (((โโ(2 ยท
๐)) / 3) ยท
(logโ2)))) |
424 | 360, 362 | addcld 11036 |
. . . . . . . . . . 11
โข (๐ โ ((((โโ(2
ยท ๐)) / 3) ยท
(logโ๐)) + (((2
ยท ๐) / 3) ยท
((9 / 4) ยท (๐บโ(๐ / 2))))) โ โ) |
425 | 424, 359 | addcomd 11219 |
. . . . . . . . . 10
โข (๐ โ (((((โโ(2
ยท ๐)) / 3) ยท
(logโ๐)) + (((2
ยท ๐) / 3) ยท
((9 / 4) ยท (๐บโ(๐ / 2))))) + (((โโ(2 ยท
๐)) / 3) ยท
(logโ2))) = ((((โโ(2 ยท ๐)) / 3) ยท (logโ2)) +
((((โโ(2 ยท ๐)) / 3) ยท (logโ๐)) + (((2 ยท ๐) / 3) ยท ((9 / 4)
ยท (๐บโ(๐ / 2))))))) |
426 | 372, 423,
425 | 3eqtrd 2780 |
. . . . . . . . 9
โข (๐ โ (((2 ยท ๐) / 3) ยท (๐นโ๐)) = ((((โโ(2 ยท ๐)) / 3) ยท (logโ2))
+ ((((โโ(2 ยท ๐)) / 3) ยท (logโ๐)) + (((2 ยท ๐) / 3) ยท ((9 / 4)
ยท (๐บโ(๐ / 2))))))) |
427 | 363, 367,
426 | 3eqtr4rd 2787 |
. . . . . . . 8
โข (๐ โ (((2 ยท ๐) / 3) ยท (๐นโ๐)) = ((((โโ(2 ยท ๐)) / 3) ยท (logโ(2
ยท ๐))) + (((2
ยท ๐) / 3) ยท
((9 / 4) ยท (๐บโ(๐ / 2)))))) |
428 | 251, 253 | mulcld 11037 |
. . . . . . . . 9
โข (๐ โ (((โโ(2
ยท ๐)) / 3) ยท
(logโ(2 ยท ๐)))
โ โ) |
429 | | addcl 10995 |
. . . . . . . . . 10
โข (((2
ยท (logโ2)) โ โ โง (2 ยท (logโ๐)) โ โ) โ ((2
ยท (logโ2)) + (2 ยท (logโ๐))) โ โ) |
430 | 351, 283,
429 | sylancr 588 |
. . . . . . . . 9
โข (๐ โ ((2 ยท
(logโ2)) + (2 ยท (logโ๐))) โ โ) |
431 | 428, 430,
354 | addassd 11039 |
. . . . . . . 8
โข (๐ โ (((((โโ(2
ยท ๐)) / 3) ยท
(logโ(2 ยท ๐)))
+ ((2 ยท (logโ2)) + (2 ยท (logโ๐)))) + ((logโ๐) โ (5 ยท (logโ2)))) =
((((โโ(2 ยท ๐)) / 3) ยท (logโ(2 ยท
๐))) + (((2 ยท
(logโ2)) + (2 ยท (logโ๐))) + ((logโ๐) โ (5 ยท
(logโ2)))))) |
432 | 357, 427,
431 | 3eqtr4d 2786 |
. . . . . . 7
โข (๐ โ (((2 ยท ๐) / 3) ยท (๐นโ๐)) = (((((โโ(2 ยท ๐)) / 3) ยท (logโ(2
ยท ๐))) + ((2
ยท (logโ2)) + (2 ยท (logโ๐)))) + ((logโ๐) โ (5 ยท
(logโ2))))) |
433 | 270, 272,
432 | 3eqtr4rd 2787 |
. . . . . 6
โข (๐ โ (((2 ยท ๐) / 3) ยท (๐นโ๐)) = ((((((โโ(2 ยท ๐)) / 3) + 2) ยท
(logโ(2 ยท ๐)))
+ ((((4 ยท ๐) / 3)
โ 5) ยท (logโ2))) โ ((((4 ยท ๐) / 3) ยท (logโ2)) โ
(logโ๐)))) |
434 | 191, 250,
433 | 3brtr4d 5113 |
. . . . 5
โข (๐ โ (((2 ยท ๐) / 3) ยท (logโ2))
< (((2 ยท ๐) / 3)
ยท (๐นโ๐))) |
435 | 99, 98, 213 | ltmul2d 12856 |
. . . . 5
โข (๐ โ ((logโ2) < (๐นโ๐) โ (((2 ยท ๐) / 3) ยท (logโ2)) < (((2
ยท ๐) / 3) ยท
(๐นโ๐)))) |
436 | 434, 435 | mpbird 258 |
. . . 4
โข (๐ โ (logโ2) < (๐นโ๐)) |
437 | 45, 99, 98, 100, 436 | lttrd 11178 |
. . 3
โข (๐ โ (๐นโ;64) < (๐นโ๐)) |
438 | 45, 98, 437 | ltnsymd 11166 |
. 2
โข (๐ โ ยฌ (๐นโ๐) < (๐นโ;64)) |
439 | 42, 438 | pm2.21dd 194 |
1
โข (๐ โ ๐) |