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

Metamath Proof Explorer

Theorem sgmmul

Description: The divisor function for fixed parameter A is a multiplicative function. (Contributed by Mario Carneiro, 2-Jul-2015)

Ref Expression
Assertion sgmmul ( ( 𝐴 ∈ ℂ ∧ ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ ( 𝑀 gcd 𝑁 ) = 1 ) ) → ( 𝐴 σ ( 𝑀 · 𝑁 ) ) = ( ( 𝐴 σ 𝑀 ) · ( 𝐴 σ 𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 simpr1 ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ ( 𝑀 gcd 𝑁 ) = 1 ) ) → 𝑀 ∈ ℕ )
2 simpr2 ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ ( 𝑀 gcd 𝑁 ) = 1 ) ) → 𝑁 ∈ ℕ )
3 simpr3 ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ ( 𝑀 gcd 𝑁 ) = 1 ) ) → ( 𝑀 gcd 𝑁 ) = 1 )
4 eqid ⊢ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑀 } = { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑀 }
5 eqid ⊢ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } = { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 }
6 eqid ⊢ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑀 · 𝑁 ) } = { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑀 · 𝑁 ) }
7 ssrab2 ⊢ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑀 } ⊆ ℕ
8 simpr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ ( 𝑀 gcd 𝑁 ) = 1 ) ) ∧ 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑀 } ) → 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑀 } )
9 7 8 sselid ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ ( 𝑀 gcd 𝑁 ) = 1 ) ) ∧ 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑀 } ) → 𝑗 ∈ ℕ )
10 9 nncnd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ ( 𝑀 gcd 𝑁 ) = 1 ) ) ∧ 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑀 } ) → 𝑗 ∈ ℂ )
11 simpll ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ ( 𝑀 gcd 𝑁 ) = 1 ) ) ∧ 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑀 } ) → 𝐴 ∈ ℂ )
12 10 11 cxpcld ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ ( 𝑀 gcd 𝑁 ) = 1 ) ) ∧ 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑀 } ) → ( 𝑗 ↑𝑐 𝐴 ) ∈ ℂ )
13 ssrab2 ⊢ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ⊆ ℕ
14 simpr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ ( 𝑀 gcd 𝑁 ) = 1 ) ) ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } )
15 13 14 sselid ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ ( 𝑀 gcd 𝑁 ) = 1 ) ) ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → 𝑘 ∈ ℕ )
16 15 nncnd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ ( 𝑀 gcd 𝑁 ) = 1 ) ) ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → 𝑘 ∈ ℂ )
17 simpll ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ ( 𝑀 gcd 𝑁 ) = 1 ) ) ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → 𝐴 ∈ ℂ )
18 16 17 cxpcld ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ ( 𝑀 gcd 𝑁 ) = 1 ) ) ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → ( 𝑘 ↑𝑐 𝐴 ) ∈ ℂ )
19 9 adantrr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ ( 𝑀 gcd 𝑁 ) = 1 ) ) ∧ ( 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑀 } ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) ) → 𝑗 ∈ ℕ )
20 19 nnred ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ ( 𝑀 gcd 𝑁 ) = 1 ) ) ∧ ( 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑀 } ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) ) → 𝑗 ∈ ℝ )
21 19 nnnn0d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ ( 𝑀 gcd 𝑁 ) = 1 ) ) ∧ ( 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑀 } ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) ) → 𝑗 ∈ ℕ0 )
22 21 nn0ge0d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ ( 𝑀 gcd 𝑁 ) = 1 ) ) ∧ ( 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑀 } ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) ) → 0 ≤ 𝑗 )
23 15 adantrl ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ ( 𝑀 gcd 𝑁 ) = 1 ) ) ∧ ( 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑀 } ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) ) → 𝑘 ∈ ℕ )
24 23 nnred ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ ( 𝑀 gcd 𝑁 ) = 1 ) ) ∧ ( 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑀 } ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) ) → 𝑘 ∈ ℝ )
25 23 nnnn0d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ ( 𝑀 gcd 𝑁 ) = 1 ) ) ∧ ( 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑀 } ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) ) → 𝑘 ∈ ℕ0 )
26 25 nn0ge0d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ ( 𝑀 gcd 𝑁 ) = 1 ) ) ∧ ( 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑀 } ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) ) → 0 ≤ 𝑘 )
27 simpll ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ ( 𝑀 gcd 𝑁 ) = 1 ) ) ∧ ( 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑀 } ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) ) → 𝐴 ∈ ℂ )
28 20 22 24 26 27 mulcxpd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ ( 𝑀 gcd 𝑁 ) = 1 ) ) ∧ ( 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑀 } ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) ) → ( ( 𝑗 · 𝑘 ) ↑𝑐 𝐴 ) = ( ( 𝑗 ↑𝑐 𝐴 ) · ( 𝑘 ↑𝑐 𝐴 ) ) )
29 28 eqcomd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ ( 𝑀 gcd 𝑁 ) = 1 ) ) ∧ ( 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑀 } ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) ) → ( ( 𝑗 ↑𝑐 𝐴 ) · ( 𝑘 ↑𝑐 𝐴 ) ) = ( ( 𝑗 · 𝑘 ) ↑𝑐 𝐴 ) )
30 oveq1 ⊢ ( 𝑖 = ( 𝑗 · 𝑘 ) → ( 𝑖 ↑𝑐 𝐴 ) = ( ( 𝑗 · 𝑘 ) ↑𝑐 𝐴 ) )
31 1 2 3 4 5 6 12 18 29 30 fsumdvdsmul ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ ( 𝑀 gcd 𝑁 ) = 1 ) ) → ( Σ 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑀 } ( 𝑗 ↑𝑐 𝐴 ) · Σ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ( 𝑘 ↑𝑐 𝐴 ) ) = Σ 𝑖 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑀 · 𝑁 ) } ( 𝑖 ↑𝑐 𝐴 ) )
32 sgmval ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ ) → ( 𝐴 σ 𝑀 ) = Σ 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑀 } ( 𝑗 ↑𝑐 𝐴 ) )
33 1 32 syldan ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ ( 𝑀 gcd 𝑁 ) = 1 ) ) → ( 𝐴 σ 𝑀 ) = Σ 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑀 } ( 𝑗 ↑𝑐 𝐴 ) )
34 sgmval ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ) → ( 𝐴 σ 𝑁 ) = Σ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ( 𝑘 ↑𝑐 𝐴 ) )
35 2 34 syldan ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ ( 𝑀 gcd 𝑁 ) = 1 ) ) → ( 𝐴 σ 𝑁 ) = Σ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ( 𝑘 ↑𝑐 𝐴 ) )
36 33 35 oveq12d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ ( 𝑀 gcd 𝑁 ) = 1 ) ) → ( ( 𝐴 σ 𝑀 ) · ( 𝐴 σ 𝑁 ) ) = ( Σ 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑀 } ( 𝑗 ↑𝑐 𝐴 ) · Σ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ( 𝑘 ↑𝑐 𝐴 ) ) )
37 1 2 nnmulcld ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ ( 𝑀 gcd 𝑁 ) = 1 ) ) → ( 𝑀 · 𝑁 ) ∈ ℕ )
38 sgmval ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑀 · 𝑁 ) ∈ ℕ ) → ( 𝐴 σ ( 𝑀 · 𝑁 ) ) = Σ 𝑖 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑀 · 𝑁 ) } ( 𝑖 ↑𝑐 𝐴 ) )
39 37 38 syldan ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ ( 𝑀 gcd 𝑁 ) = 1 ) ) → ( 𝐴 σ ( 𝑀 · 𝑁 ) ) = Σ 𝑖 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑀 · 𝑁 ) } ( 𝑖 ↑𝑐 𝐴 ) )
40 31 36 39 3eqtr4rd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ ( 𝑀 gcd 𝑁 ) = 1 ) ) → ( 𝐴 σ ( 𝑀 · 𝑁 ) ) = ( ( 𝐴 σ 𝑀 ) · ( 𝐴 σ 𝑁 ) ) )