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) Avoid ax-mulf . (Revised by GG, 18-Apr-2025)

	Ref	Expression
Hypotheses	mpodvdsmulf1o.1	$⊢ φ \to M \in ℕ$
	mpodvdsmulf1o.2	$⊢ φ \to N \in ℕ$
	mpodvdsmulf1o.3	$⊢ φ \to M \gcd N = 1$
	mpodvdsmulf1o.x	$⊢ X = \{x \in ℕ \| x ∥ M\}$
	mpodvdsmulf1o.y	$⊢ Y = \{x \in ℕ \| x ∥ N\}$
	mpodvdsmulf1o.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		mpodvdsmulf1o.1	$⊢ φ \to M \in ℕ$
2		mpodvdsmulf1o.2	$⊢ φ \to N \in ℕ$
3		mpodvdsmulf1o.3	$⊢ φ \to M \gcd N = 1$
4		mpodvdsmulf1o.x	$⊢ X = \{x \in ℕ \| x ∥ M\}$
5		mpodvdsmulf1o.y	$⊢ Y = \{x \in ℕ \| x ∥ N\}$
6		mpodvdsmulf1o.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		elxpi	$⊢ z \in (X \times Y) \to \exists u \exists v (z = ⟨u, v⟩ \land (u \in X \land v \in Y))$
31		fveq2	$⊢ ⟨u, v⟩ = z \to (x \in ℂ, y \in ℂ ⟼ x y) (⟨u, v⟩) = (x \in ℂ, y \in ℂ ⟼ x y) (z)$
32	31	eqcoms	$⊢ z = ⟨u, v⟩ \to (x \in ℂ, y \in ℂ ⟼ x y) (⟨u, v⟩) = (x \in ℂ, y \in ℂ ⟼ x y) (z)$
33		fveq2	$⊢ ⟨u, v⟩ = z \to \times (⟨u, v⟩) = \times (z)$
34	33	eqcoms	$⊢ z = ⟨u, v⟩ \to \times (⟨u, v⟩) = \times (z)$
35	32 34	eqeq12d	$⊢ z = ⟨u, v⟩ \to ((x \in ℂ, y \in ℂ ⟼ x y) (⟨u, v⟩) = \times (⟨u, v⟩) \leftrightarrow (x \in ℂ, y \in ℂ ⟼ x y) (z) = \times (z))$
36	35	biimpd	$⊢ z = ⟨u, v⟩ \to ((x \in ℂ, y \in ℂ ⟼ x y) (⟨u, v⟩) = \times (⟨u, v⟩) \to (x \in ℂ, y \in ℂ ⟼ x y) (z) = \times (z))$
37	4	ssrab3	$⊢ X \subseteq ℕ$
38		nnsscn	$⊢ ℕ \subseteq ℂ$
39	37 38	sstri	$⊢ X \subseteq ℂ$
40	39	sseli	$⊢ u \in X \to u \in ℂ$
41	5	ssrab3	$⊢ Y \subseteq ℕ$
42	41 38	sstri	$⊢ Y \subseteq ℂ$
43	42	sseli	$⊢ v \in Y \to v \in ℂ$
44		ovmpot	$⊢ (u \in ℂ \land v \in ℂ) \to u (x \in ℂ, y \in ℂ ⟼ x y) v = u v$
45		df-ov	$⊢ u (x \in ℂ, y \in ℂ ⟼ x y) v = (x \in ℂ, y \in ℂ ⟼ x y) (⟨u, v⟩)$
46		df-ov	$⊢ u v = \times (⟨u, v⟩)$
47	44 45 46	3eqtr3g	$⊢ (u \in ℂ \land v \in ℂ) \to (x \in ℂ, y \in ℂ ⟼ x y) (⟨u, v⟩) = \times (⟨u, v⟩)$
48	40 43 47	syl2an	$⊢ (u \in X \land v \in Y) \to (x \in ℂ, y \in ℂ ⟼ x y) (⟨u, v⟩) = \times (⟨u, v⟩)$
49	36 48	impel	$⊢ (z = ⟨u, v⟩ \land (u \in X \land v \in Y)) \to (x \in ℂ, y \in ℂ ⟼ x y) (z) = \times (z)$
50	49	exlimivv	$⊢ \exists u \exists v (z = ⟨u, v⟩ \land (u \in X \land v \in Y)) \to (x \in ℂ, y \in ℂ ⟼ x y) (z) = \times (z)$
51	30 50	syl	$⊢ z \in (X \times Y) \to (x \in ℂ, y \in ℂ ⟼ x y) (z) = \times (z)$
52	51	eqcomd	$⊢ z \in (X \times Y) \to \times (z) = (x \in ℂ, y \in ℂ ⟼ x y) (z)$
53	52	csbeq1d	$⊢ z \in (X \times Y) \to ⦋ \times (z) / i ⦌ C = ⦋ (x \in ℂ, y \in ℂ ⟼ x y) (z) / i ⦌ C$
54	53	sumeq2i	$⊢ \sum_{z \in X \times Y} ⦋ \times (z) / i ⦌ C = \sum_{z \in X \times Y} ⦋ (x \in ℂ, y \in ℂ ⟼ x y) (z) / i ⦌ C$
55		fveq2	$⊢ z = ⟨j, k⟩ \to \times (z) = \times (⟨j, k⟩)$
56		df-ov	$⊢ j k = \times (⟨j, k⟩)$
57	55 56	eqtr4di	$⊢ z = ⟨j, k⟩ \to \times (z) = j k$
58	57	csbeq1d	$⊢ z = ⟨j, k⟩ \to ⦋ \times (z) / i ⦌ C = ⦋ j k / i ⦌ C$
59		ovex	$⊢ j k \in V$
60	59 10	csbie	$⊢ ⦋ j k / i ⦌ C = D$
61	58 60	eqtrdi	$⊢ z = ⟨j, k⟩ \to ⦋ \times (z) / i ⦌ C = D$
62	7	adantrr	$⊢ (φ \land (j \in X \land k \in Y)) \to A \in ℂ$
63	8	adantrl	$⊢ (φ \land (j \in X \land k \in Y)) \to B \in ℂ$
64	62 63	mulcld	$⊢ (φ \land (j \in X \land k \in Y)) \to A B \in ℂ$
65	9 64	eqeltrrd	$⊢ (φ \land (j \in X \land k \in Y)) \to D \in ℂ$
66	61 15 20 65	fsumxp	$⊢ φ \to \sum_{j \in X} \sum_{k \in Y} D = \sum_{z \in X \times Y} ⦋ \times (z) / i ⦌ C$
67		csbeq1a	$⊢ i = w \to C = ⦋ w / i ⦌ C$
68		nfcv	$⊢ \underline{Ⅎ} w C$
69		nfcsb1v	$⊢ \underline{Ⅎ} i ⦋ w / i ⦌ C$
70	67 68 69	cbvsum	$⊢ \sum_{i \in Z} C = \sum_{w \in Z} ⦋ w / i ⦌ C$
71		csbeq1	$⊢ w = (x \in ℂ, y \in ℂ ⟼ x y) (z) \to ⦋ w / i ⦌ C = ⦋ (x \in ℂ, y \in ℂ ⟼ x y) (z) / i ⦌ C$
72		xpfi	$⊢ (X \in Fin \land Y \in Fin) \to X \times Y \in Fin$
73	15 20 72	syl2anc	$⊢ φ \to X \times Y \in Fin$
74	1 2 3 4 5 6	mpodvdsmulf1o	$⊢ φ \to ({(x \in ℂ, y \in ℂ ⟼ x y) ↾}_{(X \times Y)}) : X \times Y \underset{1-1 onto}{⟶} Z$
75		fvres	$⊢ z \in (X \times Y) \to ({(x \in ℂ, y \in ℂ ⟼ x y) ↾}_{(X \times Y)}) (z) = (x \in ℂ, y \in ℂ ⟼ x y) (z)$
76	75	adantl	$⊢ (φ \land z \in (X \times Y)) \to ({(x \in ℂ, y \in ℂ ⟼ x y) ↾}_{(X \times Y)}) (z) = (x \in ℂ, y \in ℂ ⟼ x y) (z)$
77	65	ralrimivva	$⊢ φ \to \forall j \in X \forall k \in Y D \in ℂ$
78	61	eleq1d	$⊢ z = ⟨j, k⟩ \to (⦋ \times (z) / i ⦌ C \in ℂ \leftrightarrow D \in ℂ)$
79	78	ralxp	$⊢ \forall z \in (X \times Y) ⦋ \times (z) / i ⦌ C \in ℂ \leftrightarrow \forall j \in X \forall k \in Y D \in ℂ$
80	77 79	sylibr	$⊢ φ \to \forall z \in (X \times Y) ⦋ \times (z) / i ⦌ C \in ℂ$
81		fveq2	$⊢ z = w \to \times (z) = \times (w)$
82	81	csbeq1d	$⊢ z = w \to ⦋ \times (z) / i ⦌ C = ⦋ \times (w) / i ⦌ C$
83	82	eleq1d	$⊢ z = w \to (⦋ \times (z) / i ⦌ C \in ℂ \leftrightarrow ⦋ \times (w) / i ⦌ C \in ℂ)$
84	83	cbvralvw	$⊢ \forall z \in (X \times Y) ⦋ \times (z) / i ⦌ C \in ℂ \leftrightarrow \forall w \in (X \times Y) ⦋ \times (w) / i ⦌ C \in ℂ$
85		id	$⊢ z \in (X \times Y) \to z \in (X \times Y)$
86	82	eqcoms	$⊢ w = z \to ⦋ \times (z) / i ⦌ C = ⦋ \times (w) / i ⦌ C$
87	86	adantl	$⊢ (z \in (X \times Y) \land w = z) \to ⦋ \times (z) / i ⦌ C = ⦋ \times (w) / i ⦌ C$
88	87	eleq1d	$⊢ (z \in (X \times Y) \land w = z) \to (⦋ \times (z) / i ⦌ C \in ℂ \leftrightarrow ⦋ \times (w) / i ⦌ C \in ℂ)$
89	53	eleq1d	$⊢ z \in (X \times Y) \to (⦋ \times (z) / i ⦌ C \in ℂ \leftrightarrow ⦋ (x \in ℂ, y \in ℂ ⟼ x y) (z) / i ⦌ C \in ℂ)$
90	89	adantr	$⊢ (z \in (X \times Y) \land w = z) \to (⦋ \times (z) / i ⦌ C \in ℂ \leftrightarrow ⦋ (x \in ℂ, y \in ℂ ⟼ x y) (z) / i ⦌ C \in ℂ)$
91	88 90	bitr3d	$⊢ (z \in (X \times Y) \land w = z) \to (⦋ \times (w) / i ⦌ C \in ℂ \leftrightarrow ⦋ (x \in ℂ, y \in ℂ ⟼ x y) (z) / i ⦌ C \in ℂ)$
92	85 91	rspcdv	$⊢ z \in (X \times Y) \to (\forall w \in (X \times Y) ⦋ \times (w) / i ⦌ C \in ℂ \to ⦋ (x \in ℂ, y \in ℂ ⟼ x y) (z) / i ⦌ C \in ℂ)$
93	92	com12	$⊢ \forall w \in (X \times Y) ⦋ \times (w) / i ⦌ C \in ℂ \to (z \in (X \times Y) \to ⦋ (x \in ℂ, y \in ℂ ⟼ x y) (z) / i ⦌ C \in ℂ)$
94	93	ralrimiv	$⊢ \forall w \in (X \times Y) ⦋ \times (w) / i ⦌ C \in ℂ \to \forall z \in (X \times Y) ⦋ (x \in ℂ, y \in ℂ ⟼ x y) (z) / i ⦌ C \in ℂ$
95	84 94	sylbi	$⊢ \forall z \in (X \times Y) ⦋ \times (z) / i ⦌ C \in ℂ \to \forall z \in (X \times Y) ⦋ (x \in ℂ, y \in ℂ ⟼ x y) (z) / i ⦌ C \in ℂ$
96	80 95	syl	$⊢ φ \to \forall z \in (X \times Y) ⦋ (x \in ℂ, y \in ℂ ⟼ x y) (z) / i ⦌ C \in ℂ$
97		mpomulf	$⊢ (x \in ℂ, y \in ℂ ⟼ x y) : ℂ \times ℂ ⟶ ℂ$
98		ffn	$⊢ (x \in ℂ, y \in ℂ ⟼ x y) : ℂ \times ℂ ⟶ ℂ \to (x \in ℂ, y \in ℂ ⟼ x y) Fn (ℂ \times ℂ)$
99	97 98	ax-mp	$⊢ (x \in ℂ, y \in ℂ ⟼ x y) Fn (ℂ \times ℂ)$
100		xpss12	$⊢ (X \subseteq ℂ \land Y \subseteq ℂ) \to X \times Y \subseteq ℂ \times ℂ$
101	39 42 100	mp2an	$⊢ X \times Y \subseteq ℂ \times ℂ$
102	71	eleq1d	$⊢ w = (x \in ℂ, y \in ℂ ⟼ x y) (z) \to (⦋ w / i ⦌ C \in ℂ \leftrightarrow ⦋ (x \in ℂ, y \in ℂ ⟼ x y) (z) / i ⦌ C \in ℂ)$
103	102	ralima	$⊢ ((x \in ℂ, y \in ℂ ⟼ x y) Fn (ℂ \times ℂ) \land X \times Y \subseteq ℂ \times ℂ) \to (\forall w \in (x \in ℂ, y \in ℂ ⟼ x y) [X \times Y] ⦋ w / i ⦌ C \in ℂ \leftrightarrow \forall z \in (X \times Y) ⦋ (x \in ℂ, y \in ℂ ⟼ x y) (z) / i ⦌ C \in ℂ)$
104	99 101 103	mp2an	$⊢ \forall w \in (x \in ℂ, y \in ℂ ⟼ x y) [X \times Y] ⦋ w / i ⦌ C \in ℂ \leftrightarrow \forall z \in (X \times Y) ⦋ (x \in ℂ, y \in ℂ ⟼ x y) (z) / i ⦌ C \in ℂ$
105		df-ima	$⊢ (x \in ℂ, y \in ℂ ⟼ x y) [X \times Y] = ran ({(x \in ℂ, y \in ℂ ⟼ x y) ↾}_{(X \times Y)})$
106		f1ofo	$⊢ ({(x \in ℂ, y \in ℂ ⟼ x y) ↾}_{(X \times Y)}) : X \times Y \underset{1-1 onto}{⟶} Z \to ({(x \in ℂ, y \in ℂ ⟼ x y) ↾}_{(X \times Y)}) : X \times Y \underset{onto}{⟶} Z$
107		forn	$⊢ ({(x \in ℂ, y \in ℂ ⟼ x y) ↾}_{(X \times Y)}) : X \times Y \underset{onto}{⟶} Z \to ran ({(x \in ℂ, y \in ℂ ⟼ x y) ↾}_{(X \times Y)}) = Z$
108	74 106 107	3syl	$⊢ φ \to ran ({(x \in ℂ, y \in ℂ ⟼ x y) ↾}_{(X \times Y)}) = Z$
109	105 108	eqtrid	$⊢ φ \to (x \in ℂ, y \in ℂ ⟼ x y) [X \times Y] = Z$
110	109	raleqdv	$⊢ φ \to (\forall w \in (x \in ℂ, y \in ℂ ⟼ x y) [X \times Y] ⦋ w / i ⦌ C \in ℂ \leftrightarrow \forall w \in Z ⦋ w / i ⦌ C \in ℂ)$
111	104 110	bitr3id	$⊢ φ \to (\forall z \in (X \times Y) ⦋ (x \in ℂ, y \in ℂ ⟼ x y) (z) / i ⦌ C \in ℂ \leftrightarrow \forall w \in Z ⦋ w / i ⦌ C \in ℂ)$
112	96 111	mpbid	$⊢ φ \to \forall w \in Z ⦋ w / i ⦌ C \in ℂ$
113	112	r19.21bi	$⊢ (φ \land w \in Z) \to ⦋ w / i ⦌ C \in ℂ$
114	71 73 74 76 113	fsumf1o	$⊢ φ \to \sum_{w \in Z} ⦋ w / i ⦌ C = \sum_{z \in X \times Y} ⦋ (x \in ℂ, y \in ℂ ⟼ x y) (z) / i ⦌ C$
115	70 114	eqtrid	$⊢ φ \to \sum_{i \in Z} C = \sum_{z \in X \times Y} ⦋ (x \in ℂ, y \in ℂ ⟼ x y) (z) / i ⦌ C$
116	54 66 115	3eqtr4a	$⊢ φ \to \sum_{j \in X} \sum_{k \in Y} D = \sum_{i \in Z} C$
117	22 29 116	3eqtrd	$⊢ φ \to \sum_{j \in X} A \sum_{k \in Y} B = \sum_{i \in Z} C$

Metamath Proof Explorer

Theorem fsumdvdsmul

Proof