Step | Hyp | Ref
| Expression |
1 | | zmulcl 9225 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝐶 ∈ ℤ) → (𝐴 · 𝐶) ∈ ℤ) |
2 | 1 | 3adant2 1001 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → (𝐴 · 𝐶) ∈ ℤ) |
3 | | zmulcl 9225 |
. . . 4
⊢ ((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → (𝐵 · 𝐶) ∈ ℤ) |
4 | 3 | 3adant1 1000 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → (𝐵 · 𝐶) ∈ ℤ) |
5 | | simpl 108 |
. . 3
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁))) → 𝑁 ∈ ℕ) |
6 | | congr 11992 |
. . 3
⊢ (((𝐴 · 𝐶) ∈ ℤ ∧ (𝐵 · 𝐶) ∈ ℤ ∧ 𝑁 ∈ ℕ) → (((𝐴 · 𝐶) mod 𝑁) = ((𝐵 · 𝐶) mod 𝑁) ↔ ∃𝑘 ∈ ℤ (𝑘 · 𝑁) = ((𝐴 · 𝐶) − (𝐵 · 𝐶)))) |
7 | 2, 4, 5, 6 | syl2an3an 1280 |
. 2
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) → (((𝐴 · 𝐶) mod 𝑁) = ((𝐵 · 𝐶) mod 𝑁) ↔ ∃𝑘 ∈ ℤ (𝑘 · 𝑁) = ((𝐴 · 𝐶) − (𝐵 · 𝐶)))) |
8 | | simpl 108 |
. . . . . . . . . . . 12
⊢ ((𝐶 ∈ ℤ ∧ 𝑁 ∈ ℕ) → 𝐶 ∈
ℤ) |
9 | | nnz 9191 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℤ) |
10 | | nnne0 8866 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℕ → 𝑁 ≠ 0) |
11 | 9, 10 | jca 304 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ → (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) |
12 | 11 | adantl 275 |
. . . . . . . . . . . 12
⊢ ((𝐶 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) |
13 | | eqidd 2158 |
. . . . . . . . . . . 12
⊢ ((𝐶 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝐶 gcd 𝑁) = (𝐶 gcd 𝑁)) |
14 | 8, 12, 13 | 3jca 1162 |
. . . . . . . . . . 11
⊢ ((𝐶 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝐶 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐶 gcd 𝑁) = (𝐶 gcd 𝑁))) |
15 | 14 | ex 114 |
. . . . . . . . . 10
⊢ (𝐶 ∈ ℤ → (𝑁 ∈ ℕ → (𝐶 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐶 gcd 𝑁) = (𝐶 gcd 𝑁)))) |
16 | 15 | 3ad2ant3 1005 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → (𝑁 ∈ ℕ → (𝐶 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐶 gcd 𝑁) = (𝐶 gcd 𝑁)))) |
17 | 16 | com12 30 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → (𝐶 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐶 gcd 𝑁) = (𝐶 gcd 𝑁)))) |
18 | 17 | adantr 274 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁))) → ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → (𝐶 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐶 gcd 𝑁) = (𝐶 gcd 𝑁)))) |
19 | 18 | impcom 124 |
. . . . . 6
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) → (𝐶 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐶 gcd 𝑁) = (𝐶 gcd 𝑁))) |
20 | | divgcdcoprmex 11994 |
. . . . . 6
⊢ ((𝐶 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝐶 gcd 𝑁) = (𝐶 gcd 𝑁)) → ∃𝑟 ∈ ℤ ∃𝑠 ∈ ℤ (𝐶 = ((𝐶 gcd 𝑁) · 𝑟) ∧ 𝑁 = ((𝐶 gcd 𝑁) · 𝑠) ∧ (𝑟 gcd 𝑠) = 1)) |
21 | 19, 20 | syl 14 |
. . . . 5
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) → ∃𝑟 ∈ ℤ ∃𝑠 ∈ ℤ (𝐶 = ((𝐶 gcd 𝑁) · 𝑟) ∧ 𝑁 = ((𝐶 gcd 𝑁) · 𝑠) ∧ (𝑟 gcd 𝑠) = 1)) |
22 | 21 | adantr 274 |
. . . 4
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) → ∃𝑟 ∈ ℤ ∃𝑠 ∈ ℤ (𝐶 = ((𝐶 gcd 𝑁) · 𝑟) ∧ 𝑁 = ((𝐶 gcd 𝑁) · 𝑠) ∧ (𝑟 gcd 𝑠) = 1)) |
23 | | oveq2 5834 |
. . . . . . . . . 10
⊢ (𝑁 = ((𝐶 gcd 𝑁) · 𝑠) → (𝑘 · 𝑁) = (𝑘 · ((𝐶 gcd 𝑁) · 𝑠))) |
24 | 23 | 3ad2ant2 1004 |
. . . . . . . . 9
⊢ ((𝐶 = ((𝐶 gcd 𝑁) · 𝑟) ∧ 𝑁 = ((𝐶 gcd 𝑁) · 𝑠) ∧ (𝑟 gcd 𝑠) = 1) → (𝑘 · 𝑁) = (𝑘 · ((𝐶 gcd 𝑁) · 𝑠))) |
25 | 24 | adantl 275 |
. . . . . . . 8
⊢
((((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝐶 ∈
ℤ) ∧ (𝑁 ∈
ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ (𝐶 = ((𝐶 gcd 𝑁) · 𝑟) ∧ 𝑁 = ((𝐶 gcd 𝑁) · 𝑠) ∧ (𝑟 gcd 𝑠) = 1)) → (𝑘 · 𝑁) = (𝑘 · ((𝐶 gcd 𝑁) · 𝑠))) |
26 | | oveq2 5834 |
. . . . . . . . . . 11
⊢ (𝐶 = ((𝐶 gcd 𝑁) · 𝑟) → (𝐴 · 𝐶) = (𝐴 · ((𝐶 gcd 𝑁) · 𝑟))) |
27 | | oveq2 5834 |
. . . . . . . . . . 11
⊢ (𝐶 = ((𝐶 gcd 𝑁) · 𝑟) → (𝐵 · 𝐶) = (𝐵 · ((𝐶 gcd 𝑁) · 𝑟))) |
28 | 26, 27 | oveq12d 5844 |
. . . . . . . . . 10
⊢ (𝐶 = ((𝐶 gcd 𝑁) · 𝑟) → ((𝐴 · 𝐶) − (𝐵 · 𝐶)) = ((𝐴 · ((𝐶 gcd 𝑁) · 𝑟)) − (𝐵 · ((𝐶 gcd 𝑁) · 𝑟)))) |
29 | 28 | 3ad2ant1 1003 |
. . . . . . . . 9
⊢ ((𝐶 = ((𝐶 gcd 𝑁) · 𝑟) ∧ 𝑁 = ((𝐶 gcd 𝑁) · 𝑠) ∧ (𝑟 gcd 𝑠) = 1) → ((𝐴 · 𝐶) − (𝐵 · 𝐶)) = ((𝐴 · ((𝐶 gcd 𝑁) · 𝑟)) − (𝐵 · ((𝐶 gcd 𝑁) · 𝑟)))) |
30 | 29 | adantl 275 |
. . . . . . . 8
⊢
((((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝐶 ∈
ℤ) ∧ (𝑁 ∈
ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ (𝐶 = ((𝐶 gcd 𝑁) · 𝑟) ∧ 𝑁 = ((𝐶 gcd 𝑁) · 𝑠) ∧ (𝑟 gcd 𝑠) = 1)) → ((𝐴 · 𝐶) − (𝐵 · 𝐶)) = ((𝐴 · ((𝐶 gcd 𝑁) · 𝑟)) − (𝐵 · ((𝐶 gcd 𝑁) · 𝑟)))) |
31 | 25, 30 | eqeq12d 2172 |
. . . . . . 7
⊢
((((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝐶 ∈
ℤ) ∧ (𝑁 ∈
ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ (𝐶 = ((𝐶 gcd 𝑁) · 𝑟) ∧ 𝑁 = ((𝐶 gcd 𝑁) · 𝑠) ∧ (𝑟 gcd 𝑠) = 1)) → ((𝑘 · 𝑁) = ((𝐴 · 𝐶) − (𝐵 · 𝐶)) ↔ (𝑘 · ((𝐶 gcd 𝑁) · 𝑠)) = ((𝐴 · ((𝐶 gcd 𝑁) · 𝑟)) − (𝐵 · ((𝐶 gcd 𝑁) · 𝑟))))) |
32 | | simpr 109 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) → 𝑘 ∈ ℤ) |
33 | 32 | zcnd 9292 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) → 𝑘 ∈ ℂ) |
34 | 33 | adantr 274 |
. . . . . . . . . . . 12
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝐶 ∈
ℤ) ∧ (𝑁 ∈
ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → 𝑘 ∈ ℂ) |
35 | | simp3 984 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → 𝐶 ∈
ℤ) |
36 | 35 | adantr 274 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) → 𝐶 ∈ ℤ) |
37 | 9 | ad2antrl 482 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) → 𝑁 ∈ ℤ) |
38 | 36, 37 | gcdcld 11867 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) → (𝐶 gcd 𝑁) ∈
ℕ0) |
39 | 38 | nn0cnd 9150 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) → (𝐶 gcd 𝑁) ∈ ℂ) |
40 | 39 | ad2antrr 480 |
. . . . . . . . . . . 12
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝐶 ∈
ℤ) ∧ (𝑁 ∈
ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → (𝐶 gcd 𝑁) ∈ ℂ) |
41 | | simpr 109 |
. . . . . . . . . . . . . 14
⊢ ((𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ) → 𝑠 ∈
ℤ) |
42 | 41 | zcnd 9292 |
. . . . . . . . . . . . 13
⊢ ((𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ) → 𝑠 ∈
ℂ) |
43 | 42 | adantl 275 |
. . . . . . . . . . . 12
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝐶 ∈
ℤ) ∧ (𝑁 ∈
ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → 𝑠 ∈ ℂ) |
44 | 34, 40, 43 | mul12d 8031 |
. . . . . . . . . . 11
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝐶 ∈
ℤ) ∧ (𝑁 ∈
ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → (𝑘 · ((𝐶 gcd 𝑁) · 𝑠)) = ((𝐶 gcd 𝑁) · (𝑘 · 𝑠))) |
45 | | simp1 982 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → 𝐴 ∈
ℤ) |
46 | 45 | zcnd 9292 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → 𝐴 ∈
ℂ) |
47 | 46 | ad3antrrr 484 |
. . . . . . . . . . . . 13
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝐶 ∈
ℤ) ∧ (𝑁 ∈
ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → 𝐴 ∈ ℂ) |
48 | 35 | ad2antrr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) → 𝐶 ∈ ℤ) |
49 | 5 | nnzd 9290 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁))) → 𝑁 ∈ ℤ) |
50 | 49 | adantl 275 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) → 𝑁 ∈ ℤ) |
51 | 50 | adantr 274 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) → 𝑁 ∈ ℤ) |
52 | 48, 51 | gcdcld 11867 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) → (𝐶 gcd 𝑁) ∈
ℕ0) |
53 | 52 | nn0cnd 9150 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) → (𝐶 gcd 𝑁) ∈ ℂ) |
54 | 53 | adantr 274 |
. . . . . . . . . . . . 13
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝐶 ∈
ℤ) ∧ (𝑁 ∈
ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → (𝐶 gcd 𝑁) ∈ ℂ) |
55 | | simpl 108 |
. . . . . . . . . . . . . . 15
⊢ ((𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ) → 𝑟 ∈
ℤ) |
56 | 55 | zcnd 9292 |
. . . . . . . . . . . . . 14
⊢ ((𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ) → 𝑟 ∈
ℂ) |
57 | 56 | adantl 275 |
. . . . . . . . . . . . 13
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝐶 ∈
ℤ) ∧ (𝑁 ∈
ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → 𝑟 ∈ ℂ) |
58 | 47, 54, 57 | mul12d 8031 |
. . . . . . . . . . . 12
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝐶 ∈
ℤ) ∧ (𝑁 ∈
ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → (𝐴 · ((𝐶 gcd 𝑁) · 𝑟)) = ((𝐶 gcd 𝑁) · (𝐴 · 𝑟))) |
59 | | simp2 983 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → 𝐵 ∈
ℤ) |
60 | 59 | zcnd 9292 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → 𝐵 ∈
ℂ) |
61 | 60 | ad3antrrr 484 |
. . . . . . . . . . . . 13
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝐶 ∈
ℤ) ∧ (𝑁 ∈
ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → 𝐵 ∈ ℂ) |
62 | 36, 50 | gcdcld 11867 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) → (𝐶 gcd 𝑁) ∈
ℕ0) |
63 | 62 | nn0cnd 9150 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) → (𝐶 gcd 𝑁) ∈ ℂ) |
64 | 63 | ad2antrr 480 |
. . . . . . . . . . . . 13
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝐶 ∈
ℤ) ∧ (𝑁 ∈
ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → (𝐶 gcd 𝑁) ∈ ℂ) |
65 | 61, 64, 57 | mul12d 8031 |
. . . . . . . . . . . 12
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝐶 ∈
ℤ) ∧ (𝑁 ∈
ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → (𝐵 · ((𝐶 gcd 𝑁) · 𝑟)) = ((𝐶 gcd 𝑁) · (𝐵 · 𝑟))) |
66 | 58, 65 | oveq12d 5844 |
. . . . . . . . . . 11
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝐶 ∈
ℤ) ∧ (𝑁 ∈
ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → ((𝐴 · ((𝐶 gcd 𝑁) · 𝑟)) − (𝐵 · ((𝐶 gcd 𝑁) · 𝑟))) = (((𝐶 gcd 𝑁) · (𝐴 · 𝑟)) − ((𝐶 gcd 𝑁) · (𝐵 · 𝑟)))) |
67 | 44, 66 | eqeq12d 2172 |
. . . . . . . . . 10
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝐶 ∈
ℤ) ∧ (𝑁 ∈
ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → ((𝑘 · ((𝐶 gcd 𝑁) · 𝑠)) = ((𝐴 · ((𝐶 gcd 𝑁) · 𝑟)) − (𝐵 · ((𝐶 gcd 𝑁) · 𝑟))) ↔ ((𝐶 gcd 𝑁) · (𝑘 · 𝑠)) = (((𝐶 gcd 𝑁) · (𝐴 · 𝑟)) − ((𝐶 gcd 𝑁) · (𝐵 · 𝑟))))) |
68 | 45 | ad3antrrr 484 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝐶 ∈
ℤ) ∧ (𝑁 ∈
ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → 𝐴 ∈ ℤ) |
69 | 55 | adantl 275 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝐶 ∈
ℤ) ∧ (𝑁 ∈
ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → 𝑟 ∈ ℤ) |
70 | 68, 69 | zmulcld 9297 |
. . . . . . . . . . . . . 14
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝐶 ∈
ℤ) ∧ (𝑁 ∈
ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → (𝐴 · 𝑟) ∈ ℤ) |
71 | 70 | zcnd 9292 |
. . . . . . . . . . . . 13
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝐶 ∈
ℤ) ∧ (𝑁 ∈
ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → (𝐴 · 𝑟) ∈ ℂ) |
72 | 59 | ad3antrrr 484 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝐶 ∈
ℤ) ∧ (𝑁 ∈
ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → 𝐵 ∈ ℤ) |
73 | 72, 69 | zmulcld 9297 |
. . . . . . . . . . . . . 14
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝐶 ∈
ℤ) ∧ (𝑁 ∈
ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → (𝐵 · 𝑟) ∈ ℤ) |
74 | 73 | zcnd 9292 |
. . . . . . . . . . . . 13
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝐶 ∈
ℤ) ∧ (𝑁 ∈
ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → (𝐵 · 𝑟) ∈ ℂ) |
75 | 64, 71, 74 | subdid 8293 |
. . . . . . . . . . . 12
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝐶 ∈
ℤ) ∧ (𝑁 ∈
ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → ((𝐶 gcd 𝑁) · ((𝐴 · 𝑟) − (𝐵 · 𝑟))) = (((𝐶 gcd 𝑁) · (𝐴 · 𝑟)) − ((𝐶 gcd 𝑁) · (𝐵 · 𝑟)))) |
76 | 75 | eqcomd 2163 |
. . . . . . . . . . 11
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝐶 ∈
ℤ) ∧ (𝑁 ∈
ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → (((𝐶 gcd 𝑁) · (𝐴 · 𝑟)) − ((𝐶 gcd 𝑁) · (𝐵 · 𝑟))) = ((𝐶 gcd 𝑁) · ((𝐴 · 𝑟) − (𝐵 · 𝑟)))) |
77 | 76 | eqeq2d 2169 |
. . . . . . . . . 10
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝐶 ∈
ℤ) ∧ (𝑁 ∈
ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → (((𝐶 gcd 𝑁) · (𝑘 · 𝑠)) = (((𝐶 gcd 𝑁) · (𝐴 · 𝑟)) − ((𝐶 gcd 𝑁) · (𝐵 · 𝑟))) ↔ ((𝐶 gcd 𝑁) · (𝑘 · 𝑠)) = ((𝐶 gcd 𝑁) · ((𝐴 · 𝑟) − (𝐵 · 𝑟))))) |
78 | 32 | adantr 274 |
. . . . . . . . . . . . 13
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝐶 ∈
ℤ) ∧ (𝑁 ∈
ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → 𝑘 ∈ ℤ) |
79 | | simprr 522 |
. . . . . . . . . . . . 13
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝐶 ∈
ℤ) ∧ (𝑁 ∈
ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → 𝑠 ∈ ℤ) |
80 | 78, 79 | zmulcld 9297 |
. . . . . . . . . . . 12
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝐶 ∈
ℤ) ∧ (𝑁 ∈
ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → (𝑘 · 𝑠) ∈ ℤ) |
81 | 80 | zcnd 9292 |
. . . . . . . . . . 11
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝐶 ∈
ℤ) ∧ (𝑁 ∈
ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → (𝑘 · 𝑠) ∈ ℂ) |
82 | | zmulcl 9225 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∈ ℤ ∧ 𝑟 ∈ ℤ) → (𝐴 · 𝑟) ∈ ℤ) |
83 | 82 | ad2ant2r 501 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → (𝐴 · 𝑟) ∈ ℤ) |
84 | | zmulcl 9225 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐵 ∈ ℤ ∧ 𝑟 ∈ ℤ) → (𝐵 · 𝑟) ∈ ℤ) |
85 | 84 | ad2ant2lr 502 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → (𝐵 · 𝑟) ∈ ℤ) |
86 | 83, 85 | zsubcld 9296 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → ((𝐴 · 𝑟) − (𝐵 · 𝑟)) ∈ ℤ) |
87 | 86 | zcnd 9292 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → ((𝐴 · 𝑟) − (𝐵 · 𝑟)) ∈ ℂ) |
88 | 87 | ex 114 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ) → ((𝐴 · 𝑟) − (𝐵 · 𝑟)) ∈ ℂ)) |
89 | 88 | 3adant3 1002 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → ((𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ) → ((𝐴 · 𝑟) − (𝐵 · 𝑟)) ∈ ℂ)) |
90 | 89 | ad2antrr 480 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) → ((𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ) → ((𝐴 · 𝑟) − (𝐵 · 𝑟)) ∈ ℂ)) |
91 | 90 | imp 123 |
. . . . . . . . . . 11
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝐶 ∈
ℤ) ∧ (𝑁 ∈
ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → ((𝐴 · 𝑟) − (𝐵 · 𝑟)) ∈ ℂ) |
92 | 10 | ad2antrl 482 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) → 𝑁 ≠ 0) |
93 | | gcd2n0cl 11868 |
. . . . . . . . . . . . . . 15
⊢ ((𝐶 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (𝐶 gcd 𝑁) ∈ ℕ) |
94 | 36, 50, 92, 93 | syl3anc 1220 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) → (𝐶 gcd 𝑁) ∈ ℕ) |
95 | 94 | nnne0d 8883 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) → (𝐶 gcd 𝑁) ≠ 0) |
96 | 95 | ad2antrr 480 |
. . . . . . . . . . . 12
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝐶 ∈
ℤ) ∧ (𝑁 ∈
ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → (𝐶 gcd 𝑁) ≠ 0) |
97 | 52 | adantr 274 |
. . . . . . . . . . . . . 14
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝐶 ∈
ℤ) ∧ (𝑁 ∈
ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → (𝐶 gcd 𝑁) ∈
ℕ0) |
98 | 97 | nn0zd 9289 |
. . . . . . . . . . . . 13
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝐶 ∈
ℤ) ∧ (𝑁 ∈
ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → (𝐶 gcd 𝑁) ∈ ℤ) |
99 | | 0zd 9184 |
. . . . . . . . . . . . 13
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝐶 ∈
ℤ) ∧ (𝑁 ∈
ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → 0 ∈
ℤ) |
100 | | zapne 9243 |
. . . . . . . . . . . . 13
⊢ (((𝐶 gcd 𝑁) ∈ ℤ ∧ 0 ∈ ℤ)
→ ((𝐶 gcd 𝑁) # 0 ↔ (𝐶 gcd 𝑁) ≠ 0)) |
101 | 98, 99, 100 | syl2anc 409 |
. . . . . . . . . . . 12
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝐶 ∈
ℤ) ∧ (𝑁 ∈
ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → ((𝐶 gcd 𝑁) # 0 ↔ (𝐶 gcd 𝑁) ≠ 0)) |
102 | 96, 101 | mpbird 166 |
. . . . . . . . . . 11
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝐶 ∈
ℤ) ∧ (𝑁 ∈
ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → (𝐶 gcd 𝑁) # 0) |
103 | 81, 91, 64, 102 | mulcanapd 8539 |
. . . . . . . . . 10
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝐶 ∈
ℤ) ∧ (𝑁 ∈
ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → (((𝐶 gcd 𝑁) · (𝑘 · 𝑠)) = ((𝐶 gcd 𝑁) · ((𝐴 · 𝑟) − (𝐵 · 𝑟))) ↔ (𝑘 · 𝑠) = ((𝐴 · 𝑟) − (𝐵 · 𝑟)))) |
104 | 67, 77, 103 | 3bitrd 213 |
. . . . . . . . 9
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝐶 ∈
ℤ) ∧ (𝑁 ∈
ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → ((𝑘 · ((𝐶 gcd 𝑁) · 𝑠)) = ((𝐴 · ((𝐶 gcd 𝑁) · 𝑟)) − (𝐵 · ((𝐶 gcd 𝑁) · 𝑟))) ↔ (𝑘 · 𝑠) = ((𝐴 · 𝑟) − (𝐵 · 𝑟)))) |
105 | 104 | adantr 274 |
. . . . . . . 8
⊢
((((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝐶 ∈
ℤ) ∧ (𝑁 ∈
ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ (𝐶 = ((𝐶 gcd 𝑁) · 𝑟) ∧ 𝑁 = ((𝐶 gcd 𝑁) · 𝑠) ∧ (𝑟 gcd 𝑠) = 1)) → ((𝑘 · ((𝐶 gcd 𝑁) · 𝑠)) = ((𝐴 · ((𝐶 gcd 𝑁) · 𝑟)) − (𝐵 · ((𝐶 gcd 𝑁) · 𝑟))) ↔ (𝑘 · 𝑠) = ((𝐴 · 𝑟) − (𝐵 · 𝑟)))) |
106 | | zcn 9177 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐴 ∈ ℤ → 𝐴 ∈
ℂ) |
107 | | zcn 9177 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐵 ∈ ℤ → 𝐵 ∈
ℂ) |
108 | 106, 107 | anim12i 336 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 ∈ ℂ ∧ 𝐵 ∈
ℂ)) |
109 | 108 | 3adant3 1002 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → (𝐴 ∈ ℂ ∧ 𝐵 ∈
ℂ)) |
110 | 109 | ad2antrr 480 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) → (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ)) |
111 | 110, 56 | anim12i 336 |
. . . . . . . . . . . . . 14
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝐶 ∈
ℤ) ∧ (𝑁 ∈
ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑟 ∈ ℂ)) |
112 | | df-3an 965 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑟 ∈ ℂ) ↔ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑟 ∈
ℂ)) |
113 | 111, 112 | sylibr 133 |
. . . . . . . . . . . . 13
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝐶 ∈
ℤ) ∧ (𝑁 ∈
ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑟 ∈ ℂ)) |
114 | | subdir 8265 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑟 ∈ ℂ) → ((𝐴 − 𝐵) · 𝑟) = ((𝐴 · 𝑟) − (𝐵 · 𝑟))) |
115 | 113, 114 | syl 14 |
. . . . . . . . . . . 12
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝐶 ∈
ℤ) ∧ (𝑁 ∈
ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → ((𝐴 − 𝐵) · 𝑟) = ((𝐴 · 𝑟) − (𝐵 · 𝑟))) |
116 | 115 | eqcomd 2163 |
. . . . . . . . . . 11
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝐶 ∈
ℤ) ∧ (𝑁 ∈
ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → ((𝐴 · 𝑟) − (𝐵 · 𝑟)) = ((𝐴 − 𝐵) · 𝑟)) |
117 | 116 | adantr 274 |
. . . . . . . . . 10
⊢
((((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝐶 ∈
ℤ) ∧ (𝑁 ∈
ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ (𝐶 = ((𝐶 gcd 𝑁) · 𝑟) ∧ 𝑁 = ((𝐶 gcd 𝑁) · 𝑠) ∧ (𝑟 gcd 𝑠) = 1)) → ((𝐴 · 𝑟) − (𝐵 · 𝑟)) = ((𝐴 − 𝐵) · 𝑟)) |
118 | 117 | eqeq2d 2169 |
. . . . . . . . 9
⊢
((((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝐶 ∈
ℤ) ∧ (𝑁 ∈
ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ (𝐶 = ((𝐶 gcd 𝑁) · 𝑟) ∧ 𝑁 = ((𝐶 gcd 𝑁) · 𝑠) ∧ (𝑟 gcd 𝑠) = 1)) → ((𝑘 · 𝑠) = ((𝐴 · 𝑟) − (𝐵 · 𝑟)) ↔ (𝑘 · 𝑠) = ((𝐴 − 𝐵) · 𝑟))) |
119 | 5 | nncnd 8852 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁))) → 𝑁 ∈ ℂ) |
120 | 119 | adantl 275 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) → 𝑁 ∈ ℂ) |
121 | 120 | ad2antrr 480 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝐶 ∈
ℤ) ∧ (𝑁 ∈
ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → 𝑁 ∈ ℂ) |
122 | 79 | zcnd 9292 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝐶 ∈
ℤ) ∧ (𝑁 ∈
ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → 𝑠 ∈ ℂ) |
123 | 121, 122,
40, 102 | divmulap2d 8701 |
. . . . . . . . . . . . . 14
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝐶 ∈
ℤ) ∧ (𝑁 ∈
ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → ((𝑁 / (𝐶 gcd 𝑁)) = 𝑠 ↔ 𝑁 = ((𝐶 gcd 𝑁) · 𝑠))) |
124 | | simpll 519 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝐶 ∈
ℤ) ∧ (𝑁 ∈
ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ (𝑁 / (𝐶 gcd 𝑁)) = 𝑠) → (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ)) |
125 | 69 | adantr 274 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝐶 ∈
ℤ) ∧ (𝑁 ∈
ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ (𝑁 / (𝐶 gcd 𝑁)) = 𝑠) → 𝑟 ∈ ℤ) |
126 | 5 | adantl 275 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) → 𝑁 ∈ ℕ) |
127 | | divgcdnnr 11875 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑁 ∈ ℕ ∧ 𝐶 ∈ ℤ) → (𝑁 / (𝐶 gcd 𝑁)) ∈ ℕ) |
128 | 126, 36, 127 | syl2anc 409 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) → (𝑁 / (𝐶 gcd 𝑁)) ∈ ℕ) |
129 | 128 | ad3antrrr 484 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝐶 ∈
ℤ) ∧ (𝑁 ∈
ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ (𝑁 / (𝐶 gcd 𝑁)) = 𝑠) → (𝑁 / (𝐶 gcd 𝑁)) ∈ ℕ) |
130 | | eleq1 2220 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑠 = (𝑁 / (𝐶 gcd 𝑁)) → (𝑠 ∈ ℕ ↔ (𝑁 / (𝐶 gcd 𝑁)) ∈ ℕ)) |
131 | 130 | eqcoms 2160 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑁 / (𝐶 gcd 𝑁)) = 𝑠 → (𝑠 ∈ ℕ ↔ (𝑁 / (𝐶 gcd 𝑁)) ∈ ℕ)) |
132 | 131 | adantl 275 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝐶 ∈
ℤ) ∧ (𝑁 ∈
ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ (𝑁 / (𝐶 gcd 𝑁)) = 𝑠) → (𝑠 ∈ ℕ ↔ (𝑁 / (𝐶 gcd 𝑁)) ∈ ℕ)) |
133 | 129, 132 | mpbird 166 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝐶 ∈
ℤ) ∧ (𝑁 ∈
ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ (𝑁 / (𝐶 gcd 𝑁)) = 𝑠) → 𝑠 ∈ ℕ) |
134 | 125, 133 | jca 304 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝐶 ∈
ℤ) ∧ (𝑁 ∈
ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ (𝑁 / (𝐶 gcd 𝑁)) = 𝑠) → (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ)) |
135 | 124, 134 | jca 304 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝐶 ∈
ℤ) ∧ (𝑁 ∈
ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ (𝑁 / (𝐶 gcd 𝑁)) = 𝑠) → ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ))) |
136 | | simpr 109 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝐶 ∈
ℤ) ∧ (𝑁 ∈
ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ (𝑁 / (𝐶 gcd 𝑁)) = 𝑠) → (𝑁 / (𝐶 gcd 𝑁)) = 𝑠) |
137 | | nnz 9191 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑠 ∈ ℕ → 𝑠 ∈
ℤ) |
138 | 137 | adantl 275 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ) → 𝑠 ∈
ℤ) |
139 | 138 | anim2i 340 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑘 ∈ ℤ ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ)) → (𝑘 ∈ ℤ ∧ 𝑠 ∈
ℤ)) |
140 | 139 | adantl 275 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝑘 ∈ ℤ ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ))) → (𝑘 ∈ ℤ ∧ 𝑠 ∈
ℤ)) |
141 | | dvdsmul2 11721 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑘 ∈ ℤ ∧ 𝑠 ∈ ℤ) → 𝑠 ∥ (𝑘 · 𝑠)) |
142 | 140, 141 | syl 14 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝑘 ∈ ℤ ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ))) → 𝑠 ∥ (𝑘 · 𝑠)) |
143 | | breq2 3971 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑘 · 𝑠) = ((𝐴 − 𝐵) · 𝑟) → (𝑠 ∥ (𝑘 · 𝑠) ↔ 𝑠 ∥ ((𝐴 − 𝐵) · 𝑟))) |
144 | | zsubcl 9213 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 − 𝐵) ∈ ℤ) |
145 | 144 | zcnd 9292 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 − 𝐵) ∈ ℂ) |
146 | 145 | adantr 274 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝑘 ∈ ℤ ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ))) → (𝐴 − 𝐵) ∈ ℂ) |
147 | | zcn 9177 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑟 ∈ ℤ → 𝑟 ∈
ℂ) |
148 | 147 | ad2antrl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑘 ∈ ℤ ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ)) → 𝑟 ∈
ℂ) |
149 | 148 | adantl 275 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝑘 ∈ ℤ ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ))) → 𝑟 ∈
ℂ) |
150 | 146, 149 | mulcomd 7901 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝑘 ∈ ℤ ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ))) →
((𝐴 − 𝐵) · 𝑟) = (𝑟 · (𝐴 − 𝐵))) |
151 | 150 | breq2d 3979 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝑘 ∈ ℤ ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ))) → (𝑠 ∥ ((𝐴 − 𝐵) · 𝑟) ↔ 𝑠 ∥ (𝑟 · (𝐴 − 𝐵)))) |
152 | 137 | anim2i 340 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ) → (𝑟 ∈ ℤ ∧ 𝑠 ∈
ℤ)) |
153 | | gcdcom 11872 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ) → (𝑟 gcd 𝑠) = (𝑠 gcd 𝑟)) |
154 | 152, 153 | syl 14 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ) → (𝑟 gcd 𝑠) = (𝑠 gcd 𝑟)) |
155 | 154 | eqeq1d 2166 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ) → ((𝑟 gcd 𝑠) = 1 ↔ (𝑠 gcd 𝑟) = 1)) |
156 | 155 | ad2antll 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝑘 ∈ ℤ ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ))) →
((𝑟 gcd 𝑠) = 1 ↔ (𝑠 gcd 𝑟) = 1)) |
157 | 152 | adantl 275 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ ((𝑘 ∈ ℤ ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ)) → (𝑟 ∈ ℤ ∧ 𝑠 ∈
ℤ)) |
158 | 157 | ancomd 265 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((𝑘 ∈ ℤ ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ)) → (𝑠 ∈ ℤ ∧ 𝑟 ∈
ℤ)) |
159 | 144, 158 | anim12i 336 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝑘 ∈ ℤ ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ))) →
((𝐴 − 𝐵) ∈ ℤ ∧ (𝑠 ∈ ℤ ∧ 𝑟 ∈
ℤ))) |
160 | 159 | ancomd 265 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝑘 ∈ ℤ ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ))) →
((𝑠 ∈ ℤ ∧
𝑟 ∈ ℤ) ∧
(𝐴 − 𝐵) ∈
ℤ)) |
161 | | df-3an 965 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝑠 ∈ ℤ ∧ 𝑟 ∈ ℤ ∧ (𝐴 − 𝐵) ∈ ℤ) ↔ ((𝑠 ∈ ℤ ∧ 𝑟 ∈ ℤ) ∧ (𝐴 − 𝐵) ∈ ℤ)) |
162 | 160, 161 | sylibr 133 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝑘 ∈ ℤ ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ))) → (𝑠 ∈ ℤ ∧ 𝑟 ∈ ℤ ∧ (𝐴 − 𝐵) ∈ ℤ)) |
163 | | coprmdvds 11984 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝑠 ∈ ℤ ∧ 𝑟 ∈ ℤ ∧ (𝐴 − 𝐵) ∈ ℤ) → ((𝑠 ∥ (𝑟 · (𝐴 − 𝐵)) ∧ (𝑠 gcd 𝑟) = 1) → 𝑠 ∥ (𝐴 − 𝐵))) |
164 | 162, 163 | syl 14 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝑘 ∈ ℤ ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ))) →
((𝑠 ∥ (𝑟 · (𝐴 − 𝐵)) ∧ (𝑠 gcd 𝑟) = 1) → 𝑠 ∥ (𝐴 − 𝐵))) |
165 | | simprr 522 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((𝑘 ∈ ℤ ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ)) → 𝑠 ∈
ℕ) |
166 | 165 | anim2i 340 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝑘 ∈ ℤ ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ))) →
((𝐴 ∈ ℤ ∧
𝐵 ∈ ℤ) ∧
𝑠 ∈
ℕ)) |
167 | 166 | ancomd 265 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝑘 ∈ ℤ ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ))) → (𝑠 ∈ ℕ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈
ℤ))) |
168 | | 3anass 967 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝑠 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ↔ (𝑠 ∈ ℕ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈
ℤ))) |
169 | 167, 168 | sylibr 133 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝑘 ∈ ℤ ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ))) → (𝑠 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈
ℤ)) |
170 | | moddvds 11706 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝑠 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝐴 mod 𝑠) = (𝐵 mod 𝑠) ↔ 𝑠 ∥ (𝐴 − 𝐵))) |
171 | 169, 170 | syl 14 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝑘 ∈ ℤ ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ))) →
((𝐴 mod 𝑠) = (𝐵 mod 𝑠) ↔ 𝑠 ∥ (𝐴 − 𝐵))) |
172 | 164, 171 | sylibrd 168 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝑘 ∈ ℤ ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ))) →
((𝑠 ∥ (𝑟 · (𝐴 − 𝐵)) ∧ (𝑠 gcd 𝑟) = 1) → (𝐴 mod 𝑠) = (𝐵 mod 𝑠))) |
173 | 172 | expcomd 1421 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝑘 ∈ ℤ ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ))) →
((𝑠 gcd 𝑟) = 1 → (𝑠 ∥ (𝑟 · (𝐴 − 𝐵)) → (𝐴 mod 𝑠) = (𝐵 mod 𝑠)))) |
174 | 156, 173 | sylbid 149 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝑘 ∈ ℤ ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ))) →
((𝑟 gcd 𝑠) = 1 → (𝑠 ∥ (𝑟 · (𝐴 − 𝐵)) → (𝐴 mod 𝑠) = (𝐵 mod 𝑠)))) |
175 | 174 | com23 78 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝑘 ∈ ℤ ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ))) → (𝑠 ∥ (𝑟 · (𝐴 − 𝐵)) → ((𝑟 gcd 𝑠) = 1 → (𝐴 mod 𝑠) = (𝐵 mod 𝑠)))) |
176 | 151, 175 | sylbid 149 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝑘 ∈ ℤ ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ))) → (𝑠 ∥ ((𝐴 − 𝐵) · 𝑟) → ((𝑟 gcd 𝑠) = 1 → (𝐴 mod 𝑠) = (𝐵 mod 𝑠)))) |
177 | 176 | com3l 81 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑠 ∥ ((𝐴 − 𝐵) · 𝑟) → ((𝑟 gcd 𝑠) = 1 → (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝑘 ∈ ℤ ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ))) → (𝐴 mod 𝑠) = (𝐵 mod 𝑠)))) |
178 | 143, 177 | syl6bi 162 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑘 · 𝑠) = ((𝐴 − 𝐵) · 𝑟) → (𝑠 ∥ (𝑘 · 𝑠) → ((𝑟 gcd 𝑠) = 1 → (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝑘 ∈ ℤ ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ))) → (𝐴 mod 𝑠) = (𝐵 mod 𝑠))))) |
179 | 178 | com14 88 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝑘 ∈ ℤ ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ))) → (𝑠 ∥ (𝑘 · 𝑠) → ((𝑟 gcd 𝑠) = 1 → ((𝑘 · 𝑠) = ((𝐴 − 𝐵) · 𝑟) → (𝐴 mod 𝑠) = (𝐵 mod 𝑠))))) |
180 | 142, 179 | mpd 13 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝑘 ∈ ℤ ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ))) →
((𝑟 gcd 𝑠) = 1 → ((𝑘 · 𝑠) = ((𝐴 − 𝐵) · 𝑟) → (𝐴 mod 𝑠) = (𝐵 mod 𝑠)))) |
181 | 180 | ex 114 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝑘 ∈ ℤ ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ)) → ((𝑟 gcd 𝑠) = 1 → ((𝑘 · 𝑠) = ((𝐴 − 𝐵) · 𝑟) → (𝐴 mod 𝑠) = (𝐵 mod 𝑠))))) |
182 | 181 | 3adant3 1002 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → ((𝑘 ∈ ℤ ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ)) → ((𝑟 gcd 𝑠) = 1 → ((𝑘 · 𝑠) = ((𝐴 − 𝐵) · 𝑟) → (𝐴 mod 𝑠) = (𝐵 mod 𝑠))))) |
183 | 182 | adantr 274 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) → ((𝑘 ∈ ℤ ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ)) → ((𝑟 gcd 𝑠) = 1 → ((𝑘 · 𝑠) = ((𝐴 − 𝐵) · 𝑟) → (𝐴 mod 𝑠) = (𝐵 mod 𝑠))))) |
184 | 183 | impl 378 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝐶 ∈
ℤ) ∧ (𝑁 ∈
ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ)) → ((𝑟 gcd 𝑠) = 1 → ((𝑘 · 𝑠) = ((𝐴 − 𝐵) · 𝑟) → (𝐴 mod 𝑠) = (𝐵 mod 𝑠)))) |
185 | 184 | adantr 274 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝐶 ∈
ℤ) ∧ (𝑁 ∈
ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ)) ∧ (𝑁 / (𝐶 gcd 𝑁)) = 𝑠) → ((𝑟 gcd 𝑠) = 1 → ((𝑘 · 𝑠) = ((𝐴 − 𝐵) · 𝑟) → (𝐴 mod 𝑠) = (𝐵 mod 𝑠)))) |
186 | 185 | imp 123 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝐶 ∈
ℤ) ∧ (𝑁 ∈
ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ)) ∧ (𝑁 / (𝐶 gcd 𝑁)) = 𝑠) ∧ (𝑟 gcd 𝑠) = 1) → ((𝑘 · 𝑠) = ((𝐴 − 𝐵) · 𝑟) → (𝐴 mod 𝑠) = (𝐵 mod 𝑠))) |
187 | | eqtr2 2176 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑁 / (𝐶 gcd 𝑁)) = 𝑀 ∧ (𝑁 / (𝐶 gcd 𝑁)) = 𝑠) → 𝑀 = 𝑠) |
188 | | oveq2 5834 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑀 = 𝑠 → (𝐴 mod 𝑀) = (𝐴 mod 𝑠)) |
189 | | oveq2 5834 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑀 = 𝑠 → (𝐵 mod 𝑀) = (𝐵 mod 𝑠)) |
190 | 188, 189 | eqeq12d 2172 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑀 = 𝑠 → ((𝐴 mod 𝑀) = (𝐵 mod 𝑀) ↔ (𝐴 mod 𝑠) = (𝐵 mod 𝑠))) |
191 | 187, 190 | syl 14 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑁 / (𝐶 gcd 𝑁)) = 𝑀 ∧ (𝑁 / (𝐶 gcd 𝑁)) = 𝑠) → ((𝐴 mod 𝑀) = (𝐵 mod 𝑀) ↔ (𝐴 mod 𝑠) = (𝐵 mod 𝑠))) |
192 | 191 | ex 114 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑁 / (𝐶 gcd 𝑁)) = 𝑀 → ((𝑁 / (𝐶 gcd 𝑁)) = 𝑠 → ((𝐴 mod 𝑀) = (𝐵 mod 𝑀) ↔ (𝐴 mod 𝑠) = (𝐵 mod 𝑠)))) |
193 | 192 | eqcoms 2160 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑀 = (𝑁 / (𝐶 gcd 𝑁)) → ((𝑁 / (𝐶 gcd 𝑁)) = 𝑠 → ((𝐴 mod 𝑀) = (𝐵 mod 𝑀) ↔ (𝐴 mod 𝑠) = (𝐵 mod 𝑠)))) |
194 | 193 | ad2antll 483 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) → ((𝑁 / (𝐶 gcd 𝑁)) = 𝑠 → ((𝐴 mod 𝑀) = (𝐵 mod 𝑀) ↔ (𝐴 mod 𝑠) = (𝐵 mod 𝑠)))) |
195 | 194 | ad2antrr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝐶 ∈
ℤ) ∧ (𝑁 ∈
ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ)) → ((𝑁 / (𝐶 gcd 𝑁)) = 𝑠 → ((𝐴 mod 𝑀) = (𝐵 mod 𝑀) ↔ (𝐴 mod 𝑠) = (𝐵 mod 𝑠)))) |
196 | 195 | imp 123 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝐶 ∈
ℤ) ∧ (𝑁 ∈
ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ)) ∧ (𝑁 / (𝐶 gcd 𝑁)) = 𝑠) → ((𝐴 mod 𝑀) = (𝐵 mod 𝑀) ↔ (𝐴 mod 𝑠) = (𝐵 mod 𝑠))) |
197 | 196 | adantr 274 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝐶 ∈
ℤ) ∧ (𝑁 ∈
ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ)) ∧ (𝑁 / (𝐶 gcd 𝑁)) = 𝑠) ∧ (𝑟 gcd 𝑠) = 1) → ((𝐴 mod 𝑀) = (𝐵 mod 𝑀) ↔ (𝐴 mod 𝑠) = (𝐵 mod 𝑠))) |
198 | 186, 197 | sylibrd 168 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝐶 ∈
ℤ) ∧ (𝑁 ∈
ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ)) ∧ (𝑁 / (𝐶 gcd 𝑁)) = 𝑠) ∧ (𝑟 gcd 𝑠) = 1) → ((𝑘 · 𝑠) = ((𝐴 − 𝐵) · 𝑟) → (𝐴 mod 𝑀) = (𝐵 mod 𝑀))) |
199 | 198 | ex 114 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝐶 ∈
ℤ) ∧ (𝑁 ∈
ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℕ)) ∧ (𝑁 / (𝐶 gcd 𝑁)) = 𝑠) → ((𝑟 gcd 𝑠) = 1 → ((𝑘 · 𝑠) = ((𝐴 − 𝐵) · 𝑟) → (𝐴 mod 𝑀) = (𝐵 mod 𝑀)))) |
200 | 135, 136,
199 | syl2anc 409 |
. . . . . . . . . . . . . . 15
⊢
((((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝐶 ∈
ℤ) ∧ (𝑁 ∈
ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ (𝑁 / (𝐶 gcd 𝑁)) = 𝑠) → ((𝑟 gcd 𝑠) = 1 → ((𝑘 · 𝑠) = ((𝐴 − 𝐵) · 𝑟) → (𝐴 mod 𝑀) = (𝐵 mod 𝑀)))) |
201 | 200 | ex 114 |
. . . . . . . . . . . . . 14
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝐶 ∈
ℤ) ∧ (𝑁 ∈
ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → ((𝑁 / (𝐶 gcd 𝑁)) = 𝑠 → ((𝑟 gcd 𝑠) = 1 → ((𝑘 · 𝑠) = ((𝐴 − 𝐵) · 𝑟) → (𝐴 mod 𝑀) = (𝐵 mod 𝑀))))) |
202 | 123, 201 | sylbird 169 |
. . . . . . . . . . . . 13
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝐶 ∈
ℤ) ∧ (𝑁 ∈
ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → (𝑁 = ((𝐶 gcd 𝑁) · 𝑠) → ((𝑟 gcd 𝑠) = 1 → ((𝑘 · 𝑠) = ((𝐴 − 𝐵) · 𝑟) → (𝐴 mod 𝑀) = (𝐵 mod 𝑀))))) |
203 | 202 | com3l 81 |
. . . . . . . . . . . 12
⊢ (𝑁 = ((𝐶 gcd 𝑁) · 𝑠) → ((𝑟 gcd 𝑠) = 1 → (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → ((𝑘 · 𝑠) = ((𝐴 − 𝐵) · 𝑟) → (𝐴 mod 𝑀) = (𝐵 mod 𝑀))))) |
204 | 203 | a1i 9 |
. . . . . . . . . . 11
⊢ (𝐶 = ((𝐶 gcd 𝑁) · 𝑟) → (𝑁 = ((𝐶 gcd 𝑁) · 𝑠) → ((𝑟 gcd 𝑠) = 1 → (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → ((𝑘 · 𝑠) = ((𝐴 − 𝐵) · 𝑟) → (𝐴 mod 𝑀) = (𝐵 mod 𝑀)))))) |
205 | 204 | 3imp 1176 |
. . . . . . . . . 10
⊢ ((𝐶 = ((𝐶 gcd 𝑁) · 𝑟) ∧ 𝑁 = ((𝐶 gcd 𝑁) · 𝑠) ∧ (𝑟 gcd 𝑠) = 1) → (((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → ((𝑘 · 𝑠) = ((𝐴 − 𝐵) · 𝑟) → (𝐴 mod 𝑀) = (𝐵 mod 𝑀)))) |
206 | 205 | impcom 124 |
. . . . . . . . 9
⊢
((((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝐶 ∈
ℤ) ∧ (𝑁 ∈
ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ (𝐶 = ((𝐶 gcd 𝑁) · 𝑟) ∧ 𝑁 = ((𝐶 gcd 𝑁) · 𝑠) ∧ (𝑟 gcd 𝑠) = 1)) → ((𝑘 · 𝑠) = ((𝐴 − 𝐵) · 𝑟) → (𝐴 mod 𝑀) = (𝐵 mod 𝑀))) |
207 | 118, 206 | sylbid 149 |
. . . . . . . 8
⊢
((((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝐶 ∈
ℤ) ∧ (𝑁 ∈
ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ (𝐶 = ((𝐶 gcd 𝑁) · 𝑟) ∧ 𝑁 = ((𝐶 gcd 𝑁) · 𝑠) ∧ (𝑟 gcd 𝑠) = 1)) → ((𝑘 · 𝑠) = ((𝐴 · 𝑟) − (𝐵 · 𝑟)) → (𝐴 mod 𝑀) = (𝐵 mod 𝑀))) |
208 | 105, 207 | sylbid 149 |
. . . . . . 7
⊢
((((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝐶 ∈
ℤ) ∧ (𝑁 ∈
ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ (𝐶 = ((𝐶 gcd 𝑁) · 𝑟) ∧ 𝑁 = ((𝐶 gcd 𝑁) · 𝑠) ∧ (𝑟 gcd 𝑠) = 1)) → ((𝑘 · ((𝐶 gcd 𝑁) · 𝑠)) = ((𝐴 · ((𝐶 gcd 𝑁) · 𝑟)) − (𝐵 · ((𝐶 gcd 𝑁) · 𝑟))) → (𝐴 mod 𝑀) = (𝐵 mod 𝑀))) |
209 | 31, 208 | sylbid 149 |
. . . . . 6
⊢
((((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝐶 ∈
ℤ) ∧ (𝑁 ∈
ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) ∧ (𝐶 = ((𝐶 gcd 𝑁) · 𝑟) ∧ 𝑁 = ((𝐶 gcd 𝑁) · 𝑠) ∧ (𝑟 gcd 𝑠) = 1)) → ((𝑘 · 𝑁) = ((𝐴 · 𝐶) − (𝐵 · 𝐶)) → (𝐴 mod 𝑀) = (𝐵 mod 𝑀))) |
210 | 209 | ex 114 |
. . . . 5
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ ∧ 𝐶 ∈
ℤ) ∧ (𝑁 ∈
ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) ∧ (𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ)) → ((𝐶 = ((𝐶 gcd 𝑁) · 𝑟) ∧ 𝑁 = ((𝐶 gcd 𝑁) · 𝑠) ∧ (𝑟 gcd 𝑠) = 1) → ((𝑘 · 𝑁) = ((𝐴 · 𝐶) − (𝐵 · 𝐶)) → (𝐴 mod 𝑀) = (𝐵 mod 𝑀)))) |
211 | 210 | rexlimdvva 2582 |
. . . 4
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) → (∃𝑟 ∈ ℤ ∃𝑠 ∈ ℤ (𝐶 = ((𝐶 gcd 𝑁) · 𝑟) ∧ 𝑁 = ((𝐶 gcd 𝑁) · 𝑠) ∧ (𝑟 gcd 𝑠) = 1) → ((𝑘 · 𝑁) = ((𝐴 · 𝐶) − (𝐵 · 𝐶)) → (𝐴 mod 𝑀) = (𝐵 mod 𝑀)))) |
212 | 22, 211 | mpd 13 |
. . 3
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) ∧ 𝑘 ∈ ℤ) → ((𝑘 · 𝑁) = ((𝐴 · 𝐶) − (𝐵 · 𝐶)) → (𝐴 mod 𝑀) = (𝐵 mod 𝑀))) |
213 | 212 | rexlimdva 2574 |
. 2
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) → (∃𝑘 ∈ ℤ (𝑘 · 𝑁) = ((𝐴 · 𝐶) − (𝐵 · 𝐶)) → (𝐴 mod 𝑀) = (𝐵 mod 𝑀))) |
214 | 7, 213 | sylbid 149 |
1
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) → (((𝐴 · 𝐶) mod 𝑁) = ((𝐵 · 𝐶) mod 𝑁) → (𝐴 mod 𝑀) = (𝐵 mod 𝑀))) |