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‘𝑧))) |