Proof of Theorem moddvds
Step | Hyp | Ref
| Expression |
1 | | nnrp 12597 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℝ+) |
2 | 1 | adantr 484 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ)) → 𝑁 ∈
ℝ+) |
3 | | 0mod 13475 |
. . . . 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 12180 |
. . . . . . 7
⊢ (𝐴 ∈ ℤ → 𝐴 ∈
ℝ) |
7 | 6 | ad2antrl 728 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ)) → 𝐴 ∈
ℝ) |
8 | | zre 12180 |
. . . . . . 7
⊢ (𝐵 ∈ ℤ → 𝐵 ∈
ℝ) |
9 | 8 | ad2antll 729 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ)) → 𝐵 ∈
ℝ) |
10 | 9 | renegcld 11259 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ)) → -𝐵 ∈
ℝ) |
11 | | modadd1 13481 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (-𝐵 ∈ ℝ ∧ 𝑁 ∈ ℝ+)
∧ (𝐴 mod 𝑁) = (𝐵 mod 𝑁)) → ((𝐴 + -𝐵) mod 𝑁) = ((𝐵 + -𝐵) mod 𝑁)) |
12 | 11 | 3expia 1123 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (-𝐵 ∈ ℝ ∧ 𝑁 ∈ ℝ+))
→ ((𝐴 mod 𝑁) = (𝐵 mod 𝑁) → ((𝐴 + -𝐵) mod 𝑁) = ((𝐵 + -𝐵) mod 𝑁))) |
13 | 7, 9, 10, 2, 12 | syl22anc 839 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ)) → ((𝐴 mod 𝑁) = (𝐵 mod 𝑁) → ((𝐴 + -𝐵) mod 𝑁) = ((𝐵 + -𝐵) mod 𝑁))) |
14 | 7 | recnd 10861 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ)) → 𝐴 ∈
ℂ) |
15 | 9 | recnd 10861 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ)) → 𝐵 ∈
ℂ) |
16 | 14, 15 | negsubd 11195 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ)) → (𝐴 + -𝐵) = (𝐴 − 𝐵)) |
17 | 16 | oveq1d 7228 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ)) → ((𝐴 + -𝐵) mod 𝑁) = ((𝐴 − 𝐵) mod 𝑁)) |
18 | 15 | negidd 11179 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ)) → (𝐵 + -𝐵) = 0) |
19 | 18 | oveq1d 7228 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ)) → ((𝐵 + -𝐵) mod 𝑁) = (0 mod 𝑁)) |
20 | 17, 19 | eqeq12d 2753 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ)) →
(((𝐴 + -𝐵) mod 𝑁) = ((𝐵 + -𝐵) mod 𝑁) ↔ ((𝐴 − 𝐵) mod 𝑁) = (0 mod 𝑁))) |
21 | 13, 20 | sylibd 242 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ)) → ((𝐴 mod 𝑁) = (𝐵 mod 𝑁) → ((𝐴 − 𝐵) mod 𝑁) = (0 mod 𝑁))) |
22 | 7, 9 | resubcld 11260 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ)) → (𝐴 − 𝐵) ∈ ℝ) |
23 | | 0red 10836 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ)) → 0
∈ ℝ) |
24 | | modadd1 13481 |
. . . . . . 7
⊢ ((((𝐴 − 𝐵) ∈ ℝ ∧ 0 ∈ ℝ)
∧ (𝐵 ∈ ℝ
∧ 𝑁 ∈
ℝ+) ∧ ((𝐴 − 𝐵) mod 𝑁) = (0 mod 𝑁)) → (((𝐴 − 𝐵) + 𝐵) mod 𝑁) = ((0 + 𝐵) mod 𝑁)) |
25 | 24 | 3expia 1123 |
. . . . . 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 11193 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ)) → ((𝐴 − 𝐵) + 𝐵) = 𝐴) |
28 | 27 | oveq1d 7228 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ)) →
(((𝐴 − 𝐵) + 𝐵) mod 𝑁) = (𝐴 mod 𝑁)) |
29 | 15 | addid2d 11033 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ)) → (0 +
𝐵) = 𝐵) |
30 | 29 | oveq1d 7228 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ)) → ((0 +
𝐵) mod 𝑁) = (𝐵 mod 𝑁)) |
31 | 28, 30 | eqeq12d 2753 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ)) →
((((𝐴 − 𝐵) + 𝐵) mod 𝑁) = ((0 + 𝐵) mod 𝑁) ↔ (𝐴 mod 𝑁) = (𝐵 mod 𝑁))) |
32 | 26, 31 | sylibd 242 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ)) →
(((𝐴 − 𝐵) mod 𝑁) = (0 mod 𝑁) → (𝐴 mod 𝑁) = (𝐵 mod 𝑁))) |
33 | 21, 32 | impbid 215 |
. . 3
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ)) → ((𝐴 mod 𝑁) = (𝐵 mod 𝑁) ↔ ((𝐴 − 𝐵) mod 𝑁) = (0 mod 𝑁))) |
34 | | zsubcl 12219 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 − 𝐵) ∈ ℤ) |
35 | | dvdsval3 15819 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 − 𝐵) ∈ ℤ) → (𝑁 ∥ (𝐴 − 𝐵) ↔ ((𝐴 − 𝐵) mod 𝑁) = 0)) |
36 | 34, 35 | sylan2 596 |
. . 3
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ)) → (𝑁 ∥ (𝐴 − 𝐵) ↔ ((𝐴 − 𝐵) mod 𝑁) = 0)) |
37 | 5, 33, 36 | 3bitr4d 314 |
. 2
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ)) → ((𝐴 mod 𝑁) = (𝐵 mod 𝑁) ↔ 𝑁 ∥ (𝐴 − 𝐵))) |
38 | 37 | 3impb 1117 |
1
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝐴 mod 𝑁) = (𝐵 mod 𝑁) ↔ 𝑁 ∥ (𝐴 − 𝐵))) |