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 \in ℕ \land N \in ℤ) \to \exists a \in (0 \dots A) (2 A ∥ (a - N) \lor 2 A ∥ (a - -N))$

Proof

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

Metamath Proof Explorer

Theorem acongrep

Proof