Theorem phimul

Description: The Euler phi function is a multiplicative function, meaning that it distributes over multiplication at relatively prime arguments. Theorem 2.5(c) in ApostolNT p. 28. (Contributed by Mario Carneiro, 24-Feb-2014)

	Ref	Expression
Assertion	phimul	|- ( ( M e. NN /\ N e. NN /\ ( M gcd N ) = 1 ) -> ( phi ` ( M x. N ) ) = ( ( phi ` M ) x. ( phi ` N ) ) )

Proof

Step	Hyp	Ref	Expression
1		eqid	|- ( 0 ..^ ( M x. N ) ) = ( 0 ..^ ( M x. N ) )
2		eqid	|- ( ( 0 ..^ M ) X. ( 0 ..^ N ) ) = ( ( 0 ..^ M ) X. ( 0 ..^ N ) )
3		eqid	|- ( x e. ( 0 ..^ ( M x. N ) ) |-> <. ( x mod M ) , ( x mod N ) >. ) = ( x e. ( 0 ..^ ( M x. N ) ) |-> <. ( x mod M ) , ( x mod N ) >. )
4		id	|- ( ( M e. NN /\ N e. NN /\ ( M gcd N ) = 1 ) -> ( M e. NN /\ N e. NN /\ ( M gcd N ) = 1 ) )
5		eqid	|- { y e. ( 0 ..^ M ) | ( y gcd M ) = 1 } = { y e. ( 0 ..^ M ) | ( y gcd M ) = 1 }
6		eqid	|- { y e. ( 0 ..^ N ) | ( y gcd N ) = 1 } = { y e. ( 0 ..^ N ) | ( y gcd N ) = 1 }
7		eqid	|- { y e. ( 0 ..^ ( M x. N ) ) | ( y gcd ( M x. N ) ) = 1 } = { y e. ( 0 ..^ ( M x. N ) ) | ( y gcd ( M x. N ) ) = 1 }
8	1 2 3 4 5 6 7	phimullem	|- ( ( M e. NN /\ N e. NN /\ ( M gcd N ) = 1 ) -> ( phi ` ( M x. N ) ) = ( ( phi ` M ) x. ( phi ` N ) ) )