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 ) → ( ϕ ‘ ( 𝑀 · 𝑁 ) ) = ( ( ϕ ‘ 𝑀 ) · ( ϕ ‘ 𝑁 ) ) )