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 \in ℤ \land B \in ℤ) \to A \mod 1 = B \mod 1$

Step	Hyp	Ref	Expression
1		zmod10	$⊢ A \in ℤ \to A \mod 1 = 0$
2	1	adantr	$⊢ (A \in ℤ \land B \in ℤ) \to A \mod 1 = 0$
3		zmod10	$⊢ B \in ℤ \to B \mod 1 = 0$
4	3	adantl	$⊢ (A \in ℤ \land B \in ℤ) \to B \mod 1 = 0$
5	2 4	eqtr4d	$⊢ (A \in ℤ \land B \in ℤ) \to A \mod 1 = B \mod 1$