dvdsflf1o

Description: A bijection from the numbers less than N / A to the multiples of A less than N . Useful for some sum manipulations. (Contributed by Mario Carneiro, 3-May-2016)

	Ref	Expression
Hypotheses	dvdsflf1o.1	$⊢ φ \to A \in ℝ$
	dvdsflf1o.2	$⊢ φ \to N \in ℕ$
	dvdsflf1o.f	$⊢ F = (n \in (1 \dots ⌊\frac{A}{N}⌋) ⟼ N n)$
Assertion	dvdsflf1o	$⊢ φ \to F : (1 \dots ⌊\frac{A}{N}⌋) \underset{1-1 onto}{⟶} \{x \in (1 \dots ⌊A⌋) \| N ∥ x\}$

Proof

Step	Hyp	Ref	Expression
1		dvdsflf1o.1	$⊢ φ \to A \in ℝ$
2		dvdsflf1o.2	$⊢ φ \to N \in ℕ$
3		dvdsflf1o.f	$⊢ F = (n \in (1 \dots ⌊\frac{A}{N}⌋) ⟼ N n)$
4		breq2	$⊢ x = N n \to (N ∥ x \leftrightarrow N ∥ N n)$
5		elfznn	$⊢ n \in (1 \dots ⌊\frac{A}{N}⌋) \to n \in ℕ$
6		nnmulcl	$⊢ (N \in ℕ \land n \in ℕ) \to N n \in ℕ$
7	2 5 6	syl2an	$⊢ (φ \land n \in (1 \dots ⌊\frac{A}{N}⌋)) \to N n \in ℕ$
8	1 2	nndivred	$⊢ φ \to \frac{A}{N} \in ℝ$
9		fznnfl	$⊢ \frac{A}{N} \in ℝ \to (n \in (1 \dots ⌊\frac{A}{N}⌋) \leftrightarrow (n \in ℕ \land n \leq \frac{A}{N}))$
10	8 9	syl	$⊢ φ \to (n \in (1 \dots ⌊\frac{A}{N}⌋) \leftrightarrow (n \in ℕ \land n \leq \frac{A}{N}))$
11	10	simplbda	$⊢ (φ \land n \in (1 \dots ⌊\frac{A}{N}⌋)) \to n \leq \frac{A}{N}$
12	5	adantl	$⊢ (φ \land n \in (1 \dots ⌊\frac{A}{N}⌋)) \to n \in ℕ$
13	12	nnred	$⊢ (φ \land n \in (1 \dots ⌊\frac{A}{N}⌋)) \to n \in ℝ$
14	1	adantr	$⊢ (φ \land n \in (1 \dots ⌊\frac{A}{N}⌋)) \to A \in ℝ$
15	2	nnred	$⊢ φ \to N \in ℝ$
16	15	adantr	$⊢ (φ \land n \in (1 \dots ⌊\frac{A}{N}⌋)) \to N \in ℝ$
17	2	nngt0d	$⊢ φ \to 0 < N$
18	17	adantr	$⊢ (φ \land n \in (1 \dots ⌊\frac{A}{N}⌋)) \to 0 < N$
19		lemuldiv2	$⊢ (n \in ℝ \land A \in ℝ \land (N \in ℝ \land 0 < N)) \to (N n \leq A \leftrightarrow n \leq \frac{A}{N})$
20	13 14 16 18 19	syl112anc	$⊢ (φ \land n \in (1 \dots ⌊\frac{A}{N}⌋)) \to (N n \leq A \leftrightarrow n \leq \frac{A}{N})$
21	11 20	mpbird	$⊢ (φ \land n \in (1 \dots ⌊\frac{A}{N}⌋)) \to N n \leq A$
22	2	nnzd	$⊢ φ \to N \in ℤ$
23		elfzelz	$⊢ n \in (1 \dots ⌊\frac{A}{N}⌋) \to n \in ℤ$
24		zmulcl	$⊢ (N \in ℤ \land n \in ℤ) \to N n \in ℤ$
25	22 23 24	syl2an	$⊢ (φ \land n \in (1 \dots ⌊\frac{A}{N}⌋)) \to N n \in ℤ$
26		flge	$⊢ (A \in ℝ \land N n \in ℤ) \to (N n \leq A \leftrightarrow N n \leq ⌊A⌋)$
27	14 25 26	syl2anc	$⊢ (φ \land n \in (1 \dots ⌊\frac{A}{N}⌋)) \to (N n \leq A \leftrightarrow N n \leq ⌊A⌋)$
28	21 27	mpbid	$⊢ (φ \land n \in (1 \dots ⌊\frac{A}{N}⌋)) \to N n \leq ⌊A⌋$
29	1	flcld	$⊢ φ \to ⌊A⌋ \in ℤ$
30	29	adantr	$⊢ (φ \land n \in (1 \dots ⌊\frac{A}{N}⌋)) \to ⌊A⌋ \in ℤ$
31		fznn	$⊢ ⌊A⌋ \in ℤ \to (N n \in (1 \dots ⌊A⌋) \leftrightarrow (N n \in ℕ \land N n \leq ⌊A⌋))$
32	30 31	syl	$⊢ (φ \land n \in (1 \dots ⌊\frac{A}{N}⌋)) \to (N n \in (1 \dots ⌊A⌋) \leftrightarrow (N n \in ℕ \land N n \leq ⌊A⌋))$
33	7 28 32	mpbir2and	$⊢ (φ \land n \in (1 \dots ⌊\frac{A}{N}⌋)) \to N n \in (1 \dots ⌊A⌋)$
34		dvdsmul1	$⊢ (N \in ℤ \land n \in ℤ) \to N ∥ N n$
35	22 23 34	syl2an	$⊢ (φ \land n \in (1 \dots ⌊\frac{A}{N}⌋)) \to N ∥ N n$
36	4 33 35	elrabd	$⊢ (φ \land n \in (1 \dots ⌊\frac{A}{N}⌋)) \to N n \in \{x \in (1 \dots ⌊A⌋) \| N ∥ x\}$
37		breq2	$⊢ x = m \to (N ∥ x \leftrightarrow N ∥ m)$
38	37	elrab	$⊢ m \in \{x \in (1 \dots ⌊A⌋) \| N ∥ x\} \leftrightarrow (m \in (1 \dots ⌊A⌋) \land N ∥ m)$
39	38	simprbi	$⊢ m \in \{x \in (1 \dots ⌊A⌋) \| N ∥ x\} \to N ∥ m$
40	39	adantl	$⊢ (φ \land m \in \{x \in (1 \dots ⌊A⌋) \| N ∥ x\}) \to N ∥ m$
41		elrabi	$⊢ m \in \{x \in (1 \dots ⌊A⌋) \| N ∥ x\} \to m \in (1 \dots ⌊A⌋)$
42	41	adantl	$⊢ (φ \land m \in \{x \in (1 \dots ⌊A⌋) \| N ∥ x\}) \to m \in (1 \dots ⌊A⌋)$
43		elfznn	$⊢ m \in (1 \dots ⌊A⌋) \to m \in ℕ$
44	42 43	syl	$⊢ (φ \land m \in \{x \in (1 \dots ⌊A⌋) \| N ∥ x\}) \to m \in ℕ$
45	2	adantr	$⊢ (φ \land m \in \{x \in (1 \dots ⌊A⌋) \| N ∥ x\}) \to N \in ℕ$
46		nndivdvds	$⊢ (m \in ℕ \land N \in ℕ) \to (N ∥ m \leftrightarrow \frac{m}{N} \in ℕ)$
47	44 45 46	syl2anc	$⊢ (φ \land m \in \{x \in (1 \dots ⌊A⌋) \| N ∥ x\}) \to (N ∥ m \leftrightarrow \frac{m}{N} \in ℕ)$
48	40 47	mpbid	$⊢ (φ \land m \in \{x \in (1 \dots ⌊A⌋) \| N ∥ x\}) \to \frac{m}{N} \in ℕ$
49		fznnfl	$⊢ A \in ℝ \to (m \in (1 \dots ⌊A⌋) \leftrightarrow (m \in ℕ \land m \leq A))$
50	1 49	syl	$⊢ φ \to (m \in (1 \dots ⌊A⌋) \leftrightarrow (m \in ℕ \land m \leq A))$
51	50	simplbda	$⊢ (φ \land m \in (1 \dots ⌊A⌋)) \to m \leq A$
52	41 51	sylan2	$⊢ (φ \land m \in \{x \in (1 \dots ⌊A⌋) \| N ∥ x\}) \to m \leq A$
53	44	nnred	$⊢ (φ \land m \in \{x \in (1 \dots ⌊A⌋) \| N ∥ x\}) \to m \in ℝ$
54	1	adantr	$⊢ (φ \land m \in \{x \in (1 \dots ⌊A⌋) \| N ∥ x\}) \to A \in ℝ$
55	15	adantr	$⊢ (φ \land m \in \{x \in (1 \dots ⌊A⌋) \| N ∥ x\}) \to N \in ℝ$
56	17	adantr	$⊢ (φ \land m \in \{x \in (1 \dots ⌊A⌋) \| N ∥ x\}) \to 0 < N$
57		lediv1	$⊢ (m \in ℝ \land A \in ℝ \land (N \in ℝ \land 0 < N)) \to (m \leq A \leftrightarrow \frac{m}{N} \leq \frac{A}{N})$
58	53 54 55 56 57	syl112anc	$⊢ (φ \land m \in \{x \in (1 \dots ⌊A⌋) \| N ∥ x\}) \to (m \leq A \leftrightarrow \frac{m}{N} \leq \frac{A}{N})$
59	52 58	mpbid	$⊢ (φ \land m \in \{x \in (1 \dots ⌊A⌋) \| N ∥ x\}) \to \frac{m}{N} \leq \frac{A}{N}$
60	8	adantr	$⊢ (φ \land m \in \{x \in (1 \dots ⌊A⌋) \| N ∥ x\}) \to \frac{A}{N} \in ℝ$
61		fznnfl	$⊢ \frac{A}{N} \in ℝ \to (\frac{m}{N} \in (1 \dots ⌊\frac{A}{N}⌋) \leftrightarrow (\frac{m}{N} \in ℕ \land \frac{m}{N} \leq \frac{A}{N}))$
62	60 61	syl	$⊢ (φ \land m \in \{x \in (1 \dots ⌊A⌋) \| N ∥ x\}) \to (\frac{m}{N} \in (1 \dots ⌊\frac{A}{N}⌋) \leftrightarrow (\frac{m}{N} \in ℕ \land \frac{m}{N} \leq \frac{A}{N}))$
63	48 59 62	mpbir2and	$⊢ (φ \land m \in \{x \in (1 \dots ⌊A⌋) \| N ∥ x\}) \to \frac{m}{N} \in (1 \dots ⌊\frac{A}{N}⌋)$
64	44	nncnd	$⊢ (φ \land m \in \{x \in (1 \dots ⌊A⌋) \| N ∥ x\}) \to m \in ℂ$
65	64	adantrl	$⊢ (φ \land (n \in (1 \dots ⌊\frac{A}{N}⌋) \land m \in \{x \in (1 \dots ⌊A⌋) \| N ∥ x\})) \to m \in ℂ$
66	2	nncnd	$⊢ φ \to N \in ℂ$
67	66	adantr	$⊢ (φ \land (n \in (1 \dots ⌊\frac{A}{N}⌋) \land m \in \{x \in (1 \dots ⌊A⌋) \| N ∥ x\})) \to N \in ℂ$
68	12	nncnd	$⊢ (φ \land n \in (1 \dots ⌊\frac{A}{N}⌋)) \to n \in ℂ$
69	68	adantrr	$⊢ (φ \land (n \in (1 \dots ⌊\frac{A}{N}⌋) \land m \in \{x \in (1 \dots ⌊A⌋) \| N ∥ x\})) \to n \in ℂ$
70	2	nnne0d	$⊢ φ \to N \neq 0$
71	70	adantr	$⊢ (φ \land (n \in (1 \dots ⌊\frac{A}{N}⌋) \land m \in \{x \in (1 \dots ⌊A⌋) \| N ∥ x\})) \to N \neq 0$
72	65 67 69 71	divmuld	$⊢ (φ \land (n \in (1 \dots ⌊\frac{A}{N}⌋) \land m \in \{x \in (1 \dots ⌊A⌋) \| N ∥ x\})) \to (\frac{m}{N} = n \leftrightarrow N n = m)$
73		eqcom	$⊢ n = \frac{m}{N} \leftrightarrow \frac{m}{N} = n$
74		eqcom	$⊢ m = N n \leftrightarrow N n = m$
75	72 73 74	3bitr4g	$⊢ (φ \land (n \in (1 \dots ⌊\frac{A}{N}⌋) \land m \in \{x \in (1 \dots ⌊A⌋) \| N ∥ x\})) \to (n = \frac{m}{N} \leftrightarrow m = N n)$
76	3 36 63 75	f1o2d	$⊢ φ \to F : (1 \dots ⌊\frac{A}{N}⌋) \underset{1-1 onto}{⟶} \{x \in (1 \dots ⌊A⌋) \| N ∥ x\}$

Metamath Proof Explorer

Theorem dvdsflf1o

Proof