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

Theorem congabseq 35530
 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 10942 . . . . 5
213ad2ant2 1027 . . . 4
4 zcn 10942 . . . . 5
543ad2ant3 1028 . . . 4
7 zsubcl 10979 . . . . . . . . . 10
873adant1 1023 . . . . . . . . 9
98zcnd 11041 . . . . . . . 8
109abscld 13476 . . . . . . 7
1110adantr 466 . . . . . 6
12 nnre 10616 . . . . . . . 8
13123ad2ant1 1026 . . . . . . 7
1413adantr 466 . . . . . 6
1511, 14ltnled 9781 . . . . 5
1615biimpa 486 . . . 4
17 nnz 10959 . . . . . . . . . 10
18173ad2ant1 1026 . . . . . . . . 9
1918ad3antrrr 734 . . . . . . . 8
208ad3antrrr 734 . . . . . . . 8
21 simpr 462 . . . . . . . 8
2219, 20, 213jca 1185 . . . . . . 7
23 simpllr 767 . . . . . . 7
24 dvdsleabs 14329 . . . . . . 7
2522, 23, 24sylc 62 . . . . . 6
2625ex 435 . . . . 5
2726necon1bd 2649 . . . 4
2816, 27mpd 15 . . 3
293, 6, 28subeq0d 9993 . 2
30 oveq1 6312 . . . . . 6
3130adantl 467 . . . . 5
325ad2antrr 730 . . . . . 6
3332subidd 9973 . . . . 5
3431, 33eqtrd 2470 . . . 4
3534abs00bd 13333 . . 3
36 nngt0 10638 . . . . 5
37363ad2ant1 1026 . . . 4