This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( 𝑁 ∈ ℕ → ( 2 ∥ 𝑁 ↔ ∃ 𝑛 ∈ ℕ ( 2 · 𝑛 ) = 𝑁 ) )

Proof

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