ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  elnn0z GIF version

Theorem elnn0z 9283
Description: Nonnegative integer property expressed in terms of integers. (Contributed by NM, 9-May-2004.)
Assertion
Ref Expression
elnn0z (𝑁 ∈ ℕ0 ↔ (𝑁 ∈ ℤ ∧ 0 ≤ 𝑁))

Proof of Theorem elnn0z
StepHypRef Expression
1 nn0re 9202 . . . 4 (𝑁 ∈ ℕ0𝑁 ∈ ℝ)
2 elnn0 9195 . . . . . . 7 (𝑁 ∈ ℕ0 ↔ (𝑁 ∈ ℕ ∨ 𝑁 = 0))
32biimpi 120 . . . . . 6 (𝑁 ∈ ℕ0 → (𝑁 ∈ ℕ ∨ 𝑁 = 0))
43orcomd 730 . . . . 5 (𝑁 ∈ ℕ0 → (𝑁 = 0 ∨ 𝑁 ∈ ℕ))
5 3mix1 1167 . . . . . 6 (𝑁 = 0 → (𝑁 = 0 ∨ 𝑁 ∈ ℕ ∨ -𝑁 ∈ ℕ))
6 3mix2 1168 . . . . . 6 (𝑁 ∈ ℕ → (𝑁 = 0 ∨ 𝑁 ∈ ℕ ∨ -𝑁 ∈ ℕ))
75, 6jaoi 717 . . . . 5 ((𝑁 = 0 ∨ 𝑁 ∈ ℕ) → (𝑁 = 0 ∨ 𝑁 ∈ ℕ ∨ -𝑁 ∈ ℕ))
84, 7syl 14 . . . 4 (𝑁 ∈ ℕ0 → (𝑁 = 0 ∨ 𝑁 ∈ ℕ ∨ -𝑁 ∈ ℕ))
9 elz 9272 . . . 4 (𝑁 ∈ ℤ ↔ (𝑁 ∈ ℝ ∧ (𝑁 = 0 ∨ 𝑁 ∈ ℕ ∨ -𝑁 ∈ ℕ)))
101, 8, 9sylanbrc 417 . . 3 (𝑁 ∈ ℕ0𝑁 ∈ ℤ)
11 nn0ge0 9218 . . 3 (𝑁 ∈ ℕ0 → 0 ≤ 𝑁)
1210, 11jca 306 . 2 (𝑁 ∈ ℕ0 → (𝑁 ∈ ℤ ∧ 0 ≤ 𝑁))
139simprbi 275 . . . 4 (𝑁 ∈ ℤ → (𝑁 = 0 ∨ 𝑁 ∈ ℕ ∨ -𝑁 ∈ ℕ))
1413adantr 276 . . 3 ((𝑁 ∈ ℤ ∧ 0 ≤ 𝑁) → (𝑁 = 0 ∨ 𝑁 ∈ ℕ ∨ -𝑁 ∈ ℕ))
15 0nn0 9208 . . . . . 6 0 ∈ ℕ0
16 eleq1 2251 . . . . . 6 (𝑁 = 0 → (𝑁 ∈ ℕ0 ↔ 0 ∈ ℕ0))
1715, 16mpbiri 168 . . . . 5 (𝑁 = 0 → 𝑁 ∈ ℕ0)
1817a1i 9 . . . 4 ((𝑁 ∈ ℤ ∧ 0 ≤ 𝑁) → (𝑁 = 0 → 𝑁 ∈ ℕ0))
19 nnnn0 9200 . . . . 5 (𝑁 ∈ ℕ → 𝑁 ∈ ℕ0)
2019a1i 9 . . . 4 ((𝑁 ∈ ℤ ∧ 0 ≤ 𝑁) → (𝑁 ∈ ℕ → 𝑁 ∈ ℕ0))
21 simpr 110 . . . . . . 7 ((𝑁 ∈ ℤ ∧ 0 ≤ 𝑁) → 0 ≤ 𝑁)
22 0red 7975 . . . . . . . 8 ((𝑁 ∈ ℤ ∧ 0 ≤ 𝑁) → 0 ∈ ℝ)
23 zre 9274 . . . . . . . . 9 (𝑁 ∈ ℤ → 𝑁 ∈ ℝ)
2423adantr 276 . . . . . . . 8 ((𝑁 ∈ ℤ ∧ 0 ≤ 𝑁) → 𝑁 ∈ ℝ)
2522, 24lenltd 8092 . . . . . . 7 ((𝑁 ∈ ℤ ∧ 0 ≤ 𝑁) → (0 ≤ 𝑁 ↔ ¬ 𝑁 < 0))
2621, 25mpbid 147 . . . . . 6 ((𝑁 ∈ ℤ ∧ 0 ≤ 𝑁) → ¬ 𝑁 < 0)
27 nngt0 8961 . . . . . . 7 (-𝑁 ∈ ℕ → 0 < -𝑁)
2824lt0neg1d 8489 . . . . . . 7 ((𝑁 ∈ ℤ ∧ 0 ≤ 𝑁) → (𝑁 < 0 ↔ 0 < -𝑁))
2927, 28imbitrrid 156 . . . . . 6 ((𝑁 ∈ ℤ ∧ 0 ≤ 𝑁) → (-𝑁 ∈ ℕ → 𝑁 < 0))
3026, 29mtod 664 . . . . 5 ((𝑁 ∈ ℤ ∧ 0 ≤ 𝑁) → ¬ -𝑁 ∈ ℕ)
3130pm2.21d 620 . . . 4 ((𝑁 ∈ ℤ ∧ 0 ≤ 𝑁) → (-𝑁 ∈ ℕ → 𝑁 ∈ ℕ0))
3218, 20, 313jaod 1314 . . 3 ((𝑁 ∈ ℤ ∧ 0 ≤ 𝑁) → ((𝑁 = 0 ∨ 𝑁 ∈ ℕ ∨ -𝑁 ∈ ℕ) → 𝑁 ∈ ℕ0))
3314, 32mpd 13 . 2 ((𝑁 ∈ ℤ ∧ 0 ≤ 𝑁) → 𝑁 ∈ ℕ0)
3412, 33impbii 126 1 (𝑁 ∈ ℕ0 ↔ (𝑁 ∈ ℤ ∧ 0 ≤ 𝑁))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 104  wb 105  wo 709  w3o 978   = wceq 1363  wcel 2159   class class class wbr 4017  cr 7827  0cc0 7828   < clt 8009  cle 8010  -cneg 8146  cn 8936  0cn0 9193  cz 9270
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 710  ax-5 1457  ax-7 1458  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-8 1514  ax-10 1515  ax-11 1516  ax-i12 1517  ax-bndl 1519  ax-4 1520  ax-17 1536  ax-i9 1540  ax-ial 1544  ax-i5r 1545  ax-13 2161  ax-14 2162  ax-ext 2170  ax-sep 4135  ax-pow 4188  ax-pr 4223  ax-un 4447  ax-setind 4550  ax-cnex 7919  ax-resscn 7920  ax-1cn 7921  ax-1re 7922  ax-icn 7923  ax-addcl 7924  ax-addrcl 7925  ax-mulcl 7926  ax-addcom 7928  ax-addass 7930  ax-distr 7932  ax-i2m1 7933  ax-0lt1 7934  ax-0id 7936  ax-rnegex 7937  ax-cnre 7939  ax-pre-ltirr 7940  ax-pre-ltwlin 7941  ax-pre-lttrn 7942  ax-pre-ltadd 7944
This theorem depends on definitions:  df-bi 117  df-3or 980  df-3an 981  df-tru 1366  df-fal 1369  df-nf 1471  df-sb 1773  df-eu 2040  df-mo 2041  df-clab 2175  df-cleq 2181  df-clel 2184  df-nfc 2320  df-ne 2360  df-nel 2455  df-ral 2472  df-rex 2473  df-reu 2474  df-rab 2476  df-v 2753  df-sbc 2977  df-dif 3145  df-un 3147  df-in 3149  df-ss 3156  df-pw 3591  df-sn 3612  df-pr 3613  df-op 3615  df-uni 3824  df-int 3859  df-br 4018  df-opab 4079  df-id 4307  df-xp 4646  df-rel 4647  df-cnv 4648  df-co 4649  df-dm 4650  df-iota 5192  df-fun 5232  df-fv 5238  df-riota 5846  df-ov 5893  df-oprab 5894  df-mpo 5895  df-pnf 8011  df-mnf 8012  df-xr 8013  df-ltxr 8014  df-le 8015  df-sub 8147  df-neg 8148  df-inn 8937  df-n0 9194  df-z 9271
This theorem is referenced by:  nn0zrab  9295  znn0sub  9335  nn0ind  9384  fnn0ind  9386  fznn0  10130  elfz0ubfz0  10142  elfz0fzfz0  10143  fz0fzelfz0  10144  elfzmlbp  10149  difelfzle  10151  difelfznle  10152  elfzo0z  10201  fzofzim  10205  ubmelm1fzo  10243  flqge0nn0  10310  zmodcl  10361  modqmuladdnn0  10385  modsumfzodifsn  10413  uzennn  10453  zsqcl2  10615  nn0abscl  11111  geolim2  11537  cvgratnnlemabsle  11552  oexpneg  11899  oddnn02np1  11902  evennn02n  11904  nn0ehalf  11925  nn0oddm1d2  11931  divalgb  11947  dfgcd2  12032  uzwodc  12055  algcvga  12068  hashgcdlem  12255  pockthlem  12371  ennnfoneleminc  12429
  Copyright terms: Public domain W3C validator