Theorem fsumdvdsdiaglem

Description: A "diagonal commutation" of divisor sums analogous to fsum0diag . (Contributed by Mario Carneiro, 2-Jul-2015) (Revised by Mario Carneiro, 8-Apr-2016)

	Ref	Expression
Hypothesis	fsumdvdsdiag.1	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
Assertion	fsumdvdsdiaglem	⊢ ( 𝜑 → ( ( 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑗 ) } ) → ( 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ∧ 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑘 ) } ) ) )

Proof

Step	Hyp	Ref	Expression
1		fsumdvdsdiag.1	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
2		breq1	⊢ ( 𝑥 = 𝑘 → ( 𝑥 ∥ 𝑁 ↔ 𝑘 ∥ 𝑁 ) )
3		elrabi	⊢ ( 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑗 ) } → 𝑘 ∈ ℕ )
4	3	ad2antll	⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑗 ) } ) ) → 𝑘 ∈ ℕ )
5	4	nnzd	⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑗 ) } ) ) → 𝑘 ∈ ℤ )
6	1	adantr	⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑗 ) } ) ) → 𝑁 ∈ ℕ )
7		simprl	⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑗 ) } ) ) → 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } )
8		dvdsdivcl	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → ( 𝑁 / 𝑗 ) ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } )
9	6 7 8	syl2anc	⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑗 ) } ) ) → ( 𝑁 / 𝑗 ) ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } )
10		elrabi	⊢ ( ( 𝑁 / 𝑗 ) ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } → ( 𝑁 / 𝑗 ) ∈ ℕ )
11	9 10	syl	⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑗 ) } ) ) → ( 𝑁 / 𝑗 ) ∈ ℕ )
12	11	nnzd	⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑗 ) } ) ) → ( 𝑁 / 𝑗 ) ∈ ℤ )
13	6	nnzd	⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑗 ) } ) ) → 𝑁 ∈ ℤ )
14		breq1	⊢ ( 𝑥 = 𝑘 → ( 𝑥 ∥ ( 𝑁 / 𝑗 ) ↔ 𝑘 ∥ ( 𝑁 / 𝑗 ) ) )
15	14	elrab	⊢ ( 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑗 ) } ↔ ( 𝑘 ∈ ℕ ∧ 𝑘 ∥ ( 𝑁 / 𝑗 ) ) )
16	15	simprbi	⊢ ( 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑗 ) } → 𝑘 ∥ ( 𝑁 / 𝑗 ) )
17	16	ad2antll	⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑗 ) } ) ) → 𝑘 ∥ ( 𝑁 / 𝑗 ) )
18		breq1	⊢ ( 𝑥 = ( 𝑁 / 𝑗 ) → ( 𝑥 ∥ 𝑁 ↔ ( 𝑁 / 𝑗 ) ∥ 𝑁 ) )
19	18	elrab	⊢ ( ( 𝑁 / 𝑗 ) ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ↔ ( ( 𝑁 / 𝑗 ) ∈ ℕ ∧ ( 𝑁 / 𝑗 ) ∥ 𝑁 ) )
20	19	simprbi	⊢ ( ( 𝑁 / 𝑗 ) ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } → ( 𝑁 / 𝑗 ) ∥ 𝑁 )
21	9 20	syl	⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑗 ) } ) ) → ( 𝑁 / 𝑗 ) ∥ 𝑁 )
22	5 12 13 17 21	dvdstrd	⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑗 ) } ) ) → 𝑘 ∥ 𝑁 )
23	2 4 22	elrabd	⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑗 ) } ) ) → 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } )
24		breq1	⊢ ( 𝑥 = 𝑗 → ( 𝑥 ∥ ( 𝑁 / 𝑘 ) ↔ 𝑗 ∥ ( 𝑁 / 𝑘 ) ) )
25		elrabi	⊢ ( 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } → 𝑗 ∈ ℕ )
26	25	ad2antrl	⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑗 ) } ) ) → 𝑗 ∈ ℕ )
27	26	nnzd	⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑗 ) } ) ) → 𝑗 ∈ ℤ )
28	26	nnne0d	⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑗 ) } ) ) → 𝑗 ≠ 0 )
29		dvdsmulcr	⊢ ( ( 𝑘 ∈ ℤ ∧ ( 𝑁 / 𝑗 ) ∈ ℤ ∧ ( 𝑗 ∈ ℤ ∧ 𝑗 ≠ 0 ) ) → ( ( 𝑘 · 𝑗 ) ∥ ( ( 𝑁 / 𝑗 ) · 𝑗 ) ↔ 𝑘 ∥ ( 𝑁 / 𝑗 ) ) )
30	5 12 27 28 29	syl112anc	⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑗 ) } ) ) → ( ( 𝑘 · 𝑗 ) ∥ ( ( 𝑁 / 𝑗 ) · 𝑗 ) ↔ 𝑘 ∥ ( 𝑁 / 𝑗 ) ) )
31	17 30	mpbird	⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑗 ) } ) ) → ( 𝑘 · 𝑗 ) ∥ ( ( 𝑁 / 𝑗 ) · 𝑗 ) )
32	6	nncnd	⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑗 ) } ) ) → 𝑁 ∈ ℂ )
33	26	nncnd	⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑗 ) } ) ) → 𝑗 ∈ ℂ )
34	32 33 28	divcan1d	⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑗 ) } ) ) → ( ( 𝑁 / 𝑗 ) · 𝑗 ) = 𝑁 )
35	4	nncnd	⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑗 ) } ) ) → 𝑘 ∈ ℂ )
36	4	nnne0d	⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑗 ) } ) ) → 𝑘 ≠ 0 )
37	32 35 36	divcan2d	⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑗 ) } ) ) → ( 𝑘 · ( 𝑁 / 𝑘 ) ) = 𝑁 )
38	34 37	eqtr4d	⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑗 ) } ) ) → ( ( 𝑁 / 𝑗 ) · 𝑗 ) = ( 𝑘 · ( 𝑁 / 𝑘 ) ) )
39	31 38	breqtrd	⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑗 ) } ) ) → ( 𝑘 · 𝑗 ) ∥ ( 𝑘 · ( 𝑁 / 𝑘 ) ) )
40		ssrab2	⊢ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ⊆ ℕ
41		dvdsdivcl	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → ( 𝑁 / 𝑘 ) ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } )
42	6 23 41	syl2anc	⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑗 ) } ) ) → ( 𝑁 / 𝑘 ) ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } )
43	40 42	sselid	⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑗 ) } ) ) → ( 𝑁 / 𝑘 ) ∈ ℕ )
44	43	nnzd	⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑗 ) } ) ) → ( 𝑁 / 𝑘 ) ∈ ℤ )
45		dvdscmulr	⊢ ( ( 𝑗 ∈ ℤ ∧ ( 𝑁 / 𝑘 ) ∈ ℤ ∧ ( 𝑘 ∈ ℤ ∧ 𝑘 ≠ 0 ) ) → ( ( 𝑘 · 𝑗 ) ∥ ( 𝑘 · ( 𝑁 / 𝑘 ) ) ↔ 𝑗 ∥ ( 𝑁 / 𝑘 ) ) )
46	27 44 5 36 45	syl112anc	⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑗 ) } ) ) → ( ( 𝑘 · 𝑗 ) ∥ ( 𝑘 · ( 𝑁 / 𝑘 ) ) ↔ 𝑗 ∥ ( 𝑁 / 𝑘 ) ) )
47	39 46	mpbid	⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑗 ) } ) ) → 𝑗 ∥ ( 𝑁 / 𝑘 ) )
48	24 26 47	elrabd	⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑗 ) } ) ) → 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑘 ) } )
49	23 48	jca	⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑗 ) } ) ) → ( 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ∧ 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑘 ) } ) )
50	49	ex	⊢ ( 𝜑 → ( ( 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑗 ) } ) → ( 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ∧ 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑘 ) } ) ) )