Metamath Proof Explorer

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 sseldi ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑗 ) } ) ) → ( 𝑁 / 𝑘 ) ∈ ℕ )
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 ⊢ ( 𝜑 → ( ( 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑗 ) } ) → ( 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ∧ 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑘 ) } ) ) )