acongeq

Description: Two numbers in the fundamental domain are alternating-congruent iff they are equal. TODO: could be used to shorten jm2.26 . (Contributed by Stefan O'Rear, 4-Oct-2014)

		Ref	Expression
	Assertion	acongeq	$⊢ (A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \to (B = C \leftrightarrow (2 A ∥ (B - C) \lor 2 A ∥ (B - (- C))))$

Proof

Step	Hyp	Ref	Expression
1		2z	$⊢ 2 \in ℤ$
2		nnz	$⊢ A \in ℕ \to A \in ℤ$
3	2	3ad2ant1	$⊢ (A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \to A \in ℤ$
4		zmulcl	$⊢ (2 \in ℤ \land A \in ℤ) \to 2 A \in ℤ$
5	1 3 4	sylancr	$⊢ (A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \to 2 A \in ℤ$
6		elfzelz	$⊢ B \in (0 \dots A) \to B \in ℤ$
7	6	3ad2ant2	$⊢ (A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \to B \in ℤ$
8		congid	$⊢ (2 A \in ℤ \land B \in ℤ) \to 2 A ∥ (B - B)$
9	5 7 8	syl2anc	$⊢ (A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \to 2 A ∥ (B - B)$
10	9	adantr	$⊢ ((A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \land B = C) \to 2 A ∥ (B - B)$
11		oveq2	$⊢ B = C \to B - B = B - C$
12	11	adantl	$⊢ ((A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \land B = C) \to B - B = B - C$
13	10 12	breqtrd	$⊢ ((A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \land B = C) \to 2 A ∥ (B - C)$
14	13	orcd	$⊢ ((A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \land B = C) \to (2 A ∥ (B - C) \lor 2 A ∥ (B - (- C)))$
15		elfzelz	$⊢ C \in (0 \dots A) \to C \in ℤ$
16	15	3ad2ant3	$⊢ (A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \to C \in ℤ$
17	7 16	zsubcld	$⊢ (A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \to B - C \in ℤ$
18	17	zcnd	$⊢ (A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \to B - C \in ℂ$
19	18	abscld	$⊢ (A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \to \|B - C\| \in ℝ$
20		nnre	$⊢ A \in ℕ \to A \in ℝ$
21	20	3ad2ant1	$⊢ (A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \to A \in ℝ$
22		0re	$⊢ 0 \in ℝ$
23		resubcl	$⊢ (A \in ℝ \land 0 \in ℝ) \to A - 0 \in ℝ$
24	21 22 23	sylancl	$⊢ (A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \to A - 0 \in ℝ$
25		2re	$⊢ 2 \in ℝ$
26		remulcl	$⊢ (2 \in ℝ \land A \in ℝ) \to 2 A \in ℝ$
27	25 21 26	sylancr	$⊢ (A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \to 2 A \in ℝ$
28		simp2	$⊢ (A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \to B \in (0 \dots A)$
29		simp3	$⊢ (A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \to C \in (0 \dots A)$
30	24	leidd	$⊢ (A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \to A - 0 \leq A - 0$
31		fzmaxdif	$⊢ ((A \in ℤ \land B \in (0 \dots A)) \land (A \in ℤ \land C \in (0 \dots A)) \land A - 0 \leq A - 0) \to \|B - C\| \leq A - 0$
32	3 28 3 29 30 31	syl221anc	$⊢ (A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \to \|B - C\| \leq A - 0$
33		nnrp	$⊢ A \in ℕ \to A \in ℝ^{+}$
34	33	3ad2ant1	$⊢ (A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \to A \in ℝ^{+}$
35	21 34	ltaddrpd	$⊢ (A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \to A < A + A$
36	21	recnd	$⊢ (A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \to A \in ℂ$
37	36	subid1d	$⊢ (A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \to A - 0 = A$
38	36	2timesd	$⊢ (A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \to 2 A = A + A$
39	35 37 38	3brtr4d	$⊢ (A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \to A - 0 < 2 A$
40	19 24 27 32 39	lelttrd	$⊢ (A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \to \|B - C\| < 2 A$
41	40	adantr	$⊢ ((A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \land 2 A ∥ (B - C)) \to \|B - C\| < 2 A$
42		2nn	$⊢ 2 \in ℕ$
43		simpl1	$⊢ ((A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \land 2 A ∥ (B - C)) \to A \in ℕ$
44		nnmulcl	$⊢ (2 \in ℕ \land A \in ℕ) \to 2 A \in ℕ$
45	42 43 44	sylancr	$⊢ ((A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \land 2 A ∥ (B - C)) \to 2 A \in ℕ$
46		simpl2	$⊢ ((A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \land 2 A ∥ (B - C)) \to B \in (0 \dots A)$
47	46 6	syl	$⊢ ((A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \land 2 A ∥ (B - C)) \to B \in ℤ$
48		simpl3	$⊢ ((A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \land 2 A ∥ (B - C)) \to C \in (0 \dots A)$
49	48 15	syl	$⊢ ((A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \land 2 A ∥ (B - C)) \to C \in ℤ$
50		simpr	$⊢ ((A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \land 2 A ∥ (B - C)) \to 2 A ∥ (B - C)$
51		congabseq	$⊢ ((2 A \in ℕ \land B \in ℤ \land C \in ℤ) \land 2 A ∥ (B - C)) \to (\|B - C\| < 2 A \leftrightarrow B = C)$
52	45 47 49 50 51	syl31anc	$⊢ ((A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \land 2 A ∥ (B - C)) \to (\|B - C\| < 2 A \leftrightarrow B = C)$
53	41 52	mpbid	$⊢ ((A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \land 2 A ∥ (B - C)) \to B = C$
54		simpll2	$⊢ (((A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \land 2 A ∥ (B - (- C))) \land C \in (0 \dots A - 1)) \to B \in (0 \dots A)$
55		elfzle1	$⊢ B \in (0 \dots A) \to 0 \leq B$
56	54 55	syl	$⊢ (((A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \land 2 A ∥ (B - (- C))) \land C \in (0 \dots A - 1)) \to 0 \leq B$
57	7	zred	$⊢ (A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \to B \in ℝ$
58	16	zred	$⊢ (A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \to C \in ℝ$
59	58	renegcld	$⊢ (A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \to - C \in ℝ$
60	57 59	resubcld	$⊢ (A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \to B - (- C) \in ℝ$
61	60	recnd	$⊢ (A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \to B - (- C) \in ℂ$
62	61	abscld	$⊢ (A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \to \|B - (- C)\| \in ℝ$
63	62	ad2antrr	$⊢ (((A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \land 2 A ∥ (B - (- C))) \land C \in (0 \dots A - 1)) \to \|B - (- C)\| \in ℝ$
64		1re	$⊢ 1 \in ℝ$
65		resubcl	$⊢ (A \in ℝ \land 1 \in ℝ) \to A - 1 \in ℝ$
66	21 64 65	sylancl	$⊢ (A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \to A - 1 \in ℝ$
67	66	renegcld	$⊢ (A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \to - (A - 1) \in ℝ$
68	21 67	resubcld	$⊢ (A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \to A - (- (A - 1)) \in ℝ$
69	68	ad2antrr	$⊢ (((A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \land 2 A ∥ (B - (- C))) \land C \in (0 \dots A - 1)) \to A - (- (A - 1)) \in ℝ$
70	27	ad2antrr	$⊢ (((A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \land 2 A ∥ (B - (- C))) \land C \in (0 \dots A - 1)) \to 2 A \in ℝ$
71	7	ad2antrr	$⊢ (((A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \land 2 A ∥ (B - (- C))) \land C \in (0 \dots A - 1)) \to B \in ℤ$
72	71	zcnd	$⊢ (((A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \land 2 A ∥ (B - (- C))) \land C \in (0 \dots A - 1)) \to B \in ℂ$
73	16	znegcld	$⊢ (A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \to - C \in ℤ$
74	73	ad2antrr	$⊢ (((A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \land 2 A ∥ (B - (- C))) \land C \in (0 \dots A - 1)) \to - C \in ℤ$
75	74	zcnd	$⊢ (((A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \land 2 A ∥ (B - (- C))) \land C \in (0 \dots A - 1)) \to - C \in ℂ$
76	72 75	abssubd	$⊢ (((A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \land 2 A ∥ (B - (- C))) \land C \in (0 \dots A - 1)) \to \|B - (- C)\| = \|- C - B\|$
77		0zd	$⊢ (((A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \land 2 A ∥ (B - (- C))) \land C \in (0 \dots A - 1)) \to 0 \in ℤ$
78		simpr	$⊢ (((A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \land 2 A ∥ (B - (- C))) \land C \in (0 \dots A - 1)) \to C \in (0 \dots A - 1)$
79		0zd	$⊢ (A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \to 0 \in ℤ$
80		1z	$⊢ 1 \in ℤ$
81		zsubcl	$⊢ (A \in ℤ \land 1 \in ℤ) \to A - 1 \in ℤ$
82	3 80 81	sylancl	$⊢ (A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \to A - 1 \in ℤ$
83		fzneg	$⊢ (C \in ℤ \land 0 \in ℤ \land A - 1 \in ℤ) \to (C \in (0 \dots A - 1) \leftrightarrow - C \in (- (A - 1) \dots - 0))$
84	16 79 82 83	syl3anc	$⊢ (A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \to (C \in (0 \dots A - 1) \leftrightarrow - C \in (- (A - 1) \dots - 0))$
85	84	ad2antrr	$⊢ (((A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \land 2 A ∥ (B - (- C))) \land C \in (0 \dots A - 1)) \to (C \in (0 \dots A - 1) \leftrightarrow - C \in (- (A - 1) \dots - 0))$
86	78 85	mpbid	$⊢ (((A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \land 2 A ∥ (B - (- C))) \land C \in (0 \dots A - 1)) \to - C \in (- (A - 1) \dots - 0)$
87		neg0	$⊢ - 0 = 0$
88	87	a1i	$⊢ (((A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \land 2 A ∥ (B - (- C))) \land C \in (0 \dots A - 1)) \to - 0 = 0$
89	88	oveq2d	$⊢ (((A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \land 2 A ∥ (B - (- C))) \land C \in (0 \dots A - 1)) \to (- (A - 1) \dots - 0) = (- (A - 1) \dots 0)$
90	86 89	eleqtrd	$⊢ (((A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \land 2 A ∥ (B - (- C))) \land C \in (0 \dots A - 1)) \to - C \in (- (A - 1) \dots 0)$
91	3	ad2antrr	$⊢ (((A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \land 2 A ∥ (B - (- C))) \land C \in (0 \dots A - 1)) \to A \in ℤ$
92		simp1	$⊢ (A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \to A \in ℕ$
93	42 92 44	sylancr	$⊢ (A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \to 2 A \in ℕ$
94		nnm1nn0	$⊢ 2 A \in ℕ \to 2 A - 1 \in ℕ_{0}$
95	93 94	syl	$⊢ (A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \to 2 A - 1 \in ℕ_{0}$
96	95	nn0ge0d	$⊢ (A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \to 0 \leq 2 A - 1$
97		0m0e0	$⊢ 0 - 0 = 0$
98	97	a1i	$⊢ (A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \to 0 - 0 = 0$
99		1cnd	$⊢ (A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \to 1 \in ℂ$
100	36 36 99	addsubassd	$⊢ (A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \to A + A - 1 = A + A - 1$
101	38	oveq1d	$⊢ (A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \to 2 A - 1 = A + A - 1$
102		ax-1cn	$⊢ 1 \in ℂ$
103		subcl	$⊢ (A \in ℂ \land 1 \in ℂ) \to A - 1 \in ℂ$
104	36 102 103	sylancl	$⊢ (A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \to A - 1 \in ℂ$
105	36 104	subnegd	$⊢ (A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \to A - (- (A - 1)) = A + A - 1$
106	100 101 105	3eqtr4rd	$⊢ (A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \to A - (- (A - 1)) = 2 A - 1$
107	96 98 106	3brtr4d	$⊢ (A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \to 0 - 0 \leq A - (- (A - 1))$
108	107	ad2antrr	$⊢ (((A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \land 2 A ∥ (B - (- C))) \land C \in (0 \dots A - 1)) \to 0 - 0 \leq A - (- (A - 1))$
109		fzmaxdif	$⊢ ((0 \in ℤ \land - C \in (- (A - 1) \dots 0)) \land (A \in ℤ \land B \in (0 \dots A)) \land 0 - 0 \leq A - (- (A - 1))) \to \|- C - B\| \leq A - (- (A - 1))$
110	77 90 91 54 108 109	syl221anc	$⊢ (((A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \land 2 A ∥ (B - (- C))) \land C \in (0 \dots A - 1)) \to \|- C - B\| \leq A - (- (A - 1))$
111	76 110	eqbrtrd	$⊢ (((A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \land 2 A ∥ (B - (- C))) \land C \in (0 \dots A - 1)) \to \|B - (- C)\| \leq A - (- (A - 1))$
112	27	ltm1d	$⊢ (A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \to 2 A - 1 < 2 A$
113	106 112	eqbrtrd	$⊢ (A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \to A - (- (A - 1)) < 2 A$
114	113	ad2antrr	$⊢ (((A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \land 2 A ∥ (B - (- C))) \land C \in (0 \dots A - 1)) \to A - (- (A - 1)) < 2 A$
115	63 69 70 111 114	lelttrd	$⊢ (((A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \land 2 A ∥ (B - (- C))) \land C \in (0 \dots A - 1)) \to \|B - (- C)\| < 2 A$
116	93	ad2antrr	$⊢ (((A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \land 2 A ∥ (B - (- C))) \land C \in (0 \dots A - 1)) \to 2 A \in ℕ$
117		simplr	$⊢ (((A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \land 2 A ∥ (B - (- C))) \land C \in (0 \dots A - 1)) \to 2 A ∥ (B - (- C))$
118		congabseq	$⊢ ((2 A \in ℕ \land B \in ℤ \land - C \in ℤ) \land 2 A ∥ (B - (- C))) \to (\|B - (- C)\| < 2 A \leftrightarrow B = - C)$
119	116 71 74 117 118	syl31anc	$⊢ (((A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \land 2 A ∥ (B - (- C))) \land C \in (0 \dots A - 1)) \to (\|B - (- C)\| < 2 A \leftrightarrow B = - C)$
120	115 119	mpbid	$⊢ (((A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \land 2 A ∥ (B - (- C))) \land C \in (0 \dots A - 1)) \to B = - C$
121	56 120	breqtrd	$⊢ (((A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \land 2 A ∥ (B - (- C))) \land C \in (0 \dots A - 1)) \to 0 \leq - C$
122		elfzelz	$⊢ C \in (0 \dots A - 1) \to C \in ℤ$
123	122	zred	$⊢ C \in (0 \dots A - 1) \to C \in ℝ$
124	123	adantl	$⊢ (((A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \land 2 A ∥ (B - (- C))) \land C \in (0 \dots A - 1)) \to C \in ℝ$
125	124	le0neg1d	$⊢ (((A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \land 2 A ∥ (B - (- C))) \land C \in (0 \dots A - 1)) \to (C \leq 0 \leftrightarrow 0 \leq - C)$
126	121 125	mpbird	$⊢ (((A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \land 2 A ∥ (B - (- C))) \land C \in (0 \dots A - 1)) \to C \leq 0$
127		elfzle1	$⊢ C \in (0 \dots A - 1) \to 0 \leq C$
128	127	adantl	$⊢ (((A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \land 2 A ∥ (B - (- C))) \land C \in (0 \dots A - 1)) \to 0 \leq C$
129		letri3	$⊢ (C \in ℝ \land 0 \in ℝ) \to (C = 0 \leftrightarrow (C \leq 0 \land 0 \leq C))$
130	124 22 129	sylancl	$⊢ (((A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \land 2 A ∥ (B - (- C))) \land C \in (0 \dots A - 1)) \to (C = 0 \leftrightarrow (C \leq 0 \land 0 \leq C))$
131	126 128 130	mpbir2and	$⊢ (((A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \land 2 A ∥ (B - (- C))) \land C \in (0 \dots A - 1)) \to C = 0$
132	131	negeqd	$⊢ (((A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \land 2 A ∥ (B - (- C))) \land C \in (0 \dots A - 1)) \to - C = - 0$
133	132 88	eqtrd	$⊢ (((A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \land 2 A ∥ (B - (- C))) \land C \in (0 \dots A - 1)) \to - C = 0$
134	133 120 131	3eqtr4d	$⊢ (((A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \land 2 A ∥ (B - (- C))) \land C \in (0 \dots A - 1)) \to B = C$
135		oveq2	$⊢ C = A \to B - C = B - A$
136	135	adantl	$⊢ (((A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \land 2 A ∥ (B - (- C))) \land C = A) \to B - C = B - A$
137	136	fveq2d	$⊢ (((A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \land 2 A ∥ (B - (- C))) \land C = A) \to \|B - C\| = \|B - A\|$
138	40	ad2antrr	$⊢ (((A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \land 2 A ∥ (B - (- C))) \land C = A) \to \|B - C\| < 2 A$
139	137 138	eqbrtrrd	$⊢ (((A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \land 2 A ∥ (B - (- C))) \land C = A) \to \|B - A\| < 2 A$
140	93	ad2antrr	$⊢ (((A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \land 2 A ∥ (B - (- C))) \land C = A) \to 2 A \in ℕ$
141	7	ad2antrr	$⊢ (((A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \land 2 A ∥ (B - (- C))) \land C = A) \to B \in ℤ$
142	3	ad2antrr	$⊢ (((A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \land 2 A ∥ (B - (- C))) \land C = A) \to A \in ℤ$
143		simplr	$⊢ (((A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \land 2 A ∥ (B - (- C))) \land C = A) \to 2 A ∥ (B - (- C))$
144	7	zcnd	$⊢ (A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \to B \in ℂ$
145	36 36 144	ppncand	$⊢ (A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \to A + A + (B - A) = A + B$
146	36 144	addcomd	$⊢ (A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \to A + B = B + A$
147	145 146	eqtrd	$⊢ (A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \to A + A + (B - A) = B + A$
148	147	ad2antrr	$⊢ (((A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \land 2 A ∥ (B - (- C))) \land C = A) \to A + A + (B - A) = B + A$
149		oveq2	$⊢ C = A \to B + C = B + A$
150	149	adantl	$⊢ (((A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \land 2 A ∥ (B - (- C))) \land C = A) \to B + C = B + A$
151	148 150	eqtr4d	$⊢ (((A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \land 2 A ∥ (B - (- C))) \land C = A) \to A + A + (B - A) = B + C$
152	38	oveq1d	$⊢ (A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \to 2 A + B - A = A + A + (B - A)$
153	152	ad2antrr	$⊢ (((A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \land 2 A ∥ (B - (- C))) \land C = A) \to 2 A + B - A = A + A + (B - A)$
154	16	zcnd	$⊢ (A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \to C \in ℂ$
155	144 154	subnegd	$⊢ (A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \to B - (- C) = B + C$
156	155	ad2antrr	$⊢ (((A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \land 2 A ∥ (B - (- C))) \land C = A) \to B - (- C) = B + C$
157	151 153 156	3eqtr4d	$⊢ (((A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \land 2 A ∥ (B - (- C))) \land C = A) \to 2 A + B - A = B - (- C)$
158	143 157	breqtrrd	$⊢ (((A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \land 2 A ∥ (B - (- C))) \land C = A) \to 2 A ∥ (2 A + B - A)$
159	5	ad2antrr	$⊢ (((A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \land 2 A ∥ (B - (- C))) \land C = A) \to 2 A \in ℤ$
160	7 3	zsubcld	$⊢ (A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \to B - A \in ℤ$
161	160	ad2antrr	$⊢ (((A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \land 2 A ∥ (B - (- C))) \land C = A) \to B - A \in ℤ$
162		dvdsadd	$⊢ (2 A \in ℤ \land B - A \in ℤ) \to (2 A ∥ (B - A) \leftrightarrow 2 A ∥ (2 A + B - A))$
163	159 161 162	syl2anc	$⊢ (((A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \land 2 A ∥ (B - (- C))) \land C = A) \to (2 A ∥ (B - A) \leftrightarrow 2 A ∥ (2 A + B - A))$
164	158 163	mpbird	$⊢ (((A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \land 2 A ∥ (B - (- C))) \land C = A) \to 2 A ∥ (B - A)$
165		congabseq	$⊢ ((2 A \in ℕ \land B \in ℤ \land A \in ℤ) \land 2 A ∥ (B - A)) \to (\|B - A\| < 2 A \leftrightarrow B = A)$
166	140 141 142 164 165	syl31anc	$⊢ (((A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \land 2 A ∥ (B - (- C))) \land C = A) \to (\|B - A\| < 2 A \leftrightarrow B = A)$
167	139 166	mpbid	$⊢ (((A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \land 2 A ∥ (B - (- C))) \land C = A) \to B = A$
168		simpr	$⊢ (((A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \land 2 A ∥ (B - (- C))) \land C = A) \to C = A$
169	167 168	eqtr4d	$⊢ (((A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \land 2 A ∥ (B - (- C))) \land C = A) \to B = C$
170		nnnn0	$⊢ A \in ℕ \to A \in ℕ_{0}$
171	170	3ad2ant1	$⊢ (A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \to A \in ℕ_{0}$
172		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
173	171 172	eleqtrdi	$⊢ (A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \to A \in ℤ_{\geq 0}$
174		fzm1	$⊢ A \in ℤ_{\geq 0} \to (C \in (0 \dots A) \leftrightarrow (C \in (0 \dots A - 1) \lor C = A))$
175	174	biimpa	$⊢ (A \in ℤ_{\geq 0} \land C \in (0 \dots A)) \to (C \in (0 \dots A - 1) \lor C = A)$
176	173 29 175	syl2anc	$⊢ (A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \to (C \in (0 \dots A - 1) \lor C = A)$
177	176	adantr	$⊢ ((A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \land 2 A ∥ (B - (- C))) \to (C \in (0 \dots A - 1) \lor C = A)$
178	134 169 177	mpjaodan	$⊢ ((A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \land 2 A ∥ (B - (- C))) \to B = C$
179	53 178	jaodan	$⊢ ((A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \land (2 A ∥ (B - C) \lor 2 A ∥ (B - (- C)))) \to B = C$
180	14 179	impbida	$⊢ (A \in ℕ \land B \in (0 \dots A) \land C \in (0 \dots A)) \to (B = C \leftrightarrow (2 A ∥ (B - C) \lor 2 A ∥ (B - (- C))))$

Metamath Proof Explorer

Theorem acongeq

Proof