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

Metamath Proof Explorer

Theorem phival

Description: Value of the Euler phi function. (Contributed by Mario Carneiro, 23-Feb-2014)

Ref Expression
Assertion phival 
|- ( N e. NN -> ( phi ` N ) = ( # ` { x e. ( 1 ... N ) | ( x gcd N ) = 1 } ) )

Proof

Step Hyp Ref Expression
1 oveq2 
 |-  ( n = N -> ( 1 ... n ) = ( 1 ... N ) )
2 oveq2 
 |-  ( n = N -> ( x gcd n ) = ( x gcd N ) )
3 2 eqeq1d 
 |-  ( n = N -> ( ( x gcd n ) = 1 <-> ( x gcd N ) = 1 ) )
4 1 3 rabeqbidv 
 |-  ( n = N -> { x e. ( 1 ... n ) | ( x gcd n ) = 1 } = { x e. ( 1 ... N ) | ( x gcd N ) = 1 } )
5 4 fveq2d 
 |-  ( n = N -> ( # ` { x e. ( 1 ... n ) | ( x gcd n ) = 1 } ) = ( # ` { x e. ( 1 ... N ) | ( x gcd N ) = 1 } ) )
6 df-phi 
 |-  phi = ( n e. NN |-> ( # ` { x e. ( 1 ... n ) | ( x gcd n ) = 1 } ) )
7 fvex 
 |-  ( # ` { x e. ( 1 ... N ) | ( x gcd N ) = 1 } ) e. _V
8 5 6 7 fvmpt 
 |-  ( N e. NN -> ( phi ` N ) = ( # ` { x e. ( 1 ... N ) | ( x gcd N ) = 1 } ) )