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

Definition df-phi 14296
Description: Define the Euler phi function, which counts the number of integers less than and coprime to it. (Contributed by Mario Carneiro, 23-Feb-2014.)
Assertion
Ref Expression
df-phi
Distinct variable group:   ,

Detailed syntax breakdown of Definition df-phi
StepHypRef Expression
1 cphi 14294 . 2
2 vn . . 3
3 cn 10561 . . 3
4 vx . . . . . . . 8
54cv 1394 . . . . . . 7
62cv 1394 . . . . . . 7
7 cgcd 14144 . . . . . . 7
85, 6, 7co 6296 . . . . . 6
9 c1 9514 . . . . . 6
108, 9wceq 1395 . . . . 5
11 cfz 11701 . . . . . 6
129, 6, 11co 6296 . . . . 5
1310, 4, 12crab 2811 . . . 4
14 chash 12405 . . . 4
1513, 14cfv 5593 . . 3
162, 3, 15cmpt 4510 . 2
171, 16wceq 1395 1
Colors of variables: wff setvar class
This definition is referenced by:  phival  14297
  Copyright terms: Public domain W3C validator