fsumdvdsmul

Description: Product of two divisor sums. (This is also the main part of the proof that " sum_ k || N F ( k ) is a multiplicative function if F is".) (Contributed by Mario Carneiro, 2-Jul-2015)

	Ref	Expression
Hypotheses	dvdsmulf1o.1	$⊢ φ \to M \in ℕ$
	dvdsmulf1o.2	$⊢ φ \to N \in ℕ$
	dvdsmulf1o.3	$⊢ φ \to M \gcd N = 1$
	dvdsmulf1o.x	$⊢ X = \{x \in ℕ \| x ∥ M\}$
	dvdsmulf1o.y	$⊢ Y = \{x \in ℕ \| x ∥ N\}$
	dvdsmulf1o.z	$⊢ Z = \{x \in ℕ \| x ∥ M \cdot N\}$
	fsumdvdsmul.4	$⊢ (φ \land j \in X) \to A \in ℂ$
	fsumdvdsmul.5	$⊢ (φ \land k \in Y) \to B \in ℂ$
	fsumdvdsmul.6	$⊢ (φ \land (j \in X \land k \in Y)) \to A B = D$
	fsumdvdsmul.7	$⊢ i = j k \to C = D$
Assertion	fsumdvdsmul	$⊢ φ \to \sum_{j \in X} A \sum_{k \in Y} B = \sum_{i \in Z} C$

Proof

Step	Hyp	Ref	Expression
1		dvdsmulf1o.1	$⊢ φ \to M \in ℕ$
2		dvdsmulf1o.2	$⊢ φ \to N \in ℕ$
3		dvdsmulf1o.3	$⊢ φ \to M \gcd N = 1$
4		dvdsmulf1o.x	$⊢ X = \{x \in ℕ \| x ∥ M\}$
5		dvdsmulf1o.y	$⊢ Y = \{x \in ℕ \| x ∥ N\}$
6		dvdsmulf1o.z	$⊢ Z = \{x \in ℕ \| x ∥ M \cdot N\}$
7		fsumdvdsmul.4	$⊢ (φ \land j \in X) \to A \in ℂ$
8		fsumdvdsmul.5	$⊢ (φ \land k \in Y) \to B \in ℂ$
9		fsumdvdsmul.6	$⊢ (φ \land (j \in X \land k \in Y)) \to A B = D$
10		fsumdvdsmul.7	$⊢ i = j k \to C = D$
11		fzfid	$⊢ φ \to (1 \dots M) \in Fin$
12		dvdsssfz1	$⊢ M \in ℕ \to \{x \in ℕ \| x ∥ M\} \subseteq (1 \dots M)$
13	1 12	syl	$⊢ φ \to \{x \in ℕ \| x ∥ M\} \subseteq (1 \dots M)$
14	4 13	eqsstrid	$⊢ φ \to X \subseteq (1 \dots M)$
15	11 14	ssfid	$⊢ φ \to X \in Fin$
16		fzfid	$⊢ φ \to (1 \dots N) \in Fin$
17		dvdsssfz1	$⊢ N \in ℕ \to \{x \in ℕ \| x ∥ N\} \subseteq (1 \dots N)$
18	2 17	syl	$⊢ φ \to \{x \in ℕ \| x ∥ N\} \subseteq (1 \dots N)$
19	5 18	eqsstrid	$⊢ φ \to Y \subseteq (1 \dots N)$
20	16 19	ssfid	$⊢ φ \to Y \in Fin$
21	20 8	fsumcl	$⊢ φ \to \sum_{k \in Y} B \in ℂ$
22	15 21 7	fsummulc1	$⊢ φ \to \sum_{j \in X} A \sum_{k \in Y} B = \sum_{j \in X} A \sum_{k \in Y} B$
23	20	adantr	$⊢ (φ \land j \in X) \to Y \in Fin$
24	8	adantlr	$⊢ ((φ \land j \in X) \land k \in Y) \to B \in ℂ$
25	23 7 24	fsummulc2	$⊢ (φ \land j \in X) \to A \sum_{k \in Y} B = \sum_{k \in Y} A B$
26	9	anassrs	$⊢ ((φ \land j \in X) \land k \in Y) \to A B = D$
27	26	sumeq2dv	$⊢ (φ \land j \in X) \to \sum_{k \in Y} A B = \sum_{k \in Y} D$
28	25 27	eqtrd	$⊢ (φ \land j \in X) \to A \sum_{k \in Y} B = \sum_{k \in Y} D$
29	28	sumeq2dv	$⊢ φ \to \sum_{j \in X} A \sum_{k \in Y} B = \sum_{j \in X} \sum_{k \in Y} D$
30		fveq2	$⊢ z = ⟨j, k⟩ \to \times (z) = \times (⟨j, k⟩)$
31		df-ov	$⊢ j k = \times (⟨j, k⟩)$
32	30 31	eqtr4di	$⊢ z = ⟨j, k⟩ \to \times (z) = j k$
33	32	csbeq1d	$⊢ z = ⟨j, k⟩ \to ⦋ \times (z) / i ⦌ C = ⦋ j k / i ⦌ C$
34		ovex	$⊢ j k \in V$
35	34 10	csbie	$⊢ ⦋ j k / i ⦌ C = D$
36	33 35	eqtrdi	$⊢ z = ⟨j, k⟩ \to ⦋ \times (z) / i ⦌ C = D$
37	7	adantrr	$⊢ (φ \land (j \in X \land k \in Y)) \to A \in ℂ$
38	8	adantrl	$⊢ (φ \land (j \in X \land k \in Y)) \to B \in ℂ$
39	37 38	mulcld	$⊢ (φ \land (j \in X \land k \in Y)) \to A B \in ℂ$
40	9 39	eqeltrrd	$⊢ (φ \land (j \in X \land k \in Y)) \to D \in ℂ$
41	36 15 20 40	fsumxp	$⊢ φ \to \sum_{j \in X} \sum_{k \in Y} D = \sum_{z \in X \times Y} ⦋ \times (z) / i ⦌ C$
42		nfcv	$⊢ \underline{Ⅎ} w C$
43		nfcsb1v	$⊢ \underline{Ⅎ} i ⦋ w / i ⦌ C$
44		csbeq1a	$⊢ i = w \to C = ⦋ w / i ⦌ C$
45	42 43 44	cbvsumi	$⊢ \sum_{i \in Z} C = \sum_{w \in Z} ⦋ w / i ⦌ C$
46		csbeq1	$⊢ w = \times (z) \to ⦋ w / i ⦌ C = ⦋ \times (z) / i ⦌ C$
47		xpfi	$⊢ (X \in Fin \land Y \in Fin) \to X \times Y \in Fin$
48	15 20 47	syl2anc	$⊢ φ \to X \times Y \in Fin$
49	1 2 3 4 5 6	dvdsmulf1o	$⊢ φ \to ({\times ↾}_{(X \times Y)}) : X \times Y \underset{1-1 onto}{⟶} Z$
50		fvres	$⊢ z \in (X \times Y) \to ({\times ↾}_{(X \times Y)}) (z) = \times (z)$
51	50	adantl	$⊢ (φ \land z \in (X \times Y)) \to ({\times ↾}_{(X \times Y)}) (z) = \times (z)$
52	40	ralrimivva	$⊢ φ \to \forall j \in X \forall k \in Y D \in ℂ$
53	36	eleq1d	$⊢ z = ⟨j, k⟩ \to (⦋ \times (z) / i ⦌ C \in ℂ \leftrightarrow D \in ℂ)$
54	53	ralxp	$⊢ \forall z \in (X \times Y) ⦋ \times (z) / i ⦌ C \in ℂ \leftrightarrow \forall j \in X \forall k \in Y D \in ℂ$
55	52 54	sylibr	$⊢ φ \to \forall z \in (X \times Y) ⦋ \times (z) / i ⦌ C \in ℂ$
56		ax-mulf	$⊢ \times : ℂ \times ℂ ⟶ ℂ$
57		ffn	$⊢ \times : ℂ \times ℂ ⟶ ℂ \to \times Fn (ℂ \times ℂ)$
58	56 57	ax-mp	$⊢ \times Fn (ℂ \times ℂ)$
59	4	ssrab3	$⊢ X \subseteq ℕ$
60		nnsscn	$⊢ ℕ \subseteq ℂ$
61	59 60	sstri	$⊢ X \subseteq ℂ$
62	5	ssrab3	$⊢ Y \subseteq ℕ$
63	62 60	sstri	$⊢ Y \subseteq ℂ$
64		xpss12	$⊢ (X \subseteq ℂ \land Y \subseteq ℂ) \to X \times Y \subseteq ℂ \times ℂ$
65	61 63 64	mp2an	$⊢ X \times Y \subseteq ℂ \times ℂ$
66	46	eleq1d	$⊢ w = \times (z) \to (⦋ w / i ⦌ C \in ℂ \leftrightarrow ⦋ \times (z) / i ⦌ C \in ℂ)$
67	66	ralima	$⊢ (\times Fn (ℂ \times ℂ) \land X \times Y \subseteq ℂ \times ℂ) \to (\forall w \in \times [X \times Y] ⦋ w / i ⦌ C \in ℂ \leftrightarrow \forall z \in (X \times Y) ⦋ \times (z) / i ⦌ C \in ℂ)$
68	58 65 67	mp2an	$⊢ \forall w \in \times [X \times Y] ⦋ w / i ⦌ C \in ℂ \leftrightarrow \forall z \in (X \times Y) ⦋ \times (z) / i ⦌ C \in ℂ$
69		df-ima	$⊢ \times [X \times Y] = ran ({\times ↾}_{(X \times Y)})$
70		f1ofo	$⊢ ({\times ↾}_{(X \times Y)}) : X \times Y \underset{1-1 onto}{⟶} Z \to ({\times ↾}_{(X \times Y)}) : X \times Y \underset{onto}{⟶} Z$
71		forn	$⊢ ({\times ↾}_{(X \times Y)}) : X \times Y \underset{onto}{⟶} Z \to ran ({\times ↾}_{(X \times Y)}) = Z$
72	49 70 71	3syl	$⊢ φ \to ran ({\times ↾}_{(X \times Y)}) = Z$
73	69 72	syl5eq	$⊢ φ \to \times [X \times Y] = Z$
74	73	raleqdv	$⊢ φ \to (\forall w \in \times [X \times Y] ⦋ w / i ⦌ C \in ℂ \leftrightarrow \forall w \in Z ⦋ w / i ⦌ C \in ℂ)$
75	68 74	bitr3id	$⊢ φ \to (\forall z \in (X \times Y) ⦋ \times (z) / i ⦌ C \in ℂ \leftrightarrow \forall w \in Z ⦋ w / i ⦌ C \in ℂ)$
76	55 75	mpbid	$⊢ φ \to \forall w \in Z ⦋ w / i ⦌ C \in ℂ$
77	76	r19.21bi	$⊢ (φ \land w \in Z) \to ⦋ w / i ⦌ C \in ℂ$
78	46 48 49 51 77	fsumf1o	$⊢ φ \to \sum_{w \in Z} ⦋ w / i ⦌ C = \sum_{z \in X \times Y} ⦋ \times (z) / i ⦌ C$
79	45 78	syl5eq	$⊢ φ \to \sum_{i \in Z} C = \sum_{z \in X \times Y} ⦋ \times (z) / i ⦌ C$
80	41 79	eqtr4d	$⊢ φ \to \sum_{j \in X} \sum_{k \in Y} D = \sum_{i \in Z} C$
81	22 29 80	3eqtrd	$⊢ φ \to \sum_{j \in X} A \sum_{k \in Y} B = \sum_{i \in Z} C$

Metamath Proof Explorer

Theorem fsumdvdsmul

Proof