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

Theorem 1nn 11638
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 10626 . . . 4 1 ∈ V
2 fr0g 8062 . . . 4 (1 ∈ V → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘∅) = 1)
31, 2ax-mp 5 . . 3 ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘∅) = 1
4 frfnom 8061 . . . 4 (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω) Fn ω
5 peano1 7589 . . . 4 ∅ ∈ ω
6 fnfvelrn 6844 . . . 4 (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω) Fn ω ∧ ∅ ∈ ω) → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘∅) ∈ ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω))
74, 5, 6mp2an 688 . . 3 ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘∅) ∈ ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)
83, 7eqeltrri 2915 . 2 1 ∈ ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)
9 df-nn 11628 . . 3 ℕ = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) “ ω)
10 df-ima 5567 . . 3 (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) “ ω) = ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)
119, 10eqtri 2849 . 2 ℕ = ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)
128, 11eleqtrri 2917 1 1 ∈ ℕ
Colors of variables: wff setvar class
Syntax hints:   = wceq 1530  wcel 2107  Vcvv 3500  c0 4295  cmpt 5143  ran crn 5555  cres 5556  cima 5557   Fn wfn 6347  cfv 6352  (class class class)co 7148  ωcom 7568  reccrdg 8036  1c1 10527   + caddc 10529  cn 11627
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798  ax-sep 5200  ax-nul 5207  ax-pow 5263  ax-pr 5326  ax-un 7451  ax-1cn 10584
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3or 1082  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2620  df-eu 2652  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-ne 3022  df-ral 3148  df-rex 3149  df-reu 3150  df-rab 3152  df-v 3502  df-sbc 3777  df-csb 3888  df-dif 3943  df-un 3945  df-in 3947  df-ss 3956  df-pss 3958  df-nul 4296  df-if 4471  df-pw 4544  df-sn 4565  df-pr 4567  df-tp 4569  df-op 4571  df-uni 4838  df-iun 4919  df-br 5064  df-opab 5126  df-mpt 5144  df-tr 5170  df-id 5459  df-eprel 5464  df-po 5473  df-so 5474  df-fr 5513  df-we 5515  df-xp 5560  df-rel 5561  df-cnv 5562  df-co 5563  df-dm 5564  df-rn 5565  df-res 5566  df-ima 5567  df-pred 6146  df-ord 6192  df-on 6193  df-lim 6194  df-suc 6195  df-iota 6312  df-fun 6354  df-fn 6355  df-f 6356  df-f1 6357  df-fo 6358  df-f1o 6359  df-fv 6360  df-om 7569  df-wrecs 7938  df-recs 7999  df-rdg 8037  df-nn 11628
This theorem is referenced by:  dfnn2  11640  dfnn3  11641  nnind  11645  nn1suc  11648  2nn  11699  nnunb  11882  1nn0  11902  nn0p1nn  11925  elz2  11988  1z  12001  neg1z  12007  nneo  12055  9p1e10  12089  elnn1uz2  12314  zq  12343  zqOLD  12344  rpnnen1lem4  12369  rpnnen1lem5  12370  ser1const  13416  exp1  13425  nnexpcl  13432  expnbnd  13583  fac1  13627  faccl  13633  faclbnd3  13642  faclbnd4lem1  13643  faclbnd4lem2  13644  faclbnd4lem3  13645  faclbnd4lem4  13646  lsw0  13907  ccat2s1p1  13975  ccat2s1p1OLD  13977  cats1un  14073  revs1  14117  cats1fvn  14210  relexpsucnnl  14381  relexpaddg  14402  isercolllem2  15012  isercolllem3  15013  isercoll  15014  sumsnf  15089  climcndslem1  15194  climcndslem2  15195  fprodnncl  15299  prodsn  15306  prodsnf  15308  nnrisefaccl  15363  eftlub  15452  eirrlem  15547  rpnnen2lem5  15561  rpnnen2lem8  15564  rpnnen2lem12  15568  dvdsle  15650  n2dvds1OLD  15708  ndvdsp1  15752  gcd1  15866  bezoutr1  15903  1nprm  16013  1idssfct  16014  isprm2lem  16015  qden1elz  16087  phi1  16100  phiprm  16104  pcpre1  16169  pczpre  16174  pcmptcl  16217  pcmpt  16218  infpnlem2  16237  prmreclem1  16242  prmreclem6  16247  mul4sq  16280  vdwmc2  16305  vdwlem8  16314  vdwlem13  16319  vdwnnlem3  16323  prmocl  16360  prmop1  16364  fvprmselelfz  16370  fvprmselgcd1  16371  prmolefac  16372  prmodvdslcmf  16373  prmgapprmo  16388  5prm  16432  7prm  16434  11prm  16438  13prm  16439  17prm  16440  19prm  16441  37prm  16444  43prm  16445  83prm  16446  139prm  16447  163prm  16448  317prm  16449  631prm  16450  1259lem4  16457  1259lem5  16458  1259prm  16459  2503lem3  16462  2503prm  16463  4001lem1  16464  4001lem2  16465  4001lem3  16466  4001lem4  16467  4001prm  16468  baseid  16533  basendx  16537  basendxnn  16538  ressval3d  16551  1strstr  16588  2strstr  16592  basendxnplusgndx  16598  basendxnmulrndx  16608  rngstr  16609  lmodstr  16626  topgrpstr  16651  otpsstr  16658  ocndx  16663  ocid  16664  ressds  16676  resshom  16681  ressco  16682  slotsbhcdif  16683  oppcbas  16978  rescbas  17089  rescabs  17093  catstr  17217  estrreslem1  17377  ipostr  17753  mulgfval  18156  mulg1  18165  mulg2  18167  oppgbas  18409  od1  18606  gex1  18636  efgsval2  18779  efgsp1  18783  torsubg  18894  pgpfaclem1  19123  mgpbas  19165  mgpds  19169  opprbas  19299  rmodislmod  19622  srabase  19870  srads  19878  opsrbas  20177  cnfldfun  20473  zlmbas  20581  znbas2  20602  thlbas  20756  thlle  20757  pmatcollpw3fi1lem2  21311  hauspwdom  22025  ressunif  22786  tuslem  22791  imasdsf1olem  22898  setsmsds  23001  tmslem  23007  tnglem  23164  tngbas  23165  tngds  23172  cphipval  23761  bcthlem4  23845  bcth3  23849  ovolmge0  23993  ovollb2  24005  ovolctb  24006  ovolunlem1a  24012  ovolunlem1  24013  ovoliunlem1  24018  ovoliun  24021  ovoliun2  24022  ovolicc1  24032  voliunlem1  24066  volsup  24072  ioombl1lem2  24075  ioombl1lem4  24077  uniioombllem1  24097  uniioombllem2  24099  uniioombllem6  24104  itg1climres  24230  itg2seq  24258  itg2monolem1  24266  itg2monolem2  24267  itg2monolem3  24268  itg2mono  24269  itg2i1fseq2  24272  itg2cnlem1  24277  aalioulem5  24840  aaliou2b  24845  aaliou3lem4  24850  aaliou3lem7  24853  log2ub  25441  emcllem6  25492  emcllem7  25493  lgam1  25555  gam1  25556  ftalem7  25570  efnnfsumcl  25594  vmaprm  25608  efvmacl  25611  efchtdvds  25650  vma1  25657  prmorcht  25669  sqff1o  25673  pclogsum  25705  perfectlem1  25719  perfectlem2  25720  bpos1  25773  bposlem5  25778  lgsdir  25822  lgs1  25831  lgsquad2lem2  25875  addsqn2reu  25931  addsqrexnreu  25932  dchrmusumlema  25983  dchrisum0lema  26004  trkgstr  26144  ttgbas  26577  ttgplusg  26578  ttgvsca  26580  eengstr  26680  baseltedgf  26693  usgrexmplef  26955  lfgrn1cycl  27497  clwwlkn1  27733  ipval2  28398  opsqrlem2  29832  ssnnssfz  30423  nnindf  30448  nn0min  30450  isarchi3  30730  resvbas  30819  rge0scvg  31078  zlmds  31091  qqh0  31111  qqh1  31112  esumfzf  31214  esumfsup  31215  esumpcvgval  31223  voliune  31374  eulerpartgbij  31516  eulerpartlemgs2  31524  fib2  31546  rrvsum  31598  ballotlem4  31642  ballotlemi1  31646  ballotlemii  31647  ballotlemic  31650  ballotlem1c  31651  hgt750lem  31808  hgt750leme  31815  0nn0m1nnn0  32235  faclimlem1  32859  nn0prpwlem  33554  nn0prpw  33555  poimirlem32  34791  ovoliunnfl  34801  voliunnfl  34803  volsupnfl  34804  incsequz  34891  bfplem1  34968  rrncmslem  34978  hlhilsbase  38942  nnmulcom  39030  3cubes  39152  jm2.23  39458  rmydioph  39476  rmxdioph  39478  expdiophlem2  39484  expdioph  39485  relexp2  39887  iunrelexpmin1  39918  iunrelexpmin2  39922  dftrcl3  39930  fvtrcllb1d  39932  cotrcltrcl  39935  corcltrcl  39949  cotrclrcl  39952  prmunb2  40508  sumsnd  41148  nnn0  41512  xrralrecnnge  41527  iooiinicc  41683  iooiinioc  41697  mccl  41744  sumnnodd  41776  wallispilem4  42219  wallispi2lem1  42222  wallispi2lem2  42223  stirlinglem8  42232  stirlinglem11  42235  stirlinglem12  42236  stirlinglem13  42237  fourierdlem31  42289  nnfoctbdjlem  42603  hoicvr  42696  hoicvrrex  42704  hoidmvlelem3  42745  ovnhoilem1  42749  ovnhoilem2  42750  ovnlecvr2  42758  ovnsubadd2lem  42793  iinhoiicclem  42821  vonicclem2  42832  iccpartlt  43416  257prm  43555  fmtnoprmfac2lem1  43560  fmtno4prmfac193  43567  fmtno4nprmfac193  43568  fmtno5nprm  43577  3ndvds4  43590  139prmALT  43591  31prm  43592  127prm  43595  3exp4mod41  43613  41prothprmlem2  43615  perfectALTVlem1  43718  perfectALTVlem2  43719  2exp340mod341  43730  341fppr2  43731  4fppr1  43732  nnsum3primesprm  43787  bgoldbtbndlem1  43802  tgblthelfgott  43812  nnsgrpmgm  43915  nnsgrpnmnd  43917  blennn0elnn  44469  blen1  44476
  Copyright terms: Public domain W3C validator