Detailed syntax breakdown of Definition df-odz
Step | Hyp | Ref
| Expression |
1 | | codz 12155 |
. 2
class
odℤ |
2 | | vn |
. . 3
setvar 𝑛 |
3 | | cn 8871 |
. . 3
class
ℕ |
4 | | vx |
. . . 4
setvar 𝑥 |
5 | 4 | cv 1347 |
. . . . . . 7
class 𝑥 |
6 | 2 | cv 1347 |
. . . . . . 7
class 𝑛 |
7 | | cgcd 11890 |
. . . . . . 7
class
gcd |
8 | 5, 6, 7 | co 5851 |
. . . . . 6
class (𝑥 gcd 𝑛) |
9 | | c1 7768 |
. . . . . 6
class
1 |
10 | 8, 9 | wceq 1348 |
. . . . 5
wff (𝑥 gcd 𝑛) = 1 |
11 | | cz 9205 |
. . . . 5
class
ℤ |
12 | 10, 4, 11 | crab 2452 |
. . . 4
class {𝑥 ∈ ℤ ∣ (𝑥 gcd 𝑛) = 1} |
13 | | vm |
. . . . . . . . . 10
setvar 𝑚 |
14 | 13 | cv 1347 |
. . . . . . . . 9
class 𝑚 |
15 | | cexp 10468 |
. . . . . . . . 9
class
↑ |
16 | 5, 14, 15 | co 5851 |
. . . . . . . 8
class (𝑥↑𝑚) |
17 | | cmin 8083 |
. . . . . . . 8
class
− |
18 | 16, 9, 17 | co 5851 |
. . . . . . 7
class ((𝑥↑𝑚) − 1) |
19 | | cdvds 11742 |
. . . . . . 7
class
∥ |
20 | 6, 18, 19 | wbr 3987 |
. . . . . 6
wff 𝑛 ∥ ((𝑥↑𝑚) − 1) |
21 | 20, 13, 3 | crab 2452 |
. . . . 5
class {𝑚 ∈ ℕ ∣ 𝑛 ∥ ((𝑥↑𝑚) − 1)} |
22 | | cr 7766 |
. . . . 5
class
ℝ |
23 | | clt 7947 |
. . . . 5
class
< |
24 | 21, 22, 23 | cinf 6958 |
. . . 4
class
inf({𝑚 ∈
ℕ ∣ 𝑛 ∥
((𝑥↑𝑚) − 1)}, ℝ, <
) |
25 | 4, 12, 24 | cmpt 4048 |
. . 3
class (𝑥 ∈ {𝑥 ∈ ℤ ∣ (𝑥 gcd 𝑛) = 1} ↦ inf({𝑚 ∈ ℕ ∣ 𝑛 ∥ ((𝑥↑𝑚) − 1)}, ℝ, <
)) |
26 | 2, 3, 25 | cmpt 4048 |
. 2
class (𝑛 ∈ ℕ ↦ (𝑥 ∈ {𝑥 ∈ ℤ ∣ (𝑥 gcd 𝑛) = 1} ↦ inf({𝑚 ∈ ℕ ∣ 𝑛 ∥ ((𝑥↑𝑚) − 1)}, ℝ, <
))) |
27 | 1, 26 | wceq 1348 |
1
wff
odℤ = (𝑛 ∈ ℕ ↦ (𝑥 ∈ {𝑥 ∈ ℤ ∣ (𝑥 gcd 𝑛) = 1} ↦ inf({𝑚 ∈ ℕ ∣ 𝑛 ∥ ((𝑥↑𝑚) − 1)}, ℝ, <
))) |