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 ${⊢}\left({A}\in ℕ\wedge {B}\in \left(0\dots {A}\right)\wedge {C}\in \left(0\dots {A}\right)\right)\to \left({B}={C}↔\left(2{A}\parallel \left({B}-{C}\right)\vee 2{A}\parallel \left({B}-\left(-{C}\right)\right)\right)\right)$

Proof

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