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 } ) )