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 ⊢ φ → N ∈ ℕ
Assertion fsumdvdsdiaglem ⊢ φ → j ∈ x ∈ ℕ | x ∥ N ∧ k ∈ x ∈ ℕ | x ∥ N j → k ∈ x ∈ ℕ | x ∥ N ∧ j ∈ x ∈ ℕ | x ∥ N k

Proof

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