Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > df-phi | Structured version Visualization version 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 15307 | . 2 class ϕ | |
2 | vn | . . 3 setvar 𝑛 | |
3 | cn 10897 | . . 3 class ℕ | |
4 | vx | . . . . . . . 8 setvar 𝑥 | |
5 | 4 | cv 1474 | . . . . . . 7 class 𝑥 |
6 | 2 | cv 1474 | . . . . . . 7 class 𝑛 |
7 | cgcd 15054 | . . . . . . 7 class gcd | |
8 | 5, 6, 7 | co 6549 | . . . . . 6 class (𝑥 gcd 𝑛) |
9 | c1 9816 | . . . . . 6 class 1 | |
10 | 8, 9 | wceq 1475 | . . . . 5 wff (𝑥 gcd 𝑛) = 1 |
11 | cfz 12197 | . . . . . 6 class ... | |
12 | 9, 6, 11 | co 6549 | . . . . 5 class (1...𝑛) |
13 | 10, 4, 12 | crab 2900 | . . . 4 class {𝑥 ∈ (1...𝑛) ∣ (𝑥 gcd 𝑛) = 1} |
14 | chash 12979 | . . . 4 class # | |
15 | 13, 14 | cfv 5804 | . . 3 class (#‘{𝑥 ∈ (1...𝑛) ∣ (𝑥 gcd 𝑛) = 1}) |
16 | 2, 3, 15 | cmpt 4643 | . 2 class (𝑛 ∈ ℕ ↦ (#‘{𝑥 ∈ (1...𝑛) ∣ (𝑥 gcd 𝑛) = 1})) |
17 | 1, 16 | wceq 1475 | 1 wff ϕ = (𝑛 ∈ ℕ ↦ (#‘{𝑥 ∈ (1...𝑛) ∣ (𝑥 gcd 𝑛) = 1})) |
Colors of variables: wff setvar class |
This definition is referenced by: phival 15310 |
Copyright terms: Public domain | W3C validator |