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∈ℕ∧N∈ℤ→∃a∈0…A2⁢A∥a−N∨2⁢A∥a−- N

Proof

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