Proof of Theorem acongeq
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | 2z 12649 | . . . . . . 7
⊢ 2 ∈
ℤ | 
| 2 |  | nnz 12634 | . . . . . . . 8
⊢ (𝐴 ∈ ℕ → 𝐴 ∈
ℤ) | 
| 3 | 2 | 3ad2ant1 1134 | . . . . . . 7
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) → 𝐴 ∈ ℤ) | 
| 4 |  | zmulcl 12666 | . . . . . . 7
⊢ ((2
∈ ℤ ∧ 𝐴
∈ ℤ) → (2 · 𝐴) ∈ ℤ) | 
| 5 | 1, 3, 4 | sylancr 587 | . . . . . 6
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) → (2 · 𝐴) ∈ ℤ) | 
| 6 |  | elfzelz 13564 | . . . . . . 7
⊢ (𝐵 ∈ (0...𝐴) → 𝐵 ∈ ℤ) | 
| 7 | 6 | 3ad2ant2 1135 | . . . . . 6
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) → 𝐵 ∈ ℤ) | 
| 8 |  | congid 42983 | . . . . . 6
⊢ (((2
· 𝐴) ∈ ℤ
∧ 𝐵 ∈ ℤ)
→ (2 · 𝐴)
∥ (𝐵 − 𝐵)) | 
| 9 | 5, 7, 8 | syl2anc 584 | . . . . 5
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) → (2 · 𝐴) ∥ (𝐵 − 𝐵)) | 
| 10 | 9 | adantr 480 | . . . 4
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) ∧ 𝐵 = 𝐶) → (2 · 𝐴) ∥ (𝐵 − 𝐵)) | 
| 11 |  | oveq2 7439 | . . . . 5
⊢ (𝐵 = 𝐶 → (𝐵 − 𝐵) = (𝐵 − 𝐶)) | 
| 12 | 11 | adantl 481 | . . . 4
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) ∧ 𝐵 = 𝐶) → (𝐵 − 𝐵) = (𝐵 − 𝐶)) | 
| 13 | 10, 12 | breqtrd 5169 | . . 3
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) ∧ 𝐵 = 𝐶) → (2 · 𝐴) ∥ (𝐵 − 𝐶)) | 
| 14 | 13 | orcd 874 | . 2
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) ∧ 𝐵 = 𝐶) → ((2 · 𝐴) ∥ (𝐵 − 𝐶) ∨ (2 · 𝐴) ∥ (𝐵 − -𝐶))) | 
| 15 |  | elfzelz 13564 | . . . . . . . . . 10
⊢ (𝐶 ∈ (0...𝐴) → 𝐶 ∈ ℤ) | 
| 16 | 15 | 3ad2ant3 1136 | . . . . . . . . 9
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) → 𝐶 ∈ ℤ) | 
| 17 | 7, 16 | zsubcld 12727 | . . . . . . . 8
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) → (𝐵 − 𝐶) ∈ ℤ) | 
| 18 | 17 | zcnd 12723 | . . . . . . 7
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) → (𝐵 − 𝐶) ∈ ℂ) | 
| 19 | 18 | abscld 15475 | . . . . . 6
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) → (abs‘(𝐵 − 𝐶)) ∈ ℝ) | 
| 20 |  | nnre 12273 | . . . . . . . 8
⊢ (𝐴 ∈ ℕ → 𝐴 ∈
ℝ) | 
| 21 | 20 | 3ad2ant1 1134 | . . . . . . 7
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) → 𝐴 ∈ ℝ) | 
| 22 |  | 0re 11263 | . . . . . . 7
⊢ 0 ∈
ℝ | 
| 23 |  | resubcl 11573 | . . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 0 ∈
ℝ) → (𝐴 −
0) ∈ ℝ) | 
| 24 | 21, 22, 23 | sylancl 586 | . . . . . 6
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) → (𝐴 − 0) ∈ ℝ) | 
| 25 |  | 2re 12340 | . . . . . . 7
⊢ 2 ∈
ℝ | 
| 26 |  | remulcl 11240 | . . . . . . 7
⊢ ((2
∈ ℝ ∧ 𝐴
∈ ℝ) → (2 · 𝐴) ∈ ℝ) | 
| 27 | 25, 21, 26 | sylancr 587 | . . . . . 6
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) → (2 · 𝐴) ∈ ℝ) | 
| 28 |  | simp2 1138 | . . . . . . 7
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) → 𝐵 ∈ (0...𝐴)) | 
| 29 |  | simp3 1139 | . . . . . . 7
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) → 𝐶 ∈ (0...𝐴)) | 
| 30 | 24 | leidd 11829 | . . . . . . 7
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) → (𝐴 − 0) ≤ (𝐴 − 0)) | 
| 31 |  | fzmaxdif 42993 | . . . . . . 7
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ (0...𝐴)) ∧ (𝐴 ∈ ℤ ∧ 𝐶 ∈ (0...𝐴)) ∧ (𝐴 − 0) ≤ (𝐴 − 0)) → (abs‘(𝐵 − 𝐶)) ≤ (𝐴 − 0)) | 
| 32 | 3, 28, 3, 29, 30, 31 | syl221anc 1383 | . . . . . 6
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) → (abs‘(𝐵 − 𝐶)) ≤ (𝐴 − 0)) | 
| 33 |  | nnrp 13046 | . . . . . . . . 9
⊢ (𝐴 ∈ ℕ → 𝐴 ∈
ℝ+) | 
| 34 | 33 | 3ad2ant1 1134 | . . . . . . . 8
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) → 𝐴 ∈
ℝ+) | 
| 35 | 21, 34 | ltaddrpd 13110 | . . . . . . 7
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) → 𝐴 < (𝐴 + 𝐴)) | 
| 36 | 21 | recnd 11289 | . . . . . . . 8
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) → 𝐴 ∈ ℂ) | 
| 37 | 36 | subid1d 11609 | . . . . . . 7
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) → (𝐴 − 0) = 𝐴) | 
| 38 | 36 | 2timesd 12509 | . . . . . . 7
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) → (2 · 𝐴) = (𝐴 + 𝐴)) | 
| 39 | 35, 37, 38 | 3brtr4d 5175 | . . . . . 6
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) → (𝐴 − 0) < (2 · 𝐴)) | 
| 40 | 19, 24, 27, 32, 39 | lelttrd 11419 | . . . . 5
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) → (abs‘(𝐵 − 𝐶)) < (2 · 𝐴)) | 
| 41 | 40 | adantr 480 | . . . 4
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) ∧ (2 · 𝐴) ∥ (𝐵 − 𝐶)) → (abs‘(𝐵 − 𝐶)) < (2 · 𝐴)) | 
| 42 |  | 2nn 12339 | . . . . . 6
⊢ 2 ∈
ℕ | 
| 43 |  | simpl1 1192 | . . . . . 6
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) ∧ (2 · 𝐴) ∥ (𝐵 − 𝐶)) → 𝐴 ∈ ℕ) | 
| 44 |  | nnmulcl 12290 | . . . . . 6
⊢ ((2
∈ ℕ ∧ 𝐴
∈ ℕ) → (2 · 𝐴) ∈ ℕ) | 
| 45 | 42, 43, 44 | sylancr 587 | . . . . 5
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) ∧ (2 · 𝐴) ∥ (𝐵 − 𝐶)) → (2 · 𝐴) ∈ ℕ) | 
| 46 |  | simpl2 1193 | . . . . . 6
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) ∧ (2 · 𝐴) ∥ (𝐵 − 𝐶)) → 𝐵 ∈ (0...𝐴)) | 
| 47 | 46 | elfzelzd 13565 | . . . . 5
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) ∧ (2 · 𝐴) ∥ (𝐵 − 𝐶)) → 𝐵 ∈ ℤ) | 
| 48 |  | simpl3 1194 | . . . . . 6
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) ∧ (2 · 𝐴) ∥ (𝐵 − 𝐶)) → 𝐶 ∈ (0...𝐴)) | 
| 49 | 48 | elfzelzd 13565 | . . . . 5
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) ∧ (2 · 𝐴) ∥ (𝐵 − 𝐶)) → 𝐶 ∈ ℤ) | 
| 50 |  | simpr 484 | . . . . 5
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) ∧ (2 · 𝐴) ∥ (𝐵 − 𝐶)) → (2 · 𝐴) ∥ (𝐵 − 𝐶)) | 
| 51 |  | congabseq 42986 | . . . . 5
⊢ ((((2
· 𝐴) ∈ ℕ
∧ 𝐵 ∈ ℤ
∧ 𝐶 ∈ ℤ)
∧ (2 · 𝐴)
∥ (𝐵 − 𝐶)) → ((abs‘(𝐵 − 𝐶)) < (2 · 𝐴) ↔ 𝐵 = 𝐶)) | 
| 52 | 45, 47, 49, 50, 51 | syl31anc 1375 | . . . 4
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) ∧ (2 · 𝐴) ∥ (𝐵 − 𝐶)) → ((abs‘(𝐵 − 𝐶)) < (2 · 𝐴) ↔ 𝐵 = 𝐶)) | 
| 53 | 41, 52 | mpbid 232 | . . 3
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) ∧ (2 · 𝐴) ∥ (𝐵 − 𝐶)) → 𝐵 = 𝐶) | 
| 54 |  | simpll2 1214 | . . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) ∧ (2 · 𝐴) ∥ (𝐵 − -𝐶)) ∧ 𝐶 ∈ (0...(𝐴 − 1))) → 𝐵 ∈ (0...𝐴)) | 
| 55 |  | elfzle1 13567 | . . . . . . . . . . 11
⊢ (𝐵 ∈ (0...𝐴) → 0 ≤ 𝐵) | 
| 56 | 54, 55 | syl 17 | . . . . . . . . . 10
⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) ∧ (2 · 𝐴) ∥ (𝐵 − -𝐶)) ∧ 𝐶 ∈ (0...(𝐴 − 1))) → 0 ≤ 𝐵) | 
| 57 | 7 | zred 12722 | . . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) → 𝐵 ∈ ℝ) | 
| 58 | 16 | zred 12722 | . . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) → 𝐶 ∈ ℝ) | 
| 59 | 58 | renegcld 11690 | . . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) → -𝐶 ∈ ℝ) | 
| 60 | 57, 59 | resubcld 11691 | . . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) → (𝐵 − -𝐶) ∈ ℝ) | 
| 61 | 60 | recnd 11289 | . . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) → (𝐵 − -𝐶) ∈ ℂ) | 
| 62 | 61 | abscld 15475 | . . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) → (abs‘(𝐵 − -𝐶)) ∈ ℝ) | 
| 63 | 62 | ad2antrr 726 | . . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) ∧ (2 · 𝐴) ∥ (𝐵 − -𝐶)) ∧ 𝐶 ∈ (0...(𝐴 − 1))) → (abs‘(𝐵 − -𝐶)) ∈ ℝ) | 
| 64 |  | 1re 11261 | . . . . . . . . . . . . . . . 16
⊢ 1 ∈
ℝ | 
| 65 |  | resubcl 11573 | . . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℝ ∧ 1 ∈
ℝ) → (𝐴 −
1) ∈ ℝ) | 
| 66 | 21, 64, 65 | sylancl 586 | . . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) → (𝐴 − 1) ∈ ℝ) | 
| 67 | 66 | renegcld 11690 | . . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) → -(𝐴 − 1) ∈ ℝ) | 
| 68 | 21, 67 | resubcld 11691 | . . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) → (𝐴 − -(𝐴 − 1)) ∈
ℝ) | 
| 69 | 68 | ad2antrr 726 | . . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) ∧ (2 · 𝐴) ∥ (𝐵 − -𝐶)) ∧ 𝐶 ∈ (0...(𝐴 − 1))) → (𝐴 − -(𝐴 − 1)) ∈
ℝ) | 
| 70 | 27 | ad2antrr 726 | . . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) ∧ (2 · 𝐴) ∥ (𝐵 − -𝐶)) ∧ 𝐶 ∈ (0...(𝐴 − 1))) → (2 · 𝐴) ∈
ℝ) | 
| 71 | 7 | ad2antrr 726 | . . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) ∧ (2 · 𝐴) ∥ (𝐵 − -𝐶)) ∧ 𝐶 ∈ (0...(𝐴 − 1))) → 𝐵 ∈ ℤ) | 
| 72 | 71 | zcnd 12723 | . . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) ∧ (2 · 𝐴) ∥ (𝐵 − -𝐶)) ∧ 𝐶 ∈ (0...(𝐴 − 1))) → 𝐵 ∈ ℂ) | 
| 73 | 16 | znegcld 12724 | . . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) → -𝐶 ∈ ℤ) | 
| 74 | 73 | ad2antrr 726 | . . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) ∧ (2 · 𝐴) ∥ (𝐵 − -𝐶)) ∧ 𝐶 ∈ (0...(𝐴 − 1))) → -𝐶 ∈ ℤ) | 
| 75 | 74 | zcnd 12723 | . . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) ∧ (2 · 𝐴) ∥ (𝐵 − -𝐶)) ∧ 𝐶 ∈ (0...(𝐴 − 1))) → -𝐶 ∈ ℂ) | 
| 76 | 72, 75 | abssubd 15492 | . . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) ∧ (2 · 𝐴) ∥ (𝐵 − -𝐶)) ∧ 𝐶 ∈ (0...(𝐴 − 1))) → (abs‘(𝐵 − -𝐶)) = (abs‘(-𝐶 − 𝐵))) | 
| 77 |  | 0zd 12625 | . . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) ∧ (2 · 𝐴) ∥ (𝐵 − -𝐶)) ∧ 𝐶 ∈ (0...(𝐴 − 1))) → 0 ∈
ℤ) | 
| 78 |  | simpr 484 | . . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) ∧ (2 · 𝐴) ∥ (𝐵 − -𝐶)) ∧ 𝐶 ∈ (0...(𝐴 − 1))) → 𝐶 ∈ (0...(𝐴 − 1))) | 
| 79 |  | 0zd 12625 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) → 0 ∈ ℤ) | 
| 80 |  | 1z 12647 | . . . . . . . . . . . . . . . . . . 19
⊢ 1 ∈
ℤ | 
| 81 |  | zsubcl 12659 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 ∈ ℤ ∧ 1 ∈
ℤ) → (𝐴 −
1) ∈ ℤ) | 
| 82 | 3, 80, 81 | sylancl 586 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) → (𝐴 − 1) ∈ ℤ) | 
| 83 |  | fzneg 42994 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝐶 ∈ ℤ ∧ 0 ∈
ℤ ∧ (𝐴 − 1)
∈ ℤ) → (𝐶
∈ (0...(𝐴 − 1))
↔ -𝐶 ∈ (-(𝐴 −
1)...-0))) | 
| 84 | 16, 79, 82, 83 | syl3anc 1373 | . . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) → (𝐶 ∈ (0...(𝐴 − 1)) ↔ -𝐶 ∈ (-(𝐴 − 1)...-0))) | 
| 85 | 84 | ad2antrr 726 | . . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) ∧ (2 · 𝐴) ∥ (𝐵 − -𝐶)) ∧ 𝐶 ∈ (0...(𝐴 − 1))) → (𝐶 ∈ (0...(𝐴 − 1)) ↔ -𝐶 ∈ (-(𝐴 − 1)...-0))) | 
| 86 | 78, 85 | mpbid 232 | . . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) ∧ (2 · 𝐴) ∥ (𝐵 − -𝐶)) ∧ 𝐶 ∈ (0...(𝐴 − 1))) → -𝐶 ∈ (-(𝐴 − 1)...-0)) | 
| 87 |  | neg0 11555 | . . . . . . . . . . . . . . . . 17
⊢ -0 =
0 | 
| 88 | 87 | a1i 11 | . . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) ∧ (2 · 𝐴) ∥ (𝐵 − -𝐶)) ∧ 𝐶 ∈ (0...(𝐴 − 1))) → -0 =
0) | 
| 89 | 88 | oveq2d 7447 | . . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) ∧ (2 · 𝐴) ∥ (𝐵 − -𝐶)) ∧ 𝐶 ∈ (0...(𝐴 − 1))) → (-(𝐴 − 1)...-0) = (-(𝐴 − 1)...0)) | 
| 90 | 86, 89 | eleqtrd 2843 | . . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) ∧ (2 · 𝐴) ∥ (𝐵 − -𝐶)) ∧ 𝐶 ∈ (0...(𝐴 − 1))) → -𝐶 ∈ (-(𝐴 − 1)...0)) | 
| 91 | 3 | ad2antrr 726 | . . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) ∧ (2 · 𝐴) ∥ (𝐵 − -𝐶)) ∧ 𝐶 ∈ (0...(𝐴 − 1))) → 𝐴 ∈ ℤ) | 
| 92 |  | simp1 1137 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) → 𝐴 ∈ ℕ) | 
| 93 | 42, 92, 44 | sylancr 587 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) → (2 · 𝐴) ∈ ℕ) | 
| 94 |  | nnm1nn0 12567 | . . . . . . . . . . . . . . . . . 18
⊢ ((2
· 𝐴) ∈ ℕ
→ ((2 · 𝐴)
− 1) ∈ ℕ0) | 
| 95 | 93, 94 | syl 17 | . . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) → ((2 · 𝐴) − 1) ∈
ℕ0) | 
| 96 | 95 | nn0ge0d 12590 | . . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) → 0 ≤ ((2 · 𝐴) − 1)) | 
| 97 |  | 0m0e0 12386 | . . . . . . . . . . . . . . . . 17
⊢ (0
− 0) = 0 | 
| 98 | 97 | a1i 11 | . . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) → (0 − 0) =
0) | 
| 99 |  | 1cnd 11256 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) → 1 ∈ ℂ) | 
| 100 | 36, 36, 99 | addsubassd 11640 | . . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) → ((𝐴 + 𝐴) − 1) = (𝐴 + (𝐴 − 1))) | 
| 101 | 38 | oveq1d 7446 | . . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) → ((2 · 𝐴) − 1) = ((𝐴 + 𝐴) − 1)) | 
| 102 |  | ax-1cn 11213 | . . . . . . . . . . . . . . . . . . 19
⊢ 1 ∈
ℂ | 
| 103 |  | subcl 11507 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 ∈ ℂ ∧ 1 ∈
ℂ) → (𝐴 −
1) ∈ ℂ) | 
| 104 | 36, 102, 103 | sylancl 586 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) → (𝐴 − 1) ∈ ℂ) | 
| 105 | 36, 104 | subnegd 11627 | . . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) → (𝐴 − -(𝐴 − 1)) = (𝐴 + (𝐴 − 1))) | 
| 106 | 100, 101,
105 | 3eqtr4rd 2788 | . . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) → (𝐴 − -(𝐴 − 1)) = ((2 · 𝐴) − 1)) | 
| 107 | 96, 98, 106 | 3brtr4d 5175 | . . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) → (0 − 0) ≤ (𝐴 − -(𝐴 − 1))) | 
| 108 | 107 | ad2antrr 726 | . . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) ∧ (2 · 𝐴) ∥ (𝐵 − -𝐶)) ∧ 𝐶 ∈ (0...(𝐴 − 1))) → (0 − 0) ≤
(𝐴 − -(𝐴 − 1))) | 
| 109 |  | fzmaxdif 42993 | . . . . . . . . . . . . . 14
⊢ (((0
∈ ℤ ∧ -𝐶
∈ (-(𝐴 −
1)...0)) ∧ (𝐴 ∈
ℤ ∧ 𝐵 ∈
(0...𝐴)) ∧ (0 −
0) ≤ (𝐴 − -(𝐴 − 1))) →
(abs‘(-𝐶 −
𝐵)) ≤ (𝐴 − -(𝐴 − 1))) | 
| 110 | 77, 90, 91, 54, 108, 109 | syl221anc 1383 | . . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) ∧ (2 · 𝐴) ∥ (𝐵 − -𝐶)) ∧ 𝐶 ∈ (0...(𝐴 − 1))) → (abs‘(-𝐶 − 𝐵)) ≤ (𝐴 − -(𝐴 − 1))) | 
| 111 | 76, 110 | eqbrtrd 5165 | . . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) ∧ (2 · 𝐴) ∥ (𝐵 − -𝐶)) ∧ 𝐶 ∈ (0...(𝐴 − 1))) → (abs‘(𝐵 − -𝐶)) ≤ (𝐴 − -(𝐴 − 1))) | 
| 112 | 27 | ltm1d 12200 | . . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) → ((2 · 𝐴) − 1) < (2 · 𝐴)) | 
| 113 | 106, 112 | eqbrtrd 5165 | . . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) → (𝐴 − -(𝐴 − 1)) < (2 · 𝐴)) | 
| 114 | 113 | ad2antrr 726 | . . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) ∧ (2 · 𝐴) ∥ (𝐵 − -𝐶)) ∧ 𝐶 ∈ (0...(𝐴 − 1))) → (𝐴 − -(𝐴 − 1)) < (2 · 𝐴)) | 
| 115 | 63, 69, 70, 111, 114 | lelttrd 11419 | . . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) ∧ (2 · 𝐴) ∥ (𝐵 − -𝐶)) ∧ 𝐶 ∈ (0...(𝐴 − 1))) → (abs‘(𝐵 − -𝐶)) < (2 · 𝐴)) | 
| 116 | 93 | ad2antrr 726 | . . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) ∧ (2 · 𝐴) ∥ (𝐵 − -𝐶)) ∧ 𝐶 ∈ (0...(𝐴 − 1))) → (2 · 𝐴) ∈
ℕ) | 
| 117 |  | simplr 769 | . . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) ∧ (2 · 𝐴) ∥ (𝐵 − -𝐶)) ∧ 𝐶 ∈ (0...(𝐴 − 1))) → (2 · 𝐴) ∥ (𝐵 − -𝐶)) | 
| 118 |  | congabseq 42986 | . . . . . . . . . . . 12
⊢ ((((2
· 𝐴) ∈ ℕ
∧ 𝐵 ∈ ℤ
∧ -𝐶 ∈ ℤ)
∧ (2 · 𝐴)
∥ (𝐵 − -𝐶)) → ((abs‘(𝐵 − -𝐶)) < (2 · 𝐴) ↔ 𝐵 = -𝐶)) | 
| 119 | 116, 71, 74, 117, 118 | syl31anc 1375 | . . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) ∧ (2 · 𝐴) ∥ (𝐵 − -𝐶)) ∧ 𝐶 ∈ (0...(𝐴 − 1))) → ((abs‘(𝐵 − -𝐶)) < (2 · 𝐴) ↔ 𝐵 = -𝐶)) | 
| 120 | 115, 119 | mpbid 232 | . . . . . . . . . 10
⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) ∧ (2 · 𝐴) ∥ (𝐵 − -𝐶)) ∧ 𝐶 ∈ (0...(𝐴 − 1))) → 𝐵 = -𝐶) | 
| 121 | 56, 120 | breqtrd 5169 | . . . . . . . . 9
⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) ∧ (2 · 𝐴) ∥ (𝐵 − -𝐶)) ∧ 𝐶 ∈ (0...(𝐴 − 1))) → 0 ≤ -𝐶) | 
| 122 |  | elfzelz 13564 | . . . . . . . . . . . 12
⊢ (𝐶 ∈ (0...(𝐴 − 1)) → 𝐶 ∈ ℤ) | 
| 123 | 122 | zred 12722 | . . . . . . . . . . 11
⊢ (𝐶 ∈ (0...(𝐴 − 1)) → 𝐶 ∈ ℝ) | 
| 124 | 123 | adantl 481 | . . . . . . . . . 10
⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) ∧ (2 · 𝐴) ∥ (𝐵 − -𝐶)) ∧ 𝐶 ∈ (0...(𝐴 − 1))) → 𝐶 ∈ ℝ) | 
| 125 | 124 | le0neg1d 11834 | . . . . . . . . 9
⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) ∧ (2 · 𝐴) ∥ (𝐵 − -𝐶)) ∧ 𝐶 ∈ (0...(𝐴 − 1))) → (𝐶 ≤ 0 ↔ 0 ≤ -𝐶)) | 
| 126 | 121, 125 | mpbird 257 | . . . . . . . 8
⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) ∧ (2 · 𝐴) ∥ (𝐵 − -𝐶)) ∧ 𝐶 ∈ (0...(𝐴 − 1))) → 𝐶 ≤ 0) | 
| 127 |  | elfzle1 13567 | . . . . . . . . 9
⊢ (𝐶 ∈ (0...(𝐴 − 1)) → 0 ≤ 𝐶) | 
| 128 | 127 | adantl 481 | . . . . . . . 8
⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) ∧ (2 · 𝐴) ∥ (𝐵 − -𝐶)) ∧ 𝐶 ∈ (0...(𝐴 − 1))) → 0 ≤ 𝐶) | 
| 129 |  | letri3 11346 | . . . . . . . . 9
⊢ ((𝐶 ∈ ℝ ∧ 0 ∈
ℝ) → (𝐶 = 0
↔ (𝐶 ≤ 0 ∧ 0
≤ 𝐶))) | 
| 130 | 124, 22, 129 | sylancl 586 | . . . . . . . 8
⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) ∧ (2 · 𝐴) ∥ (𝐵 − -𝐶)) ∧ 𝐶 ∈ (0...(𝐴 − 1))) → (𝐶 = 0 ↔ (𝐶 ≤ 0 ∧ 0 ≤ 𝐶))) | 
| 131 | 126, 128,
130 | mpbir2and 713 | . . . . . . 7
⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) ∧ (2 · 𝐴) ∥ (𝐵 − -𝐶)) ∧ 𝐶 ∈ (0...(𝐴 − 1))) → 𝐶 = 0) | 
| 132 | 131 | negeqd 11502 | . . . . . 6
⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) ∧ (2 · 𝐴) ∥ (𝐵 − -𝐶)) ∧ 𝐶 ∈ (0...(𝐴 − 1))) → -𝐶 = -0) | 
| 133 | 132, 88 | eqtrd 2777 | . . . . 5
⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) ∧ (2 · 𝐴) ∥ (𝐵 − -𝐶)) ∧ 𝐶 ∈ (0...(𝐴 − 1))) → -𝐶 = 0) | 
| 134 | 133, 120,
131 | 3eqtr4d 2787 | . . . 4
⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) ∧ (2 · 𝐴) ∥ (𝐵 − -𝐶)) ∧ 𝐶 ∈ (0...(𝐴 − 1))) → 𝐵 = 𝐶) | 
| 135 |  | oveq2 7439 | . . . . . . . . 9
⊢ (𝐶 = 𝐴 → (𝐵 − 𝐶) = (𝐵 − 𝐴)) | 
| 136 | 135 | adantl 481 | . . . . . . . 8
⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) ∧ (2 · 𝐴) ∥ (𝐵 − -𝐶)) ∧ 𝐶 = 𝐴) → (𝐵 − 𝐶) = (𝐵 − 𝐴)) | 
| 137 | 136 | fveq2d 6910 | . . . . . . 7
⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) ∧ (2 · 𝐴) ∥ (𝐵 − -𝐶)) ∧ 𝐶 = 𝐴) → (abs‘(𝐵 − 𝐶)) = (abs‘(𝐵 − 𝐴))) | 
| 138 | 40 | ad2antrr 726 | . . . . . . 7
⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) ∧ (2 · 𝐴) ∥ (𝐵 − -𝐶)) ∧ 𝐶 = 𝐴) → (abs‘(𝐵 − 𝐶)) < (2 · 𝐴)) | 
| 139 | 137, 138 | eqbrtrrd 5167 | . . . . . 6
⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) ∧ (2 · 𝐴) ∥ (𝐵 − -𝐶)) ∧ 𝐶 = 𝐴) → (abs‘(𝐵 − 𝐴)) < (2 · 𝐴)) | 
| 140 | 93 | ad2antrr 726 | . . . . . . 7
⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) ∧ (2 · 𝐴) ∥ (𝐵 − -𝐶)) ∧ 𝐶 = 𝐴) → (2 · 𝐴) ∈ ℕ) | 
| 141 | 7 | ad2antrr 726 | . . . . . . 7
⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) ∧ (2 · 𝐴) ∥ (𝐵 − -𝐶)) ∧ 𝐶 = 𝐴) → 𝐵 ∈ ℤ) | 
| 142 | 3 | ad2antrr 726 | . . . . . . 7
⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) ∧ (2 · 𝐴) ∥ (𝐵 − -𝐶)) ∧ 𝐶 = 𝐴) → 𝐴 ∈ ℤ) | 
| 143 |  | simplr 769 | . . . . . . . . 9
⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) ∧ (2 · 𝐴) ∥ (𝐵 − -𝐶)) ∧ 𝐶 = 𝐴) → (2 · 𝐴) ∥ (𝐵 − -𝐶)) | 
| 144 | 7 | zcnd 12723 | . . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) → 𝐵 ∈ ℂ) | 
| 145 | 36, 36, 144 | ppncand 11660 | . . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) → ((𝐴 + 𝐴) + (𝐵 − 𝐴)) = (𝐴 + 𝐵)) | 
| 146 | 36, 144 | addcomd 11463 | . . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) → (𝐴 + 𝐵) = (𝐵 + 𝐴)) | 
| 147 | 145, 146 | eqtrd 2777 | . . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) → ((𝐴 + 𝐴) + (𝐵 − 𝐴)) = (𝐵 + 𝐴)) | 
| 148 | 147 | ad2antrr 726 | . . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) ∧ (2 · 𝐴) ∥ (𝐵 − -𝐶)) ∧ 𝐶 = 𝐴) → ((𝐴 + 𝐴) + (𝐵 − 𝐴)) = (𝐵 + 𝐴)) | 
| 149 |  | oveq2 7439 | . . . . . . . . . . . 12
⊢ (𝐶 = 𝐴 → (𝐵 + 𝐶) = (𝐵 + 𝐴)) | 
| 150 | 149 | adantl 481 | . . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) ∧ (2 · 𝐴) ∥ (𝐵 − -𝐶)) ∧ 𝐶 = 𝐴) → (𝐵 + 𝐶) = (𝐵 + 𝐴)) | 
| 151 | 148, 150 | eqtr4d 2780 | . . . . . . . . . 10
⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) ∧ (2 · 𝐴) ∥ (𝐵 − -𝐶)) ∧ 𝐶 = 𝐴) → ((𝐴 + 𝐴) + (𝐵 − 𝐴)) = (𝐵 + 𝐶)) | 
| 152 | 38 | oveq1d 7446 | . . . . . . . . . . 11
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) → ((2 · 𝐴) + (𝐵 − 𝐴)) = ((𝐴 + 𝐴) + (𝐵 − 𝐴))) | 
| 153 | 152 | ad2antrr 726 | . . . . . . . . . 10
⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) ∧ (2 · 𝐴) ∥ (𝐵 − -𝐶)) ∧ 𝐶 = 𝐴) → ((2 · 𝐴) + (𝐵 − 𝐴)) = ((𝐴 + 𝐴) + (𝐵 − 𝐴))) | 
| 154 | 16 | zcnd 12723 | . . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) → 𝐶 ∈ ℂ) | 
| 155 | 144, 154 | subnegd 11627 | . . . . . . . . . . 11
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) → (𝐵 − -𝐶) = (𝐵 + 𝐶)) | 
| 156 | 155 | ad2antrr 726 | . . . . . . . . . 10
⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) ∧ (2 · 𝐴) ∥ (𝐵 − -𝐶)) ∧ 𝐶 = 𝐴) → (𝐵 − -𝐶) = (𝐵 + 𝐶)) | 
| 157 | 151, 153,
156 | 3eqtr4d 2787 | . . . . . . . . 9
⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) ∧ (2 · 𝐴) ∥ (𝐵 − -𝐶)) ∧ 𝐶 = 𝐴) → ((2 · 𝐴) + (𝐵 − 𝐴)) = (𝐵 − -𝐶)) | 
| 158 | 143, 157 | breqtrrd 5171 | . . . . . . . 8
⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) ∧ (2 · 𝐴) ∥ (𝐵 − -𝐶)) ∧ 𝐶 = 𝐴) → (2 · 𝐴) ∥ ((2 · 𝐴) + (𝐵 − 𝐴))) | 
| 159 | 5 | ad2antrr 726 | . . . . . . . . 9
⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) ∧ (2 · 𝐴) ∥ (𝐵 − -𝐶)) ∧ 𝐶 = 𝐴) → (2 · 𝐴) ∈ ℤ) | 
| 160 | 7, 3 | zsubcld 12727 | . . . . . . . . . 10
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) → (𝐵 − 𝐴) ∈ ℤ) | 
| 161 | 160 | ad2antrr 726 | . . . . . . . . 9
⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) ∧ (2 · 𝐴) ∥ (𝐵 − -𝐶)) ∧ 𝐶 = 𝐴) → (𝐵 − 𝐴) ∈ ℤ) | 
| 162 |  | dvdsadd 16339 | . . . . . . . . 9
⊢ (((2
· 𝐴) ∈ ℤ
∧ (𝐵 − 𝐴) ∈ ℤ) → ((2
· 𝐴) ∥ (𝐵 − 𝐴) ↔ (2 · 𝐴) ∥ ((2 · 𝐴) + (𝐵 − 𝐴)))) | 
| 163 | 159, 161,
162 | syl2anc 584 | . . . . . . . 8
⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) ∧ (2 · 𝐴) ∥ (𝐵 − -𝐶)) ∧ 𝐶 = 𝐴) → ((2 · 𝐴) ∥ (𝐵 − 𝐴) ↔ (2 · 𝐴) ∥ ((2 · 𝐴) + (𝐵 − 𝐴)))) | 
| 164 | 158, 163 | mpbird 257 | . . . . . . 7
⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) ∧ (2 · 𝐴) ∥ (𝐵 − -𝐶)) ∧ 𝐶 = 𝐴) → (2 · 𝐴) ∥ (𝐵 − 𝐴)) | 
| 165 |  | congabseq 42986 | . . . . . . 7
⊢ ((((2
· 𝐴) ∈ ℕ
∧ 𝐵 ∈ ℤ
∧ 𝐴 ∈ ℤ)
∧ (2 · 𝐴)
∥ (𝐵 − 𝐴)) → ((abs‘(𝐵 − 𝐴)) < (2 · 𝐴) ↔ 𝐵 = 𝐴)) | 
| 166 | 140, 141,
142, 164, 165 | syl31anc 1375 | . . . . . 6
⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) ∧ (2 · 𝐴) ∥ (𝐵 − -𝐶)) ∧ 𝐶 = 𝐴) → ((abs‘(𝐵 − 𝐴)) < (2 · 𝐴) ↔ 𝐵 = 𝐴)) | 
| 167 | 139, 166 | mpbid 232 | . . . . 5
⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) ∧ (2 · 𝐴) ∥ (𝐵 − -𝐶)) ∧ 𝐶 = 𝐴) → 𝐵 = 𝐴) | 
| 168 |  | simpr 484 | . . . . 5
⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) ∧ (2 · 𝐴) ∥ (𝐵 − -𝐶)) ∧ 𝐶 = 𝐴) → 𝐶 = 𝐴) | 
| 169 | 167, 168 | eqtr4d 2780 | . . . 4
⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) ∧ (2 · 𝐴) ∥ (𝐵 − -𝐶)) ∧ 𝐶 = 𝐴) → 𝐵 = 𝐶) | 
| 170 |  | nnnn0 12533 | . . . . . . . 8
⊢ (𝐴 ∈ ℕ → 𝐴 ∈
ℕ0) | 
| 171 | 170 | 3ad2ant1 1134 | . . . . . . 7
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) → 𝐴 ∈
ℕ0) | 
| 172 |  | nn0uz 12920 | . . . . . . 7
⊢
ℕ0 = (ℤ≥‘0) | 
| 173 | 171, 172 | eleqtrdi 2851 | . . . . . 6
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) → 𝐴 ∈
(ℤ≥‘0)) | 
| 174 |  | fzm1 13647 | . . . . . . 7
⊢ (𝐴 ∈
(ℤ≥‘0) → (𝐶 ∈ (0...𝐴) ↔ (𝐶 ∈ (0...(𝐴 − 1)) ∨ 𝐶 = 𝐴))) | 
| 175 | 174 | biimpa 476 | . . . . . 6
⊢ ((𝐴 ∈
(ℤ≥‘0) ∧ 𝐶 ∈ (0...𝐴)) → (𝐶 ∈ (0...(𝐴 − 1)) ∨ 𝐶 = 𝐴)) | 
| 176 | 173, 29, 175 | syl2anc 584 | . . . . 5
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) → (𝐶 ∈ (0...(𝐴 − 1)) ∨ 𝐶 = 𝐴)) | 
| 177 | 176 | adantr 480 | . . . 4
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) ∧ (2 · 𝐴) ∥ (𝐵 − -𝐶)) → (𝐶 ∈ (0...(𝐴 − 1)) ∨ 𝐶 = 𝐴)) | 
| 178 | 134, 169,
177 | mpjaodan 961 | . . 3
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) ∧ (2 · 𝐴) ∥ (𝐵 − -𝐶)) → 𝐵 = 𝐶) | 
| 179 | 53, 178 | jaodan 960 | . 2
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) ∧ ((2 · 𝐴) ∥ (𝐵 − 𝐶) ∨ (2 · 𝐴) ∥ (𝐵 − -𝐶))) → 𝐵 = 𝐶) | 
| 180 | 14, 179 | impbida 801 | 1
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) → (𝐵 = 𝐶 ↔ ((2 · 𝐴) ∥ (𝐵 − 𝐶) ∨ (2 · 𝐴) ∥ (𝐵 − -𝐶)))) |