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 B A mod 1 = B mod 1

Proof

Step Hyp Ref Expression
1 zmod10 A A mod 1 = 0
2 1 adantr A B A mod 1 = 0
3 zmod10 B B mod 1 = 0
4 3 adantl A B B mod 1 = 0
5 2 4 eqtr4d A B A mod 1 = B mod 1