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

Theorem 1nn 11314
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 10319 . . . 4 1 ∈ V
2 fr0g 7765 . . . 4 (1 ∈ V → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘∅) = 1)
31, 2ax-mp 5 . . 3 ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘∅) = 1
4 frfnom 7764 . . . 4 (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω) Fn ω
5 peano1 7313 . . . 4 ∅ ∈ ω
6 fnfvelrn 6576 . . . 4 (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω) Fn ω ∧ ∅ ∈ ω) → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘∅) ∈ ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω))
74, 5, 6mp2an 675 . . 3 ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘∅) ∈ ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)
83, 7eqeltrri 2880 . 2 1 ∈ ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)
9 df-nn 11304 . . 3 ℕ = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) “ ω)
10 df-ima 5322 . . 3 (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) “ ω) = ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)
119, 10eqtri 2826 . 2 ℕ = ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)
128, 11eleqtrri 2882 1 1 ∈ ℕ
Colors of variables: wff setvar class
Syntax hints:   = wceq 1637  wcel 2156  Vcvv 3389  c0 4114  cmpt 4921  ran crn 5310  cres 5311  cima 5312   Fn wfn 6094  cfv 6099  (class class class)co 6872  ωcom 7293  reccrdg 7739  1c1 10220   + caddc 10222  cn 11303
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-8 2158  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2782  ax-sep 4973  ax-nul 4981  ax-pow 5033  ax-pr 5094  ax-un 7177  ax-1cn 10277
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-eu 2634  df-mo 2635  df-clab 2791  df-cleq 2797  df-clel 2800  df-nfc 2935  df-ne 2977  df-ral 3099  df-rex 3100  df-reu 3101  df-rab 3103  df-v 3391  df-sbc 3632  df-csb 3727  df-dif 3770  df-un 3772  df-in 3774  df-ss 3781  df-pss 3783  df-nul 4115  df-if 4278  df-pw 4351  df-sn 4369  df-pr 4371  df-tp 4373  df-op 4375  df-uni 4629  df-iun 4712  df-br 4843  df-opab 4905  df-mpt 4922  df-tr 4945  df-id 5217  df-eprel 5222  df-po 5230  df-so 5231  df-fr 5268  df-we 5270  df-xp 5315  df-rel 5316  df-cnv 5317  df-co 5318  df-dm 5319  df-rn 5320  df-res 5321  df-ima 5322  df-pred 5891  df-ord 5937  df-on 5938  df-lim 5939  df-suc 5940  df-iota 6062  df-fun 6101  df-fn 6102  df-f 6103  df-f1 6104  df-fo 6105  df-f1o 6106  df-fv 6107  df-om 7294  df-wrecs 7640  df-recs 7702  df-rdg 7740  df-nn 11304
This theorem is referenced by:  dfnn2  11316  dfnn3  11317  nnind  11321  nn1suc  11324  2nn  11460  nnunb  11553  1nn0  11573  nn0p1nn  11596  elz2  11658  1z  11671  neg1z  11677  nneo  11725  9p1e10  11759  elnn1uz2  11982  zq  12011  rpnnen1lem4  12034  rpnnen1lem5  12035  ser1const  13078  exp1  13087  nnexpcl  13094  expnbnd  13214  3dec  13271  fac1  13282  faccl  13288  faclbnd3  13297  faclbnd4lem1  13298  faclbnd4lem2  13299  faclbnd4lem3  13300  faclbnd4lem4  13301  lsw0  13562  eqs1  13605  ccat2s1p1  13625  cats1un  13697  revs1  13736  cats1fvn  13825  relexpsucnnl  13993  relexpaddg  14014  isercolllem2  14617  isercolllem3  14618  isercoll  14619  sumsnf  14694  sumsn  14696  climcndslem1  14801  climcndslem2  14802  fprodnncl  14904  prodsn  14911  prodsnf  14913  nnrisefaccl  14968  eftlub  15057  eirrlem  15150  rpnnen2lem5  15165  rpnnen2lem8  15168  rpnnen2lem12  15172  dvdsle  15253  n2dvds1  15322  ndvdsp1  15352  gcd1  15466  bezoutr1  15499  1nprm  15608  1idssfct  15609  isprm2lem  15610  qden1elz  15680  phi1  15693  phiprm  15697  pcpre1  15762  pczpre  15767  pcmptcl  15810  pcmpt  15811  infpnlem2  15830  prmreclem1  15835  prmreclem6  15840  mul4sq  15873  vdwmc2  15898  vdwlem8  15907  vdwlem13  15912  vdwnnlem3  15916  prmocl  15953  prmop1  15957  fvprmselelfz  15963  fvprmselgcd1  15964  prmolefac  15965  prmodvdslcmf  15966  prmgapprmo  15981  5prm  16025  7prm  16027  11prm  16031  13prm  16032  17prm  16033  19prm  16034  37prm  16037  43prm  16038  83prm  16039  139prm  16040  163prm  16041  317prm  16042  631prm  16043  1259lem4  16050  1259lem5  16051  1259prm  16052  2503lem3  16055  2503prm  16056  4001lem1  16057  4001lem2  16058  4001lem3  16059  4001lem4  16060  4001prm  16061  baseid  16128  basendx  16132  basendxnn  16133  ressval3d  16146  ressval3dOLD  16147  1strstr  16188  2strstr  16192  basendxnplusgndx  16198  basendxnmulrndx  16208  rngstr  16209  lmodstr  16226  topgrpstr  16251  otpsstr  16258  ocndx  16263  ocid  16264  ressds  16276  resshom  16281  ressco  16282  slotsbhcdif  16283  oppcbas  16580  rescbas  16691  rescabs  16695  catstr  16819  estrreslem1  16979  ipostr  17356  mulg1  17751  mulg2  17753  oppgbas  17980  od1  18175  gex1  18205  efgsval2  18345  efgsp1  18349  torsubg  18456  pgpfaclem1  18680  mgpbas  18695  mgpds  18699  opprbas  18829  rmodislmod  19133  srabase  19385  srads  19393  opsrbas  19685  cnfldfun  19964  zlmbas  20072  znbas2  20093  thlbas  20248  thlle  20249  pmatcollpw3fi1lem2  20803  hauspwdom  21516  ressunif  22277  tuslem  22282  imasdsf1olem  22389  setsmsds  22492  tmslem  22498  tnglem  22655  tngbas  22656  tngds  22663  cphipval  23252  bcthlem4  23334  bcth3  23338  ovolmge0  23456  ovollb2  23468  ovolctb  23469  ovolunlem1a  23475  ovolunlem1  23476  ovoliunlem1  23481  ovoliun  23484  ovoliun2  23485  ovolicc1  23495  voliunlem1  23529  volsup  23535  ioombl1lem2  23538  ioombl1lem4  23540  uniioombllem1  23560  uniioombllem2  23562  uniioombllem6  23567  itg1climres  23693  itg2seq  23721  itg2monolem1  23729  itg2monolem2  23730  itg2monolem3  23731  itg2mono  23732  itg2i1fseq2  23735  itg2cnlem1  23740  aalioulem5  24303  aaliou2b  24308  aaliou3lem4  24313  aaliou3lem7  24316  dcubic1lem  24782  dcubic2  24783  mcubic  24786  log2ub  24888  emcllem6  24939  emcllem7  24940  lgam1  25002  gam1  25003  ftalem7  25017  efnnfsumcl  25041  vmaprm  25055  efvmacl  25058  efchtdvds  25097  vma1  25104  prmorcht  25116  sqff1o  25120  pclogsum  25152  perfectlem1  25166  perfectlem2  25167  bpos1  25220  bposlem5  25225  lgsdir  25269  lgs1  25278  lgsquad2lem2  25322  dchrmusumlema  25394  dchrisum0lema  25415  trkgstr  25555  ttgbas  25969  ttgplusg  25970  ttgvsca  25972  eengstr  26072  baseltedgf  26084  basvtxvalOLD  26115  usgrexmplef  26365  lfgrn1cycl  26924  clwwlkn1  27188  ipval2  27888  opsqrlem2  29326  ssnnssfz  29874  nnindf  29890  nn0min  29892  isarchi3  30064  resvbas  30155  rge0scvg  30318  zlmds  30331  qqh0  30351  qqh1  30352  esumfzf  30454  esumfsup  30455  esumpcvgval  30463  voliune  30615  eulerpartgbij  30757  eulerpartlemgs2  30765  fib2  30787  rrvsum  30839  ballotlem4  30883  ballotlemi1  30887  ballotlemii  30888  ballotlemic  30891  ballotlem1c  30892  hgt750lem  31052  hgt750leme  31059  faclimlem1  31949  nn0prpwlem  32636  nn0prpw  32637  poimirlem32  33752  ovoliunnfl  33762  voliunnfl  33764  volsupnfl  33765  incsequz  33853  bfplem1  33930  rrncmslem  33940  hlhilsbase  37718  jm2.23  38062  rmydioph  38080  rmxdioph  38082  expdiophlem2  38088  expdioph  38089  relexp2  38467  iunrelexpmin1  38498  iunrelexpmin2  38502  dftrcl3  38510  fvtrcllb1d  38512  cotrcltrcl  38515  corcltrcl  38529  cotrclrcl  38532  prmunb2  39008  sumsnd  39677  nnn0  40073  xrralrecnnge  40090  iooiinicc  40247  iooiinioc  40261  mccl  40308  sumnnodd  40340  wallispilem4  40762  wallispi2lem1  40765  wallispi2lem2  40766  stirlinglem8  40775  stirlinglem11  40778  stirlinglem12  40779  stirlinglem13  40780  fourierdlem31  40832  nnfoctbdjlem  41149  hoicvr  41242  hoicvrrex  41250  hoidmvlelem3  41291  ovnhoilem1  41295  ovnhoilem2  41296  ovnlecvr2  41304  ovnsubadd2lem  41339  iinhoiicclem  41367  vonicclem2  41378  iccpartlt  41933  257prm  42046  fmtnoprmfac2lem1  42051  fmtno4prmfac193  42058  fmtno4nprmfac193  42059  fmtno5nprm  42068  3ndvds4  42083  139prmALT  42084  31prm  42085  127prm  42088  3exp4mod41  42106  41prothprmlem2  42108  perfectALTVlem1  42203  perfectALTVlem2  42204  nnsum3primesprm  42251  bgoldbtbndlem1  42266  tgblthelfgott  42276  nnsgrpmgm  42382  nnsgrpnmnd  42384  blennn0elnn  42937  blen1  42944
  Copyright terms: Public domain W3C validator