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

Theorem elnn0z 10978
Description: Nonnegative integer property expressed in terms of integers. (Contributed by NM, 9-May-2004.)
Assertion
Ref Expression
elnn0z  |-  ( N  e.  NN0  <->  ( N  e.  ZZ  /\  0  <_  N ) )

Proof of Theorem elnn0z
StepHypRef Expression
1 elnn0 10899 . 2  |-  ( N  e.  NN0  <->  ( N  e.  NN  \/  N  =  0 ) )
2 elnnz 10975 . . 3  |-  ( N  e.  NN  <->  ( N  e.  ZZ  /\  0  < 
N ) )
3 eqcom 2468 . . 3  |-  ( N  =  0  <->  0  =  N )
42, 3orbi12i 528 . 2  |-  ( ( N  e.  NN  \/  N  =  0 )  <-> 
( ( N  e.  ZZ  /\  0  < 
N )  \/  0  =  N ) )
5 id 22 . . . . . 6  |-  ( N  e.  ZZ  ->  N  e.  ZZ )
6 0z 10976 . . . . . . 7  |-  0  e.  ZZ
7 eleq1 2527 . . . . . . 7  |-  ( 0  =  N  ->  (
0  e.  ZZ  <->  N  e.  ZZ ) )
86, 7mpbii 216 . . . . . 6  |-  ( 0  =  N  ->  N  e.  ZZ )
95, 8jaoi 385 . . . . 5  |-  ( ( N  e.  ZZ  \/  0  =  N )  ->  N  e.  ZZ )
10 orc 391 . . . . 5  |-  ( N  e.  ZZ  ->  ( N  e.  ZZ  \/  0  =  N )
)
119, 10impbii 192 . . . 4  |-  ( ( N  e.  ZZ  \/  0  =  N )  <->  N  e.  ZZ )
1211anbi1i 706 . . 3  |-  ( ( ( N  e.  ZZ  \/  0  =  N
)  /\  ( 0  <  N  \/  0  =  N ) )  <-> 
( N  e.  ZZ  /\  ( 0  <  N  \/  0  =  N
) ) )
13 ordir 881 . . 3  |-  ( ( ( N  e.  ZZ  /\  0  <  N )  \/  0  =  N )  <->  ( ( N  e.  ZZ  \/  0  =  N )  /\  ( 0  <  N  \/  0  =  N
) ) )
14 0re 9668 . . . . 5  |-  0  e.  RR
15 zre 10969 . . . . 5  |-  ( N  e.  ZZ  ->  N  e.  RR )
16 leloe 9745 . . . . 5  |-  ( ( 0  e.  RR  /\  N  e.  RR )  ->  ( 0  <_  N  <->  ( 0  <  N  \/  0  =  N )
) )
1714, 15, 16sylancr 674 . . . 4  |-  ( N  e.  ZZ  ->  (
0  <_  N  <->  ( 0  <  N  \/  0  =  N ) ) )
1817pm5.32i 647 . . 3  |-  ( ( N  e.  ZZ  /\  0  <_  N )  <->  ( N  e.  ZZ  /\  ( 0  <  N  \/  0  =  N ) ) )
1912, 13, 183bitr4i 285 . 2  |-  ( ( ( N  e.  ZZ  /\  0  <  N )  \/  0  =  N )  <->  ( N  e.  ZZ  /\  0  <_  N ) )
201, 4, 193bitri 279 1  |-  ( N  e.  NN0  <->  ( N  e.  ZZ  /\  0  <_  N ) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 189    \/ wo 374    /\ wa 375    = wceq 1454    e. wcel 1897   class class class wbr 4415   RRcr 9563   0cc0 9564    < clt 9700    <_ cle 9701   NNcn 10636   NN0cn0 10897   ZZcz 10965
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-8 1899  ax-9 1906  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441  ax-sep 4538  ax-nul 4547  ax-pow 4594  ax-pr 4652  ax-un 6609  ax-resscn 9621  ax-1cn 9622  ax-icn 9623  ax-addcl 9624  ax-addrcl 9625  ax-mulcl 9626  ax-mulrcl 9627  ax-mulcom 9628  ax-addass 9629  ax-mulass 9630  ax-distr 9631  ax-i2m1 9632  ax-1ne0 9633  ax-1rid 9634  ax-rnegex 9635  ax-rrecex 9636  ax-cnre 9637  ax-pre-lttri 9638  ax-pre-lttrn 9639  ax-pre-ltadd 9640  ax-pre-mulgt0 9641
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 992  df-3an 993  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-eu 2313  df-mo 2314  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2591  df-ne 2634  df-nel 2635  df-ral 2753  df-rex 2754  df-reu 2755  df-rab 2757  df-v 3058  df-sbc 3279  df-csb 3375  df-dif 3418  df-un 3420  df-in 3422  df-ss 3429  df-pss 3431  df-nul 3743  df-if 3893  df-pw 3964  df-sn 3980  df-pr 3982  df-tp 3984  df-op 3986  df-uni 4212  df-iun 4293  df-br 4416  df-opab 4475  df-mpt 4476  df-tr 4511  df-eprel 4763  df-id 4767  df-po 4773  df-so 4774  df-fr 4811  df-we 4813  df-xp 4858  df-rel 4859  df-cnv 4860  df-co 4861  df-dm 4862  df-rn 4863  df-res 4864  df-ima 4865  df-pred 5398  df-ord 5444  df-on 5445  df-lim 5446  df-suc 5447  df-iota 5564  df-fun 5602  df-fn 5603  df-f 5604  df-f1 5605  df-fo 5606  df-f1o 5607  df-fv 5608  df-riota 6276  df-ov 6317  df-oprab 6318  df-mpt2 6319  df-om 6719  df-wrecs 7053  df-recs 7115  df-rdg 7153  df-er 7388  df-en 7595  df-dom 7596  df-sdom 7597  df-pnf 9702  df-mnf 9703  df-xr 9704  df-ltxr 9705  df-le 9706  df-sub 9887  df-neg 9888  df-nn 10637  df-n0 10898  df-z 10966
This theorem is referenced by:  nn0zrab  10994  znn0sub  11012  nn0ind  11058  fnn0ind  11062  fznn0  11914  elfz0ubfz0  11923  elfz0fzfz0  11924  fz0fzelfz0  11925  elfzmlbp  11931  difelfzle  11933  difelfznle  11934  elfzo0z  11988  fzofzim  11992  ubmelm1fzo  12037  flge0nn0  12085  zmodcl  12147  zsqcl2  12383  swrdswrdlem  12851  swrdswrd  12852  swrdccatin2  12879  swrdccatin12lem2  12881  swrdccatin12lem3  12882  repswswrd  12923  cshwidxmod  12941  nn0abscl  13423  iseralt  13799  binomrisefac  14143  oexpneg  14416  divalglem2  14421  divalglem2OLD  14422  divalglem8  14428  divalglem10  14431  divalgb  14433  bitsinv1lem  14463  algcvga  14586  iserodd  14833  pockthlem  14897  4sqlem14OLD  14950  4sqlem14  14956  cshwshashlem2  15115  chfacfscmul0  19930  chfacfpmmul0  19934  taylfvallem1  23360  tayl0  23365  leibpilem1  23914  basellem3  24057  bcmono  24253  clwlkisclwwlklem2a1  25555  clwlkisclwwlklem2fv2  25559  clwlkisclwwlklem2a  25561  wwlksubclwwlk  25580  irrapxlem1  35710  rmynn0  35851  rmyabs  35852  jm2.22  35894  jm2.23  35895  jm2.27a  35904  jm2.27c  35906  hashgcdlem  36118  dvnprodlem1  37858  wallispilem4  37967  stirlinglem5  37977  elaa2lem  38134  elaa2lemOLD  38135  etransclem3  38139  etransclem7  38143  etransclem10  38146  etransclem19  38155  etransclem20  38156  etransclem21  38157  etransclem22  38158  etransclem24  38160  etransclem27  38163  oexpnegALTV  38843  nn0oALTV  38862  nn0e  38863  pfxccatin12lem2  39004  zm1nn  39090  lesubnn0  39091  eluzge0nn0  39094  elfz2z  39096  2elfz2melfz  39099  subsubelfzo0  39103  nn0eo  40607  dig1  40691
  Copyright terms: Public domain W3C validator