Metamath Proof Explorer

Theorem congid

Description: Every integer is congruent to itself mod every base. (Contributed by Stefan O'Rear, 1-Oct-2014)

		Ref	Expression
	Assertion	congid	$⊢ (A \in ℤ \land B \in ℤ) \to A ∥ (B - B)$

Step	Hyp	Ref	Expression
1		dvds0	$⊢ A \in ℤ \to A ∥ 0$
2	1	adantr	$⊢ (A \in ℤ \land B \in ℤ) \to A ∥ 0$
3		zcn	$⊢ B \in ℤ \to B \in ℂ$
4	3	adantl	$⊢ (A \in ℤ \land B \in ℤ) \to B \in ℂ$
5	4	subidd	$⊢ (A \in ℤ \land B \in ℤ) \to B - B = 0$
6	2 5	breqtrrd	$⊢ (A \in ℤ \land B \in ℤ) \to A ∥ (B - B)$