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

Theorem elnnz 12568
Description: Positive integer property expressed in terms of integers. (Contributed by NM, 8-Jan-2002.)
Assertion
Ref Expression
elnnz (𝑁 ∈ ℕ ↔ (𝑁 ∈ ℤ ∧ 0 < 𝑁))

Proof of Theorem elnnz
StepHypRef Expression
1 nnre 12219 . . . 4 (𝑁 ∈ ℕ → 𝑁 ∈ ℝ)
2 orc 866 . . . 4 (𝑁 ∈ ℕ → (𝑁 ∈ ℕ ∨ (-𝑁 ∈ ℕ ∨ 𝑁 = 0)))
3 nngt0 12243 . . . 4 (𝑁 ∈ ℕ → 0 < 𝑁)
41, 2, 3jca31 516 . . 3 (𝑁 ∈ ℕ → ((𝑁 ∈ ℝ ∧ (𝑁 ∈ ℕ ∨ (-𝑁 ∈ ℕ ∨ 𝑁 = 0))) ∧ 0 < 𝑁))
5 idd 24 . . . . . . 7 ((𝑁 ∈ ℝ ∧ 0 < 𝑁) → (𝑁 ∈ ℕ → 𝑁 ∈ ℕ))
6 lt0neg2 11721 . . . . . . . . . . . 12 (𝑁 ∈ ℝ → (0 < 𝑁 ↔ -𝑁 < 0))
7 renegcl 11523 . . . . . . . . . . . . 13 (𝑁 ∈ ℝ → -𝑁 ∈ ℝ)
8 0re 11216 . . . . . . . . . . . . 13 0 ∈ ℝ
9 ltnsym 11312 . . . . . . . . . . . . 13 ((-𝑁 ∈ ℝ ∧ 0 ∈ ℝ) → (-𝑁 < 0 → ¬ 0 < -𝑁))
107, 8, 9sylancl 587 . . . . . . . . . . . 12 (𝑁 ∈ ℝ → (-𝑁 < 0 → ¬ 0 < -𝑁))
116, 10sylbid 239 . . . . . . . . . . 11 (𝑁 ∈ ℝ → (0 < 𝑁 → ¬ 0 < -𝑁))
1211imp 408 . . . . . . . . . 10 ((𝑁 ∈ ℝ ∧ 0 < 𝑁) → ¬ 0 < -𝑁)
13 nngt0 12243 . . . . . . . . . 10 (-𝑁 ∈ ℕ → 0 < -𝑁)
1412, 13nsyl 140 . . . . . . . . 9 ((𝑁 ∈ ℝ ∧ 0 < 𝑁) → ¬ -𝑁 ∈ ℕ)
15 gt0ne0 11679 . . . . . . . . . 10 ((𝑁 ∈ ℝ ∧ 0 < 𝑁) → 𝑁 ≠ 0)
1615neneqd 2946 . . . . . . . . 9 ((𝑁 ∈ ℝ ∧ 0 < 𝑁) → ¬ 𝑁 = 0)
17 ioran 983 . . . . . . . . 9 (¬ (-𝑁 ∈ ℕ ∨ 𝑁 = 0) ↔ (¬ -𝑁 ∈ ℕ ∧ ¬ 𝑁 = 0))
1814, 16, 17sylanbrc 584 . . . . . . . 8 ((𝑁 ∈ ℝ ∧ 0 < 𝑁) → ¬ (-𝑁 ∈ ℕ ∨ 𝑁 = 0))
1918pm2.21d 121 . . . . . . 7 ((𝑁 ∈ ℝ ∧ 0 < 𝑁) → ((-𝑁 ∈ ℕ ∨ 𝑁 = 0) → 𝑁 ∈ ℕ))
205, 19jaod 858 . . . . . 6 ((𝑁 ∈ ℝ ∧ 0 < 𝑁) → ((𝑁 ∈ ℕ ∨ (-𝑁 ∈ ℕ ∨ 𝑁 = 0)) → 𝑁 ∈ ℕ))
2120ex 414 . . . . 5 (𝑁 ∈ ℝ → (0 < 𝑁 → ((𝑁 ∈ ℕ ∨ (-𝑁 ∈ ℕ ∨ 𝑁 = 0)) → 𝑁 ∈ ℕ)))
2221com23 86 . . . 4 (𝑁 ∈ ℝ → ((𝑁 ∈ ℕ ∨ (-𝑁 ∈ ℕ ∨ 𝑁 = 0)) → (0 < 𝑁𝑁 ∈ ℕ)))
2322imp31 419 . . 3 (((𝑁 ∈ ℝ ∧ (𝑁 ∈ ℕ ∨ (-𝑁 ∈ ℕ ∨ 𝑁 = 0))) ∧ 0 < 𝑁) → 𝑁 ∈ ℕ)
244, 23impbii 208 . 2 (𝑁 ∈ ℕ ↔ ((𝑁 ∈ ℝ ∧ (𝑁 ∈ ℕ ∨ (-𝑁 ∈ ℕ ∨ 𝑁 = 0))) ∧ 0 < 𝑁))
25 elz 12560 . . . 4 (𝑁 ∈ ℤ ↔ (𝑁 ∈ ℝ ∧ (𝑁 = 0 ∨ 𝑁 ∈ ℕ ∨ -𝑁 ∈ ℕ)))
26 3orrot 1093 . . . . . 6 ((𝑁 = 0 ∨ 𝑁 ∈ ℕ ∨ -𝑁 ∈ ℕ) ↔ (𝑁 ∈ ℕ ∨ -𝑁 ∈ ℕ ∨ 𝑁 = 0))
27 3orass 1091 . . . . . 6 ((𝑁 ∈ ℕ ∨ -𝑁 ∈ ℕ ∨ 𝑁 = 0) ↔ (𝑁 ∈ ℕ ∨ (-𝑁 ∈ ℕ ∨ 𝑁 = 0)))
2826, 27bitri 275 . . . . 5 ((𝑁 = 0 ∨ 𝑁 ∈ ℕ ∨ -𝑁 ∈ ℕ) ↔ (𝑁 ∈ ℕ ∨ (-𝑁 ∈ ℕ ∨ 𝑁 = 0)))
2928anbi2i 624 . . . 4 ((𝑁 ∈ ℝ ∧ (𝑁 = 0 ∨ 𝑁 ∈ ℕ ∨ -𝑁 ∈ ℕ)) ↔ (𝑁 ∈ ℝ ∧ (𝑁 ∈ ℕ ∨ (-𝑁 ∈ ℕ ∨ 𝑁 = 0))))
3025, 29bitri 275 . . 3 (𝑁 ∈ ℤ ↔ (𝑁 ∈ ℝ ∧ (𝑁 ∈ ℕ ∨ (-𝑁 ∈ ℕ ∨ 𝑁 = 0))))
3130anbi1i 625 . 2 ((𝑁 ∈ ℤ ∧ 0 < 𝑁) ↔ ((𝑁 ∈ ℝ ∧ (𝑁 ∈ ℕ ∨ (-𝑁 ∈ ℕ ∨ 𝑁 = 0))) ∧ 0 < 𝑁))
3224, 31bitr4i 278 1 (𝑁 ∈ ℕ ↔ (𝑁 ∈ ℤ ∧ 0 < 𝑁))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 397  wo 846  w3o 1087   = wceq 1542  wcel 2107   class class class wbr 5149  cr 11109  0cc0 11110   < clt 11248  -cneg 11445  cn 12212  cz 12558
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7725  ax-resscn 11167  ax-1cn 11168  ax-icn 11169  ax-addcl 11170  ax-addrcl 11171  ax-mulcl 11172  ax-mulrcl 11173  ax-mulcom 11174  ax-addass 11175  ax-mulass 11176  ax-distr 11177  ax-i2m1 11178  ax-1ne0 11179  ax-1rid 11180  ax-rnegex 11181  ax-rrecex 11182  ax-cnre 11183  ax-pre-lttri 11184  ax-pre-lttrn 11185  ax-pre-ltadd 11186  ax-pre-mulgt0 11187
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-iun 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-pred 6301  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-riota 7365  df-ov 7412  df-oprab 7413  df-mpo 7414  df-om 7856  df-2nd 7976  df-frecs 8266  df-wrecs 8297  df-recs 8371  df-rdg 8410  df-er 8703  df-en 8940  df-dom 8941  df-sdom 8942  df-pnf 11250  df-mnf 11251  df-xr 11252  df-ltxr 11253  df-le 11254  df-sub 11446  df-neg 11447  df-nn 12213  df-z 12559
This theorem is referenced by:  elnn0z  12571  elnnz1  12588  znnsub  12608  nn0ge0div  12631  msqznn  12644  elpq  12959  lbfzo0  13672  elfzo0z  13674  fzofzim  13679  fzo1fzo0n0  13683  elfzodifsumelfzo  13698  elfznelfzo  13737  nnesq  14190  swrdlsw  14617  pfxccatin12lem3  14682  repswswrd  14734  cshwcsh2id  14779  swrd2lsw  14903  2swrd2eqwrdeq  14904  nnabscl  15272  iseralt  15631  sqrt2irrlem  16191  p1modz1  16204  nndivdvds  16206  oddge22np1  16292  evennn2n  16294  nno  16325  nnoddm1d2  16329  ndvdsadd  16353  bitsfzolem  16375  sqgcd  16502  qredeu  16595  prmind2  16622  qgt0numnn  16687  oddprm  16743  pythagtriplem6  16754  pythagtriplem11  16758  pythagtriplem13  16760  pythagtriplem19  16766  pc2dvds  16812  pcadd  16822  prmreclem3  16851  4sqlem11  16888  4sqlem12  16889  prmgaplem7  16990  cshwshashlem2  17030  subgmulg  19020  znidomb  21117  sgmnncl  26651  muinv  26697  mersenne  26730  bposlem6  26792  gausslemma2dlem1a  26868  lgseisenlem1  26878  lgsquadlem1  26883  lgsquadlem2  26884  2sqlem8  26929  2sqnn0  26941  dchrisum0flblem2  27012  clwlkclwwlklem2a2  29246  clwlkclwwlklem2a4  29250  clwlkclwwlklem2a  29251  eucrct2eupth1  29497  nn0prpwlem  35207  poimirlem7  36495  poimirlem29  36517  mblfinlem2  36526  lcmineqlem15  40908  lcmineqlem23  40916  aks4d1lem1  40927  aks4d1p1p2  40935  aks4d1p1  40941  aks4d1p2  40942  aks4d1p3  40943  aks4d1p5  40945  aks4d1p6  40946  aks4d1p7d1  40947  aks4d1p8  40952  2ap1caineq  40961  posqsqznn  41234  rtprmirr  41237  dffltz  41376  irrapxlem4  41563  rmspecnonsq  41645  rmynn  41695  jm2.24  41702  jm2.23  41735  jm2.20nn  41736  jm2.27a  41744  jm2.27c  41746  rmydioph  41753  jm3.1lem3  41758  sumnnodd  44346  dvnxpaek  44658  dirkertrigeqlem3  44816  fourierdlem47  44869  fouriersw  44947  etransclem15  44965  etransclem24  44974  etransclem25  44975  etransclem35  44985  etransclem48  44998  zm1nn  46010  iccpartigtl  46091  nnoALTV  46363  nneven  46366  ztprmneprm  47023  blennngt2o2  47278
  Copyright terms: Public domain W3C validator