Proof of Theorem moddvds
| Step | Hyp | Ref
| Expression |
| 1 | | nnrp 13046 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℝ+) |
| 2 | 1 | adantr 480 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ)) → 𝑁 ∈
ℝ+) |
| 3 | | 0mod 13942 |
. . . . 5
⊢ (𝑁 ∈ ℝ+
→ (0 mod 𝑁) =
0) |
| 4 | 2, 3 | syl 17 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ)) → (0 mod
𝑁) = 0) |
| 5 | 4 | eqeq2d 2748 |
. . 3
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ)) →
(((𝐴 − 𝐵) mod 𝑁) = (0 mod 𝑁) ↔ ((𝐴 − 𝐵) mod 𝑁) = 0)) |
| 6 | | zre 12617 |
. . . . . . 7
⊢ (𝐴 ∈ ℤ → 𝐴 ∈
ℝ) |
| 7 | 6 | ad2antrl 728 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ)) → 𝐴 ∈
ℝ) |
| 8 | | zre 12617 |
. . . . . . 7
⊢ (𝐵 ∈ ℤ → 𝐵 ∈
ℝ) |
| 9 | 8 | ad2antll 729 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ)) → 𝐵 ∈
ℝ) |
| 10 | 9 | renegcld 11690 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ)) → -𝐵 ∈
ℝ) |
| 11 | | modadd1 13948 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (-𝐵 ∈ ℝ ∧ 𝑁 ∈ ℝ+)
∧ (𝐴 mod 𝑁) = (𝐵 mod 𝑁)) → ((𝐴 + -𝐵) mod 𝑁) = ((𝐵 + -𝐵) mod 𝑁)) |
| 12 | 11 | 3expia 1122 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (-𝐵 ∈ ℝ ∧ 𝑁 ∈ ℝ+))
→ ((𝐴 mod 𝑁) = (𝐵 mod 𝑁) → ((𝐴 + -𝐵) mod 𝑁) = ((𝐵 + -𝐵) mod 𝑁))) |
| 13 | 7, 9, 10, 2, 12 | syl22anc 839 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ)) → ((𝐴 mod 𝑁) = (𝐵 mod 𝑁) → ((𝐴 + -𝐵) mod 𝑁) = ((𝐵 + -𝐵) mod 𝑁))) |
| 14 | 7 | recnd 11289 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ)) → 𝐴 ∈
ℂ) |
| 15 | 9 | recnd 11289 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ)) → 𝐵 ∈
ℂ) |
| 16 | 14, 15 | negsubd 11626 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ)) → (𝐴 + -𝐵) = (𝐴 − 𝐵)) |
| 17 | 16 | oveq1d 7446 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ)) → ((𝐴 + -𝐵) mod 𝑁) = ((𝐴 − 𝐵) mod 𝑁)) |
| 18 | 15 | negidd 11610 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ)) → (𝐵 + -𝐵) = 0) |
| 19 | 18 | oveq1d 7446 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ)) → ((𝐵 + -𝐵) mod 𝑁) = (0 mod 𝑁)) |
| 20 | 17, 19 | eqeq12d 2753 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ)) →
(((𝐴 + -𝐵) mod 𝑁) = ((𝐵 + -𝐵) mod 𝑁) ↔ ((𝐴 − 𝐵) mod 𝑁) = (0 mod 𝑁))) |
| 21 | 13, 20 | sylibd 239 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ)) → ((𝐴 mod 𝑁) = (𝐵 mod 𝑁) → ((𝐴 − 𝐵) mod 𝑁) = (0 mod 𝑁))) |
| 22 | 7, 9 | resubcld 11691 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ)) → (𝐴 − 𝐵) ∈ ℝ) |
| 23 | | 0red 11264 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ)) → 0
∈ ℝ) |
| 24 | | modadd1 13948 |
. . . . . . 7
⊢ ((((𝐴 − 𝐵) ∈ ℝ ∧ 0 ∈ ℝ)
∧ (𝐵 ∈ ℝ
∧ 𝑁 ∈
ℝ+) ∧ ((𝐴 − 𝐵) mod 𝑁) = (0 mod 𝑁)) → (((𝐴 − 𝐵) + 𝐵) mod 𝑁) = ((0 + 𝐵) mod 𝑁)) |
| 25 | 24 | 3expia 1122 |
. . . . . 6
⊢ ((((𝐴 − 𝐵) ∈ ℝ ∧ 0 ∈ ℝ)
∧ (𝐵 ∈ ℝ
∧ 𝑁 ∈
ℝ+)) → (((𝐴 − 𝐵) mod 𝑁) = (0 mod 𝑁) → (((𝐴 − 𝐵) + 𝐵) mod 𝑁) = ((0 + 𝐵) mod 𝑁))) |
| 26 | 22, 23, 9, 2, 25 | syl22anc 839 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ)) →
(((𝐴 − 𝐵) mod 𝑁) = (0 mod 𝑁) → (((𝐴 − 𝐵) + 𝐵) mod 𝑁) = ((0 + 𝐵) mod 𝑁))) |
| 27 | 14, 15 | npcand 11624 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ)) → ((𝐴 − 𝐵) + 𝐵) = 𝐴) |
| 28 | 27 | oveq1d 7446 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ)) →
(((𝐴 − 𝐵) + 𝐵) mod 𝑁) = (𝐴 mod 𝑁)) |
| 29 | 15 | addlidd 11462 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ)) → (0 +
𝐵) = 𝐵) |
| 30 | 29 | oveq1d 7446 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ)) → ((0 +
𝐵) mod 𝑁) = (𝐵 mod 𝑁)) |
| 31 | 28, 30 | eqeq12d 2753 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ)) →
((((𝐴 − 𝐵) + 𝐵) mod 𝑁) = ((0 + 𝐵) mod 𝑁) ↔ (𝐴 mod 𝑁) = (𝐵 mod 𝑁))) |
| 32 | 26, 31 | sylibd 239 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ)) →
(((𝐴 − 𝐵) mod 𝑁) = (0 mod 𝑁) → (𝐴 mod 𝑁) = (𝐵 mod 𝑁))) |
| 33 | 21, 32 | impbid 212 |
. . 3
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ)) → ((𝐴 mod 𝑁) = (𝐵 mod 𝑁) ↔ ((𝐴 − 𝐵) mod 𝑁) = (0 mod 𝑁))) |
| 34 | | zsubcl 12659 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 − 𝐵) ∈ ℤ) |
| 35 | | dvdsval3 16294 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 − 𝐵) ∈ ℤ) → (𝑁 ∥ (𝐴 − 𝐵) ↔ ((𝐴 − 𝐵) mod 𝑁) = 0)) |
| 36 | 34, 35 | sylan2 593 |
. . 3
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ)) → (𝑁 ∥ (𝐴 − 𝐵) ↔ ((𝐴 − 𝐵) mod 𝑁) = 0)) |
| 37 | 5, 33, 36 | 3bitr4d 311 |
. 2
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ)) → ((𝐴 mod 𝑁) = (𝐵 mod 𝑁) ↔ 𝑁 ∥ (𝐴 − 𝐵))) |
| 38 | 37 | 3impb 1115 |
1
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝐴 mod 𝑁) = (𝐵 mod 𝑁) ↔ 𝑁 ∥ (𝐴 − 𝐵))) |