Proof of Theorem modsumfzodifsn
Step | Hyp | Ref
| Expression |
1 | | elfzo0 12508 |
. . . . . 6
⊢ (𝐽 ∈ (0..^𝑁) ↔ (𝐽 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁)) |
2 | | elfzoelz 12470 |
. . . . . . . . 9
⊢ (𝐾 ∈ (1..^𝑁) → 𝐾 ∈ ℤ) |
3 | 2 | zred 11482 |
. . . . . . . 8
⊢ (𝐾 ∈ (1..^𝑁) → 𝐾 ∈ ℝ) |
4 | | nn0re 11301 |
. . . . . . . . 9
⊢ (𝐽 ∈ ℕ0
→ 𝐽 ∈
ℝ) |
5 | 4 | 3ad2ant1 1082 |
. . . . . . . 8
⊢ ((𝐽 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝐽 < 𝑁) → 𝐽 ∈ ℝ) |
6 | | readdcl 10019 |
. . . . . . . 8
⊢ ((𝐾 ∈ ℝ ∧ 𝐽 ∈ ℝ) → (𝐾 + 𝐽) ∈ ℝ) |
7 | 3, 5, 6 | syl2anr 495 |
. . . . . . 7
⊢ (((𝐽 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝐽 < 𝑁) ∧ 𝐾 ∈ (1..^𝑁)) → (𝐾 + 𝐽) ∈ ℝ) |
8 | | nnrp 11842 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℝ+) |
9 | 8 | 3ad2ant2 1083 |
. . . . . . . 8
⊢ ((𝐽 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝐽 < 𝑁) → 𝑁 ∈
ℝ+) |
10 | 9 | adantr 481 |
. . . . . . 7
⊢ (((𝐽 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝐽 < 𝑁) ∧ 𝐾 ∈ (1..^𝑁)) → 𝑁 ∈
ℝ+) |
11 | 7, 10 | jca 554 |
. . . . . 6
⊢ (((𝐽 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝐽 < 𝑁) ∧ 𝐾 ∈ (1..^𝑁)) → ((𝐾 + 𝐽) ∈ ℝ ∧ 𝑁 ∈
ℝ+)) |
12 | 1, 11 | sylanb 489 |
. . . . 5
⊢ ((𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁)) → ((𝐾 + 𝐽) ∈ ℝ ∧ 𝑁 ∈
ℝ+)) |
13 | 12 | adantl 482 |
. . . 4
⊢ (((𝐾 + 𝐽) < 𝑁 ∧ (𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁))) → ((𝐾 + 𝐽) ∈ ℝ ∧ 𝑁 ∈
ℝ+)) |
14 | | elfzo1 12517 |
. . . . . . . . 9
⊢ (𝐾 ∈ (1..^𝑁) ↔ (𝐾 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐾 < 𝑁)) |
15 | | nnnn0 11299 |
. . . . . . . . . 10
⊢ (𝐾 ∈ ℕ → 𝐾 ∈
ℕ0) |
16 | 15 | 3ad2ant1 1082 |
. . . . . . . . 9
⊢ ((𝐾 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐾 < 𝑁) → 𝐾 ∈
ℕ0) |
17 | 14, 16 | sylbi 207 |
. . . . . . . 8
⊢ (𝐾 ∈ (1..^𝑁) → 𝐾 ∈
ℕ0) |
18 | | elfzonn0 12512 |
. . . . . . . 8
⊢ (𝐽 ∈ (0..^𝑁) → 𝐽 ∈
ℕ0) |
19 | | nn0addcl 11328 |
. . . . . . . 8
⊢ ((𝐾 ∈ ℕ0
∧ 𝐽 ∈
ℕ0) → (𝐾 + 𝐽) ∈
ℕ0) |
20 | 17, 18, 19 | syl2anr 495 |
. . . . . . 7
⊢ ((𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁)) → (𝐾 + 𝐽) ∈
ℕ0) |
21 | 20 | adantl 482 |
. . . . . 6
⊢ (((𝐾 + 𝐽) < 𝑁 ∧ (𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁))) → (𝐾 + 𝐽) ∈
ℕ0) |
22 | 21 | nn0ge0d 11354 |
. . . . 5
⊢ (((𝐾 + 𝐽) < 𝑁 ∧ (𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁))) → 0 ≤ (𝐾 + 𝐽)) |
23 | | simpl 473 |
. . . . 5
⊢ (((𝐾 + 𝐽) < 𝑁 ∧ (𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁))) → (𝐾 + 𝐽) < 𝑁) |
24 | 22, 23 | jca 554 |
. . . 4
⊢ (((𝐾 + 𝐽) < 𝑁 ∧ (𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁))) → (0 ≤ (𝐾 + 𝐽) ∧ (𝐾 + 𝐽) < 𝑁)) |
25 | | modid 12695 |
. . . 4
⊢ ((((𝐾 + 𝐽) ∈ ℝ ∧ 𝑁 ∈ ℝ+) ∧ (0 ≤
(𝐾 + 𝐽) ∧ (𝐾 + 𝐽) < 𝑁)) → ((𝐾 + 𝐽) mod 𝑁) = (𝐾 + 𝐽)) |
26 | 13, 24, 25 | syl2anc 693 |
. . 3
⊢ (((𝐾 + 𝐽) < 𝑁 ∧ (𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁))) → ((𝐾 + 𝐽) mod 𝑁) = (𝐾 + 𝐽)) |
27 | | simp2 1062 |
. . . . . . . 8
⊢ ((𝐽 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝐽 < 𝑁) → 𝑁 ∈ ℕ) |
28 | 1, 27 | sylbi 207 |
. . . . . . 7
⊢ (𝐽 ∈ (0..^𝑁) → 𝑁 ∈ ℕ) |
29 | 28 | adantr 481 |
. . . . . 6
⊢ ((𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁)) → 𝑁 ∈ ℕ) |
30 | 29 | adantl 482 |
. . . . 5
⊢ (((𝐾 + 𝐽) < 𝑁 ∧ (𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁))) → 𝑁 ∈ ℕ) |
31 | | elfzo0 12508 |
. . . . 5
⊢ ((𝐾 + 𝐽) ∈ (0..^𝑁) ↔ ((𝐾 + 𝐽) ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ (𝐾 + 𝐽) < 𝑁)) |
32 | 21, 30, 23, 31 | syl3anbrc 1246 |
. . . 4
⊢ (((𝐾 + 𝐽) < 𝑁 ∧ (𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁))) → (𝐾 + 𝐽) ∈ (0..^𝑁)) |
33 | 2 | zcnd 11483 |
. . . . . . . 8
⊢ (𝐾 ∈ (1..^𝑁) → 𝐾 ∈ ℂ) |
34 | 33 | adantl 482 |
. . . . . . 7
⊢ ((𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁)) → 𝐾 ∈ ℂ) |
35 | | 0cnd 10033 |
. . . . . . 7
⊢ ((𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁)) → 0 ∈ ℂ) |
36 | | elfzoelz 12470 |
. . . . . . . . 9
⊢ (𝐽 ∈ (0..^𝑁) → 𝐽 ∈ ℤ) |
37 | 36 | zcnd 11483 |
. . . . . . . 8
⊢ (𝐽 ∈ (0..^𝑁) → 𝐽 ∈ ℂ) |
38 | 37 | adantr 481 |
. . . . . . 7
⊢ ((𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁)) → 𝐽 ∈ ℂ) |
39 | | nnne0 11053 |
. . . . . . . . . 10
⊢ (𝐾 ∈ ℕ → 𝐾 ≠ 0) |
40 | 39 | 3ad2ant1 1082 |
. . . . . . . . 9
⊢ ((𝐾 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐾 < 𝑁) → 𝐾 ≠ 0) |
41 | 14, 40 | sylbi 207 |
. . . . . . . 8
⊢ (𝐾 ∈ (1..^𝑁) → 𝐾 ≠ 0) |
42 | 41 | adantl 482 |
. . . . . . 7
⊢ ((𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁)) → 𝐾 ≠ 0) |
43 | 34, 35, 38, 42 | addneintr2d 10244 |
. . . . . 6
⊢ ((𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁)) → (𝐾 + 𝐽) ≠ (0 + 𝐽)) |
44 | 43 | adantl 482 |
. . . . 5
⊢ (((𝐾 + 𝐽) < 𝑁 ∧ (𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁))) → (𝐾 + 𝐽) ≠ (0 + 𝐽)) |
45 | 38 | adantl 482 |
. . . . . 6
⊢ (((𝐾 + 𝐽) < 𝑁 ∧ (𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁))) → 𝐽 ∈ ℂ) |
46 | | addid2 10219 |
. . . . . . 7
⊢ (𝐽 ∈ ℂ → (0 +
𝐽) = 𝐽) |
47 | 46 | eqcomd 2628 |
. . . . . 6
⊢ (𝐽 ∈ ℂ → 𝐽 = (0 + 𝐽)) |
48 | 45, 47 | syl 17 |
. . . . 5
⊢ (((𝐾 + 𝐽) < 𝑁 ∧ (𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁))) → 𝐽 = (0 + 𝐽)) |
49 | 44, 48 | neeqtrrd 2868 |
. . . 4
⊢ (((𝐾 + 𝐽) < 𝑁 ∧ (𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁))) → (𝐾 + 𝐽) ≠ 𝐽) |
50 | | eldifsn 4317 |
. . . 4
⊢ ((𝐾 + 𝐽) ∈ ((0..^𝑁) ∖ {𝐽}) ↔ ((𝐾 + 𝐽) ∈ (0..^𝑁) ∧ (𝐾 + 𝐽) ≠ 𝐽)) |
51 | 32, 49, 50 | sylanbrc 698 |
. . 3
⊢ (((𝐾 + 𝐽) < 𝑁 ∧ (𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁))) → (𝐾 + 𝐽) ∈ ((0..^𝑁) ∖ {𝐽})) |
52 | 26, 51 | eqeltrd 2701 |
. 2
⊢ (((𝐾 + 𝐽) < 𝑁 ∧ (𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁))) → ((𝐾 + 𝐽) mod 𝑁) ∈ ((0..^𝑁) ∖ {𝐽})) |
53 | | elfzoel2 12469 |
. . . . . . . . . . . . . 14
⊢ (𝐽 ∈ (0..^𝑁) → 𝑁 ∈ ℤ) |
54 | 53 | zcnd 11483 |
. . . . . . . . . . . . 13
⊢ (𝐽 ∈ (0..^𝑁) → 𝑁 ∈ ℂ) |
55 | 54 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁)) → 𝑁 ∈ ℂ) |
56 | 55 | adantl 482 |
. . . . . . . . . . 11
⊢ ((¬
(𝐾 + 𝐽) < 𝑁 ∧ (𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁))) → 𝑁 ∈ ℂ) |
57 | 56 | mulm1d 10482 |
. . . . . . . . . 10
⊢ ((¬
(𝐾 + 𝐽) < 𝑁 ∧ (𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁))) → (-1 · 𝑁) = -𝑁) |
58 | 57 | oveq2d 6666 |
. . . . . . . . 9
⊢ ((¬
(𝐾 + 𝐽) < 𝑁 ∧ (𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁))) → ((𝐾 + 𝐽) + (-1 · 𝑁)) = ((𝐾 + 𝐽) + -𝑁)) |
59 | | zaddcl 11417 |
. . . . . . . . . . . . . 14
⊢ ((𝐾 ∈ ℤ ∧ 𝐽 ∈ ℤ) → (𝐾 + 𝐽) ∈ ℤ) |
60 | 2, 36, 59 | syl2anr 495 |
. . . . . . . . . . . . 13
⊢ ((𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁)) → (𝐾 + 𝐽) ∈ ℤ) |
61 | 60 | zcnd 11483 |
. . . . . . . . . . . 12
⊢ ((𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁)) → (𝐾 + 𝐽) ∈ ℂ) |
62 | 61, 55 | jca 554 |
. . . . . . . . . . 11
⊢ ((𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁)) → ((𝐾 + 𝐽) ∈ ℂ ∧ 𝑁 ∈ ℂ)) |
63 | 62 | adantl 482 |
. . . . . . . . . 10
⊢ ((¬
(𝐾 + 𝐽) < 𝑁 ∧ (𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁))) → ((𝐾 + 𝐽) ∈ ℂ ∧ 𝑁 ∈ ℂ)) |
64 | | negsub 10329 |
. . . . . . . . . 10
⊢ (((𝐾 + 𝐽) ∈ ℂ ∧ 𝑁 ∈ ℂ) → ((𝐾 + 𝐽) + -𝑁) = ((𝐾 + 𝐽) − 𝑁)) |
65 | 63, 64 | syl 17 |
. . . . . . . . 9
⊢ ((¬
(𝐾 + 𝐽) < 𝑁 ∧ (𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁))) → ((𝐾 + 𝐽) + -𝑁) = ((𝐾 + 𝐽) − 𝑁)) |
66 | 58, 65 | eqtrd 2656 |
. . . . . . . 8
⊢ ((¬
(𝐾 + 𝐽) < 𝑁 ∧ (𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁))) → ((𝐾 + 𝐽) + (-1 · 𝑁)) = ((𝐾 + 𝐽) − 𝑁)) |
67 | 66 | oveq1d 6665 |
. . . . . . 7
⊢ ((¬
(𝐾 + 𝐽) < 𝑁 ∧ (𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁))) → (((𝐾 + 𝐽) + (-1 · 𝑁)) mod 𝑁) = (((𝐾 + 𝐽) − 𝑁) mod 𝑁)) |
68 | 2, 36, 59 | syl2an 494 |
. . . . . . . . . . . . 13
⊢ ((𝐾 ∈ (1..^𝑁) ∧ 𝐽 ∈ (0..^𝑁)) → (𝐾 + 𝐽) ∈ ℤ) |
69 | 68 | zred 11482 |
. . . . . . . . . . . 12
⊢ ((𝐾 ∈ (1..^𝑁) ∧ 𝐽 ∈ (0..^𝑁)) → (𝐾 + 𝐽) ∈ ℝ) |
70 | 69 | ancoms 469 |
. . . . . . . . . . 11
⊢ ((𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁)) → (𝐾 + 𝐽) ∈ ℝ) |
71 | 53 | zred 11482 |
. . . . . . . . . . . 12
⊢ (𝐽 ∈ (0..^𝑁) → 𝑁 ∈ ℝ) |
72 | 71 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁)) → 𝑁 ∈ ℝ) |
73 | 70, 72 | resubcld 10458 |
. . . . . . . . . 10
⊢ ((𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁)) → ((𝐾 + 𝐽) − 𝑁) ∈ ℝ) |
74 | 73 | adantl 482 |
. . . . . . . . 9
⊢ ((¬
(𝐾 + 𝐽) < 𝑁 ∧ (𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁))) → ((𝐾 + 𝐽) − 𝑁) ∈ ℝ) |
75 | 27 | nnrpd 11870 |
. . . . . . . . . . . 12
⊢ ((𝐽 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝐽 < 𝑁) → 𝑁 ∈
ℝ+) |
76 | 1, 75 | sylbi 207 |
. . . . . . . . . . 11
⊢ (𝐽 ∈ (0..^𝑁) → 𝑁 ∈
ℝ+) |
77 | 76 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁)) → 𝑁 ∈
ℝ+) |
78 | 77 | adantl 482 |
. . . . . . . . 9
⊢ ((¬
(𝐾 + 𝐽) < 𝑁 ∧ (𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁))) → 𝑁 ∈
ℝ+) |
79 | | nnre 11027 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐾 ∈ ℕ → 𝐾 ∈
ℝ) |
80 | 79 | 3ad2ant1 1082 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐾 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐾 < 𝑁) → 𝐾 ∈ ℝ) |
81 | 80 | adantl 482 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐽 ∈ ℕ0
∧ 𝐽 < 𝑁) ∧ (𝐾 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐾 < 𝑁)) → 𝐾 ∈ ℝ) |
82 | 4 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐽 ∈ ℕ0
∧ 𝐽 < 𝑁) → 𝐽 ∈ ℝ) |
83 | 82 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐽 ∈ ℕ0
∧ 𝐽 < 𝑁) ∧ (𝐾 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐾 < 𝑁)) → 𝐽 ∈ ℝ) |
84 | | nnre 11027 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℝ) |
85 | 84 | 3ad2ant2 1083 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐾 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐾 < 𝑁) → 𝑁 ∈ ℝ) |
86 | 85 | adantl 482 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐽 ∈ ℕ0
∧ 𝐽 < 𝑁) ∧ (𝐾 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐾 < 𝑁)) → 𝑁 ∈ ℝ) |
87 | | simp3 1063 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐾 ∈ ℝ ∧ 𝐽 ∈ ℝ ∧ 𝑁 ∈ ℝ) → 𝑁 ∈
ℝ) |
88 | 6 | 3adant3 1081 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐾 ∈ ℝ ∧ 𝐽 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (𝐾 + 𝐽) ∈ ℝ) |
89 | 87, 88 | lenltd 10183 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐾 ∈ ℝ ∧ 𝐽 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (𝑁 ≤ (𝐾 + 𝐽) ↔ ¬ (𝐾 + 𝐽) < 𝑁)) |
90 | 89 | biimprd 238 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐾 ∈ ℝ ∧ 𝐽 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (¬
(𝐾 + 𝐽) < 𝑁 → 𝑁 ≤ (𝐾 + 𝐽))) |
91 | 88, 87 | subge0d 10617 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐾 ∈ ℝ ∧ 𝐽 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (0 ≤
((𝐾 + 𝐽) − 𝑁) ↔ 𝑁 ≤ (𝐾 + 𝐽))) |
92 | 90, 91 | sylibrd 249 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐾 ∈ ℝ ∧ 𝐽 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (¬
(𝐾 + 𝐽) < 𝑁 → 0 ≤ ((𝐾 + 𝐽) − 𝑁))) |
93 | 81, 83, 86, 92 | syl3anc 1326 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐽 ∈ ℕ0
∧ 𝐽 < 𝑁) ∧ (𝐾 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐾 < 𝑁)) → (¬ (𝐾 + 𝐽) < 𝑁 → 0 ≤ ((𝐾 + 𝐽) − 𝑁))) |
94 | 82, 80 | anim12ci 591 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐽 ∈ ℕ0
∧ 𝐽 < 𝑁) ∧ (𝐾 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐾 < 𝑁)) → (𝐾 ∈ ℝ ∧ 𝐽 ∈ ℝ)) |
95 | 84, 84 | jca 554 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑁 ∈ ℕ → (𝑁 ∈ ℝ ∧ 𝑁 ∈
ℝ)) |
96 | 95 | 3ad2ant2 1083 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐾 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐾 < 𝑁) → (𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ)) |
97 | 96 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐽 ∈ ℕ0
∧ 𝐽 < 𝑁) ∧ (𝐾 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐾 < 𝑁)) → (𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ)) |
98 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐽 ∈ ℕ0
∧ 𝐽 < 𝑁) → 𝐽 < 𝑁) |
99 | | simp3 1063 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐾 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐾 < 𝑁) → 𝐾 < 𝑁) |
100 | 98, 99 | anim12ci 591 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐽 ∈ ℕ0
∧ 𝐽 < 𝑁) ∧ (𝐾 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐾 < 𝑁)) → (𝐾 < 𝑁 ∧ 𝐽 < 𝑁)) |
101 | 94, 97, 100 | jca31 557 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐽 ∈ ℕ0
∧ 𝐽 < 𝑁) ∧ (𝐾 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐾 < 𝑁)) → (((𝐾 ∈ ℝ ∧ 𝐽 ∈ ℝ) ∧ (𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ)) ∧ (𝐾 < 𝑁 ∧ 𝐽 < 𝑁))) |
102 | | lt2add 10513 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐾 ∈ ℝ ∧ 𝐽 ∈ ℝ) ∧ (𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ)) → ((𝐾 < 𝑁 ∧ 𝐽 < 𝑁) → (𝐾 + 𝐽) < (𝑁 + 𝑁))) |
103 | 102 | imp 445 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐾 ∈ ℝ ∧ 𝐽 ∈ ℝ) ∧ (𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ)) ∧ (𝐾 < 𝑁 ∧ 𝐽 < 𝑁)) → (𝐾 + 𝐽) < (𝑁 + 𝑁)) |
104 | 101, 103 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐽 ∈ ℕ0
∧ 𝐽 < 𝑁) ∧ (𝐾 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐾 < 𝑁)) → (𝐾 + 𝐽) < (𝑁 + 𝑁)) |
105 | 80, 82, 6 | syl2anr 495 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐽 ∈ ℕ0
∧ 𝐽 < 𝑁) ∧ (𝐾 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐾 < 𝑁)) → (𝐾 + 𝐽) ∈ ℝ) |
106 | | ltsubadd 10498 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐾 + 𝐽) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (((𝐾 + 𝐽) − 𝑁) < 𝑁 ↔ (𝐾 + 𝐽) < (𝑁 + 𝑁))) |
107 | 105, 86, 86, 106 | syl3anc 1326 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐽 ∈ ℕ0
∧ 𝐽 < 𝑁) ∧ (𝐾 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐾 < 𝑁)) → (((𝐾 + 𝐽) − 𝑁) < 𝑁 ↔ (𝐾 + 𝐽) < (𝑁 + 𝑁))) |
108 | 104, 107 | mpbird 247 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐽 ∈ ℕ0
∧ 𝐽 < 𝑁) ∧ (𝐾 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐾 < 𝑁)) → ((𝐾 + 𝐽) − 𝑁) < 𝑁) |
109 | 93, 108 | jctird 567 |
. . . . . . . . . . . . . . 15
⊢ (((𝐽 ∈ ℕ0
∧ 𝐽 < 𝑁) ∧ (𝐾 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐾 < 𝑁)) → (¬ (𝐾 + 𝐽) < 𝑁 → (0 ≤ ((𝐾 + 𝐽) − 𝑁) ∧ ((𝐾 + 𝐽) − 𝑁) < 𝑁))) |
110 | 109 | ex 450 |
. . . . . . . . . . . . . 14
⊢ ((𝐽 ∈ ℕ0
∧ 𝐽 < 𝑁) → ((𝐾 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐾 < 𝑁) → (¬ (𝐾 + 𝐽) < 𝑁 → (0 ≤ ((𝐾 + 𝐽) − 𝑁) ∧ ((𝐾 + 𝐽) − 𝑁) < 𝑁)))) |
111 | 14, 110 | syl5bi 232 |
. . . . . . . . . . . . 13
⊢ ((𝐽 ∈ ℕ0
∧ 𝐽 < 𝑁) → (𝐾 ∈ (1..^𝑁) → (¬ (𝐾 + 𝐽) < 𝑁 → (0 ≤ ((𝐾 + 𝐽) − 𝑁) ∧ ((𝐾 + 𝐽) − 𝑁) < 𝑁)))) |
112 | 111 | 3adant2 1080 |
. . . . . . . . . . . 12
⊢ ((𝐽 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝐽 < 𝑁) → (𝐾 ∈ (1..^𝑁) → (¬ (𝐾 + 𝐽) < 𝑁 → (0 ≤ ((𝐾 + 𝐽) − 𝑁) ∧ ((𝐾 + 𝐽) − 𝑁) < 𝑁)))) |
113 | 1, 112 | sylbi 207 |
. . . . . . . . . . 11
⊢ (𝐽 ∈ (0..^𝑁) → (𝐾 ∈ (1..^𝑁) → (¬ (𝐾 + 𝐽) < 𝑁 → (0 ≤ ((𝐾 + 𝐽) − 𝑁) ∧ ((𝐾 + 𝐽) − 𝑁) < 𝑁)))) |
114 | 113 | imp 445 |
. . . . . . . . . 10
⊢ ((𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁)) → (¬ (𝐾 + 𝐽) < 𝑁 → (0 ≤ ((𝐾 + 𝐽) − 𝑁) ∧ ((𝐾 + 𝐽) − 𝑁) < 𝑁))) |
115 | 114 | impcom 446 |
. . . . . . . . 9
⊢ ((¬
(𝐾 + 𝐽) < 𝑁 ∧ (𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁))) → (0 ≤ ((𝐾 + 𝐽) − 𝑁) ∧ ((𝐾 + 𝐽) − 𝑁) < 𝑁)) |
116 | 74, 78, 115 | jca31 557 |
. . . . . . . 8
⊢ ((¬
(𝐾 + 𝐽) < 𝑁 ∧ (𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁))) → ((((𝐾 + 𝐽) − 𝑁) ∈ ℝ ∧ 𝑁 ∈ ℝ+) ∧ (0 ≤
((𝐾 + 𝐽) − 𝑁) ∧ ((𝐾 + 𝐽) − 𝑁) < 𝑁))) |
117 | | modid 12695 |
. . . . . . . 8
⊢
(((((𝐾 + 𝐽) − 𝑁) ∈ ℝ ∧ 𝑁 ∈ ℝ+) ∧ (0 ≤
((𝐾 + 𝐽) − 𝑁) ∧ ((𝐾 + 𝐽) − 𝑁) < 𝑁)) → (((𝐾 + 𝐽) − 𝑁) mod 𝑁) = ((𝐾 + 𝐽) − 𝑁)) |
118 | 116, 117 | syl 17 |
. . . . . . 7
⊢ ((¬
(𝐾 + 𝐽) < 𝑁 ∧ (𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁))) → (((𝐾 + 𝐽) − 𝑁) mod 𝑁) = ((𝐾 + 𝐽) − 𝑁)) |
119 | 67, 118 | eqtrd 2656 |
. . . . . 6
⊢ ((¬
(𝐾 + 𝐽) < 𝑁 ∧ (𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁))) → (((𝐾 + 𝐽) + (-1 · 𝑁)) mod 𝑁) = ((𝐾 + 𝐽) − 𝑁)) |
120 | 119 | eqcomd 2628 |
. . . . 5
⊢ ((¬
(𝐾 + 𝐽) < 𝑁 ∧ (𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁))) → ((𝐾 + 𝐽) − 𝑁) = (((𝐾 + 𝐽) + (-1 · 𝑁)) mod 𝑁)) |
121 | 1, 9 | sylbi 207 |
. . . . . . 7
⊢ (𝐽 ∈ (0..^𝑁) → 𝑁 ∈
ℝ+) |
122 | 121 | adantr 481 |
. . . . . 6
⊢ ((𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁)) → 𝑁 ∈
ℝ+) |
123 | | neg1z 11413 |
. . . . . . 7
⊢ -1 ∈
ℤ |
124 | 123 | a1i 11 |
. . . . . 6
⊢ ((¬
(𝐾 + 𝐽) < 𝑁 ∧ (𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁))) → -1 ∈
ℤ) |
125 | | modcyc 12705 |
. . . . . 6
⊢ (((𝐾 + 𝐽) ∈ ℝ ∧ 𝑁 ∈ ℝ+ ∧ -1 ∈
ℤ) → (((𝐾 +
𝐽) + (-1 · 𝑁)) mod 𝑁) = ((𝐾 + 𝐽) mod 𝑁)) |
126 | 70, 122, 124, 125 | syl2an23an 1387 |
. . . . 5
⊢ ((¬
(𝐾 + 𝐽) < 𝑁 ∧ (𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁))) → (((𝐾 + 𝐽) + (-1 · 𝑁)) mod 𝑁) = ((𝐾 + 𝐽) mod 𝑁)) |
127 | 120, 126 | eqtrd 2656 |
. . . 4
⊢ ((¬
(𝐾 + 𝐽) < 𝑁 ∧ (𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁))) → ((𝐾 + 𝐽) − 𝑁) = ((𝐾 + 𝐽) mod 𝑁)) |
128 | 127 | eqcomd 2628 |
. . 3
⊢ ((¬
(𝐾 + 𝐽) < 𝑁 ∧ (𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁))) → ((𝐾 + 𝐽) mod 𝑁) = ((𝐾 + 𝐽) − 𝑁)) |
129 | 53 | adantr 481 |
. . . . . . . 8
⊢ ((𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁)) → 𝑁 ∈ ℤ) |
130 | 60, 129 | zsubcld 11487 |
. . . . . . 7
⊢ ((𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁)) → ((𝐾 + 𝐽) − 𝑁) ∈ ℤ) |
131 | 130 | adantl 482 |
. . . . . 6
⊢ ((¬
(𝐾 + 𝐽) < 𝑁 ∧ (𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁))) → ((𝐾 + 𝐽) − 𝑁) ∈ ℤ) |
132 | 3 | adantl 482 |
. . . . . . . 8
⊢ ((𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁)) → 𝐾 ∈ ℝ) |
133 | 36 | zred 11482 |
. . . . . . . . 9
⊢ (𝐽 ∈ (0..^𝑁) → 𝐽 ∈ ℝ) |
134 | 133 | adantr 481 |
. . . . . . . 8
⊢ ((𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁)) → 𝐽 ∈ ℝ) |
135 | 91 | biimprd 238 |
. . . . . . . . 9
⊢ ((𝐾 ∈ ℝ ∧ 𝐽 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (𝑁 ≤ (𝐾 + 𝐽) → 0 ≤ ((𝐾 + 𝐽) − 𝑁))) |
136 | 89, 135 | sylbird 250 |
. . . . . . . 8
⊢ ((𝐾 ∈ ℝ ∧ 𝐽 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (¬
(𝐾 + 𝐽) < 𝑁 → 0 ≤ ((𝐾 + 𝐽) − 𝑁))) |
137 | 132, 134,
72, 136 | syl3anc 1326 |
. . . . . . 7
⊢ ((𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁)) → (¬ (𝐾 + 𝐽) < 𝑁 → 0 ≤ ((𝐾 + 𝐽) − 𝑁))) |
138 | 137 | impcom 446 |
. . . . . 6
⊢ ((¬
(𝐾 + 𝐽) < 𝑁 ∧ (𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁))) → 0 ≤ ((𝐾 + 𝐽) − 𝑁)) |
139 | | elnn0z 11390 |
. . . . . 6
⊢ (((𝐾 + 𝐽) − 𝑁) ∈ ℕ0 ↔ (((𝐾 + 𝐽) − 𝑁) ∈ ℤ ∧ 0 ≤ ((𝐾 + 𝐽) − 𝑁))) |
140 | 131, 138,
139 | sylanbrc 698 |
. . . . 5
⊢ ((¬
(𝐾 + 𝐽) < 𝑁 ∧ (𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁))) → ((𝐾 + 𝐽) − 𝑁) ∈
ℕ0) |
141 | 29 | adantl 482 |
. . . . 5
⊢ ((¬
(𝐾 + 𝐽) < 𝑁 ∧ (𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁))) → 𝑁 ∈ ℕ) |
142 | 101 | expcom 451 |
. . . . . . . . . . . . 13
⊢ ((𝐾 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐾 < 𝑁) → ((𝐽 ∈ ℕ0 ∧ 𝐽 < 𝑁) → (((𝐾 ∈ ℝ ∧ 𝐽 ∈ ℝ) ∧ (𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ)) ∧ (𝐾 < 𝑁 ∧ 𝐽 < 𝑁)))) |
143 | 14, 142 | sylbi 207 |
. . . . . . . . . . . 12
⊢ (𝐾 ∈ (1..^𝑁) → ((𝐽 ∈ ℕ0 ∧ 𝐽 < 𝑁) → (((𝐾 ∈ ℝ ∧ 𝐽 ∈ ℝ) ∧ (𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ)) ∧ (𝐾 < 𝑁 ∧ 𝐽 < 𝑁)))) |
144 | 143 | com12 32 |
. . . . . . . . . . 11
⊢ ((𝐽 ∈ ℕ0
∧ 𝐽 < 𝑁) → (𝐾 ∈ (1..^𝑁) → (((𝐾 ∈ ℝ ∧ 𝐽 ∈ ℝ) ∧ (𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ)) ∧ (𝐾 < 𝑁 ∧ 𝐽 < 𝑁)))) |
145 | 144 | 3adant2 1080 |
. . . . . . . . . 10
⊢ ((𝐽 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝐽 < 𝑁) → (𝐾 ∈ (1..^𝑁) → (((𝐾 ∈ ℝ ∧ 𝐽 ∈ ℝ) ∧ (𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ)) ∧ (𝐾 < 𝑁 ∧ 𝐽 < 𝑁)))) |
146 | 1, 145 | sylbi 207 |
. . . . . . . . 9
⊢ (𝐽 ∈ (0..^𝑁) → (𝐾 ∈ (1..^𝑁) → (((𝐾 ∈ ℝ ∧ 𝐽 ∈ ℝ) ∧ (𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ)) ∧ (𝐾 < 𝑁 ∧ 𝐽 < 𝑁)))) |
147 | 146 | imp 445 |
. . . . . . . 8
⊢ ((𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁)) → (((𝐾 ∈ ℝ ∧ 𝐽 ∈ ℝ) ∧ (𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ)) ∧ (𝐾 < 𝑁 ∧ 𝐽 < 𝑁))) |
148 | 147, 103 | syl 17 |
. . . . . . 7
⊢ ((𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁)) → (𝐾 + 𝐽) < (𝑁 + 𝑁)) |
149 | 4 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((𝐽 ∈ ℕ0
∧ 𝑁 ∈ ℕ)
→ 𝐽 ∈
ℝ) |
150 | 3, 149, 6 | syl2anr 495 |
. . . . . . . . . . . . 13
⊢ (((𝐽 ∈ ℕ0
∧ 𝑁 ∈ ℕ)
∧ 𝐾 ∈ (1..^𝑁)) → (𝐾 + 𝐽) ∈ ℝ) |
151 | 84 | adantl 482 |
. . . . . . . . . . . . . 14
⊢ ((𝐽 ∈ ℕ0
∧ 𝑁 ∈ ℕ)
→ 𝑁 ∈
ℝ) |
152 | 151 | adantr 481 |
. . . . . . . . . . . . 13
⊢ (((𝐽 ∈ ℕ0
∧ 𝑁 ∈ ℕ)
∧ 𝐾 ∈ (1..^𝑁)) → 𝑁 ∈ ℝ) |
153 | 150, 152,
152 | 3jca 1242 |
. . . . . . . . . . . 12
⊢ (((𝐽 ∈ ℕ0
∧ 𝑁 ∈ ℕ)
∧ 𝐾 ∈ (1..^𝑁)) → ((𝐾 + 𝐽) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ)) |
154 | 153 | ex 450 |
. . . . . . . . . . 11
⊢ ((𝐽 ∈ ℕ0
∧ 𝑁 ∈ ℕ)
→ (𝐾 ∈ (1..^𝑁) → ((𝐾 + 𝐽) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ))) |
155 | 154 | 3adant3 1081 |
. . . . . . . . . 10
⊢ ((𝐽 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝐽 < 𝑁) → (𝐾 ∈ (1..^𝑁) → ((𝐾 + 𝐽) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ))) |
156 | 1, 155 | sylbi 207 |
. . . . . . . . 9
⊢ (𝐽 ∈ (0..^𝑁) → (𝐾 ∈ (1..^𝑁) → ((𝐾 + 𝐽) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ))) |
157 | 156 | imp 445 |
. . . . . . . 8
⊢ ((𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁)) → ((𝐾 + 𝐽) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ)) |
158 | 157, 106 | syl 17 |
. . . . . . 7
⊢ ((𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁)) → (((𝐾 + 𝐽) − 𝑁) < 𝑁 ↔ (𝐾 + 𝐽) < (𝑁 + 𝑁))) |
159 | 148, 158 | mpbird 247 |
. . . . . 6
⊢ ((𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁)) → ((𝐾 + 𝐽) − 𝑁) < 𝑁) |
160 | 159 | adantl 482 |
. . . . 5
⊢ ((¬
(𝐾 + 𝐽) < 𝑁 ∧ (𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁))) → ((𝐾 + 𝐽) − 𝑁) < 𝑁) |
161 | | elfzo0 12508 |
. . . . 5
⊢ (((𝐾 + 𝐽) − 𝑁) ∈ (0..^𝑁) ↔ (((𝐾 + 𝐽) − 𝑁) ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ ((𝐾 + 𝐽) − 𝑁) < 𝑁)) |
162 | 140, 141,
160, 161 | syl3anbrc 1246 |
. . . 4
⊢ ((¬
(𝐾 + 𝐽) < 𝑁 ∧ (𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁))) → ((𝐾 + 𝐽) − 𝑁) ∈ (0..^𝑁)) |
163 | | nncn 11028 |
. . . . . . . . . . 11
⊢ (𝐾 ∈ ℕ → 𝐾 ∈
ℂ) |
164 | | nncn 11028 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℂ) |
165 | | subcl 10280 |
. . . . . . . . . . 11
⊢ ((𝐾 ∈ ℂ ∧ 𝑁 ∈ ℂ) → (𝐾 − 𝑁) ∈ ℂ) |
166 | 163, 164,
165 | syl2an 494 |
. . . . . . . . . 10
⊢ ((𝐾 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝐾 − 𝑁) ∈ ℂ) |
167 | 166 | 3adant3 1081 |
. . . . . . . . 9
⊢ ((𝐾 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐾 < 𝑁) → (𝐾 − 𝑁) ∈ ℂ) |
168 | 14, 167 | sylbi 207 |
. . . . . . . 8
⊢ (𝐾 ∈ (1..^𝑁) → (𝐾 − 𝑁) ∈ ℂ) |
169 | 168 | adantl 482 |
. . . . . . 7
⊢ ((𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁)) → (𝐾 − 𝑁) ∈ ℂ) |
170 | 169 | adantl 482 |
. . . . . 6
⊢ ((¬
(𝐾 + 𝐽) < 𝑁 ∧ (𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁))) → (𝐾 − 𝑁) ∈ ℂ) |
171 | | 0cnd 10033 |
. . . . . 6
⊢ ((¬
(𝐾 + 𝐽) < 𝑁 ∧ (𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁))) → 0 ∈
ℂ) |
172 | 38 | adantl 482 |
. . . . . 6
⊢ ((¬
(𝐾 + 𝐽) < 𝑁 ∧ (𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁))) → 𝐽 ∈ ℂ) |
173 | | elfzoel2 12469 |
. . . . . . . . . 10
⊢ (𝐾 ∈ (1..^𝑁) → 𝑁 ∈ ℤ) |
174 | 173 | zcnd 11483 |
. . . . . . . . 9
⊢ (𝐾 ∈ (1..^𝑁) → 𝑁 ∈ ℂ) |
175 | 80, 99 | ltned 10173 |
. . . . . . . . . 10
⊢ ((𝐾 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐾 < 𝑁) → 𝐾 ≠ 𝑁) |
176 | 14, 175 | sylbi 207 |
. . . . . . . . 9
⊢ (𝐾 ∈ (1..^𝑁) → 𝐾 ≠ 𝑁) |
177 | 33, 174, 176 | subne0d 10401 |
. . . . . . . 8
⊢ (𝐾 ∈ (1..^𝑁) → (𝐾 − 𝑁) ≠ 0) |
178 | 177 | adantl 482 |
. . . . . . 7
⊢ ((𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁)) → (𝐾 − 𝑁) ≠ 0) |
179 | 178 | adantl 482 |
. . . . . 6
⊢ ((¬
(𝐾 + 𝐽) < 𝑁 ∧ (𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁))) → (𝐾 − 𝑁) ≠ 0) |
180 | 170, 171,
172, 179 | addneintr2d 10244 |
. . . . 5
⊢ ((¬
(𝐾 + 𝐽) < 𝑁 ∧ (𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁))) → ((𝐾 − 𝑁) + 𝐽) ≠ (0 + 𝐽)) |
181 | 34, 38, 55 | 3jca 1242 |
. . . . . . 7
⊢ ((𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁)) → (𝐾 ∈ ℂ ∧ 𝐽 ∈ ℂ ∧ 𝑁 ∈ ℂ)) |
182 | 181 | adantl 482 |
. . . . . 6
⊢ ((¬
(𝐾 + 𝐽) < 𝑁 ∧ (𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁))) → (𝐾 ∈ ℂ ∧ 𝐽 ∈ ℂ ∧ 𝑁 ∈ ℂ)) |
183 | | addsub 10292 |
. . . . . 6
⊢ ((𝐾 ∈ ℂ ∧ 𝐽 ∈ ℂ ∧ 𝑁 ∈ ℂ) → ((𝐾 + 𝐽) − 𝑁) = ((𝐾 − 𝑁) + 𝐽)) |
184 | 182, 183 | syl 17 |
. . . . 5
⊢ ((¬
(𝐾 + 𝐽) < 𝑁 ∧ (𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁))) → ((𝐾 + 𝐽) − 𝑁) = ((𝐾 − 𝑁) + 𝐽)) |
185 | 172, 46 | syl 17 |
. . . . . 6
⊢ ((¬
(𝐾 + 𝐽) < 𝑁 ∧ (𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁))) → (0 + 𝐽) = 𝐽) |
186 | 185 | eqcomd 2628 |
. . . . 5
⊢ ((¬
(𝐾 + 𝐽) < 𝑁 ∧ (𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁))) → 𝐽 = (0 + 𝐽)) |
187 | 180, 184,
186 | 3netr4d 2871 |
. . . 4
⊢ ((¬
(𝐾 + 𝐽) < 𝑁 ∧ (𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁))) → ((𝐾 + 𝐽) − 𝑁) ≠ 𝐽) |
188 | | eldifsn 4317 |
. . . 4
⊢ (((𝐾 + 𝐽) − 𝑁) ∈ ((0..^𝑁) ∖ {𝐽}) ↔ (((𝐾 + 𝐽) − 𝑁) ∈ (0..^𝑁) ∧ ((𝐾 + 𝐽) − 𝑁) ≠ 𝐽)) |
189 | 162, 187,
188 | sylanbrc 698 |
. . 3
⊢ ((¬
(𝐾 + 𝐽) < 𝑁 ∧ (𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁))) → ((𝐾 + 𝐽) − 𝑁) ∈ ((0..^𝑁) ∖ {𝐽})) |
190 | 128, 189 | eqeltrd 2701 |
. 2
⊢ ((¬
(𝐾 + 𝐽) < 𝑁 ∧ (𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁))) → ((𝐾 + 𝐽) mod 𝑁) ∈ ((0..^𝑁) ∖ {𝐽})) |
191 | 52, 190 | pm2.61ian 831 |
1
⊢ ((𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁)) → ((𝐾 + 𝐽) mod 𝑁) ∈ ((0..^𝑁) ∖ {𝐽})) |