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

Theorem elnnz 12564
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 12215 . . . 4 (𝑁 ∈ ℕ → 𝑁 ∈ ℝ)
2 orc 865 . . . 4 (𝑁 ∈ ℕ → (𝑁 ∈ ℕ ∨ (-𝑁 ∈ ℕ ∨ 𝑁 = 0)))
3 nngt0 12239 . . . 4 (𝑁 ∈ ℕ → 0 < 𝑁)
41, 2, 3jca31 515 . . 3 (𝑁 ∈ ℕ → ((𝑁 ∈ ℝ ∧ (𝑁 ∈ ℕ ∨ (-𝑁 ∈ ℕ ∨ 𝑁 = 0))) ∧ 0 < 𝑁))
5 idd 24 . . . . . . 7 ((𝑁 ∈ ℝ ∧ 0 < 𝑁) → (𝑁 ∈ ℕ → 𝑁 ∈ ℕ))
6 lt0neg2 11717 . . . . . . . . . . . 12 (𝑁 ∈ ℝ → (0 < 𝑁 ↔ -𝑁 < 0))
7 renegcl 11519 . . . . . . . . . . . . 13 (𝑁 ∈ ℝ → -𝑁 ∈ ℝ)
8 0re 11212 . . . . . . . . . . . . 13 0 ∈ ℝ
9 ltnsym 11308 . . . . . . . . . . . . 13 ((-𝑁 ∈ ℝ ∧ 0 ∈ ℝ) → (-𝑁 < 0 → ¬ 0 < -𝑁))
107, 8, 9sylancl 586 . . . . . . . . . . . 12 (𝑁 ∈ ℝ → (-𝑁 < 0 → ¬ 0 < -𝑁))
116, 10sylbid 239 . . . . . . . . . . 11 (𝑁 ∈ ℝ → (0 < 𝑁 → ¬ 0 < -𝑁))
1211imp 407 . . . . . . . . . 10 ((𝑁 ∈ ℝ ∧ 0 < 𝑁) → ¬ 0 < -𝑁)
13 nngt0 12239 . . . . . . . . . 10 (-𝑁 ∈ ℕ → 0 < -𝑁)
1412, 13nsyl 140 . . . . . . . . 9 ((𝑁 ∈ ℝ ∧ 0 < 𝑁) → ¬ -𝑁 ∈ ℕ)
15 gt0ne0 11675 . . . . . . . . . 10 ((𝑁 ∈ ℝ ∧ 0 < 𝑁) → 𝑁 ≠ 0)
1615neneqd 2945 . . . . . . . . 9 ((𝑁 ∈ ℝ ∧ 0 < 𝑁) → ¬ 𝑁 = 0)
17 ioran 982 . . . . . . . . 9 (¬ (-𝑁 ∈ ℕ ∨ 𝑁 = 0) ↔ (¬ -𝑁 ∈ ℕ ∧ ¬ 𝑁 = 0))
1814, 16, 17sylanbrc 583 . . . . . . . 8 ((𝑁 ∈ ℝ ∧ 0 < 𝑁) → ¬ (-𝑁 ∈ ℕ ∨ 𝑁 = 0))
1918pm2.21d 121 . . . . . . 7 ((𝑁 ∈ ℝ ∧ 0 < 𝑁) → ((-𝑁 ∈ ℕ ∨ 𝑁 = 0) → 𝑁 ∈ ℕ))
205, 19jaod 857 . . . . . 6 ((𝑁 ∈ ℝ ∧ 0 < 𝑁) → ((𝑁 ∈ ℕ ∨ (-𝑁 ∈ ℕ ∨ 𝑁 = 0)) → 𝑁 ∈ ℕ))
2120ex 413 . . . . 5 (𝑁 ∈ ℝ → (0 < 𝑁 → ((𝑁 ∈ ℕ ∨ (-𝑁 ∈ ℕ ∨ 𝑁 = 0)) → 𝑁 ∈ ℕ)))
2221com23 86 . . . 4 (𝑁 ∈ ℝ → ((𝑁 ∈ ℕ ∨ (-𝑁 ∈ ℕ ∨ 𝑁 = 0)) → (0 < 𝑁𝑁 ∈ ℕ)))
2322imp31 418 . . 3 (((𝑁 ∈ ℝ ∧ (𝑁 ∈ ℕ ∨ (-𝑁 ∈ ℕ ∨ 𝑁 = 0))) ∧ 0 < 𝑁) → 𝑁 ∈ ℕ)
244, 23impbii 208 . 2 (𝑁 ∈ ℕ ↔ ((𝑁 ∈ ℝ ∧ (𝑁 ∈ ℕ ∨ (-𝑁 ∈ ℕ ∨ 𝑁 = 0))) ∧ 0 < 𝑁))
25 elz 12556 . . . 4 (𝑁 ∈ ℤ ↔ (𝑁 ∈ ℝ ∧ (𝑁 = 0 ∨ 𝑁 ∈ ℕ ∨ -𝑁 ∈ ℕ)))
26 3orrot 1092 . . . . . 6 ((𝑁 = 0 ∨ 𝑁 ∈ ℕ ∨ -𝑁 ∈ ℕ) ↔ (𝑁 ∈ ℕ ∨ -𝑁 ∈ ℕ ∨ 𝑁 = 0))
27 3orass 1090 . . . . . 6 ((𝑁 ∈ ℕ ∨ -𝑁 ∈ ℕ ∨ 𝑁 = 0) ↔ (𝑁 ∈ ℕ ∨ (-𝑁 ∈ ℕ ∨ 𝑁 = 0)))
2826, 27bitri 274 . . . . 5 ((𝑁 = 0 ∨ 𝑁 ∈ ℕ ∨ -𝑁 ∈ ℕ) ↔ (𝑁 ∈ ℕ ∨ (-𝑁 ∈ ℕ ∨ 𝑁 = 0)))
2928anbi2i 623 . . . 4 ((𝑁 ∈ ℝ ∧ (𝑁 = 0 ∨ 𝑁 ∈ ℕ ∨ -𝑁 ∈ ℕ)) ↔ (𝑁 ∈ ℝ ∧ (𝑁 ∈ ℕ ∨ (-𝑁 ∈ ℕ ∨ 𝑁 = 0))))
3025, 29bitri 274 . . 3 (𝑁 ∈ ℤ ↔ (𝑁 ∈ ℝ ∧ (𝑁 ∈ ℕ ∨ (-𝑁 ∈ ℕ ∨ 𝑁 = 0))))
3130anbi1i 624 . 2 ((𝑁 ∈ ℤ ∧ 0 < 𝑁) ↔ ((𝑁 ∈ ℝ ∧ (𝑁 ∈ ℕ ∨ (-𝑁 ∈ ℕ ∨ 𝑁 = 0))) ∧ 0 < 𝑁))
3224, 31bitr4i 277 1 (𝑁 ∈ ℕ ↔ (𝑁 ∈ ℤ ∧ 0 < 𝑁))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396  wo 845  w3o 1086   = wceq 1541  wcel 2106   class class class wbr 5147  cr 11105  0cc0 11106   < clt 11244  -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-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7721  ax-resscn 11163  ax-1cn 11164  ax-icn 11165  ax-addcl 11166  ax-addrcl 11167  ax-mulcl 11168  ax-mulrcl 11169  ax-mulcom 11170  ax-addass 11171  ax-mulass 11172  ax-distr 11173  ax-i2m1 11174  ax-1ne0 11175  ax-1rid 11176  ax-rnegex 11177  ax-rrecex 11178  ax-cnre 11179  ax-pre-lttri 11180  ax-pre-lttrn 11181  ax-pre-ltadd 11182  ax-pre-mulgt0 11183
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-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6297  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-riota 7361  df-ov 7408  df-oprab 7409  df-mpo 7410  df-om 7852  df-2nd 7972  df-frecs 8262  df-wrecs 8293  df-recs 8367  df-rdg 8406  df-er 8699  df-en 8936  df-dom 8937  df-sdom 8938  df-pnf 11246  df-mnf 11247  df-xr 11248  df-ltxr 11249  df-le 11250  df-sub 11442  df-neg 11443  df-nn 12209  df-z 12555
This theorem is referenced by:  elnn0z  12567  elnnz1  12584  znnsub  12604  nn0ge0div  12627  msqznn  12640  elpq  12955  lbfzo0  13668  elfzo0z  13670  fzofzim  13675  fzo1fzo0n0  13679  elfzodifsumelfzo  13694  elfznelfzo  13733  nnesq  14186  swrdlsw  14613  pfxccatin12lem3  14678  repswswrd  14730  cshwcsh2id  14775  swrd2lsw  14899  2swrd2eqwrdeq  14900  nnabscl  15268  iseralt  15627  sqrt2irrlem  16187  p1modz1  16200  nndivdvds  16202  oddge22np1  16288  evennn2n  16290  nno  16321  nnoddm1d2  16325  ndvdsadd  16349  bitsfzolem  16371  sqgcd  16498  qredeu  16591  prmind2  16618  qgt0numnn  16683  oddprm  16739  pythagtriplem6  16750  pythagtriplem11  16754  pythagtriplem13  16756  pythagtriplem19  16762  pc2dvds  16808  pcadd  16818  prmreclem3  16847  4sqlem11  16884  4sqlem12  16885  prmgaplem7  16986  cshwshashlem2  17026  subgmulg  19014  znidomb  21108  sgmnncl  26640  muinv  26686  mersenne  26719  bposlem6  26781  gausslemma2dlem1a  26857  lgseisenlem1  26867  lgsquadlem1  26872  lgsquadlem2  26873  2sqlem8  26918  2sqnn0  26930  dchrisum0flblem2  27001  clwlkclwwlklem2a2  29235  clwlkclwwlklem2a4  29239  clwlkclwwlklem2a  29240  eucrct2eupth1  29486  nn0prpwlem  35195  poimirlem7  36483  poimirlem29  36505  mblfinlem2  36514  lcmineqlem15  40896  lcmineqlem23  40904  aks4d1lem1  40915  aks4d1p1p2  40923  aks4d1p1  40929  aks4d1p2  40930  aks4d1p3  40931  aks4d1p5  40933  aks4d1p6  40934  aks4d1p7d1  40935  aks4d1p8  40940  2ap1caineq  40949  posqsqznn  41229  rtprmirr  41233  dffltz  41372  irrapxlem4  41548  rmspecnonsq  41630  rmynn  41680  jm2.24  41687  jm2.23  41720  jm2.20nn  41721  jm2.27a  41729  jm2.27c  41731  rmydioph  41738  jm3.1lem3  41743  sumnnodd  44332  dvnxpaek  44644  dirkertrigeqlem3  44802  fourierdlem47  44855  fouriersw  44933  etransclem15  44951  etransclem24  44960  etransclem25  44961  etransclem35  44971  etransclem48  44984  zm1nn  45996  iccpartigtl  46077  nnoALTV  46349  nneven  46352  ztprmneprm  46976  blennngt2o2  47231
  Copyright terms: Public domain W3C validator