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	$⊢ n = d m \to B = C$
	dvdsflsumcom.2	$⊢ φ \to A \in ℝ$
	dvdsflsumcom.3	$⊢ (φ \land (n \in (1 \dots ⌊A⌋) \land d \in \{x \in ℕ \| x ∥ n\})) \to B \in ℂ$
Assertion	dvdsflsumcom	$⊢ φ \to \sum_{n = 1}^{⌊A⌋} \sum_{d \in \{x \in ℕ \| x ∥ n\}} B = \sum_{d = 1}^{⌊A⌋} \sum_{m = 1}^{⌊\frac{A}{d}⌋} C$

Proof

Step	Hyp	Ref	Expression
1		dvdsflsumcom.1	$⊢ n = d m \to B = C$
2		dvdsflsumcom.2	$⊢ φ \to A \in ℝ$
3		dvdsflsumcom.3	$⊢ (φ \land (n \in (1 \dots ⌊A⌋) \land d \in \{x \in ℕ \| x ∥ n\})) \to B \in ℂ$
4		fzfid	$⊢ φ \to (1 \dots ⌊A⌋) \in Fin$
5		fzfid	$⊢ (φ \land n \in (1 \dots ⌊A⌋)) \to (1 \dots n) \in Fin$
6		elfznn	$⊢ n \in (1 \dots ⌊A⌋) \to n \in ℕ$
7	6	adantl	$⊢ (φ \land n \in (1 \dots ⌊A⌋)) \to n \in ℕ$
8		dvdsssfz1	$⊢ n \in ℕ \to \{x \in ℕ \| x ∥ n\} \subseteq (1 \dots n)$
9	7 8	syl	$⊢ (φ \land n \in (1 \dots ⌊A⌋)) \to \{x \in ℕ \| x ∥ n\} \subseteq (1 \dots n)$
10	5 9	ssfid	$⊢ (φ \land n \in (1 \dots ⌊A⌋)) \to \{x \in ℕ \| x ∥ n\} \in Fin$
11		nnre	$⊢ d \in ℕ \to d \in ℝ$
12	11	ad2antrl	$⊢ ((φ \land n \in (1 \dots ⌊A⌋)) \land (d \in ℕ \land d ∥ n)) \to d \in ℝ$
13	7	adantr	$⊢ ((φ \land n \in (1 \dots ⌊A⌋)) \land (d \in ℕ \land d ∥ n)) \to n \in ℕ$
14	13	nnred	$⊢ ((φ \land n \in (1 \dots ⌊A⌋)) \land (d \in ℕ \land d ∥ n)) \to n \in ℝ$
15	2	ad2antrr	$⊢ ((φ \land n \in (1 \dots ⌊A⌋)) \land (d \in ℕ \land d ∥ n)) \to A \in ℝ$
16		nnz	$⊢ d \in ℕ \to d \in ℤ$
17		dvdsle	$⊢ (d \in ℤ \land n \in ℕ) \to (d ∥ n \to d \leq n)$
18	16 7 17	syl2anr	$⊢ ((φ \land n \in (1 \dots ⌊A⌋)) \land d \in ℕ) \to (d ∥ n \to d \leq n)$
19	18	impr	$⊢ ((φ \land n \in (1 \dots ⌊A⌋)) \land (d \in ℕ \land d ∥ n)) \to d \leq n$
20		fznnfl	$⊢ A \in ℝ \to (n \in (1 \dots ⌊A⌋) \leftrightarrow (n \in ℕ \land n \leq A))$
21	2 20	syl	$⊢ φ \to (n \in (1 \dots ⌊A⌋) \leftrightarrow (n \in ℕ \land n \leq A))$
22	21	simplbda	$⊢ (φ \land n \in (1 \dots ⌊A⌋)) \to n \leq A$
23	22	adantr	$⊢ ((φ \land n \in (1 \dots ⌊A⌋)) \land (d \in ℕ \land d ∥ n)) \to n \leq A$
24	12 14 15 19 23	letrd	$⊢ ((φ \land n \in (1 \dots ⌊A⌋)) \land (d \in ℕ \land d ∥ n)) \to d \leq A$
25	24	ex	$⊢ (φ \land n \in (1 \dots ⌊A⌋)) \to ((d \in ℕ \land d ∥ n) \to d \leq A)$
26	25	pm4.71rd	$⊢ (φ \land n \in (1 \dots ⌊A⌋)) \to ((d \in ℕ \land d ∥ n) \leftrightarrow (d \leq A \land (d \in ℕ \land d ∥ n)))$
27		ancom	$⊢ (d \leq A \land (d \in ℕ \land d ∥ n)) \leftrightarrow ((d \in ℕ \land d ∥ n) \land d \leq A)$
28		an32	$⊢ ((d \in ℕ \land d ∥ n) \land d \leq A) \leftrightarrow ((d \in ℕ \land d \leq A) \land d ∥ n)$
29	27 28	bitri	$⊢ (d \leq A \land (d \in ℕ \land d ∥ n)) \leftrightarrow ((d \in ℕ \land d \leq A) \land d ∥ n)$
30	26 29	bitrdi	$⊢ (φ \land n \in (1 \dots ⌊A⌋)) \to ((d \in ℕ \land d ∥ n) \leftrightarrow ((d \in ℕ \land d \leq A) \land d ∥ n))$
31		fznnfl	$⊢ A \in ℝ \to (d \in (1 \dots ⌊A⌋) \leftrightarrow (d \in ℕ \land d \leq A))$
32	2 31	syl	$⊢ φ \to (d \in (1 \dots ⌊A⌋) \leftrightarrow (d \in ℕ \land d \leq A))$
33	32	adantr	$⊢ (φ \land n \in (1 \dots ⌊A⌋)) \to (d \in (1 \dots ⌊A⌋) \leftrightarrow (d \in ℕ \land d \leq A))$
34	33	anbi1d	$⊢ (φ \land n \in (1 \dots ⌊A⌋)) \to ((d \in (1 \dots ⌊A⌋) \land d ∥ n) \leftrightarrow ((d \in ℕ \land d \leq A) \land d ∥ n))$
35	30 34	bitr4d	$⊢ (φ \land n \in (1 \dots ⌊A⌋)) \to ((d \in ℕ \land d ∥ n) \leftrightarrow (d \in (1 \dots ⌊A⌋) \land d ∥ n))$
36	35	pm5.32da	$⊢ φ \to ((n \in (1 \dots ⌊A⌋) \land (d \in ℕ \land d ∥ n)) \leftrightarrow (n \in (1 \dots ⌊A⌋) \land (d \in (1 \dots ⌊A⌋) \land d ∥ n)))$
37		an12	$⊢ (n \in (1 \dots ⌊A⌋) \land (d \in (1 \dots ⌊A⌋) \land d ∥ n)) \leftrightarrow (d \in (1 \dots ⌊A⌋) \land (n \in (1 \dots ⌊A⌋) \land d ∥ n))$
38	36 37	bitrdi	$⊢ φ \to ((n \in (1 \dots ⌊A⌋) \land (d \in ℕ \land d ∥ n)) \leftrightarrow (d \in (1 \dots ⌊A⌋) \land (n \in (1 \dots ⌊A⌋) \land d ∥ n)))$
39		breq1	$⊢ x = d \to (x ∥ n \leftrightarrow d ∥ n)$
40	39	elrab	$⊢ d \in \{x \in ℕ \| x ∥ n\} \leftrightarrow (d \in ℕ \land d ∥ n)$
41	40	anbi2i	$⊢ (n \in (1 \dots ⌊A⌋) \land d \in \{x \in ℕ \| x ∥ n\}) \leftrightarrow (n \in (1 \dots ⌊A⌋) \land (d \in ℕ \land d ∥ n))$
42		breq2	$⊢ x = n \to (d ∥ x \leftrightarrow d ∥ n)$
43	42	elrab	$⊢ n \in \{x \in (1 \dots ⌊A⌋) \| d ∥ x\} \leftrightarrow (n \in (1 \dots ⌊A⌋) \land d ∥ n)$
44	43	anbi2i	$⊢ (d \in (1 \dots ⌊A⌋) \land n \in \{x \in (1 \dots ⌊A⌋) \| d ∥ x\}) \leftrightarrow (d \in (1 \dots ⌊A⌋) \land (n \in (1 \dots ⌊A⌋) \land d ∥ n))$
45	38 41 44	3bitr4g	$⊢ φ \to ((n \in (1 \dots ⌊A⌋) \land d \in \{x \in ℕ \| x ∥ n\}) \leftrightarrow (d \in (1 \dots ⌊A⌋) \land n \in \{x \in (1 \dots ⌊A⌋) \| d ∥ x\}))$
46	4 4 10 45 3	fsumcom2	$⊢ φ \to \sum_{n = 1}^{⌊A⌋} \sum_{d \in \{x \in ℕ \| x ∥ n\}} B = \sum_{d = 1}^{⌊A⌋} \sum_{n \in \{x \in (1 \dots ⌊A⌋) \| d ∥ x\}} B$
47		fzfid	$⊢ (φ \land d \in (1 \dots ⌊A⌋)) \to (1 \dots ⌊\frac{A}{d}⌋) \in Fin$
48	2	adantr	$⊢ (φ \land d \in (1 \dots ⌊A⌋)) \to A \in ℝ$
49	32	simprbda	$⊢ (φ \land d \in (1 \dots ⌊A⌋)) \to d \in ℕ$
50		eqid	$⊢ (y \in (1 \dots ⌊\frac{A}{d}⌋) ⟼ d y) = (y \in (1 \dots ⌊\frac{A}{d}⌋) ⟼ d y)$
51	48 49 50	dvdsflf1o	$⊢ (φ \land d \in (1 \dots ⌊A⌋)) \to (y \in (1 \dots ⌊\frac{A}{d}⌋) ⟼ d y) : (1 \dots ⌊\frac{A}{d}⌋) \underset{1-1 onto}{⟶} \{x \in (1 \dots ⌊A⌋) \| d ∥ x\}$
52		oveq2	$⊢ y = m \to d y = d m$
53		ovex	$⊢ d m \in V$
54	52 50 53	fvmpt	$⊢ m \in (1 \dots ⌊\frac{A}{d}⌋) \to (y \in (1 \dots ⌊\frac{A}{d}⌋) ⟼ d y) (m) = d m$
55	54	adantl	$⊢ ((φ \land d \in (1 \dots ⌊A⌋)) \land m \in (1 \dots ⌊\frac{A}{d}⌋)) \to (y \in (1 \dots ⌊\frac{A}{d}⌋) ⟼ d y) (m) = d m$
56	45	biimpar	$⊢ (φ \land (d \in (1 \dots ⌊A⌋) \land n \in \{x \in (1 \dots ⌊A⌋) \| d ∥ x\})) \to (n \in (1 \dots ⌊A⌋) \land d \in \{x \in ℕ \| x ∥ n\})$
57	56 3	syldan	$⊢ (φ \land (d \in (1 \dots ⌊A⌋) \land n \in \{x \in (1 \dots ⌊A⌋) \| d ∥ x\})) \to B \in ℂ$
58	57	anassrs	$⊢ ((φ \land d \in (1 \dots ⌊A⌋)) \land n \in \{x \in (1 \dots ⌊A⌋) \| d ∥ x\}) \to B \in ℂ$
59	1 47 51 55 58	fsumf1o	$⊢ (φ \land d \in (1 \dots ⌊A⌋)) \to \sum_{n \in \{x \in (1 \dots ⌊A⌋) \| d ∥ x\}} B = \sum_{m = 1}^{⌊\frac{A}{d}⌋} C$
60	59	sumeq2dv	$⊢ φ \to \sum_{d = 1}^{⌊A⌋} \sum_{n \in \{x \in (1 \dots ⌊A⌋) \| d ∥ x\}} B = \sum_{d = 1}^{⌊A⌋} \sum_{m = 1}^{⌊\frac{A}{d}⌋} C$
61	46 60	eqtrd	$⊢ φ \to \sum_{n = 1}^{⌊A⌋} \sum_{d \in \{x \in ℕ \| x ∥ n\}} B = \sum_{d = 1}^{⌊A⌋} \sum_{m = 1}^{⌊\frac{A}{d}⌋} C$

Metamath Proof Explorer

Theorem dvdsflsumcom

Proof