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 ( ( 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℤ ) → ∃ 𝑎 ∈ ( 0 ... 𝐴 ) ( ( 2 · 𝐴 ) ∥ ( 𝑎 − 𝑁 ) ∨ ( 2 · 𝐴 ) ∥ ( 𝑎 − - 𝑁 ) ) )

Proof

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