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

Metamath Proof Explorer

Theorem evennn02n

Description: A nonnegative integer is even iff it is twice another nonnegative integer. (Contributed by AV, 12-Aug-2021) (Proof shortened by AV, 10-Jul-2022)

Ref Expression
Assertion evennn02n ( 𝑁 ∈ ℕ0 → ( 2 ∥ 𝑁 ↔ ∃ 𝑛 ∈ ℕ0 ( 2 · 𝑛 ) = 𝑁 ) )

Proof

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