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 ⊢ A ∈ ℤ ∧ B = 2 ⁢ A → 2 ∥ B

Proof

Step Hyp Ref Expression
1 2z ⊢ 2 ∈ ℤ
2 dvdsmul1 ⊢ 2 ∈ ℤ ∧ A ∈ ℤ → 2 ∥ 2 ⁢ A
3 1 2 mpan ⊢ A ∈ ℤ → 2 ∥ 2 ⁢ A
4 3 adantr ⊢ A ∈ ℤ ∧ B = 2 ⁢ A → 2 ∥ 2 ⁢ A
5 breq2 ⊢ B = 2 ⁢ A → 2 ∥ B ↔ 2 ∥ 2 ⁢ A
6 5 adantl ⊢ A ∈ ℤ ∧ B = 2 ⁢ A → 2 ∥ B ↔ 2 ∥ 2 ⁢ A
7 4 6 mpbird ⊢ A ∈ ℤ ∧ B = 2 ⁢ A → 2 ∥ B