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 e. NN /\ B e. ZZ /\ C e. ZZ ) /\ A || ( B - C ) ) -> ( ( abs ` ( B - C ) ) < A <-> B = C ) )

Proof

Step Hyp Ref Expression
1 zcn 
 |-  ( B e. ZZ -> B e. CC )
2 1 3ad2ant2 
 |-  ( ( A e. NN /\ B e. ZZ /\ C e. ZZ ) -> B e. CC )
3 2 ad2antrr 
 |-  ( ( ( ( A e. NN /\ B e. ZZ /\ C e. ZZ ) /\ A || ( B - C ) ) /\ ( abs ` ( B - C ) ) < A ) -> B e. CC )
4 zcn 
 |-  ( C e. ZZ -> C e. CC )
5 4 3ad2ant3 
 |-  ( ( A e. NN /\ B e. ZZ /\ C e. ZZ ) -> C e. CC )
6 5 ad2antrr 
 |-  ( ( ( ( A e. NN /\ B e. ZZ /\ C e. ZZ ) /\ A || ( B - C ) ) /\ ( abs ` ( B - C ) ) < A ) -> C e. CC )
7 zsubcl 
 |-  ( ( B e. ZZ /\ C e. ZZ ) -> ( B - C ) e. ZZ )
8 7 3adant1 
 |-  ( ( A e. NN /\ B e. ZZ /\ C e. ZZ ) -> ( B - C ) e. ZZ )
9 8 zcnd 
 |-  ( ( A e. NN /\ B e. ZZ /\ C e. ZZ ) -> ( B - C ) e. CC )
10 9 abscld 
 |-  ( ( A e. NN /\ B e. ZZ /\ C e. ZZ ) -> ( abs ` ( B - C ) ) e. RR )
11 10 adantr 
 |-  ( ( ( A e. NN /\ B e. ZZ /\ C e. ZZ ) /\ A || ( B - C ) ) -> ( abs ` ( B - C ) ) e. RR )
12 nnre 
 |-  ( A e. NN -> A e. RR )
13 12 3ad2ant1 
 |-  ( ( A e. NN /\ B e. ZZ /\ C e. ZZ ) -> A e. RR )
14 13 adantr 
 |-  ( ( ( A e. NN /\ B e. ZZ /\ C e. ZZ ) /\ A || ( B - C ) ) -> A e. RR )
15 11 14 ltnled 
 |-  ( ( ( A e. NN /\ B e. ZZ /\ C e. ZZ ) /\ A || ( B - C ) ) -> ( ( abs ` ( B - C ) ) < A <-> -. A <_ ( abs ` ( B - C ) ) ) )
16 15 biimpa 
 |-  ( ( ( ( A e. NN /\ B e. ZZ /\ C e. ZZ ) /\ A || ( B - C ) ) /\ ( abs ` ( B - C ) ) < A ) -> -. A <_ ( abs ` ( B - C ) ) )
17 nnz 
 |-  ( A e. NN -> A e. ZZ )
18 17 3ad2ant1 
 |-  ( ( A e. NN /\ B e. ZZ /\ C e. ZZ ) -> A e. ZZ )
19 18 ad3antrrr 
 |-  ( ( ( ( ( A e. NN /\ B e. ZZ /\ C e. ZZ ) /\ A || ( B - C ) ) /\ ( abs ` ( B - C ) ) < A ) /\ ( B - C ) =/= 0 ) -> A e. ZZ )
20 8 ad3antrrr 
 |-  ( ( ( ( ( A e. NN /\ B e. ZZ /\ C e. ZZ ) /\ A || ( B - C ) ) /\ ( abs ` ( B - C ) ) < A ) /\ ( B - C ) =/= 0 ) -> ( B - C ) e. ZZ )
21 simpr 
 |-  ( ( ( ( ( A e. NN /\ B e. ZZ /\ C e. ZZ ) /\ A || ( B - C ) ) /\ ( abs ` ( B - C ) ) < A ) /\ ( B - C ) =/= 0 ) -> ( B - C ) =/= 0 )
22 19 20 21 3jca 
 |-  ( ( ( ( ( A e. NN /\ B e. ZZ /\ C e. ZZ ) /\ A || ( B - C ) ) /\ ( abs ` ( B - C ) ) < A ) /\ ( B - C ) =/= 0 ) -> ( A e. ZZ /\ ( B - C ) e. ZZ /\ ( B - C ) =/= 0 ) )
23 simpllr 
 |-  ( ( ( ( ( A e. NN /\ B e. ZZ /\ C e. ZZ ) /\ A || ( B - C ) ) /\ ( abs ` ( B - C ) ) < A ) /\ ( B - C ) =/= 0 ) -> A || ( B - C ) )
24 dvdsleabs 
 |-  ( ( A e. ZZ /\ ( B - C ) e. ZZ /\ ( B - C ) =/= 0 ) -> ( A || ( B - C ) -> A <_ ( abs ` ( B - C ) ) ) )
25 22 23 24 sylc 
 |-  ( ( ( ( ( A e. NN /\ B e. ZZ /\ C e. ZZ ) /\ A || ( B - C ) ) /\ ( abs ` ( B - C ) ) < A ) /\ ( B - C ) =/= 0 ) -> A <_ ( abs ` ( B - C ) ) )
26 25 ex 
 |-  ( ( ( ( A e. NN /\ B e. ZZ /\ C e. ZZ ) /\ A || ( B - C ) ) /\ ( abs ` ( B - C ) ) < A ) -> ( ( B - C ) =/= 0 -> A <_ ( abs ` ( B - C ) ) ) )
27 26 necon1bd 
 |-  ( ( ( ( A e. NN /\ B e. ZZ /\ C e. ZZ ) /\ A || ( B - C ) ) /\ ( abs ` ( B - C ) ) < A ) -> ( -. A <_ ( abs ` ( B - C ) ) -> ( B - C ) = 0 ) )
28 16 27 mpd 
 |-  ( ( ( ( A e. NN /\ B e. ZZ /\ C e. ZZ ) /\ A || ( B - C ) ) /\ ( abs ` ( B - C ) ) < A ) -> ( B - C ) = 0 )
29 3 6 28 subeq0d 
 |-  ( ( ( ( A e. NN /\ B e. ZZ /\ C e. ZZ ) /\ A || ( B - C ) ) /\ ( abs ` ( B - C ) ) < A ) -> B = C )
30 oveq1 
 |-  ( B = C -> ( B - C ) = ( C - C ) )
31 30 adantl 
 |-  ( ( ( ( A e. NN /\ B e. ZZ /\ C e. ZZ ) /\ A || ( B - C ) ) /\ B = C ) -> ( B - C ) = ( C - C ) )
32 5 ad2antrr 
 |-  ( ( ( ( A e. NN /\ B e. ZZ /\ C e. ZZ ) /\ A || ( B - C ) ) /\ B = C ) -> C e. CC )
33 32 subidd 
 |-  ( ( ( ( A e. NN /\ B e. ZZ /\ C e. ZZ ) /\ A || ( B - C ) ) /\ B = C ) -> ( C - C ) = 0 )
34 31 33 eqtrd 
 |-  ( ( ( ( A e. NN /\ B e. ZZ /\ C e. ZZ ) /\ A || ( B - C ) ) /\ B = C ) -> ( B - C ) = 0 )
35 34 abs00bd 
 |-  ( ( ( ( A e. NN /\ B e. ZZ /\ C e. ZZ ) /\ A || ( B - C ) ) /\ B = C ) -> ( abs ` ( B - C ) ) = 0 )
36 nngt0 
 |-  ( A e. NN -> 0 < A )
37 36 3ad2ant1 
 |-  ( ( A e. NN /\ B e. ZZ /\ C e. ZZ ) -> 0 < A )
38 37 ad2antrr 
 |-  ( ( ( ( A e. NN /\ B e. ZZ /\ C e. ZZ ) /\ A || ( B - C ) ) /\ B = C ) -> 0 < A )
39 35 38 eqbrtrd 
 |-  ( ( ( ( A e. NN /\ B e. ZZ /\ C e. ZZ ) /\ A || ( B - C ) ) /\ B = C ) -> ( abs ` ( B - C ) ) < A )
40 29 39 impbida 
 |-  ( ( ( A e. NN /\ B e. ZZ /\ C e. ZZ ) /\ A || ( B - C ) ) -> ( ( abs ` ( B - C ) ) < A <-> B = C ) )