Metamath Proof Explorer


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 ∥ 𝐵 )