Metamath Proof Explorer

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 \in ℕ \land N \in ℕ \land M \gcd N = 1) \to ϕ (M \cdot N) = ϕ (M) ϕ (N)$

Proof

Step	Hyp	Ref	Expression
1		eqid	$⊢ (0 ..^M \cdot N) = (0 ..^M \cdot N)$
2		eqid	$⊢ (0 ..^M) \times (0 ..^N) = (0 ..^M) \times (0 ..^N)$
3		eqid	$⊢ (x \in (0 ..^M \cdot N) ⟼ ⟨x \mod M, x \mod N⟩) = (x \in (0 ..^M \cdot N) ⟼ ⟨x \mod M, x \mod N⟩)$
4		id	$⊢ (M \in ℕ \land N \in ℕ \land M \gcd N = 1) \to (M \in ℕ \land N \in ℕ \land M \gcd N = 1)$
5		eqid	$⊢ \{y \in (0 ..^M) \| y \gcd M = 1\} = \{y \in (0 ..^M) \| y \gcd M = 1\}$
6		eqid	$⊢ \{y \in (0 ..^N) \| y \gcd N = 1\} = \{y \in (0 ..^N) \| y \gcd N = 1\}$
7		eqid	$⊢ \{y \in (0 ..^M \cdot N) \| y \gcd M \cdot N = 1\} = \{y \in (0 ..^M \cdot N) \| y \gcd M \cdot N = 1\}$
8	1 2 3 4 5 6 7	phimullem	$⊢ (M \in ℕ \land N \in ℕ \land M \gcd N = 1) \to ϕ (M \cdot N) = ϕ (M) ϕ (N)$