Detailed syntax breakdown of Definition df-lgam
| Step | Hyp | Ref
| Expression |
| 1 | | clgam 27059 |
. 2
class log
Γ |
| 2 | | vz |
. . 3
setvar 𝑧 |
| 3 | | cc 11153 |
. . . 4
class
ℂ |
| 4 | | cz 12613 |
. . . . 5
class
ℤ |
| 5 | | cn 12266 |
. . . . 5
class
ℕ |
| 6 | 4, 5 | cdif 3948 |
. . . 4
class (ℤ
∖ ℕ) |
| 7 | 3, 6 | cdif 3948 |
. . 3
class (ℂ
∖ (ℤ ∖ ℕ)) |
| 8 | 2 | cv 1539 |
. . . . . . 7
class 𝑧 |
| 9 | | vm |
. . . . . . . . . . 11
setvar 𝑚 |
| 10 | 9 | cv 1539 |
. . . . . . . . . 10
class 𝑚 |
| 11 | | c1 11156 |
. . . . . . . . . 10
class
1 |
| 12 | | caddc 11158 |
. . . . . . . . . 10
class
+ |
| 13 | 10, 11, 12 | co 7431 |
. . . . . . . . 9
class (𝑚 + 1) |
| 14 | | cdiv 11920 |
. . . . . . . . 9
class
/ |
| 15 | 13, 10, 14 | co 7431 |
. . . . . . . 8
class ((𝑚 + 1) / 𝑚) |
| 16 | | clog 26596 |
. . . . . . . 8
class
log |
| 17 | 15, 16 | cfv 6561 |
. . . . . . 7
class
(log‘((𝑚 + 1)
/ 𝑚)) |
| 18 | | cmul 11160 |
. . . . . . 7
class
· |
| 19 | 8, 17, 18 | co 7431 |
. . . . . 6
class (𝑧 · (log‘((𝑚 + 1) / 𝑚))) |
| 20 | 8, 10, 14 | co 7431 |
. . . . . . . 8
class (𝑧 / 𝑚) |
| 21 | 20, 11, 12 | co 7431 |
. . . . . . 7
class ((𝑧 / 𝑚) + 1) |
| 22 | 21, 16 | cfv 6561 |
. . . . . 6
class
(log‘((𝑧 /
𝑚) + 1)) |
| 23 | | cmin 11492 |
. . . . . 6
class
− |
| 24 | 19, 22, 23 | co 7431 |
. . . . 5
class ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1))) |
| 25 | 5, 24, 9 | csu 15722 |
. . . 4
class
Σ𝑚 ∈
ℕ ((𝑧 ·
(log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1))) |
| 26 | 8, 16 | cfv 6561 |
. . . 4
class
(log‘𝑧) |
| 27 | 25, 26, 23 | co 7431 |
. . 3
class
(Σ𝑚 ∈
ℕ ((𝑧 ·
(log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1))) − (log‘𝑧)) |
| 28 | 2, 7, 27 | cmpt 5225 |
. 2
class (𝑧 ∈ (ℂ ∖
(ℤ ∖ ℕ)) ↦ (Σ𝑚 ∈ ℕ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1))) − (log‘𝑧))) |
| 29 | 1, 28 | wceq 1540 |
1
wff log Γ
= (𝑧 ∈ (ℂ
∖ (ℤ ∖ ℕ)) ↦ (Σ𝑚 ∈ ℕ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1))) − (log‘𝑧))) |