Theorem congid

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

	Ref	Expression
Assertion	congid	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → 𝐴 ∥ ( 𝐵 − 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		dvds0	⊢ ( 𝐴 ∈ ℤ → 𝐴 ∥ 0 )
2	1	adantr	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → 𝐴 ∥ 0 )
3		zcn	⊢ ( 𝐵 ∈ ℤ → 𝐵 ∈ ℂ )
4	3	adantl	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → 𝐵 ∈ ℂ )
5	4	subidd	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝐵 − 𝐵 ) = 0 )
6	2 5	breqtrrd	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → 𝐴 ∥ ( 𝐵 − 𝐵 ) )