Theorem fsumdvdsmulOLD

Description: Obsolete version of fsumdvdsmul as of 18-Apr-2025. (Contributed by Mario Carneiro, 2-Jul-2015) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypotheses	dvdsmulf1o.1	⊢ ( 𝜑 → 𝑀 ∈ ℕ )
	dvdsmulf1o.2	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
	dvdsmulf1o.3	⊢ ( 𝜑 → ( 𝑀 gcd 𝑁 ) = 1 )
	dvdsmulf1o.x	⊢ 𝑋 = { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑀 }
	dvdsmulf1o.y	⊢ 𝑌 = { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 }
	dvdsmulf1o.z	⊢ 𝑍 = { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑀 · 𝑁 ) }
	fsumdvdsmulOLD.4	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑋 ) → 𝐴 ∈ ℂ )
	fsumdvdsmulOLD.5	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑌 ) → 𝐵 ∈ ℂ )
	fsumdvdsmulOLD.6	⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑋 ∧ 𝑘 ∈ 𝑌 ) ) → ( 𝐴 · 𝐵 ) = 𝐷 )
	fsumdvdsmulOLD.7	⊢ ( 𝑖 = ( 𝑗 · 𝑘 ) → 𝐶 = 𝐷 )
Assertion	fsumdvdsmulOLD	⊢ ( 𝜑 → ( Σ 𝑗 ∈ 𝑋 𝐴 · Σ 𝑘 ∈ 𝑌 𝐵 ) = Σ 𝑖 ∈ 𝑍 𝐶 )

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		fsumdvdsmulOLD.4	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑋 ) → 𝐴 ∈ ℂ )
8		fsumdvdsmulOLD.5	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑌 ) → 𝐵 ∈ ℂ )
9		fsumdvdsmulOLD.6	⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑋 ∧ 𝑘 ∈ 𝑌 ) ) → ( 𝐴 · 𝐵 ) = 𝐷 )
10		fsumdvdsmulOLD.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		csbeq1a	⊢ ( 𝑖 = 𝑤 → 𝐶 = ⦋ 𝑤 / 𝑖 ⦌ 𝐶 )
43		nfcv	⊢ Ⅎ 𝑤 𝐶
44		nfcsb1v	⊢ Ⅎ 𝑖 ⦋ 𝑤 / 𝑖 ⦌ 𝐶
45	42 43 44	cbvsum	⊢ Σ 𝑖 ∈ 𝑍 𝐶 = Σ 𝑤 ∈ 𝑍 ⦋ 𝑤 / 𝑖 ⦌ 𝐶
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	eqtrid	⊢ ( 𝜑 → ( · “ ( 𝑋 × 𝑌 ) ) = 𝑍 )
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	eqtrid	⊢ ( 𝜑 → Σ 𝑖 ∈ 𝑍 𝐶 = Σ 𝑧 ∈ ( 𝑋 × 𝑌 ) ⦋ ( · ‘ 𝑧 ) / 𝑖 ⦌ 𝐶 )
80	41 79	eqtr4d	⊢ ( 𝜑 → Σ 𝑗 ∈ 𝑋 Σ 𝑘 ∈ 𝑌 𝐷 = Σ 𝑖 ∈ 𝑍 𝐶 )
81	22 29 80	3eqtrd	⊢ ( 𝜑 → ( Σ 𝑗 ∈ 𝑋 𝐴 · Σ 𝑘 ∈ 𝑌 𝐵 ) = Σ 𝑖 ∈ 𝑍 𝐶 )