sgmmul

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

		Ref	Expression
	Assertion	sgmmul	$⊢ (A \in ℂ \land (M \in ℕ \land N \in ℕ \land M \gcd N = 1)) \to A σ M \cdot N = (A σ M) (A σ N)$

Proof

Step	Hyp	Ref	Expression
1		simpr1	$⊢ (A \in ℂ \land (M \in ℕ \land N \in ℕ \land M \gcd N = 1)) \to M \in ℕ$
2		simpr2	$⊢ (A \in ℂ \land (M \in ℕ \land N \in ℕ \land M \gcd N = 1)) \to N \in ℕ$
3		simpr3	$⊢ (A \in ℂ \land (M \in ℕ \land N \in ℕ \land M \gcd N = 1)) \to M \gcd N = 1$
4		eqid	$⊢ \{x \in ℕ \| x ∥ M\} = \{x \in ℕ \| x ∥ M\}$
5		eqid	$⊢ \{x \in ℕ \| x ∥ N\} = \{x \in ℕ \| x ∥ N\}$
6		eqid	$⊢ \{x \in ℕ \| x ∥ M \cdot N\} = \{x \in ℕ \| x ∥ M \cdot N\}$
7		ssrab2	$⊢ \{x \in ℕ \| x ∥ M\} \subseteq ℕ$
8		simpr	$⊢ ((A \in ℂ \land (M \in ℕ \land N \in ℕ \land M \gcd N = 1)) \land j \in \{x \in ℕ \| x ∥ M\}) \to j \in \{x \in ℕ \| x ∥ M\}$
9	7 8	sseldi	$⊢ ((A \in ℂ \land (M \in ℕ \land N \in ℕ \land M \gcd N = 1)) \land j \in \{x \in ℕ \| x ∥ M\}) \to j \in ℕ$
10	9	nncnd	$⊢ ((A \in ℂ \land (M \in ℕ \land N \in ℕ \land M \gcd N = 1)) \land j \in \{x \in ℕ \| x ∥ M\}) \to j \in ℂ$
11		simpll	$⊢ ((A \in ℂ \land (M \in ℕ \land N \in ℕ \land M \gcd N = 1)) \land j \in \{x \in ℕ \| x ∥ M\}) \to A \in ℂ$
12	10 11	cxpcld	$⊢ ((A \in ℂ \land (M \in ℕ \land N \in ℕ \land M \gcd N = 1)) \land j \in \{x \in ℕ \| x ∥ M\}) \to j^{A} \in ℂ$
13		ssrab2	$⊢ \{x \in ℕ \| x ∥ N\} \subseteq ℕ$
14		simpr	$⊢ ((A \in ℂ \land (M \in ℕ \land N \in ℕ \land M \gcd N = 1)) \land k \in \{x \in ℕ \| x ∥ N\}) \to k \in \{x \in ℕ \| x ∥ N\}$
15	13 14	sseldi	$⊢ ((A \in ℂ \land (M \in ℕ \land N \in ℕ \land M \gcd N = 1)) \land k \in \{x \in ℕ \| x ∥ N\}) \to k \in ℕ$
16	15	nncnd	$⊢ ((A \in ℂ \land (M \in ℕ \land N \in ℕ \land M \gcd N = 1)) \land k \in \{x \in ℕ \| x ∥ N\}) \to k \in ℂ$
17		simpll	$⊢ ((A \in ℂ \land (M \in ℕ \land N \in ℕ \land M \gcd N = 1)) \land k \in \{x \in ℕ \| x ∥ N\}) \to A \in ℂ$
18	16 17	cxpcld	$⊢ ((A \in ℂ \land (M \in ℕ \land N \in ℕ \land M \gcd N = 1)) \land k \in \{x \in ℕ \| x ∥ N\}) \to k^{A} \in ℂ$
19	9	adantrr	$⊢ ((A \in ℂ \land (M \in ℕ \land N \in ℕ \land M \gcd N = 1)) \land (j \in \{x \in ℕ \| x ∥ M\} \land k \in \{x \in ℕ \| x ∥ N\})) \to j \in ℕ$
20	19	nnred	$⊢ ((A \in ℂ \land (M \in ℕ \land N \in ℕ \land M \gcd N = 1)) \land (j \in \{x \in ℕ \| x ∥ M\} \land k \in \{x \in ℕ \| x ∥ N\})) \to j \in ℝ$
21	19	nnnn0d	$⊢ ((A \in ℂ \land (M \in ℕ \land N \in ℕ \land M \gcd N = 1)) \land (j \in \{x \in ℕ \| x ∥ M\} \land k \in \{x \in ℕ \| x ∥ N\})) \to j \in ℕ_{0}$
22	21	nn0ge0d	$⊢ ((A \in ℂ \land (M \in ℕ \land N \in ℕ \land M \gcd N = 1)) \land (j \in \{x \in ℕ \| x ∥ M\} \land k \in \{x \in ℕ \| x ∥ N\})) \to 0 \leq j$
23	15	adantrl	$⊢ ((A \in ℂ \land (M \in ℕ \land N \in ℕ \land M \gcd N = 1)) \land (j \in \{x \in ℕ \| x ∥ M\} \land k \in \{x \in ℕ \| x ∥ N\})) \to k \in ℕ$
24	23	nnred	$⊢ ((A \in ℂ \land (M \in ℕ \land N \in ℕ \land M \gcd N = 1)) \land (j \in \{x \in ℕ \| x ∥ M\} \land k \in \{x \in ℕ \| x ∥ N\})) \to k \in ℝ$
25	23	nnnn0d	$⊢ ((A \in ℂ \land (M \in ℕ \land N \in ℕ \land M \gcd N = 1)) \land (j \in \{x \in ℕ \| x ∥ M\} \land k \in \{x \in ℕ \| x ∥ N\})) \to k \in ℕ_{0}$
26	25	nn0ge0d	$⊢ ((A \in ℂ \land (M \in ℕ \land N \in ℕ \land M \gcd N = 1)) \land (j \in \{x \in ℕ \| x ∥ M\} \land k \in \{x \in ℕ \| x ∥ N\})) \to 0 \leq k$
27		simpll	$⊢ ((A \in ℂ \land (M \in ℕ \land N \in ℕ \land M \gcd N = 1)) \land (j \in \{x \in ℕ \| x ∥ M\} \land k \in \{x \in ℕ \| x ∥ N\})) \to A \in ℂ$
28	20 22 24 26 27	mulcxpd	$⊢ ((A \in ℂ \land (M \in ℕ \land N \in ℕ \land M \gcd N = 1)) \land (j \in \{x \in ℕ \| x ∥ M\} \land k \in \{x \in ℕ \| x ∥ N\})) \to {j k}^{A} = j^{A} k^{A}$
29	28	eqcomd	$⊢ ((A \in ℂ \land (M \in ℕ \land N \in ℕ \land M \gcd N = 1)) \land (j \in \{x \in ℕ \| x ∥ M\} \land k \in \{x \in ℕ \| x ∥ N\})) \to j^{A} k^{A} = {j k}^{A}$
30		oveq1	$⊢ i = j k \to i^{A} = {j k}^{A}$
31	1 2 3 4 5 6 12 18 29 30	fsumdvdsmul	$⊢ (A \in ℂ \land (M \in ℕ \land N \in ℕ \land M \gcd N = 1)) \to \sum_{j \in \{x \in ℕ \| x ∥ M\}} j^{A} \sum_{k \in \{x \in ℕ \| x ∥ N\}} k^{A} = \sum_{i \in \{x \in ℕ \| x ∥ M \cdot N\}} i^{A}$
32		sgmval	$⊢ (A \in ℂ \land M \in ℕ) \to A σ M = \sum_{j \in \{x \in ℕ \| x ∥ M\}} j^{A}$
33	1 32	syldan	$⊢ (A \in ℂ \land (M \in ℕ \land N \in ℕ \land M \gcd N = 1)) \to A σ M = \sum_{j \in \{x \in ℕ \| x ∥ M\}} j^{A}$
34		sgmval	$⊢ (A \in ℂ \land N \in ℕ) \to A σ N = \sum_{k \in \{x \in ℕ \| x ∥ N\}} k^{A}$
35	2 34	syldan	$⊢ (A \in ℂ \land (M \in ℕ \land N \in ℕ \land M \gcd N = 1)) \to A σ N = \sum_{k \in \{x \in ℕ \| x ∥ N\}} k^{A}$
36	33 35	oveq12d	$⊢ (A \in ℂ \land (M \in ℕ \land N \in ℕ \land M \gcd N = 1)) \to (A σ M) (A σ N) = \sum_{j \in \{x \in ℕ \| x ∥ M\}} j^{A} \sum_{k \in \{x \in ℕ \| x ∥ N\}} k^{A}$
37	1 2	nnmulcld	$⊢ (A \in ℂ \land (M \in ℕ \land N \in ℕ \land M \gcd N = 1)) \to M \cdot N \in ℕ$
38		sgmval	$⊢ (A \in ℂ \land M \cdot N \in ℕ) \to A σ M \cdot N = \sum_{i \in \{x \in ℕ \| x ∥ M \cdot N\}} i^{A}$
39	37 38	syldan	$⊢ (A \in ℂ \land (M \in ℕ \land N \in ℕ \land M \gcd N = 1)) \to A σ M \cdot N = \sum_{i \in \{x \in ℕ \| x ∥ M \cdot N\}} i^{A}$
40	31 36 39	3eqtr4rd	$⊢ (A \in ℂ \land (M \in ℕ \land N \in ℕ \land M \gcd N = 1)) \to A σ M \cdot N = (A σ M) (A σ N)$

Metamath Proof Explorer

Theorem sgmmul

Proof