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 ⊢ ϕ = n ∈ ℕ ⟼ x ∈ 1 … n | x gcd n = 1

Detailed syntax breakdown

Step Hyp Ref Expression
0 cphi class ϕ
1 vn setvar n
2 cn class ℕ
3 chash class .
4 vx setvar x
5 c1 class 1
6 cfz class …
7 1 cv setvar n
8 5 7 6 co class 1 … n
9 4 cv setvar x
10 cgcd class gcd
11 9 7 10 co class x gcd n
12 11 5 wceq wff x gcd n = 1
13 12 4 8 crab class x ∈ 1 … n | x gcd n = 1
14 13 3 cfv class x ∈ 1 … n | x gcd n = 1
15 1 2 14 cmpt class n ∈ ℕ ⟼ x ∈ 1 … n | x gcd n = 1
16 0 15 wceq wff ϕ = n ∈ ℕ ⟼ x ∈ 1 … n | x gcd n = 1