Proof of Theorem dvdsmod
Step | Hyp | Ref
| Expression |
1 | | simpl3 1059 |
. . . . 5
⊢ (((𝑃 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ) ∧ 𝑃 ∥ 𝑁) → 𝐾 ∈ ℤ) |
2 | 1 | zred 11358 |
. . . 4
⊢ (((𝑃 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ) ∧ 𝑃 ∥ 𝑁) → 𝐾 ∈ ℝ) |
3 | | simpl2 1058 |
. . . . 5
⊢ (((𝑃 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ) ∧ 𝑃 ∥ 𝑁) → 𝑁 ∈ ℕ) |
4 | 3 | nnrpd 11746 |
. . . 4
⊢ (((𝑃 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ) ∧ 𝑃 ∥ 𝑁) → 𝑁 ∈
ℝ+) |
5 | | modval 12532 |
. . . 4
⊢ ((𝐾 ∈ ℝ ∧ 𝑁 ∈ ℝ+)
→ (𝐾 mod 𝑁) = (𝐾 − (𝑁 · (⌊‘(𝐾 / 𝑁))))) |
6 | 2, 4, 5 | syl2anc 691 |
. . 3
⊢ (((𝑃 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ) ∧ 𝑃 ∥ 𝑁) → (𝐾 mod 𝑁) = (𝐾 − (𝑁 · (⌊‘(𝐾 / 𝑁))))) |
7 | 6 | breq2d 4595 |
. 2
⊢ (((𝑃 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ) ∧ 𝑃 ∥ 𝑁) → (𝑃 ∥ (𝐾 mod 𝑁) ↔ 𝑃 ∥ (𝐾 − (𝑁 · (⌊‘(𝐾 / 𝑁)))))) |
8 | | simpr 476 |
. . . . . . 7
⊢ (((𝑃 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ) ∧ 𝑃 ∥ 𝑁) → 𝑃 ∥ 𝑁) |
9 | | simpl1 1057 |
. . . . . . . . 9
⊢ (((𝑃 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ) ∧ 𝑃 ∥ 𝑁) → 𝑃 ∈ ℕ) |
10 | 9 | nnzd 11357 |
. . . . . . . 8
⊢ (((𝑃 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ) ∧ 𝑃 ∥ 𝑁) → 𝑃 ∈ ℤ) |
11 | 3 | nnzd 11357 |
. . . . . . . 8
⊢ (((𝑃 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ) ∧ 𝑃 ∥ 𝑁) → 𝑁 ∈ ℤ) |
12 | 2, 3 | nndivred 10946 |
. . . . . . . . 9
⊢ (((𝑃 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ) ∧ 𝑃 ∥ 𝑁) → (𝐾 / 𝑁) ∈ ℝ) |
13 | 12 | flcld 12461 |
. . . . . . . 8
⊢ (((𝑃 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ) ∧ 𝑃 ∥ 𝑁) → (⌊‘(𝐾 / 𝑁)) ∈ ℤ) |
14 | | dvdsmultr1 14857 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧
(⌊‘(𝐾 / 𝑁)) ∈ ℤ) → (𝑃 ∥ 𝑁 → 𝑃 ∥ (𝑁 · (⌊‘(𝐾 / 𝑁))))) |
15 | 10, 11, 13, 14 | syl3anc 1318 |
. . . . . . 7
⊢ (((𝑃 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ) ∧ 𝑃 ∥ 𝑁) → (𝑃 ∥ 𝑁 → 𝑃 ∥ (𝑁 · (⌊‘(𝐾 / 𝑁))))) |
16 | 8, 15 | mpd 15 |
. . . . . 6
⊢ (((𝑃 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ) ∧ 𝑃 ∥ 𝑁) → 𝑃 ∥ (𝑁 · (⌊‘(𝐾 / 𝑁)))) |
17 | 11, 13 | zmulcld 11364 |
. . . . . . . 8
⊢ (((𝑃 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ) ∧ 𝑃 ∥ 𝑁) → (𝑁 · (⌊‘(𝐾 / 𝑁))) ∈ ℤ) |
18 | 17 | zcnd 11359 |
. . . . . . 7
⊢ (((𝑃 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ) ∧ 𝑃 ∥ 𝑁) → (𝑁 · (⌊‘(𝐾 / 𝑁))) ∈ ℂ) |
19 | 18 | subid1d 10260 |
. . . . . 6
⊢ (((𝑃 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ) ∧ 𝑃 ∥ 𝑁) → ((𝑁 · (⌊‘(𝐾 / 𝑁))) − 0) = (𝑁 · (⌊‘(𝐾 / 𝑁)))) |
20 | 16, 19 | breqtrrd 4611 |
. . . . 5
⊢ (((𝑃 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ) ∧ 𝑃 ∥ 𝑁) → 𝑃 ∥ ((𝑁 · (⌊‘(𝐾 / 𝑁))) − 0)) |
21 | | 0zd 11266 |
. . . . . 6
⊢ (((𝑃 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ) ∧ 𝑃 ∥ 𝑁) → 0 ∈ ℤ) |
22 | | moddvds 14829 |
. . . . . 6
⊢ ((𝑃 ∈ ℕ ∧ (𝑁 · (⌊‘(𝐾 / 𝑁))) ∈ ℤ ∧ 0 ∈ ℤ)
→ (((𝑁 ·
(⌊‘(𝐾 / 𝑁))) mod 𝑃) = (0 mod 𝑃) ↔ 𝑃 ∥ ((𝑁 · (⌊‘(𝐾 / 𝑁))) − 0))) |
23 | 9, 17, 21, 22 | syl3anc 1318 |
. . . . 5
⊢ (((𝑃 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ) ∧ 𝑃 ∥ 𝑁) → (((𝑁 · (⌊‘(𝐾 / 𝑁))) mod 𝑃) = (0 mod 𝑃) ↔ 𝑃 ∥ ((𝑁 · (⌊‘(𝐾 / 𝑁))) − 0))) |
24 | 20, 23 | mpbird 246 |
. . . 4
⊢ (((𝑃 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ) ∧ 𝑃 ∥ 𝑁) → ((𝑁 · (⌊‘(𝐾 / 𝑁))) mod 𝑃) = (0 mod 𝑃)) |
25 | 24 | eqeq2d 2620 |
. . 3
⊢ (((𝑃 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ) ∧ 𝑃 ∥ 𝑁) → ((𝐾 mod 𝑃) = ((𝑁 · (⌊‘(𝐾 / 𝑁))) mod 𝑃) ↔ (𝐾 mod 𝑃) = (0 mod 𝑃))) |
26 | | moddvds 14829 |
. . . 4
⊢ ((𝑃 ∈ ℕ ∧ 𝐾 ∈ ℤ ∧ (𝑁 · (⌊‘(𝐾 / 𝑁))) ∈ ℤ) → ((𝐾 mod 𝑃) = ((𝑁 · (⌊‘(𝐾 / 𝑁))) mod 𝑃) ↔ 𝑃 ∥ (𝐾 − (𝑁 · (⌊‘(𝐾 / 𝑁)))))) |
27 | 9, 1, 17, 26 | syl3anc 1318 |
. . 3
⊢ (((𝑃 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ) ∧ 𝑃 ∥ 𝑁) → ((𝐾 mod 𝑃) = ((𝑁 · (⌊‘(𝐾 / 𝑁))) mod 𝑃) ↔ 𝑃 ∥ (𝐾 − (𝑁 · (⌊‘(𝐾 / 𝑁)))))) |
28 | | moddvds 14829 |
. . . 4
⊢ ((𝑃 ∈ ℕ ∧ 𝐾 ∈ ℤ ∧ 0 ∈
ℤ) → ((𝐾 mod
𝑃) = (0 mod 𝑃) ↔ 𝑃 ∥ (𝐾 − 0))) |
29 | 9, 1, 21, 28 | syl3anc 1318 |
. . 3
⊢ (((𝑃 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ) ∧ 𝑃 ∥ 𝑁) → ((𝐾 mod 𝑃) = (0 mod 𝑃) ↔ 𝑃 ∥ (𝐾 − 0))) |
30 | 25, 27, 29 | 3bitr3d 297 |
. 2
⊢ (((𝑃 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ) ∧ 𝑃 ∥ 𝑁) → (𝑃 ∥ (𝐾 − (𝑁 · (⌊‘(𝐾 / 𝑁)))) ↔ 𝑃 ∥ (𝐾 − 0))) |
31 | 1 | zcnd 11359 |
. . . 4
⊢ (((𝑃 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ) ∧ 𝑃 ∥ 𝑁) → 𝐾 ∈ ℂ) |
32 | 31 | subid1d 10260 |
. . 3
⊢ (((𝑃 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ) ∧ 𝑃 ∥ 𝑁) → (𝐾 − 0) = 𝐾) |
33 | 32 | breq2d 4595 |
. 2
⊢ (((𝑃 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ) ∧ 𝑃 ∥ 𝑁) → (𝑃 ∥ (𝐾 − 0) ↔ 𝑃 ∥ 𝐾)) |
34 | 7, 30, 33 | 3bitrd 293 |
1
⊢ (((𝑃 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ) ∧ 𝑃 ∥ 𝑁) → (𝑃 ∥ (𝐾 mod 𝑁) ↔ 𝑃 ∥ 𝐾)) |