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 
|- ( ( A e. NN /\ B e. ( 0 ... A ) /\ C e. ( 0 ... A ) ) -> ( B = C <-> ( ( 2 x. A ) || ( B - C ) \/ ( 2 x. A ) || ( B - -u C ) ) ) )

Proof

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