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

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 ∈ ℕ ∧ N ∈ ℕ ∧ M gcd N = 1 → ϕ ⁡ M ⋅ N = ϕ ⁡ M ⁢ ϕ ⁡ N

Proof

Step Hyp Ref Expression
1 eqid ⊢ 0 ..^ M ⋅ N = 0 ..^ M ⋅ N
2 eqid ⊢ 0 ..^ M × 0 ..^ N = 0 ..^ M × 0 ..^ N
3 eqid ⊢ x ∈ 0 ..^ M ⋅ N ⟼ x mod M x mod N = x ∈ 0 ..^ M ⋅ N ⟼ x mod M x mod N
4 id ⊢ M ∈ ℕ ∧ N ∈ ℕ ∧ M gcd N = 1 → M ∈ ℕ ∧ N ∈ ℕ ∧ M gcd N = 1
5 eqid ⊢ y ∈ 0 ..^ M | y gcd M = 1 = y ∈ 0 ..^ M | y gcd M = 1
6 eqid ⊢ y ∈ 0 ..^ N | y gcd N = 1 = y ∈ 0 ..^ N | y gcd N = 1
7 eqid ⊢ y ∈ 0 ..^ M ⋅ N | y gcd M ⋅ N = 1 = y ∈ 0 ..^ M ⋅ N | y gcd M ⋅ N = 1
8 1 2 3 4 5 6 7 phimullem ⊢ M ∈ ℕ ∧ N ∈ ℕ ∧ M gcd N = 1 → ϕ ⁡ M ⋅ N = ϕ ⁡ M ⁢ ϕ ⁡ N