Theorem 2teven

Description: A number which is twice an integer is even. (Contributed by AV, 16-Jul-2021)

	Ref	Expression
Assertion	2teven	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 = ( 2 · 𝐴 ) ) → 2 ∥ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		2z	⊢ 2 ∈ ℤ
2		dvdsmul1	⊢ ( ( 2 ∈ ℤ ∧ 𝐴 ∈ ℤ ) → 2 ∥ ( 2 · 𝐴 ) )
3	1 2	mpan	⊢ ( 𝐴 ∈ ℤ → 2 ∥ ( 2 · 𝐴 ) )
4	3	adantr	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 = ( 2 · 𝐴 ) ) → 2 ∥ ( 2 · 𝐴 ) )
5		breq2	⊢ ( 𝐵 = ( 2 · 𝐴 ) → ( 2 ∥ 𝐵 ↔ 2 ∥ ( 2 · 𝐴 ) ) )
6	5	adantl	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 = ( 2 · 𝐴 ) ) → ( 2 ∥ 𝐵 ↔ 2 ∥ ( 2 · 𝐴 ) ) )
7	4 6	mpbird	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 = ( 2 · 𝐴 ) ) → 2 ∥ 𝐵 )