Step | Hyp | Ref
| Expression |
1 | | reelprrecn 11150 |
. . 3
โข โ
โ {โ, โ} |
2 | 1 | a1i 11 |
. 2
โข (๐ โ โ โ {โ,
โ}) |
3 | | 2cnd 12238 |
. . 3
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ 2 โ โ) |
4 | | 2re 12234 |
. . . . . 6
โข 2 โ
โ |
5 | 4 | a1i 11 |
. . . . 5
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ 2 โ โ) |
6 | | 2pos 12263 |
. . . . . 6
โข 0 <
2 |
7 | 6 | a1i 11 |
. . . . 5
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ 0 < 2) |
8 | | elioore 13301 |
. . . . . . . . 9
โข (๐ฅ โ (๐ด(,)๐ต) โ ๐ฅ โ โ) |
9 | 8 | adantl 483 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ ๐ฅ โ โ) |
10 | | 0red 11165 |
. . . . . . . . 9
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ 0 โ โ) |
11 | | aks4d1p1p6.1 |
. . . . . . . . . 10
โข (๐ โ ๐ด โ โ) |
12 | 11 | adantr 482 |
. . . . . . . . 9
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ ๐ด โ โ) |
13 | | 3re 12240 |
. . . . . . . . . . 11
โข 3 โ
โ |
14 | 13 | a1i 11 |
. . . . . . . . . 10
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ 3 โ โ) |
15 | | 3pos 12265 |
. . . . . . . . . . 11
โข 0 <
3 |
16 | 15 | a1i 11 |
. . . . . . . . . 10
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ 0 < 3) |
17 | | aks4d1p1p6.3 |
. . . . . . . . . . 11
โข (๐ โ 3 โค ๐ด) |
18 | 17 | adantr 482 |
. . . . . . . . . 10
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ 3 โค ๐ด) |
19 | 10, 14, 12, 16, 18 | ltletrd 11322 |
. . . . . . . . 9
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ 0 < ๐ด) |
20 | | simpr 486 |
. . . . . . . . . . 11
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ ๐ฅ โ (๐ด(,)๐ต)) |
21 | 11 | rexrd 11212 |
. . . . . . . . . . . . 13
โข (๐ โ ๐ด โ
โ*) |
22 | 21 | adantr 482 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ ๐ด โ
โ*) |
23 | | aks4d1p1p6.2 |
. . . . . . . . . . . . . 14
โข (๐ โ ๐ต โ โ) |
24 | 23 | rexrd 11212 |
. . . . . . . . . . . . 13
โข (๐ โ ๐ต โ
โ*) |
25 | 24 | adantr 482 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ ๐ต โ
โ*) |
26 | 9 | rexrd 11212 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ ๐ฅ โ โ*) |
27 | | elioo5 13328 |
. . . . . . . . . . . 12
โข ((๐ด โ โ*
โง ๐ต โ
โ* โง ๐ฅ
โ โ*) โ (๐ฅ โ (๐ด(,)๐ต) โ (๐ด < ๐ฅ โง ๐ฅ < ๐ต))) |
28 | 22, 25, 26, 27 | syl3anc 1372 |
. . . . . . . . . . 11
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ (๐ฅ โ (๐ด(,)๐ต) โ (๐ด < ๐ฅ โง ๐ฅ < ๐ต))) |
29 | 20, 28 | mpbid 231 |
. . . . . . . . . 10
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ (๐ด < ๐ฅ โง ๐ฅ < ๐ต)) |
30 | 29 | simpld 496 |
. . . . . . . . 9
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ ๐ด < ๐ฅ) |
31 | 10, 12, 9, 19, 30 | lttrd 11323 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ 0 < ๐ฅ) |
32 | | 1red 11163 |
. . . . . . . . . 10
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ 1 โ โ) |
33 | | 1lt2 12331 |
. . . . . . . . . . 11
โข 1 <
2 |
34 | 33 | a1i 11 |
. . . . . . . . . 10
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ 1 < 2) |
35 | 32, 34 | ltned 11298 |
. . . . . . . . 9
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ 1 โ 2) |
36 | 35 | necomd 3000 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ 2 โ 1) |
37 | 5, 7, 9, 31, 36 | relogbcld 40459 |
. . . . . . 7
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ (2 logb ๐ฅ) โ
โ) |
38 | | 5nn0 12440 |
. . . . . . . 8
โข 5 โ
โ0 |
39 | 38 | a1i 11 |
. . . . . . 7
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ 5 โ
โ0) |
40 | 37, 39 | reexpcld 14075 |
. . . . . 6
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ ((2 logb ๐ฅ)โ5) โ
โ) |
41 | 40, 32 | readdcld 11191 |
. . . . 5
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ (((2 logb ๐ฅ)โ5) + 1) โ
โ) |
42 | 10, 32 | readdcld 11191 |
. . . . . 6
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ (0 + 1) โ
โ) |
43 | 10 | ltp1d 12092 |
. . . . . 6
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ 0 < (0 + 1)) |
44 | 39 | nn0zd 12532 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ 5 โ โค) |
45 | | 2cnd 12238 |
. . . . . . . . . . 11
โข (โค
โ 2 โ โ) |
46 | | 0red 11165 |
. . . . . . . . . . . . 13
โข (โค
โ 0 โ โ) |
47 | 6 | a1i 11 |
. . . . . . . . . . . . 13
โข (โค
โ 0 < 2) |
48 | 46, 47 | ltned 11298 |
. . . . . . . . . . . 12
โข (โค
โ 0 โ 2) |
49 | 48 | necomd 3000 |
. . . . . . . . . . 11
โข (โค
โ 2 โ 0) |
50 | | 1red 11163 |
. . . . . . . . . . . . 13
โข (โค
โ 1 โ โ) |
51 | 33 | a1i 11 |
. . . . . . . . . . . . 13
โข (โค
โ 1 < 2) |
52 | 50, 51 | ltned 11298 |
. . . . . . . . . . . 12
โข (โค
โ 1 โ 2) |
53 | 52 | necomd 3000 |
. . . . . . . . . . 11
โข (โค
โ 2 โ 1) |
54 | | logb1 26135 |
. . . . . . . . . . 11
โข ((2
โ โ โง 2 โ 0 โง 2 โ 1) โ (2 logb 1) =
0) |
55 | 45, 49, 53, 54 | syl3anc 1372 |
. . . . . . . . . 10
โข (โค
โ (2 logb 1) = 0) |
56 | 55 | mptru 1549 |
. . . . . . . . 9
โข (2
logb 1) = 0 |
57 | | 2lt3 12332 |
. . . . . . . . . . . . . 14
โข 2 <
3 |
58 | 57 | a1i 11 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ 2 < 3) |
59 | 32, 5, 14, 34, 58 | lttrd 11323 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ 1 < 3) |
60 | 32, 14, 12, 59, 18 | ltletrd 11322 |
. . . . . . . . . . 11
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ 1 < ๐ด) |
61 | 32, 12, 9, 60, 30 | lttrd 11323 |
. . . . . . . . . 10
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ 1 < ๐ฅ) |
62 | | 2z 12542 |
. . . . . . . . . . . . 13
โข 2 โ
โค |
63 | 62 | a1i 11 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ 2 โ โค) |
64 | 63 | uzidd 12786 |
. . . . . . . . . . 11
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ 2 โ
(โคโฅโ2)) |
65 | | 1rp 12926 |
. . . . . . . . . . . 12
โข 1 โ
โ+ |
66 | 65 | a1i 11 |
. . . . . . . . . . 11
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ 1 โ
โ+) |
67 | 9, 31 | elrpd 12961 |
. . . . . . . . . . 11
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ ๐ฅ โ โ+) |
68 | | logblt 26150 |
. . . . . . . . . . 11
โข ((2
โ (โคโฅโ2) โง 1 โ โ+
โง ๐ฅ โ
โ+) โ (1 < ๐ฅ โ (2 logb 1) < (2
logb ๐ฅ))) |
69 | 64, 66, 67, 68 | syl3anc 1372 |
. . . . . . . . . 10
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ (1 < ๐ฅ โ (2 logb 1) < (2
logb ๐ฅ))) |
70 | 61, 69 | mpbid 231 |
. . . . . . . . 9
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ (2 logb 1) < (2
logb ๐ฅ)) |
71 | 56, 70 | eqbrtrrid 5146 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ 0 < (2 logb ๐ฅ)) |
72 | | expgt0 14008 |
. . . . . . . 8
โข (((2
logb ๐ฅ) โ
โ โง 5 โ โค โง 0 < (2 logb ๐ฅ)) โ 0 < ((2
logb ๐ฅ)โ5)) |
73 | 37, 44, 71, 72 | syl3anc 1372 |
. . . . . . 7
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ 0 < ((2 logb ๐ฅ)โ5)) |
74 | 10, 40, 32, 73 | ltadd1dd 11773 |
. . . . . 6
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ (0 + 1) < (((2 logb
๐ฅ)โ5) +
1)) |
75 | 10, 42, 41, 43, 74 | lttrd 11323 |
. . . . 5
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ 0 < (((2 logb ๐ฅ)โ5) + 1)) |
76 | 5, 7, 41, 75, 36 | relogbcld 40459 |
. . . 4
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ (2 logb (((2
logb ๐ฅ)โ5)
+ 1)) โ โ) |
77 | | recn 11148 |
. . . 4
โข ((2
logb (((2 logb ๐ฅ)โ5) + 1)) โ โ โ (2
logb (((2 logb ๐ฅ)โ5) + 1)) โ
โ) |
78 | 76, 77 | syl 17 |
. . 3
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ (2 logb (((2
logb ๐ฅ)โ5)
+ 1)) โ โ) |
79 | 3, 78 | mulcld 11182 |
. 2
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ (2 ยท (2 logb
(((2 logb ๐ฅ)โ5) + 1))) โ
โ) |
80 | | 2rp 12927 |
. . . . . . . 8
โข 2 โ
โ+ |
81 | 80 | a1i 11 |
. . . . . . 7
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ 2 โ
โ+) |
82 | 81 | relogcld 25994 |
. . . . . 6
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ (logโ2) โ
โ) |
83 | 41, 82 | remulcld 11192 |
. . . . 5
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ ((((2 logb ๐ฅ)โ5) + 1) ยท
(logโ2)) โ โ) |
84 | 40 | recnd 11190 |
. . . . . . 7
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ ((2 logb ๐ฅ)โ5) โ
โ) |
85 | | 1cnd 11157 |
. . . . . . 7
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ 1 โ โ) |
86 | 84, 85 | addcld 11181 |
. . . . . 6
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ (((2 logb ๐ฅ)โ5) + 1) โ
โ) |
87 | 7 | gt0ne0d 11726 |
. . . . . . 7
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ 2 โ 0) |
88 | 3, 87 | logcld 25942 |
. . . . . 6
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ (logโ2) โ
โ) |
89 | 75 | gt0ne0d 11726 |
. . . . . 6
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ (((2 logb ๐ฅ)โ5) + 1) โ
0) |
90 | | 0red 11165 |
. . . . . . . . 9
โข (๐ โ 0 โ
โ) |
91 | | loggt0b 26003 |
. . . . . . . . . . . 12
โข (2 โ
โ+ โ (0 < (logโ2) โ 1 <
2)) |
92 | 80, 91 | ax-mp 5 |
. . . . . . . . . . 11
โข (0 <
(logโ2) โ 1 < 2) |
93 | 33, 92 | mpbir 230 |
. . . . . . . . . 10
โข 0 <
(logโ2) |
94 | 93 | a1i 11 |
. . . . . . . . 9
โข (๐ โ 0 <
(logโ2)) |
95 | 90, 94 | ltned 11298 |
. . . . . . . 8
โข (๐ โ 0 โ
(logโ2)) |
96 | 95 | necomd 3000 |
. . . . . . 7
โข (๐ โ (logโ2) โ
0) |
97 | 96 | adantr 482 |
. . . . . 6
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ (logโ2) โ
0) |
98 | 86, 88, 89, 97 | mulne0d 11814 |
. . . . 5
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ ((((2 logb ๐ฅ)โ5) + 1) ยท
(logโ2)) โ 0) |
99 | 32, 83, 98 | redivcld 11990 |
. . . 4
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ (1 / ((((2 logb ๐ฅ)โ5) + 1) ยท
(logโ2))) โ โ) |
100 | | 5re 12247 |
. . . . . . . 8
โข 5 โ
โ |
101 | 100 | a1i 11 |
. . . . . . 7
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ 5 โ โ) |
102 | | 4nn0 12439 |
. . . . . . . . 9
โข 4 โ
โ0 |
103 | 102 | a1i 11 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ 4 โ
โ0) |
104 | 37, 103 | reexpcld 14075 |
. . . . . . 7
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ ((2 logb ๐ฅ)โ4) โ
โ) |
105 | 101, 104 | remulcld 11192 |
. . . . . 6
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ (5 ยท ((2 logb
๐ฅ)โ4)) โ
โ) |
106 | 9, 82 | remulcld 11192 |
. . . . . . 7
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ (๐ฅ ยท (logโ2)) โ
โ) |
107 | 9 | recnd 11190 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ ๐ฅ โ โ) |
108 | 10, 31 | gtned 11297 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ ๐ฅ โ 0) |
109 | 107, 88, 108, 97 | mulne0d 11814 |
. . . . . . 7
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ (๐ฅ ยท (logโ2)) โ
0) |
110 | 32, 106, 109 | redivcld 11990 |
. . . . . 6
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ (1 / (๐ฅ ยท (logโ2))) โ
โ) |
111 | 105, 110 | remulcld 11192 |
. . . . 5
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ ((5 ยท ((2 logb
๐ฅ)โ4)) ยท (1 /
(๐ฅ ยท
(logโ2)))) โ โ) |
112 | 111, 10 | readdcld 11191 |
. . . 4
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ (((5 ยท ((2 logb
๐ฅ)โ4)) ยท (1 /
(๐ฅ ยท
(logโ2)))) + 0) โ โ) |
113 | 99, 112 | remulcld 11192 |
. . 3
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ ((1 / ((((2 logb ๐ฅ)โ5) + 1) ยท
(logโ2))) ยท (((5 ยท ((2 logb ๐ฅ)โ4)) ยท (1 / (๐ฅ ยท (logโ2)))) + 0)) โ
โ) |
114 | 5, 113 | remulcld 11192 |
. 2
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ (2 ยท ((1 / ((((2
logb ๐ฅ)โ5)
+ 1) ยท (logโ2))) ยท (((5 ยท ((2 logb ๐ฅ)โ4)) ยท (1 / (๐ฅ ยท (logโ2)))) +
0))) โ โ) |
115 | 41, 75 | elrpd 12961 |
. . . 4
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ (((2 logb ๐ฅ)โ5) + 1) โ
โ+) |
116 | 4 | a1i 11 |
. . . . . 6
โข ((๐ โง ๐ฆ โ โ+) โ 2 โ
โ) |
117 | 6 | a1i 11 |
. . . . . 6
โข ((๐ โง ๐ฆ โ โ+) โ 0 <
2) |
118 | | rpre 12930 |
. . . . . . 7
โข (๐ฆ โ โ+
โ ๐ฆ โ
โ) |
119 | 118 | adantl 483 |
. . . . . 6
โข ((๐ โง ๐ฆ โ โ+) โ ๐ฆ โ
โ) |
120 | | rpgt0 12934 |
. . . . . . 7
โข (๐ฆ โ โ+
โ 0 < ๐ฆ) |
121 | 120 | adantl 483 |
. . . . . 6
โข ((๐ โง ๐ฆ โ โ+) โ 0 <
๐ฆ) |
122 | | 1red 11163 |
. . . . . . . 8
โข ((๐ โง ๐ฆ โ โ+) โ 1 โ
โ) |
123 | 33 | a1i 11 |
. . . . . . . 8
โข ((๐ โง ๐ฆ โ โ+) โ 1 <
2) |
124 | 122, 123 | ltned 11298 |
. . . . . . 7
โข ((๐ โง ๐ฆ โ โ+) โ 1 โ
2) |
125 | 124 | necomd 3000 |
. . . . . 6
โข ((๐ โง ๐ฆ โ โ+) โ 2 โ
1) |
126 | 116, 117,
119, 121, 125 | relogbcld 40459 |
. . . . 5
โข ((๐ โง ๐ฆ โ โ+) โ (2
logb ๐ฆ) โ
โ) |
127 | 126 | recnd 11190 |
. . . 4
โข ((๐ โง ๐ฆ โ โ+) โ (2
logb ๐ฆ) โ
โ) |
128 | 80 | a1i 11 |
. . . . . . 7
โข ((๐ โง ๐ฆ โ โ+) โ 2 โ
โ+) |
129 | 128 | relogcld 25994 |
. . . . . 6
โข ((๐ โง ๐ฆ โ โ+) โ
(logโ2) โ โ) |
130 | 119, 129 | remulcld 11192 |
. . . . 5
โข ((๐ โง ๐ฆ โ โ+) โ (๐ฆ ยท (logโ2)) โ
โ) |
131 | 119 | recnd 11190 |
. . . . . 6
โข ((๐ โง ๐ฆ โ โ+) โ ๐ฆ โ
โ) |
132 | | 2cnd 12238 |
. . . . . . 7
โข ((๐ โง ๐ฆ โ โ+) โ 2 โ
โ) |
133 | 128 | rpne0d 12969 |
. . . . . . 7
โข ((๐ โง ๐ฆ โ โ+) โ 2 โ
0) |
134 | 132, 133 | logcld 25942 |
. . . . . 6
โข ((๐ โง ๐ฆ โ โ+) โ
(logโ2) โ โ) |
135 | | rpne0 12938 |
. . . . . . 7
โข (๐ฆ โ โ+
โ ๐ฆ โ
0) |
136 | 135 | adantl 483 |
. . . . . 6
โข ((๐ โง ๐ฆ โ โ+) โ ๐ฆ โ 0) |
137 | 96 | necomd 3000 |
. . . . . . . 8
โข (๐ โ 0 โ
(logโ2)) |
138 | 137 | adantr 482 |
. . . . . . 7
โข ((๐ โง ๐ฆ โ โ+) โ 0 โ
(logโ2)) |
139 | 138 | necomd 3000 |
. . . . . 6
โข ((๐ โง ๐ฆ โ โ+) โ
(logโ2) โ 0) |
140 | 131, 134,
136, 139 | mulne0d 11814 |
. . . . 5
โข ((๐ โง ๐ฆ โ โ+) โ (๐ฆ ยท (logโ2)) โ
0) |
141 | 122, 130,
140 | redivcld 11990 |
. . . 4
โข ((๐ โง ๐ฆ โ โ+) โ (1 /
(๐ฆ ยท (logโ2)))
โ โ) |
142 | | cnelprrecn 11151 |
. . . . . . 7
โข โ
โ {โ, โ} |
143 | 142 | a1i 11 |
. . . . . 6
โข (๐ โ โ โ {โ,
โ}) |
144 | 37 | recnd 11190 |
. . . . . 6
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ (2 logb ๐ฅ) โ
โ) |
145 | | simpr 486 |
. . . . . . 7
โข ((๐ โง ๐ง โ โ) โ ๐ง โ โ) |
146 | 38 | a1i 11 |
. . . . . . 7
โข ((๐ โง ๐ง โ โ) โ 5 โ
โ0) |
147 | 145, 146 | expcld 14058 |
. . . . . 6
โข ((๐ โง ๐ง โ โ) โ (๐งโ5) โ โ) |
148 | | 5cn 12248 |
. . . . . . . 8
โข 5 โ
โ |
149 | 148 | a1i 11 |
. . . . . . 7
โข ((๐ โง ๐ง โ โ) โ 5 โ
โ) |
150 | 102 | a1i 11 |
. . . . . . . 8
โข ((๐ โง ๐ง โ โ) โ 4 โ
โ0) |
151 | 145, 150 | expcld 14058 |
. . . . . . 7
โข ((๐ โง ๐ง โ โ) โ (๐งโ4) โ โ) |
152 | 149, 151 | mulcld 11182 |
. . . . . 6
โข ((๐ โง ๐ง โ โ) โ (5 ยท (๐งโ4)) โ
โ) |
153 | 13 | a1i 11 |
. . . . . . . . 9
โข (๐ โ 3 โ
โ) |
154 | 15 | a1i 11 |
. . . . . . . . 9
โข (๐ โ 0 < 3) |
155 | 90, 153, 11, 154, 17 | ltletrd 11322 |
. . . . . . . 8
โข (๐ โ 0 < ๐ด) |
156 | 90, 11, 155 | ltled 11310 |
. . . . . . 7
โข (๐ โ 0 โค ๐ด) |
157 | | aks4d1p1p6.4 |
. . . . . . 7
โข (๐ โ ๐ด โค ๐ต) |
158 | | eqid 2737 |
. . . . . . 7
โข (๐ฅ โ (๐ด(,)๐ต) โฆ (2 logb ๐ฅ)) = (๐ฅ โ (๐ด(,)๐ต) โฆ (2 logb ๐ฅ)) |
159 | | eqid 2737 |
. . . . . . 7
โข (๐ฅ โ (๐ด(,)๐ต) โฆ (1 / (๐ฅ ยท (logโ2)))) = (๐ฅ โ (๐ด(,)๐ต) โฆ (1 / (๐ฅ ยท (logโ2)))) |
160 | 21, 24, 156, 157, 158, 159 | dvrelog2b 40552 |
. . . . . 6
โข (๐ โ (โ D (๐ฅ โ (๐ด(,)๐ต) โฆ (2 logb ๐ฅ))) = (๐ฅ โ (๐ด(,)๐ต) โฆ (1 / (๐ฅ ยท (logโ2))))) |
161 | | 5nn 12246 |
. . . . . . . 8
โข 5 โ
โ |
162 | | dvexp 25333 |
. . . . . . . 8
โข (5 โ
โ โ (โ D (๐ง โ โ โฆ (๐งโ5))) = (๐ง โ โ โฆ (5 ยท (๐งโ(5 โ
1))))) |
163 | 161, 162 | ax-mp 5 |
. . . . . . 7
โข (โ
D (๐ง โ โ โฆ
(๐งโ5))) = (๐ง โ โ โฆ (5
ยท (๐งโ(5 โ
1)))) |
164 | | 5m1e4 12290 |
. . . . . . . . . . 11
โข (5
โ 1) = 4 |
165 | 164 | a1i 11 |
. . . . . . . . . 10
โข ((๐ โง ๐ง โ โ) โ (5 โ 1) =
4) |
166 | 165 | oveq2d 7378 |
. . . . . . . . 9
โข ((๐ โง ๐ง โ โ) โ (๐งโ(5 โ 1)) = (๐งโ4)) |
167 | 166 | oveq2d 7378 |
. . . . . . . 8
โข ((๐ โง ๐ง โ โ) โ (5 ยท (๐งโ(5 โ 1))) = (5
ยท (๐งโ4))) |
168 | 167 | mpteq2dva 5210 |
. . . . . . 7
โข (๐ โ (๐ง โ โ โฆ (5 ยท (๐งโ(5 โ 1)))) = (๐ง โ โ โฆ (5
ยท (๐งโ4)))) |
169 | 163, 168 | eqtrid 2789 |
. . . . . 6
โข (๐ โ (โ D (๐ง โ โ โฆ (๐งโ5))) = (๐ง โ โ โฆ (5 ยท (๐งโ4)))) |
170 | | oveq1 7369 |
. . . . . 6
โข (๐ง = (2 logb ๐ฅ) โ (๐งโ5) = ((2 logb ๐ฅ)โ5)) |
171 | | oveq1 7369 |
. . . . . . 7
โข (๐ง = (2 logb ๐ฅ) โ (๐งโ4) = ((2 logb ๐ฅ)โ4)) |
172 | 171 | oveq2d 7378 |
. . . . . 6
โข (๐ง = (2 logb ๐ฅ) โ (5 ยท (๐งโ4)) = (5 ยท ((2
logb ๐ฅ)โ4))) |
173 | 2, 143, 144, 110, 147, 152, 160, 169, 170, 172 | dvmptco 25352 |
. . . . 5
โข (๐ โ (โ D (๐ฅ โ (๐ด(,)๐ต) โฆ ((2 logb ๐ฅ)โ5))) = (๐ฅ โ (๐ด(,)๐ต) โฆ ((5 ยท ((2 logb
๐ฅ)โ4)) ยท (1 /
(๐ฅ ยท
(logโ2)))))) |
174 | | 1cnd 11157 |
. . . . . . 7
โข (๐ โ 1 โ
โ) |
175 | 174 | adantr 482 |
. . . . . 6
โข ((๐ โง ๐ฅ โ โ) โ 1 โ
โ) |
176 | | 0red 11165 |
. . . . . 6
โข ((๐ โง ๐ฅ โ โ) โ 0 โ
โ) |
177 | 2, 174 | dvmptc 25338 |
. . . . . 6
โข (๐ โ (โ D (๐ฅ โ โ โฆ 1)) =
(๐ฅ โ โ โฆ
0)) |
178 | | ioossre 13332 |
. . . . . . 7
โข (๐ด(,)๐ต) โ โ |
179 | 178 | a1i 11 |
. . . . . 6
โข (๐ โ (๐ด(,)๐ต) โ โ) |
180 | | eqid 2737 |
. . . . . . 7
โข
(TopOpenโโfld) =
(TopOpenโโfld) |
181 | 180 | tgioo2 24182 |
. . . . . 6
โข
(topGenโran (,)) = ((TopOpenโโfld)
โพt โ) |
182 | | iooretop 24145 |
. . . . . . 7
โข (๐ด(,)๐ต) โ (topGenโran
(,)) |
183 | 182 | a1i 11 |
. . . . . 6
โข (๐ โ (๐ด(,)๐ต) โ (topGenโran
(,))) |
184 | 2, 175, 176, 177, 179, 181, 180, 183 | dvmptres 25343 |
. . . . 5
โข (๐ โ (โ D (๐ฅ โ (๐ด(,)๐ต) โฆ 1)) = (๐ฅ โ (๐ด(,)๐ต) โฆ 0)) |
185 | 2, 84, 111, 173, 85, 10, 184 | dvmptadd 25340 |
. . . 4
โข (๐ โ (โ D (๐ฅ โ (๐ด(,)๐ต) โฆ (((2 logb ๐ฅ)โ5) + 1))) = (๐ฅ โ (๐ด(,)๐ต) โฆ (((5 ยท ((2 logb
๐ฅ)โ4)) ยท (1 /
(๐ฅ ยท
(logโ2)))) + 0))) |
186 | | dfrp2 13320 |
. . . . . . . 8
โข
โ+ = (0(,)+โ) |
187 | 186 | a1i 11 |
. . . . . . 7
โข (๐ โ โ+ =
(0(,)+โ)) |
188 | 187 | mpteq1d 5205 |
. . . . . 6
โข (๐ โ (๐ฆ โ โ+ โฆ (2
logb ๐ฆ)) =
(๐ฆ โ (0(,)+โ)
โฆ (2 logb ๐ฆ))) |
189 | 188 | oveq2d 7378 |
. . . . 5
โข (๐ โ (โ D (๐ฆ โ โ+
โฆ (2 logb ๐ฆ))) = (โ D (๐ฆ โ (0(,)+โ) โฆ (2
logb ๐ฆ)))) |
190 | 90 | rexrd 11212 |
. . . . . . 7
โข (๐ โ 0 โ
โ*) |
191 | | pnfxr 11216 |
. . . . . . . 8
โข +โ
โ โ* |
192 | 191 | a1i 11 |
. . . . . . 7
โข (๐ โ +โ โ
โ*) |
193 | 90 | leidd 11728 |
. . . . . . 7
โข (๐ โ 0 โค 0) |
194 | | 0lepnf 13060 |
. . . . . . . 8
โข 0 โค
+โ |
195 | 194 | a1i 11 |
. . . . . . 7
โข (๐ โ 0 โค
+โ) |
196 | | eqid 2737 |
. . . . . . 7
โข (๐ฆ โ (0(,)+โ) โฆ
(2 logb ๐ฆ)) =
(๐ฆ โ (0(,)+โ)
โฆ (2 logb ๐ฆ)) |
197 | | eqid 2737 |
. . . . . . 7
โข (๐ฆ โ (0(,)+โ) โฆ
(1 / (๐ฆ ยท
(logโ2)))) = (๐ฆ
โ (0(,)+โ) โฆ (1 / (๐ฆ ยท (logโ2)))) |
198 | 190, 192,
193, 195, 196, 197 | dvrelog2b 40552 |
. . . . . 6
โข (๐ โ (โ D (๐ฆ โ (0(,)+โ) โฆ
(2 logb ๐ฆ))) =
(๐ฆ โ (0(,)+โ)
โฆ (1 / (๐ฆ ยท
(logโ2))))) |
199 | 187 | eqcomd 2743 |
. . . . . . 7
โข (๐ โ (0(,)+โ) =
โ+) |
200 | 199 | mpteq1d 5205 |
. . . . . 6
โข (๐ โ (๐ฆ โ (0(,)+โ) โฆ (1 / (๐ฆ ยท (logโ2)))) =
(๐ฆ โ
โ+ โฆ (1 / (๐ฆ ยท (logโ2))))) |
201 | 198, 200 | eqtrd 2777 |
. . . . 5
โข (๐ โ (โ D (๐ฆ โ (0(,)+โ) โฆ
(2 logb ๐ฆ))) =
(๐ฆ โ
โ+ โฆ (1 / (๐ฆ ยท (logโ2))))) |
202 | 189, 201 | eqtrd 2777 |
. . . 4
โข (๐ โ (โ D (๐ฆ โ โ+
โฆ (2 logb ๐ฆ))) = (๐ฆ โ โ+ โฆ (1 /
(๐ฆ ยท
(logโ2))))) |
203 | | oveq2 7370 |
. . . 4
โข (๐ฆ = (((2 logb ๐ฅ)โ5) + 1) โ (2
logb ๐ฆ) = (2
logb (((2 logb ๐ฅ)โ5) + 1))) |
204 | | oveq1 7369 |
. . . . 5
โข (๐ฆ = (((2 logb ๐ฅ)โ5) + 1) โ (๐ฆ ยท (logโ2)) = ((((2
logb ๐ฅ)โ5)
+ 1) ยท (logโ2))) |
205 | 204 | oveq2d 7378 |
. . . 4
โข (๐ฆ = (((2 logb ๐ฅ)โ5) + 1) โ (1 /
(๐ฆ ยท (logโ2)))
= (1 / ((((2 logb ๐ฅ)โ5) + 1) ยท
(logโ2)))) |
206 | 2, 2, 115, 112, 127, 141, 185, 202, 203, 205 | dvmptco 25352 |
. . 3
โข (๐ โ (โ D (๐ฅ โ (๐ด(,)๐ต) โฆ (2 logb (((2
logb ๐ฅ)โ5)
+ 1)))) = (๐ฅ โ (๐ด(,)๐ต) โฆ ((1 / ((((2 logb ๐ฅ)โ5) + 1) ยท
(logโ2))) ยท (((5 ยท ((2 logb ๐ฅ)โ4)) ยท (1 / (๐ฅ ยท (logโ2)))) +
0)))) |
207 | 4 | a1i 11 |
. . . 4
โข (๐ โ 2 โ
โ) |
208 | 207 | recnd 11190 |
. . 3
โข (๐ โ 2 โ
โ) |
209 | 2, 78, 113, 206, 208 | dvmptcmul 25344 |
. 2
โข (๐ โ (โ D (๐ฅ โ (๐ด(,)๐ต) โฆ (2 ยท (2 logb
(((2 logb ๐ฅ)โ5) + 1))))) = (๐ฅ โ (๐ด(,)๐ต) โฆ (2 ยท ((1 / ((((2
logb ๐ฅ)โ5)
+ 1) ยท (logโ2))) ยท (((5 ยท ((2 logb ๐ฅ)โ4)) ยท (1 / (๐ฅ ยท (logโ2)))) +
0))))) |
210 | 144 | sqcld 14056 |
. 2
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ ((2 logb ๐ฅ)โ2) โ
โ) |
211 | 82 | resqcld 14037 |
. . . 4
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ ((logโ2)โ2) โ
โ) |
212 | 81 | rpne0d 12969 |
. . . . . 6
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ 2 โ 0) |
213 | 3, 212 | logcld 25942 |
. . . . 5
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ (logโ2) โ
โ) |
214 | 213, 97, 63 | expne0d 14064 |
. . . 4
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ ((logโ2)โ2) โ
0) |
215 | 5, 211, 214 | redivcld 11990 |
. . 3
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ (2 / ((logโ2)โ2))
โ โ) |
216 | 67 | relogcld 25994 |
. . . . 5
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ (logโ๐ฅ) โ โ) |
217 | | 2m1e1 12286 |
. . . . . . 7
โข (2
โ 1) = 1 |
218 | | 1nn0 12436 |
. . . . . . 7
โข 1 โ
โ0 |
219 | 217, 218 | eqeltri 2834 |
. . . . . 6
โข (2
โ 1) โ โ0 |
220 | 219 | a1i 11 |
. . . . 5
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ (2 โ 1) โ
โ0) |
221 | 216, 220 | reexpcld 14075 |
. . . 4
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ ((logโ๐ฅ)โ(2 โ 1)) โ
โ) |
222 | 67 | rpne0d 12969 |
. . . 4
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ ๐ฅ โ 0) |
223 | 221, 9, 222 | redivcld 11990 |
. . 3
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ (((logโ๐ฅ)โ(2 โ 1)) / ๐ฅ) โ โ) |
224 | 215, 223 | remulcld 11192 |
. 2
โข ((๐ โง ๐ฅ โ (๐ด(,)๐ต)) โ ((2 / ((logโ2)โ2))
ยท (((logโ๐ฅ)โ(2 โ 1)) / ๐ฅ)) โ โ) |
225 | | eqid 2737 |
. . 3
โข (๐ฅ โ (๐ด(,)๐ต) โฆ ((2 logb ๐ฅ)โ2)) = (๐ฅ โ (๐ด(,)๐ต) โฆ ((2 logb ๐ฅ)โ2)) |
226 | | eqid 2737 |
. . 3
โข (๐ฅ โ (๐ด(,)๐ต) โฆ ((2 / ((logโ2)โ2))
ยท (((logโ๐ฅ)โ(2 โ 1)) / ๐ฅ))) = (๐ฅ โ (๐ด(,)๐ต) โฆ ((2 / ((logโ2)โ2))
ยท (((logโ๐ฅ)โ(2 โ 1)) / ๐ฅ))) |
227 | | eqid 2737 |
. . 3
โข (2 /
((logโ2)โ2)) = (2 / ((logโ2)โ2)) |
228 | | 2nn 12233 |
. . . 4
โข 2 โ
โ |
229 | 228 | a1i 11 |
. . 3
โข (๐ โ 2 โ
โ) |
230 | 11, 23, 155, 157, 225, 226, 227, 229 | dvrelogpow2b 40554 |
. 2
โข (๐ โ (โ D (๐ฅ โ (๐ด(,)๐ต) โฆ ((2 logb ๐ฅ)โ2))) = (๐ฅ โ (๐ด(,)๐ต) โฆ ((2 / ((logโ2)โ2))
ยท (((logโ๐ฅ)โ(2 โ 1)) / ๐ฅ)))) |
231 | 2, 79, 114, 209, 210, 224, 230 | dvmptadd 25340 |
1
โข (๐ โ (โ D (๐ฅ โ (๐ด(,)๐ต) โฆ ((2 ยท (2 logb
(((2 logb ๐ฅ)โ5) + 1))) + ((2 logb ๐ฅ)โ2)))) = (๐ฅ โ (๐ด(,)๐ต) โฆ ((2 ยท ((1 / ((((2
logb ๐ฅ)โ5)
+ 1) ยท (logโ2))) ยท (((5 ยท ((2 logb ๐ฅ)โ4)) ยท (1 / (๐ฅ ยท (logโ2)))) +
0))) + ((2 / ((logโ2)โ2)) ยท (((logโ๐ฅ)โ(2 โ 1)) / ๐ฅ))))) |