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 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) 𝐶 )