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

Theorem 1nn 11223
 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 ∈ ℕ

Proof of Theorem 1nn
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 1ex 10227 . . . 4 1 ∈ V
2 fr0g 7700 . . . 4 (1 ∈ V → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘∅) = 1)
31, 2ax-mp 5 . . 3 ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘∅) = 1
4 frfnom 7699 . . . 4 (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω) Fn ω
5 peano1 7250 . . . 4 ∅ ∈ ω
6 fnfvelrn 6519 . . . 4 (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω) Fn ω ∧ ∅ ∈ ω) → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘∅) ∈ ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω))
74, 5, 6mp2an 710 . . 3 ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘∅) ∈ ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)
83, 7eqeltrri 2836 . 2 1 ∈ ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)
9 df-nn 11213 . . 3 ℕ = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) “ ω)
10 df-ima 5279 . . 3 (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) “ ω) = ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)
119, 10eqtri 2782 . 2 ℕ = ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)
128, 11eleqtrri 2838 1 1 ∈ ℕ
 Colors of variables: wff setvar class Syntax hints:   = wceq 1632   ∈ wcel 2139  Vcvv 3340  ∅c0 4058   ↦ cmpt 4881  ran crn 5267   ↾ cres 5268   “ cima 5269   Fn wfn 6044  ‘cfv 6049  (class class class)co 6813  ωcom 7230  reccrdg 7674  1c1 10129   + caddc 10131  ℕcn 11212 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-un 7114  ax-1cn 10186 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-ral 3055  df-rex 3056  df-reu 3057  df-rab 3059  df-v 3342  df-sbc 3577  df-csb 3675  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-pss 3731  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-tp 4326  df-op 4328  df-uni 4589  df-iun 4674  df-br 4805  df-opab 4865  df-mpt 4882  df-tr 4905  df-id 5174  df-eprel 5179  df-po 5187  df-so 5188  df-fr 5225  df-we 5227  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-pred 5841  df-ord 5887  df-on 5888  df-lim 5889  df-suc 5890  df-iota 6012  df-fun 6051  df-fn 6052  df-f 6053  df-f1 6054  df-fo 6055  df-f1o 6056  df-fv 6057  df-om 7231  df-wrecs 7576  df-recs 7637  df-rdg 7675  df-nn 11213 This theorem is referenced by:  dfnn2  11225  dfnn3  11226  nnind  11230  nn1suc  11233  2nn  11377  nnunb  11480  1nn0  11500  nn0p1nn  11524  elz2  11586  1z  11599  neg1z  11605  nneo  11653  9p1e10  11688  elnn1uz2  11958  zq  11987  rpnnen1lem4  12010  rpnnen1lem5  12011  rpnnen1lem4OLD  12016  rpnnen1lem5OLD  12017  ser1const  13051  exp1  13060  nnexpcl  13067  expnbnd  13187  3dec  13244  fac1  13258  faccl  13264  faclbnd3  13273  faclbnd4lem1  13274  faclbnd4lem2  13275  faclbnd4lem3  13276  faclbnd4lem4  13277  lsw0  13539  eqs1  13583  ccat2s1p1  13603  cats1un  13675  revs1  13714  cats1fvn  13803  relexpsucnnl  13971  relexpaddg  13992  isercolllem2  14595  isercolllem3  14596  isercoll  14597  sumsnf  14672  sumsn  14674  climcndslem1  14780  climcndslem2  14781  fprodnncl  14884  prodsn  14891  prodsnf  14893  nnrisefaccl  14949  eftlub  15038  eirrlem  15131  rpnnen2lem5  15146  rpnnen2lem8  15149  rpnnen2lem12  15153  dvdsle  15234  n2dvds1  15306  ndvdsp1  15337  gcd1  15451  bezoutr1  15484  1nprm  15594  1idssfct  15595  isprm2lem  15596  qden1elz  15667  phi1  15680  phiprm  15684  pcpre1  15749  pczpre  15754  pcmptcl  15797  pcmpt  15798  infpnlem2  15817  prmreclem1  15822  prmreclem6  15827  mul4sq  15860  vdwmc2  15885  vdwlem8  15894  vdwlem13  15899  vdwnnlem3  15903  prmocl  15940  prmop1  15944  fvprmselelfz  15950  fvprmselgcd1  15951  prmolefac  15952  prmodvdslcmf  15953  prmgapprmo  15968  5prm  16017  7prm  16019  11prm  16024  13prm  16025  17prm  16026  19prm  16027  37prm  16030  43prm  16031  83prm  16032  139prm  16033  163prm  16034  317prm  16035  631prm  16036  1259lem4  16043  1259lem5  16044  1259prm  16045  2503lem3  16048  2503prm  16049  4001lem1  16050  4001lem2  16051  4001lem3  16052  4001lem4  16053  4001prm  16054  baseid  16121  basendx  16125  basendxnn  16126  ressval3d  16139  1strstr  16181  2strstr  16185  basendxnplusgndx  16191  basendxnmulrndx  16201  rngstr  16202  lmodstr  16219  topgrpstr  16244  otpsstr  16253  otpsstrOLD  16257  ocndx  16262  ocid  16263  ressds  16275  resshom  16280  ressco  16281  slotsbhcdif  16282  oppcbas  16579  rescbas  16690  rescabs  16694  catstr  16818  estrreslem1  16978  ipostr  17354  mulg1  17749  mulg2  17751  oppgbas  17981  od1  18176  gex1  18206  efgsval2  18346  efgsp1  18350  torsubg  18457  pgpfaclem1  18680  mgpbas  18695  mgpds  18699  opprbas  18829  rmodislmod  19133  srabase  19380  srads  19388  opsrbas  19681  cnfldfun  19960  zlmbas  20068  znbas2  20090  thlbas  20242  thlle  20243  pmatcollpw3fi1lem2  20794  hauspwdom  21506  ressunif  22267  tuslem  22272  imasdsf1olem  22379  setsmsds  22482  tmslem  22488  tnglem  22645  tngbas  22646  tngds  22653  cphipval  23242  bcthlem4  23324  bcth3  23328  ovolmge0  23445  ovollb2  23457  ovolctb  23458  ovolunlem1a  23464  ovolunlem1  23465  ovoliunlem1  23470  ovoliun  23473  ovoliun2  23474  ovolicc1  23484  voliunlem1  23518  volsup  23524  ioombl1lem2  23527  ioombl1lem4  23529  uniioombllem1  23549  uniioombllem2  23551  uniioombllem6  23556  itg1climres  23680  itg2seq  23708  itg2monolem1  23716  itg2monolem2  23717  itg2monolem3  23718  itg2mono  23719  itg2i1fseq2  23722  itg2cnlem1  23727  aalioulem5  24290  aaliou2b  24295  aaliou3lem4  24300  aaliou3lem7  24303  dcubic1lem  24769  dcubic2  24770  mcubic  24773  log2ub  24875  emcllem6  24926  emcllem7  24927  lgam1  24989  gam1  24990  ftalem7  25004  efnnfsumcl  25028  vmaprm  25042  efvmacl  25045  efchtdvds  25084  vma1  25091  prmorcht  25103  sqff1o  25107  pclogsum  25139  perfectlem1  25153  perfectlem2  25154  bpos1  25207  bposlem5  25212  lgsdir  25256  lgs1  25265  lgsquad2lem2  25309  dchrmusumlema  25381  dchrisum0lema  25402  trkgstr  25542  ttgbas  25956  ttgplusg  25957  ttgvsca  25959  eengstr  26059  baseltedgf  26071  basvtxvalOLD  26102  usgrexmplef  26350  lfgrn1cycl  26908  clwwlkn1  27170  ipval2  27871  opsqrlem2  29309  ssnnssfz  29858  nnindf  29874  nn0min  29876  isarchi3  30050  resvbas  30141  rge0scvg  30304  zlmds  30317  qqh0  30337  qqh1  30338  esumfzf  30440  esumfsup  30441  esumpcvgval  30449  voliune  30601  eulerpartgbij  30743  eulerpartlemgs2  30751  fib2  30773  rrvsum  30825  ballotlem4  30869  ballotlemi1  30873  ballotlemii  30874  ballotlemic  30877  ballotlem1c  30878  hgt750lem  31038  hgt750leme  31045  faclimlem1  31936  nn0prpwlem  32623  nn0prpw  32624  poimirlem32  33754  ovoliunnfl  33764  voliunnfl  33766  volsupnfl  33767  incsequz  33857  bfplem1  33934  rrncmslem  33944  hlhilsbase  37733  jm2.23  38065  rmydioph  38083  rmxdioph  38085  expdiophlem2  38091  expdioph  38092  relexp2  38471  iunrelexpmin1  38502  iunrelexpmin2  38506  dftrcl3  38514  fvtrcllb1d  38516  cotrcltrcl  38519  corcltrcl  38533  cotrclrcl  38536  prmunb2  39012  sumsnd  39684  nnn0  40093  xrralrecnnge  40111  iooiinicc  40272  iooiinioc  40286  mccl  40333  sumnnodd  40365  wallispilem4  40788  wallispi2lem1  40791  wallispi2lem2  40792  stirlinglem8  40801  stirlinglem11  40804  stirlinglem12  40805  stirlinglem13  40806  fourierdlem31  40858  nnfoctbdjlem  41175  hoicvr  41268  hoicvrrex  41276  hoidmvlelem3  41317  ovnhoilem1  41321  ovnhoilem2  41322  ovnlecvr2  41330  ovnsubadd2lem  41365  iinhoiicclem  41393  vonicclem2  41404  iccpartlt  41870  257prm  41983  fmtnoprmfac2lem1  41988  fmtno4prmfac193  41995  fmtno4nprmfac193  41996  fmtno5nprm  42005  3ndvds4  42020  139prmALT  42021  31prm  42022  127prm  42025  3exp4mod41  42043  41prothprmlem2  42045  perfectALTVlem1  42140  perfectALTVlem2  42141  nnsum3primesprm  42188  bgoldbtbndlem1  42203  tgblthelfgott  42213  tgblthelfgottOLD  42219  nnsgrpmgm  42326  nnsgrpnmnd  42328  blennn0elnn  42881  blen1  42888
 Copyright terms: Public domain W3C validator