Metamath Proof Explorer

Theorem dvdsflsumcom

Description: A sum commutation from sum_ n <_ A , sum_ d || n , B ( n , d ) to sum_ d <_ A , sum_ m <_ A / d , B ( n , d m ) . (Contributed by Mario Carneiro, 4-May-2016)

Ref Expression
Hypotheses dvdsflsumcom.1 ⊢ ( 𝑛 = ( 𝑑 · 𝑚 ) → 𝐵 = 𝐶 )
dvdsflsumcom.2 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
dvdsflsumcom.3 ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛 } ) ) → 𝐵 ∈ ℂ )
Assertion dvdsflsumcom ( 𝜑 → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) Σ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛 } 𝐵 = Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) 𝐶 )

Proof

Step Hyp Ref Expression
1 dvdsflsumcom.1 ⊢ ( 𝑛 = ( 𝑑 · 𝑚 ) → 𝐵 = 𝐶 )
2 dvdsflsumcom.2 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
3 dvdsflsumcom.3 ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛 } ) ) → 𝐵 ∈ ℂ )
4 fzfid ⊢ ( 𝜑 → ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∈ Fin )
5 fzfid ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( 1 ... 𝑛 ) ∈ Fin )
6 elfznn ⊢ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) → 𝑛 ∈ ℕ )
7 6 adantl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → 𝑛 ∈ ℕ )
8 dvdsssfz1 ⊢ ( 𝑛 ∈ ℕ → { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛 } ⊆ ( 1 ... 𝑛 ) )
9 7 8 syl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛 } ⊆ ( 1 ... 𝑛 ) )
10 5 9 ssfid ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛 } ∈ Fin )
11 nnre ⊢ ( 𝑑 ∈ ℕ → 𝑑 ∈ ℝ )
12 11 ad2antrl ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ ( 𝑑 ∈ ℕ ∧ 𝑑 ∥ 𝑛 ) ) → 𝑑 ∈ ℝ )
13 7 adantr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ ( 𝑑 ∈ ℕ ∧ 𝑑 ∥ 𝑛 ) ) → 𝑛 ∈ ℕ )
14 13 nnred ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ ( 𝑑 ∈ ℕ ∧ 𝑑 ∥ 𝑛 ) ) → 𝑛 ∈ ℝ )
15 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ ( 𝑑 ∈ ℕ ∧ 𝑑 ∥ 𝑛 ) ) → 𝐴 ∈ ℝ )
16 nnz ⊢ ( 𝑑 ∈ ℕ → 𝑑 ∈ ℤ )
17 dvdsle ⊢ ( ( 𝑑 ∈ ℤ ∧ 𝑛 ∈ ℕ ) → ( 𝑑 ∥ 𝑛 → 𝑑 ≤ 𝑛 ) )
18 16 7 17 syl2anr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑑 ∈ ℕ ) → ( 𝑑 ∥ 𝑛 → 𝑑 ≤ 𝑛 ) )
19 18 impr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ ( 𝑑 ∈ ℕ ∧ 𝑑 ∥ 𝑛 ) ) → 𝑑 ≤ 𝑛 )
20 fznnfl ⊢ ( 𝐴 ∈ ℝ → ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ↔ ( 𝑛 ∈ ℕ ∧ 𝑛 ≤ 𝐴 ) ) )
21 2 20 syl ⊢ ( 𝜑 → ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ↔ ( 𝑛 ∈ ℕ ∧ 𝑛 ≤ 𝐴 ) ) )
22 21 simplbda ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → 𝑛 ≤ 𝐴 )
23 22 adantr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ ( 𝑑 ∈ ℕ ∧ 𝑑 ∥ 𝑛 ) ) → 𝑛 ≤ 𝐴 )
24 12 14 15 19 23 letrd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ ( 𝑑 ∈ ℕ ∧ 𝑑 ∥ 𝑛 ) ) → 𝑑 ≤ 𝐴 )
25 24 ex ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( ( 𝑑 ∈ ℕ ∧ 𝑑 ∥ 𝑛 ) → 𝑑 ≤ 𝐴 ) )
26 25 pm4.71rd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( ( 𝑑 ∈ ℕ ∧ 𝑑 ∥ 𝑛 ) ↔ ( 𝑑 ≤ 𝐴 ∧ ( 𝑑 ∈ ℕ ∧ 𝑑 ∥ 𝑛 ) ) ) )
27 ancom ⊢ ( ( 𝑑 ≤ 𝐴 ∧ ( 𝑑 ∈ ℕ ∧ 𝑑 ∥ 𝑛 ) ) ↔ ( ( 𝑑 ∈ ℕ ∧ 𝑑 ∥ 𝑛 ) ∧ 𝑑 ≤ 𝐴 ) )
28 an32 ⊢ ( ( ( 𝑑 ∈ ℕ ∧ 𝑑 ∥ 𝑛 ) ∧ 𝑑 ≤ 𝐴 ) ↔ ( ( 𝑑 ∈ ℕ ∧ 𝑑 ≤ 𝐴 ) ∧ 𝑑 ∥ 𝑛 ) )
29 27 28 bitri ⊢ ( ( 𝑑 ≤ 𝐴 ∧ ( 𝑑 ∈ ℕ ∧ 𝑑 ∥ 𝑛 ) ) ↔ ( ( 𝑑 ∈ ℕ ∧ 𝑑 ≤ 𝐴 ) ∧ 𝑑 ∥ 𝑛 ) )
30 26 29 bitrdi ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( ( 𝑑 ∈ ℕ ∧ 𝑑 ∥ 𝑛 ) ↔ ( ( 𝑑 ∈ ℕ ∧ 𝑑 ≤ 𝐴 ) ∧ 𝑑 ∥ 𝑛 ) ) )
31 fznnfl ⊢ ( 𝐴 ∈ ℝ → ( 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ↔ ( 𝑑 ∈ ℕ ∧ 𝑑 ≤ 𝐴 ) ) )
32 2 31 syl ⊢ ( 𝜑 → ( 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ↔ ( 𝑑 ∈ ℕ ∧ 𝑑 ≤ 𝐴 ) ) )
33 32 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ↔ ( 𝑑 ∈ ℕ ∧ 𝑑 ≤ 𝐴 ) ) )
34 33 anbi1d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( ( 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑑 ∥ 𝑛 ) ↔ ( ( 𝑑 ∈ ℕ ∧ 𝑑 ≤ 𝐴 ) ∧ 𝑑 ∥ 𝑛 ) ) )
35 30 34 bitr4d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( ( 𝑑 ∈ ℕ ∧ 𝑑 ∥ 𝑛 ) ↔ ( 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑑 ∥ 𝑛 ) ) )
36 35 pm5.32da ⊢ ( 𝜑 → ( ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ ( 𝑑 ∈ ℕ ∧ 𝑑 ∥ 𝑛 ) ) ↔ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ ( 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑑 ∥ 𝑛 ) ) ) )
37 an12 ⊢ ( ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ ( 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑑 ∥ 𝑛 ) ) ↔ ( 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑑 ∥ 𝑛 ) ) )
38 36 37 bitrdi ⊢ ( 𝜑 → ( ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ ( 𝑑 ∈ ℕ ∧ 𝑑 ∥ 𝑛 ) ) ↔ ( 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑑 ∥ 𝑛 ) ) ) )
39 breq1 ⊢ ( 𝑥 = 𝑑 → ( 𝑥 ∥ 𝑛 ↔ 𝑑 ∥ 𝑛 ) )
40 39 elrab ⊢ ( 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛 } ↔ ( 𝑑 ∈ ℕ ∧ 𝑑 ∥ 𝑛 ) )
41 40 anbi2i ⊢ ( ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛 } ) ↔ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ ( 𝑑 ∈ ℕ ∧ 𝑑 ∥ 𝑛 ) ) )
42 breq2 ⊢ ( 𝑥 = 𝑛 → ( 𝑑 ∥ 𝑥 ↔ 𝑑 ∥ 𝑛 ) )
43 42 elrab ⊢ ( 𝑛 ∈ { 𝑥 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∣ 𝑑 ∥ 𝑥 } ↔ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑑 ∥ 𝑛 ) )
44 43 anbi2i ⊢ ( ( 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑛 ∈ { 𝑥 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∣ 𝑑 ∥ 𝑥 } ) ↔ ( 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑑 ∥ 𝑛 ) ) )
45 38 41 44 3bitr4g ⊢ ( 𝜑 → ( ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛 } ) ↔ ( 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑛 ∈ { 𝑥 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∣ 𝑑 ∥ 𝑥 } ) ) )
46 4 4 10 45 3 fsumcom2 ⊢ ( 𝜑 → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) Σ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛 } 𝐵 = Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) Σ 𝑛 ∈ { 𝑥 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∣ 𝑑 ∥ 𝑥 } 𝐵 )
47 fzfid ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ∈ Fin )
48 2 adantr ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → 𝐴 ∈ ℝ )
49 32 simprbda ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → 𝑑 ∈ ℕ )
50 eqid ⊢ ( 𝑦 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ↦ ( 𝑑 · 𝑦 ) ) = ( 𝑦 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ↦ ( 𝑑 · 𝑦 ) )
51 48 49 50 dvdsflf1o ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( 𝑦 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ↦ ( 𝑑 · 𝑦 ) ) : ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) –1-1-onto→ { 𝑥 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∣ 𝑑 ∥ 𝑥 } )
52 oveq2 ⊢ ( 𝑦 = 𝑚 → ( 𝑑 · 𝑦 ) = ( 𝑑 · 𝑚 ) )
53 ovex ⊢ ( 𝑑 · 𝑚 ) ∈ V
54 52 50 53 fvmpt ⊢ ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) → ( ( 𝑦 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ↦ ( 𝑑 · 𝑦 ) ) ‘ 𝑚 ) = ( 𝑑 · 𝑚 ) )
55 54 adantl ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → ( ( 𝑦 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ↦ ( 𝑑 · 𝑦 ) ) ‘ 𝑚 ) = ( 𝑑 · 𝑚 ) )
56 45 biimpar ⊢ ( ( 𝜑 ∧ ( 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑛 ∈ { 𝑥 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∣ 𝑑 ∥ 𝑥 } ) ) → ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛 } ) )
57 56 3 syldan ⊢ ( ( 𝜑 ∧ ( 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑛 ∈ { 𝑥 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∣ 𝑑 ∥ 𝑥 } ) ) → 𝐵 ∈ ℂ )
58 57 anassrs ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑛 ∈ { 𝑥 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∣ 𝑑 ∥ 𝑥 } ) → 𝐵 ∈ ℂ )
59 1 47 51 55 58 fsumf1o ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → Σ 𝑛 ∈ { 𝑥 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∣ 𝑑 ∥ 𝑥 } 𝐵 = Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) 𝐶 )
60 59 sumeq2dv ⊢ ( 𝜑 → Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) Σ 𝑛 ∈ { 𝑥 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∣ 𝑑 ∥ 𝑥 } 𝐵 = Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) 𝐶 )
61 46 60 eqtrd ⊢ ( 𝜑 → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) Σ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛 } 𝐵 = Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) 𝐶 )