| Step | Hyp | Ref
| Expression |
| 1 | | dvdsflf1o.f |
. 2
⊢ 𝐹 = (𝑛 ∈ (1...(⌊‘(𝐴 / 𝑁))) ↦ (𝑁 · 𝑛)) |
| 2 | | breq2 5147 |
. . 3
⊢ (𝑥 = (𝑁 · 𝑛) → (𝑁 ∥ 𝑥 ↔ 𝑁 ∥ (𝑁 · 𝑛))) |
| 3 | | dvdsflf1o.2 |
. . . . 5
⊢ (𝜑 → 𝑁 ∈ ℕ) |
| 4 | | elfznn 13593 |
. . . . 5
⊢ (𝑛 ∈
(1...(⌊‘(𝐴 /
𝑁))) → 𝑛 ∈
ℕ) |
| 5 | | nnmulcl 12290 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℕ) → (𝑁 · 𝑛) ∈ ℕ) |
| 6 | 3, 4, 5 | syl2an 596 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘(𝐴 / 𝑁)))) → (𝑁 · 𝑛) ∈ ℕ) |
| 7 | | dvdsflf1o.1 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ∈ ℝ) |
| 8 | 7, 3 | nndivred 12320 |
. . . . . . . 8
⊢ (𝜑 → (𝐴 / 𝑁) ∈ ℝ) |
| 9 | | fznnfl 13902 |
. . . . . . . 8
⊢ ((𝐴 / 𝑁) ∈ ℝ → (𝑛 ∈ (1...(⌊‘(𝐴 / 𝑁))) ↔ (𝑛 ∈ ℕ ∧ 𝑛 ≤ (𝐴 / 𝑁)))) |
| 10 | 8, 9 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (𝑛 ∈ (1...(⌊‘(𝐴 / 𝑁))) ↔ (𝑛 ∈ ℕ ∧ 𝑛 ≤ (𝐴 / 𝑁)))) |
| 11 | 10 | simplbda 499 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘(𝐴 / 𝑁)))) → 𝑛 ≤ (𝐴 / 𝑁)) |
| 12 | 4 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘(𝐴 / 𝑁)))) → 𝑛 ∈ ℕ) |
| 13 | 12 | nnred 12281 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘(𝐴 / 𝑁)))) → 𝑛 ∈ ℝ) |
| 14 | 7 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘(𝐴 / 𝑁)))) → 𝐴 ∈ ℝ) |
| 15 | 3 | nnred 12281 |
. . . . . . . 8
⊢ (𝜑 → 𝑁 ∈ ℝ) |
| 16 | 15 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘(𝐴 / 𝑁)))) → 𝑁 ∈ ℝ) |
| 17 | 3 | nngt0d 12315 |
. . . . . . . 8
⊢ (𝜑 → 0 < 𝑁) |
| 18 | 17 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘(𝐴 / 𝑁)))) → 0 < 𝑁) |
| 19 | | lemuldiv2 12149 |
. . . . . . 7
⊢ ((𝑛 ∈ ℝ ∧ 𝐴 ∈ ℝ ∧ (𝑁 ∈ ℝ ∧ 0 <
𝑁)) → ((𝑁 · 𝑛) ≤ 𝐴 ↔ 𝑛 ≤ (𝐴 / 𝑁))) |
| 20 | 13, 14, 16, 18, 19 | syl112anc 1376 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘(𝐴 / 𝑁)))) → ((𝑁 · 𝑛) ≤ 𝐴 ↔ 𝑛 ≤ (𝐴 / 𝑁))) |
| 21 | 11, 20 | mpbird 257 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘(𝐴 / 𝑁)))) → (𝑁 · 𝑛) ≤ 𝐴) |
| 22 | 3 | nnzd 12640 |
. . . . . . 7
⊢ (𝜑 → 𝑁 ∈ ℤ) |
| 23 | | elfzelz 13564 |
. . . . . . 7
⊢ (𝑛 ∈
(1...(⌊‘(𝐴 /
𝑁))) → 𝑛 ∈
ℤ) |
| 24 | | zmulcl 12666 |
. . . . . . 7
⊢ ((𝑁 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (𝑁 · 𝑛) ∈ ℤ) |
| 25 | 22, 23, 24 | syl2an 596 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘(𝐴 / 𝑁)))) → (𝑁 · 𝑛) ∈ ℤ) |
| 26 | | flge 13845 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ (𝑁 · 𝑛) ∈ ℤ) → ((𝑁 · 𝑛) ≤ 𝐴 ↔ (𝑁 · 𝑛) ≤ (⌊‘𝐴))) |
| 27 | 14, 25, 26 | syl2anc 584 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘(𝐴 / 𝑁)))) → ((𝑁 · 𝑛) ≤ 𝐴 ↔ (𝑁 · 𝑛) ≤ (⌊‘𝐴))) |
| 28 | 21, 27 | mpbid 232 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘(𝐴 / 𝑁)))) → (𝑁 · 𝑛) ≤ (⌊‘𝐴)) |
| 29 | 7 | flcld 13838 |
. . . . . 6
⊢ (𝜑 → (⌊‘𝐴) ∈
ℤ) |
| 30 | 29 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘(𝐴 / 𝑁)))) → (⌊‘𝐴) ∈ ℤ) |
| 31 | | fznn 13632 |
. . . . 5
⊢
((⌊‘𝐴)
∈ ℤ → ((𝑁
· 𝑛) ∈
(1...(⌊‘𝐴))
↔ ((𝑁 · 𝑛) ∈ ℕ ∧ (𝑁 · 𝑛) ≤ (⌊‘𝐴)))) |
| 32 | 30, 31 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘(𝐴 / 𝑁)))) → ((𝑁 · 𝑛) ∈ (1...(⌊‘𝐴)) ↔ ((𝑁 · 𝑛) ∈ ℕ ∧ (𝑁 · 𝑛) ≤ (⌊‘𝐴)))) |
| 33 | 6, 28, 32 | mpbir2and 713 |
. . 3
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘(𝐴 / 𝑁)))) → (𝑁 · 𝑛) ∈ (1...(⌊‘𝐴))) |
| 34 | | dvdsmul1 16315 |
. . . 4
⊢ ((𝑁 ∈ ℤ ∧ 𝑛 ∈ ℤ) → 𝑁 ∥ (𝑁 · 𝑛)) |
| 35 | 22, 23, 34 | syl2an 596 |
. . 3
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘(𝐴 / 𝑁)))) → 𝑁 ∥ (𝑁 · 𝑛)) |
| 36 | 2, 33, 35 | elrabd 3694 |
. 2
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘(𝐴 / 𝑁)))) → (𝑁 · 𝑛) ∈ {𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑁 ∥ 𝑥}) |
| 37 | | breq2 5147 |
. . . . . . 7
⊢ (𝑥 = 𝑚 → (𝑁 ∥ 𝑥 ↔ 𝑁 ∥ 𝑚)) |
| 38 | 37 | elrab 3692 |
. . . . . 6
⊢ (𝑚 ∈ {𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑁 ∥ 𝑥} ↔ (𝑚 ∈ (1...(⌊‘𝐴)) ∧ 𝑁 ∥ 𝑚)) |
| 39 | 38 | simprbi 496 |
. . . . 5
⊢ (𝑚 ∈ {𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑁 ∥ 𝑥} → 𝑁 ∥ 𝑚) |
| 40 | 39 | adantl 481 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ {𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑁 ∥ 𝑥}) → 𝑁 ∥ 𝑚) |
| 41 | | elrabi 3687 |
. . . . . . 7
⊢ (𝑚 ∈ {𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑁 ∥ 𝑥} → 𝑚 ∈ (1...(⌊‘𝐴))) |
| 42 | 41 | adantl 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ {𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑁 ∥ 𝑥}) → 𝑚 ∈ (1...(⌊‘𝐴))) |
| 43 | | elfznn 13593 |
. . . . . 6
⊢ (𝑚 ∈
(1...(⌊‘𝐴))
→ 𝑚 ∈
ℕ) |
| 44 | 42, 43 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ {𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑁 ∥ 𝑥}) → 𝑚 ∈ ℕ) |
| 45 | 3 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ {𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑁 ∥ 𝑥}) → 𝑁 ∈ ℕ) |
| 46 | | nndivdvds 16299 |
. . . . 5
⊢ ((𝑚 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑁 ∥ 𝑚 ↔ (𝑚 / 𝑁) ∈ ℕ)) |
| 47 | 44, 45, 46 | syl2anc 584 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ {𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑁 ∥ 𝑥}) → (𝑁 ∥ 𝑚 ↔ (𝑚 / 𝑁) ∈ ℕ)) |
| 48 | 40, 47 | mpbid 232 |
. . 3
⊢ ((𝜑 ∧ 𝑚 ∈ {𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑁 ∥ 𝑥}) → (𝑚 / 𝑁) ∈ ℕ) |
| 49 | | fznnfl 13902 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ → (𝑚 ∈
(1...(⌊‘𝐴))
↔ (𝑚 ∈ ℕ
∧ 𝑚 ≤ 𝐴))) |
| 50 | 7, 49 | syl 17 |
. . . . . 6
⊢ (𝜑 → (𝑚 ∈ (1...(⌊‘𝐴)) ↔ (𝑚 ∈ ℕ ∧ 𝑚 ≤ 𝐴))) |
| 51 | 50 | simplbda 499 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ (1...(⌊‘𝐴))) → 𝑚 ≤ 𝐴) |
| 52 | 41, 51 | sylan2 593 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ {𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑁 ∥ 𝑥}) → 𝑚 ≤ 𝐴) |
| 53 | 44 | nnred 12281 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ {𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑁 ∥ 𝑥}) → 𝑚 ∈ ℝ) |
| 54 | 7 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ {𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑁 ∥ 𝑥}) → 𝐴 ∈ ℝ) |
| 55 | 15 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ {𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑁 ∥ 𝑥}) → 𝑁 ∈ ℝ) |
| 56 | 17 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ {𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑁 ∥ 𝑥}) → 0 < 𝑁) |
| 57 | | lediv1 12133 |
. . . . 5
⊢ ((𝑚 ∈ ℝ ∧ 𝐴 ∈ ℝ ∧ (𝑁 ∈ ℝ ∧ 0 <
𝑁)) → (𝑚 ≤ 𝐴 ↔ (𝑚 / 𝑁) ≤ (𝐴 / 𝑁))) |
| 58 | 53, 54, 55, 56, 57 | syl112anc 1376 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ {𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑁 ∥ 𝑥}) → (𝑚 ≤ 𝐴 ↔ (𝑚 / 𝑁) ≤ (𝐴 / 𝑁))) |
| 59 | 52, 58 | mpbid 232 |
. . 3
⊢ ((𝜑 ∧ 𝑚 ∈ {𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑁 ∥ 𝑥}) → (𝑚 / 𝑁) ≤ (𝐴 / 𝑁)) |
| 60 | 8 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ {𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑁 ∥ 𝑥}) → (𝐴 / 𝑁) ∈ ℝ) |
| 61 | | fznnfl 13902 |
. . . 4
⊢ ((𝐴 / 𝑁) ∈ ℝ → ((𝑚 / 𝑁) ∈ (1...(⌊‘(𝐴 / 𝑁))) ↔ ((𝑚 / 𝑁) ∈ ℕ ∧ (𝑚 / 𝑁) ≤ (𝐴 / 𝑁)))) |
| 62 | 60, 61 | syl 17 |
. . 3
⊢ ((𝜑 ∧ 𝑚 ∈ {𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑁 ∥ 𝑥}) → ((𝑚 / 𝑁) ∈ (1...(⌊‘(𝐴 / 𝑁))) ↔ ((𝑚 / 𝑁) ∈ ℕ ∧ (𝑚 / 𝑁) ≤ (𝐴 / 𝑁)))) |
| 63 | 48, 59, 62 | mpbir2and 713 |
. 2
⊢ ((𝜑 ∧ 𝑚 ∈ {𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑁 ∥ 𝑥}) → (𝑚 / 𝑁) ∈ (1...(⌊‘(𝐴 / 𝑁)))) |
| 64 | 44 | nncnd 12282 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ {𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑁 ∥ 𝑥}) → 𝑚 ∈ ℂ) |
| 65 | 64 | adantrl 716 |
. . . 4
⊢ ((𝜑 ∧ (𝑛 ∈ (1...(⌊‘(𝐴 / 𝑁))) ∧ 𝑚 ∈ {𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑁 ∥ 𝑥})) → 𝑚 ∈ ℂ) |
| 66 | 3 | nncnd 12282 |
. . . . 5
⊢ (𝜑 → 𝑁 ∈ ℂ) |
| 67 | 66 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ (𝑛 ∈ (1...(⌊‘(𝐴 / 𝑁))) ∧ 𝑚 ∈ {𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑁 ∥ 𝑥})) → 𝑁 ∈ ℂ) |
| 68 | 12 | nncnd 12282 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘(𝐴 / 𝑁)))) → 𝑛 ∈ ℂ) |
| 69 | 68 | adantrr 717 |
. . . 4
⊢ ((𝜑 ∧ (𝑛 ∈ (1...(⌊‘(𝐴 / 𝑁))) ∧ 𝑚 ∈ {𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑁 ∥ 𝑥})) → 𝑛 ∈ ℂ) |
| 70 | 3 | nnne0d 12316 |
. . . . 5
⊢ (𝜑 → 𝑁 ≠ 0) |
| 71 | 70 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ (𝑛 ∈ (1...(⌊‘(𝐴 / 𝑁))) ∧ 𝑚 ∈ {𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑁 ∥ 𝑥})) → 𝑁 ≠ 0) |
| 72 | 65, 67, 69, 71 | divmuld 12065 |
. . 3
⊢ ((𝜑 ∧ (𝑛 ∈ (1...(⌊‘(𝐴 / 𝑁))) ∧ 𝑚 ∈ {𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑁 ∥ 𝑥})) → ((𝑚 / 𝑁) = 𝑛 ↔ (𝑁 · 𝑛) = 𝑚)) |
| 73 | | eqcom 2744 |
. . 3
⊢ (𝑛 = (𝑚 / 𝑁) ↔ (𝑚 / 𝑁) = 𝑛) |
| 74 | | eqcom 2744 |
. . 3
⊢ (𝑚 = (𝑁 · 𝑛) ↔ (𝑁 · 𝑛) = 𝑚) |
| 75 | 72, 73, 74 | 3bitr4g 314 |
. 2
⊢ ((𝜑 ∧ (𝑛 ∈ (1...(⌊‘(𝐴 / 𝑁))) ∧ 𝑚 ∈ {𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑁 ∥ 𝑥})) → (𝑛 = (𝑚 / 𝑁) ↔ 𝑚 = (𝑁 · 𝑛))) |
| 76 | 1, 36, 63, 75 | f1o2d 7687 |
1
⊢ (𝜑 → 𝐹:(1...(⌊‘(𝐴 / 𝑁)))–1-1-onto→{𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑁 ∥ 𝑥}) |