Step | Hyp | Ref
| Expression |
1 | | oveq2 6557 |
. . . . 5
⊢ ((𝐴 mod 𝑁) = 0 → (((𝐴 − 1) mod 𝑁) − (𝐴 mod 𝑁)) = (((𝐴 − 1) mod 𝑁) − 0)) |
2 | 1 | adantl 481 |
. . . 4
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ (𝐴 mod 𝑁) = 0) → (((𝐴 − 1) mod 𝑁) − (𝐴 mod 𝑁)) = (((𝐴 − 1) mod 𝑁) − 0)) |
3 | | peano2zm 11297 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℤ → (𝐴 − 1) ∈
ℤ) |
4 | 3 | zred 11358 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℤ → (𝐴 − 1) ∈
ℝ) |
5 | 4 | adantr 480 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝐴 − 1) ∈
ℝ) |
6 | | nnrp 11718 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℝ+) |
7 | 6 | adantl 481 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) → 𝑁 ∈
ℝ+) |
8 | 5, 7 | modcld 12536 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝐴 − 1) mod 𝑁) ∈
ℝ) |
9 | 8 | recnd 9947 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝐴 − 1) mod 𝑁) ∈
ℂ) |
10 | 9 | subid1d 10260 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (((𝐴 − 1) mod 𝑁) − 0) = ((𝐴 − 1) mod 𝑁)) |
11 | 10 | adantr 480 |
. . . 4
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ (𝐴 mod 𝑁) = 0) → (((𝐴 − 1) mod 𝑁) − 0) = ((𝐴 − 1) mod 𝑁)) |
12 | | mod0mul 42108 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝐴 mod 𝑁) = 0 → ∃𝑥 ∈ ℤ 𝐴 = (𝑥 · 𝑁))) |
13 | 12 | imp 444 |
. . . . 5
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ (𝐴 mod 𝑁) = 0) → ∃𝑥 ∈ ℤ 𝐴 = (𝑥 · 𝑁)) |
14 | | oveq1 6556 |
. . . . . . . . . 10
⊢ (𝐴 = (𝑥 · 𝑁) → (𝐴 − 1) = ((𝑥 · 𝑁) − 1)) |
15 | 14 | oveq1d 6564 |
. . . . . . . . 9
⊢ (𝐴 = (𝑥 · 𝑁) → ((𝐴 − 1) mod 𝑁) = (((𝑥 · 𝑁) − 1) mod 𝑁)) |
16 | | zcn 11259 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ ℤ → 𝑥 ∈
ℂ) |
17 | | nncn 10905 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℂ) |
18 | 17 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) → 𝑁 ∈
ℂ) |
19 | | mulcl 9899 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ ℂ ∧ 𝑁 ∈ ℂ) → (𝑥 · 𝑁) ∈ ℂ) |
20 | 16, 18, 19 | syl2anr 494 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ 𝑥 ∈ ℤ) → (𝑥 · 𝑁) ∈ ℂ) |
21 | 18 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ 𝑥 ∈ ℤ) → 𝑁 ∈
ℂ) |
22 | 20, 21 | npcand 10275 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ 𝑥 ∈ ℤ) → (((𝑥 · 𝑁) − 𝑁) + 𝑁) = (𝑥 · 𝑁)) |
23 | 22 | eqcomd 2616 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ 𝑥 ∈ ℤ) → (𝑥 · 𝑁) = (((𝑥 · 𝑁) − 𝑁) + 𝑁)) |
24 | 16 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ 𝑥 ∈ ℤ) → 𝑥 ∈
ℂ) |
25 | 24, 21 | mulsubfacd 10371 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ 𝑥 ∈ ℤ) → ((𝑥 · 𝑁) − 𝑁) = ((𝑥 − 1) · 𝑁)) |
26 | 25 | oveq1d 6564 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ 𝑥 ∈ ℤ) → (((𝑥 · 𝑁) − 𝑁) + 𝑁) = (((𝑥 − 1) · 𝑁) + 𝑁)) |
27 | 23, 26 | eqtrd 2644 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ 𝑥 ∈ ℤ) → (𝑥 · 𝑁) = (((𝑥 − 1) · 𝑁) + 𝑁)) |
28 | 27 | oveq1d 6564 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ 𝑥 ∈ ℤ) → ((𝑥 · 𝑁) − 1) = ((((𝑥 − 1) · 𝑁) + 𝑁) − 1)) |
29 | | peano2zm 11297 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℤ → (𝑥 − 1) ∈
ℤ) |
30 | 29 | zcnd 11359 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℤ → (𝑥 − 1) ∈
ℂ) |
31 | | mulcl 9899 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 − 1) ∈ ℂ ∧
𝑁 ∈ ℂ) →
((𝑥 − 1) ·
𝑁) ∈
ℂ) |
32 | 30, 18, 31 | syl2anr 494 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ 𝑥 ∈ ℤ) → ((𝑥 − 1) · 𝑁) ∈
ℂ) |
33 | | 1cnd 9935 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ 𝑥 ∈ ℤ) → 1 ∈
ℂ) |
34 | 32, 21, 33 | addsubassd 10291 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ 𝑥 ∈ ℤ) →
((((𝑥 − 1) ·
𝑁) + 𝑁) − 1) = (((𝑥 − 1) · 𝑁) + (𝑁 − 1))) |
35 | 28, 34 | eqtrd 2644 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ 𝑥 ∈ ℤ) → ((𝑥 · 𝑁) − 1) = (((𝑥 − 1) · 𝑁) + (𝑁 − 1))) |
36 | 35 | oveq1d 6564 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ 𝑥 ∈ ℤ) → (((𝑥 · 𝑁) − 1) mod 𝑁) = ((((𝑥 − 1) · 𝑁) + (𝑁 − 1)) mod 𝑁)) |
37 | | nnre 10904 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℝ) |
38 | | peano2rem 10227 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ ℝ → (𝑁 − 1) ∈
ℝ) |
39 | 37, 38 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈
ℝ) |
40 | 39 | recnd 9947 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈
ℂ) |
41 | 40 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑁 − 1) ∈
ℂ) |
42 | 41 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ 𝑥 ∈ ℤ) → (𝑁 − 1) ∈
ℂ) |
43 | 32, 42 | addcomd 10117 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ 𝑥 ∈ ℤ) → (((𝑥 − 1) · 𝑁) + (𝑁 − 1)) = ((𝑁 − 1) + ((𝑥 − 1) · 𝑁))) |
44 | 43 | oveq1d 6564 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ 𝑥 ∈ ℤ) →
((((𝑥 − 1) ·
𝑁) + (𝑁 − 1)) mod 𝑁) = (((𝑁 − 1) + ((𝑥 − 1) · 𝑁)) mod 𝑁)) |
45 | 39 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑁 − 1) ∈
ℝ) |
46 | 45 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ 𝑥 ∈ ℤ) → (𝑁 − 1) ∈
ℝ) |
47 | 7 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ 𝑥 ∈ ℤ) → 𝑁 ∈
ℝ+) |
48 | 29 | adantl 481 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ 𝑥 ∈ ℤ) → (𝑥 − 1) ∈
ℤ) |
49 | | modcyc 12567 |
. . . . . . . . . . . 12
⊢ (((𝑁 − 1) ∈ ℝ ∧
𝑁 ∈
ℝ+ ∧ (𝑥 − 1) ∈ ℤ) → (((𝑁 − 1) + ((𝑥 − 1) · 𝑁)) mod 𝑁) = ((𝑁 − 1) mod 𝑁)) |
50 | 46, 47, 48, 49 | syl3anc 1318 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ 𝑥 ∈ ℤ) → (((𝑁 − 1) + ((𝑥 − 1) · 𝑁)) mod 𝑁) = ((𝑁 − 1) mod 𝑁)) |
51 | 39, 6 | jca 553 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℕ → ((𝑁 − 1) ∈ ℝ ∧
𝑁 ∈
ℝ+)) |
52 | 51 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝑁 − 1) ∈ ℝ ∧
𝑁 ∈
ℝ+)) |
53 | 52 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ 𝑥 ∈ ℤ) → ((𝑁 − 1) ∈ ℝ ∧
𝑁 ∈
ℝ+)) |
54 | | nnm1ge0 11321 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℕ → 0 ≤
(𝑁 −
1)) |
55 | 54 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) → 0 ≤
(𝑁 −
1)) |
56 | 55 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ 𝑥 ∈ ℤ) → 0 ≤
(𝑁 −
1)) |
57 | 37 | ltm1d 10835 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℕ → (𝑁 − 1) < 𝑁) |
58 | 57 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑁 − 1) < 𝑁) |
59 | 58 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ 𝑥 ∈ ℤ) → (𝑁 − 1) < 𝑁) |
60 | | modid 12557 |
. . . . . . . . . . . 12
⊢ ((((𝑁 − 1) ∈ ℝ ∧
𝑁 ∈
ℝ+) ∧ (0 ≤ (𝑁 − 1) ∧ (𝑁 − 1) < 𝑁)) → ((𝑁 − 1) mod 𝑁) = (𝑁 − 1)) |
61 | 53, 56, 59, 60 | syl12anc 1316 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ 𝑥 ∈ ℤ) → ((𝑁 − 1) mod 𝑁) = (𝑁 − 1)) |
62 | 50, 61 | eqtrd 2644 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ 𝑥 ∈ ℤ) → (((𝑁 − 1) + ((𝑥 − 1) · 𝑁)) mod 𝑁) = (𝑁 − 1)) |
63 | 36, 44, 62 | 3eqtrd 2648 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ 𝑥 ∈ ℤ) → (((𝑥 · 𝑁) − 1) mod 𝑁) = (𝑁 − 1)) |
64 | 15, 63 | sylan9eqr 2666 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ 𝑥 ∈ ℤ) ∧ 𝐴 = (𝑥 · 𝑁)) → ((𝐴 − 1) mod 𝑁) = (𝑁 − 1)) |
65 | 64 | ex 449 |
. . . . . . 7
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ 𝑥 ∈ ℤ) → (𝐴 = (𝑥 · 𝑁) → ((𝐴 − 1) mod 𝑁) = (𝑁 − 1))) |
66 | 65 | rexlimdva 3013 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) →
(∃𝑥 ∈ ℤ
𝐴 = (𝑥 · 𝑁) → ((𝐴 − 1) mod 𝑁) = (𝑁 − 1))) |
67 | 66 | adantr 480 |
. . . . 5
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ (𝐴 mod 𝑁) = 0) → (∃𝑥 ∈ ℤ 𝐴 = (𝑥 · 𝑁) → ((𝐴 − 1) mod 𝑁) = (𝑁 − 1))) |
68 | 13, 67 | mpd 15 |
. . . 4
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ (𝐴 mod 𝑁) = 0) → ((𝐴 − 1) mod 𝑁) = (𝑁 − 1)) |
69 | 2, 11, 68 | 3eqtrrd 2649 |
. . 3
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ (𝐴 mod 𝑁) = 0) → (𝑁 − 1) = (((𝐴 − 1) mod 𝑁) − (𝐴 mod 𝑁))) |
70 | | df-ne 2782 |
. . . . 5
⊢ ((𝐴 mod 𝑁) ≠ 0 ↔ ¬ (𝐴 mod 𝑁) = 0) |
71 | | modn0mul 42109 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝐴 mod 𝑁) ≠ 0 → ∃𝑥 ∈ ℤ ∃𝑦 ∈ (1..^𝑁)𝐴 = ((𝑥 · 𝑁) + 𝑦))) |
72 | | oveq1 6556 |
. . . . . . . . . . . . 13
⊢ (𝐴 = ((𝑥 · 𝑁) + 𝑦) → (𝐴 − 1) = (((𝑥 · 𝑁) + 𝑦) − 1)) |
73 | 72 | oveq1d 6564 |
. . . . . . . . . . . 12
⊢ (𝐴 = ((𝑥 · 𝑁) + 𝑦) → ((𝐴 − 1) mod 𝑁) = ((((𝑥 · 𝑁) + 𝑦) − 1) mod 𝑁)) |
74 | | oveq1 6556 |
. . . . . . . . . . . 12
⊢ (𝐴 = ((𝑥 · 𝑁) + 𝑦) → (𝐴 mod 𝑁) = (((𝑥 · 𝑁) + 𝑦) mod 𝑁)) |
75 | 73, 74 | oveq12d 6567 |
. . . . . . . . . . 11
⊢ (𝐴 = ((𝑥 · 𝑁) + 𝑦) → (((𝐴 − 1) mod 𝑁) − (𝐴 mod 𝑁)) = (((((𝑥 · 𝑁) + 𝑦) − 1) mod 𝑁) − (((𝑥 · 𝑁) + 𝑦) mod 𝑁))) |
76 | 16 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ (1..^𝑁)) → 𝑥 ∈ ℂ) |
77 | 76, 18, 19 | syl2anr 494 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ (1..^𝑁))) → (𝑥 · 𝑁) ∈ ℂ) |
78 | | elfzoelz 12339 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 ∈ (1..^𝑁) → 𝑦 ∈ ℤ) |
79 | 78 | zcnd 11359 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ (1..^𝑁) → 𝑦 ∈ ℂ) |
80 | 79 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ (1..^𝑁)) → 𝑦 ∈ ℂ) |
81 | 80 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ (1..^𝑁))) → 𝑦 ∈ ℂ) |
82 | | 1cnd 9935 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ (1..^𝑁))) → 1 ∈
ℂ) |
83 | 77, 81, 82 | addsubassd 10291 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ (1..^𝑁))) → (((𝑥 · 𝑁) + 𝑦) − 1) = ((𝑥 · 𝑁) + (𝑦 − 1))) |
84 | | peano2zm 11297 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 ∈ ℤ → (𝑦 − 1) ∈
ℤ) |
85 | 78, 84 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 ∈ (1..^𝑁) → (𝑦 − 1) ∈ ℤ) |
86 | 85 | zcnd 11359 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ (1..^𝑁) → (𝑦 − 1) ∈ ℂ) |
87 | 86 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ (1..^𝑁)) → (𝑦 − 1) ∈ ℂ) |
88 | 87 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ (1..^𝑁))) → (𝑦 − 1) ∈ ℂ) |
89 | 77, 88 | addcomd 10117 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ (1..^𝑁))) → ((𝑥 · 𝑁) + (𝑦 − 1)) = ((𝑦 − 1) + (𝑥 · 𝑁))) |
90 | 83, 89 | eqtrd 2644 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ (1..^𝑁))) → (((𝑥 · 𝑁) + 𝑦) − 1) = ((𝑦 − 1) + (𝑥 · 𝑁))) |
91 | 90 | oveq1d 6564 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ (1..^𝑁))) → ((((𝑥 · 𝑁) + 𝑦) − 1) mod 𝑁) = (((𝑦 − 1) + (𝑥 · 𝑁)) mod 𝑁)) |
92 | 85 | zred 11358 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ (1..^𝑁) → (𝑦 − 1) ∈ ℝ) |
93 | 92 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ (1..^𝑁)) → (𝑦 − 1) ∈ ℝ) |
94 | 93 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ (1..^𝑁))) → (𝑦 − 1) ∈ ℝ) |
95 | 7 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ (1..^𝑁))) → 𝑁 ∈
ℝ+) |
96 | | simprl 790 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ (1..^𝑁))) → 𝑥 ∈ ℤ) |
97 | | modcyc 12567 |
. . . . . . . . . . . . . 14
⊢ (((𝑦 − 1) ∈ ℝ ∧
𝑁 ∈
ℝ+ ∧ 𝑥
∈ ℤ) → (((𝑦
− 1) + (𝑥 ·
𝑁)) mod 𝑁) = ((𝑦 − 1) mod 𝑁)) |
98 | 94, 95, 96, 97 | syl3anc 1318 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ (1..^𝑁))) → (((𝑦 − 1) + (𝑥 · 𝑁)) mod 𝑁) = ((𝑦 − 1) mod 𝑁)) |
99 | 91, 98 | eqtrd 2644 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ (1..^𝑁))) → ((((𝑥 · 𝑁) + 𝑦) − 1) mod 𝑁) = ((𝑦 − 1) mod 𝑁)) |
100 | 77, 81 | addcomd 10117 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ (1..^𝑁))) → ((𝑥 · 𝑁) + 𝑦) = (𝑦 + (𝑥 · 𝑁))) |
101 | 100 | oveq1d 6564 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ (1..^𝑁))) → (((𝑥 · 𝑁) + 𝑦) mod 𝑁) = ((𝑦 + (𝑥 · 𝑁)) mod 𝑁)) |
102 | 78 | zred 11358 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ (1..^𝑁) → 𝑦 ∈ ℝ) |
103 | 102 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ (1..^𝑁)) → 𝑦 ∈ ℝ) |
104 | 103 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ (1..^𝑁))) → 𝑦 ∈ ℝ) |
105 | | modcyc 12567 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ ℝ ∧ 𝑁 ∈ ℝ+
∧ 𝑥 ∈ ℤ)
→ ((𝑦 + (𝑥 · 𝑁)) mod 𝑁) = (𝑦 mod 𝑁)) |
106 | 104, 95, 96, 105 | syl3anc 1318 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ (1..^𝑁))) → ((𝑦 + (𝑥 · 𝑁)) mod 𝑁) = (𝑦 mod 𝑁)) |
107 | 7, 103 | anim12ci 589 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ (1..^𝑁))) → (𝑦 ∈ ℝ ∧ 𝑁 ∈
ℝ+)) |
108 | | elfzole1 12347 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 ∈ (1..^𝑁) → 1 ≤ 𝑦) |
109 | | 0lt1 10429 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 0 <
1 |
110 | | 0red 9920 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 ∈ (1..^𝑁) → 0 ∈ ℝ) |
111 | | 1red 9934 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 ∈ (1..^𝑁) → 1 ∈ ℝ) |
112 | | ltleletr 10009 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((0
∈ ℝ ∧ 1 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((0 < 1 ∧ 1
≤ 𝑦) → 0 ≤ 𝑦)) |
113 | 110, 111,
102, 112 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 ∈ (1..^𝑁) → ((0 < 1 ∧ 1 ≤ 𝑦) → 0 ≤ 𝑦)) |
114 | 109, 113 | mpani 708 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 ∈ (1..^𝑁) → (1 ≤ 𝑦 → 0 ≤ 𝑦)) |
115 | 108, 114 | mpd 15 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ (1..^𝑁) → 0 ≤ 𝑦) |
116 | | elfzolt2 12348 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ (1..^𝑁) → 𝑦 < 𝑁) |
117 | 115, 116 | jca 553 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ (1..^𝑁) → (0 ≤ 𝑦 ∧ 𝑦 < 𝑁)) |
118 | 117 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ (1..^𝑁)) → (0 ≤ 𝑦 ∧ 𝑦 < 𝑁)) |
119 | 118 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ (1..^𝑁))) → (0 ≤ 𝑦 ∧ 𝑦 < 𝑁)) |
120 | 107, 119 | jca 553 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ (1..^𝑁))) → ((𝑦 ∈ ℝ ∧ 𝑁 ∈ ℝ+) ∧ (0 ≤
𝑦 ∧ 𝑦 < 𝑁))) |
121 | | modid 12557 |
. . . . . . . . . . . . . 14
⊢ (((𝑦 ∈ ℝ ∧ 𝑁 ∈ ℝ+)
∧ (0 ≤ 𝑦 ∧ 𝑦 < 𝑁)) → (𝑦 mod 𝑁) = 𝑦) |
122 | 120, 121 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ (1..^𝑁))) → (𝑦 mod 𝑁) = 𝑦) |
123 | 101, 106,
122 | 3eqtrd 2648 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ (1..^𝑁))) → (((𝑥 · 𝑁) + 𝑦) mod 𝑁) = 𝑦) |
124 | 99, 123 | oveq12d 6567 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ (1..^𝑁))) → (((((𝑥 · 𝑁) + 𝑦) − 1) mod 𝑁) − (((𝑥 · 𝑁) + 𝑦) mod 𝑁)) = (((𝑦 − 1) mod 𝑁) − 𝑦)) |
125 | 75, 124 | sylan9eqr 2666 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ (1..^𝑁))) ∧ 𝐴 = ((𝑥 · 𝑁) + 𝑦)) → (((𝐴 − 1) mod 𝑁) − (𝐴 mod 𝑁)) = (((𝑦 − 1) mod 𝑁) − 𝑦)) |
126 | 7, 93 | anim12ci 589 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ (1..^𝑁))) → ((𝑦 − 1) ∈ ℝ ∧ 𝑁 ∈
ℝ+)) |
127 | | elfzo2 12342 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ (1..^𝑁) ↔ (𝑦 ∈ (ℤ≥‘1)
∧ 𝑁 ∈ ℤ
∧ 𝑦 < 𝑁)) |
128 | | eluz2 11569 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 ∈
(ℤ≥‘1) ↔ (1 ∈ ℤ ∧ 𝑦 ∈ ℤ ∧ 1 ≤
𝑦)) |
129 | | zre 11258 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 ∈ ℤ → 𝑦 ∈
ℝ) |
130 | | zre 11258 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (1 ∈
ℤ → 1 ∈ ℝ) |
131 | | subge0 10420 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑦 ∈ ℝ ∧ 1 ∈
ℝ) → (0 ≤ (𝑦
− 1) ↔ 1 ≤ 𝑦)) |
132 | 129, 130,
131 | syl2anr 494 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((1
∈ ℤ ∧ 𝑦
∈ ℤ) → (0 ≤ (𝑦 − 1) ↔ 1 ≤ 𝑦)) |
133 | 132 | biimp3ar 1425 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((1
∈ ℤ ∧ 𝑦
∈ ℤ ∧ 1 ≤ 𝑦) → 0 ≤ (𝑦 − 1)) |
134 | 128, 133 | sylbi 206 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈
(ℤ≥‘1) → 0 ≤ (𝑦 − 1)) |
135 | 134 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈
(ℤ≥‘1) ∧ 𝑁 ∈ ℤ ∧ 𝑦 < 𝑁) → 0 ≤ (𝑦 − 1)) |
136 | 127, 135 | sylbi 206 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ (1..^𝑁) → 0 ≤ (𝑦 − 1)) |
137 | 136 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ (1..^𝑁)) → 0 ≤ (𝑦 − 1)) |
138 | 137 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ (1..^𝑁))) → 0 ≤ (𝑦 − 1)) |
139 | | eluzelz 11573 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑦 ∈
(ℤ≥‘1) → 𝑦 ∈ ℤ) |
140 | 139 | zred 11358 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 ∈
(ℤ≥‘1) → 𝑦 ∈ ℝ) |
141 | | zre 11258 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
ℝ) |
142 | | ltle 10005 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑦 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (𝑦 < 𝑁 → 𝑦 ≤ 𝑁)) |
143 | 140, 141,
142 | syl2an 493 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑦 ∈
(ℤ≥‘1) ∧ 𝑁 ∈ ℤ) → (𝑦 < 𝑁 → 𝑦 ≤ 𝑁)) |
144 | 143 | 3impia 1253 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑦 ∈
(ℤ≥‘1) ∧ 𝑁 ∈ ℤ ∧ 𝑦 < 𝑁) → 𝑦 ≤ 𝑁) |
145 | 139 | anim1i 590 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑦 ∈
(ℤ≥‘1) ∧ 𝑁 ∈ ℤ) → (𝑦 ∈ ℤ ∧ 𝑁 ∈ ℤ)) |
146 | 145 | 3adant3 1074 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑦 ∈
(ℤ≥‘1) ∧ 𝑁 ∈ ℤ ∧ 𝑦 < 𝑁) → (𝑦 ∈ ℤ ∧ 𝑁 ∈ ℤ)) |
147 | | zlem1lt 11306 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑦 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑦 ≤ 𝑁 ↔ (𝑦 − 1) < 𝑁)) |
148 | 146, 147 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑦 ∈
(ℤ≥‘1) ∧ 𝑁 ∈ ℤ ∧ 𝑦 < 𝑁) → (𝑦 ≤ 𝑁 ↔ (𝑦 − 1) < 𝑁)) |
149 | 144, 148 | mpbid 221 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 ∈
(ℤ≥‘1) ∧ 𝑁 ∈ ℤ ∧ 𝑦 < 𝑁) → (𝑦 − 1) < 𝑁) |
150 | 149 | a1d 25 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈
(ℤ≥‘1) ∧ 𝑁 ∈ ℤ ∧ 𝑦 < 𝑁) → ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑦 − 1) < 𝑁)) |
151 | 127, 150 | sylbi 206 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ (1..^𝑁) → ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑦 − 1) < 𝑁)) |
152 | 151 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ (1..^𝑁)) → ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑦 − 1) < 𝑁)) |
153 | 152 | impcom 445 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ (1..^𝑁))) → (𝑦 − 1) < 𝑁) |
154 | | modid 12557 |
. . . . . . . . . . . . . 14
⊢ ((((𝑦 − 1) ∈ ℝ ∧
𝑁 ∈
ℝ+) ∧ (0 ≤ (𝑦 − 1) ∧ (𝑦 − 1) < 𝑁)) → ((𝑦 − 1) mod 𝑁) = (𝑦 − 1)) |
155 | 126, 138,
153, 154 | syl12anc 1316 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ (1..^𝑁))) → ((𝑦 − 1) mod 𝑁) = (𝑦 − 1)) |
156 | 155 | oveq1d 6564 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ (1..^𝑁))) → (((𝑦 − 1) mod 𝑁) − 𝑦) = ((𝑦 − 1) − 𝑦)) |
157 | | 1cnd 9935 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ (1..^𝑁) → 1 ∈ ℂ) |
158 | 79, 157, 79 | sub32d 10303 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ (1..^𝑁) → ((𝑦 − 1) − 𝑦) = ((𝑦 − 𝑦) − 1)) |
159 | 79 | subidd 10259 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ (1..^𝑁) → (𝑦 − 𝑦) = 0) |
160 | 159 | oveq1d 6564 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ (1..^𝑁) → ((𝑦 − 𝑦) − 1) = (0 −
1)) |
161 | 158, 160 | eqtrd 2644 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ (1..^𝑁) → ((𝑦 − 1) − 𝑦) = (0 − 1)) |
162 | 161 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ (1..^𝑁)) → ((𝑦 − 1) − 𝑦) = (0 − 1)) |
163 | 162 | adantl 481 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ (1..^𝑁))) → ((𝑦 − 1) − 𝑦) = (0 − 1)) |
164 | | df-neg 10148 |
. . . . . . . . . . . . 13
⊢ -1 = (0
− 1) |
165 | 163, 164 | syl6eqr 2662 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ (1..^𝑁))) → ((𝑦 − 1) − 𝑦) = -1) |
166 | 156, 165 | eqtrd 2644 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ (1..^𝑁))) → (((𝑦 − 1) mod 𝑁) − 𝑦) = -1) |
167 | 166 | adantr 480 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ (1..^𝑁))) ∧ 𝐴 = ((𝑥 · 𝑁) + 𝑦)) → (((𝑦 − 1) mod 𝑁) − 𝑦) = -1) |
168 | 125, 167 | eqtrd 2644 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ (1..^𝑁))) ∧ 𝐴 = ((𝑥 · 𝑁) + 𝑦)) → (((𝐴 − 1) mod 𝑁) − (𝐴 mod 𝑁)) = -1) |
169 | 168 | eqcomd 2616 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ (1..^𝑁))) ∧ 𝐴 = ((𝑥 · 𝑁) + 𝑦)) → -1 = (((𝐴 − 1) mod 𝑁) − (𝐴 mod 𝑁))) |
170 | 169 | ex 449 |
. . . . . . 7
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ (1..^𝑁))) → (𝐴 = ((𝑥 · 𝑁) + 𝑦) → -1 = (((𝐴 − 1) mod 𝑁) − (𝐴 mod 𝑁)))) |
171 | 170 | rexlimdvva 3020 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) →
(∃𝑥 ∈ ℤ
∃𝑦 ∈ (1..^𝑁)𝐴 = ((𝑥 · 𝑁) + 𝑦) → -1 = (((𝐴 − 1) mod 𝑁) − (𝐴 mod 𝑁)))) |
172 | 71, 171 | syld 46 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝐴 mod 𝑁) ≠ 0 → -1 = (((𝐴 − 1) mod 𝑁) − (𝐴 mod 𝑁)))) |
173 | 70, 172 | syl5bir 232 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (¬
(𝐴 mod 𝑁) = 0 → -1 = (((𝐴 − 1) mod 𝑁) − (𝐴 mod 𝑁)))) |
174 | 173 | imp 444 |
. . 3
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) ∧ ¬
(𝐴 mod 𝑁) = 0) → -1 = (((𝐴 − 1) mod 𝑁) − (𝐴 mod 𝑁))) |
175 | 69, 174 | ifeqda 4071 |
. 2
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) →
if((𝐴 mod 𝑁) = 0, (𝑁 − 1), -1) = (((𝐴 − 1) mod 𝑁) − (𝐴 mod 𝑁))) |
176 | 175 | eqcomd 2616 |
1
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (((𝐴 − 1) mod 𝑁) − (𝐴 mod 𝑁)) = if((𝐴 mod 𝑁) = 0, (𝑁 − 1), -1)) |