Metamath Proof Explorer

Theorem 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 ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
dvdsmulf1o.2 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
dvdsmulf1o.3 ⊢ ( 𝜑 → ( 𝑀 gcd 𝑁 ) = 1 )
dvdsmulf1o.x ⊢ 𝑋 = { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑀 }
dvdsmulf1o.y ⊢ 𝑌 = { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 }
dvdsmulf1o.z ⊢ 𝑍 = { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑀 · 𝑁 ) }
fsumdvdsmul.4 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑋 ) → 𝐴 ∈ ℂ )
fsumdvdsmul.5 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑌 ) → 𝐵 ∈ ℂ )
fsumdvdsmul.6 ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑋 ∧ 𝑘 ∈ 𝑌 ) ) → ( 𝐴 · 𝐵 ) = 𝐷 )
fsumdvdsmul.7 ⊢ ( 𝑖 = ( 𝑗 · 𝑘 ) → 𝐶 = 𝐷 )
Assertion fsumdvdsmul ( 𝜑 → ( Σ 𝑗 ∈ 𝑋 𝐴 · Σ 𝑘 ∈ 𝑌 𝐵 ) = Σ 𝑖 ∈ 𝑍 𝐶 )

Proof

Step Hyp Ref Expression
1 dvdsmulf1o.1 ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
2 dvdsmulf1o.2 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
3 dvdsmulf1o.3 ⊢ ( 𝜑 → ( 𝑀 gcd 𝑁 ) = 1 )
4 dvdsmulf1o.x ⊢ 𝑋 = { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑀 }
5 dvdsmulf1o.y ⊢ 𝑌 = { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 }
6 dvdsmulf1o.z ⊢ 𝑍 = { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑀 · 𝑁 ) }
7 fsumdvdsmul.4 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑋 ) → 𝐴 ∈ ℂ )
8 fsumdvdsmul.5 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑌 ) → 𝐵 ∈ ℂ )
9 fsumdvdsmul.6 ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑋 ∧ 𝑘 ∈ 𝑌 ) ) → ( 𝐴 · 𝐵 ) = 𝐷 )
10 fsumdvdsmul.7 ⊢ ( 𝑖 = ( 𝑗 · 𝑘 ) → 𝐶 = 𝐷 )
11 fzfid ⊢ ( 𝜑 → ( 1 ... 𝑀 ) ∈ Fin )
12 dvdsssfz1 ⊢ ( 𝑀 ∈ ℕ → { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑀 } ⊆ ( 1 ... 𝑀 ) )
13 1 12 syl ⊢ ( 𝜑 → { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑀 } ⊆ ( 1 ... 𝑀 ) )
14 4 13 eqsstrid ⊢ ( 𝜑 → 𝑋 ⊆ ( 1 ... 𝑀 ) )
15 11 14 ssfid ⊢ ( 𝜑 → 𝑋 ∈ Fin )
16 fzfid ⊢ ( 𝜑 → ( 1 ... 𝑁 ) ∈ Fin )
17 dvdsssfz1 ⊢ ( 𝑁 ∈ ℕ → { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ⊆ ( 1 ... 𝑁 ) )
18 2 17 syl ⊢ ( 𝜑 → { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ⊆ ( 1 ... 𝑁 ) )
19 5 18 eqsstrid ⊢ ( 𝜑 → 𝑌 ⊆ ( 1 ... 𝑁 ) )
20 16 19 ssfid ⊢ ( 𝜑 → 𝑌 ∈ Fin )
21 20 8 fsumcl ⊢ ( 𝜑 → Σ 𝑘 ∈ 𝑌 𝐵 ∈ ℂ )
22 15 21 7 fsummulc1 ⊢ ( 𝜑 → ( Σ 𝑗 ∈ 𝑋 𝐴 · Σ 𝑘 ∈ 𝑌 𝐵 ) = Σ 𝑗 ∈ 𝑋 ( 𝐴 · Σ 𝑘 ∈ 𝑌 𝐵 ) )
23 20 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑋 ) → 𝑌 ∈ Fin )
24 8 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝑌 ) → 𝐵 ∈ ℂ )
25 23 7 24 fsummulc2 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑋 ) → ( 𝐴 · Σ 𝑘 ∈ 𝑌 𝐵 ) = Σ 𝑘 ∈ 𝑌 ( 𝐴 · 𝐵 ) )
26 9 anassrs ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝑌 ) → ( 𝐴 · 𝐵 ) = 𝐷 )
27 26 sumeq2dv ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑋 ) → Σ 𝑘 ∈ 𝑌 ( 𝐴 · 𝐵 ) = Σ 𝑘 ∈ 𝑌 𝐷 )
28 25 27 eqtrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑋 ) → ( 𝐴 · Σ 𝑘 ∈ 𝑌 𝐵 ) = Σ 𝑘 ∈ 𝑌 𝐷 )
29 28 sumeq2dv ⊢ ( 𝜑 → Σ 𝑗 ∈ 𝑋 ( 𝐴 · Σ 𝑘 ∈ 𝑌 𝐵 ) = Σ 𝑗 ∈ 𝑋 Σ 𝑘 ∈ 𝑌 𝐷 )
30 fveq2 ⊢ ( 𝑧 = ⟨ 𝑗 , 𝑘 ⟩ → ( · ‘ 𝑧 ) = ( · ‘ ⟨ 𝑗 , 𝑘 ⟩ ) )
31 df-ov ⊢ ( 𝑗 · 𝑘 ) = ( · ‘ ⟨ 𝑗 , 𝑘 ⟩ )
32 30 31 eqtr4di ⊢ ( 𝑧 = ⟨ 𝑗 , 𝑘 ⟩ → ( · ‘ 𝑧 ) = ( 𝑗 · 𝑘 ) )
33 32 csbeq1d ⊢ ( 𝑧 = ⟨ 𝑗 , 𝑘 ⟩ → ⦋ ( · ‘ 𝑧 ) / 𝑖 ⦌ 𝐶 = ⦋ ( 𝑗 · 𝑘 ) / 𝑖 ⦌ 𝐶 )
34 ovex ⊢ ( 𝑗 · 𝑘 ) ∈ V
35 34 10 csbie ⊢ ⦋ ( 𝑗 · 𝑘 ) / 𝑖 ⦌ 𝐶 = 𝐷
36 33 35 eqtrdi ⊢ ( 𝑧 = ⟨ 𝑗 , 𝑘 ⟩ → ⦋ ( · ‘ 𝑧 ) / 𝑖 ⦌ 𝐶 = 𝐷 )
37 7 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑋 ∧ 𝑘 ∈ 𝑌 ) ) → 𝐴 ∈ ℂ )
38 8 adantrl ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑋 ∧ 𝑘 ∈ 𝑌 ) ) → 𝐵 ∈ ℂ )
39 37 38 mulcld ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑋 ∧ 𝑘 ∈ 𝑌 ) ) → ( 𝐴 · 𝐵 ) ∈ ℂ )
40 9 39 eqeltrrd ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑋 ∧ 𝑘 ∈ 𝑌 ) ) → 𝐷 ∈ ℂ )
41 36 15 20 40 fsumxp ⊢ ( 𝜑 → Σ 𝑗 ∈ 𝑋 Σ 𝑘 ∈ 𝑌 𝐷 = Σ 𝑧 ∈ ( 𝑋 × 𝑌 ) ⦋ ( · ‘ 𝑧 ) / 𝑖 ⦌ 𝐶 )
42 nfcv ⊢ Ⅎ 𝑤 𝐶
43 nfcsb1v ⊢ Ⅎ 𝑖 ⦋ 𝑤 / 𝑖 ⦌ 𝐶
44 csbeq1a ⊢ ( 𝑖 = 𝑤 → 𝐶 = ⦋ 𝑤 / 𝑖 ⦌ 𝐶 )
45 42 43 44 cbvsumi ⊢ Σ 𝑖 ∈ 𝑍 𝐶 = Σ 𝑤 ∈ 𝑍 ⦋ 𝑤 / 𝑖 ⦌ 𝐶
46 csbeq1 ⊢ ( 𝑤 = ( · ‘ 𝑧 ) → ⦋ 𝑤 / 𝑖 ⦌ 𝐶 = ⦋ ( · ‘ 𝑧 ) / 𝑖 ⦌ 𝐶 )
47 xpfi ⊢ ( ( 𝑋 ∈ Fin ∧ 𝑌 ∈ Fin ) → ( 𝑋 × 𝑌 ) ∈ Fin )
48 15 20 47 syl2anc ⊢ ( 𝜑 → ( 𝑋 × 𝑌 ) ∈ Fin )
49 1 2 3 4 5 6 dvdsmulf1o ⊢ ( 𝜑 → ( · ↾ ( 𝑋 × 𝑌 ) ) : ( 𝑋 × 𝑌 ) –1-1-onto→ 𝑍 )
50 fvres ⊢ ( 𝑧 ∈ ( 𝑋 × 𝑌 ) → ( ( · ↾ ( 𝑋 × 𝑌 ) ) ‘ 𝑧 ) = ( · ‘ 𝑧 ) )
51 50 adantl ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑋 × 𝑌 ) ) → ( ( · ↾ ( 𝑋 × 𝑌 ) ) ‘ 𝑧 ) = ( · ‘ 𝑧 ) )
52 40 ralrimivva ⊢ ( 𝜑 → ∀ 𝑗 ∈ 𝑋 ∀ 𝑘 ∈ 𝑌 𝐷 ∈ ℂ )
53 36 eleq1d ⊢ ( 𝑧 = ⟨ 𝑗 , 𝑘 ⟩ → ( ⦋ ( · ‘ 𝑧 ) / 𝑖 ⦌ 𝐶 ∈ ℂ ↔ 𝐷 ∈ ℂ ) )
54 53 ralxp ⊢ ( ∀ 𝑧 ∈ ( 𝑋 × 𝑌 ) ⦋ ( · ‘ 𝑧 ) / 𝑖 ⦌ 𝐶 ∈ ℂ ↔ ∀ 𝑗 ∈ 𝑋 ∀ 𝑘 ∈ 𝑌 𝐷 ∈ ℂ )
55 52 54 sylibr ⊢ ( 𝜑 → ∀ 𝑧 ∈ ( 𝑋 × 𝑌 ) ⦋ ( · ‘ 𝑧 ) / 𝑖 ⦌ 𝐶 ∈ ℂ )
56 ax-mulf ⊢ · : ( ℂ × ℂ ) ⟶ ℂ
57 ffn ⊢ ( · : ( ℂ × ℂ ) ⟶ ℂ → · Fn ( ℂ × ℂ ) )
58 56 57 ax-mp ⊢ · Fn ( ℂ × ℂ )
59 4 ssrab3 ⊢ 𝑋 ⊆ ℕ
60 nnsscn ⊢ ℕ ⊆ ℂ
61 59 60 sstri ⊢ 𝑋 ⊆ ℂ
62 5 ssrab3 ⊢ 𝑌 ⊆ ℕ
63 62 60 sstri ⊢ 𝑌 ⊆ ℂ
64 xpss12 ⊢ ( ( 𝑋 ⊆ ℂ ∧ 𝑌 ⊆ ℂ ) → ( 𝑋 × 𝑌 ) ⊆ ( ℂ × ℂ ) )
65 61 63 64 mp2an ⊢ ( 𝑋 × 𝑌 ) ⊆ ( ℂ × ℂ )
66 46 eleq1d ⊢ ( 𝑤 = ( · ‘ 𝑧 ) → ( ⦋ 𝑤 / 𝑖 ⦌ 𝐶 ∈ ℂ ↔ ⦋ ( · ‘ 𝑧 ) / 𝑖 ⦌ 𝐶 ∈ ℂ ) )
67 66 ralima ⊢ ( ( · Fn ( ℂ × ℂ ) ∧ ( 𝑋 × 𝑌 ) ⊆ ( ℂ × ℂ ) ) → ( ∀ 𝑤 ∈ ( · “ ( 𝑋 × 𝑌 ) ) ⦋ 𝑤 / 𝑖 ⦌ 𝐶 ∈ ℂ ↔ ∀ 𝑧 ∈ ( 𝑋 × 𝑌 ) ⦋ ( · ‘ 𝑧 ) / 𝑖 ⦌ 𝐶 ∈ ℂ ) )
68 58 65 67 mp2an ⊢ ( ∀ 𝑤 ∈ ( · “ ( 𝑋 × 𝑌 ) ) ⦋ 𝑤 / 𝑖 ⦌ 𝐶 ∈ ℂ ↔ ∀ 𝑧 ∈ ( 𝑋 × 𝑌 ) ⦋ ( · ‘ 𝑧 ) / 𝑖 ⦌ 𝐶 ∈ ℂ )
69 df-ima ⊢ ( · “ ( 𝑋 × 𝑌 ) ) = ran ( · ↾ ( 𝑋 × 𝑌 ) )
70 f1ofo ⊢ ( ( · ↾ ( 𝑋 × 𝑌 ) ) : ( 𝑋 × 𝑌 ) –1-1-onto→ 𝑍 → ( · ↾ ( 𝑋 × 𝑌 ) ) : ( 𝑋 × 𝑌 ) –onto→ 𝑍 )
71 forn ⊢ ( ( · ↾ ( 𝑋 × 𝑌 ) ) : ( 𝑋 × 𝑌 ) –onto→ 𝑍 → ran ( · ↾ ( 𝑋 × 𝑌 ) ) = 𝑍 )
72 49 70 71 3syl ⊢ ( 𝜑 → ran ( · ↾ ( 𝑋 × 𝑌 ) ) = 𝑍 )
73 69 72 syl5eq ⊢ ( 𝜑 → ( · “ ( 𝑋 × 𝑌 ) ) = 𝑍 )
74 73 raleqdv ⊢ ( 𝜑 → ( ∀ 𝑤 ∈ ( · “ ( 𝑋 × 𝑌 ) ) ⦋ 𝑤 / 𝑖 ⦌ 𝐶 ∈ ℂ ↔ ∀ 𝑤 ∈ 𝑍 ⦋ 𝑤 / 𝑖 ⦌ 𝐶 ∈ ℂ ) )
75 68 74 bitr3id ⊢ ( 𝜑 → ( ∀ 𝑧 ∈ ( 𝑋 × 𝑌 ) ⦋ ( · ‘ 𝑧 ) / 𝑖 ⦌ 𝐶 ∈ ℂ ↔ ∀ 𝑤 ∈ 𝑍 ⦋ 𝑤 / 𝑖 ⦌ 𝐶 ∈ ℂ ) )
76 55 75 mpbid ⊢ ( 𝜑 → ∀ 𝑤 ∈ 𝑍 ⦋ 𝑤 / 𝑖 ⦌ 𝐶 ∈ ℂ )
77 76 r19.21bi ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑍 ) → ⦋ 𝑤 / 𝑖 ⦌ 𝐶 ∈ ℂ )
78 46 48 49 51 77 fsumf1o ⊢ ( 𝜑 → Σ 𝑤 ∈ 𝑍 ⦋ 𝑤 / 𝑖 ⦌ 𝐶 = Σ 𝑧 ∈ ( 𝑋 × 𝑌 ) ⦋ ( · ‘ 𝑧 ) / 𝑖 ⦌ 𝐶 )
79 45 78 syl5eq ⊢ ( 𝜑 → Σ 𝑖 ∈ 𝑍 𝐶 = Σ 𝑧 ∈ ( 𝑋 × 𝑌 ) ⦋ ( · ‘ 𝑧 ) / 𝑖 ⦌ 𝐶 )
80 41 79 eqtr4d ⊢ ( 𝜑 → Σ 𝑗 ∈ 𝑋 Σ 𝑘 ∈ 𝑌 𝐷 = Σ 𝑖 ∈ 𝑍 𝐶 )
81 22 29 80 3eqtrd ⊢ ( 𝜑 → ( Σ 𝑗 ∈ 𝑋 𝐴 · Σ 𝑘 ∈ 𝑌 𝐵 ) = Σ 𝑖 ∈ 𝑍 𝐶 )