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

Theorem 1nn 10627
Description: Peano postulate: 1 is a positive integer. (Contributed by NM, 11-Jan-1997.) (Revised by Mario Carneiro, 17-Nov-2014.)
Assertion
Ref Expression
1nn  |-  1  e.  NN

Proof of Theorem 1nn
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 1ex 9645 . . . 4  |-  1  e.  _V
2 fr0g 7164 . . . 4  |-  ( 1  e.  _V  ->  (
( rec ( ( x  e.  _V  |->  ( x  +  1 ) ) ,  1 )  |`  om ) `  (/) )  =  1 )
31, 2ax-mp 5 . . 3  |-  ( ( rec ( ( x  e.  _V  |->  ( x  +  1 ) ) ,  1 )  |`  om ) `  (/) )  =  1
4 frfnom 7163 . . . 4  |-  ( rec ( ( x  e. 
_V  |->  ( x  + 
1 ) ) ,  1 )  |`  om )  Fn  om
5 peano1 6726 . . . 4  |-  (/)  e.  om
6 fnfvelrn 6034 . . . 4  |-  ( ( ( rec ( ( x  e.  _V  |->  ( x  +  1 ) ) ,  1 )  |`  om )  Fn  om  /\  (/)  e.  om )  -> 
( ( rec (
( x  e.  _V  |->  ( x  +  1
) ) ,  1 )  |`  om ) `  (/) )  e.  ran  ( rec ( ( x  e.  _V  |->  ( x  +  1 ) ) ,  1 )  |`  om ) )
74, 5, 6mp2an 676 . . 3  |-  ( ( rec ( ( x  e.  _V  |->  ( x  +  1 ) ) ,  1 )  |`  om ) `  (/) )  e. 
ran  ( rec (
( x  e.  _V  |->  ( x  +  1
) ) ,  1 )  |`  om )
83, 7eqeltrri 2504 . 2  |-  1  e.  ran  ( rec (
( x  e.  _V  |->  ( x  +  1
) ) ,  1 )  |`  om )
9 df-nn 10617 . . 3  |-  NN  =  ( rec ( ( x  e.  _V  |->  ( x  +  1 ) ) ,  1 ) " om )
10 df-ima 4866 . . 3  |-  ( rec ( ( x  e. 
_V  |->  ( x  + 
1 ) ) ,  1 ) " om )  =  ran  ( rec ( ( x  e. 
_V  |->  ( x  + 
1 ) ) ,  1 )  |`  om )
119, 10eqtri 2451 . 2  |-  NN  =  ran  ( rec ( ( x  e.  _V  |->  ( x  +  1 ) ) ,  1 )  |`  om )
128, 11eleqtrri 2506 1  |-  1  e.  NN
Colors of variables: wff setvar class
Syntax hints:    = wceq 1437    e. wcel 1872   _Vcvv 3080   (/)c0 3761    |-> cmpt 4482   ran crn 4854    |` cres 4855   "cima 4856    Fn wfn 5596   ` cfv 5601  (class class class)co 6305   omcom 6706   reccrdg 7138   1c1 9547    + caddc 9549   NNcn 10616
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401  ax-sep 4546  ax-nul 4555  ax-pow 4602  ax-pr 4660  ax-un 6597  ax-1cn 9604
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2273  df-mo 2274  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-ne 2616  df-ral 2776  df-rex 2777  df-reu 2778  df-rab 2780  df-v 3082  df-sbc 3300  df-csb 3396  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-pss 3452  df-nul 3762  df-if 3912  df-pw 3983  df-sn 3999  df-pr 4001  df-tp 4003  df-op 4005  df-uni 4220  df-iun 4301  df-br 4424  df-opab 4483  df-mpt 4484  df-tr 4519  df-eprel 4764  df-id 4768  df-po 4774  df-so 4775  df-fr 4812  df-we 4814  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866  df-pred 5399  df-ord 5445  df-on 5446  df-lim 5447  df-suc 5448  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-om 6707  df-wrecs 7039  df-recs 7101  df-rdg 7139  df-nn 10617
This theorem is referenced by:  dfnn2  10629  dfnn3  10630  nnind  10634  nn1suc  10637  2nn  10774  nnunb  10872  1nn0  10892  nn0p1nn  10916  elz2  10961  1z  10974  neg1z  10980  nneo  11026  elnn1uz2  11242  zq  11277  rpnnen1lem4  11300  rpnnen1lem5  11301  ser1const  12275  exp1  12284  nnexpcl  12291  expnbnd  12407  fac1  12469  faccl  12475  faclbnd3  12483  faclbnd4lem1  12484  faclbnd4lem2  12485  faclbnd4lem3  12486  faclbnd4lem4  12487  lsw0  12716  eqs1  12752  ccat2s1p1  12763  cats1un  12834  revs1  12872  cats1fvn  12956  relexpsucnnl  13095  relexpaddg  13116  isercolllem2  13728  isercolllem3  13729  isercoll  13730  sumsn  13806  climcndslem1  13906  climcndslem2  13907  fprodnncl  14008  prodsn  14015  prodsnf  14017  nnrisefaccl  14071  eftlub  14162  eirrlem  14255  rpnnen2lem5  14270  rpnnen2lem8  14273  rpnnen2  14277  dvdsle  14349  n2dvds1  14353  ndvdsp1  14389  gcd1  14495  lcmslefacOLD  14585  1nprm  14628  1idssfct  14629  qden1elz  14705  phi1  14720  phiprm  14724  pcpre1  14791  pczpre  14796  pcmptcl  14835  pcmpt  14836  infpnlem2  14854  prmreclem1  14859  prmreclem6  14864  mul4sq  14897  vdwmc2  14928  vdwlem8  14937  vdwlem13  14942  vdwnnlem3  14946  prmocl  14991  prmop1  14995  fvprmselelfz  15001  fvprmselgcd1  15002  prmolefac  15003  prmodvdslcmf  15004  prmormapnnOLD  15013  prmorlefacOLD  15017  prmordvdslcmfOLD  15018  prmordvdslcmsOLDOLD  15020  prmgapprmo  15032  5prm  15079  7prm  15081  11prm  15085  13prm  15086  17prm  15087  19prm  15088  37prm  15091  43prm  15092  83prm  15093  139prm  15094  163prm  15095  317prm  15096  631prm  15097  1259lem4  15104  1259lem5  15105  1259prm  15106  2503lem3  15109  2503prm  15110  4001lem1  15111  4001lem2  15112  4001lem3  15113  4001lem4  15114  4001prm  15115  baseid  15168  basendx  15172  basendxnn  15173  ressval3d  15185  1strstr  15225  2strstr  15229  rngstr  15243  lmodstr  15260  topgrpstr  15285  otpsstr  15292  ocndx  15297  ocid  15298  ressds  15310  resshom  15315  ressco  15316  slotsbhcdif  15317  oppcbas  15622  rescbas  15733  rescabs  15737  catstr  15861  estrreslem1  16021  ipostr  16398  mulg1  16764  mulg2  16766  oppgbas  17001  od1  17209  gex1  17242  efgsval2  17382  efgsp1  17386  torsubg  17491  pgpfaclem1  17713  mgpbas  17728  mgpds  17732  opprbas  17856  srabase  18400  srads  18408  opsrbas  18701  zlmbas  19087  znbas2  19108  thlbas  19257  thlle  19258  pmatcollpw3fi1lem2  19809  hauspwdom  20514  ressunif  21275  tuslem  21280  imasdsf1olem  21386  setsmsds  21489  tmslem  21495  tnglem  21646  tngbas  21647  tngds  21654  bcthlem4  22293  bcth3  22297  ovolmge0  22428  ovollb2  22440  ovolctb  22441  ovolunlem1a  22447  ovolunlem1  22448  ovoliunlem1  22453  ovoliun  22456  ovoliun2  22457  ovolicc1  22467  voliunlem1  22501  volsup  22507  ioombl1lem2  22510  ioombl1lem4  22512  uniioombllem1  22536  uniioombllem2  22538  uniioombllem2OLD  22539  uniioombllem6  22544  itg1climres  22670  itg2seq  22698  itg2monolem1  22706  itg2monolem2  22707  itg2monolem3  22708  itg2mono  22709  itg2i1fseq2  22712  itg2cnlem1  22717  aalioulem5  23290  aaliou2b  23295  aaliou3lem4  23300  aaliou3lem7  23303  dcubic1lem  23767  dcubic2  23768  mcubic  23771  log2ub  23873  emcllem6  23924  emcllem7  23925  lgam1  23987  gam1  23988  ftalem7  24003  efnnfsumcl  24027  vmaprm  24042  efvmacl  24045  efchtdvds  24084  vma1  24091  prmorcht  24103  sqff1o  24107  pclogsum  24141  perfectlem1  24155  perfectlem2  24156  bpos1  24209  bposlem5  24214  lgsdir  24256  1lgs  24263  lgs1  24264  lgsquad2lem2  24285  dchrmusumlema  24329  dchrisum0lema  24350  trkgstr  24490  ttgbas  24905  ttgplusg  24906  ttgvsca  24908  eengstr  25008  usgraexmplef  25126  konigsberg  25713  gx1  25988  ipval2  26341  opsqrlem2  27792  ssnnssfz  28373  nnindf  28389  nn0min  28391  isarchi3  28511  resvbas  28603  rge0scvg  28763  zlmds  28776  qqh0  28796  qqh1  28797  esumfzf  28898  esumfsup  28899  esumpcvgval  28907  voliune  29060  eulerpartgbij  29213  eulerpartlemgs2  29221  fib2  29243  rrvsum  29295  ballotlem4  29339  ballotlemi1  29343  ballotlemii  29344  ballotlemic  29347  ballotlem1c  29348  ballotlemi1OLD  29381  ballotlemiiOLD  29382  ballotlemicOLD  29385  ballotlem1cOLD  29386  faclimlem1  30386  nn0prpwlem  30983  nn0prpw  30984  poimirlem32  31936  ovoliunnfl  31946  voliunnfl  31948  volsupnfl  31949  incsequz  32041  bfplem1  32118  rrncmslem  32128  hlhilsbase  35479  bezoutr1  35806  jm2.23  35821  rmydioph  35839  rmxdioph  35841  expdiophlem2  35847  expdioph  35848  relexp2  36239  iunrelexpmin1  36270  iunrelexpmin2  36274  dftrcl3  36282  fvtrcllb1d  36284  cotrcltrcl  36287  corcltrcl  36301  cotrclrcl  36304  prmunb2  36629  sumsnd  37320  sumsnf  37589  mccl  37618  sumnnodd  37650  wallispilem4  37870  wallispi2lem1  37873  wallispi2lem2  37874  stirlinglem8  37883  stirlinglem11  37886  stirlinglem12  37887  stirlinglem13  37888  fourierdlem31  37940  fourierdlem31OLD  37941  nnfoctbdjlem  38201  hoicvr  38274  hoicvrrex  38282  hoidmvlelem3  38323  ovnhoilem1  38327  ovnhoilem2  38328  iccpartlt  38608  perfectALTVlem1  38713  perfectALTVlem2  38714  nnsum3primesprm  38755  bgoldbtbndlem1  38770  tgblthelfgott  38778  3exp4mod41  38786  41prothprmlem2  38788  baseltedgf  38929  basvtxval  38947  nnsgrpmgm  39435  nnsgrpnmnd  39437  basendxnmulrndx  39573  blennn0elnn  40009  blen1  40016
  Copyright terms: Public domain W3C validator