This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-phi

Description: Define the Euler phi function (also called "Euler totient function"), which counts the number of integers less than n and coprime to it, see definition in ApostolNT p. 25. (Contributed by Mario Carneiro, 23-Feb-2014)

Ref Expression
Assertion df-phi ϕ = ( 𝑛 ∈ ℕ ↦ ( ♯ ‘ { 𝑥 ∈ ( 1 ... 𝑛 ) ∣ ( 𝑥 gcd 𝑛 ) = 1 } ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cphi ⊢ ϕ
1 vn ⊢ 𝑛
2 cn ⊢ ℕ
3 chash ⊢ ♯
4 vx ⊢ 𝑥
5 c1 ⊢ 1
6 cfz ⊢ ...
7 1 cv ⊢ 𝑛
8 5 7 6 co ⊢ ( 1 ... 𝑛 )
9 4 cv ⊢ 𝑥
10 cgcd ⊢ gcd
11 9 7 10 co ⊢ ( 𝑥 gcd 𝑛 )
12 11 5 wceq ⊢ ( 𝑥 gcd 𝑛 ) = 1
13 12 4 8 crab ⊢ { 𝑥 ∈ ( 1 ... 𝑛 ) ∣ ( 𝑥 gcd 𝑛 ) = 1 }
14 13 3 cfv ⊢ ( ♯ ‘ { 𝑥 ∈ ( 1 ... 𝑛 ) ∣ ( 𝑥 gcd 𝑛 ) = 1 } )
15 1 2 14 cmpt ⊢ ( 𝑛 ∈ ℕ ↦ ( ♯ ‘ { 𝑥 ∈ ( 1 ... 𝑛 ) ∣ ( 𝑥 gcd 𝑛 ) = 1 } ) )
16 0 15 wceq ⊢ ϕ = ( 𝑛 ∈ ℕ ↦ ( ♯ ‘ { 𝑥 ∈ ( 1 ... 𝑛 ) ∣ ( 𝑥 gcd 𝑛 ) = 1 } ) )