MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-phi Structured version   Visualization version   GIF version

Definition df-phi 15695
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.)
Assertion
Ref Expression
df-phi ϕ = (𝑛 ∈ ℕ ↦ (♯‘{𝑥 ∈ (1...𝑛) ∣ (𝑥 gcd 𝑛) = 1}))
Distinct variable group:   𝑥,𝑛

Detailed syntax breakdown of Definition df-phi
StepHypRef Expression
1 cphi 15693 . 2 class ϕ
2 vn . . 3 setvar 𝑛
3 cn 11312 . . 3 class
4 vx . . . . . . . 8 setvar 𝑥
54cv 1636 . . . . . . 7 class 𝑥
62cv 1636 . . . . . . 7 class 𝑛
7 cgcd 15442 . . . . . . 7 class gcd
85, 6, 7co 6881 . . . . . 6 class (𝑥 gcd 𝑛)
9 c1 10229 . . . . . 6 class 1
108, 9wceq 1637 . . . . 5 wff (𝑥 gcd 𝑛) = 1
11 cfz 12556 . . . . . 6 class ...
129, 6, 11co 6881 . . . . 5 class (1...𝑛)
1310, 4, 12crab 3111 . . . 4 class {𝑥 ∈ (1...𝑛) ∣ (𝑥 gcd 𝑛) = 1}
14 chash 13344 . . . 4 class
1513, 14cfv 6108 . . 3 class (♯‘{𝑥 ∈ (1...𝑛) ∣ (𝑥 gcd 𝑛) = 1})
162, 3, 15cmpt 4934 . 2 class (𝑛 ∈ ℕ ↦ (♯‘{𝑥 ∈ (1...𝑛) ∣ (𝑥 gcd 𝑛) = 1}))
171, 16wceq 1637 1 wff ϕ = (𝑛 ∈ ℕ ↦ (♯‘{𝑥 ∈ (1...𝑛) ∣ (𝑥 gcd 𝑛) = 1}))
Colors of variables: wff setvar class
This definition is referenced by:  phival  15696
  Copyright terms: Public domain W3C validator