# 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 ${⊢}\left({A}\in ℕ\wedge {N}\in ℤ\right)\to \exists {a}\in \left(0\dots {A}\right)\phantom{\rule{.4em}{0ex}}\left(2{A}\parallel \left({a}-{N}\right)\vee 2{A}\parallel \left({a}--{N}\right)\right)$

### Proof

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