Metamath Proof Explorer

Theorem evennn2n

Description: A positive integer is even iff it is twice another positive integer. (Contributed by AV, 12-Aug-2021)

Ref Expression
Assertion evennn2n ⊢ N ∈ ℕ → 2 ∥ N ↔ ∃ n ∈ ℕ 2 ⁢ n = N

Proof

Step Hyp Ref Expression
1 eleq1 ⊢ 2 ⁢ n = N → 2 ⁢ n ∈ ℕ ↔ N ∈ ℕ
2 simpr ⊢ 2 ⁢ n ∈ ℕ ∧ n ∈ ℤ → n ∈ ℤ
3 2re ⊢ 2 ∈ ℝ
4 3 a1i ⊢ 2 ⁢ n ∈ ℕ ∧ n ∈ ℤ → 2 ∈ ℝ
5 zre ⊢ n ∈ ℤ → n ∈ ℝ
6 5 adantl ⊢ 2 ⁢ n ∈ ℕ ∧ n ∈ ℤ → n ∈ ℝ
7 0le2 ⊢ 0 ≤ 2
8 7 a1i ⊢ 2 ⁢ n ∈ ℕ ∧ n ∈ ℤ → 0 ≤ 2
9 nngt0 ⊢ 2 ⁢ n ∈ ℕ → 0 < 2 ⁢ n
10 9 adantr ⊢ 2 ⁢ n ∈ ℕ ∧ n ∈ ℤ → 0 < 2 ⁢ n
11 prodgt0 ⊢ 2 ∈ ℝ ∧ n ∈ ℝ ∧ 0 ≤ 2 ∧ 0 < 2 ⁢ n → 0 < n
12 4 6 8 10 11 syl22anc ⊢ 2 ⁢ n ∈ ℕ ∧ n ∈ ℤ → 0 < n
13 elnnz ⊢ n ∈ ℕ ↔ n ∈ ℤ ∧ 0 < n
14 2 12 13 sylanbrc ⊢ 2 ⁢ n ∈ ℕ ∧ n ∈ ℤ → n ∈ ℕ
15 14 ex ⊢ 2 ⁢ n ∈ ℕ → n ∈ ℤ → n ∈ ℕ
16 1 15 biimtrrdi ⊢ 2 ⁢ n = N → N ∈ ℕ → n ∈ ℤ → n ∈ ℕ
17 16 com13 ⊢ n ∈ ℤ → N ∈ ℕ → 2 ⁢ n = N → n ∈ ℕ
18 17 impcom ⊢ N ∈ ℕ ∧ n ∈ ℤ → 2 ⁢ n = N → n ∈ ℕ
19 18 pm4.71rd ⊢ N ∈ ℕ ∧ n ∈ ℤ → 2 ⁢ n = N ↔ n ∈ ℕ ∧ 2 ⁢ n = N
20 19 bicomd ⊢ N ∈ ℕ ∧ n ∈ ℤ → n ∈ ℕ ∧ 2 ⁢ n = N ↔ 2 ⁢ n = N
21 20 rexbidva ⊢ N ∈ ℕ → ∃ n ∈ ℤ n ∈ ℕ ∧ 2 ⁢ n = N ↔ ∃ n ∈ ℤ 2 ⁢ n = N
22 nnssz ⊢ ℕ ⊆ ℤ
23 rexss ⊢ ℕ ⊆ ℤ → ∃ n ∈ ℕ 2 ⁢ n = N ↔ ∃ n ∈ ℤ n ∈ ℕ ∧ 2 ⁢ n = N
24 22 23 mp1i ⊢ N ∈ ℕ → ∃ n ∈ ℕ 2 ⁢ n = N ↔ ∃ n ∈ ℤ n ∈ ℕ ∧ 2 ⁢ n = N
25 even2n ⊢ 2 ∥ N ↔ ∃ n ∈ ℤ 2 ⁢ n = N
26 25 a1i ⊢ N ∈ ℕ → 2 ∥ N ↔ ∃ n ∈ ℤ 2 ⁢ n = N
27 21 24 26 3bitr4rd ⊢ N ∈ ℕ → 2 ∥ N ↔ ∃ n ∈ ℕ 2 ⁢ n = N