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