Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > df-phi | GIF version |
Description: Define the Euler phi function (also called "Euler totient function"), which counts the number of integers less than 𝑛 and coprime to it, see definition in [ApostolNT] p. 25. (Contributed by Mario Carneiro, 23-Feb-2014.) |
Ref | Expression |
---|---|
df-phi | ⊢ ϕ = (𝑛 ∈ ℕ ↦ (♯‘{𝑥 ∈ (1...𝑛) ∣ (𝑥 gcd 𝑛) = 1})) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cphi 12130 | . 2 class ϕ | |
2 | vn | . . 3 setvar 𝑛 | |
3 | cn 8849 | . . 3 class ℕ | |
4 | vx | . . . . . . . 8 setvar 𝑥 | |
5 | 4 | cv 1341 | . . . . . . 7 class 𝑥 |
6 | 2 | cv 1341 | . . . . . . 7 class 𝑛 |
7 | cgcd 11864 | . . . . . . 7 class gcd | |
8 | 5, 6, 7 | co 5837 | . . . . . 6 class (𝑥 gcd 𝑛) |
9 | c1 7746 | . . . . . 6 class 1 | |
10 | 8, 9 | wceq 1342 | . . . . 5 wff (𝑥 gcd 𝑛) = 1 |
11 | cfz 9936 | . . . . . 6 class ... | |
12 | 9, 6, 11 | co 5837 | . . . . 5 class (1...𝑛) |
13 | 10, 4, 12 | crab 2446 | . . . 4 class {𝑥 ∈ (1...𝑛) ∣ (𝑥 gcd 𝑛) = 1} |
14 | chash 10678 | . . . 4 class ♯ | |
15 | 13, 14 | cfv 5183 | . . 3 class (♯‘{𝑥 ∈ (1...𝑛) ∣ (𝑥 gcd 𝑛) = 1}) |
16 | 2, 3, 15 | cmpt 4038 | . 2 class (𝑛 ∈ ℕ ↦ (♯‘{𝑥 ∈ (1...𝑛) ∣ (𝑥 gcd 𝑛) = 1})) |
17 | 1, 16 | wceq 1342 | 1 wff ϕ = (𝑛 ∈ ℕ ↦ (♯‘{𝑥 ∈ (1...𝑛) ∣ (𝑥 gcd 𝑛) = 1})) |
Colors of variables: wff set class |
This definition is referenced by: phival 12134 |
Copyright terms: Public domain | W3C validator |