Metamath Proof Explorer

Theorem acongrep

Description: Every integer is alternating-congruent to some number in the first half of the fundamental domain. (Contributed by Stefan O'Rear, 2-Oct-2014)

Ref Expression
Assertion acongrep 
|- ( ( A e. NN /\ N e. ZZ ) -> E. a e. ( 0 ... A ) ( ( 2 x. A ) || ( a - N ) \/ ( 2 x. A ) || ( a - -u N ) ) )

Proof

Step Hyp Ref Expression
1 2nn 
 |-  2 e. NN
2 simpl 
 |-  ( ( A e. NN /\ N e. ZZ ) -> A e. NN )
3 nnmulcl 
 |-  ( ( 2 e. NN /\ A e. NN ) -> ( 2 x. A ) e. NN )
4 1 2 3 sylancr 
 |-  ( ( A e. NN /\ N e. ZZ ) -> ( 2 x. A ) e. NN )
5 simpr 
 |-  ( ( A e. NN /\ N e. ZZ ) -> N e. ZZ )
6 congrep 
 |-  ( ( ( 2 x. A ) e. NN /\ N e. ZZ ) -> E. b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) ( 2 x. A ) || ( b - N ) )
7 4 5 6 syl2anc 
 |-  ( ( A e. NN /\ N e. ZZ ) -> E. b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) ( 2 x. A ) || ( b - N ) )
8 elfzelz 
 |-  ( b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) -> b e. ZZ )
9 8 zred 
 |-  ( b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) -> b e. RR )
10 9 ad2antrl 
 |-  ( ( ( A e. NN /\ N e. ZZ ) /\ ( b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) /\ ( 2 x. A ) || ( b - N ) ) ) -> b e. RR )
11 nnre 
 |-  ( A e. NN -> A e. RR )
12 11 ad2antrr 
 |-  ( ( ( A e. NN /\ N e. ZZ ) /\ ( b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) /\ ( 2 x. A ) || ( b - N ) ) ) -> A e. RR )
13 elfzle1 
 |-  ( b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) -> 0 <_ b )
14 13 ad2antrl 
 |-  ( ( ( A e. NN /\ N e. ZZ ) /\ ( b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) /\ ( 2 x. A ) || ( b - N ) ) ) -> 0 <_ b )
15 14 anim1i 
 |-  ( ( ( ( A e. NN /\ N e. ZZ ) /\ ( b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) /\ ( 2 x. A ) || ( b - N ) ) ) /\ b <_ A ) -> ( 0 <_ b /\ b <_ A ) )
16 8 ad2antrl 
 |-  ( ( ( A e. NN /\ N e. ZZ ) /\ ( b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) /\ ( 2 x. A ) || ( b - N ) ) ) -> b e. ZZ )
17 0zd 
 |-  ( ( ( A e. NN /\ N e. ZZ ) /\ ( b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) /\ ( 2 x. A ) || ( b - N ) ) ) -> 0 e. ZZ )
18 nnz 
 |-  ( A e. NN -> A e. ZZ )
19 18 ad2antrr 
 |-  ( ( ( A e. NN /\ N e. ZZ ) /\ ( b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) /\ ( 2 x. A ) || ( b - N ) ) ) -> A e. ZZ )
20 elfz 
 |-  ( ( b e. ZZ /\ 0 e. ZZ /\ A e. ZZ ) -> ( b e. ( 0 ... A ) <-> ( 0 <_ b /\ b <_ A ) ) )
21 16 17 19 20 syl3anc 
 |-  ( ( ( A e. NN /\ N e. ZZ ) /\ ( b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) /\ ( 2 x. A ) || ( b - N ) ) ) -> ( b e. ( 0 ... A ) <-> ( 0 <_ b /\ b <_ A ) ) )
22 21 adantr 
 |-  ( ( ( ( A e. NN /\ N e. ZZ ) /\ ( b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) /\ ( 2 x. A ) || ( b - N ) ) ) /\ b <_ A ) -> ( b e. ( 0 ... A ) <-> ( 0 <_ b /\ b <_ A ) ) )
23 15 22 mpbird 
 |-  ( ( ( ( A e. NN /\ N e. ZZ ) /\ ( b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) /\ ( 2 x. A ) || ( b - N ) ) ) /\ b <_ A ) -> b e. ( 0 ... A ) )
24 simplrr 
 |-  ( ( ( ( A e. NN /\ N e. ZZ ) /\ ( b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) /\ ( 2 x. A ) || ( b - N ) ) ) /\ b <_ A ) -> ( 2 x. A ) || ( b - N ) )
25 24 orcd 
 |-  ( ( ( ( A e. NN /\ N e. ZZ ) /\ ( b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) /\ ( 2 x. A ) || ( b - N ) ) ) /\ b <_ A ) -> ( ( 2 x. A ) || ( b - N ) \/ ( 2 x. A ) || ( b - -u N ) ) )
26 id 
 |-  ( a = b -> a = b )
27 eqidd 
 |-  ( a = b -> N = N )
28 26 27 acongeq12d 
 |-  ( a = b -> ( ( ( 2 x. A ) || ( a - N ) \/ ( 2 x. A ) || ( a - -u N ) ) <-> ( ( 2 x. A ) || ( b - N ) \/ ( 2 x. A ) || ( b - -u N ) ) ) )
29 28 rspcev 
 |-  ( ( b e. ( 0 ... A ) /\ ( ( 2 x. A ) || ( b - N ) \/ ( 2 x. A ) || ( b - -u N ) ) ) -> E. a e. ( 0 ... A ) ( ( 2 x. A ) || ( a - N ) \/ ( 2 x. A ) || ( a - -u N ) ) )
30 23 25 29 syl2anc 
 |-  ( ( ( ( A e. NN /\ N e. ZZ ) /\ ( b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) /\ ( 2 x. A ) || ( b - N ) ) ) /\ b <_ A ) -> E. a e. ( 0 ... A ) ( ( 2 x. A ) || ( a - N ) \/ ( 2 x. A ) || ( a - -u N ) ) )
31 simplll 
 |-  ( ( ( ( A e. NN /\ N e. ZZ ) /\ ( b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) /\ ( 2 x. A ) || ( b - N ) ) ) /\ A <_ b ) -> A e. NN )
32 simplrl 
 |-  ( ( ( ( A e. NN /\ N e. ZZ ) /\ ( b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) /\ ( 2 x. A ) || ( b - N ) ) ) /\ A <_ b ) -> b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) )
33 simpr 
 |-  ( ( ( ( A e. NN /\ N e. ZZ ) /\ ( b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) /\ ( 2 x. A ) || ( b - N ) ) ) /\ A <_ b ) -> A <_ b )
34 9 3ad2ant2 
 |-  ( ( A e. NN /\ b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) /\ A <_ b ) -> b e. RR )
35 2re 
 |-  2 e. RR
36 remulcl 
 |-  ( ( 2 e. RR /\ A e. RR ) -> ( 2 x. A ) e. RR )
37 35 11 36 sylancr 
 |-  ( A e. NN -> ( 2 x. A ) e. RR )
38 37 3ad2ant1 
 |-  ( ( A e. NN /\ b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) /\ A <_ b ) -> ( 2 x. A ) e. RR )
39 0zd 
 |-  ( ( A e. NN /\ b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) /\ A <_ b ) -> 0 e. ZZ )
40 2z 
 |-  2 e. ZZ
41 zmulcl 
 |-  ( ( 2 e. ZZ /\ A e. ZZ ) -> ( 2 x. A ) e. ZZ )
42 40 18 41 sylancr 
 |-  ( A e. NN -> ( 2 x. A ) e. ZZ )
43 42 3ad2ant1 
 |-  ( ( A e. NN /\ b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) /\ A <_ b ) -> ( 2 x. A ) e. ZZ )
44 simp2 
 |-  ( ( A e. NN /\ b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) /\ A <_ b ) -> b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) )
45 elfzm11 
 |-  ( ( 0 e. ZZ /\ ( 2 x. A ) e. ZZ ) -> ( b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) <-> ( b e. ZZ /\ 0 <_ b /\ b < ( 2 x. A ) ) ) )
46 45 biimpa 
 |-  ( ( ( 0 e. ZZ /\ ( 2 x. A ) e. ZZ ) /\ b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) ) -> ( b e. ZZ /\ 0 <_ b /\ b < ( 2 x. A ) ) )
47 39 43 44 46 syl21anc 
 |-  ( ( A e. NN /\ b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) /\ A <_ b ) -> ( b e. ZZ /\ 0 <_ b /\ b < ( 2 x. A ) ) )
48 47 simp3d 
 |-  ( ( A e. NN /\ b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) /\ A <_ b ) -> b < ( 2 x. A ) )
49 34 38 48 ltled 
 |-  ( ( A e. NN /\ b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) /\ A <_ b ) -> b <_ ( 2 x. A ) )
50 38 34 subge0d 
 |-  ( ( A e. NN /\ b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) /\ A <_ b ) -> ( 0 <_ ( ( 2 x. A ) - b ) <-> b <_ ( 2 x. A ) ) )
51 49 50 mpbird 
 |-  ( ( A e. NN /\ b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) /\ A <_ b ) -> 0 <_ ( ( 2 x. A ) - b ) )
52 11 3ad2ant1 
 |-  ( ( A e. NN /\ b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) /\ A <_ b ) -> A e. RR )
53 nncn 
 |-  ( A e. NN -> A e. CC )
54 2times 
 |-  ( A e. CC -> ( 2 x. A ) = ( A + A ) )
55 54 oveq1d 
 |-  ( A e. CC -> ( ( 2 x. A ) - A ) = ( ( A + A ) - A ) )
56 pncan2 
 |-  ( ( A e. CC /\ A e. CC ) -> ( ( A + A ) - A ) = A )
57 56 anidms 
 |-  ( A e. CC -> ( ( A + A ) - A ) = A )
58 55 57 eqtrd 
 |-  ( A e. CC -> ( ( 2 x. A ) - A ) = A )
59 53 58 syl 
 |-  ( A e. NN -> ( ( 2 x. A ) - A ) = A )
60 59 3ad2ant1 
 |-  ( ( A e. NN /\ b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) /\ A <_ b ) -> ( ( 2 x. A ) - A ) = A )
61 simp3 
 |-  ( ( A e. NN /\ b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) /\ A <_ b ) -> A <_ b )
62 60 61 eqbrtrd 
 |-  ( ( A e. NN /\ b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) /\ A <_ b ) -> ( ( 2 x. A ) - A ) <_ b )
63 38 52 34 62 subled 
 |-  ( ( A e. NN /\ b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) /\ A <_ b ) -> ( ( 2 x. A ) - b ) <_ A )
64 51 63 jca 
 |-  ( ( A e. NN /\ b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) /\ A <_ b ) -> ( 0 <_ ( ( 2 x. A ) - b ) /\ ( ( 2 x. A ) - b ) <_ A ) )
65 31 32 33 64 syl3anc 
 |-  ( ( ( ( A e. NN /\ N e. ZZ ) /\ ( b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) /\ ( 2 x. A ) || ( b - N ) ) ) /\ A <_ b ) -> ( 0 <_ ( ( 2 x. A ) - b ) /\ ( ( 2 x. A ) - b ) <_ A ) )
66 40 19 41 sylancr 
 |-  ( ( ( A e. NN /\ N e. ZZ ) /\ ( b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) /\ ( 2 x. A ) || ( b - N ) ) ) -> ( 2 x. A ) e. ZZ )
67 66 16 zsubcld 
 |-  ( ( ( A e. NN /\ N e. ZZ ) /\ ( b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) /\ ( 2 x. A ) || ( b - N ) ) ) -> ( ( 2 x. A ) - b ) e. ZZ )
68 elfz 
 |-  ( ( ( ( 2 x. A ) - b ) e. ZZ /\ 0 e. ZZ /\ A e. ZZ ) -> ( ( ( 2 x. A ) - b ) e. ( 0 ... A ) <-> ( 0 <_ ( ( 2 x. A ) - b ) /\ ( ( 2 x. A ) - b ) <_ A ) ) )
69 67 17 19 68 syl3anc 
 |-  ( ( ( A e. NN /\ N e. ZZ ) /\ ( b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) /\ ( 2 x. A ) || ( b - N ) ) ) -> ( ( ( 2 x. A ) - b ) e. ( 0 ... A ) <-> ( 0 <_ ( ( 2 x. A ) - b ) /\ ( ( 2 x. A ) - b ) <_ A ) ) )
70 69 adantr 
 |-  ( ( ( ( A e. NN /\ N e. ZZ ) /\ ( b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) /\ ( 2 x. A ) || ( b - N ) ) ) /\ A <_ b ) -> ( ( ( 2 x. A ) - b ) e. ( 0 ... A ) <-> ( 0 <_ ( ( 2 x. A ) - b ) /\ ( ( 2 x. A ) - b ) <_ A ) ) )
71 65 70 mpbird 
 |-  ( ( ( ( A e. NN /\ N e. ZZ ) /\ ( b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) /\ ( 2 x. A ) || ( b - N ) ) ) /\ A <_ b ) -> ( ( 2 x. A ) - b ) e. ( 0 ... A ) )
72 simplr 
 |-  ( ( ( A e. NN /\ N e. ZZ ) /\ ( b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) /\ ( 2 x. A ) || ( b - N ) ) ) -> N e. ZZ )
73 simprr 
 |-  ( ( ( A e. NN /\ N e. ZZ ) /\ ( b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) /\ ( 2 x. A ) || ( b - N ) ) ) -> ( 2 x. A ) || ( b - N ) )
74 congsym 
 |-  ( ( ( ( 2 x. A ) e. ZZ /\ b e. ZZ ) /\ ( N e. ZZ /\ ( 2 x. A ) || ( b - N ) ) ) -> ( 2 x. A ) || ( N - b ) )
75 66 16 72 73 74 syl22anc 
 |-  ( ( ( A e. NN /\ N e. ZZ ) /\ ( b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) /\ ( 2 x. A ) || ( b - N ) ) ) -> ( 2 x. A ) || ( N - b ) )
76 72 16 zsubcld 
 |-  ( ( ( A e. NN /\ N e. ZZ ) /\ ( b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) /\ ( 2 x. A ) || ( b - N ) ) ) -> ( N - b ) e. ZZ )
77 dvdsadd 
 |-  ( ( ( 2 x. A ) e. ZZ /\ ( N - b ) e. ZZ ) -> ( ( 2 x. A ) || ( N - b ) <-> ( 2 x. A ) || ( ( 2 x. A ) + ( N - b ) ) ) )
78 66 76 77 syl2anc 
 |-  ( ( ( A e. NN /\ N e. ZZ ) /\ ( b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) /\ ( 2 x. A ) || ( b - N ) ) ) -> ( ( 2 x. A ) || ( N - b ) <-> ( 2 x. A ) || ( ( 2 x. A ) + ( N - b ) ) ) )
79 75 78 mpbid 
 |-  ( ( ( A e. NN /\ N e. ZZ ) /\ ( b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) /\ ( 2 x. A ) || ( b - N ) ) ) -> ( 2 x. A ) || ( ( 2 x. A ) + ( N - b ) ) )
80 67 zcnd 
 |-  ( ( ( A e. NN /\ N e. ZZ ) /\ ( b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) /\ ( 2 x. A ) || ( b - N ) ) ) -> ( ( 2 x. A ) - b ) e. CC )
81 zcn 
 |-  ( N e. ZZ -> N e. CC )
82 81 ad2antlr 
 |-  ( ( ( A e. NN /\ N e. ZZ ) /\ ( b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) /\ ( 2 x. A ) || ( b - N ) ) ) -> N e. CC )
83 80 82 subnegd 
 |-  ( ( ( A e. NN /\ N e. ZZ ) /\ ( b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) /\ ( 2 x. A ) || ( b - N ) ) ) -> ( ( ( 2 x. A ) - b ) - -u N ) = ( ( ( 2 x. A ) - b ) + N ) )
84 66 zcnd 
 |-  ( ( ( A e. NN /\ N e. ZZ ) /\ ( b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) /\ ( 2 x. A ) || ( b - N ) ) ) -> ( 2 x. A ) e. CC )
85 10 recnd 
 |-  ( ( ( A e. NN /\ N e. ZZ ) /\ ( b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) /\ ( 2 x. A ) || ( b - N ) ) ) -> b e. CC )
86 84 85 82 subadd23d 
 |-  ( ( ( A e. NN /\ N e. ZZ ) /\ ( b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) /\ ( 2 x. A ) || ( b - N ) ) ) -> ( ( ( 2 x. A ) - b ) + N ) = ( ( 2 x. A ) + ( N - b ) ) )
87 83 86 eqtrd 
 |-  ( ( ( A e. NN /\ N e. ZZ ) /\ ( b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) /\ ( 2 x. A ) || ( b - N ) ) ) -> ( ( ( 2 x. A ) - b ) - -u N ) = ( ( 2 x. A ) + ( N - b ) ) )
88 79 87 breqtrrd 
 |-  ( ( ( A e. NN /\ N e. ZZ ) /\ ( b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) /\ ( 2 x. A ) || ( b - N ) ) ) -> ( 2 x. A ) || ( ( ( 2 x. A ) - b ) - -u N ) )
89 88 adantr 
 |-  ( ( ( ( A e. NN /\ N e. ZZ ) /\ ( b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) /\ ( 2 x. A ) || ( b - N ) ) ) /\ A <_ b ) -> ( 2 x. A ) || ( ( ( 2 x. A ) - b ) - -u N ) )
90 89 olcd 
 |-  ( ( ( ( A e. NN /\ N e. ZZ ) /\ ( b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) /\ ( 2 x. A ) || ( b - N ) ) ) /\ A <_ b ) -> ( ( 2 x. A ) || ( ( ( 2 x. A ) - b ) - N ) \/ ( 2 x. A ) || ( ( ( 2 x. A ) - b ) - -u N ) ) )
91 id 
 |-  ( a = ( ( 2 x. A ) - b ) -> a = ( ( 2 x. A ) - b ) )
92 eqidd 
 |-  ( a = ( ( 2 x. A ) - b ) -> N = N )
93 91 92 acongeq12d 
 |-  ( a = ( ( 2 x. A ) - b ) -> ( ( ( 2 x. A ) || ( a - N ) \/ ( 2 x. A ) || ( a - -u N ) ) <-> ( ( 2 x. A ) || ( ( ( 2 x. A ) - b ) - N ) \/ ( 2 x. A ) || ( ( ( 2 x. A ) - b ) - -u N ) ) ) )
94 93 rspcev 
 |-  ( ( ( ( 2 x. A ) - b ) e. ( 0 ... A ) /\ ( ( 2 x. A ) || ( ( ( 2 x. A ) - b ) - N ) \/ ( 2 x. A ) || ( ( ( 2 x. A ) - b ) - -u N ) ) ) -> E. a e. ( 0 ... A ) ( ( 2 x. A ) || ( a - N ) \/ ( 2 x. A ) || ( a - -u N ) ) )
95 71 90 94 syl2anc 
 |-  ( ( ( ( A e. NN /\ N e. ZZ ) /\ ( b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) /\ ( 2 x. A ) || ( b - N ) ) ) /\ A <_ b ) -> E. a e. ( 0 ... A ) ( ( 2 x. A ) || ( a - N ) \/ ( 2 x. A ) || ( a - -u N ) ) )
96 10 12 30 95 lecasei 
 |-  ( ( ( A e. NN /\ N e. ZZ ) /\ ( b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) /\ ( 2 x. A ) || ( b - N ) ) ) -> E. a e. ( 0 ... A ) ( ( 2 x. A ) || ( a - N ) \/ ( 2 x. A ) || ( a - -u N ) ) )
97 7 96 rexlimddv 
 |-  ( ( A e. NN /\ N e. ZZ ) -> E. a e. ( 0 ... A ) ( ( 2 x. A ) || ( a - N ) \/ ( 2 x. A ) || ( a - -u N ) ) )