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 ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ ( 𝑀 gcd 𝑁 ) = 1 ) → ( ϕ ‘ ( 𝑀 · 𝑁 ) ) = ( ( ϕ ‘ 𝑀 ) · ( ϕ ‘ 𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 eqid ⊢ ( 0 ..^ ( 𝑀 · 𝑁 ) ) = ( 0 ..^ ( 𝑀 · 𝑁 ) )
2 eqid ⊢ ( ( 0 ..^ 𝑀 ) × ( 0 ..^ 𝑁 ) ) = ( ( 0 ..^ 𝑀 ) × ( 0 ..^ 𝑁 ) )
3 eqid ⊢ ( 𝑥 ∈ ( 0 ..^ ( 𝑀 · 𝑁 ) ) ↦ ⟨ ( 𝑥 mod 𝑀 ) , ( 𝑥 mod 𝑁 ) ⟩ ) = ( 𝑥 ∈ ( 0 ..^ ( 𝑀 · 𝑁 ) ) ↦ ⟨ ( 𝑥 mod 𝑀 ) , ( 𝑥 mod 𝑁 ) ⟩ )
4 id ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ ( 𝑀 gcd 𝑁 ) = 1 ) → ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ ( 𝑀 gcd 𝑁 ) = 1 ) )
5 eqid ⊢ { 𝑦 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑦 gcd 𝑀 ) = 1 } = { 𝑦 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑦 gcd 𝑀 ) = 1 }
6 eqid ⊢ { 𝑦 ∈ ( 0 ..^ 𝑁 ) ∣ ( 𝑦 gcd 𝑁 ) = 1 } = { 𝑦 ∈ ( 0 ..^ 𝑁 ) ∣ ( 𝑦 gcd 𝑁 ) = 1 }
7 eqid ⊢ { 𝑦 ∈ ( 0 ..^ ( 𝑀 · 𝑁 ) ) ∣ ( 𝑦 gcd ( 𝑀 · 𝑁 ) ) = 1 } = { 𝑦 ∈ ( 0 ..^ ( 𝑀 · 𝑁 ) ) ∣ ( 𝑦 gcd ( 𝑀 · 𝑁 ) ) = 1 }
8 1 2 3 4 5 6 7 phimullem ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ ( 𝑀 gcd 𝑁 ) = 1 ) → ( ϕ ‘ ( 𝑀 · 𝑁 ) ) = ( ( ϕ ‘ 𝑀 ) · ( ϕ ‘ 𝑁 ) ) )