Metamath Proof Explorer

Theorem 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 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
dvdsflf1o.2 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
dvdsflf1o.f ⊢ 𝐹 = ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑁 ) ) ) ↦ ( 𝑁 · 𝑛 ) )
Assertion dvdsflf1o ( 𝜑 → 𝐹 : ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑁 ) ) ) –1-1-onto→ { 𝑥 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∣ 𝑁 ∥ 𝑥 } )

Proof

Step Hyp Ref Expression
1 dvdsflf1o.1 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2 dvdsflf1o.2 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
3 dvdsflf1o.f ⊢ 𝐹 = ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑁 ) ) ) ↦ ( 𝑁 · 𝑛 ) )
4 breq2 ⊢ ( 𝑥 = ( 𝑁 · 𝑛 ) → ( 𝑁 ∥ 𝑥 ↔ 𝑁 ∥ ( 𝑁 · 𝑛 ) ) )
5 elfznn ⊢ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑁 ) ) ) → 𝑛 ∈ ℕ )
6 nnmulcl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ℕ ) → ( 𝑁 · 𝑛 ) ∈ ℕ )
7 2 5 6 syl2an ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑁 ) ) ) ) → ( 𝑁 · 𝑛 ) ∈ ℕ )
8 1 2 nndivred ⊢ ( 𝜑 → ( 𝐴 / 𝑁 ) ∈ ℝ )
9 fznnfl ⊢ ( ( 𝐴 / 𝑁 ) ∈ ℝ → ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑁 ) ) ) ↔ ( 𝑛 ∈ ℕ ∧ 𝑛 ≤ ( 𝐴 / 𝑁 ) ) ) )
10 8 9 syl ⊢ ( 𝜑 → ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑁 ) ) ) ↔ ( 𝑛 ∈ ℕ ∧ 𝑛 ≤ ( 𝐴 / 𝑁 ) ) ) )
11 10 simplbda ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑁 ) ) ) ) → 𝑛 ≤ ( 𝐴 / 𝑁 ) )
12 5 adantl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑁 ) ) ) ) → 𝑛 ∈ ℕ )
13 12 nnred ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑁 ) ) ) ) → 𝑛 ∈ ℝ )
14 1 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑁 ) ) ) ) → 𝐴 ∈ ℝ )
15 2 nnred ⊢ ( 𝜑 → 𝑁 ∈ ℝ )
16 15 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑁 ) ) ) ) → 𝑁 ∈ ℝ )
17 2 nngt0d ⊢ ( 𝜑 → 0 < 𝑁 )
18 17 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑁 ) ) ) ) → 0 < 𝑁 )
19 lemuldiv2 ⊢ ( ( 𝑛 ∈ ℝ ∧ 𝐴 ∈ ℝ ∧ ( 𝑁 ∈ ℝ ∧ 0 < 𝑁 ) ) → ( ( 𝑁 · 𝑛 ) ≤ 𝐴 ↔ 𝑛 ≤ ( 𝐴 / 𝑁 ) ) )
20 13 14 16 18 19 syl112anc ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑁 ) ) ) ) → ( ( 𝑁 · 𝑛 ) ≤ 𝐴 ↔ 𝑛 ≤ ( 𝐴 / 𝑁 ) ) )
21 11 20 mpbird ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑁 ) ) ) ) → ( 𝑁 · 𝑛 ) ≤ 𝐴 )
22 2 nnzd ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
23 elfzelz ⊢ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑁 ) ) ) → 𝑛 ∈ ℤ )
24 zmulcl ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( 𝑁 · 𝑛 ) ∈ ℤ )
25 22 23 24 syl2an ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑁 ) ) ) ) → ( 𝑁 · 𝑛 ) ∈ ℤ )
26 flge ⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝑁 · 𝑛 ) ∈ ℤ ) → ( ( 𝑁 · 𝑛 ) ≤ 𝐴 ↔ ( 𝑁 · 𝑛 ) ≤ ( ⌊ ‘ 𝐴 ) ) )
27 14 25 26 syl2anc ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑁 ) ) ) ) → ( ( 𝑁 · 𝑛 ) ≤ 𝐴 ↔ ( 𝑁 · 𝑛 ) ≤ ( ⌊ ‘ 𝐴 ) ) )
28 21 27 mpbid ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑁 ) ) ) ) → ( 𝑁 · 𝑛 ) ≤ ( ⌊ ‘ 𝐴 ) )
29 1 flcld ⊢ ( 𝜑 → ( ⌊ ‘ 𝐴 ) ∈ ℤ )
30 29 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑁 ) ) ) ) → ( ⌊ ‘ 𝐴 ) ∈ ℤ )
31 fznn ⊢ ( ( ⌊ ‘ 𝐴 ) ∈ ℤ → ( ( 𝑁 · 𝑛 ) ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ↔ ( ( 𝑁 · 𝑛 ) ∈ ℕ ∧ ( 𝑁 · 𝑛 ) ≤ ( ⌊ ‘ 𝐴 ) ) ) )
32 30 31 syl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑁 ) ) ) ) → ( ( 𝑁 · 𝑛 ) ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ↔ ( ( 𝑁 · 𝑛 ) ∈ ℕ ∧ ( 𝑁 · 𝑛 ) ≤ ( ⌊ ‘ 𝐴 ) ) ) )
33 7 28 32 mpbir2and ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑁 ) ) ) ) → ( 𝑁 · 𝑛 ) ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) )
34 dvdsmul1 ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → 𝑁 ∥ ( 𝑁 · 𝑛 ) )
35 22 23 34 syl2an ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑁 ) ) ) ) → 𝑁 ∥ ( 𝑁 · 𝑛 ) )
36 4 33 35 elrabd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑁 ) ) ) ) → ( 𝑁 · 𝑛 ) ∈ { 𝑥 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∣ 𝑁 ∥ 𝑥 } )
37 breq2 ⊢ ( 𝑥 = 𝑚 → ( 𝑁 ∥ 𝑥 ↔ 𝑁 ∥ 𝑚 ) )
38 37 elrab ⊢ ( 𝑚 ∈ { 𝑥 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∣ 𝑁 ∥ 𝑥 } ↔ ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑁 ∥ 𝑚 ) )
39 38 simprbi ⊢ ( 𝑚 ∈ { 𝑥 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∣ 𝑁 ∥ 𝑥 } → 𝑁 ∥ 𝑚 )
40 39 adantl ⊢ ( ( 𝜑 ∧ 𝑚 ∈ { 𝑥 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∣ 𝑁 ∥ 𝑥 } ) → 𝑁 ∥ 𝑚 )
41 elrabi ⊢ ( 𝑚 ∈ { 𝑥 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∣ 𝑁 ∥ 𝑥 } → 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) )
42 41 adantl ⊢ ( ( 𝜑 ∧ 𝑚 ∈ { 𝑥 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∣ 𝑁 ∥ 𝑥 } ) → 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) )
43 elfznn ⊢ ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) → 𝑚 ∈ ℕ )
44 42 43 syl ⊢ ( ( 𝜑 ∧ 𝑚 ∈ { 𝑥 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∣ 𝑁 ∥ 𝑥 } ) → 𝑚 ∈ ℕ )
45 2 adantr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ { 𝑥 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∣ 𝑁 ∥ 𝑥 } ) → 𝑁 ∈ ℕ )
46 nndivdvds ⊢ ( ( 𝑚 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 𝑁 ∥ 𝑚 ↔ ( 𝑚 / 𝑁 ) ∈ ℕ ) )
47 44 45 46 syl2anc ⊢ ( ( 𝜑 ∧ 𝑚 ∈ { 𝑥 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∣ 𝑁 ∥ 𝑥 } ) → ( 𝑁 ∥ 𝑚 ↔ ( 𝑚 / 𝑁 ) ∈ ℕ ) )
48 40 47 mpbid ⊢ ( ( 𝜑 ∧ 𝑚 ∈ { 𝑥 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∣ 𝑁 ∥ 𝑥 } ) → ( 𝑚 / 𝑁 ) ∈ ℕ )
49 fznnfl ⊢ ( 𝐴 ∈ ℝ → ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ↔ ( 𝑚 ∈ ℕ ∧ 𝑚 ≤ 𝐴 ) ) )
50 1 49 syl ⊢ ( 𝜑 → ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ↔ ( 𝑚 ∈ ℕ ∧ 𝑚 ≤ 𝐴 ) ) )
51 50 simplbda ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → 𝑚 ≤ 𝐴 )
52 41 51 sylan2 ⊢ ( ( 𝜑 ∧ 𝑚 ∈ { 𝑥 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∣ 𝑁 ∥ 𝑥 } ) → 𝑚 ≤ 𝐴 )
53 44 nnred ⊢ ( ( 𝜑 ∧ 𝑚 ∈ { 𝑥 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∣ 𝑁 ∥ 𝑥 } ) → 𝑚 ∈ ℝ )
54 1 adantr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ { 𝑥 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∣ 𝑁 ∥ 𝑥 } ) → 𝐴 ∈ ℝ )
55 15 adantr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ { 𝑥 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∣ 𝑁 ∥ 𝑥 } ) → 𝑁 ∈ ℝ )
56 17 adantr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ { 𝑥 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∣ 𝑁 ∥ 𝑥 } ) → 0 < 𝑁 )
57 lediv1 ⊢ ( ( 𝑚 ∈ ℝ ∧ 𝐴 ∈ ℝ ∧ ( 𝑁 ∈ ℝ ∧ 0 < 𝑁 ) ) → ( 𝑚 ≤ 𝐴 ↔ ( 𝑚 / 𝑁 ) ≤ ( 𝐴 / 𝑁 ) ) )
58 53 54 55 56 57 syl112anc ⊢ ( ( 𝜑 ∧ 𝑚 ∈ { 𝑥 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∣ 𝑁 ∥ 𝑥 } ) → ( 𝑚 ≤ 𝐴 ↔ ( 𝑚 / 𝑁 ) ≤ ( 𝐴 / 𝑁 ) ) )
59 52 58 mpbid ⊢ ( ( 𝜑 ∧ 𝑚 ∈ { 𝑥 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∣ 𝑁 ∥ 𝑥 } ) → ( 𝑚 / 𝑁 ) ≤ ( 𝐴 / 𝑁 ) )
60 8 adantr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ { 𝑥 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∣ 𝑁 ∥ 𝑥 } ) → ( 𝐴 / 𝑁 ) ∈ ℝ )
61 fznnfl ⊢ ( ( 𝐴 / 𝑁 ) ∈ ℝ → ( ( 𝑚 / 𝑁 ) ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑁 ) ) ) ↔ ( ( 𝑚 / 𝑁 ) ∈ ℕ ∧ ( 𝑚 / 𝑁 ) ≤ ( 𝐴 / 𝑁 ) ) ) )
62 60 61 syl ⊢ ( ( 𝜑 ∧ 𝑚 ∈ { 𝑥 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∣ 𝑁 ∥ 𝑥 } ) → ( ( 𝑚 / 𝑁 ) ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑁 ) ) ) ↔ ( ( 𝑚 / 𝑁 ) ∈ ℕ ∧ ( 𝑚 / 𝑁 ) ≤ ( 𝐴 / 𝑁 ) ) ) )
63 48 59 62 mpbir2and ⊢ ( ( 𝜑 ∧ 𝑚 ∈ { 𝑥 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∣ 𝑁 ∥ 𝑥 } ) → ( 𝑚 / 𝑁 ) ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑁 ) ) ) )
64 44 nncnd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ { 𝑥 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∣ 𝑁 ∥ 𝑥 } ) → 𝑚 ∈ ℂ )
65 64 adantrl ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑁 ) ) ) ∧ 𝑚 ∈ { 𝑥 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∣ 𝑁 ∥ 𝑥 } ) ) → 𝑚 ∈ ℂ )
66 2 nncnd ⊢ ( 𝜑 → 𝑁 ∈ ℂ )
67 66 adantr ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑁 ) ) ) ∧ 𝑚 ∈ { 𝑥 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∣ 𝑁 ∥ 𝑥 } ) ) → 𝑁 ∈ ℂ )
68 12 nncnd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑁 ) ) ) ) → 𝑛 ∈ ℂ )
69 68 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑁 ) ) ) ∧ 𝑚 ∈ { 𝑥 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∣ 𝑁 ∥ 𝑥 } ) ) → 𝑛 ∈ ℂ )
70 2 nnne0d ⊢ ( 𝜑 → 𝑁 ≠ 0 )
71 70 adantr ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑁 ) ) ) ∧ 𝑚 ∈ { 𝑥 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∣ 𝑁 ∥ 𝑥 } ) ) → 𝑁 ≠ 0 )
72 65 67 69 71 divmuld ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑁 ) ) ) ∧ 𝑚 ∈ { 𝑥 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∣ 𝑁 ∥ 𝑥 } ) ) → ( ( 𝑚 / 𝑁 ) = 𝑛 ↔ ( 𝑁 · 𝑛 ) = 𝑚 ) )
73 eqcom ⊢ ( 𝑛 = ( 𝑚 / 𝑁 ) ↔ ( 𝑚 / 𝑁 ) = 𝑛 )
74 eqcom ⊢ ( 𝑚 = ( 𝑁 · 𝑛 ) ↔ ( 𝑁 · 𝑛 ) = 𝑚 )
75 72 73 74 3bitr4g ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑁 ) ) ) ∧ 𝑚 ∈ { 𝑥 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∣ 𝑁 ∥ 𝑥 } ) ) → ( 𝑛 = ( 𝑚 / 𝑁 ) ↔ 𝑚 = ( 𝑁 · 𝑛 ) ) )
76 3 36 63 75 f1o2d ⊢ ( 𝜑 → 𝐹 : ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑁 ) ) ) –1-1-onto→ { 𝑥 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∣ 𝑁 ∥ 𝑥 } )