ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-phi Unicode version

Definition df-phi 10967
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.)
Assertion
Ref Expression
df-phi  |-  phi  =  ( n  e.  NN  |->  ( `  { x  e.  ( 1 ... n
)  |  ( x  gcd  n )  =  1 } ) )
Distinct variable group:    x, n

Detailed syntax breakdown of Definition df-phi
StepHypRef Expression
1 cphi 10966 . 2  class  phi
2 vn . . 3  setvar  n
3 cn 8316 . . 3  class  NN
4 vx . . . . . . . 8  setvar  x
54cv 1284 . . . . . . 7  class  x
62cv 1284 . . . . . . 7  class  n
7 cgcd 10718 . . . . . . 7  class  gcd
85, 6, 7co 5591 . . . . . 6  class  ( x  gcd  n )
9 c1 7254 . . . . . 6  class  1
108, 9wceq 1285 . . . . 5  wff  ( x  gcd  n )  =  1
11 cfz 9319 . . . . . 6  class  ...
129, 6, 11co 5591 . . . . 5  class  ( 1 ... n )
1310, 4, 12crab 2357 . . . 4  class  { x  e.  ( 1 ... n
)  |  ( x  gcd  n )  =  1 }
14 chash 10018 . . . 4  class
1513, 14cfv 4969 . . 3  class  ( `  {
x  e.  ( 1 ... n )  |  ( x  gcd  n
)  =  1 } )
162, 3, 15cmpt 3865 . 2  class  ( n  e.  NN  |->  ( `  {
x  e.  ( 1 ... n )  |  ( x  gcd  n
)  =  1 } ) )
171, 16wceq 1285 1  wff  phi  =  ( n  e.  NN  |->  ( `  { x  e.  ( 1 ... n
)  |  ( x  gcd  n )  =  1 } ) )
Colors of variables: wff set class
This definition is referenced by:  phival  10969
  Copyright terms: Public domain W3C validator