Step | Hyp | Ref
| Expression |
1 | | dvdsflf1o.f |
. 2
⊢ 𝐹 = (𝑛 ∈ (1...(⌊‘(𝐴 / 𝑁))) ↦ (𝑁 · 𝑛)) |
2 | | dvdsflf1o.2 |
. . . . 5
⊢ (𝜑 → 𝑁 ∈ ℕ) |
3 | | elfznn 12241 |
. . . . 5
⊢ (𝑛 ∈
(1...(⌊‘(𝐴 /
𝑁))) → 𝑛 ∈
ℕ) |
4 | | nnmulcl 10920 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℕ) → (𝑁 · 𝑛) ∈ ℕ) |
5 | 2, 3, 4 | syl2an 493 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘(𝐴 / 𝑁)))) → (𝑁 · 𝑛) ∈ ℕ) |
6 | | dvdsflf1o.1 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ∈ ℝ) |
7 | 6, 2 | nndivred 10946 |
. . . . . . . 8
⊢ (𝜑 → (𝐴 / 𝑁) ∈ ℝ) |
8 | | fznnfl 12523 |
. . . . . . . 8
⊢ ((𝐴 / 𝑁) ∈ ℝ → (𝑛 ∈ (1...(⌊‘(𝐴 / 𝑁))) ↔ (𝑛 ∈ ℕ ∧ 𝑛 ≤ (𝐴 / 𝑁)))) |
9 | 7, 8 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (𝑛 ∈ (1...(⌊‘(𝐴 / 𝑁))) ↔ (𝑛 ∈ ℕ ∧ 𝑛 ≤ (𝐴 / 𝑁)))) |
10 | 9 | simplbda 652 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘(𝐴 / 𝑁)))) → 𝑛 ≤ (𝐴 / 𝑁)) |
11 | 3 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘(𝐴 / 𝑁)))) → 𝑛 ∈ ℕ) |
12 | 11 | nnred 10912 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘(𝐴 / 𝑁)))) → 𝑛 ∈ ℝ) |
13 | 6 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘(𝐴 / 𝑁)))) → 𝐴 ∈ ℝ) |
14 | 2 | nnred 10912 |
. . . . . . . 8
⊢ (𝜑 → 𝑁 ∈ ℝ) |
15 | 14 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘(𝐴 / 𝑁)))) → 𝑁 ∈ ℝ) |
16 | 2 | nngt0d 10941 |
. . . . . . . 8
⊢ (𝜑 → 0 < 𝑁) |
17 | 16 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘(𝐴 / 𝑁)))) → 0 < 𝑁) |
18 | | lemuldiv2 10783 |
. . . . . . 7
⊢ ((𝑛 ∈ ℝ ∧ 𝐴 ∈ ℝ ∧ (𝑁 ∈ ℝ ∧ 0 <
𝑁)) → ((𝑁 · 𝑛) ≤ 𝐴 ↔ 𝑛 ≤ (𝐴 / 𝑁))) |
19 | 12, 13, 15, 17, 18 | syl112anc 1322 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘(𝐴 / 𝑁)))) → ((𝑁 · 𝑛) ≤ 𝐴 ↔ 𝑛 ≤ (𝐴 / 𝑁))) |
20 | 10, 19 | mpbird 246 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘(𝐴 / 𝑁)))) → (𝑁 · 𝑛) ≤ 𝐴) |
21 | 2 | nnzd 11357 |
. . . . . . 7
⊢ (𝜑 → 𝑁 ∈ ℤ) |
22 | | elfzelz 12213 |
. . . . . . 7
⊢ (𝑛 ∈
(1...(⌊‘(𝐴 /
𝑁))) → 𝑛 ∈
ℤ) |
23 | | zmulcl 11303 |
. . . . . . 7
⊢ ((𝑁 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (𝑁 · 𝑛) ∈ ℤ) |
24 | 21, 22, 23 | syl2an 493 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘(𝐴 / 𝑁)))) → (𝑁 · 𝑛) ∈ ℤ) |
25 | | flge 12468 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ (𝑁 · 𝑛) ∈ ℤ) → ((𝑁 · 𝑛) ≤ 𝐴 ↔ (𝑁 · 𝑛) ≤ (⌊‘𝐴))) |
26 | 13, 24, 25 | syl2anc 691 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘(𝐴 / 𝑁)))) → ((𝑁 · 𝑛) ≤ 𝐴 ↔ (𝑁 · 𝑛) ≤ (⌊‘𝐴))) |
27 | 20, 26 | mpbid 221 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘(𝐴 / 𝑁)))) → (𝑁 · 𝑛) ≤ (⌊‘𝐴)) |
28 | 6 | flcld 12461 |
. . . . . 6
⊢ (𝜑 → (⌊‘𝐴) ∈
ℤ) |
29 | 28 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘(𝐴 / 𝑁)))) → (⌊‘𝐴) ∈ ℤ) |
30 | | fznn 12278 |
. . . . 5
⊢
((⌊‘𝐴)
∈ ℤ → ((𝑁
· 𝑛) ∈
(1...(⌊‘𝐴))
↔ ((𝑁 · 𝑛) ∈ ℕ ∧ (𝑁 · 𝑛) ≤ (⌊‘𝐴)))) |
31 | 29, 30 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘(𝐴 / 𝑁)))) → ((𝑁 · 𝑛) ∈ (1...(⌊‘𝐴)) ↔ ((𝑁 · 𝑛) ∈ ℕ ∧ (𝑁 · 𝑛) ≤ (⌊‘𝐴)))) |
32 | 5, 27, 31 | mpbir2and 959 |
. . 3
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘(𝐴 / 𝑁)))) → (𝑁 · 𝑛) ∈ (1...(⌊‘𝐴))) |
33 | | dvdsmul1 14841 |
. . . 4
⊢ ((𝑁 ∈ ℤ ∧ 𝑛 ∈ ℤ) → 𝑁 ∥ (𝑁 · 𝑛)) |
34 | 21, 22, 33 | syl2an 493 |
. . 3
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘(𝐴 / 𝑁)))) → 𝑁 ∥ (𝑁 · 𝑛)) |
35 | | breq2 4587 |
. . . 4
⊢ (𝑥 = (𝑁 · 𝑛) → (𝑁 ∥ 𝑥 ↔ 𝑁 ∥ (𝑁 · 𝑛))) |
36 | 35 | elrab 3331 |
. . 3
⊢ ((𝑁 · 𝑛) ∈ {𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑁 ∥ 𝑥} ↔ ((𝑁 · 𝑛) ∈ (1...(⌊‘𝐴)) ∧ 𝑁 ∥ (𝑁 · 𝑛))) |
37 | 32, 34, 36 | sylanbrc 695 |
. 2
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘(𝐴 / 𝑁)))) → (𝑁 · 𝑛) ∈ {𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑁 ∥ 𝑥}) |
38 | | breq2 4587 |
. . . . . . 7
⊢ (𝑥 = 𝑚 → (𝑁 ∥ 𝑥 ↔ 𝑁 ∥ 𝑚)) |
39 | 38 | elrab 3331 |
. . . . . 6
⊢ (𝑚 ∈ {𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑁 ∥ 𝑥} ↔ (𝑚 ∈ (1...(⌊‘𝐴)) ∧ 𝑁 ∥ 𝑚)) |
40 | 39 | simprbi 479 |
. . . . 5
⊢ (𝑚 ∈ {𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑁 ∥ 𝑥} → 𝑁 ∥ 𝑚) |
41 | 40 | adantl 481 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ {𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑁 ∥ 𝑥}) → 𝑁 ∥ 𝑚) |
42 | | elrabi 3328 |
. . . . . . 7
⊢ (𝑚 ∈ {𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑁 ∥ 𝑥} → 𝑚 ∈ (1...(⌊‘𝐴))) |
43 | 42 | adantl 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ {𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑁 ∥ 𝑥}) → 𝑚 ∈ (1...(⌊‘𝐴))) |
44 | | elfznn 12241 |
. . . . . 6
⊢ (𝑚 ∈
(1...(⌊‘𝐴))
→ 𝑚 ∈
ℕ) |
45 | 43, 44 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ {𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑁 ∥ 𝑥}) → 𝑚 ∈ ℕ) |
46 | 2 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ {𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑁 ∥ 𝑥}) → 𝑁 ∈ ℕ) |
47 | | nndivdvds 14827 |
. . . . 5
⊢ ((𝑚 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑁 ∥ 𝑚 ↔ (𝑚 / 𝑁) ∈ ℕ)) |
48 | 45, 46, 47 | syl2anc 691 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ {𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑁 ∥ 𝑥}) → (𝑁 ∥ 𝑚 ↔ (𝑚 / 𝑁) ∈ ℕ)) |
49 | 41, 48 | mpbid 221 |
. . 3
⊢ ((𝜑 ∧ 𝑚 ∈ {𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑁 ∥ 𝑥}) → (𝑚 / 𝑁) ∈ ℕ) |
50 | | fznnfl 12523 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ → (𝑚 ∈
(1...(⌊‘𝐴))
↔ (𝑚 ∈ ℕ
∧ 𝑚 ≤ 𝐴))) |
51 | 6, 50 | syl 17 |
. . . . . 6
⊢ (𝜑 → (𝑚 ∈ (1...(⌊‘𝐴)) ↔ (𝑚 ∈ ℕ ∧ 𝑚 ≤ 𝐴))) |
52 | 51 | simplbda 652 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ (1...(⌊‘𝐴))) → 𝑚 ≤ 𝐴) |
53 | 42, 52 | sylan2 490 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ {𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑁 ∥ 𝑥}) → 𝑚 ≤ 𝐴) |
54 | 45 | nnred 10912 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ {𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑁 ∥ 𝑥}) → 𝑚 ∈ ℝ) |
55 | 6 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ {𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑁 ∥ 𝑥}) → 𝐴 ∈ ℝ) |
56 | 14 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ {𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑁 ∥ 𝑥}) → 𝑁 ∈ ℝ) |
57 | 16 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ {𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑁 ∥ 𝑥}) → 0 < 𝑁) |
58 | | lediv1 10767 |
. . . . 5
⊢ ((𝑚 ∈ ℝ ∧ 𝐴 ∈ ℝ ∧ (𝑁 ∈ ℝ ∧ 0 <
𝑁)) → (𝑚 ≤ 𝐴 ↔ (𝑚 / 𝑁) ≤ (𝐴 / 𝑁))) |
59 | 54, 55, 56, 57, 58 | syl112anc 1322 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ {𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑁 ∥ 𝑥}) → (𝑚 ≤ 𝐴 ↔ (𝑚 / 𝑁) ≤ (𝐴 / 𝑁))) |
60 | 53, 59 | mpbid 221 |
. . 3
⊢ ((𝜑 ∧ 𝑚 ∈ {𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑁 ∥ 𝑥}) → (𝑚 / 𝑁) ≤ (𝐴 / 𝑁)) |
61 | 7 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ {𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑁 ∥ 𝑥}) → (𝐴 / 𝑁) ∈ ℝ) |
62 | | fznnfl 12523 |
. . . 4
⊢ ((𝐴 / 𝑁) ∈ ℝ → ((𝑚 / 𝑁) ∈ (1...(⌊‘(𝐴 / 𝑁))) ↔ ((𝑚 / 𝑁) ∈ ℕ ∧ (𝑚 / 𝑁) ≤ (𝐴 / 𝑁)))) |
63 | 61, 62 | syl 17 |
. . 3
⊢ ((𝜑 ∧ 𝑚 ∈ {𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑁 ∥ 𝑥}) → ((𝑚 / 𝑁) ∈ (1...(⌊‘(𝐴 / 𝑁))) ↔ ((𝑚 / 𝑁) ∈ ℕ ∧ (𝑚 / 𝑁) ≤ (𝐴 / 𝑁)))) |
64 | 49, 60, 63 | mpbir2and 959 |
. 2
⊢ ((𝜑 ∧ 𝑚 ∈ {𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑁 ∥ 𝑥}) → (𝑚 / 𝑁) ∈ (1...(⌊‘(𝐴 / 𝑁)))) |
65 | 45 | nncnd 10913 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ {𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑁 ∥ 𝑥}) → 𝑚 ∈ ℂ) |
66 | 65 | adantrl 748 |
. . . 4
⊢ ((𝜑 ∧ (𝑛 ∈ (1...(⌊‘(𝐴 / 𝑁))) ∧ 𝑚 ∈ {𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑁 ∥ 𝑥})) → 𝑚 ∈ ℂ) |
67 | 2 | nncnd 10913 |
. . . . 5
⊢ (𝜑 → 𝑁 ∈ ℂ) |
68 | 67 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ (𝑛 ∈ (1...(⌊‘(𝐴 / 𝑁))) ∧ 𝑚 ∈ {𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑁 ∥ 𝑥})) → 𝑁 ∈ ℂ) |
69 | 11 | nncnd 10913 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘(𝐴 / 𝑁)))) → 𝑛 ∈ ℂ) |
70 | 69 | adantrr 749 |
. . . 4
⊢ ((𝜑 ∧ (𝑛 ∈ (1...(⌊‘(𝐴 / 𝑁))) ∧ 𝑚 ∈ {𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑁 ∥ 𝑥})) → 𝑛 ∈ ℂ) |
71 | 2 | nnne0d 10942 |
. . . . 5
⊢ (𝜑 → 𝑁 ≠ 0) |
72 | 71 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ (𝑛 ∈ (1...(⌊‘(𝐴 / 𝑁))) ∧ 𝑚 ∈ {𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑁 ∥ 𝑥})) → 𝑁 ≠ 0) |
73 | 66, 68, 70, 72 | divmuld 10702 |
. . 3
⊢ ((𝜑 ∧ (𝑛 ∈ (1...(⌊‘(𝐴 / 𝑁))) ∧ 𝑚 ∈ {𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑁 ∥ 𝑥})) → ((𝑚 / 𝑁) = 𝑛 ↔ (𝑁 · 𝑛) = 𝑚)) |
74 | | eqcom 2617 |
. . 3
⊢ (𝑛 = (𝑚 / 𝑁) ↔ (𝑚 / 𝑁) = 𝑛) |
75 | | eqcom 2617 |
. . 3
⊢ (𝑚 = (𝑁 · 𝑛) ↔ (𝑁 · 𝑛) = 𝑚) |
76 | 73, 74, 75 | 3bitr4g 302 |
. 2
⊢ ((𝜑 ∧ (𝑛 ∈ (1...(⌊‘(𝐴 / 𝑁))) ∧ 𝑚 ∈ {𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑁 ∥ 𝑥})) → (𝑛 = (𝑚 / 𝑁) ↔ 𝑚 = (𝑁 · 𝑛))) |
77 | 1, 37, 64, 76 | f1o2d 6785 |
1
⊢ (𝜑 → 𝐹:(1...(⌊‘(𝐴 / 𝑁)))–1-1-onto→{𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑁 ∥ 𝑥}) |