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 6841 . . . 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 2910 . 2 1 ∈ ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)
9 df-nn 11628 . . 3 ℕ = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) “ ω)
10 df-ima 5562 . . 3 (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) “ ω) = ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)
119, 10eqtri 2844 . 2 ℕ = ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)
128, 11eleqtrri 2912 1 1 ∈ ℕ
Colors of variables: wff setvar class
Syntax hints:   = wceq 1528  wcel 2105  Vcvv 3495  c0 4290  cmpt 5138  ran crn 5550  cres 5551  cima 5552   Fn wfn 6344  cfv 6349  (class class class)co 7145  ω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 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793  ax-sep 5195  ax-nul 5202  ax-pow 5258  ax-pr 5321  ax-un 7450  ax-1cn 10584
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-reu 3145  df-rab 3147  df-v 3497  df-sbc 3772  df-csb 3883  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-pss 3953  df-nul 4291  df-if 4466  df-pw 4539  df-sn 4560  df-pr 4562  df-tp 4564  df-op 4566  df-uni 4833  df-iun 4914  df-br 5059  df-opab 5121  df-mpt 5139  df-tr 5165  df-id 5454  df-eprel 5459  df-po 5468  df-so 5469  df-fr 5508  df-we 5510  df-xp 5555  df-rel 5556  df-cnv 5557  df-co 5558  df-dm 5559  df-rn 5560  df-res 5561  df-ima 5562  df-pred 6142  df-ord 6188  df-on 6189  df-lim 6190  df-suc 6191  df-iota 6308  df-fun 6351  df-fn 6352  df-f 6353  df-f1 6354  df-fo 6355  df-f1o 6356  df-fv 6357  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  18166  mulg1  18175  mulg2  18177  oppgbas  18419  od1  18617  gex1  18647  efgsval2  18790  efgsp1  18794  torsubg  18905  pgpfaclem1  19134  mgpbas  19176  mgpds  19180  opprbas  19310  rmodislmod  19633  srabase  19881  srads  19889  opsrbas  20189  cnfldfun  20487  zlmbas  20595  znbas2  20616  thlbas  20770  thlle  20771  pmatcollpw3fi1lem2  21325  hauspwdom  22039  ressunif  22800  tuslem  22805  imasdsf1olem  22912  setsmsds  23015  tmslem  23021  tnglem  23178  tngbas  23179  tngds  23186  cphipval  23775  bcthlem4  23859  bcth3  23863  ovolmge0  24007  ovollb2  24019  ovolctb  24020  ovolunlem1a  24026  ovolunlem1  24027  ovoliunlem1  24032  ovoliun  24035  ovoliun2  24036  ovolicc1  24046  voliunlem1  24080  volsup  24086  ioombl1lem2  24089  ioombl1lem4  24091  uniioombllem1  24111  uniioombllem2  24113  uniioombllem6  24118  itg1climres  24244  itg2seq  24272  itg2monolem1  24280  itg2monolem2  24281  itg2monolem3  24282  itg2mono  24283  itg2i1fseq2  24286  itg2cnlem1  24291  aalioulem5  24854  aaliou2b  24859  aaliou3lem4  24864  aaliou3lem7  24867  log2ub  25455  emcllem6  25506  emcllem7  25507  lgam1  25569  gam1  25570  ftalem7  25584  efnnfsumcl  25608  vmaprm  25622  efvmacl  25625  efchtdvds  25664  vma1  25671  prmorcht  25683  sqff1o  25687  pclogsum  25719  perfectlem1  25733  perfectlem2  25734  bpos1  25787  bposlem5  25792  lgsdir  25836  lgs1  25845  lgsquad2lem2  25889  addsqn2reu  25945  addsqrexnreu  25946  dchrmusumlema  25997  dchrisum0lema  26018  trkgstr  26158  ttgbas  26591  ttgplusg  26592  ttgvsca  26594  eengstr  26694  baseltedgf  26707  usgrexmplef  26969  lfgrn1cycl  27511  clwwlkn1  27747  ipval2  28412  opsqrlem2  29846  ssnnssfz  30437  nnindf  30462  nn0min  30464  isarchi3  30744  resvbas  30833  rge0scvg  31092  zlmds  31105  qqh0  31125  qqh1  31126  esumfzf  31228  esumfsup  31229  esumpcvgval  31237  voliune  31388  eulerpartgbij  31530  eulerpartlemgs2  31538  fib2  31560  rrvsum  31612  ballotlem4  31656  ballotlemi1  31660  ballotlemii  31661  ballotlemic  31664  ballotlem1c  31665  hgt750lem  31822  hgt750leme  31829  0nn0m1nnn0  32249  faclimlem1  32873  nn0prpwlem  33568  nn0prpw  33569  poimirlem32  34806  ovoliunnfl  34816  voliunnfl  34818  volsupnfl  34819  incsequz  34906  bfplem1  34983  rrncmslem  34993  hlhilsbase  38957  nnmulcom  39045  3cubes  39167  jm2.23  39473  rmydioph  39491  rmxdioph  39493  expdiophlem2  39499  expdioph  39500  relexp2  39902  iunrelexpmin1  39933  iunrelexpmin2  39937  dftrcl3  39945  fvtrcllb1d  39947  cotrcltrcl  39950  corcltrcl  39964  cotrclrcl  39967  prmunb2  40523  sumsnd  41163  nnn0  41527  xrralrecnnge  41542  iooiinicc  41698  iooiinioc  41712  mccl  41759  sumnnodd  41791  wallispilem4  42234  wallispi2lem1  42237  wallispi2lem2  42238  stirlinglem8  42247  stirlinglem11  42250  stirlinglem12  42251  stirlinglem13  42252  fourierdlem31  42304  nnfoctbdjlem  42618  hoicvr  42711  hoicvrrex  42719  hoidmvlelem3  42760  ovnhoilem1  42764  ovnhoilem2  42765  ovnlecvr2  42773  ovnsubadd2lem  42808  iinhoiicclem  42836  vonicclem2  42847  iccpartlt  43431  257prm  43570  fmtnoprmfac2lem1  43575  fmtno4prmfac193  43582  fmtno4nprmfac193  43583  fmtno5nprm  43592  3ndvds4  43605  139prmALT  43606  31prm  43607  127prm  43610  3exp4mod41  43628  41prothprmlem2  43630  perfectALTVlem1  43733  perfectALTVlem2  43734  2exp340mod341  43745  341fppr2  43746  4fppr1  43747  nnsum3primesprm  43802  bgoldbtbndlem1  43817  tgblthelfgott  43827  nnsgrpmgm  43930  nnsgrpnmnd  43932  blennn0elnn  44535  blen1  44542
  Copyright terms: Public domain W3C validator