Theorem elz 12617

Description: Membership in the set of integers. (Contributed by NM, 8-Jan-2002.)

Assertion

Ref	Expression
elz	⊢ (𝑁 ∈ ℤ ↔ (𝑁 ∈ ℝ ∧ (𝑁 = 0 ∨ 𝑁 ∈ ℕ ∨ -𝑁 ∈ ℕ)))

Proof of Theorem elz

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqeq1 2764	. . 3 ⊢ (𝑥 = 𝑁 → (𝑥 = 0 ↔ 𝑁 = 0))
2		eleq1 2848	. . 3 ⊢ (𝑥 = 𝑁 → (𝑥 ∈ ℕ ↔ 𝑁 ∈ ℕ))
3		negeq 11473	. . . 4 ⊢ (𝑥 = 𝑁 → -𝑥 = -𝑁)
4	3	eleq1d 2845	. . 3 ⊢ (𝑥 = 𝑁 → (-𝑥 ∈ ℕ ↔ -𝑁 ∈ ℕ))
5	1, 2, 4	3orbi123d 1463	. 2 ⊢ (𝑥 = 𝑁 → ((𝑥 = 0 ∨ 𝑥 ∈ ℕ ∨ -𝑥 ∈ ℕ) ↔ (𝑁 = 0 ∨ 𝑁 ∈ ℕ ∨ -𝑁 ∈ ℕ)))
6		df-z 12616	. 2 ⊢ ℤ = {𝑥 ∈ ℝ ∣ (𝑥 = 0 ∨ 𝑥 ∈ ℕ ∨ -𝑥 ∈ ℕ)}
7	5, 6	elrab2 3649	1 ⊢ (𝑁 ∈ ℤ ↔ (𝑁 ∈ ℝ ∧ (𝑁 = 0 ∨ 𝑁 ∈ ℕ ∨ -𝑁 ∈ ℕ)))

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   ∨ w3o 1102   = wceq 1570   ∈ wcel 2145  ℝcr 11123  0cc0 11124  -cneg 11466  ℕcn 12257  ℤcz 12615

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-iota 6489  df-fv 6541  df-ov 7416  df-neg 11468  df-z 12616

This theorem is used by:  nnnegz  12618  zre  12619  elnnz  12625  0z  12626  elznn0nn  12629  elznn0  12630  elznn  12631  nnz  12636  znegcl  12653  zeo  12707  addmodlteq  14010  zabsle1  27532  ostthlem1  27863  ostth3  27874  elzdif0  34490  qqhval2lem  34491  exp11d  43201