Metamath Proof Explorer

Theorem acongeq

Description: Two numbers in the fundamental domain are alternating-congruent iff they are equal. TODO: could be used to shorten jm2.26 . (Contributed by Stefan O'Rear, 4-Oct-2014)

Ref Expression
Assertion acongeq ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → ( 𝐵 = 𝐶 ↔ ( ( 2 · 𝐴 ) ∥ ( 𝐵 − 𝐶 ) ∨ ( 2 · 𝐴 ) ∥ ( 𝐵 − - 𝐶 ) ) ) )

Proof

Step Hyp Ref Expression
1 2z ⊢ 2 ∈ ℤ
2 nnz ⊢ ( 𝐴 ∈ ℕ → 𝐴 ∈ ℤ )
3 2 3ad2ant1 ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → 𝐴 ∈ ℤ )
4 zmulcl ⊢ ( ( 2 ∈ ℤ ∧ 𝐴 ∈ ℤ ) → ( 2 · 𝐴 ) ∈ ℤ )
5 1 3 4 sylancr ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → ( 2 · 𝐴 ) ∈ ℤ )
6 elfzelz ⊢ ( 𝐵 ∈ ( 0 ... 𝐴 ) → 𝐵 ∈ ℤ )
7 6 3ad2ant2 ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → 𝐵 ∈ ℤ )
8 congid ⊢ ( ( ( 2 · 𝐴 ) ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 2 · 𝐴 ) ∥ ( 𝐵 − 𝐵 ) )
9 5 7 8 syl2anc ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → ( 2 · 𝐴 ) ∥ ( 𝐵 − 𝐵 ) )
10 9 adantr ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) ∧ 𝐵 = 𝐶 ) → ( 2 · 𝐴 ) ∥ ( 𝐵 − 𝐵 ) )
11 oveq2 ⊢ ( 𝐵 = 𝐶 → ( 𝐵 − 𝐵 ) = ( 𝐵 − 𝐶 ) )
12 11 adantl ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) ∧ 𝐵 = 𝐶 ) → ( 𝐵 − 𝐵 ) = ( 𝐵 − 𝐶 ) )
13 10 12 breqtrd ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) ∧ 𝐵 = 𝐶 ) → ( 2 · 𝐴 ) ∥ ( 𝐵 − 𝐶 ) )
14 13 orcd ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) ∧ 𝐵 = 𝐶 ) → ( ( 2 · 𝐴 ) ∥ ( 𝐵 − 𝐶 ) ∨ ( 2 · 𝐴 ) ∥ ( 𝐵 − - 𝐶 ) ) )
15 elfzelz ⊢ ( 𝐶 ∈ ( 0 ... 𝐴 ) → 𝐶 ∈ ℤ )
16 15 3ad2ant3 ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → 𝐶 ∈ ℤ )
17 7 16 zsubcld ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → ( 𝐵 − 𝐶 ) ∈ ℤ )
18 17 zcnd ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → ( 𝐵 − 𝐶 ) ∈ ℂ )
19 18 abscld ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → ( abs ‘ ( 𝐵 − 𝐶 ) ) ∈ ℝ )
20 nnre ⊢ ( 𝐴 ∈ ℕ → 𝐴 ∈ ℝ )
21 20 3ad2ant1 ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → 𝐴 ∈ ℝ )
22 0re ⊢ 0 ∈ ℝ
23 resubcl ⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ∈ ℝ ) → ( 𝐴 − 0 ) ∈ ℝ )
24 21 22 23 sylancl ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → ( 𝐴 − 0 ) ∈ ℝ )
25 2re ⊢ 2 ∈ ℝ
26 remulcl ⊢ ( ( 2 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( 2 · 𝐴 ) ∈ ℝ )
27 25 21 26 sylancr ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → ( 2 · 𝐴 ) ∈ ℝ )
28 simp2 ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → 𝐵 ∈ ( 0 ... 𝐴 ) )
29 simp3 ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → 𝐶 ∈ ( 0 ... 𝐴 ) )
30 24 leidd ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → ( 𝐴 − 0 ) ≤ ( 𝐴 − 0 ) )
31 fzmaxdif ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ) ∧ ( 𝐴 ∈ ℤ ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) ∧ ( 𝐴 − 0 ) ≤ ( 𝐴 − 0 ) ) → ( abs ‘ ( 𝐵 − 𝐶 ) ) ≤ ( 𝐴 − 0 ) )
32 3 28 3 29 30 31 syl221anc ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → ( abs ‘ ( 𝐵 − 𝐶 ) ) ≤ ( 𝐴 − 0 ) )
33 nnrp ⊢ ( 𝐴 ∈ ℕ → 𝐴 ∈ ℝ+ )
34 33 3ad2ant1 ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → 𝐴 ∈ ℝ+ )
35 21 34 ltaddrpd ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → 𝐴 < ( 𝐴 + 𝐴 ) )
36 21 recnd ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → 𝐴 ∈ ℂ )
37 36 subid1d ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → ( 𝐴 − 0 ) = 𝐴 )
38 36 2timesd ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → ( 2 · 𝐴 ) = ( 𝐴 + 𝐴 ) )
39 35 37 38 3brtr4d ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → ( 𝐴 − 0 ) < ( 2 · 𝐴 ) )
40 19 24 27 32 39 lelttrd ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → ( abs ‘ ( 𝐵 − 𝐶 ) ) < ( 2 · 𝐴 ) )
41 40 adantr ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) ∧ ( 2 · 𝐴 ) ∥ ( 𝐵 − 𝐶 ) ) → ( abs ‘ ( 𝐵 − 𝐶 ) ) < ( 2 · 𝐴 ) )
42 2nn ⊢ 2 ∈ ℕ
43 simpl1 ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) ∧ ( 2 · 𝐴 ) ∥ ( 𝐵 − 𝐶 ) ) → 𝐴 ∈ ℕ )
44 nnmulcl ⊢ ( ( 2 ∈ ℕ ∧ 𝐴 ∈ ℕ ) → ( 2 · 𝐴 ) ∈ ℕ )
45 42 43 44 sylancr ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) ∧ ( 2 · 𝐴 ) ∥ ( 𝐵 − 𝐶 ) ) → ( 2 · 𝐴 ) ∈ ℕ )
46 simpl2 ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) ∧ ( 2 · 𝐴 ) ∥ ( 𝐵 − 𝐶 ) ) → 𝐵 ∈ ( 0 ... 𝐴 ) )
47 46 6 syl ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) ∧ ( 2 · 𝐴 ) ∥ ( 𝐵 − 𝐶 ) ) → 𝐵 ∈ ℤ )
48 simpl3 ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) ∧ ( 2 · 𝐴 ) ∥ ( 𝐵 − 𝐶 ) ) → 𝐶 ∈ ( 0 ... 𝐴 ) )
49 48 15 syl ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) ∧ ( 2 · 𝐴 ) ∥ ( 𝐵 − 𝐶 ) ) → 𝐶 ∈ ℤ )
50 simpr ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) ∧ ( 2 · 𝐴 ) ∥ ( 𝐵 − 𝐶 ) ) → ( 2 · 𝐴 ) ∥ ( 𝐵 − 𝐶 ) )
51 congabseq ⊢ ( ( ( ( 2 · 𝐴 ) ∈ ℕ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 2 · 𝐴 ) ∥ ( 𝐵 − 𝐶 ) ) → ( ( abs ‘ ( 𝐵 − 𝐶 ) ) < ( 2 · 𝐴 ) ↔ 𝐵 = 𝐶 ) )
52 45 47 49 50 51 syl31anc ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) ∧ ( 2 · 𝐴 ) ∥ ( 𝐵 − 𝐶 ) ) → ( ( abs ‘ ( 𝐵 − 𝐶 ) ) < ( 2 · 𝐴 ) ↔ 𝐵 = 𝐶 ) )
53 41 52 mpbid ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) ∧ ( 2 · 𝐴 ) ∥ ( 𝐵 − 𝐶 ) ) → 𝐵 = 𝐶 )
54 simpll2 ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) ∧ ( 2 · 𝐴 ) ∥ ( 𝐵 − - 𝐶 ) ) ∧ 𝐶 ∈ ( 0 ... ( 𝐴 − 1 ) ) ) → 𝐵 ∈ ( 0 ... 𝐴 ) )
55 elfzle1 ⊢ ( 𝐵 ∈ ( 0 ... 𝐴 ) → 0 ≤ 𝐵 )
56 54 55 syl ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) ∧ ( 2 · 𝐴 ) ∥ ( 𝐵 − - 𝐶 ) ) ∧ 𝐶 ∈ ( 0 ... ( 𝐴 − 1 ) ) ) → 0 ≤ 𝐵 )
57 7 zred ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → 𝐵 ∈ ℝ )
58 16 zred ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → 𝐶 ∈ ℝ )
59 58 renegcld ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → - 𝐶 ∈ ℝ )
60 57 59 resubcld ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → ( 𝐵 − - 𝐶 ) ∈ ℝ )
61 60 recnd ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → ( 𝐵 − - 𝐶 ) ∈ ℂ )
62 61 abscld ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → ( abs ‘ ( 𝐵 − - 𝐶 ) ) ∈ ℝ )
63 62 ad2antrr ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) ∧ ( 2 · 𝐴 ) ∥ ( 𝐵 − - 𝐶 ) ) ∧ 𝐶 ∈ ( 0 ... ( 𝐴 − 1 ) ) ) → ( abs ‘ ( 𝐵 − - 𝐶 ) ) ∈ ℝ )
64 1re ⊢ 1 ∈ ℝ
65 resubcl ⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ∈ ℝ ) → ( 𝐴 − 1 ) ∈ ℝ )
66 21 64 65 sylancl ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → ( 𝐴 − 1 ) ∈ ℝ )
67 66 renegcld ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → - ( 𝐴 − 1 ) ∈ ℝ )
68 21 67 resubcld ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → ( 𝐴 − - ( 𝐴 − 1 ) ) ∈ ℝ )
69 68 ad2antrr ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) ∧ ( 2 · 𝐴 ) ∥ ( 𝐵 − - 𝐶 ) ) ∧ 𝐶 ∈ ( 0 ... ( 𝐴 − 1 ) ) ) → ( 𝐴 − - ( 𝐴 − 1 ) ) ∈ ℝ )
70 27 ad2antrr ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) ∧ ( 2 · 𝐴 ) ∥ ( 𝐵 − - 𝐶 ) ) ∧ 𝐶 ∈ ( 0 ... ( 𝐴 − 1 ) ) ) → ( 2 · 𝐴 ) ∈ ℝ )
71 7 ad2antrr ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) ∧ ( 2 · 𝐴 ) ∥ ( 𝐵 − - 𝐶 ) ) ∧ 𝐶 ∈ ( 0 ... ( 𝐴 − 1 ) ) ) → 𝐵 ∈ ℤ )
72 71 zcnd ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) ∧ ( 2 · 𝐴 ) ∥ ( 𝐵 − - 𝐶 ) ) ∧ 𝐶 ∈ ( 0 ... ( 𝐴 − 1 ) ) ) → 𝐵 ∈ ℂ )
73 16 znegcld ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → - 𝐶 ∈ ℤ )
74 73 ad2antrr ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) ∧ ( 2 · 𝐴 ) ∥ ( 𝐵 − - 𝐶 ) ) ∧ 𝐶 ∈ ( 0 ... ( 𝐴 − 1 ) ) ) → - 𝐶 ∈ ℤ )
75 74 zcnd ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) ∧ ( 2 · 𝐴 ) ∥ ( 𝐵 − - 𝐶 ) ) ∧ 𝐶 ∈ ( 0 ... ( 𝐴 − 1 ) ) ) → - 𝐶 ∈ ℂ )
76 72 75 abssubd ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) ∧ ( 2 · 𝐴 ) ∥ ( 𝐵 − - 𝐶 ) ) ∧ 𝐶 ∈ ( 0 ... ( 𝐴 − 1 ) ) ) → ( abs ‘ ( 𝐵 − - 𝐶 ) ) = ( abs ‘ ( - 𝐶 − 𝐵 ) ) )
77 0zd ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) ∧ ( 2 · 𝐴 ) ∥ ( 𝐵 − - 𝐶 ) ) ∧ 𝐶 ∈ ( 0 ... ( 𝐴 − 1 ) ) ) → 0 ∈ ℤ )
78 simpr ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) ∧ ( 2 · 𝐴 ) ∥ ( 𝐵 − - 𝐶 ) ) ∧ 𝐶 ∈ ( 0 ... ( 𝐴 − 1 ) ) ) → 𝐶 ∈ ( 0 ... ( 𝐴 − 1 ) ) )
79 0zd ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → 0 ∈ ℤ )
80 1z ⊢ 1 ∈ ℤ
81 zsubcl ⊢ ( ( 𝐴 ∈ ℤ ∧ 1 ∈ ℤ ) → ( 𝐴 − 1 ) ∈ ℤ )
82 3 80 81 sylancl ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → ( 𝐴 − 1 ) ∈ ℤ )
83 fzneg ⊢ ( ( 𝐶 ∈ ℤ ∧ 0 ∈ ℤ ∧ ( 𝐴 − 1 ) ∈ ℤ ) → ( 𝐶 ∈ ( 0 ... ( 𝐴 − 1 ) ) ↔ - 𝐶 ∈ ( - ( 𝐴 − 1 ) ... - 0 ) ) )
84 16 79 82 83 syl3anc ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → ( 𝐶 ∈ ( 0 ... ( 𝐴 − 1 ) ) ↔ - 𝐶 ∈ ( - ( 𝐴 − 1 ) ... - 0 ) ) )
85 84 ad2antrr ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) ∧ ( 2 · 𝐴 ) ∥ ( 𝐵 − - 𝐶 ) ) ∧ 𝐶 ∈ ( 0 ... ( 𝐴 − 1 ) ) ) → ( 𝐶 ∈ ( 0 ... ( 𝐴 − 1 ) ) ↔ - 𝐶 ∈ ( - ( 𝐴 − 1 ) ... - 0 ) ) )
86 78 85 mpbid ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) ∧ ( 2 · 𝐴 ) ∥ ( 𝐵 − - 𝐶 ) ) ∧ 𝐶 ∈ ( 0 ... ( 𝐴 − 1 ) ) ) → - 𝐶 ∈ ( - ( 𝐴 − 1 ) ... - 0 ) )
87 neg0 ⊢ - 0 = 0
88 87 a1i ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) ∧ ( 2 · 𝐴 ) ∥ ( 𝐵 − - 𝐶 ) ) ∧ 𝐶 ∈ ( 0 ... ( 𝐴 − 1 ) ) ) → - 0 = 0 )
89 88 oveq2d ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) ∧ ( 2 · 𝐴 ) ∥ ( 𝐵 − - 𝐶 ) ) ∧ 𝐶 ∈ ( 0 ... ( 𝐴 − 1 ) ) ) → ( - ( 𝐴 − 1 ) ... - 0 ) = ( - ( 𝐴 − 1 ) ... 0 ) )
90 86 89 eleqtrd ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) ∧ ( 2 · 𝐴 ) ∥ ( 𝐵 − - 𝐶 ) ) ∧ 𝐶 ∈ ( 0 ... ( 𝐴 − 1 ) ) ) → - 𝐶 ∈ ( - ( 𝐴 − 1 ) ... 0 ) )
91 3 ad2antrr ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) ∧ ( 2 · 𝐴 ) ∥ ( 𝐵 − - 𝐶 ) ) ∧ 𝐶 ∈ ( 0 ... ( 𝐴 − 1 ) ) ) → 𝐴 ∈ ℤ )
92 simp1 ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → 𝐴 ∈ ℕ )
93 42 92 44 sylancr ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → ( 2 · 𝐴 ) ∈ ℕ )
94 nnm1nn0 ⊢ ( ( 2 · 𝐴 ) ∈ ℕ → ( ( 2 · 𝐴 ) − 1 ) ∈ ℕ0 )
95 93 94 syl ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → ( ( 2 · 𝐴 ) − 1 ) ∈ ℕ0 )
96 95 nn0ge0d ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → 0 ≤ ( ( 2 · 𝐴 ) − 1 ) )
97 0m0e0 ⊢ ( 0 − 0 ) = 0
98 97 a1i ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → ( 0 − 0 ) = 0 )
99 1cnd ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → 1 ∈ ℂ )
100 36 36 99 addsubassd ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → ( ( 𝐴 + 𝐴 ) − 1 ) = ( 𝐴 + ( 𝐴 − 1 ) ) )
101 38 oveq1d ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → ( ( 2 · 𝐴 ) − 1 ) = ( ( 𝐴 + 𝐴 ) − 1 ) )
102 ax-1cn ⊢ 1 ∈ ℂ
103 subcl ⊢ ( ( 𝐴 ∈ ℂ ∧ 1 ∈ ℂ ) → ( 𝐴 − 1 ) ∈ ℂ )
104 36 102 103 sylancl ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → ( 𝐴 − 1 ) ∈ ℂ )
105 36 104 subnegd ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → ( 𝐴 − - ( 𝐴 − 1 ) ) = ( 𝐴 + ( 𝐴 − 1 ) ) )
106 100 101 105 3eqtr4rd ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → ( 𝐴 − - ( 𝐴 − 1 ) ) = ( ( 2 · 𝐴 ) − 1 ) )
107 96 98 106 3brtr4d ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → ( 0 − 0 ) ≤ ( 𝐴 − - ( 𝐴 − 1 ) ) )
108 107 ad2antrr ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) ∧ ( 2 · 𝐴 ) ∥ ( 𝐵 − - 𝐶 ) ) ∧ 𝐶 ∈ ( 0 ... ( 𝐴 − 1 ) ) ) → ( 0 − 0 ) ≤ ( 𝐴 − - ( 𝐴 − 1 ) ) )
109 fzmaxdif ⊢ ( ( ( 0 ∈ ℤ ∧ - 𝐶 ∈ ( - ( 𝐴 − 1 ) ... 0 ) ) ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ) ∧ ( 0 − 0 ) ≤ ( 𝐴 − - ( 𝐴 − 1 ) ) ) → ( abs ‘ ( - 𝐶 − 𝐵 ) ) ≤ ( 𝐴 − - ( 𝐴 − 1 ) ) )
110 77 90 91 54 108 109 syl221anc ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) ∧ ( 2 · 𝐴 ) ∥ ( 𝐵 − - 𝐶 ) ) ∧ 𝐶 ∈ ( 0 ... ( 𝐴 − 1 ) ) ) → ( abs ‘ ( - 𝐶 − 𝐵 ) ) ≤ ( 𝐴 − - ( 𝐴 − 1 ) ) )
111 76 110 eqbrtrd ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) ∧ ( 2 · 𝐴 ) ∥ ( 𝐵 − - 𝐶 ) ) ∧ 𝐶 ∈ ( 0 ... ( 𝐴 − 1 ) ) ) → ( abs ‘ ( 𝐵 − - 𝐶 ) ) ≤ ( 𝐴 − - ( 𝐴 − 1 ) ) )
112 27 ltm1d ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → ( ( 2 · 𝐴 ) − 1 ) < ( 2 · 𝐴 ) )
113 106 112 eqbrtrd ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → ( 𝐴 − - ( 𝐴 − 1 ) ) < ( 2 · 𝐴 ) )
114 113 ad2antrr ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) ∧ ( 2 · 𝐴 ) ∥ ( 𝐵 − - 𝐶 ) ) ∧ 𝐶 ∈ ( 0 ... ( 𝐴 − 1 ) ) ) → ( 𝐴 − - ( 𝐴 − 1 ) ) < ( 2 · 𝐴 ) )
115 63 69 70 111 114 lelttrd ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) ∧ ( 2 · 𝐴 ) ∥ ( 𝐵 − - 𝐶 ) ) ∧ 𝐶 ∈ ( 0 ... ( 𝐴 − 1 ) ) ) → ( abs ‘ ( 𝐵 − - 𝐶 ) ) < ( 2 · 𝐴 ) )
116 93 ad2antrr ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) ∧ ( 2 · 𝐴 ) ∥ ( 𝐵 − - 𝐶 ) ) ∧ 𝐶 ∈ ( 0 ... ( 𝐴 − 1 ) ) ) → ( 2 · 𝐴 ) ∈ ℕ )
117 simplr ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) ∧ ( 2 · 𝐴 ) ∥ ( 𝐵 − - 𝐶 ) ) ∧ 𝐶 ∈ ( 0 ... ( 𝐴 − 1 ) ) ) → ( 2 · 𝐴 ) ∥ ( 𝐵 − - 𝐶 ) )
118 congabseq ⊢ ( ( ( ( 2 · 𝐴 ) ∈ ℕ ∧ 𝐵 ∈ ℤ ∧ - 𝐶 ∈ ℤ ) ∧ ( 2 · 𝐴 ) ∥ ( 𝐵 − - 𝐶 ) ) → ( ( abs ‘ ( 𝐵 − - 𝐶 ) ) < ( 2 · 𝐴 ) ↔ 𝐵 = - 𝐶 ) )
119 116 71 74 117 118 syl31anc ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) ∧ ( 2 · 𝐴 ) ∥ ( 𝐵 − - 𝐶 ) ) ∧ 𝐶 ∈ ( 0 ... ( 𝐴 − 1 ) ) ) → ( ( abs ‘ ( 𝐵 − - 𝐶 ) ) < ( 2 · 𝐴 ) ↔ 𝐵 = - 𝐶 ) )
120 115 119 mpbid ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) ∧ ( 2 · 𝐴 ) ∥ ( 𝐵 − - 𝐶 ) ) ∧ 𝐶 ∈ ( 0 ... ( 𝐴 − 1 ) ) ) → 𝐵 = - 𝐶 )
121 56 120 breqtrd ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) ∧ ( 2 · 𝐴 ) ∥ ( 𝐵 − - 𝐶 ) ) ∧ 𝐶 ∈ ( 0 ... ( 𝐴 − 1 ) ) ) → 0 ≤ - 𝐶 )
122 elfzelz ⊢ ( 𝐶 ∈ ( 0 ... ( 𝐴 − 1 ) ) → 𝐶 ∈ ℤ )
123 122 zred ⊢ ( 𝐶 ∈ ( 0 ... ( 𝐴 − 1 ) ) → 𝐶 ∈ ℝ )
124 123 adantl ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) ∧ ( 2 · 𝐴 ) ∥ ( 𝐵 − - 𝐶 ) ) ∧ 𝐶 ∈ ( 0 ... ( 𝐴 − 1 ) ) ) → 𝐶 ∈ ℝ )
125 124 le0neg1d ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) ∧ ( 2 · 𝐴 ) ∥ ( 𝐵 − - 𝐶 ) ) ∧ 𝐶 ∈ ( 0 ... ( 𝐴 − 1 ) ) ) → ( 𝐶 ≤ 0 ↔ 0 ≤ - 𝐶 ) )
126 121 125 mpbird ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) ∧ ( 2 · 𝐴 ) ∥ ( 𝐵 − - 𝐶 ) ) ∧ 𝐶 ∈ ( 0 ... ( 𝐴 − 1 ) ) ) → 𝐶 ≤ 0 )
127 elfzle1 ⊢ ( 𝐶 ∈ ( 0 ... ( 𝐴 − 1 ) ) → 0 ≤ 𝐶 )
128 127 adantl ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) ∧ ( 2 · 𝐴 ) ∥ ( 𝐵 − - 𝐶 ) ) ∧ 𝐶 ∈ ( 0 ... ( 𝐴 − 1 ) ) ) → 0 ≤ 𝐶 )
129 letri3 ⊢ ( ( 𝐶 ∈ ℝ ∧ 0 ∈ ℝ ) → ( 𝐶 = 0 ↔ ( 𝐶 ≤ 0 ∧ 0 ≤ 𝐶 ) ) )
130 124 22 129 sylancl ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) ∧ ( 2 · 𝐴 ) ∥ ( 𝐵 − - 𝐶 ) ) ∧ 𝐶 ∈ ( 0 ... ( 𝐴 − 1 ) ) ) → ( 𝐶 = 0 ↔ ( 𝐶 ≤ 0 ∧ 0 ≤ 𝐶 ) ) )
131 126 128 130 mpbir2and ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) ∧ ( 2 · 𝐴 ) ∥ ( 𝐵 − - 𝐶 ) ) ∧ 𝐶 ∈ ( 0 ... ( 𝐴 − 1 ) ) ) → 𝐶 = 0 )
132 131 negeqd ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) ∧ ( 2 · 𝐴 ) ∥ ( 𝐵 − - 𝐶 ) ) ∧ 𝐶 ∈ ( 0 ... ( 𝐴 − 1 ) ) ) → - 𝐶 = - 0 )
133 132 88 eqtrd ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) ∧ ( 2 · 𝐴 ) ∥ ( 𝐵 − - 𝐶 ) ) ∧ 𝐶 ∈ ( 0 ... ( 𝐴 − 1 ) ) ) → - 𝐶 = 0 )
134 133 120 131 3eqtr4d ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) ∧ ( 2 · 𝐴 ) ∥ ( 𝐵 − - 𝐶 ) ) ∧ 𝐶 ∈ ( 0 ... ( 𝐴 − 1 ) ) ) → 𝐵 = 𝐶 )
135 oveq2 ⊢ ( 𝐶 = 𝐴 → ( 𝐵 − 𝐶 ) = ( 𝐵 − 𝐴 ) )
136 135 adantl ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) ∧ ( 2 · 𝐴 ) ∥ ( 𝐵 − - 𝐶 ) ) ∧ 𝐶 = 𝐴 ) → ( 𝐵 − 𝐶 ) = ( 𝐵 − 𝐴 ) )
137 136 fveq2d ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) ∧ ( 2 · 𝐴 ) ∥ ( 𝐵 − - 𝐶 ) ) ∧ 𝐶 = 𝐴 ) → ( abs ‘ ( 𝐵 − 𝐶 ) ) = ( abs ‘ ( 𝐵 − 𝐴 ) ) )
138 40 ad2antrr ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) ∧ ( 2 · 𝐴 ) ∥ ( 𝐵 − - 𝐶 ) ) ∧ 𝐶 = 𝐴 ) → ( abs ‘ ( 𝐵 − 𝐶 ) ) < ( 2 · 𝐴 ) )
139 137 138 eqbrtrrd ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) ∧ ( 2 · 𝐴 ) ∥ ( 𝐵 − - 𝐶 ) ) ∧ 𝐶 = 𝐴 ) → ( abs ‘ ( 𝐵 − 𝐴 ) ) < ( 2 · 𝐴 ) )
140 93 ad2antrr ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) ∧ ( 2 · 𝐴 ) ∥ ( 𝐵 − - 𝐶 ) ) ∧ 𝐶 = 𝐴 ) → ( 2 · 𝐴 ) ∈ ℕ )
141 7 ad2antrr ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) ∧ ( 2 · 𝐴 ) ∥ ( 𝐵 − - 𝐶 ) ) ∧ 𝐶 = 𝐴 ) → 𝐵 ∈ ℤ )
142 3 ad2antrr ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) ∧ ( 2 · 𝐴 ) ∥ ( 𝐵 − - 𝐶 ) ) ∧ 𝐶 = 𝐴 ) → 𝐴 ∈ ℤ )
143 simplr ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) ∧ ( 2 · 𝐴 ) ∥ ( 𝐵 − - 𝐶 ) ) ∧ 𝐶 = 𝐴 ) → ( 2 · 𝐴 ) ∥ ( 𝐵 − - 𝐶 ) )
144 7 zcnd ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → 𝐵 ∈ ℂ )
145 36 36 144 ppncand ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → ( ( 𝐴 + 𝐴 ) + ( 𝐵 − 𝐴 ) ) = ( 𝐴 + 𝐵 ) )
146 36 144 addcomd ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → ( 𝐴 + 𝐵 ) = ( 𝐵 + 𝐴 ) )
147 145 146 eqtrd ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → ( ( 𝐴 + 𝐴 ) + ( 𝐵 − 𝐴 ) ) = ( 𝐵 + 𝐴 ) )
148 147 ad2antrr ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) ∧ ( 2 · 𝐴 ) ∥ ( 𝐵 − - 𝐶 ) ) ∧ 𝐶 = 𝐴 ) → ( ( 𝐴 + 𝐴 ) + ( 𝐵 − 𝐴 ) ) = ( 𝐵 + 𝐴 ) )
149 oveq2 ⊢ ( 𝐶 = 𝐴 → ( 𝐵 + 𝐶 ) = ( 𝐵 + 𝐴 ) )
150 149 adantl ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) ∧ ( 2 · 𝐴 ) ∥ ( 𝐵 − - 𝐶 ) ) ∧ 𝐶 = 𝐴 ) → ( 𝐵 + 𝐶 ) = ( 𝐵 + 𝐴 ) )
151 148 150 eqtr4d ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) ∧ ( 2 · 𝐴 ) ∥ ( 𝐵 − - 𝐶 ) ) ∧ 𝐶 = 𝐴 ) → ( ( 𝐴 + 𝐴 ) + ( 𝐵 − 𝐴 ) ) = ( 𝐵 + 𝐶 ) )
152 38 oveq1d ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → ( ( 2 · 𝐴 ) + ( 𝐵 − 𝐴 ) ) = ( ( 𝐴 + 𝐴 ) + ( 𝐵 − 𝐴 ) ) )
153 152 ad2antrr ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) ∧ ( 2 · 𝐴 ) ∥ ( 𝐵 − - 𝐶 ) ) ∧ 𝐶 = 𝐴 ) → ( ( 2 · 𝐴 ) + ( 𝐵 − 𝐴 ) ) = ( ( 𝐴 + 𝐴 ) + ( 𝐵 − 𝐴 ) ) )
154 16 zcnd ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → 𝐶 ∈ ℂ )
155 144 154 subnegd ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → ( 𝐵 − - 𝐶 ) = ( 𝐵 + 𝐶 ) )
156 155 ad2antrr ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) ∧ ( 2 · 𝐴 ) ∥ ( 𝐵 − - 𝐶 ) ) ∧ 𝐶 = 𝐴 ) → ( 𝐵 − - 𝐶 ) = ( 𝐵 + 𝐶 ) )
157 151 153 156 3eqtr4d ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) ∧ ( 2 · 𝐴 ) ∥ ( 𝐵 − - 𝐶 ) ) ∧ 𝐶 = 𝐴 ) → ( ( 2 · 𝐴 ) + ( 𝐵 − 𝐴 ) ) = ( 𝐵 − - 𝐶 ) )
158 143 157 breqtrrd ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) ∧ ( 2 · 𝐴 ) ∥ ( 𝐵 − - 𝐶 ) ) ∧ 𝐶 = 𝐴 ) → ( 2 · 𝐴 ) ∥ ( ( 2 · 𝐴 ) + ( 𝐵 − 𝐴 ) ) )
159 5 ad2antrr ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) ∧ ( 2 · 𝐴 ) ∥ ( 𝐵 − - 𝐶 ) ) ∧ 𝐶 = 𝐴 ) → ( 2 · 𝐴 ) ∈ ℤ )
160 7 3 zsubcld ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → ( 𝐵 − 𝐴 ) ∈ ℤ )
161 160 ad2antrr ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) ∧ ( 2 · 𝐴 ) ∥ ( 𝐵 − - 𝐶 ) ) ∧ 𝐶 = 𝐴 ) → ( 𝐵 − 𝐴 ) ∈ ℤ )
162 dvdsadd ⊢ ( ( ( 2 · 𝐴 ) ∈ ℤ ∧ ( 𝐵 − 𝐴 ) ∈ ℤ ) → ( ( 2 · 𝐴 ) ∥ ( 𝐵 − 𝐴 ) ↔ ( 2 · 𝐴 ) ∥ ( ( 2 · 𝐴 ) + ( 𝐵 − 𝐴 ) ) ) )
163 159 161 162 syl2anc ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) ∧ ( 2 · 𝐴 ) ∥ ( 𝐵 − - 𝐶 ) ) ∧ 𝐶 = 𝐴 ) → ( ( 2 · 𝐴 ) ∥ ( 𝐵 − 𝐴 ) ↔ ( 2 · 𝐴 ) ∥ ( ( 2 · 𝐴 ) + ( 𝐵 − 𝐴 ) ) ) )
164 158 163 mpbird ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) ∧ ( 2 · 𝐴 ) ∥ ( 𝐵 − - 𝐶 ) ) ∧ 𝐶 = 𝐴 ) → ( 2 · 𝐴 ) ∥ ( 𝐵 − 𝐴 ) )
165 congabseq ⊢ ( ( ( ( 2 · 𝐴 ) ∈ ℕ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∈ ℤ ) ∧ ( 2 · 𝐴 ) ∥ ( 𝐵 − 𝐴 ) ) → ( ( abs ‘ ( 𝐵 − 𝐴 ) ) < ( 2 · 𝐴 ) ↔ 𝐵 = 𝐴 ) )
166 140 141 142 164 165 syl31anc ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) ∧ ( 2 · 𝐴 ) ∥ ( 𝐵 − - 𝐶 ) ) ∧ 𝐶 = 𝐴 ) → ( ( abs ‘ ( 𝐵 − 𝐴 ) ) < ( 2 · 𝐴 ) ↔ 𝐵 = 𝐴 ) )
167 139 166 mpbid ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) ∧ ( 2 · 𝐴 ) ∥ ( 𝐵 − - 𝐶 ) ) ∧ 𝐶 = 𝐴 ) → 𝐵 = 𝐴 )
168 simpr ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) ∧ ( 2 · 𝐴 ) ∥ ( 𝐵 − - 𝐶 ) ) ∧ 𝐶 = 𝐴 ) → 𝐶 = 𝐴 )
169 167 168 eqtr4d ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) ∧ ( 2 · 𝐴 ) ∥ ( 𝐵 − - 𝐶 ) ) ∧ 𝐶 = 𝐴 ) → 𝐵 = 𝐶 )
170 nnnn0 ⊢ ( 𝐴 ∈ ℕ → 𝐴 ∈ ℕ0 )
171 170 3ad2ant1 ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → 𝐴 ∈ ℕ0 )
172 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
173 171 172 eleqtrdi ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → 𝐴 ∈ ( ℤ≥ ‘ 0 ) )
174 fzm1 ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 0 ) → ( 𝐶 ∈ ( 0 ... 𝐴 ) ↔ ( 𝐶 ∈ ( 0 ... ( 𝐴 − 1 ) ) ∨ 𝐶 = 𝐴 ) ) )
175 174 biimpa ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 0 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → ( 𝐶 ∈ ( 0 ... ( 𝐴 − 1 ) ) ∨ 𝐶 = 𝐴 ) )
176 173 29 175 syl2anc ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → ( 𝐶 ∈ ( 0 ... ( 𝐴 − 1 ) ) ∨ 𝐶 = 𝐴 ) )
177 176 adantr ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) ∧ ( 2 · 𝐴 ) ∥ ( 𝐵 − - 𝐶 ) ) → ( 𝐶 ∈ ( 0 ... ( 𝐴 − 1 ) ) ∨ 𝐶 = 𝐴 ) )
178 134 169 177 mpjaodan ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) ∧ ( 2 · 𝐴 ) ∥ ( 𝐵 − - 𝐶 ) ) → 𝐵 = 𝐶 )
179 53 178 jaodan ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) ∧ ( ( 2 · 𝐴 ) ∥ ( 𝐵 − 𝐶 ) ∨ ( 2 · 𝐴 ) ∥ ( 𝐵 − - 𝐶 ) ) ) → 𝐵 = 𝐶 )
180 14 179 impbida ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐴 ) ∧ 𝐶 ∈ ( 0 ... 𝐴 ) ) → ( 𝐵 = 𝐶 ↔ ( ( 2 · 𝐴 ) ∥ ( 𝐵 − 𝐶 ) ∨ ( 2 · 𝐴 ) ∥ ( 𝐵 − - 𝐶 ) ) ) )