Metamath Proof Explorer

Theorem zmod1congr

Description: Two arbitrary integers are congruent modulo 1, see example 4 in ApostolNT p. 107. (Contributed by AV, 21-Jul-2021)

Ref Expression
Assertion zmod1congr 
|- ( ( A e. ZZ /\ B e. ZZ ) -> ( A mod 1 ) = ( B mod 1 ) )

Proof

Step Hyp Ref Expression
1 zmod10 
 |-  ( A e. ZZ -> ( A mod 1 ) = 0 )
2 1 adantr 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( A mod 1 ) = 0 )
3 zmod10 
 |-  ( B e. ZZ -> ( B mod 1 ) = 0 )
4 3 adantl 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( B mod 1 ) = 0 )
5 2 4 eqtr4d 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( A mod 1 ) = ( B mod 1 ) )