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∥Nj→k∈x∈ℕ|x∥N∧j∈x∈ℕ|x∥Nk

Proof

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