Step | Hyp | Ref
| Expression |
1 | | 7nn0 12442 |
. . . . 5
โข 7 โ
โ0 |
2 | | 3re 12240 |
. . . . . . 7
โข 3 โ
โ |
3 | | 4re 12244 |
. . . . . . . . 9
โข 4 โ
โ |
4 | | 8re 12256 |
. . . . . . . . 9
โข 8 โ
โ |
5 | 3, 4 | pm3.2i 472 |
. . . . . . . 8
โข (4 โ
โ โง 8 โ โ) |
6 | | dp2cl 31778 |
. . . . . . . 8
โข ((4
โ โ โง 8 โ โ) โ _48 โ โ) |
7 | 5, 6 | ax-mp 5 |
. . . . . . 7
โข _48 โ โ |
8 | 2, 7 | pm3.2i 472 |
. . . . . 6
โข (3 โ
โ โง _48 โ
โ) |
9 | | dp2cl 31778 |
. . . . . 6
โข ((3
โ โ โง _48 โ
โ) โ _3_48 โ โ) |
10 | 8, 9 | ax-mp 5 |
. . . . 5
โข _3_48 โ โ |
11 | | dpcl 31789 |
. . . . 5
โข ((7
โ โ0 โง _3_48
โ โ) โ (7._3_48) โ โ) |
12 | 1, 10, 11 | mp2an 691 |
. . . 4
โข (7._3_48) โ โ |
13 | 12 | a1i 11 |
. . 3
โข ((๐ โ โ0
โง (;10โ;27) โค ๐) โ (7._3_48)
โ โ) |
14 | | nn0re 12429 |
. . . . . . 7
โข (๐ โ โ0
โ ๐ โ
โ) |
15 | 14 | adantr 482 |
. . . . . 6
โข ((๐ โ โ0
โง (;10โ;27) โค ๐) โ ๐ โ โ) |
16 | | 0re 11164 |
. . . . . . . 8
โข 0 โ
โ |
17 | 16 | a1i 11 |
. . . . . . 7
โข ((๐ โ โ0
โง (;10โ;27) โค ๐) โ 0 โ โ) |
18 | | 10re 12644 |
. . . . . . . . 9
โข ;10 โ โ |
19 | | 2nn0 12437 |
. . . . . . . . . 10
โข 2 โ
โ0 |
20 | 19, 1 | deccl 12640 |
. . . . . . . . 9
โข ;27 โ
โ0 |
21 | | reexpcl 13991 |
. . . . . . . . 9
โข ((;10 โ โ โง ;27 โ โ0) โ
(;10โ;27) โ โ) |
22 | 18, 20, 21 | mp2an 691 |
. . . . . . . 8
โข (;10โ;27) โ โ |
23 | 22 | a1i 11 |
. . . . . . 7
โข ((๐ โ โ0
โง (;10โ;27) โค ๐) โ (;10โ;27) โ โ) |
24 | | 0lt1 11684 |
. . . . . . . . 9
โข 0 <
1 |
25 | | 1nn 12171 |
. . . . . . . . . . 11
โข 1 โ
โ |
26 | | 0nn0 12435 |
. . . . . . . . . . 11
โข 0 โ
โ0 |
27 | | 1nn0 12436 |
. . . . . . . . . . 11
โข 1 โ
โ0 |
28 | | 1re 11162 |
. . . . . . . . . . . 12
โข 1 โ
โ |
29 | | 9re 12259 |
. . . . . . . . . . . 12
โข 9 โ
โ |
30 | | 1lt9 12366 |
. . . . . . . . . . . 12
โข 1 <
9 |
31 | 28, 29, 30 | ltleii 11285 |
. . . . . . . . . . 11
โข 1 โค
9 |
32 | 25, 26, 27, 31 | declei 12661 |
. . . . . . . . . 10
โข 1 โค
;10 |
33 | | expge1 14012 |
. . . . . . . . . 10
โข ((;10 โ โ โง ;27 โ โ0 โง 1
โค ;10) โ 1 โค (;10โ;27)) |
34 | 18, 20, 32, 33 | mp3an 1462 |
. . . . . . . . 9
โข 1 โค
(;10โ;27) |
35 | 16, 28, 22 | ltletri 11290 |
. . . . . . . . 9
โข ((0 <
1 โง 1 โค (;10โ;27)) โ 0 < (;10โ;27)) |
36 | 24, 34, 35 | mp2an 691 |
. . . . . . . 8
โข 0 <
(;10โ;27) |
37 | 36 | a1i 11 |
. . . . . . 7
โข ((๐ โ โ0
โง (;10โ;27) โค ๐) โ 0 < (;10โ;27)) |
38 | | simpr 486 |
. . . . . . 7
โข ((๐ โ โ0
โง (;10โ;27) โค ๐) โ (;10โ;27) โค ๐) |
39 | 17, 23, 15, 37, 38 | ltletrd 11322 |
. . . . . 6
โข ((๐ โ โ0
โง (;10โ;27) โค ๐) โ 0 < ๐) |
40 | 15, 39 | elrpd 12961 |
. . . . 5
โข ((๐ โ โ0
โง (;10โ;27) โค ๐) โ ๐ โ
โ+) |
41 | 40 | relogcld 25994 |
. . . 4
โข ((๐ โ โ0
โง (;10โ;27) โค ๐) โ (logโ๐) โ โ) |
42 | 40 | rpge0d 12968 |
. . . . 5
โข ((๐ โ โ0
โง (;10โ;27) โค ๐) โ 0 โค ๐) |
43 | 15, 42 | resqrtcld 15309 |
. . . 4
โข ((๐ โ โ0
โง (;10โ;27) โค ๐) โ (โโ๐) โ โ) |
44 | 40 | sqrtgt0d 15304 |
. . . . 5
โข ((๐ โ โ0
โง (;10โ;27) โค ๐) โ 0 < (โโ๐)) |
45 | 17, 44 | gtned 11297 |
. . . 4
โข ((๐ โ โ0
โง (;10โ;27) โค ๐) โ (โโ๐) โ 0) |
46 | 41, 43, 45 | redivcld 11990 |
. . 3
โข ((๐ โ โ0
โง (;10โ;27) โค ๐) โ ((logโ๐) / (โโ๐)) โ โ) |
47 | 13, 46 | remulcld 11192 |
. 2
โข ((๐ โ โ0
โง (;10โ;27) โค ๐) โ ((7._3_48)
ยท ((logโ๐) /
(โโ๐))) โ
โ) |
48 | | elrp 12924 |
. . . . . . 7
โข ((;10โ;27) โ โ+ โ ((;10โ;27) โ โ โง 0 < (;10โ;27))) |
49 | 22, 36, 48 | mpbir2an 710 |
. . . . . 6
โข (;10โ;27) โ โ+ |
50 | | relogcl 25947 |
. . . . . 6
โข ((;10โ;27) โ โ+ โ
(logโ(;10โ;27)) โ โ) |
51 | 49, 50 | ax-mp 5 |
. . . . 5
โข
(logโ(;10โ;27)) โ โ |
52 | 22, 36 | sqrtpclii 15274 |
. . . . 5
โข
(โโ(;10โ;27)) โ โ |
53 | 22, 36 | sqrtgt0ii 15275 |
. . . . . 6
โข 0 <
(โโ(;10โ;27)) |
54 | 16, 53 | gtneii 11274 |
. . . . 5
โข
(โโ(;10โ;27)) โ 0 |
55 | 51, 52, 54 | redivcli 11929 |
. . . 4
โข
((logโ(;10โ;27)) / (โโ(;10โ;27))) โ โ |
56 | 55 | a1i 11 |
. . 3
โข ((๐ โ โ0
โง (;10โ;27) โค ๐) โ ((logโ(;10โ;27)) / (โโ(;10โ;27))) โ โ) |
57 | 13, 56 | remulcld 11192 |
. 2
โข ((๐ โ โ0
โง (;10โ;27) โค ๐) โ ((7._3_48)
ยท ((logโ(;10โ;27)) / (โโ(;10โ;27)))) โ โ) |
58 | | qssre 12891 |
. . . . 5
โข โ
โ โ |
59 | | 4nn0 12439 |
. . . . . . . . 9
โข 4 โ
โ0 |
60 | | nn0ssq 12889 |
. . . . . . . . . . . . 13
โข
โ0 โ โ |
61 | | 8nn0 12443 |
. . . . . . . . . . . . 13
โข 8 โ
โ0 |
62 | 60, 61 | sselii 3946 |
. . . . . . . . . . . 12
โข 8 โ
โ |
63 | 59, 62 | dp2clq 31779 |
. . . . . . . . . . 11
โข _48 โ โ |
64 | 19, 63 | dp2clq 31779 |
. . . . . . . . . 10
โข _2_48 โ โ |
65 | 19, 64 | dp2clq 31779 |
. . . . . . . . 9
โข _2_2_48
โ โ |
66 | 59, 65 | dp2clq 31779 |
. . . . . . . 8
โข _4_2_2_48
โ โ |
67 | 26, 66 | dp2clq 31779 |
. . . . . . 7
โข _0_4_2_2_48
โ โ |
68 | 26, 67 | dp2clq 31779 |
. . . . . 6
โข _0_0_4_2_2_48
โ โ |
69 | 26, 68 | dp2clq 31779 |
. . . . 5
โข _0_0_0_4_2_2_48
โ โ |
70 | 58, 69 | sselii 3946 |
. . . 4
โข _0_0_0_4_2_2_48
โ โ |
71 | | dpcl 31789 |
. . . 4
โข ((0
โ โ0 โง _0_0_0_4_2_2_48
โ โ) โ (0._0_0_0_4_2_2_48)
โ โ) |
72 | 26, 70, 71 | mp2an 691 |
. . 3
โข (0._0_0_0_4_2_2_48)
โ โ |
73 | 72 | a1i 11 |
. 2
โข ((๐ โ โ0
โง (;10โ;27) โค ๐) โ (0._0_0_0_4_2_2_48)
โ โ) |
74 | | 3nn0 12438 |
. . . . . . . . 9
โข 3 โ
โ0 |
75 | | 8pos 12272 |
. . . . . . . . . . 11
โข 0 <
8 |
76 | | elrp 12924 |
. . . . . . . . . . 11
โข (8 โ
โ+ โ (8 โ โ โง 0 < 8)) |
77 | 4, 75, 76 | mpbir2an 710 |
. . . . . . . . . 10
โข 8 โ
โ+ |
78 | 59, 77 | rpdp2cl 31780 |
. . . . . . . . 9
โข _48 โ
โ+ |
79 | 74, 78 | rpdp2cl 31780 |
. . . . . . . 8
โข _3_48 โ โ+ |
80 | 1, 79 | rpdpcl 31801 |
. . . . . . 7
โข (7._3_48) โ โ+ |
81 | | elrp 12924 |
. . . . . . 7
โข ((7._3_48) โ โ+ โ ((7._3_48) โ โ โง 0 < (7._3_48))) |
82 | 80, 81 | mpbi 229 |
. . . . . 6
โข ((7._3_48) โ โ โง 0 < (7._3_48)) |
83 | 82 | simpri 487 |
. . . . 5
โข 0 <
(7._3_48) |
84 | 16, 12, 83 | ltleii 11285 |
. . . 4
โข 0 โค
(7._3_48) |
85 | 84 | a1i 11 |
. . 3
โข ((๐ โ โ0
โง (;10โ;27) โค ๐) โ 0 โค (7._3_48)) |
86 | 49 | a1i 11 |
. . . 4
โข ((๐ โ โ0
โง (;10โ;27) โค ๐) โ (;10โ;27) โ โ+) |
87 | | 2cn 12235 |
. . . . . . . . . 10
โข 2 โ
โ |
88 | 87 | mulid2i 11167 |
. . . . . . . . 9
โข (1
ยท 2) = 2 |
89 | | 2nn 12233 |
. . . . . . . . . . 11
โข 2 โ
โ |
90 | 89, 1, 27, 31 | declei 12661 |
. . . . . . . . . 10
โข 1 โค
;27 |
91 | | 2pos 12263 |
. . . . . . . . . . 11
โข 0 <
2 |
92 | 20 | nn0rei 12431 |
. . . . . . . . . . . 12
โข ;27 โ โ |
93 | | 2re 12234 |
. . . . . . . . . . . 12
โข 2 โ
โ |
94 | 28, 92, 93 | lemul1i 12084 |
. . . . . . . . . . 11
โข (0 < 2
โ (1 โค ;27 โ (1
ยท 2) โค (;27 ยท
2))) |
95 | 91, 94 | ax-mp 5 |
. . . . . . . . . 10
โข (1 โค
;27 โ (1 ยท 2) โค
(;27 ยท 2)) |
96 | 90, 95 | mpbi 229 |
. . . . . . . . 9
โข (1
ยท 2) โค (;27 ยท
2) |
97 | 88, 96 | eqbrtrri 5133 |
. . . . . . . 8
โข 2 โค
(;27 ยท 2) |
98 | | 1p1e2 12285 |
. . . . . . . . . . 11
โข (1 + 1) =
2 |
99 | | loge 25958 |
. . . . . . . . . . . . . 14
โข
(logโe) = 1 |
100 | | egt2lt3 16095 |
. . . . . . . . . . . . . . . 16
โข (2 < e
โง e < 3) |
101 | 100 | simpri 487 |
. . . . . . . . . . . . . . 15
โข e <
3 |
102 | | epr 16097 |
. . . . . . . . . . . . . . . 16
โข e โ
โ+ |
103 | | 3rp 12928 |
. . . . . . . . . . . . . . . 16
โข 3 โ
โ+ |
104 | | logltb 25971 |
. . . . . . . . . . . . . . . 16
โข ((e
โ โ+ โง 3 โ โ+) โ (e < 3
โ (logโe) < (logโ3))) |
105 | 102, 103,
104 | mp2an 691 |
. . . . . . . . . . . . . . 15
โข (e < 3
โ (logโe) < (logโ3)) |
106 | 101, 105 | mpbi 229 |
. . . . . . . . . . . . . 14
โข
(logโe) < (logโ3) |
107 | 99, 106 | eqbrtrri 5133 |
. . . . . . . . . . . . 13
โข 1 <
(logโ3) |
108 | | relogcl 25947 |
. . . . . . . . . . . . . . 15
โข (3 โ
โ+ โ (logโ3) โ โ) |
109 | 103, 108 | ax-mp 5 |
. . . . . . . . . . . . . 14
โข
(logโ3) โ โ |
110 | 28, 28, 109, 109 | lt2addi 11724 |
. . . . . . . . . . . . 13
โข ((1 <
(logโ3) โง 1 < (logโ3)) โ (1 + 1) < ((logโ3) +
(logโ3))) |
111 | 107, 107,
110 | mp2an 691 |
. . . . . . . . . . . 12
โข (1 + 1)
< ((logโ3) + (logโ3)) |
112 | | 3cn 12241 |
. . . . . . . . . . . . . 14
โข 3 โ
โ |
113 | | 3ne0 12266 |
. . . . . . . . . . . . . 14
โข 3 โ
0 |
114 | | logmul2 25987 |
. . . . . . . . . . . . . 14
โข ((3
โ โ โง 3 โ 0 โง 3 โ โ+) โ
(logโ(3 ยท 3)) = ((logโ3) + (logโ3))) |
115 | 112, 113,
103, 114 | mp3an 1462 |
. . . . . . . . . . . . 13
โข
(logโ(3 ยท 3)) = ((logโ3) +
(logโ3)) |
116 | | 3t3e9 12327 |
. . . . . . . . . . . . . . 15
โข (3
ยท 3) = 9 |
117 | 116 | fveq2i 6850 |
. . . . . . . . . . . . . 14
โข
(logโ(3 ยท 3)) = (logโ9) |
118 | | 9lt10 12756 |
. . . . . . . . . . . . . . . 16
โข 9 <
;10 |
119 | 29, 18, 118 | ltleii 11285 |
. . . . . . . . . . . . . . 15
โข 9 โค
;10 |
120 | | 9pos 12273 |
. . . . . . . . . . . . . . . . 17
โข 0 <
9 |
121 | | elrp 12924 |
. . . . . . . . . . . . . . . . 17
โข (9 โ
โ+ โ (9 โ โ โง 0 < 9)) |
122 | 29, 120, 121 | mpbir2an 710 |
. . . . . . . . . . . . . . . 16
โข 9 โ
โ+ |
123 | | 10pos 12642 |
. . . . . . . . . . . . . . . . 17
โข 0 <
;10 |
124 | | elrp 12924 |
. . . . . . . . . . . . . . . . 17
โข (;10 โ โ+ โ
(;10 โ โ โง 0 <
;10)) |
125 | 18, 123, 124 | mpbir2an 710 |
. . . . . . . . . . . . . . . 16
โข ;10 โ
โ+ |
126 | | logleb 25974 |
. . . . . . . . . . . . . . . 16
โข ((9
โ โ+ โง ;10 โ โ+) โ (9 โค ;10 โ (logโ9) โค
(logโ;10))) |
127 | 122, 125,
126 | mp2an 691 |
. . . . . . . . . . . . . . 15
โข (9 โค
;10 โ (logโ9) โค
(logโ;10)) |
128 | 119, 127 | mpbi 229 |
. . . . . . . . . . . . . 14
โข
(logโ9) โค (logโ;10) |
129 | 117, 128 | eqbrtri 5131 |
. . . . . . . . . . . . 13
โข
(logโ(3 ยท 3)) โค (logโ;10) |
130 | 115, 129 | eqbrtrri 5133 |
. . . . . . . . . . . 12
โข
((logโ3) + (logโ3)) โค (logโ;10) |
131 | 28, 28 | readdcli 11177 |
. . . . . . . . . . . . 13
โข (1 + 1)
โ โ |
132 | 109, 109 | readdcli 11177 |
. . . . . . . . . . . . 13
โข
((logโ3) + (logโ3)) โ โ |
133 | | relogcl 25947 |
. . . . . . . . . . . . . 14
โข (;10 โ โ+ โ
(logโ;10) โ
โ) |
134 | 125, 133 | ax-mp 5 |
. . . . . . . . . . . . 13
โข
(logโ;10) โ
โ |
135 | 131, 132,
134 | ltletri 11290 |
. . . . . . . . . . . 12
โข (((1 + 1)
< ((logโ3) + (logโ3)) โง ((logโ3) + (logโ3)) โค
(logโ;10)) โ (1 + 1)
< (logโ;10)) |
136 | 111, 130,
135 | mp2an 691 |
. . . . . . . . . . 11
โข (1 + 1)
< (logโ;10) |
137 | 98, 136 | eqbrtrri 5133 |
. . . . . . . . . 10
โข 2 <
(logโ;10) |
138 | 93, 134 | ltlei 11284 |
. . . . . . . . . 10
โข (2 <
(logโ;10) โ 2 โค
(logโ;10)) |
139 | 137, 138 | ax-mp 5 |
. . . . . . . . 9
โข 2 โค
(logโ;10) |
140 | 16, 29, 120 | ltleii 11285 |
. . . . . . . . . . 11
โข 0 โค
9 |
141 | 89, 1, 26, 140 | decltdi 12664 |
. . . . . . . . . 10
โข 0 <
;27 |
142 | 93, 134, 92 | lemul2i 12085 |
. . . . . . . . . 10
โข (0 <
;27 โ (2 โค
(logโ;10) โ (;27 ยท 2) โค (;27 ยท (logโ;10)))) |
143 | 141, 142 | ax-mp 5 |
. . . . . . . . 9
โข (2 โค
(logโ;10) โ (;27 ยท 2) โค (;27 ยท (logโ;10))) |
144 | 139, 143 | mpbi 229 |
. . . . . . . 8
โข (;27 ยท 2) โค (;27 ยท (logโ;10)) |
145 | 92, 93 | remulcli 11178 |
. . . . . . . . 9
โข (;27 ยท 2) โ
โ |
146 | 20 | nn0zi 12535 |
. . . . . . . . . . 11
โข ;27 โ โค |
147 | | relogexp 25967 |
. . . . . . . . . . 11
โข ((;10 โ โ+ โง
;27 โ โค) โ
(logโ(;10โ;27)) = (;27 ยท (logโ;10))) |
148 | 125, 146,
147 | mp2an 691 |
. . . . . . . . . 10
โข
(logโ(;10โ;27)) = (;27 ยท (logโ;10)) |
149 | 148, 51 | eqeltrri 2835 |
. . . . . . . . 9
โข (;27 ยท (logโ;10)) โ โ |
150 | 93, 145, 149 | letri 11291 |
. . . . . . . 8
โข ((2 โค
(;27 ยท 2) โง (;27 ยท 2) โค (;27 ยท (logโ;10))) โ 2 โค (;27 ยท (logโ;10))) |
151 | 97, 144, 150 | mp2an 691 |
. . . . . . 7
โข 2 โค
(;27 ยท (logโ;10)) |
152 | | relogef 25954 |
. . . . . . . 8
โข (2 โ
โ โ (logโ(expโ2)) = 2) |
153 | 93, 152 | ax-mp 5 |
. . . . . . 7
โข
(logโ(expโ2)) = 2 |
154 | 151, 153,
148 | 3brtr4i 5140 |
. . . . . 6
โข
(logโ(expโ2)) โค (logโ(;10โ;27)) |
155 | | rpefcl 15993 |
. . . . . . . 8
โข (2 โ
โ โ (expโ2) โ โ+) |
156 | 93, 155 | ax-mp 5 |
. . . . . . 7
โข
(expโ2) โ โ+ |
157 | | logleb 25974 |
. . . . . . 7
โข
(((expโ2) โ โ+ โง (;10โ;27) โ โ+) โ
((expโ2) โค (;10โ;27) โ (logโ(expโ2)) โค
(logโ(;10โ;27)))) |
158 | 156, 49, 157 | mp2an 691 |
. . . . . 6
โข
((expโ2) โค (;10โ;27) โ (logโ(expโ2)) โค
(logโ(;10โ;27))) |
159 | 154, 158 | mpbir 230 |
. . . . 5
โข
(expโ2) โค (;10โ;27) |
160 | 159 | a1i 11 |
. . . 4
โข ((๐ โ โ0
โง (;10โ;27) โค ๐) โ (expโ2) โค (;10โ;27)) |
161 | 86, 40, 160, 38 | logdivsqrle 33303 |
. . 3
โข ((๐ โ โ0
โง (;10โ;27) โค ๐) โ ((logโ๐) / (โโ๐)) โค ((logโ(;10โ;27)) / (โโ(;10โ;27)))) |
162 | 46, 56, 13, 85, 161 | lemul2ad 12102 |
. 2
โข ((๐ โ โ0
โง (;10โ;27) โค ๐) โ ((7._3_48)
ยท ((logโ๐) /
(โโ๐))) โค
((7._3_48) ยท ((logโ(;10โ;27)) / (โโ(;10โ;27))))) |
163 | | 3lt10 12762 |
. . . . . . . 8
โข 3 <
;10 |
164 | | 4lt10 12761 |
. . . . . . . . 9
โข 4 <
;10 |
165 | | 8lt10 12757 |
. . . . . . . . 9
โข 8 <
;10 |
166 | 59, 77, 164, 165 | dp2lt10 31782 |
. . . . . . . 8
โข _48 < ;10 |
167 | 74, 78, 163, 166 | dp2lt10 31782 |
. . . . . . 7
โข _3_48 < ;10 |
168 | | 7p1e8 12309 |
. . . . . . 7
โข (7 + 1) =
8 |
169 | 1, 79, 61, 167, 168 | dplti 31803 |
. . . . . 6
โข (7._3_48) < 8 |
170 | 58, 62 | sselii 3946 |
. . . . . . 7
โข 8 โ
โ |
171 | 12, 170, 18 | lttri 11288 |
. . . . . 6
โข
(((7._3_48) < 8 โง 8 < ;10) โ (7._3_48)
< ;10) |
172 | 169, 165,
171 | mp2an 691 |
. . . . 5
โข (7._3_48) < ;10 |
173 | 27, 26 | deccl 12640 |
. . . . . . . . . 10
โข ;10 โ
โ0 |
174 | 173 | numexp0 16955 |
. . . . . . . . 9
โข (;10โ0) = 1 |
175 | | 0z 12517 |
. . . . . . . . . . 11
โข 0 โ
โค |
176 | 18, 175, 146 | 3pm3.2i 1340 |
. . . . . . . . . 10
โข (;10 โ โ โง 0 โ
โค โง ;27 โ
โค) |
177 | | 1lt10 12764 |
. . . . . . . . . . 11
โข 1 <
;10 |
178 | 177, 141 | pm3.2i 472 |
. . . . . . . . . 10
โข (1 <
;10 โง 0 < ;27) |
179 | | ltexp2a 14078 |
. . . . . . . . . 10
โข (((;10 โ โ โง 0 โ
โค โง ;27 โ โค)
โง (1 < ;10 โง 0 <
;27)) โ (;10โ0) < (;10โ;27)) |
180 | 176, 178,
179 | mp2an 691 |
. . . . . . . . 9
โข (;10โ0) < (;10โ;27) |
181 | 174, 180 | eqbrtrri 5133 |
. . . . . . . 8
โข 1 <
(;10โ;27) |
182 | | loggt0b 26003 |
. . . . . . . . 9
โข ((;10โ;27) โ โ+ โ (0 <
(logโ(;10โ;27)) โ 1 < (;10โ;27))) |
183 | 49, 182 | ax-mp 5 |
. . . . . . . 8
โข (0 <
(logโ(;10โ;27)) โ 1 < (;10โ;27)) |
184 | 181, 183 | mpbir 230 |
. . . . . . 7
โข 0 <
(logโ(;10โ;27)) |
185 | 51, 52 | divgt0i 12070 |
. . . . . . 7
โข ((0 <
(logโ(;10โ;27)) โง 0 < (โโ(;10โ;27))) โ 0 < ((logโ(;10โ;27)) / (โโ(;10โ;27)))) |
186 | 184, 53, 185 | mp2an 691 |
. . . . . 6
โข 0 <
((logโ(;10โ;27)) / (โโ(;10โ;27))) |
187 | 12, 18, 55 | ltmul1i 12080 |
. . . . . 6
โข (0 <
((logโ(;10โ;27)) / (โโ(;10โ;27))) โ ((7._3_48)
< ;10 โ ((7._3_48) ยท ((logโ(;10โ;27)) / (โโ(;10โ;27)))) < (;10 ยท ((logโ(;10โ;27)) / (โโ(;10โ;27)))))) |
188 | 186, 187 | ax-mp 5 |
. . . . 5
โข ((7._3_48) < ;10 โ ((7._3_48)
ยท ((logโ(;10โ;27)) / (โโ(;10โ;27)))) < (;10 ยท ((logโ(;10โ;27)) / (โโ(;10โ;27))))) |
189 | 172, 188 | mpbi 229 |
. . . 4
โข ((7._3_48) ยท ((logโ(;10โ;27)) / (โโ(;10โ;27)))) < (;10 ยท ((logโ(;10โ;27)) / (โโ(;10โ;27)))) |
190 | 18 | recni 11176 |
. . . . . . . . . . . . 13
โข ;10 โ โ |
191 | | expmul 14020 |
. . . . . . . . . . . . 13
โข ((;10 โ โ โง 7 โ
โ0 โง 2 โ โ0) โ (;10โ(7 ยท 2)) = ((;10โ7)โ2)) |
192 | 190, 1, 19, 191 | mp3an 1462 |
. . . . . . . . . . . 12
โข (;10โ(7 ยท 2)) = ((;10โ7)โ2) |
193 | | 7t2e14 12734 |
. . . . . . . . . . . . 13
โข (7
ยท 2) = ;14 |
194 | 193 | oveq2i 7373 |
. . . . . . . . . . . 12
โข (;10โ(7 ยท 2)) = (;10โ;14) |
195 | 192, 194 | eqtr3i 2767 |
. . . . . . . . . . 11
โข ((;10โ7)โ2) = (;10โ;14) |
196 | 195 | fveq2i 6850 |
. . . . . . . . . 10
โข
(โโ((;10โ7)โ2)) = (โโ(;10โ;14)) |
197 | | reexpcl 13991 |
. . . . . . . . . . . 12
โข ((;10 โ โ โง 7 โ
โ0) โ (;10โ7) โ โ) |
198 | 18, 1, 197 | mp2an 691 |
. . . . . . . . . . 11
โข (;10โ7) โ
โ |
199 | 1 | nn0zi 12535 |
. . . . . . . . . . . . 13
โข 7 โ
โค |
200 | | expgt0 14008 |
. . . . . . . . . . . . 13
โข ((;10 โ โ โง 7 โ
โค โง 0 < ;10) โ 0
< (;10โ7)) |
201 | 18, 199, 123, 200 | mp3an 1462 |
. . . . . . . . . . . 12
โข 0 <
(;10โ7) |
202 | 16, 198, 201 | ltleii 11285 |
. . . . . . . . . . 11
โข 0 โค
(;10โ7) |
203 | | sqrtsq 15161 |
. . . . . . . . . . 11
โข (((;10โ7) โ โ โง 0 โค
(;10โ7)) โ
(โโ((;10โ7)โ2)) = (;10โ7)) |
204 | 198, 202,
203 | mp2an 691 |
. . . . . . . . . 10
โข
(โโ((;10โ7)โ2)) = (;10โ7) |
205 | 196, 204 | eqtr3i 2767 |
. . . . . . . . 9
โข
(โโ(;10โ;14)) = (;10โ7) |
206 | 27, 59 | deccl 12640 |
. . . . . . . . . . . . 13
โข ;14 โ
โ0 |
207 | 206 | nn0zi 12535 |
. . . . . . . . . . . 12
โข ;14 โ โค |
208 | 18, 207, 146 | 3pm3.2i 1340 |
. . . . . . . . . . 11
โข (;10 โ โ โง ;14 โ โค โง ;27 โ โค) |
209 | | 1lt2 12331 |
. . . . . . . . . . . . 13
โข 1 <
2 |
210 | 27, 19, 59, 1, 164, 209 | decltc 12654 |
. . . . . . . . . . . 12
โข ;14 < ;27 |
211 | 177, 210 | pm3.2i 472 |
. . . . . . . . . . 11
โข (1 <
;10 โง ;14 < ;27) |
212 | | ltexp2a 14078 |
. . . . . . . . . . 11
โข (((;10 โ โ โง ;14 โ โค โง ;27 โ โค) โง (1 < ;10 โง ;14 < ;27)) โ (;10โ;14) < (;10โ;27)) |
213 | 208, 211,
212 | mp2an 691 |
. . . . . . . . . 10
โข (;10โ;14) < (;10โ;27) |
214 | | reexpcl 13991 |
. . . . . . . . . . . . 13
โข ((;10 โ โ โง ;14 โ โ0) โ
(;10โ;14) โ โ) |
215 | 18, 206, 214 | mp2an 691 |
. . . . . . . . . . . 12
โข (;10โ;14) โ โ |
216 | | expgt0 14008 |
. . . . . . . . . . . . . 14
โข ((;10 โ โ โง ;14 โ โค โง 0 < ;10) โ 0 < (;10โ;14)) |
217 | 18, 207, 123, 216 | mp3an 1462 |
. . . . . . . . . . . . 13
โข 0 <
(;10โ;14) |
218 | 16, 215, 217 | ltleii 11285 |
. . . . . . . . . . . 12
โข 0 โค
(;10โ;14) |
219 | 215, 218 | pm3.2i 472 |
. . . . . . . . . . 11
โข ((;10โ;14) โ โ โง 0 โค (;10โ;14)) |
220 | 16, 22, 36 | ltleii 11285 |
. . . . . . . . . . . 12
โข 0 โค
(;10โ;27) |
221 | 22, 220 | pm3.2i 472 |
. . . . . . . . . . 11
โข ((;10โ;27) โ โ โง 0 โค (;10โ;27)) |
222 | | sqrtlt 15153 |
. . . . . . . . . . 11
โข ((((;10โ;14) โ โ โง 0 โค (;10โ;14)) โง ((;10โ;27) โ โ โง 0 โค (;10โ;27))) โ ((;10โ;14) < (;10โ;27) โ (โโ(;10โ;14)) < (โโ(;10โ;27)))) |
223 | 219, 221,
222 | mp2an 691 |
. . . . . . . . . 10
โข ((;10โ;14) < (;10โ;27) โ (โโ(;10โ;14)) < (โโ(;10โ;27))) |
224 | 213, 223 | mpbi 229 |
. . . . . . . . 9
โข
(โโ(;10โ;14)) < (โโ(;10โ;27)) |
225 | 205, 224 | eqbrtrri 5133 |
. . . . . . . 8
โข (;10โ7) < (โโ(;10โ;27)) |
226 | 198, 201 | pm3.2i 472 |
. . . . . . . . 9
โข ((;10โ7) โ โ โง 0 <
(;10โ7)) |
227 | 52, 53 | pm3.2i 472 |
. . . . . . . . 9
โข
((โโ(;10โ;27)) โ โ โง 0 <
(โโ(;10โ;27))) |
228 | 51, 184 | pm3.2i 472 |
. . . . . . . . 9
โข
((logโ(;10โ;27)) โ โ โง 0 <
(logโ(;10โ;27))) |
229 | | ltdiv2 12048 |
. . . . . . . . 9
โข ((((;10โ7) โ โ โง 0 <
(;10โ7)) โง
((โโ(;10โ;27)) โ โ โง 0 <
(โโ(;10โ;27))) โง ((logโ(;10โ;27)) โ โ โง 0 < (logโ(;10โ;27)))) โ ((;10โ7) < (โโ(;10โ;27)) โ ((logโ(;10โ;27)) / (โโ(;10โ;27))) < ((logโ(;10โ;27)) / (;10โ7)))) |
230 | 226, 227,
228, 229 | mp3an 1462 |
. . . . . . . 8
โข ((;10โ7) < (โโ(;10โ;27)) โ ((logโ(;10โ;27)) / (โโ(;10โ;27))) < ((logโ(;10โ;27)) / (;10โ7))) |
231 | 225, 230 | mpbi 229 |
. . . . . . 7
โข
((logโ(;10โ;27)) / (โโ(;10โ;27))) < ((logโ(;10โ;27)) / (;10โ7)) |
232 | | 6nn 12249 |
. . . . . . . . . . . . . 14
โข 6 โ
โ |
233 | 232 | nngt0i 12199 |
. . . . . . . . . . . . . 14
โข 0 <
6 |
234 | 27, 26, 232, 233 | declt 12653 |
. . . . . . . . . . . . 13
โข ;10 < ;16 |
235 | | 6nn0 12441 |
. . . . . . . . . . . . . . . . 17
โข 6 โ
โ0 |
236 | 27, 235 | deccl 12640 |
. . . . . . . . . . . . . . . 16
โข ;16 โ
โ0 |
237 | 236 | nn0rei 12431 |
. . . . . . . . . . . . . . 15
โข ;16 โ โ |
238 | 25, 235, 26, 123 | declti 12663 |
. . . . . . . . . . . . . . 15
โข 0 <
;16 |
239 | | elrp 12924 |
. . . . . . . . . . . . . . 15
โข (;16 โ โ+ โ
(;16 โ โ โง 0 <
;16)) |
240 | 237, 238,
239 | mpbir2an 710 |
. . . . . . . . . . . . . 14
โข ;16 โ
โ+ |
241 | | logltb 25971 |
. . . . . . . . . . . . . 14
โข ((;10 โ โ+ โง
;16 โ โ+)
โ (;10 < ;16 โ (logโ;10) < (logโ;16))) |
242 | 125, 240,
241 | mp2an 691 |
. . . . . . . . . . . . 13
โข (;10 < ;16 โ (logโ;10) < (logโ;16)) |
243 | 234, 242 | mpbi 229 |
. . . . . . . . . . . 12
โข
(logโ;10) <
(logโ;16) |
244 | | 2exp4 16964 |
. . . . . . . . . . . . . 14
โข
(2โ4) = ;16 |
245 | 244 | fveq2i 6850 |
. . . . . . . . . . . . 13
โข
(logโ(2โ4)) = (logโ;16) |
246 | | 2rp 12927 |
. . . . . . . . . . . . . 14
โข 2 โ
โ+ |
247 | 59 | nn0zi 12535 |
. . . . . . . . . . . . . 14
โข 4 โ
โค |
248 | | relogexp 25967 |
. . . . . . . . . . . . . 14
โข ((2
โ โ+ โง 4 โ โค) โ
(logโ(2โ4)) = (4 ยท (logโ2))) |
249 | 246, 247,
248 | mp2an 691 |
. . . . . . . . . . . . 13
โข
(logโ(2โ4)) = (4 ยท (logโ2)) |
250 | 245, 249 | eqtr3i 2767 |
. . . . . . . . . . . 12
โข
(logโ;16) = (4
ยท (logโ2)) |
251 | 243, 250 | breqtri 5135 |
. . . . . . . . . . 11
โข
(logโ;10) < (4
ยท (logโ2)) |
252 | 100 | simpli 485 |
. . . . . . . . . . . . . . 15
โข 2 <
e |
253 | | logltb 25971 |
. . . . . . . . . . . . . . . 16
โข ((2
โ โ+ โง e โ โ+) โ (2 < e
โ (logโ2) < (logโe))) |
254 | 246, 102,
253 | mp2an 691 |
. . . . . . . . . . . . . . 15
โข (2 < e
โ (logโ2) < (logโe)) |
255 | 252, 254 | mpbi 229 |
. . . . . . . . . . . . . 14
โข
(logโ2) < (logโe) |
256 | 255, 99 | breqtri 5135 |
. . . . . . . . . . . . 13
โข
(logโ2) < 1 |
257 | | 4pos 12267 |
. . . . . . . . . . . . . 14
โข 0 <
4 |
258 | | relogcl 25947 |
. . . . . . . . . . . . . . . 16
โข (2 โ
โ+ โ (logโ2) โ โ) |
259 | 246, 258 | ax-mp 5 |
. . . . . . . . . . . . . . 15
โข
(logโ2) โ โ |
260 | 259, 28, 3 | ltmul2i 12083 |
. . . . . . . . . . . . . 14
โข (0 < 4
โ ((logโ2) < 1 โ (4 ยท (logโ2)) < (4 ยท
1))) |
261 | 257, 260 | ax-mp 5 |
. . . . . . . . . . . . 13
โข
((logโ2) < 1 โ (4 ยท (logโ2)) < (4 ยท
1)) |
262 | 256, 261 | mpbi 229 |
. . . . . . . . . . . 12
โข (4
ยท (logโ2)) < (4 ยท 1) |
263 | | 4cn 12245 |
. . . . . . . . . . . . 13
โข 4 โ
โ |
264 | 263 | mulid1i 11166 |
. . . . . . . . . . . 12
โข (4
ยท 1) = 4 |
265 | 262, 264 | breqtri 5135 |
. . . . . . . . . . 11
โข (4
ยท (logโ2)) < 4 |
266 | 3, 259 | remulcli 11178 |
. . . . . . . . . . . 12
โข (4
ยท (logโ2)) โ โ |
267 | 134, 266,
3 | lttri 11288 |
. . . . . . . . . . 11
โข
(((logโ;10) < (4
ยท (logโ2)) โง (4 ยท (logโ2)) < 4) โ
(logโ;10) <
4) |
268 | 251, 265,
267 | mp2an 691 |
. . . . . . . . . 10
โข
(logโ;10) <
4 |
269 | 134, 3, 92 | ltmul2i 12083 |
. . . . . . . . . . 11
โข (0 <
;27 โ ((logโ;10) < 4 โ (;27 ยท (logโ;10)) < (;27 ยท 4))) |
270 | 141, 269 | ax-mp 5 |
. . . . . . . . . 10
โข
((logโ;10) < 4
โ (;27 ยท
(logโ;10)) < (;27 ยท 4)) |
271 | 268, 270 | mpbi 229 |
. . . . . . . . 9
โข (;27 ยท (logโ;10)) < (;27 ยท 4) |
272 | 148, 271 | eqbrtri 5131 |
. . . . . . . 8
โข
(logโ(;10โ;27)) < (;27 ยท 4) |
273 | 92, 3 | remulcli 11178 |
. . . . . . . . . 10
โข (;27 ยท 4) โ
โ |
274 | 51, 273, 198 | ltdiv1i 12081 |
. . . . . . . . 9
โข (0 <
(;10โ7) โ
((logโ(;10โ;27)) < (;27 ยท 4) โ ((logโ(;10โ;27)) / (;10โ7)) < ((;27 ยท 4) / (;10โ7)))) |
275 | 201, 274 | ax-mp 5 |
. . . . . . . 8
โข
((logโ(;10โ;27)) < (;27 ยท 4) โ ((logโ(;10โ;27)) / (;10โ7)) < ((;27 ยท 4) / (;10โ7))) |
276 | 272, 275 | mpbi 229 |
. . . . . . 7
โข
((logโ(;10โ;27)) / (;10โ7)) < ((;27 ยท 4) / (;10โ7)) |
277 | 16, 201 | gtneii 11274 |
. . . . . . . . 9
โข (;10โ7) โ 0 |
278 | 51, 198, 277 | redivcli 11929 |
. . . . . . . 8
โข
((logโ(;10โ;27)) / (;10โ7)) โ โ |
279 | 273, 198,
277 | redivcli 11929 |
. . . . . . . 8
โข ((;27 ยท 4) / (;10โ7)) โ โ |
280 | 55, 278, 279 | lttri 11288 |
. . . . . . 7
โข
((((logโ(;10โ;27)) / (โโ(;10โ;27))) < ((logโ(;10โ;27)) / (;10โ7)) โง ((logโ(;10โ;27)) / (;10โ7)) < ((;27 ยท 4) / (;10โ7))) โ ((logโ(;10โ;27)) / (โโ(;10โ;27))) < ((;27 ยท 4) / (;10โ7))) |
281 | 231, 276,
280 | mp2an 691 |
. . . . . 6
โข
((logโ(;10โ;27)) / (โโ(;10โ;27))) < ((;27 ยท 4) / (;10โ7)) |
282 | | 7lt10 12758 |
. . . . . . . . . 10
โข 7 <
;10 |
283 | | 2lt10 12763 |
. . . . . . . . . 10
โข 2 <
;10 |
284 | 19, 173, 1, 26, 282, 283 | decltc 12654 |
. . . . . . . . 9
โข ;27 < ;;100 |
285 | | 10nn 12641 |
. . . . . . . . . . . . 13
โข ;10 โ โ |
286 | 285 | decnncl2 12649 |
. . . . . . . . . . . 12
โข ;;100 โ โ |
287 | 286 | nnrei 12169 |
. . . . . . . . . . 11
โข ;;100 โ โ |
288 | 92, 287, 3 | ltmul1i 12080 |
. . . . . . . . . 10
โข (0 < 4
โ (;27 < ;;100 โ (;27 ยท 4) < (;;100
ยท 4))) |
289 | 257, 288 | ax-mp 5 |
. . . . . . . . 9
โข (;27 < ;;100
โ (;27 ยท 4) <
(;;100 ยท 4)) |
290 | 284, 289 | mpbi 229 |
. . . . . . . 8
โข (;27 ยท 4) < (;;100
ยท 4) |
291 | 287, 3 | remulcli 11178 |
. . . . . . . . . 10
โข (;;100 ยท 4) โ โ |
292 | 273, 291,
198 | ltdiv1i 12081 |
. . . . . . . . 9
โข (0 <
(;10โ7) โ ((;27 ยท 4) < (;;100
ยท 4) โ ((;27 ยท
4) / (;10โ7)) < ((;;100 ยท 4) / (;10โ7)))) |
293 | 201, 292 | ax-mp 5 |
. . . . . . . 8
โข ((;27 ยท 4) < (;;100
ยท 4) โ ((;27 ยท
4) / (;10โ7)) < ((;;100 ยท 4) / (;10โ7))) |
294 | 290, 293 | mpbi 229 |
. . . . . . 7
โข ((;27 ยท 4) / (;10โ7)) < ((;;100
ยท 4) / (;10โ7)) |
295 | | 8nn 12255 |
. . . . . . . . . . . . . . 15
โข 8 โ
โ |
296 | | nnrp 12933 |
. . . . . . . . . . . . . . 15
โข (8 โ
โ โ 8 โ โ+) |
297 | 295, 296 | ax-mp 5 |
. . . . . . . . . . . . . 14
โข 8 โ
โ+ |
298 | 59, 297 | rpdp2cl 31780 |
. . . . . . . . . . . . 13
โข _48 โ
โ+ |
299 | 19, 298 | rpdp2cl 31780 |
. . . . . . . . . . . 12
โข _2_48 โ โ+ |
300 | 19, 299 | rpdp2cl 31780 |
. . . . . . . . . . 11
โข _2_2_48
โ โ+ |
301 | 59, 300 | dpgti 31804 |
. . . . . . . . . 10
โข 4 <
(4._2_2_48) |
302 | 72 | recni 11176 |
. . . . . . . . . . . . 13
โข (0._0_0_0_4_2_2_48)
โ โ |
303 | 198 | recni 11176 |
. . . . . . . . . . . . 13
โข (;10โ7) โ
โ |
304 | 302, 303 | mulcli 11169 |
. . . . . . . . . . . 12
โข ((0._0_0_0_4_2_2_48)
ยท (;10โ7)) โ
โ |
305 | 16, 123 | gtneii 11274 |
. . . . . . . . . . . . 13
โข ;10 โ 0 |
306 | 190, 305 | pm3.2i 472 |
. . . . . . . . . . . 12
โข (;10 โ โ โง ;10 โ 0) |
307 | 287 | recni 11176 |
. . . . . . . . . . . . 13
โข ;;100 โ โ |
308 | 286 | nnne0i 12200 |
. . . . . . . . . . . . 13
โข ;;100 โ 0 |
309 | 307, 308 | pm3.2i 472 |
. . . . . . . . . . . 12
โข (;;100 โ โ โง ;;100
โ 0) |
310 | | divdiv1 11873 |
. . . . . . . . . . . 12
โข
((((0._0_0_0_4_2_2_48)
ยท (;10โ7)) โ
โ โง (;10 โ โ
โง ;10 โ 0) โง (;;100 โ โ โง ;;100
โ 0)) โ ((((0._0_0_0_4_2_2_48)
ยท (;10โ7)) / ;10) / ;;100) =
(((0._0_0_0_4_2_2_48)
ยท (;10โ7)) / (;10 ยท ;;100))) |
311 | 304, 306,
309, 310 | mp3an 1462 |
. . . . . . . . . . 11
โข
((((0._0_0_0_4_2_2_48)
ยท (;10โ7)) / ;10) / ;;100) =
(((0._0_0_0_4_2_2_48)
ยท (;10โ7)) / (;10 ยท ;;100)) |
312 | 302, 303,
190, 305 | div23i 11920 |
. . . . . . . . . . . 12
โข
(((0._0_0_0_4_2_2_48)
ยท (;10โ7)) / ;10) = (((0._0_0_0_4_2_2_48) /
;10) ยท (;10โ7)) |
313 | 312 | oveq1i 7372 |
. . . . . . . . . . 11
โข
((((0._0_0_0_4_2_2_48)
ยท (;10โ7)) / ;10) / ;;100) =
((((0._0_0_0_4_2_2_48) /
;10) ยท (;10โ7)) / ;;100) |
314 | 190, 307 | mulcli 11169 |
. . . . . . . . . . . . 13
โข (;10 ยท ;;100)
โ โ |
315 | 190, 307,
305, 308 | mulne0i 11805 |
. . . . . . . . . . . . 13
โข (;10 ยท ;;100)
โ 0 |
316 | 302, 303,
314, 315 | divassi 11918 |
. . . . . . . . . . . 12
โข
(((0._0_0_0_4_2_2_48)
ยท (;10โ7)) / (;10 ยท ;;100))
= ((0._0_0_0_4_2_2_48)
ยท ((;10โ7) / (;10 ยท ;;100))) |
317 | | expp1 13981 |
. . . . . . . . . . . . . . . . . 18
โข ((;10 โ โ โง 2 โ
โ0) โ (;10โ(2 + 1)) = ((;10โ2) ยท ;10)) |
318 | 190, 19, 317 | mp2an 691 |
. . . . . . . . . . . . . . . . 17
โข (;10โ(2 + 1)) = ((;10โ2) ยท ;10) |
319 | | sq10 14171 |
. . . . . . . . . . . . . . . . . 18
โข (;10โ2) = ;;100 |
320 | 319 | oveq1i 7372 |
. . . . . . . . . . . . . . . . 17
โข ((;10โ2) ยท ;10) = (;;100
ยท ;10) |
321 | 307, 190 | mulcomi 11170 |
. . . . . . . . . . . . . . . . 17
โข (;;100 ยท ;10) = (;10 ยท ;;100) |
322 | 318, 320,
321 | 3eqtrri 2770 |
. . . . . . . . . . . . . . . 16
โข (;10 ยท ;;100) =
(;10โ(2 +
1)) |
323 | | 2p1e3 12302 |
. . . . . . . . . . . . . . . . 17
โข (2 + 1) =
3 |
324 | 323 | oveq2i 7373 |
. . . . . . . . . . . . . . . 16
โข (;10โ(2 + 1)) = (;10โ3) |
325 | 322, 324 | eqtri 2765 |
. . . . . . . . . . . . . . 15
โข (;10 ยท ;;100) =
(;10โ3) |
326 | 325 | oveq2i 7373 |
. . . . . . . . . . . . . 14
โข ((;10โ7) / (;10 ยท ;;100))
= ((;10โ7) / (;10โ3)) |
327 | 74 | nn0zi 12535 |
. . . . . . . . . . . . . . . 16
โข 3 โ
โค |
328 | 199, 327 | pm3.2i 472 |
. . . . . . . . . . . . . . 15
โข (7 โ
โค โง 3 โ โค) |
329 | | expsub 14023 |
. . . . . . . . . . . . . . 15
โข (((;10 โ โ โง ;10 โ 0) โง (7 โ โค
โง 3 โ โค)) โ (;10โ(7 โ 3)) = ((;10โ7) / (;10โ3))) |
330 | 306, 328,
329 | mp2an 691 |
. . . . . . . . . . . . . 14
โข (;10โ(7 โ 3)) = ((;10โ7) / (;10โ3)) |
331 | | 7cn 12254 |
. . . . . . . . . . . . . . . 16
โข 7 โ
โ |
332 | | 4p3e7 12314 |
. . . . . . . . . . . . . . . . 17
โข (4 + 3) =
7 |
333 | 263, 112,
332 | addcomli 11354 |
. . . . . . . . . . . . . . . 16
โข (3 + 4) =
7 |
334 | 331, 112,
263, 333 | subaddrii 11497 |
. . . . . . . . . . . . . . 15
โข (7
โ 3) = 4 |
335 | 334 | oveq2i 7373 |
. . . . . . . . . . . . . 14
โข (;10โ(7 โ 3)) = (;10โ4) |
336 | 326, 330,
335 | 3eqtr2i 2771 |
. . . . . . . . . . . . 13
โข ((;10โ7) / (;10 ยท ;;100))
= (;10โ4) |
337 | 336 | oveq2i 7373 |
. . . . . . . . . . . 12
โข ((0._0_0_0_4_2_2_48)
ยท ((;10โ7) / (;10 ยท ;;100)))
= ((0._0_0_0_4_2_2_48)
ยท (;10โ4)) |
338 | 173 | numexp1 16956 |
. . . . . . . . . . . . . 14
โข (;10โ1) = ;10 |
339 | 338 | oveq2i 7373 |
. . . . . . . . . . . . 13
โข ((0._4_2_2_48)
ยท (;10โ1)) = ((0._4_2_2_48)
ยท ;10) |
340 | 59, 300 | rpdp2cl 31780 |
. . . . . . . . . . . . . . 15
โข _4_2_2_48
โ โ+ |
341 | 25 | nnzi 12534 |
. . . . . . . . . . . . . . 15
โข 1 โ
โค |
342 | 89 | nnzi 12534 |
. . . . . . . . . . . . . . 15
โข 2 โ
โค |
343 | 26, 340, 98, 341, 342 | dpexpp1 31806 |
. . . . . . . . . . . . . 14
โข ((0._4_2_2_48)
ยท (;10โ1)) = ((0._0_4_2_2_48)
ยท (;10โ2)) |
344 | 26, 340 | rpdp2cl 31780 |
. . . . . . . . . . . . . . 15
โข _0_4_2_2_48
โ โ+ |
345 | 26, 344, 323, 342, 327 | dpexpp1 31806 |
. . . . . . . . . . . . . 14
โข ((0._0_4_2_2_48)
ยท (;10โ2)) = ((0._0_0_4_2_2_48)
ยท (;10โ3)) |
346 | 26, 344 | rpdp2cl 31780 |
. . . . . . . . . . . . . . 15
โข _0_0_4_2_2_48
โ โ+ |
347 | | 3p1e4 12305 |
. . . . . . . . . . . . . . 15
โข (3 + 1) =
4 |
348 | 26, 346, 347, 327, 247 | dpexpp1 31806 |
. . . . . . . . . . . . . 14
โข ((0._0_0_4_2_2_48)
ยท (;10โ3)) = ((0._0_0_0_4_2_2_48)
ยท (;10โ4)) |
349 | 343, 345,
348 | 3eqtri 2769 |
. . . . . . . . . . . . 13
โข ((0._4_2_2_48)
ยท (;10โ1)) = ((0._0_0_0_4_2_2_48)
ยท (;10โ4)) |
350 | 59, 300 | 0dp2dp 31807 |
. . . . . . . . . . . . 13
โข ((0._4_2_2_48)
ยท ;10) = (4._2_2_48) |
351 | 339, 349,
350 | 3eqtr3i 2773 |
. . . . . . . . . . . 12
โข ((0._0_0_0_4_2_2_48)
ยท (;10โ4)) = (4._2_2_48) |
352 | 316, 337,
351 | 3eqtri 2769 |
. . . . . . . . . . 11
โข
(((0._0_0_0_4_2_2_48)
ยท (;10โ7)) / (;10 ยท ;;100))
= (4._2_2_48) |
353 | 311, 313,
352 | 3eqtr3i 2773 |
. . . . . . . . . 10
โข
((((0._0_0_0_4_2_2_48) /
;10) ยท (;10โ7)) / ;;100) =
(4._2_2_48) |
354 | 301, 353 | breqtrri 5137 |
. . . . . . . . 9
โข 4 <
((((0._0_0_0_4_2_2_48) /
;10) ยท (;10โ7)) / ;;100) |
355 | 72, 18, 305 | redivcli 11929 |
. . . . . . . . . . 11
โข ((0._0_0_0_4_2_2_48) /
;10) โ
โ |
356 | 355, 198 | remulcli 11178 |
. . . . . . . . . 10
โข
(((0._0_0_0_4_2_2_48) /
;10) ยท (;10โ7)) โ โ |
357 | 286 | nngt0i 12199 |
. . . . . . . . . . 11
โข 0 <
;;100 |
358 | 287, 357 | pm3.2i 472 |
. . . . . . . . . 10
โข (;;100 โ โ โง 0 < ;;100) |
359 | | ltmuldiv2 12036 |
. . . . . . . . . 10
โข ((4
โ โ โง (((0._0_0_0_4_2_2_48) /
;10) ยท (;10โ7)) โ โ โง (;;100
โ โ โง 0 < ;;100)) โ ((;;100
ยท 4) < (((0._0_0_0_4_2_2_48) /
;10) ยท (;10โ7)) โ 4 < ((((0._0_0_0_4_2_2_48) /
;10) ยท (;10โ7)) / ;;100))) |
360 | 3, 356, 358, 359 | mp3an 1462 |
. . . . . . . . 9
โข ((;;100 ยท 4) < (((0._0_0_0_4_2_2_48) /
;10) ยท (;10โ7)) โ 4 < ((((0._0_0_0_4_2_2_48) /
;10) ยท (;10โ7)) / ;;100)) |
361 | 354, 360 | mpbir 230 |
. . . . . . . 8
โข (;;100 ยท 4) < (((0._0_0_0_4_2_2_48) /
;10) ยท (;10โ7)) |
362 | | ltdivmul2 12039 |
. . . . . . . . 9
โข (((;;100 ยท 4) โ โ โง ((0._0_0_0_4_2_2_48) /
;10) โ โ โง ((;10โ7) โ โ โง 0 <
(;10โ7))) โ (((;;100 ยท 4) / (;10โ7)) < ((0._0_0_0_4_2_2_48) /
;10) โ (;;100
ยท 4) < (((0._0_0_0_4_2_2_48) /
;10) ยท (;10โ7)))) |
363 | 291, 355,
226, 362 | mp3an 1462 |
. . . . . . . 8
โข (((;;100 ยท 4) / (;10โ7)) < ((0._0_0_0_4_2_2_48) /
;10) โ (;;100
ยท 4) < (((0._0_0_0_4_2_2_48) /
;10) ยท (;10โ7))) |
364 | 361, 363 | mpbir 230 |
. . . . . . 7
โข ((;;100 ยท 4) / (;10โ7)) < ((0._0_0_0_4_2_2_48) /
;10) |
365 | 291, 198,
277 | redivcli 11929 |
. . . . . . . 8
โข ((;;100 ยท 4) / (;10โ7)) โ โ |
366 | 279, 365,
355 | lttri 11288 |
. . . . . . 7
โข ((((;27 ยท 4) / (;10โ7)) < ((;;100
ยท 4) / (;10โ7)) โง
((;;100 ยท 4) / (;10โ7)) < ((0._0_0_0_4_2_2_48) /
;10)) โ ((;27 ยท 4) / (;10โ7)) < ((0._0_0_0_4_2_2_48) /
;10)) |
367 | 294, 364,
366 | mp2an 691 |
. . . . . 6
โข ((;27 ยท 4) / (;10โ7)) < ((0._0_0_0_4_2_2_48) /
;10) |
368 | 226 | simpli 485 |
. . . . . . . 8
โข (;10โ7) โ
โ |
369 | 273, 368,
277 | redivcli 11929 |
. . . . . . 7
โข ((;27 ยท 4) / (;10โ7)) โ โ |
370 | 55, 369, 355 | lttri 11288 |
. . . . . 6
โข
((((logโ(;10โ;27)) / (โโ(;10โ;27))) < ((;27 ยท 4) / (;10โ7)) โง ((;27 ยท 4) / (;10โ7)) < ((0._0_0_0_4_2_2_48) /
;10)) โ ((logโ(;10โ;27)) / (โโ(;10โ;27))) < ((0._0_0_0_4_2_2_48) /
;10)) |
371 | 281, 367,
370 | mp2an 691 |
. . . . 5
โข
((logโ(;10โ;27)) / (โโ(;10โ;27))) < ((0._0_0_0_4_2_2_48) /
;10) |
372 | 125, 124 | mpbi 229 |
. . . . . 6
โข (;10 โ โ โง 0 < ;10) |
373 | | ltmuldiv2 12036 |
. . . . . 6
โข
((((logโ(;10โ;27)) / (โโ(;10โ;27))) โ โ โง (0._0_0_0_4_2_2_48)
โ โ โง (;10 โ
โ โง 0 < ;10)) โ
((;10 ยท ((logโ(;10โ;27)) / (โโ(;10โ;27)))) < (0._0_0_0_4_2_2_48)
โ ((logโ(;10โ;27)) / (โโ(;10โ;27))) < ((0._0_0_0_4_2_2_48) /
;10))) |
374 | 55, 72, 372, 373 | mp3an 1462 |
. . . . 5
โข ((;10 ยท ((logโ(;10โ;27)) / (โโ(;10โ;27)))) < (0._0_0_0_4_2_2_48)
โ ((logโ(;10โ;27)) / (โโ(;10โ;27))) < ((0._0_0_0_4_2_2_48) /
;10)) |
375 | 371, 374 | mpbir 230 |
. . . 4
โข (;10 ยท ((logโ(;10โ;27)) / (โโ(;10โ;27)))) < (0._0_0_0_4_2_2_48) |
376 | 12, 55 | remulcli 11178 |
. . . . 5
โข ((7._3_48) ยท ((logโ(;10โ;27)) / (โโ(;10โ;27)))) โ โ |
377 | 18, 55 | remulcli 11178 |
. . . . 5
โข (;10 ยท ((logโ(;10โ;27)) / (โโ(;10โ;27)))) โ โ |
378 | 376, 377,
72 | lttri 11288 |
. . . 4
โข
((((7._3_48) ยท ((logโ(;10โ;27)) / (โโ(;10โ;27)))) < (;10 ยท ((logโ(;10โ;27)) / (โโ(;10โ;27)))) โง (;10 ยท ((logโ(;10โ;27)) / (โโ(;10โ;27)))) < (0._0_0_0_4_2_2_48))
โ ((7._3_48) ยท ((logโ(;10โ;27)) / (โโ(;10โ;27)))) < (0._0_0_0_4_2_2_48)) |
379 | 189, 375,
378 | mp2an 691 |
. . 3
โข ((7._3_48) ยท ((logโ(;10โ;27)) / (โโ(;10โ;27)))) < (0._0_0_0_4_2_2_48) |
380 | 379 | a1i 11 |
. 2
โข ((๐ โ โ0
โง (;10โ;27) โค ๐) โ ((7._3_48)
ยท ((logโ(;10โ;27)) / (โโ(;10โ;27)))) < (0._0_0_0_4_2_2_48)) |
381 | 47, 57, 73, 162, 380 | lelttrd 11320 |
1
โข ((๐ โ โ0
โง (;10โ;27) โค ๐) โ ((7._3_48)
ยท ((logโ๐) /
(โโ๐))) <
(0._0_0_0_4_2_2_48)) |