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 · 𝑛 ) = 𝑁 )