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 · 𝐴 ) ∥ ( 𝑎 − - 𝑁 ) ) )