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	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝐴 mod 1 ) = ( 𝐵 mod 1 ) )

Proof

Step	Hyp	Ref	Expression
1		zmod10	⊢ ( 𝐴 ∈ ℤ → ( 𝐴 mod 1 ) = 0 )
2	1	adantr	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝐴 mod 1 ) = 0 )
3		zmod10	⊢ ( 𝐵 ∈ ℤ → ( 𝐵 mod 1 ) = 0 )
4	3	adantl	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝐵 mod 1 ) = 0 )
5	2 4	eqtr4d	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝐴 mod 1 ) = ( 𝐵 mod 1 ) )