Theorem congabseq

Description: If two integers are congruent, they are either equal or separated by at least the congruence base. (Contributed by Stefan O'Rear, 4-Oct-2014)

	Ref	Expression
Assertion	congabseq	⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ 𝐴 ∥ ( 𝐵 − 𝐶 ) ) → ( ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝐴 ↔ 𝐵 = 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		zcn	⊢ ( 𝐵 ∈ ℤ → 𝐵 ∈ ℂ )
2	1	3ad2ant2	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → 𝐵 ∈ ℂ )
3	2	ad2antrr	⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ 𝐴 ∥ ( 𝐵 − 𝐶 ) ) ∧ ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝐴 ) → 𝐵 ∈ ℂ )
4		zcn	⊢ ( 𝐶 ∈ ℤ → 𝐶 ∈ ℂ )
5	4	3ad2ant3	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → 𝐶 ∈ ℂ )
6	5	ad2antrr	⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ 𝐴 ∥ ( 𝐵 − 𝐶 ) ) ∧ ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝐴 ) → 𝐶 ∈ ℂ )
7		zsubcl	⊢ ( ( 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → ( 𝐵 − 𝐶 ) ∈ ℤ )
8	7	3adant1	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → ( 𝐵 − 𝐶 ) ∈ ℤ )
9	8	zcnd	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → ( 𝐵 − 𝐶 ) ∈ ℂ )
10	9	abscld	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → ( abs ‘ ( 𝐵 − 𝐶 ) ) ∈ ℝ )
11	10	adantr	⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ 𝐴 ∥ ( 𝐵 − 𝐶 ) ) → ( abs ‘ ( 𝐵 − 𝐶 ) ) ∈ ℝ )
12		nnre	⊢ ( 𝐴 ∈ ℕ → 𝐴 ∈ ℝ )
13	12	3ad2ant1	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → 𝐴 ∈ ℝ )
14	13	adantr	⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ 𝐴 ∥ ( 𝐵 − 𝐶 ) ) → 𝐴 ∈ ℝ )
15	11 14	ltnled	⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ 𝐴 ∥ ( 𝐵 − 𝐶 ) ) → ( ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝐴 ↔ ¬ 𝐴 ≤ ( abs ‘ ( 𝐵 − 𝐶 ) ) ) )
16	15	biimpa	⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ 𝐴 ∥ ( 𝐵 − 𝐶 ) ) ∧ ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝐴 ) → ¬ 𝐴 ≤ ( abs ‘ ( 𝐵 − 𝐶 ) ) )
17		nnz	⊢ ( 𝐴 ∈ ℕ → 𝐴 ∈ ℤ )
18	17	3ad2ant1	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → 𝐴 ∈ ℤ )
19	18	ad3antrrr	⊢ ( ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ 𝐴 ∥ ( 𝐵 − 𝐶 ) ) ∧ ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝐴 ) ∧ ( 𝐵 − 𝐶 ) ≠ 0 ) → 𝐴 ∈ ℤ )
20	8	ad3antrrr	⊢ ( ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ 𝐴 ∥ ( 𝐵 − 𝐶 ) ) ∧ ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝐴 ) ∧ ( 𝐵 − 𝐶 ) ≠ 0 ) → ( 𝐵 − 𝐶 ) ∈ ℤ )
21		simpr	⊢ ( ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ 𝐴 ∥ ( 𝐵 − 𝐶 ) ) ∧ ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝐴 ) ∧ ( 𝐵 − 𝐶 ) ≠ 0 ) → ( 𝐵 − 𝐶 ) ≠ 0 )
22	19 20 21	3jca	⊢ ( ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ 𝐴 ∥ ( 𝐵 − 𝐶 ) ) ∧ ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝐴 ) ∧ ( 𝐵 − 𝐶 ) ≠ 0 ) → ( 𝐴 ∈ ℤ ∧ ( 𝐵 − 𝐶 ) ∈ ℤ ∧ ( 𝐵 − 𝐶 ) ≠ 0 ) )
23		simpllr	⊢ ( ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ 𝐴 ∥ ( 𝐵 − 𝐶 ) ) ∧ ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝐴 ) ∧ ( 𝐵 − 𝐶 ) ≠ 0 ) → 𝐴 ∥ ( 𝐵 − 𝐶 ) )
24		dvdsleabs	⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝐵 − 𝐶 ) ∈ ℤ ∧ ( 𝐵 − 𝐶 ) ≠ 0 ) → ( 𝐴 ∥ ( 𝐵 − 𝐶 ) → 𝐴 ≤ ( abs ‘ ( 𝐵 − 𝐶 ) ) ) )
25	22 23 24	sylc	⊢ ( ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ 𝐴 ∥ ( 𝐵 − 𝐶 ) ) ∧ ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝐴 ) ∧ ( 𝐵 − 𝐶 ) ≠ 0 ) → 𝐴 ≤ ( abs ‘ ( 𝐵 − 𝐶 ) ) )
26	25	ex	⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ 𝐴 ∥ ( 𝐵 − 𝐶 ) ) ∧ ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝐴 ) → ( ( 𝐵 − 𝐶 ) ≠ 0 → 𝐴 ≤ ( abs ‘ ( 𝐵 − 𝐶 ) ) ) )
27	26	necon1bd	⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ 𝐴 ∥ ( 𝐵 − 𝐶 ) ) ∧ ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝐴 ) → ( ¬ 𝐴 ≤ ( abs ‘ ( 𝐵 − 𝐶 ) ) → ( 𝐵 − 𝐶 ) = 0 ) )
28	16 27	mpd	⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ 𝐴 ∥ ( 𝐵 − 𝐶 ) ) ∧ ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝐴 ) → ( 𝐵 − 𝐶 ) = 0 )
29	3 6 28	subeq0d	⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ 𝐴 ∥ ( 𝐵 − 𝐶 ) ) ∧ ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝐴 ) → 𝐵 = 𝐶 )
30		oveq1	⊢ ( 𝐵 = 𝐶 → ( 𝐵 − 𝐶 ) = ( 𝐶 − 𝐶 ) )
31	30	adantl	⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ 𝐴 ∥ ( 𝐵 − 𝐶 ) ) ∧ 𝐵 = 𝐶 ) → ( 𝐵 − 𝐶 ) = ( 𝐶 − 𝐶 ) )
32	5	ad2antrr	⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ 𝐴 ∥ ( 𝐵 − 𝐶 ) ) ∧ 𝐵 = 𝐶 ) → 𝐶 ∈ ℂ )
33	32	subidd	⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ 𝐴 ∥ ( 𝐵 − 𝐶 ) ) ∧ 𝐵 = 𝐶 ) → ( 𝐶 − 𝐶 ) = 0 )
34	31 33	eqtrd	⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ 𝐴 ∥ ( 𝐵 − 𝐶 ) ) ∧ 𝐵 = 𝐶 ) → ( 𝐵 − 𝐶 ) = 0 )
35	34	abs00bd	⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ 𝐴 ∥ ( 𝐵 − 𝐶 ) ) ∧ 𝐵 = 𝐶 ) → ( abs ‘ ( 𝐵 − 𝐶 ) ) = 0 )
36		nngt0	⊢ ( 𝐴 ∈ ℕ → 0 < 𝐴 )
37	36	3ad2ant1	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → 0 < 𝐴 )
38	37	ad2antrr	⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ 𝐴 ∥ ( 𝐵 − 𝐶 ) ) ∧ 𝐵 = 𝐶 ) → 0 < 𝐴 )
39	35 38	eqbrtrd	⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ 𝐴 ∥ ( 𝐵 − 𝐶 ) ) ∧ 𝐵 = 𝐶 ) → ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝐴 )
40	29 39	impbida	⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ 𝐴 ∥ ( 𝐵 − 𝐶 ) ) → ( ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝐴 ↔ 𝐵 = 𝐶 ) )