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 e. ZZ /\ B e. ZZ ) -> A || ( B - B ) )

Proof

Step	Hyp	Ref	Expression
1		dvds0	|- ( A e. ZZ -> A || 0 )
2	1	adantr	|- ( ( A e. ZZ /\ B e. ZZ ) -> A || 0 )
3		zcn	|- ( B e. ZZ -> B e. CC )
4	3	adantl	|- ( ( A e. ZZ /\ B e. ZZ ) -> B e. CC )
5	4	subidd	|- ( ( A e. ZZ /\ B e. ZZ ) -> ( B - B ) = 0 )
6	2 5	breqtrrd	|- ( ( A e. ZZ /\ B e. ZZ ) -> A || ( B - B ) )