Theorem congid

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

	Ref	Expression
Assertion	congid	$$⊢\left(A\in \mathbb{Z}\wedge B\in \mathbb{Z}\right)\to A\parallel \left(B-B\right)$$

Proof

Step	Hyp	Ref	Expression
1		dvds0	$$⊢A\in \mathbb{Z}\to A\parallel 0$$
2	1	adantr	$$⊢\left(A\in \mathbb{Z}\wedge B\in \mathbb{Z}\right)\to A\parallel 0$$
3		zcn	$$⊢B\in \mathbb{Z}\to B\in ℂ$$
4	3	adantl	$$⊢\left(A\in \mathbb{Z}\wedge B\in \mathbb{Z}\right)\to B\in ℂ$$
5	4	subidd	$$⊢\left(A\in \mathbb{Z}\wedge B\in \mathbb{Z}\right)\to B-B=0$$
6	2 5	breqtrrd	$$⊢\left(A\in \mathbb{Z}\wedge B\in \mathbb{Z}\right)\to A\parallel \left(B-B\right)$$