| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | zcn 12618 | . . . . . . . . . 10
⊢ (𝐴 ∈ ℤ → 𝐴 ∈
ℂ) | 
| 2 | 1 | mul01d 11460 | . . . . . . . . 9
⊢ (𝐴 ∈ ℤ → (𝐴 · 0) =
0) | 
| 3 | 2 | 3ad2ant1 1134 | . . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → (𝐴 · 0) =
0) | 
| 4 |  | zcn 12618 | . . . . . . . . . 10
⊢ (𝐵 ∈ ℤ → 𝐵 ∈
ℂ) | 
| 5 | 4 | mul01d 11460 | . . . . . . . . 9
⊢ (𝐵 ∈ ℤ → (𝐵 · 0) =
0) | 
| 6 | 5 | 3ad2ant2 1135 | . . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → (𝐵 · 0) =
0) | 
| 7 | 3, 6 | eqtr4d 2780 | . . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → (𝐴 · 0) = (𝐵 · 0)) | 
| 8 | 7 | adantr 480 | . . . . . 6
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) → (𝐴 · 0) = (𝐵 · 0)) | 
| 9 | 8 | oveq1d 7446 | . . . . 5
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) → ((𝐴 · 0) mod 𝑁) = ((𝐵 · 0) mod 𝑁)) | 
| 10 | 9 | adantr 480 | . . . 4
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ (𝐴 mod 𝑀) = (𝐵 mod 𝑀)) → ((𝐴 · 0) mod 𝑁) = ((𝐵 · 0) mod 𝑁)) | 
| 11 |  | oveq2 7439 | . . . . . 6
⊢ (𝐶 = 0 → (𝐴 · 𝐶) = (𝐴 · 0)) | 
| 12 | 11 | oveq1d 7446 | . . . . 5
⊢ (𝐶 = 0 → ((𝐴 · 𝐶) mod 𝑁) = ((𝐴 · 0) mod 𝑁)) | 
| 13 |  | oveq2 7439 | . . . . . 6
⊢ (𝐶 = 0 → (𝐵 · 𝐶) = (𝐵 · 0)) | 
| 14 | 13 | oveq1d 7446 | . . . . 5
⊢ (𝐶 = 0 → ((𝐵 · 𝐶) mod 𝑁) = ((𝐵 · 0) mod 𝑁)) | 
| 15 | 12, 14 | eqeq12d 2753 | . . . 4
⊢ (𝐶 = 0 → (((𝐴 · 𝐶) mod 𝑁) = ((𝐵 · 𝐶) mod 𝑁) ↔ ((𝐴 · 0) mod 𝑁) = ((𝐵 · 0) mod 𝑁))) | 
| 16 | 10, 15 | imbitrrid 246 | . . 3
⊢ (𝐶 = 0 → ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ (𝐴 mod 𝑀) = (𝐵 mod 𝑀)) → ((𝐴 · 𝐶) mod 𝑁) = ((𝐵 · 𝐶) mod 𝑁))) | 
| 17 |  | oveq2 7439 | . . . . . . . . . 10
⊢ (𝑀 = (𝑁 / (𝐶 gcd 𝑁)) → (𝐴 mod 𝑀) = (𝐴 mod (𝑁 / (𝐶 gcd 𝑁)))) | 
| 18 |  | oveq2 7439 | . . . . . . . . . 10
⊢ (𝑀 = (𝑁 / (𝐶 gcd 𝑁)) → (𝐵 mod 𝑀) = (𝐵 mod (𝑁 / (𝐶 gcd 𝑁)))) | 
| 19 | 17, 18 | eqeq12d 2753 | . . . . . . . . 9
⊢ (𝑀 = (𝑁 / (𝐶 gcd 𝑁)) → ((𝐴 mod 𝑀) = (𝐵 mod 𝑀) ↔ (𝐴 mod (𝑁 / (𝐶 gcd 𝑁))) = (𝐵 mod (𝑁 / (𝐶 gcd 𝑁))))) | 
| 20 | 19 | adantl 481 | . . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁))) → ((𝐴 mod 𝑀) = (𝐵 mod 𝑀) ↔ (𝐴 mod (𝑁 / (𝐶 gcd 𝑁))) = (𝐵 mod (𝑁 / (𝐶 gcd 𝑁))))) | 
| 21 | 20 | adantl 481 | . . . . . . 7
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) → ((𝐴 mod 𝑀) = (𝐵 mod 𝑀) ↔ (𝐴 mod (𝑁 / (𝐶 gcd 𝑁))) = (𝐵 mod (𝑁 / (𝐶 gcd 𝑁))))) | 
| 22 |  | simpl 482 | . . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁))) → 𝑁 ∈ ℕ) | 
| 23 |  | simp3 1139 | . . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → 𝐶 ∈
ℤ) | 
| 24 |  | divgcdnnr 16553 | . . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝐶 ∈ ℤ) → (𝑁 / (𝐶 gcd 𝑁)) ∈ ℕ) | 
| 25 | 22, 23, 24 | syl2anr 597 | . . . . . . . 8
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) → (𝑁 / (𝐶 gcd 𝑁)) ∈ ℕ) | 
| 26 |  | simpl1 1192 | . . . . . . . 8
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) → 𝐴 ∈ ℤ) | 
| 27 |  | simpl2 1193 | . . . . . . . 8
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) → 𝐵 ∈ ℤ) | 
| 28 |  | moddvds 16301 | . . . . . . . 8
⊢ (((𝑁 / (𝐶 gcd 𝑁)) ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝐴 mod (𝑁 / (𝐶 gcd 𝑁))) = (𝐵 mod (𝑁 / (𝐶 gcd 𝑁))) ↔ (𝑁 / (𝐶 gcd 𝑁)) ∥ (𝐴 − 𝐵))) | 
| 29 | 25, 26, 27, 28 | syl3anc 1373 | . . . . . . 7
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) → ((𝐴 mod (𝑁 / (𝐶 gcd 𝑁))) = (𝐵 mod (𝑁 / (𝐶 gcd 𝑁))) ↔ (𝑁 / (𝐶 gcd 𝑁)) ∥ (𝐴 − 𝐵))) | 
| 30 | 25 | nnzd 12640 | . . . . . . . . 9
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) → (𝑁 / (𝐶 gcd 𝑁)) ∈ ℤ) | 
| 31 |  | zsubcl 12659 | . . . . . . . . . . 11
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 − 𝐵) ∈ ℤ) | 
| 32 | 31 | 3adant3 1133 | . . . . . . . . . 10
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → (𝐴 − 𝐵) ∈ ℤ) | 
| 33 | 32 | adantr 480 | . . . . . . . . 9
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) → (𝐴 − 𝐵) ∈ ℤ) | 
| 34 | 30, 33 | jca 511 | . . . . . . . 8
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) → ((𝑁 / (𝐶 gcd 𝑁)) ∈ ℤ ∧ (𝐴 − 𝐵) ∈ ℤ)) | 
| 35 |  | divides 16292 | . . . . . . . 8
⊢ (((𝑁 / (𝐶 gcd 𝑁)) ∈ ℤ ∧ (𝐴 − 𝐵) ∈ ℤ) → ((𝑁 / (𝐶 gcd 𝑁)) ∥ (𝐴 − 𝐵) ↔ ∃𝑘 ∈ ℤ (𝑘 · (𝑁 / (𝐶 gcd 𝑁))) = (𝐴 − 𝐵))) | 
| 36 | 34, 35 | syl 17 | . . . . . . 7
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) → ((𝑁 / (𝐶 gcd 𝑁)) ∥ (𝐴 − 𝐵) ↔ ∃𝑘 ∈ ℤ (𝑘 · (𝑁 / (𝐶 gcd 𝑁))) = (𝐴 − 𝐵))) | 
| 37 | 21, 29, 36 | 3bitrd 305 | . . . . . 6
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) → ((𝐴 mod 𝑀) = (𝐵 mod 𝑀) ↔ ∃𝑘 ∈ ℤ (𝑘 · (𝑁 / (𝐶 gcd 𝑁))) = (𝐴 − 𝐵))) | 
| 38 |  | simpr 484 | . . . . . . . . . . . . . . 15
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝐶 ∈
ℤ) ∧ (𝑁 ∈
ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝐶 ≠ 0) ∧ 𝑘 ∈ ℤ) → 𝑘 ∈ ℤ) | 
| 39 | 30 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝐶 ≠ 0) → (𝑁 / (𝐶 gcd 𝑁)) ∈ ℤ) | 
| 40 | 39 | adantr 480 | . . . . . . . . . . . . . . 15
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝐶 ∈
ℤ) ∧ (𝑁 ∈
ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝐶 ≠ 0) ∧ 𝑘 ∈ ℤ) → (𝑁 / (𝐶 gcd 𝑁)) ∈ ℤ) | 
| 41 | 38, 40 | zmulcld 12728 | . . . . . . . . . . . . . 14
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝐶 ∈
ℤ) ∧ (𝑁 ∈
ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝐶 ≠ 0) ∧ 𝑘 ∈ ℤ) → (𝑘 · (𝑁 / (𝐶 gcd 𝑁))) ∈ ℤ) | 
| 42 | 41 | zcnd 12723 | . . . . . . . . . . . . 13
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝐶 ∈
ℤ) ∧ (𝑁 ∈
ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝐶 ≠ 0) ∧ 𝑘 ∈ ℤ) → (𝑘 · (𝑁 / (𝐶 gcd 𝑁))) ∈ ℂ) | 
| 43 | 31 | zcnd 12723 | . . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 − 𝐵) ∈ ℂ) | 
| 44 | 43 | 3adant3 1133 | . . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → (𝐴 − 𝐵) ∈ ℂ) | 
| 45 | 44 | ad3antrrr 730 | . . . . . . . . . . . . 13
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝐶 ∈
ℤ) ∧ (𝑁 ∈
ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝐶 ≠ 0) ∧ 𝑘 ∈ ℤ) → (𝐴 − 𝐵) ∈ ℂ) | 
| 46 | 23 | zcnd 12723 | . . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → 𝐶 ∈
ℂ) | 
| 47 | 46 | ad3antrrr 730 | . . . . . . . . . . . . 13
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝐶 ∈
ℤ) ∧ (𝑁 ∈
ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝐶 ≠ 0) ∧ 𝑘 ∈ ℤ) → 𝐶 ∈ ℂ) | 
| 48 |  | simpr 484 | . . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝐶 ≠ 0) → 𝐶 ≠ 0) | 
| 49 | 48 | adantr 480 | . . . . . . . . . . . . 13
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝐶 ∈
ℤ) ∧ (𝑁 ∈
ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝐶 ≠ 0) ∧ 𝑘 ∈ ℤ) → 𝐶 ≠ 0) | 
| 50 | 42, 45, 47, 49 | mulcan2d 11897 | . . . . . . . . . . . 12
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝐶 ∈
ℤ) ∧ (𝑁 ∈
ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝐶 ≠ 0) ∧ 𝑘 ∈ ℤ) → (((𝑘 · (𝑁 / (𝐶 gcd 𝑁))) · 𝐶) = ((𝐴 − 𝐵) · 𝐶) ↔ (𝑘 · (𝑁 / (𝐶 gcd 𝑁))) = (𝐴 − 𝐵))) | 
| 51 |  | zcn 12618 | . . . . . . . . . . . . . . 15
⊢ (𝐶 ∈ ℤ → 𝐶 ∈
ℂ) | 
| 52 |  | subdir 11697 | . . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − 𝐵) · 𝐶) = ((𝐴 · 𝐶) − (𝐵 · 𝐶))) | 
| 53 | 1, 4, 51, 52 | syl3an 1161 | . . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → ((𝐴 − 𝐵) · 𝐶) = ((𝐴 · 𝐶) − (𝐵 · 𝐶))) | 
| 54 | 53 | ad3antrrr 730 | . . . . . . . . . . . . 13
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝐶 ∈
ℤ) ∧ (𝑁 ∈
ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝐶 ≠ 0) ∧ 𝑘 ∈ ℤ) → ((𝐴 − 𝐵) · 𝐶) = ((𝐴 · 𝐶) − (𝐵 · 𝐶))) | 
| 55 | 54 | eqeq2d 2748 | . . . . . . . . . . . 12
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝐶 ∈
ℤ) ∧ (𝑁 ∈
ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝐶 ≠ 0) ∧ 𝑘 ∈ ℤ) → (((𝑘 · (𝑁 / (𝐶 gcd 𝑁))) · 𝐶) = ((𝐴 − 𝐵) · 𝐶) ↔ ((𝑘 · (𝑁 / (𝐶 gcd 𝑁))) · 𝐶) = ((𝐴 · 𝐶) − (𝐵 · 𝐶)))) | 
| 56 | 50, 55 | bitr3d 281 | . . . . . . . . . . 11
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝐶 ∈
ℤ) ∧ (𝑁 ∈
ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝐶 ≠ 0) ∧ 𝑘 ∈ ℤ) → ((𝑘 · (𝑁 / (𝐶 gcd 𝑁))) = (𝐴 − 𝐵) ↔ ((𝑘 · (𝑁 / (𝐶 gcd 𝑁))) · 𝐶) = ((𝐴 · 𝐶) − (𝐵 · 𝐶)))) | 
| 57 |  | nnz 12634 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℤ) | 
| 58 | 57 | adantr 480 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ ℤ) → 𝑁 ∈
ℤ) | 
| 59 |  | simpr 484 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ ℤ) → 𝑘 ∈
ℤ) | 
| 60 | 59 | zcnd 12723 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ ℤ) → 𝑘 ∈
ℂ) | 
| 61 | 60 | adantl 481 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑘 ∈ ℤ)) → 𝑘 ∈
ℂ) | 
| 62 | 46 | adantr 480 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑘 ∈ ℤ)) → 𝐶 ∈
ℂ) | 
| 63 |  | simpl 482 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ ℤ) → 𝑁 ∈
ℕ) | 
| 64 | 63 | nnzd 12640 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ ℤ) → 𝑁 ∈
ℤ) | 
| 65 | 23, 64 | anim12i 613 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑘 ∈ ℤ)) → (𝐶 ∈ ℤ ∧ 𝑁 ∈
ℤ)) | 
| 66 |  | gcdcl 16543 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐶 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐶 gcd 𝑁) ∈
ℕ0) | 
| 67 | 65, 66 | syl 17 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑘 ∈ ℤ)) → (𝐶 gcd 𝑁) ∈
ℕ0) | 
| 68 | 67 | nn0cnd 12589 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑘 ∈ ℤ)) → (𝐶 gcd 𝑁) ∈ ℂ) | 
| 69 |  | nnne0 12300 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑁 ∈ ℕ → 𝑁 ≠ 0) | 
| 70 | 69 | neneqd 2945 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑁 ∈ ℕ → ¬
𝑁 = 0) | 
| 71 | 70 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ ℤ) → ¬
𝑁 = 0) | 
| 72 | 71 | adantl 481 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑘 ∈ ℤ)) → ¬
𝑁 = 0) | 
| 73 | 72 | intnand 488 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑘 ∈ ℤ)) → ¬
(𝐶 = 0 ∧ 𝑁 = 0)) | 
| 74 |  | gcdeq0 16554 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐶 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝐶 gcd 𝑁) = 0 ↔ (𝐶 = 0 ∧ 𝑁 = 0))) | 
| 75 | 65, 74 | syl 17 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑘 ∈ ℤ)) → ((𝐶 gcd 𝑁) = 0 ↔ (𝐶 = 0 ∧ 𝑁 = 0))) | 
| 76 | 75 | necon3abid 2977 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑘 ∈ ℤ)) → ((𝐶 gcd 𝑁) ≠ 0 ↔ ¬ (𝐶 = 0 ∧ 𝑁 = 0))) | 
| 77 | 73, 76 | mpbird 257 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑘 ∈ ℤ)) → (𝐶 gcd 𝑁) ≠ 0) | 
| 78 | 61, 62, 68, 77 | divassd 12078 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑘 ∈ ℤ)) → ((𝑘 · 𝐶) / (𝐶 gcd 𝑁)) = (𝑘 · (𝐶 / (𝐶 gcd 𝑁)))) | 
| 79 | 59 | adantl 481 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑘 ∈ ℤ)) → 𝑘 ∈
ℤ) | 
| 80 | 57, 69 | jca 511 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑁 ∈ ℕ → (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) | 
| 81 | 80 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ ℤ) → (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) | 
| 82 | 23, 81 | anim12i 613 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑘 ∈ ℤ)) → (𝐶 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0))) | 
| 83 |  | 3anass 1095 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐶 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ↔ (𝐶 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0))) | 
| 84 | 82, 83 | sylibr 234 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑘 ∈ ℤ)) → (𝐶 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) | 
| 85 |  | divgcdz 16548 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐶 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (𝐶 / (𝐶 gcd 𝑁)) ∈ ℤ) | 
| 86 | 84, 85 | syl 17 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑘 ∈ ℤ)) → (𝐶 / (𝐶 gcd 𝑁)) ∈ ℤ) | 
| 87 | 79, 86 | zmulcld 12728 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑘 ∈ ℤ)) → (𝑘 · (𝐶 / (𝐶 gcd 𝑁))) ∈ ℤ) | 
| 88 | 78, 87 | eqeltrd 2841 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑘 ∈ ℤ)) → ((𝑘 · 𝐶) / (𝐶 gcd 𝑁)) ∈ ℤ) | 
| 89 |  | dvdsmul1 16315 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑁 ∈ ℤ ∧ ((𝑘 · 𝐶) / (𝐶 gcd 𝑁)) ∈ ℤ) → 𝑁 ∥ (𝑁 · ((𝑘 · 𝐶) / (𝐶 gcd 𝑁)))) | 
| 90 | 58, 88, 89 | syl2an2 686 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑘 ∈ ℤ)) → 𝑁 ∥ (𝑁 · ((𝑘 · 𝐶) / (𝐶 gcd 𝑁)))) | 
| 91 | 63 | nncnd 12282 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ ℤ) → 𝑁 ∈
ℂ) | 
| 92 | 91 | adantl 481 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑘 ∈ ℤ)) → 𝑁 ∈
ℂ) | 
| 93 |  | divmulasscom 11946 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝑘 ∈ ℂ ∧ 𝑁 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ ((𝐶 gcd 𝑁) ∈ ℂ ∧ (𝐶 gcd 𝑁) ≠ 0)) → ((𝑘 · (𝑁 / (𝐶 gcd 𝑁))) · 𝐶) = (𝑁 · ((𝑘 · 𝐶) / (𝐶 gcd 𝑁)))) | 
| 94 | 61, 92, 62, 68, 77, 93 | syl32anc 1380 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑘 ∈ ℤ)) → ((𝑘 · (𝑁 / (𝐶 gcd 𝑁))) · 𝐶) = (𝑁 · ((𝑘 · 𝐶) / (𝐶 gcd 𝑁)))) | 
| 95 | 90, 94 | breqtrrd 5171 | . . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑘 ∈ ℤ)) → 𝑁 ∥ ((𝑘 · (𝑁 / (𝐶 gcd 𝑁))) · 𝐶)) | 
| 96 | 95 | exp32 420 | . . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → (𝑁 ∈ ℕ → (𝑘 ∈ ℤ → 𝑁 ∥ ((𝑘 · (𝑁 / (𝐶 gcd 𝑁))) · 𝐶)))) | 
| 97 | 96 | adantrd 491 | . . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → ((𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁))) → (𝑘 ∈ ℤ → 𝑁 ∥ ((𝑘 · (𝑁 / (𝐶 gcd 𝑁))) · 𝐶)))) | 
| 98 | 97 | imp 406 | . . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) → (𝑘 ∈ ℤ → 𝑁 ∥ ((𝑘 · (𝑁 / (𝐶 gcd 𝑁))) · 𝐶))) | 
| 99 | 98 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝐶 ≠ 0) → (𝑘 ∈ ℤ → 𝑁 ∥ ((𝑘 · (𝑁 / (𝐶 gcd 𝑁))) · 𝐶))) | 
| 100 | 99 | imp 406 | . . . . . . . . . . . 12
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝐶 ∈
ℤ) ∧ (𝑁 ∈
ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝐶 ≠ 0) ∧ 𝑘 ∈ ℤ) → 𝑁 ∥ ((𝑘 · (𝑁 / (𝐶 gcd 𝑁))) · 𝐶)) | 
| 101 |  | breq2 5147 | . . . . . . . . . . . 12
⊢ (((𝑘 · (𝑁 / (𝐶 gcd 𝑁))) · 𝐶) = ((𝐴 · 𝐶) − (𝐵 · 𝐶)) → (𝑁 ∥ ((𝑘 · (𝑁 / (𝐶 gcd 𝑁))) · 𝐶) ↔ 𝑁 ∥ ((𝐴 · 𝐶) − (𝐵 · 𝐶)))) | 
| 102 | 100, 101 | syl5ibcom 245 | . . . . . . . . . . 11
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝐶 ∈
ℤ) ∧ (𝑁 ∈
ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝐶 ≠ 0) ∧ 𝑘 ∈ ℤ) → (((𝑘 · (𝑁 / (𝐶 gcd 𝑁))) · 𝐶) = ((𝐴 · 𝐶) − (𝐵 · 𝐶)) → 𝑁 ∥ ((𝐴 · 𝐶) − (𝐵 · 𝐶)))) | 
| 103 | 56, 102 | sylbid 240 | . . . . . . . . . 10
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝐶 ∈
ℤ) ∧ (𝑁 ∈
ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝐶 ≠ 0) ∧ 𝑘 ∈ ℤ) → ((𝑘 · (𝑁 / (𝐶 gcd 𝑁))) = (𝐴 − 𝐵) → 𝑁 ∥ ((𝐴 · 𝐶) − (𝐵 · 𝐶)))) | 
| 104 | 103 | rexlimdva 3155 | . . . . . . . . 9
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝐶 ≠ 0) → (∃𝑘 ∈ ℤ (𝑘 · (𝑁 / (𝐶 gcd 𝑁))) = (𝐴 − 𝐵) → 𝑁 ∥ ((𝐴 · 𝐶) − (𝐵 · 𝐶)))) | 
| 105 | 22 | adantl 481 | . . . . . . . . . . 11
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) → 𝑁 ∈ ℕ) | 
| 106 |  | zmulcl 12666 | . . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℤ ∧ 𝐶 ∈ ℤ) → (𝐴 · 𝐶) ∈ ℤ) | 
| 107 | 106 | 3adant2 1132 | . . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → (𝐴 · 𝐶) ∈ ℤ) | 
| 108 | 107 | adantr 480 | . . . . . . . . . . 11
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) → (𝐴 · 𝐶) ∈ ℤ) | 
| 109 |  | zmulcl 12666 | . . . . . . . . . . . . 13
⊢ ((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → (𝐵 · 𝐶) ∈ ℤ) | 
| 110 | 109 | 3adant1 1131 | . . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → (𝐵 · 𝐶) ∈ ℤ) | 
| 111 | 110 | adantr 480 | . . . . . . . . . . 11
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) → (𝐵 · 𝐶) ∈ ℤ) | 
| 112 |  | moddvds 16301 | . . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 · 𝐶) ∈ ℤ ∧ (𝐵 · 𝐶) ∈ ℤ) → (((𝐴 · 𝐶) mod 𝑁) = ((𝐵 · 𝐶) mod 𝑁) ↔ 𝑁 ∥ ((𝐴 · 𝐶) − (𝐵 · 𝐶)))) | 
| 113 | 105, 108,
111, 112 | syl3anc 1373 | . . . . . . . . . 10
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) → (((𝐴 · 𝐶) mod 𝑁) = ((𝐵 · 𝐶) mod 𝑁) ↔ 𝑁 ∥ ((𝐴 · 𝐶) − (𝐵 · 𝐶)))) | 
| 114 | 113 | adantr 480 | . . . . . . . . 9
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝐶 ≠ 0) → (((𝐴 · 𝐶) mod 𝑁) = ((𝐵 · 𝐶) mod 𝑁) ↔ 𝑁 ∥ ((𝐴 · 𝐶) − (𝐵 · 𝐶)))) | 
| 115 | 104, 114 | sylibrd 259 | . . . . . . . 8
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝐶 ≠ 0) → (∃𝑘 ∈ ℤ (𝑘 · (𝑁 / (𝐶 gcd 𝑁))) = (𝐴 − 𝐵) → ((𝐴 · 𝐶) mod 𝑁) = ((𝐵 · 𝐶) mod 𝑁))) | 
| 116 | 115 | ex 412 | . . . . . . 7
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) → (𝐶 ≠ 0 → (∃𝑘 ∈ ℤ (𝑘 · (𝑁 / (𝐶 gcd 𝑁))) = (𝐴 − 𝐵) → ((𝐴 · 𝐶) mod 𝑁) = ((𝐵 · 𝐶) mod 𝑁)))) | 
| 117 | 116 | com23 86 | . . . . . 6
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) → (∃𝑘 ∈ ℤ (𝑘 · (𝑁 / (𝐶 gcd 𝑁))) = (𝐴 − 𝐵) → (𝐶 ≠ 0 → ((𝐴 · 𝐶) mod 𝑁) = ((𝐵 · 𝐶) mod 𝑁)))) | 
| 118 | 37, 117 | sylbid 240 | . . . . 5
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) → ((𝐴 mod 𝑀) = (𝐵 mod 𝑀) → (𝐶 ≠ 0 → ((𝐴 · 𝐶) mod 𝑁) = ((𝐵 · 𝐶) mod 𝑁)))) | 
| 119 | 118 | imp 406 | . . . 4
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ (𝐴 mod 𝑀) = (𝐵 mod 𝑀)) → (𝐶 ≠ 0 → ((𝐴 · 𝐶) mod 𝑁) = ((𝐵 · 𝐶) mod 𝑁))) | 
| 120 | 119 | com12 32 | . . 3
⊢ (𝐶 ≠ 0 → ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ (𝐴 mod 𝑀) = (𝐵 mod 𝑀)) → ((𝐴 · 𝐶) mod 𝑁) = ((𝐵 · 𝐶) mod 𝑁))) | 
| 121 | 16, 120 | pm2.61ine 3025 | . 2
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ (𝐴 mod 𝑀) = (𝐵 mod 𝑀)) → ((𝐴 · 𝐶) mod 𝑁) = ((𝐵 · 𝐶) mod 𝑁)) | 
| 122 | 121 | ex 412 | 1
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) → ((𝐴 mod 𝑀) = (𝐵 mod 𝑀) → ((𝐴 · 𝐶) mod 𝑁) = ((𝐵 · 𝐶) mod 𝑁))) |