MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  elz Structured version   Visualization version   GIF version

Theorem elz 12556
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.
StepHypRef Expression
1 eqeq1 2736 . . 3 (𝑥 = 𝑁 → (𝑥 = 0 ↔ 𝑁 = 0))
2 eleq1 2821 . . 3 (𝑥 = 𝑁 → (𝑥 ∈ ℕ ↔ 𝑁 ∈ ℕ))
3 negeq 11448 . . . 4 (𝑥 = 𝑁 → -𝑥 = -𝑁)
43eleq1d 2818 . . 3 (𝑥 = 𝑁 → (-𝑥 ∈ ℕ ↔ -𝑁 ∈ ℕ))
51, 2, 43orbi123d 1435 . 2 (𝑥 = 𝑁 → ((𝑥 = 0 ∨ 𝑥 ∈ ℕ ∨ -𝑥 ∈ ℕ) ↔ (𝑁 = 0 ∨ 𝑁 ∈ ℕ ∨ -𝑁 ∈ ℕ)))
6 df-z 12555 . 2 ℤ = {𝑥 ∈ ℝ ∣ (𝑥 = 0 ∨ 𝑥 ∈ ℕ ∨ -𝑥 ∈ ℕ)}
75, 6elrab2 3685 1 (𝑁 ∈ ℤ ↔ (𝑁 ∈ ℝ ∧ (𝑁 = 0 ∨ 𝑁 ∈ ℕ ∨ -𝑁 ∈ ℕ)))
Colors of variables: wff setvar class
Syntax hints:  wb 205  wa 396  w3o 1086   = wceq 1541  wcel 2106  cr 11105  0cc0 11106  -cneg 11441  cn 12208  cz 12554
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-rab 3433  df-v 3476  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-iota 6492  df-fv 6548  df-ov 7408  df-neg 11443  df-z 12555
This theorem is referenced by:  nnnegz  12557  zre  12558  elnnz  12564  0z  12565  elznn0nn  12568  elznn0  12569  elznn  12570  nnz  12575  znegcl  12593  zeo  12644  addmodlteq  13907  zabsle1  26788  ostthlem1  27119  ostth3  27130  elzdif0  32948  qqhval2lem  32949  exp11d  41211
  Copyright terms: Public domain W3C validator