Theorem fsumdvdscom

Description: A double commutation of divisor sums based on fsumdvdsdiag . Note that A depends on both j and k . (Contributed by Mario Carneiro, 13-May-2016)

	Ref	Expression
Hypotheses	fsumdvdscom.1	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
	fsumdvdscom.2	⊢ ( 𝑗 = ( 𝑘 · 𝑚 ) → 𝐴 = 𝐵 )
	fsumdvdscom.3	⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑗 } ) ) → 𝐴 ∈ ℂ )
Assertion	fsumdvdscom	⊢ ( 𝜑 → Σ 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } Σ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑗 } 𝐴 = Σ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } Σ 𝑚 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑘 ) } 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		fsumdvdscom.1	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
2		fsumdvdscom.2	⊢ ( 𝑗 = ( 𝑘 · 𝑚 ) → 𝐴 = 𝐵 )
3		fsumdvdscom.3	⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑗 } ) ) → 𝐴 ∈ ℂ )
4		nfcv	⊢ Ⅎ 𝑢 Σ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑗 } 𝐴
5		nfcv	⊢ Ⅎ 𝑗 { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢 }
6		nfcsb1v	⊢ Ⅎ 𝑗 ⦋ 𝑢 / 𝑗 ⦌ 𝐴
7	5 6	nfsum	⊢ Ⅎ 𝑗 Σ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢 } ⦋ 𝑢 / 𝑗 ⦌ 𝐴
8		breq2	⊢ ( 𝑗 = 𝑢 → ( 𝑥 ∥ 𝑗 ↔ 𝑥 ∥ 𝑢 ) )
9	8	rabbidv	⊢ ( 𝑗 = 𝑢 → { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑗 } = { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢 } )
10		csbeq1a	⊢ ( 𝑗 = 𝑢 → 𝐴 = ⦋ 𝑢 / 𝑗 ⦌ 𝐴 )
11	10	adantr	⊢ ( ( 𝑗 = 𝑢 ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑗 } ) → 𝐴 = ⦋ 𝑢 / 𝑗 ⦌ 𝐴 )
12	9 11	sumeq12dv	⊢ ( 𝑗 = 𝑢 → Σ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑗 } 𝐴 = Σ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢 } ⦋ 𝑢 / 𝑗 ⦌ 𝐴 )
13	4 7 12	cbvsumi	⊢ Σ 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } Σ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑗 } 𝐴 = Σ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } Σ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢 } ⦋ 𝑢 / 𝑗 ⦌ 𝐴
14		breq2	⊢ ( 𝑢 = ( 𝑁 / 𝑣 ) → ( 𝑥 ∥ 𝑢 ↔ 𝑥 ∥ ( 𝑁 / 𝑣 ) ) )
15	14	rabbidv	⊢ ( 𝑢 = ( 𝑁 / 𝑣 ) → { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢 } = { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑣 ) } )
16		csbeq1	⊢ ( 𝑢 = ( 𝑁 / 𝑣 ) → ⦋ 𝑢 / 𝑗 ⦌ 𝐴 = ⦋ ( 𝑁 / 𝑣 ) / 𝑗 ⦌ 𝐴 )
17	16	adantr	⊢ ( ( 𝑢 = ( 𝑁 / 𝑣 ) ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢 } ) → ⦋ 𝑢 / 𝑗 ⦌ 𝐴 = ⦋ ( 𝑁 / 𝑣 ) / 𝑗 ⦌ 𝐴 )
18	15 17	sumeq12dv	⊢ ( 𝑢 = ( 𝑁 / 𝑣 ) → Σ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢 } ⦋ 𝑢 / 𝑗 ⦌ 𝐴 = Σ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑣 ) } ⦋ ( 𝑁 / 𝑣 ) / 𝑗 ⦌ 𝐴 )
19		fzfid	⊢ ( 𝜑 → ( 1 ... 𝑁 ) ∈ Fin )
20		dvdsssfz1	⊢ ( 𝑁 ∈ ℕ → { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ⊆ ( 1 ... 𝑁 ) )
21	1 20	syl	⊢ ( 𝜑 → { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ⊆ ( 1 ... 𝑁 ) )
22	19 21	ssfid	⊢ ( 𝜑 → { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ∈ Fin )
23		eqid	⊢ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } = { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 }
24		eqid	⊢ ( 𝑧 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ↦ ( 𝑁 / 𝑧 ) ) = ( 𝑧 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ↦ ( 𝑁 / 𝑧 ) )
25	23 24	dvdsflip	⊢ ( 𝑁 ∈ ℕ → ( 𝑧 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ↦ ( 𝑁 / 𝑧 ) ) : { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } –1-1-onto→ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } )
26	1 25	syl	⊢ ( 𝜑 → ( 𝑧 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ↦ ( 𝑁 / 𝑧 ) ) : { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } –1-1-onto→ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } )
27		oveq2	⊢ ( 𝑧 = 𝑣 → ( 𝑁 / 𝑧 ) = ( 𝑁 / 𝑣 ) )
28		ovex	⊢ ( 𝑁 / 𝑧 ) ∈ V
29	27 24 28	fvmpt3i	⊢ ( 𝑣 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } → ( ( 𝑧 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ↦ ( 𝑁 / 𝑧 ) ) ‘ 𝑣 ) = ( 𝑁 / 𝑣 ) )
30	29	adantl	⊢ ( ( 𝜑 ∧ 𝑣 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → ( ( 𝑧 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ↦ ( 𝑁 / 𝑧 ) ) ‘ 𝑣 ) = ( 𝑁 / 𝑣 ) )
31		fzfid	⊢ ( ( 𝜑 ∧ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → ( 1 ... 𝑢 ) ∈ Fin )
32		ssrab2	⊢ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ⊆ ℕ
33		simpr	⊢ ( ( 𝜑 ∧ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } )
34	32 33	sselid	⊢ ( ( 𝜑 ∧ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → 𝑢 ∈ ℕ )
35		dvdsssfz1	⊢ ( 𝑢 ∈ ℕ → { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢 } ⊆ ( 1 ... 𝑢 ) )
36	34 35	syl	⊢ ( ( 𝜑 ∧ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢 } ⊆ ( 1 ... 𝑢 ) )
37	31 36	ssfid	⊢ ( ( 𝜑 ∧ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢 } ∈ Fin )
38	3	ralrimivva	⊢ ( 𝜑 → ∀ 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ∀ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑗 } 𝐴 ∈ ℂ )
39		nfv	⊢ Ⅎ 𝑢 ∀ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑗 } 𝐴 ∈ ℂ
40	6	nfel1	⊢ Ⅎ 𝑗 ⦋ 𝑢 / 𝑗 ⦌ 𝐴 ∈ ℂ
41	5 40	nfralw	⊢ Ⅎ 𝑗 ∀ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢 } ⦋ 𝑢 / 𝑗 ⦌ 𝐴 ∈ ℂ
42	10	eleq1d	⊢ ( 𝑗 = 𝑢 → ( 𝐴 ∈ ℂ ↔ ⦋ 𝑢 / 𝑗 ⦌ 𝐴 ∈ ℂ ) )
43	9 42	raleqbidv	⊢ ( 𝑗 = 𝑢 → ( ∀ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑗 } 𝐴 ∈ ℂ ↔ ∀ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢 } ⦋ 𝑢 / 𝑗 ⦌ 𝐴 ∈ ℂ ) )
44	39 41 43	cbvralw	⊢ ( ∀ 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ∀ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑗 } 𝐴 ∈ ℂ ↔ ∀ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ∀ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢 } ⦋ 𝑢 / 𝑗 ⦌ 𝐴 ∈ ℂ )
45	38 44	sylib	⊢ ( 𝜑 → ∀ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ∀ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢 } ⦋ 𝑢 / 𝑗 ⦌ 𝐴 ∈ ℂ )
46	45	r19.21bi	⊢ ( ( 𝜑 ∧ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → ∀ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢 } ⦋ 𝑢 / 𝑗 ⦌ 𝐴 ∈ ℂ )
47	46	r19.21bi	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢 } ) → ⦋ 𝑢 / 𝑗 ⦌ 𝐴 ∈ ℂ )
48	37 47	fsumcl	⊢ ( ( 𝜑 ∧ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → Σ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢 } ⦋ 𝑢 / 𝑗 ⦌ 𝐴 ∈ ℂ )
49	18 22 26 30 48	fsumf1o	⊢ ( 𝜑 → Σ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } Σ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢 } ⦋ 𝑢 / 𝑗 ⦌ 𝐴 = Σ 𝑣 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } Σ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑣 ) } ⦋ ( 𝑁 / 𝑣 ) / 𝑗 ⦌ 𝐴 )
50	16	eleq1d	⊢ ( 𝑢 = ( 𝑁 / 𝑣 ) → ( ⦋ 𝑢 / 𝑗 ⦌ 𝐴 ∈ ℂ ↔ ⦋ ( 𝑁 / 𝑣 ) / 𝑗 ⦌ 𝐴 ∈ ℂ ) )
51	15 50	raleqbidv	⊢ ( 𝑢 = ( 𝑁 / 𝑣 ) → ( ∀ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢 } ⦋ 𝑢 / 𝑗 ⦌ 𝐴 ∈ ℂ ↔ ∀ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑣 ) } ⦋ ( 𝑁 / 𝑣 ) / 𝑗 ⦌ 𝐴 ∈ ℂ ) )
52	45	adantr	⊢ ( ( 𝜑 ∧ 𝑣 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → ∀ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ∀ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢 } ⦋ 𝑢 / 𝑗 ⦌ 𝐴 ∈ ℂ )
53		dvdsdivcl	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑣 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → ( 𝑁 / 𝑣 ) ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } )
54	1 53	sylan	⊢ ( ( 𝜑 ∧ 𝑣 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → ( 𝑁 / 𝑣 ) ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } )
55	51 52 54	rspcdva	⊢ ( ( 𝜑 ∧ 𝑣 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → ∀ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑣 ) } ⦋ ( 𝑁 / 𝑣 ) / 𝑗 ⦌ 𝐴 ∈ ℂ )
56	55	r19.21bi	⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑣 ) } ) → ⦋ ( 𝑁 / 𝑣 ) / 𝑗 ⦌ 𝐴 ∈ ℂ )
57	56	anasss	⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑣 ) } ) ) → ⦋ ( 𝑁 / 𝑣 ) / 𝑗 ⦌ 𝐴 ∈ ℂ )
58	1 57	fsumdvdsdiag	⊢ ( 𝜑 → Σ 𝑣 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } Σ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑣 ) } ⦋ ( 𝑁 / 𝑣 ) / 𝑗 ⦌ 𝐴 = Σ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } Σ 𝑣 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑘 ) } ⦋ ( 𝑁 / 𝑣 ) / 𝑗 ⦌ 𝐴 )
59		oveq2	⊢ ( 𝑣 = ( ( 𝑁 / 𝑘 ) / 𝑚 ) → ( 𝑁 / 𝑣 ) = ( 𝑁 / ( ( 𝑁 / 𝑘 ) / 𝑚 ) ) )
60	59	csbeq1d	⊢ ( 𝑣 = ( ( 𝑁 / 𝑘 ) / 𝑚 ) → ⦋ ( 𝑁 / 𝑣 ) / 𝑗 ⦌ 𝐴 = ⦋ ( 𝑁 / ( ( 𝑁 / 𝑘 ) / 𝑚 ) ) / 𝑗 ⦌ 𝐴 )
61		fzfid	⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → ( 1 ... ( 𝑁 / 𝑘 ) ) ∈ Fin )
62		dvdsdivcl	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → ( 𝑁 / 𝑘 ) ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } )
63	32 62	sselid	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → ( 𝑁 / 𝑘 ) ∈ ℕ )
64	1 63	sylan	⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → ( 𝑁 / 𝑘 ) ∈ ℕ )
65		dvdsssfz1	⊢ ( ( 𝑁 / 𝑘 ) ∈ ℕ → { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑘 ) } ⊆ ( 1 ... ( 𝑁 / 𝑘 ) ) )
66	64 65	syl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑘 ) } ⊆ ( 1 ... ( 𝑁 / 𝑘 ) ) )
67	61 66	ssfid	⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑘 ) } ∈ Fin )
68		eqid	⊢ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑘 ) } = { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑘 ) }
69		eqid	⊢ ( 𝑧 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑘 ) } ↦ ( ( 𝑁 / 𝑘 ) / 𝑧 ) ) = ( 𝑧 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑘 ) } ↦ ( ( 𝑁 / 𝑘 ) / 𝑧 ) )
70	68 69	dvdsflip	⊢ ( ( 𝑁 / 𝑘 ) ∈ ℕ → ( 𝑧 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑘 ) } ↦ ( ( 𝑁 / 𝑘 ) / 𝑧 ) ) : { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑘 ) } –1-1-onto→ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑘 ) } )
71	64 70	syl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → ( 𝑧 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑘 ) } ↦ ( ( 𝑁 / 𝑘 ) / 𝑧 ) ) : { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑘 ) } –1-1-onto→ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑘 ) } )
72		oveq2	⊢ ( 𝑧 = 𝑚 → ( ( 𝑁 / 𝑘 ) / 𝑧 ) = ( ( 𝑁 / 𝑘 ) / 𝑚 ) )
73		ovex	⊢ ( ( 𝑁 / 𝑘 ) / 𝑧 ) ∈ V
74	72 69 73	fvmpt3i	⊢ ( 𝑚 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑘 ) } → ( ( 𝑧 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑘 ) } ↦ ( ( 𝑁 / 𝑘 ) / 𝑧 ) ) ‘ 𝑚 ) = ( ( 𝑁 / 𝑘 ) / 𝑚 ) )
75	74	adantl	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) ∧ 𝑚 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑘 ) } ) → ( ( 𝑧 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑘 ) } ↦ ( ( 𝑁 / 𝑘 ) / 𝑧 ) ) ‘ 𝑚 ) = ( ( 𝑁 / 𝑘 ) / 𝑚 ) )
76	1	fsumdvdsdiaglem	⊢ ( 𝜑 → ( ( 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ∧ 𝑣 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑘 ) } ) → ( 𝑣 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑣 ) } ) ) )
77	57	ex	⊢ ( 𝜑 → ( ( 𝑣 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑣 ) } ) → ⦋ ( 𝑁 / 𝑣 ) / 𝑗 ⦌ 𝐴 ∈ ℂ ) )
78	76 77	syld	⊢ ( 𝜑 → ( ( 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ∧ 𝑣 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑘 ) } ) → ⦋ ( 𝑁 / 𝑣 ) / 𝑗 ⦌ 𝐴 ∈ ℂ ) )
79	78	impl	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) ∧ 𝑣 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑘 ) } ) → ⦋ ( 𝑁 / 𝑣 ) / 𝑗 ⦌ 𝐴 ∈ ℂ )
80	60 67 71 75 79	fsumf1o	⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → Σ 𝑣 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑘 ) } ⦋ ( 𝑁 / 𝑣 ) / 𝑗 ⦌ 𝐴 = Σ 𝑚 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑘 ) } ⦋ ( 𝑁 / ( ( 𝑁 / 𝑘 ) / 𝑚 ) ) / 𝑗 ⦌ 𝐴 )
81		ovexd	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) ∧ 𝑚 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑘 ) } ) → ( 𝑁 / ( ( 𝑁 / 𝑘 ) / 𝑚 ) ) ∈ V )
82		nncn	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℂ )
83		nnne0	⊢ ( 𝑁 ∈ ℕ → 𝑁 ≠ 0 )
84	82 83	jca	⊢ ( 𝑁 ∈ ℕ → ( 𝑁 ∈ ℂ ∧ 𝑁 ≠ 0 ) )
85	1 84	syl	⊢ ( 𝜑 → ( 𝑁 ∈ ℂ ∧ 𝑁 ≠ 0 ) )
86	85	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) ∧ 𝑚 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑘 ) } ) → ( 𝑁 ∈ ℂ ∧ 𝑁 ≠ 0 ) )
87	86	simpld	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) ∧ 𝑚 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑘 ) } ) → 𝑁 ∈ ℂ )
88		elrabi	⊢ ( 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } → 𝑘 ∈ ℕ )
89	88	adantl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → 𝑘 ∈ ℕ )
90	89	adantr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) ∧ 𝑚 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑘 ) } ) → 𝑘 ∈ ℕ )
91		nncn	⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℂ )
92		nnne0	⊢ ( 𝑘 ∈ ℕ → 𝑘 ≠ 0 )
93	91 92	jca	⊢ ( 𝑘 ∈ ℕ → ( 𝑘 ∈ ℂ ∧ 𝑘 ≠ 0 ) )
94	90 93	syl	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) ∧ 𝑚 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑘 ) } ) → ( 𝑘 ∈ ℂ ∧ 𝑘 ≠ 0 ) )
95		elrabi	⊢ ( 𝑚 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑘 ) } → 𝑚 ∈ ℕ )
96	95	adantl	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) ∧ 𝑚 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑘 ) } ) → 𝑚 ∈ ℕ )
97		nncn	⊢ ( 𝑚 ∈ ℕ → 𝑚 ∈ ℂ )
98		nnne0	⊢ ( 𝑚 ∈ ℕ → 𝑚 ≠ 0 )
99	97 98	jca	⊢ ( 𝑚 ∈ ℕ → ( 𝑚 ∈ ℂ ∧ 𝑚 ≠ 0 ) )
100	96 99	syl	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) ∧ 𝑚 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑘 ) } ) → ( 𝑚 ∈ ℂ ∧ 𝑚 ≠ 0 ) )
101		divdiv1	⊢ ( ( 𝑁 ∈ ℂ ∧ ( 𝑘 ∈ ℂ ∧ 𝑘 ≠ 0 ) ∧ ( 𝑚 ∈ ℂ ∧ 𝑚 ≠ 0 ) ) → ( ( 𝑁 / 𝑘 ) / 𝑚 ) = ( 𝑁 / ( 𝑘 · 𝑚 ) ) )
102	87 94 100 101	syl3anc	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) ∧ 𝑚 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑘 ) } ) → ( ( 𝑁 / 𝑘 ) / 𝑚 ) = ( 𝑁 / ( 𝑘 · 𝑚 ) ) )
103	102	oveq2d	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) ∧ 𝑚 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑘 ) } ) → ( 𝑁 / ( ( 𝑁 / 𝑘 ) / 𝑚 ) ) = ( 𝑁 / ( 𝑁 / ( 𝑘 · 𝑚 ) ) ) )
104		nnmulcl	⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑚 ∈ ℕ ) → ( 𝑘 · 𝑚 ) ∈ ℕ )
105	89 95 104	syl2an	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) ∧ 𝑚 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑘 ) } ) → ( 𝑘 · 𝑚 ) ∈ ℕ )
106		nncn	⊢ ( ( 𝑘 · 𝑚 ) ∈ ℕ → ( 𝑘 · 𝑚 ) ∈ ℂ )
107		nnne0	⊢ ( ( 𝑘 · 𝑚 ) ∈ ℕ → ( 𝑘 · 𝑚 ) ≠ 0 )
108	106 107	jca	⊢ ( ( 𝑘 · 𝑚 ) ∈ ℕ → ( ( 𝑘 · 𝑚 ) ∈ ℂ ∧ ( 𝑘 · 𝑚 ) ≠ 0 ) )
109	105 108	syl	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) ∧ 𝑚 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑘 ) } ) → ( ( 𝑘 · 𝑚 ) ∈ ℂ ∧ ( 𝑘 · 𝑚 ) ≠ 0 ) )
110		ddcan	⊢ ( ( ( 𝑁 ∈ ℂ ∧ 𝑁 ≠ 0 ) ∧ ( ( 𝑘 · 𝑚 ) ∈ ℂ ∧ ( 𝑘 · 𝑚 ) ≠ 0 ) ) → ( 𝑁 / ( 𝑁 / ( 𝑘 · 𝑚 ) ) ) = ( 𝑘 · 𝑚 ) )
111	86 109 110	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) ∧ 𝑚 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑘 ) } ) → ( 𝑁 / ( 𝑁 / ( 𝑘 · 𝑚 ) ) ) = ( 𝑘 · 𝑚 ) )
112	103 111	eqtrd	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) ∧ 𝑚 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑘 ) } ) → ( 𝑁 / ( ( 𝑁 / 𝑘 ) / 𝑚 ) ) = ( 𝑘 · 𝑚 ) )
113	112	eqeq2d	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) ∧ 𝑚 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑘 ) } ) → ( 𝑗 = ( 𝑁 / ( ( 𝑁 / 𝑘 ) / 𝑚 ) ) ↔ 𝑗 = ( 𝑘 · 𝑚 ) ) )
114	113	biimpa	⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) ∧ 𝑚 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑘 ) } ) ∧ 𝑗 = ( 𝑁 / ( ( 𝑁 / 𝑘 ) / 𝑚 ) ) ) → 𝑗 = ( 𝑘 · 𝑚 ) )
115	114 2	syl	⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) ∧ 𝑚 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑘 ) } ) ∧ 𝑗 = ( 𝑁 / ( ( 𝑁 / 𝑘 ) / 𝑚 ) ) ) → 𝐴 = 𝐵 )
116	81 115	csbied	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) ∧ 𝑚 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑘 ) } ) → ⦋ ( 𝑁 / ( ( 𝑁 / 𝑘 ) / 𝑚 ) ) / 𝑗 ⦌ 𝐴 = 𝐵 )
117	116	sumeq2dv	⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → Σ 𝑚 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑘 ) } ⦋ ( 𝑁 / ( ( 𝑁 / 𝑘 ) / 𝑚 ) ) / 𝑗 ⦌ 𝐴 = Σ 𝑚 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑘 ) } 𝐵 )
118	80 117	eqtrd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → Σ 𝑣 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑘 ) } ⦋ ( 𝑁 / 𝑣 ) / 𝑗 ⦌ 𝐴 = Σ 𝑚 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑘 ) } 𝐵 )
119	118	sumeq2dv	⊢ ( 𝜑 → Σ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } Σ 𝑣 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑘 ) } ⦋ ( 𝑁 / 𝑣 ) / 𝑗 ⦌ 𝐴 = Σ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } Σ 𝑚 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑘 ) } 𝐵 )
120	49 58 119	3eqtrd	⊢ ( 𝜑 → Σ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } Σ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢 } ⦋ 𝑢 / 𝑗 ⦌ 𝐴 = Σ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } Σ 𝑚 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑘 ) } 𝐵 )
121	13 120	eqtrid	⊢ ( 𝜑 → Σ 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } Σ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑗 } 𝐴 = Σ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } Σ 𝑚 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑘 ) } 𝐵 )