Metamath Proof Explorer

Theorem even2n

Description: An integer is even iff it is twice another integer. (Contributed by AV, 25-Jun-2020)

Ref Expression
Assertion even2n ⊢2∥N↔∃n∈ℤ2⁢n=N

Proof

Step Hyp Ref Expression
1 evenelz ⊢2∥N→N∈ℤ
2 2z ⊢2∈ℤ
3 2 a1i ⊢n∈ℤ→2∈ℤ
4 id ⊢n∈ℤ→n∈ℤ
5 3 4 zmulcld ⊢n∈ℤ→2⁢n∈ℤ
6 5 adantr ⊢n∈ℤ∧2⁢n=N→2⁢n∈ℤ
7 eleq1 ⊢2⁢n=N→2⁢n∈ℤ↔N∈ℤ
8 7 adantl ⊢n∈ℤ∧2⁢n=N→2⁢n∈ℤ↔N∈ℤ
9 6 8 mpbid ⊢n∈ℤ∧2⁢n=N→N∈ℤ
10 9 rexlimiva ⊢∃n∈ℤ2⁢n=N→N∈ℤ
11 divides ⊢2∈ℤ∧N∈ℤ→2∥N↔∃n∈ℤn⋅2=N
12 zcn ⊢n∈ℤ→n∈ℂ
13 2cnd ⊢n∈ℤ→2∈ℂ
14 12 13 mulcomd ⊢n∈ℤ→n⋅2=2⁢n
15 14 eqeq1d ⊢n∈ℤ→n⋅2=N↔2⁢n=N
16 15 rexbiia ⊢∃n∈ℤn⋅2=N↔∃n∈ℤ2⁢n=N
17 11 16 bitrdi ⊢2∈ℤ∧N∈ℤ→2∥N↔∃n∈ℤ2⁢n=N
18 2 17 mpan ⊢N∈ℤ→2∥N↔∃n∈ℤ2⁢n=N
19 1 10 18 pm5.21nii ⊢2∥N↔∃n∈ℤ2⁢n=N