Mathbox for Stefan O'Rear < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  congabseq Unicode version

Theorem congabseq 27164
 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.)
Assertion
Ref Expression
congabseq

Proof of Theorem congabseq
StepHypRef Expression
1 zcn 10045 . . . . 5
213ad2ant2 977 . . . 4
4 zcn 10045 . . . . 5
543ad2ant3 978 . . . 4
7 zsubcl 10077 . . . . . . . . . 10
873adant1 973 . . . . . . . . 9
98zcnd 10134 . . . . . . . 8
109abscld 11934 . . . . . . 7
1110adantr 451 . . . . . 6
12 nnre 9769 . . . . . . . 8
13123ad2ant1 976 . . . . . . 7
1413adantr 451 . . . . . 6
1511, 14ltnled 8982 . . . . 5
1615biimpa 470 . . . 4
17 nnz 10061 . . . . . . . . . 10
18173ad2ant1 976 . . . . . . . . 9
1918ad3antrrr 710 . . . . . . . 8
208ad3antrrr 710 . . . . . . . 8
21 simpr 447 . . . . . . . 8
2219, 20, 213jca 1132 . . . . . . 7
23 simpllr 735 . . . . . . 7
24 dvdsleabs 12591 . . . . . . 7
2522, 23, 24sylc 56 . . . . . 6
2625ex 423 . . . . 5
2726necon1bd 2527 . . . 4
2816, 27mpd 14 . . 3
293, 6, 28subeq0d 9181 . 2
30 oveq1 5881 . . . . . . 7
3130adantl 452 . . . . . 6
325ad2antrr 706 . . . . . . 7
3332subidd 9161 . . . . . 6
3431, 33eqtrd 2328 . . . . 5
3534fveq2d 5545 . . . 4
36 abs0 11786 . . . 4
3735, 36syl6eq 2344 . . 3
38 nngt0 9791 . . . . 5
39383ad2ant1 976 . . . 4