Proof of Theorem modsumfzodifsn
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | elfzo0 13741 | . . . . . 6
⊢ (𝐽 ∈ (0..^𝑁) ↔ (𝐽 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁)) | 
| 2 |  | elfzoelz 13700 | . . . . . . . . 9
⊢ (𝐾 ∈ (1..^𝑁) → 𝐾 ∈ ℤ) | 
| 3 | 2 | zred 12724 | . . . . . . . 8
⊢ (𝐾 ∈ (1..^𝑁) → 𝐾 ∈ ℝ) | 
| 4 |  | nn0re 12537 | . . . . . . . . 9
⊢ (𝐽 ∈ ℕ0
→ 𝐽 ∈
ℝ) | 
| 5 | 4 | 3ad2ant1 1133 | . . . . . . . 8
⊢ ((𝐽 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝐽 < 𝑁) → 𝐽 ∈ ℝ) | 
| 6 |  | readdcl 11239 | . . . . . . . 8
⊢ ((𝐾 ∈ ℝ ∧ 𝐽 ∈ ℝ) → (𝐾 + 𝐽) ∈ ℝ) | 
| 7 | 3, 5, 6 | syl2anr 597 | . . . . . . 7
⊢ (((𝐽 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝐽 < 𝑁) ∧ 𝐾 ∈ (1..^𝑁)) → (𝐾 + 𝐽) ∈ ℝ) | 
| 8 |  | nnrp 13047 | . . . . . . . . 9
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℝ+) | 
| 9 | 8 | 3ad2ant2 1134 | . . . . . . . 8
⊢ ((𝐽 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝐽 < 𝑁) → 𝑁 ∈
ℝ+) | 
| 10 | 9 | adantr 480 | . . . . . . 7
⊢ (((𝐽 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝐽 < 𝑁) ∧ 𝐾 ∈ (1..^𝑁)) → 𝑁 ∈
ℝ+) | 
| 11 | 7, 10 | jca 511 | . . . . . 6
⊢ (((𝐽 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝐽 < 𝑁) ∧ 𝐾 ∈ (1..^𝑁)) → ((𝐾 + 𝐽) ∈ ℝ ∧ 𝑁 ∈
ℝ+)) | 
| 12 | 1, 11 | sylanb 581 | . . . . 5
⊢ ((𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁)) → ((𝐾 + 𝐽) ∈ ℝ ∧ 𝑁 ∈
ℝ+)) | 
| 13 | 12 | adantl 481 | . . . 4
⊢ (((𝐾 + 𝐽) < 𝑁 ∧ (𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁))) → ((𝐾 + 𝐽) ∈ ℝ ∧ 𝑁 ∈
ℝ+)) | 
| 14 |  | elfzo1 13753 | . . . . . . . 8
⊢ (𝐾 ∈ (1..^𝑁) ↔ (𝐾 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐾 < 𝑁)) | 
| 15 |  | nnnn0 12535 | . . . . . . . . 9
⊢ (𝐾 ∈ ℕ → 𝐾 ∈
ℕ0) | 
| 16 | 15 | 3ad2ant1 1133 | . . . . . . . 8
⊢ ((𝐾 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐾 < 𝑁) → 𝐾 ∈
ℕ0) | 
| 17 | 14, 16 | sylbi 217 | . . . . . . 7
⊢ (𝐾 ∈ (1..^𝑁) → 𝐾 ∈
ℕ0) | 
| 18 |  | elfzonn0 13748 | . . . . . . 7
⊢ (𝐽 ∈ (0..^𝑁) → 𝐽 ∈
ℕ0) | 
| 19 |  | nn0addcl 12563 | . . . . . . 7
⊢ ((𝐾 ∈ ℕ0
∧ 𝐽 ∈
ℕ0) → (𝐾 + 𝐽) ∈
ℕ0) | 
| 20 | 17, 18, 19 | syl2anr 597 | . . . . . 6
⊢ ((𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁)) → (𝐾 + 𝐽) ∈
ℕ0) | 
| 21 | 20 | adantl 481 | . . . . 5
⊢ (((𝐾 + 𝐽) < 𝑁 ∧ (𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁))) → (𝐾 + 𝐽) ∈
ℕ0) | 
| 22 | 21 | nn0ge0d 12592 | . . . 4
⊢ (((𝐾 + 𝐽) < 𝑁 ∧ (𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁))) → 0 ≤ (𝐾 + 𝐽)) | 
| 23 |  | simpl 482 | . . . 4
⊢ (((𝐾 + 𝐽) < 𝑁 ∧ (𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁))) → (𝐾 + 𝐽) < 𝑁) | 
| 24 |  | modid 13937 | . . . 4
⊢ ((((𝐾 + 𝐽) ∈ ℝ ∧ 𝑁 ∈ ℝ+) ∧ (0 ≤
(𝐾 + 𝐽) ∧ (𝐾 + 𝐽) < 𝑁)) → ((𝐾 + 𝐽) mod 𝑁) = (𝐾 + 𝐽)) | 
| 25 | 13, 22, 23, 24 | syl12anc 836 | . . 3
⊢ (((𝐾 + 𝐽) < 𝑁 ∧ (𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁))) → ((𝐾 + 𝐽) mod 𝑁) = (𝐾 + 𝐽)) | 
| 26 |  | simp2 1137 | . . . . . . . 8
⊢ ((𝐽 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝐽 < 𝑁) → 𝑁 ∈ ℕ) | 
| 27 | 1, 26 | sylbi 217 | . . . . . . 7
⊢ (𝐽 ∈ (0..^𝑁) → 𝑁 ∈ ℕ) | 
| 28 | 27 | adantr 480 | . . . . . 6
⊢ ((𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁)) → 𝑁 ∈ ℕ) | 
| 29 | 28 | adantl 481 | . . . . 5
⊢ (((𝐾 + 𝐽) < 𝑁 ∧ (𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁))) → 𝑁 ∈ ℕ) | 
| 30 |  | elfzo0 13741 | . . . . 5
⊢ ((𝐾 + 𝐽) ∈ (0..^𝑁) ↔ ((𝐾 + 𝐽) ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ (𝐾 + 𝐽) < 𝑁)) | 
| 31 | 21, 29, 23, 30 | syl3anbrc 1343 | . . . 4
⊢ (((𝐾 + 𝐽) < 𝑁 ∧ (𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁))) → (𝐾 + 𝐽) ∈ (0..^𝑁)) | 
| 32 | 2 | zcnd 12725 | . . . . . . . 8
⊢ (𝐾 ∈ (1..^𝑁) → 𝐾 ∈ ℂ) | 
| 33 | 32 | adantl 481 | . . . . . . 7
⊢ ((𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁)) → 𝐾 ∈ ℂ) | 
| 34 |  | 0cnd 11255 | . . . . . . 7
⊢ ((𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁)) → 0 ∈ ℂ) | 
| 35 |  | elfzoelz 13700 | . . . . . . . . 9
⊢ (𝐽 ∈ (0..^𝑁) → 𝐽 ∈ ℤ) | 
| 36 | 35 | zcnd 12725 | . . . . . . . 8
⊢ (𝐽 ∈ (0..^𝑁) → 𝐽 ∈ ℂ) | 
| 37 | 36 | adantr 480 | . . . . . . 7
⊢ ((𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁)) → 𝐽 ∈ ℂ) | 
| 38 |  | nnne0 12301 | . . . . . . . . . 10
⊢ (𝐾 ∈ ℕ → 𝐾 ≠ 0) | 
| 39 | 38 | 3ad2ant1 1133 | . . . . . . . . 9
⊢ ((𝐾 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐾 < 𝑁) → 𝐾 ≠ 0) | 
| 40 | 14, 39 | sylbi 217 | . . . . . . . 8
⊢ (𝐾 ∈ (1..^𝑁) → 𝐾 ≠ 0) | 
| 41 | 40 | adantl 481 | . . . . . . 7
⊢ ((𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁)) → 𝐾 ≠ 0) | 
| 42 | 33, 34, 37, 41 | addneintr2d 11470 | . . . . . 6
⊢ ((𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁)) → (𝐾 + 𝐽) ≠ (0 + 𝐽)) | 
| 43 | 42 | adantl 481 | . . . . 5
⊢ (((𝐾 + 𝐽) < 𝑁 ∧ (𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁))) → (𝐾 + 𝐽) ≠ (0 + 𝐽)) | 
| 44 | 37 | adantl 481 | . . . . . 6
⊢ (((𝐾 + 𝐽) < 𝑁 ∧ (𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁))) → 𝐽 ∈ ℂ) | 
| 45 |  | addlid 11445 | . . . . . . 7
⊢ (𝐽 ∈ ℂ → (0 +
𝐽) = 𝐽) | 
| 46 | 45 | eqcomd 2742 | . . . . . 6
⊢ (𝐽 ∈ ℂ → 𝐽 = (0 + 𝐽)) | 
| 47 | 44, 46 | syl 17 | . . . . 5
⊢ (((𝐾 + 𝐽) < 𝑁 ∧ (𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁))) → 𝐽 = (0 + 𝐽)) | 
| 48 | 43, 47 | neeqtrrd 3014 | . . . 4
⊢ (((𝐾 + 𝐽) < 𝑁 ∧ (𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁))) → (𝐾 + 𝐽) ≠ 𝐽) | 
| 49 |  | eldifsn 4785 | . . . 4
⊢ ((𝐾 + 𝐽) ∈ ((0..^𝑁) ∖ {𝐽}) ↔ ((𝐾 + 𝐽) ∈ (0..^𝑁) ∧ (𝐾 + 𝐽) ≠ 𝐽)) | 
| 50 | 31, 48, 49 | sylanbrc 583 | . . 3
⊢ (((𝐾 + 𝐽) < 𝑁 ∧ (𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁))) → (𝐾 + 𝐽) ∈ ((0..^𝑁) ∖ {𝐽})) | 
| 51 | 25, 50 | eqeltrd 2840 | . 2
⊢ (((𝐾 + 𝐽) < 𝑁 ∧ (𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁))) → ((𝐾 + 𝐽) mod 𝑁) ∈ ((0..^𝑁) ∖ {𝐽})) | 
| 52 |  | elfzoel2 13699 | . . . . . . . . . . . . . 14
⊢ (𝐽 ∈ (0..^𝑁) → 𝑁 ∈ ℤ) | 
| 53 | 52 | zcnd 12725 | . . . . . . . . . . . . 13
⊢ (𝐽 ∈ (0..^𝑁) → 𝑁 ∈ ℂ) | 
| 54 | 53 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁)) → 𝑁 ∈ ℂ) | 
| 55 | 54 | adantl 481 | . . . . . . . . . . 11
⊢ ((¬
(𝐾 + 𝐽) < 𝑁 ∧ (𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁))) → 𝑁 ∈ ℂ) | 
| 56 | 55 | mulm1d 11716 | . . . . . . . . . 10
⊢ ((¬
(𝐾 + 𝐽) < 𝑁 ∧ (𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁))) → (-1 · 𝑁) = -𝑁) | 
| 57 | 56 | oveq2d 7448 | . . . . . . . . 9
⊢ ((¬
(𝐾 + 𝐽) < 𝑁 ∧ (𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁))) → ((𝐾 + 𝐽) + (-1 · 𝑁)) = ((𝐾 + 𝐽) + -𝑁)) | 
| 58 |  | zaddcl 12659 | . . . . . . . . . . . . . 14
⊢ ((𝐾 ∈ ℤ ∧ 𝐽 ∈ ℤ) → (𝐾 + 𝐽) ∈ ℤ) | 
| 59 | 2, 35, 58 | syl2anr 597 | . . . . . . . . . . . . 13
⊢ ((𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁)) → (𝐾 + 𝐽) ∈ ℤ) | 
| 60 | 59 | zcnd 12725 | . . . . . . . . . . . 12
⊢ ((𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁)) → (𝐾 + 𝐽) ∈ ℂ) | 
| 61 | 60, 54 | jca 511 | . . . . . . . . . . 11
⊢ ((𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁)) → ((𝐾 + 𝐽) ∈ ℂ ∧ 𝑁 ∈ ℂ)) | 
| 62 | 61 | adantl 481 | . . . . . . . . . 10
⊢ ((¬
(𝐾 + 𝐽) < 𝑁 ∧ (𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁))) → ((𝐾 + 𝐽) ∈ ℂ ∧ 𝑁 ∈ ℂ)) | 
| 63 |  | negsub 11558 | . . . . . . . . . 10
⊢ (((𝐾 + 𝐽) ∈ ℂ ∧ 𝑁 ∈ ℂ) → ((𝐾 + 𝐽) + -𝑁) = ((𝐾 + 𝐽) − 𝑁)) | 
| 64 | 62, 63 | syl 17 | . . . . . . . . 9
⊢ ((¬
(𝐾 + 𝐽) < 𝑁 ∧ (𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁))) → ((𝐾 + 𝐽) + -𝑁) = ((𝐾 + 𝐽) − 𝑁)) | 
| 65 | 57, 64 | eqtrd 2776 | . . . . . . . 8
⊢ ((¬
(𝐾 + 𝐽) < 𝑁 ∧ (𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁))) → ((𝐾 + 𝐽) + (-1 · 𝑁)) = ((𝐾 + 𝐽) − 𝑁)) | 
| 66 | 65 | oveq1d 7447 | . . . . . . 7
⊢ ((¬
(𝐾 + 𝐽) < 𝑁 ∧ (𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁))) → (((𝐾 + 𝐽) + (-1 · 𝑁)) mod 𝑁) = (((𝐾 + 𝐽) − 𝑁) mod 𝑁)) | 
| 67 | 2, 35, 58 | syl2an 596 | . . . . . . . . . . . . 13
⊢ ((𝐾 ∈ (1..^𝑁) ∧ 𝐽 ∈ (0..^𝑁)) → (𝐾 + 𝐽) ∈ ℤ) | 
| 68 | 67 | zred 12724 | . . . . . . . . . . . 12
⊢ ((𝐾 ∈ (1..^𝑁) ∧ 𝐽 ∈ (0..^𝑁)) → (𝐾 + 𝐽) ∈ ℝ) | 
| 69 | 68 | ancoms 458 | . . . . . . . . . . 11
⊢ ((𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁)) → (𝐾 + 𝐽) ∈ ℝ) | 
| 70 | 52 | zred 12724 | . . . . . . . . . . . 12
⊢ (𝐽 ∈ (0..^𝑁) → 𝑁 ∈ ℝ) | 
| 71 | 70 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁)) → 𝑁 ∈ ℝ) | 
| 72 | 69, 71 | resubcld 11692 | . . . . . . . . . 10
⊢ ((𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁)) → ((𝐾 + 𝐽) − 𝑁) ∈ ℝ) | 
| 73 | 72 | adantl 481 | . . . . . . . . 9
⊢ ((¬
(𝐾 + 𝐽) < 𝑁 ∧ (𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁))) → ((𝐾 + 𝐽) − 𝑁) ∈ ℝ) | 
| 74 | 26 | nnrpd 13076 | . . . . . . . . . . . 12
⊢ ((𝐽 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝐽 < 𝑁) → 𝑁 ∈
ℝ+) | 
| 75 | 1, 74 | sylbi 217 | . . . . . . . . . . 11
⊢ (𝐽 ∈ (0..^𝑁) → 𝑁 ∈
ℝ+) | 
| 76 | 75 | adantr 480 | . . . . . . . . . 10
⊢ ((𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁)) → 𝑁 ∈
ℝ+) | 
| 77 | 76 | adantl 481 | . . . . . . . . 9
⊢ ((¬
(𝐾 + 𝐽) < 𝑁 ∧ (𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁))) → 𝑁 ∈
ℝ+) | 
| 78 |  | nnre 12274 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝐾 ∈ ℕ → 𝐾 ∈
ℝ) | 
| 79 | 78 | 3ad2ant1 1133 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝐾 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐾 < 𝑁) → 𝐾 ∈ ℝ) | 
| 80 | 79 | adantl 481 | . . . . . . . . . . . . . . . . 17
⊢ (((𝐽 ∈ ℕ0
∧ 𝐽 < 𝑁) ∧ (𝐾 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐾 < 𝑁)) → 𝐾 ∈ ℝ) | 
| 81 | 4 | adantr 480 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝐽 ∈ ℕ0
∧ 𝐽 < 𝑁) → 𝐽 ∈ ℝ) | 
| 82 | 81 | adantr 480 | . . . . . . . . . . . . . . . . 17
⊢ (((𝐽 ∈ ℕ0
∧ 𝐽 < 𝑁) ∧ (𝐾 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐾 < 𝑁)) → 𝐽 ∈ ℝ) | 
| 83 |  | nnre 12274 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℝ) | 
| 84 | 83 | 3ad2ant2 1134 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝐾 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐾 < 𝑁) → 𝑁 ∈ ℝ) | 
| 85 | 84 | adantl 481 | . . . . . . . . . . . . . . . . 17
⊢ (((𝐽 ∈ ℕ0
∧ 𝐽 < 𝑁) ∧ (𝐾 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐾 < 𝑁)) → 𝑁 ∈ ℝ) | 
| 86 |  | simp3 1138 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐾 ∈ ℝ ∧ 𝐽 ∈ ℝ ∧ 𝑁 ∈ ℝ) → 𝑁 ∈
ℝ) | 
| 87 | 6 | 3adant3 1132 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐾 ∈ ℝ ∧ 𝐽 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (𝐾 + 𝐽) ∈ ℝ) | 
| 88 | 86, 87 | lenltd 11408 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝐾 ∈ ℝ ∧ 𝐽 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (𝑁 ≤ (𝐾 + 𝐽) ↔ ¬ (𝐾 + 𝐽) < 𝑁)) | 
| 89 | 88 | biimprd 248 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝐾 ∈ ℝ ∧ 𝐽 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (¬
(𝐾 + 𝐽) < 𝑁 → 𝑁 ≤ (𝐾 + 𝐽))) | 
| 90 | 87, 86 | subge0d 11854 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝐾 ∈ ℝ ∧ 𝐽 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (0 ≤
((𝐾 + 𝐽) − 𝑁) ↔ 𝑁 ≤ (𝐾 + 𝐽))) | 
| 91 | 89, 90 | sylibrd 259 | . . . . . . . . . . . . . . . . 17
⊢ ((𝐾 ∈ ℝ ∧ 𝐽 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (¬
(𝐾 + 𝐽) < 𝑁 → 0 ≤ ((𝐾 + 𝐽) − 𝑁))) | 
| 92 | 80, 82, 85, 91 | syl3anc 1372 | . . . . . . . . . . . . . . . 16
⊢ (((𝐽 ∈ ℕ0
∧ 𝐽 < 𝑁) ∧ (𝐾 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐾 < 𝑁)) → (¬ (𝐾 + 𝐽) < 𝑁 → 0 ≤ ((𝐾 + 𝐽) − 𝑁))) | 
| 93 | 81, 79 | anim12ci 614 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝐽 ∈ ℕ0
∧ 𝐽 < 𝑁) ∧ (𝐾 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐾 < 𝑁)) → (𝐾 ∈ ℝ ∧ 𝐽 ∈ ℝ)) | 
| 94 | 83, 83 | jca 511 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑁 ∈ ℕ → (𝑁 ∈ ℝ ∧ 𝑁 ∈
ℝ)) | 
| 95 | 94 | 3ad2ant2 1134 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐾 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐾 < 𝑁) → (𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ)) | 
| 96 | 95 | adantl 481 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝐽 ∈ ℕ0
∧ 𝐽 < 𝑁) ∧ (𝐾 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐾 < 𝑁)) → (𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ)) | 
| 97 |  | simpr 484 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐽 ∈ ℕ0
∧ 𝐽 < 𝑁) → 𝐽 < 𝑁) | 
| 98 |  | simp3 1138 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐾 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐾 < 𝑁) → 𝐾 < 𝑁) | 
| 99 | 97, 98 | anim12ci 614 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝐽 ∈ ℕ0
∧ 𝐽 < 𝑁) ∧ (𝐾 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐾 < 𝑁)) → (𝐾 < 𝑁 ∧ 𝐽 < 𝑁)) | 
| 100 | 93, 96, 99 | jca31 514 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝐽 ∈ ℕ0
∧ 𝐽 < 𝑁) ∧ (𝐾 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐾 < 𝑁)) → (((𝐾 ∈ ℝ ∧ 𝐽 ∈ ℝ) ∧ (𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ)) ∧ (𝐾 < 𝑁 ∧ 𝐽 < 𝑁))) | 
| 101 |  | lt2add 11749 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝐾 ∈ ℝ ∧ 𝐽 ∈ ℝ) ∧ (𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ)) → ((𝐾 < 𝑁 ∧ 𝐽 < 𝑁) → (𝐾 + 𝐽) < (𝑁 + 𝑁))) | 
| 102 | 101 | imp 406 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝐾 ∈ ℝ ∧ 𝐽 ∈ ℝ) ∧ (𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ)) ∧ (𝐾 < 𝑁 ∧ 𝐽 < 𝑁)) → (𝐾 + 𝐽) < (𝑁 + 𝑁)) | 
| 103 | 100, 102 | syl 17 | . . . . . . . . . . . . . . . . 17
⊢ (((𝐽 ∈ ℕ0
∧ 𝐽 < 𝑁) ∧ (𝐾 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐾 < 𝑁)) → (𝐾 + 𝐽) < (𝑁 + 𝑁)) | 
| 104 | 79, 81, 6 | syl2anr 597 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝐽 ∈ ℕ0
∧ 𝐽 < 𝑁) ∧ (𝐾 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐾 < 𝑁)) → (𝐾 + 𝐽) ∈ ℝ) | 
| 105 |  | ltsubadd 11734 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝐾 + 𝐽) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (((𝐾 + 𝐽) − 𝑁) < 𝑁 ↔ (𝐾 + 𝐽) < (𝑁 + 𝑁))) | 
| 106 | 104, 85, 85, 105 | syl3anc 1372 | . . . . . . . . . . . . . . . . 17
⊢ (((𝐽 ∈ ℕ0
∧ 𝐽 < 𝑁) ∧ (𝐾 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐾 < 𝑁)) → (((𝐾 + 𝐽) − 𝑁) < 𝑁 ↔ (𝐾 + 𝐽) < (𝑁 + 𝑁))) | 
| 107 | 103, 106 | mpbird 257 | . . . . . . . . . . . . . . . 16
⊢ (((𝐽 ∈ ℕ0
∧ 𝐽 < 𝑁) ∧ (𝐾 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐾 < 𝑁)) → ((𝐾 + 𝐽) − 𝑁) < 𝑁) | 
| 108 | 92, 107 | jctird 526 | . . . . . . . . . . . . . . 15
⊢ (((𝐽 ∈ ℕ0
∧ 𝐽 < 𝑁) ∧ (𝐾 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐾 < 𝑁)) → (¬ (𝐾 + 𝐽) < 𝑁 → (0 ≤ ((𝐾 + 𝐽) − 𝑁) ∧ ((𝐾 + 𝐽) − 𝑁) < 𝑁))) | 
| 109 | 108 | ex 412 | . . . . . . . . . . . . . 14
⊢ ((𝐽 ∈ ℕ0
∧ 𝐽 < 𝑁) → ((𝐾 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐾 < 𝑁) → (¬ (𝐾 + 𝐽) < 𝑁 → (0 ≤ ((𝐾 + 𝐽) − 𝑁) ∧ ((𝐾 + 𝐽) − 𝑁) < 𝑁)))) | 
| 110 | 14, 109 | biimtrid 242 | . . . . . . . . . . . . 13
⊢ ((𝐽 ∈ ℕ0
∧ 𝐽 < 𝑁) → (𝐾 ∈ (1..^𝑁) → (¬ (𝐾 + 𝐽) < 𝑁 → (0 ≤ ((𝐾 + 𝐽) − 𝑁) ∧ ((𝐾 + 𝐽) − 𝑁) < 𝑁)))) | 
| 111 | 110 | 3adant2 1131 | . . . . . . . . . . . 12
⊢ ((𝐽 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝐽 < 𝑁) → (𝐾 ∈ (1..^𝑁) → (¬ (𝐾 + 𝐽) < 𝑁 → (0 ≤ ((𝐾 + 𝐽) − 𝑁) ∧ ((𝐾 + 𝐽) − 𝑁) < 𝑁)))) | 
| 112 | 1, 111 | sylbi 217 | . . . . . . . . . . 11
⊢ (𝐽 ∈ (0..^𝑁) → (𝐾 ∈ (1..^𝑁) → (¬ (𝐾 + 𝐽) < 𝑁 → (0 ≤ ((𝐾 + 𝐽) − 𝑁) ∧ ((𝐾 + 𝐽) − 𝑁) < 𝑁)))) | 
| 113 | 112 | imp 406 | . . . . . . . . . 10
⊢ ((𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁)) → (¬ (𝐾 + 𝐽) < 𝑁 → (0 ≤ ((𝐾 + 𝐽) − 𝑁) ∧ ((𝐾 + 𝐽) − 𝑁) < 𝑁))) | 
| 114 | 113 | impcom 407 | . . . . . . . . 9
⊢ ((¬
(𝐾 + 𝐽) < 𝑁 ∧ (𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁))) → (0 ≤ ((𝐾 + 𝐽) − 𝑁) ∧ ((𝐾 + 𝐽) − 𝑁) < 𝑁)) | 
| 115 | 73, 77, 114 | jca31 514 | . . . . . . . 8
⊢ ((¬
(𝐾 + 𝐽) < 𝑁 ∧ (𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁))) → ((((𝐾 + 𝐽) − 𝑁) ∈ ℝ ∧ 𝑁 ∈ ℝ+) ∧ (0 ≤
((𝐾 + 𝐽) − 𝑁) ∧ ((𝐾 + 𝐽) − 𝑁) < 𝑁))) | 
| 116 |  | modid 13937 | . . . . . . . 8
⊢
(((((𝐾 + 𝐽) − 𝑁) ∈ ℝ ∧ 𝑁 ∈ ℝ+) ∧ (0 ≤
((𝐾 + 𝐽) − 𝑁) ∧ ((𝐾 + 𝐽) − 𝑁) < 𝑁)) → (((𝐾 + 𝐽) − 𝑁) mod 𝑁) = ((𝐾 + 𝐽) − 𝑁)) | 
| 117 | 115, 116 | syl 17 | . . . . . . 7
⊢ ((¬
(𝐾 + 𝐽) < 𝑁 ∧ (𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁))) → (((𝐾 + 𝐽) − 𝑁) mod 𝑁) = ((𝐾 + 𝐽) − 𝑁)) | 
| 118 | 66, 117 | eqtrd 2776 | . . . . . 6
⊢ ((¬
(𝐾 + 𝐽) < 𝑁 ∧ (𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁))) → (((𝐾 + 𝐽) + (-1 · 𝑁)) mod 𝑁) = ((𝐾 + 𝐽) − 𝑁)) | 
| 119 | 118 | eqcomd 2742 | . . . . 5
⊢ ((¬
(𝐾 + 𝐽) < 𝑁 ∧ (𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁))) → ((𝐾 + 𝐽) − 𝑁) = (((𝐾 + 𝐽) + (-1 · 𝑁)) mod 𝑁)) | 
| 120 | 1, 9 | sylbi 217 | . . . . . . 7
⊢ (𝐽 ∈ (0..^𝑁) → 𝑁 ∈
ℝ+) | 
| 121 | 120 | adantr 480 | . . . . . 6
⊢ ((𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁)) → 𝑁 ∈
ℝ+) | 
| 122 |  | neg1z 12655 | . . . . . . 7
⊢ -1 ∈
ℤ | 
| 123 | 122 | a1i 11 | . . . . . 6
⊢ ((¬
(𝐾 + 𝐽) < 𝑁 ∧ (𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁))) → -1 ∈
ℤ) | 
| 124 |  | modcyc 13947 | . . . . . 6
⊢ (((𝐾 + 𝐽) ∈ ℝ ∧ 𝑁 ∈ ℝ+ ∧ -1 ∈
ℤ) → (((𝐾 +
𝐽) + (-1 · 𝑁)) mod 𝑁) = ((𝐾 + 𝐽) mod 𝑁)) | 
| 125 | 69, 121, 123, 124 | syl2an23an 1424 | . . . . 5
⊢ ((¬
(𝐾 + 𝐽) < 𝑁 ∧ (𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁))) → (((𝐾 + 𝐽) + (-1 · 𝑁)) mod 𝑁) = ((𝐾 + 𝐽) mod 𝑁)) | 
| 126 | 119, 125 | eqtrd 2776 | . . . 4
⊢ ((¬
(𝐾 + 𝐽) < 𝑁 ∧ (𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁))) → ((𝐾 + 𝐽) − 𝑁) = ((𝐾 + 𝐽) mod 𝑁)) | 
| 127 | 126 | eqcomd 2742 | . . 3
⊢ ((¬
(𝐾 + 𝐽) < 𝑁 ∧ (𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁))) → ((𝐾 + 𝐽) mod 𝑁) = ((𝐾 + 𝐽) − 𝑁)) | 
| 128 | 52 | adantr 480 | . . . . . . . 8
⊢ ((𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁)) → 𝑁 ∈ ℤ) | 
| 129 | 59, 128 | zsubcld 12729 | . . . . . . 7
⊢ ((𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁)) → ((𝐾 + 𝐽) − 𝑁) ∈ ℤ) | 
| 130 | 129 | adantl 481 | . . . . . 6
⊢ ((¬
(𝐾 + 𝐽) < 𝑁 ∧ (𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁))) → ((𝐾 + 𝐽) − 𝑁) ∈ ℤ) | 
| 131 | 3 | adantl 481 | . . . . . . . 8
⊢ ((𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁)) → 𝐾 ∈ ℝ) | 
| 132 | 35 | zred 12724 | . . . . . . . . 9
⊢ (𝐽 ∈ (0..^𝑁) → 𝐽 ∈ ℝ) | 
| 133 | 132 | adantr 480 | . . . . . . . 8
⊢ ((𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁)) → 𝐽 ∈ ℝ) | 
| 134 | 90 | biimprd 248 | . . . . . . . . 9
⊢ ((𝐾 ∈ ℝ ∧ 𝐽 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (𝑁 ≤ (𝐾 + 𝐽) → 0 ≤ ((𝐾 + 𝐽) − 𝑁))) | 
| 135 | 88, 134 | sylbird 260 | . . . . . . . 8
⊢ ((𝐾 ∈ ℝ ∧ 𝐽 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (¬
(𝐾 + 𝐽) < 𝑁 → 0 ≤ ((𝐾 + 𝐽) − 𝑁))) | 
| 136 | 131, 133,
71, 135 | syl3anc 1372 | . . . . . . 7
⊢ ((𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁)) → (¬ (𝐾 + 𝐽) < 𝑁 → 0 ≤ ((𝐾 + 𝐽) − 𝑁))) | 
| 137 | 136 | impcom 407 | . . . . . 6
⊢ ((¬
(𝐾 + 𝐽) < 𝑁 ∧ (𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁))) → 0 ≤ ((𝐾 + 𝐽) − 𝑁)) | 
| 138 |  | elnn0z 12628 | . . . . . 6
⊢ (((𝐾 + 𝐽) − 𝑁) ∈ ℕ0 ↔ (((𝐾 + 𝐽) − 𝑁) ∈ ℤ ∧ 0 ≤ ((𝐾 + 𝐽) − 𝑁))) | 
| 139 | 130, 137,
138 | sylanbrc 583 | . . . . 5
⊢ ((¬
(𝐾 + 𝐽) < 𝑁 ∧ (𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁))) → ((𝐾 + 𝐽) − 𝑁) ∈
ℕ0) | 
| 140 | 28 | adantl 481 | . . . . 5
⊢ ((¬
(𝐾 + 𝐽) < 𝑁 ∧ (𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁))) → 𝑁 ∈ ℕ) | 
| 141 | 100 | expcom 413 | . . . . . . . . . . . . 13
⊢ ((𝐾 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐾 < 𝑁) → ((𝐽 ∈ ℕ0 ∧ 𝐽 < 𝑁) → (((𝐾 ∈ ℝ ∧ 𝐽 ∈ ℝ) ∧ (𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ)) ∧ (𝐾 < 𝑁 ∧ 𝐽 < 𝑁)))) | 
| 142 | 14, 141 | sylbi 217 | . . . . . . . . . . . 12
⊢ (𝐾 ∈ (1..^𝑁) → ((𝐽 ∈ ℕ0 ∧ 𝐽 < 𝑁) → (((𝐾 ∈ ℝ ∧ 𝐽 ∈ ℝ) ∧ (𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ)) ∧ (𝐾 < 𝑁 ∧ 𝐽 < 𝑁)))) | 
| 143 | 142 | com12 32 | . . . . . . . . . . 11
⊢ ((𝐽 ∈ ℕ0
∧ 𝐽 < 𝑁) → (𝐾 ∈ (1..^𝑁) → (((𝐾 ∈ ℝ ∧ 𝐽 ∈ ℝ) ∧ (𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ)) ∧ (𝐾 < 𝑁 ∧ 𝐽 < 𝑁)))) | 
| 144 | 143 | 3adant2 1131 | . . . . . . . . . 10
⊢ ((𝐽 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝐽 < 𝑁) → (𝐾 ∈ (1..^𝑁) → (((𝐾 ∈ ℝ ∧ 𝐽 ∈ ℝ) ∧ (𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ)) ∧ (𝐾 < 𝑁 ∧ 𝐽 < 𝑁)))) | 
| 145 | 1, 144 | sylbi 217 | . . . . . . . . 9
⊢ (𝐽 ∈ (0..^𝑁) → (𝐾 ∈ (1..^𝑁) → (((𝐾 ∈ ℝ ∧ 𝐽 ∈ ℝ) ∧ (𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ)) ∧ (𝐾 < 𝑁 ∧ 𝐽 < 𝑁)))) | 
| 146 | 145 | imp 406 | . . . . . . . 8
⊢ ((𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁)) → (((𝐾 ∈ ℝ ∧ 𝐽 ∈ ℝ) ∧ (𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ)) ∧ (𝐾 < 𝑁 ∧ 𝐽 < 𝑁))) | 
| 147 | 146, 102 | syl 17 | . . . . . . 7
⊢ ((𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁)) → (𝐾 + 𝐽) < (𝑁 + 𝑁)) | 
| 148 | 4 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((𝐽 ∈ ℕ0
∧ 𝑁 ∈ ℕ)
→ 𝐽 ∈
ℝ) | 
| 149 | 3, 148, 6 | syl2anr 597 | . . . . . . . . . . . . 13
⊢ (((𝐽 ∈ ℕ0
∧ 𝑁 ∈ ℕ)
∧ 𝐾 ∈ (1..^𝑁)) → (𝐾 + 𝐽) ∈ ℝ) | 
| 150 | 83 | adantl 481 | . . . . . . . . . . . . . 14
⊢ ((𝐽 ∈ ℕ0
∧ 𝑁 ∈ ℕ)
→ 𝑁 ∈
ℝ) | 
| 151 | 150 | adantr 480 | . . . . . . . . . . . . 13
⊢ (((𝐽 ∈ ℕ0
∧ 𝑁 ∈ ℕ)
∧ 𝐾 ∈ (1..^𝑁)) → 𝑁 ∈ ℝ) | 
| 152 | 149, 151,
151 | 3jca 1128 | . . . . . . . . . . . 12
⊢ (((𝐽 ∈ ℕ0
∧ 𝑁 ∈ ℕ)
∧ 𝐾 ∈ (1..^𝑁)) → ((𝐾 + 𝐽) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ)) | 
| 153 | 152 | ex 412 | . . . . . . . . . . 11
⊢ ((𝐽 ∈ ℕ0
∧ 𝑁 ∈ ℕ)
→ (𝐾 ∈ (1..^𝑁) → ((𝐾 + 𝐽) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ))) | 
| 154 | 153 | 3adant3 1132 | . . . . . . . . . 10
⊢ ((𝐽 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝐽 < 𝑁) → (𝐾 ∈ (1..^𝑁) → ((𝐾 + 𝐽) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ))) | 
| 155 | 1, 154 | sylbi 217 | . . . . . . . . 9
⊢ (𝐽 ∈ (0..^𝑁) → (𝐾 ∈ (1..^𝑁) → ((𝐾 + 𝐽) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ))) | 
| 156 | 155 | imp 406 | . . . . . . . 8
⊢ ((𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁)) → ((𝐾 + 𝐽) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ)) | 
| 157 | 156, 105 | syl 17 | . . . . . . 7
⊢ ((𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁)) → (((𝐾 + 𝐽) − 𝑁) < 𝑁 ↔ (𝐾 + 𝐽) < (𝑁 + 𝑁))) | 
| 158 | 147, 157 | mpbird 257 | . . . . . 6
⊢ ((𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁)) → ((𝐾 + 𝐽) − 𝑁) < 𝑁) | 
| 159 | 158 | adantl 481 | . . . . 5
⊢ ((¬
(𝐾 + 𝐽) < 𝑁 ∧ (𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁))) → ((𝐾 + 𝐽) − 𝑁) < 𝑁) | 
| 160 |  | elfzo0 13741 | . . . . 5
⊢ (((𝐾 + 𝐽) − 𝑁) ∈ (0..^𝑁) ↔ (((𝐾 + 𝐽) − 𝑁) ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ ((𝐾 + 𝐽) − 𝑁) < 𝑁)) | 
| 161 | 139, 140,
159, 160 | syl3anbrc 1343 | . . . 4
⊢ ((¬
(𝐾 + 𝐽) < 𝑁 ∧ (𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁))) → ((𝐾 + 𝐽) − 𝑁) ∈ (0..^𝑁)) | 
| 162 |  | nncn 12275 | . . . . . . . . . . 11
⊢ (𝐾 ∈ ℕ → 𝐾 ∈
ℂ) | 
| 163 |  | nncn 12275 | . . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℂ) | 
| 164 |  | subcl 11508 | . . . . . . . . . . 11
⊢ ((𝐾 ∈ ℂ ∧ 𝑁 ∈ ℂ) → (𝐾 − 𝑁) ∈ ℂ) | 
| 165 | 162, 163,
164 | syl2an 596 | . . . . . . . . . 10
⊢ ((𝐾 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝐾 − 𝑁) ∈ ℂ) | 
| 166 | 165 | 3adant3 1132 | . . . . . . . . 9
⊢ ((𝐾 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐾 < 𝑁) → (𝐾 − 𝑁) ∈ ℂ) | 
| 167 | 14, 166 | sylbi 217 | . . . . . . . 8
⊢ (𝐾 ∈ (1..^𝑁) → (𝐾 − 𝑁) ∈ ℂ) | 
| 168 | 167 | adantl 481 | . . . . . . 7
⊢ ((𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁)) → (𝐾 − 𝑁) ∈ ℂ) | 
| 169 | 168 | adantl 481 | . . . . . 6
⊢ ((¬
(𝐾 + 𝐽) < 𝑁 ∧ (𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁))) → (𝐾 − 𝑁) ∈ ℂ) | 
| 170 |  | 0cnd 11255 | . . . . . 6
⊢ ((¬
(𝐾 + 𝐽) < 𝑁 ∧ (𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁))) → 0 ∈
ℂ) | 
| 171 | 37 | adantl 481 | . . . . . 6
⊢ ((¬
(𝐾 + 𝐽) < 𝑁 ∧ (𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁))) → 𝐽 ∈ ℂ) | 
| 172 |  | elfzoel2 13699 | . . . . . . . . . 10
⊢ (𝐾 ∈ (1..^𝑁) → 𝑁 ∈ ℤ) | 
| 173 | 172 | zcnd 12725 | . . . . . . . . 9
⊢ (𝐾 ∈ (1..^𝑁) → 𝑁 ∈ ℂ) | 
| 174 | 79, 98 | ltned 11398 | . . . . . . . . . 10
⊢ ((𝐾 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐾 < 𝑁) → 𝐾 ≠ 𝑁) | 
| 175 | 14, 174 | sylbi 217 | . . . . . . . . 9
⊢ (𝐾 ∈ (1..^𝑁) → 𝐾 ≠ 𝑁) | 
| 176 | 32, 173, 175 | subne0d 11630 | . . . . . . . 8
⊢ (𝐾 ∈ (1..^𝑁) → (𝐾 − 𝑁) ≠ 0) | 
| 177 | 176 | adantl 481 | . . . . . . 7
⊢ ((𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁)) → (𝐾 − 𝑁) ≠ 0) | 
| 178 | 177 | adantl 481 | . . . . . 6
⊢ ((¬
(𝐾 + 𝐽) < 𝑁 ∧ (𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁))) → (𝐾 − 𝑁) ≠ 0) | 
| 179 | 169, 170,
171, 178 | addneintr2d 11470 | . . . . 5
⊢ ((¬
(𝐾 + 𝐽) < 𝑁 ∧ (𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁))) → ((𝐾 − 𝑁) + 𝐽) ≠ (0 + 𝐽)) | 
| 180 | 33, 37, 54 | 3jca 1128 | . . . . . . 7
⊢ ((𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁)) → (𝐾 ∈ ℂ ∧ 𝐽 ∈ ℂ ∧ 𝑁 ∈ ℂ)) | 
| 181 | 180 | adantl 481 | . . . . . 6
⊢ ((¬
(𝐾 + 𝐽) < 𝑁 ∧ (𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁))) → (𝐾 ∈ ℂ ∧ 𝐽 ∈ ℂ ∧ 𝑁 ∈ ℂ)) | 
| 182 |  | addsub 11520 | . . . . . 6
⊢ ((𝐾 ∈ ℂ ∧ 𝐽 ∈ ℂ ∧ 𝑁 ∈ ℂ) → ((𝐾 + 𝐽) − 𝑁) = ((𝐾 − 𝑁) + 𝐽)) | 
| 183 | 181, 182 | syl 17 | . . . . 5
⊢ ((¬
(𝐾 + 𝐽) < 𝑁 ∧ (𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁))) → ((𝐾 + 𝐽) − 𝑁) = ((𝐾 − 𝑁) + 𝐽)) | 
| 184 | 171, 45 | syl 17 | . . . . . 6
⊢ ((¬
(𝐾 + 𝐽) < 𝑁 ∧ (𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁))) → (0 + 𝐽) = 𝐽) | 
| 185 | 184 | eqcomd 2742 | . . . . 5
⊢ ((¬
(𝐾 + 𝐽) < 𝑁 ∧ (𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁))) → 𝐽 = (0 + 𝐽)) | 
| 186 | 179, 183,
185 | 3netr4d 3017 | . . . 4
⊢ ((¬
(𝐾 + 𝐽) < 𝑁 ∧ (𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁))) → ((𝐾 + 𝐽) − 𝑁) ≠ 𝐽) | 
| 187 |  | eldifsn 4785 | . . . 4
⊢ (((𝐾 + 𝐽) − 𝑁) ∈ ((0..^𝑁) ∖ {𝐽}) ↔ (((𝐾 + 𝐽) − 𝑁) ∈ (0..^𝑁) ∧ ((𝐾 + 𝐽) − 𝑁) ≠ 𝐽)) | 
| 188 | 161, 186,
187 | sylanbrc 583 | . . 3
⊢ ((¬
(𝐾 + 𝐽) < 𝑁 ∧ (𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁))) → ((𝐾 + 𝐽) − 𝑁) ∈ ((0..^𝑁) ∖ {𝐽})) | 
| 189 | 127, 188 | eqeltrd 2840 | . 2
⊢ ((¬
(𝐾 + 𝐽) < 𝑁 ∧ (𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁))) → ((𝐾 + 𝐽) mod 𝑁) ∈ ((0..^𝑁) ∖ {𝐽})) | 
| 190 | 51, 189 | pm2.61ian 811 | 1
⊢ ((𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁)) → ((𝐾 + 𝐽) mod 𝑁) ∈ ((0..^𝑁) ∖ {𝐽})) |