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

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

Proof

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