Step | Hyp | Ref
| Expression |
1 | | clcmf 16472 |
. 2
class
lcm |
2 | | vz |
. . 3
setvar 𝑧 |
3 | | cz 12506 |
. . . 4
class
ℤ |
4 | 3 | cpw 4565 |
. . 3
class 𝒫
ℤ |
5 | | cc0 11058 |
. . . . 5
class
0 |
6 | 2 | cv 1541 |
. . . . 5
class 𝑧 |
7 | 5, 6 | wcel 2107 |
. . . 4
wff 0 ∈
𝑧 |
8 | | vm |
. . . . . . . . 9
setvar 𝑚 |
9 | 8 | cv 1541 |
. . . . . . . 8
class 𝑚 |
10 | | vn |
. . . . . . . . 9
setvar 𝑛 |
11 | 10 | cv 1541 |
. . . . . . . 8
class 𝑛 |
12 | | cdvds 16143 |
. . . . . . . 8
class
∥ |
13 | 9, 11, 12 | wbr 5110 |
. . . . . . 7
wff 𝑚 ∥ 𝑛 |
14 | 13, 8, 6 | wral 3065 |
. . . . . 6
wff
∀𝑚 ∈
𝑧 𝑚 ∥ 𝑛 |
15 | | cn 12160 |
. . . . . 6
class
ℕ |
16 | 14, 10, 15 | crab 3410 |
. . . . 5
class {𝑛 ∈ ℕ ∣
∀𝑚 ∈ 𝑧 𝑚 ∥ 𝑛} |
17 | | cr 11057 |
. . . . 5
class
ℝ |
18 | | clt 11196 |
. . . . 5
class
< |
19 | 16, 17, 18 | cinf 9384 |
. . . 4
class
inf({𝑛 ∈
ℕ ∣ ∀𝑚
∈ 𝑧 𝑚 ∥ 𝑛}, ℝ, < ) |
20 | 7, 5, 19 | cif 4491 |
. . 3
class if(0
∈ 𝑧, 0, inf({𝑛 ∈ ℕ ∣
∀𝑚 ∈ 𝑧 𝑚 ∥ 𝑛}, ℝ, < )) |
21 | 2, 4, 20 | cmpt 5193 |
. 2
class (𝑧 ∈ 𝒫 ℤ
↦ if(0 ∈ 𝑧, 0,
inf({𝑛 ∈ ℕ
∣ ∀𝑚 ∈
𝑧 𝑚 ∥ 𝑛}, ℝ, < ))) |
22 | 1, 21 | wceq 1542 |
1
wff lcm
= (𝑧 ∈ 𝒫
ℤ ↦ if(0 ∈ 𝑧, 0, inf({𝑛 ∈ ℕ ∣ ∀𝑚 ∈ 𝑧 𝑚 ∥ 𝑛}, ℝ, < ))) |