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