Metamath Proof Explorer

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 ⊢ A ∈ ℕ ∧ B ∈ ℤ ∧ C ∈ ℤ ∧ A ∥ B − C → B − C < A ↔ B = C

Proof

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