Definition df-phi 11876

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

Step	Hyp	Ref	Expression
1		cphi 11875	. 2 class ϕ
2		vn	. . 3 setvar 𝑛
3		cn 8713	. . 3 class ℕ
4		vx	. . . . . . . 8 setvar 𝑥
5	4	cv 1330	. . . . . . 7 class 𝑥
6	2	cv 1330	. . . . . . 7 class 𝑛
7		cgcd 11624	. . . . . . 7 class gcd
8	5, 6, 7	co 5767	. . . . . 6 class (𝑥 gcd 𝑛)
9		c1 7614	. . . . . 6 class 1
10	8, 9	wceq 1331	. . . . 5 wff (𝑥 gcd 𝑛) = 1
11		cfz 9783	. . . . . 6 class ...
12	9, 6, 11	co 5767	. . . . 5 class (1...𝑛)
13	10, 4, 12	crab 2418	. . . 4 class {𝑥 ∈ (1...𝑛) ∣ (𝑥 gcd 𝑛) = 1}
14		chash 10514	. . . 4 class ♯
15	13, 14	cfv 5118	. . 3 class (♯‘{𝑥 ∈ (1...𝑛) ∣ (𝑥 gcd 𝑛) = 1})
16	2, 3, 15	cmpt 3984	. 2 class (𝑛 ∈ ℕ ↦ (♯‘{𝑥 ∈ (1...𝑛) ∣ (𝑥 gcd 𝑛) = 1}))
17	1, 16	wceq 1331	1 wff ϕ = (𝑛 ∈ ℕ ↦ (♯‘{𝑥 ∈ (1...𝑛) ∣ (𝑥 gcd 𝑛) = 1}))

This definition is referenced by:  phival  11878