Step | Hyp | Ref
| Expression |
1 | | clgam 26520 |
. 2
class log
ฮ |
2 | | vz |
. . 3
setvar ๐ง |
3 | | cc 11108 |
. . . 4
class
โ |
4 | | cz 12558 |
. . . . 5
class
โค |
5 | | cn 12212 |
. . . . 5
class
โ |
6 | 4, 5 | cdif 3946 |
. . . 4
class (โค
โ โ) |
7 | 3, 6 | cdif 3946 |
. . 3
class (โ
โ (โค โ โ)) |
8 | 2 | cv 1541 |
. . . . . . 7
class ๐ง |
9 | | vm |
. . . . . . . . . . 11
setvar ๐ |
10 | 9 | cv 1541 |
. . . . . . . . . 10
class ๐ |
11 | | c1 11111 |
. . . . . . . . . 10
class
1 |
12 | | caddc 11113 |
. . . . . . . . . 10
class
+ |
13 | 10, 11, 12 | co 7409 |
. . . . . . . . 9
class (๐ + 1) |
14 | | cdiv 11871 |
. . . . . . . . 9
class
/ |
15 | 13, 10, 14 | co 7409 |
. . . . . . . 8
class ((๐ + 1) / ๐) |
16 | | clog 26063 |
. . . . . . . 8
class
log |
17 | 15, 16 | cfv 6544 |
. . . . . . 7
class
(logโ((๐ + 1)
/ ๐)) |
18 | | cmul 11115 |
. . . . . . 7
class
ยท |
19 | 8, 17, 18 | co 7409 |
. . . . . 6
class (๐ง ยท (logโ((๐ + 1) / ๐))) |
20 | 8, 10, 14 | co 7409 |
. . . . . . . 8
class (๐ง / ๐) |
21 | 20, 11, 12 | co 7409 |
. . . . . . 7
class ((๐ง / ๐) + 1) |
22 | 21, 16 | cfv 6544 |
. . . . . 6
class
(logโ((๐ง /
๐) + 1)) |
23 | | cmin 11444 |
. . . . . 6
class
โ |
24 | 19, 22, 23 | co 7409 |
. . . . 5
class ((๐ง ยท (logโ((๐ + 1) / ๐))) โ (logโ((๐ง / ๐) + 1))) |
25 | 5, 24, 9 | csu 15632 |
. . . 4
class
ฮฃ๐ โ
โ ((๐ง ยท
(logโ((๐ + 1) / ๐))) โ (logโ((๐ง / ๐) + 1))) |
26 | 8, 16 | cfv 6544 |
. . . 4
class
(logโ๐ง) |
27 | 25, 26, 23 | co 7409 |
. . 3
class
(ฮฃ๐ โ
โ ((๐ง ยท
(logโ((๐ + 1) / ๐))) โ (logโ((๐ง / ๐) + 1))) โ (logโ๐ง)) |
28 | 2, 7, 27 | cmpt 5232 |
. 2
class (๐ง โ (โ โ
(โค โ โ)) โฆ (ฮฃ๐ โ โ ((๐ง ยท (logโ((๐ + 1) / ๐))) โ (logโ((๐ง / ๐) + 1))) โ (logโ๐ง))) |
29 | 1, 28 | wceq 1542 |
1
wff log ฮ
= (๐ง โ (โ
โ (โค โ โ)) โฆ (ฮฃ๐ โ โ ((๐ง ยท (logโ((๐ + 1) / ๐))) โ (logโ((๐ง / ๐) + 1))) โ (logโ๐ง))) |