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