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