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

Theorem 1nn 10572
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

Proof of Theorem 1nn
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 1ex 9612 . . . 4
2 fr0g 7120 . . . 4
31, 2ax-mp 5 . . 3
4 frfnom 7119 . . . 4
5 peano1 6719 . . . 4
6 fnfvelrn 6028 . . . 4
74, 5, 6mp2an 672 . . 3
83, 7eqeltrri 2542 . 2
9 df-nn 10562 . . 3
10 df-ima 5017 . . 3
119, 10eqtri 2486 . 2
128, 11eleqtrri 2544 1
Colors of variables: wff setvar class
Syntax hints:  =wceq 1395  e.wcel 1818   cvv 3109   c0 3784  e.cmpt 4510  rancrn 5005  |`cres 5006  "cima 5007  Fnwfn 5588  `cfv 5593  (class class class)co 6296   com 6700  reccrdg 7094  1c1 9514   caddc 9516   cn 10561
This theorem is referenced by:  dfnn2  10574  dfnn3  10575  nnind  10579  nn1suc  10582  2nn  10718  nnunb  10816  1nn0  10836  nn0p1nn  10860  elz2  10906  1z  10919  neg1z  10925  nneo  10971  elnn1uz2  11187  zq  11217  rpnnen1lem4  11240  rpnnen1lem5  11241  ser1const  12163  exp1  12172  nnexpcl  12179  expnbnd  12295  fac1  12357  faccl  12363  faclbnd3  12370  faclbnd4lem1  12371  faclbnd4lem2  12372  faclbnd4lem3  12373  faclbnd4lem4  12374  lsw0  12586  ccat2s1p1  12632  cats1un  12701  revs1  12739  cats1fvn  12823  isercolllem2  13488  isercolllem3  13489  isercoll  13490  sumsn  13563  climcndslem1  13661  climcndslem2  13662  fprodnncl  13762  prodsn  13767  eftlub  13844  eirrlem  13937  xpnnenOLD  13943  rpnnen2lem5  13952  rpnnen2lem8  13955  rpnnen2  13959  dvdsle  14031  n2dvds1  14035  ndvdsp1  14067  gcd1  14170  1nprm  14222  1idssfct  14223  qden1elz  14290  phi1  14303  phiprm  14307  pcpre1  14366  pczpre  14371  pcmptcl  14410  pcmpt  14411  infpnlem2  14429  prmreclem1  14434  prmreclem6  14439  mul4sq  14472  vdwmc2  14497  vdwlem8  14506  vdwlem13  14511  vdwnnlem3  14515  5prm  14594  7prm  14596  11prm  14600  13prm  14601  17prm  14602  19prm  14603  37prm  14606  43prm  14607  83prm  14608  139prm  14609  163prm  14610  317prm  14611  631prm  14612  1259lem4  14616  1259lem5  14617  1259prm  14618  2503lem3  14621  2503prm  14622  4001lem1  14623  4001lem2  14624  4001lem3  14625  4001lem4  14626  4001prm  14627  baseid  14678  basendx  14682  2strstr  14733  rngstr  14744  lmodstr  14761  topgrpstr  14786  otpsstr  14793  ocndx  14798  ocid  14799  ressds  14811  resshom  14816  ressco  14817  oppcbas  15113  rescbas  15198  rescabs  15202  catstr  15326  ipostr  15783  mulg1  16149  mulg2  16151  oppgbas  16386  od1  16581  gex1  16611  efgsval2  16751  efgsp1  16755  torsubg  16860  pgpfaclem1  17132  mgpbas  17147  mgpds  17151  opprbas  17278  srabase  17824  srads  17832  opsrbas  18143  zlmbas  18555  znbas2  18578  thlbas  18727  thlle  18728  pmatcollpw3fi1lem2  19288  hauspwdom  20002  ressunif  20765  tuslem  20770  imasdsf1olem  20876  setsmsds  20979  tmslem  20985  tnglem  21154  tngbas  21155  tngds  21162  bcthlem4  21766  bcth3  21770  ovolmge0  21888  ovollb2  21900  ovolctb  21901  ovolunlem1a  21907  ovolunlem1  21908  ovoliunlem1  21913  ovoliun  21916  ovoliun2  21917  ovolicc1  21927  voliunlem1  21960  volsup  21966  ioombl1lem2  21969  ioombl1lem4  21971  uniioombllem1  21990  uniioombllem2  21992  uniioombllem6  21997  itg1climres  22121  itg2seq  22149  itg2monolem1  22157  itg2monolem2  22158  itg2monolem3  22159  itg2mono  22160  itg2i1fseq2  22163  itg2cnlem1  22168  aalioulem5  22732  aaliou2b  22737  aaliou3lem4  22742  aaliou3lem7  22745  dcubic1lem  23174  dcubic2  23175  mcubic  23178  log2ub  23280  emcllem6  23330  emcllem7  23331  ftalem7  23352  efnnfsumcl  23376  vmaprm  23391  efvmacl  23394  efchtdvds  23433  vma1  23440  prmorcht  23452  sqff1o  23456  pclogsum  23490  perfectlem1  23504  perfectlem2  23505  bpos1  23558  bposlem5  23563  lgsdir  23605  1lgs  23612  lgs1  23613  lgsquad2lem2  23634  dchrmusumlema  23678  dchrisum0lema  23699  trkgstr  23840  ttgbas  24180  ttgplusg  24181  ttgvsca  24183  eengstr  24283  usgraexmpl  24401  konigsberg  24987  gx1  25264  ipval2  25617  opsqrlem2  27060  ssnnssfz  27597  nnindf  27610  nn0min  27611  isarchi3  27731  resvbas  27822  rge0scvg  27931  zlmds  27945  qqh0  27965  qqh1  27966  esumfzf  28075  esumfsup  28076  esumpcvgval  28084  voliune  28201  eulerpartgbij  28311  eulerpartlemgs2  28319  fib2  28341  rrvsum  28393  ballotlem4  28437  ballotlemi1  28441  ballotlemii  28442  ballotlemic  28445  ballotlem1c  28446  lgam1  28606  gam1  28607  nnrisefaccl  29141  faclimlem1  29168  ovoliunnfl  30056  voliunnfl  30058  volsupnfl  30059  nn0prpwlem  30140  nn0prpw  30141  incsequz  30241  bfplem1  30318  rrncmslem  30328  bezoutr1  30924  jm2.23  30938  rmydioph  30956  rmxdioph  30958  expdiophlem2  30964  expdioph  30965  prmunb2  31191  sumsnd  31401  sumsnf  31570  prodsnf  31587  mccl  31606  sumnnodd  31636  wallispilem4  31850  wallispi2lem1  31853  wallispi2lem2  31854  stirlinglem8  31863  stirlinglem11  31866  stirlinglem12  31867  stirlinglem13  31868  fourierdlem31  31920  uhgrepe  32378  nnsgrpmgm  32504  nnsgrpnmnd  32506  ressval3d  32558  slotsbhcdif  32559  1strstr  32560  estrreslem1  32643  basendxnmulrndx  32760  hlhilsbase  37669
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-8 1820  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573  ax-nul 4581  ax-pow 4630  ax-pr 4691  ax-un 6592  ax-1cn 9571
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-eu 2286  df-mo 2287  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-reu 2814  df-rab 2816  df-v 3111  df-sbc 3328  df-csb 3435  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-pss 3491  df-nul 3785  df-if 3942  df-pw 4014  df-sn 4030  df-pr 4032  df-tp 4034  df-op 4036  df-uni 4250  df-iun 4332  df-br 4453  df-opab 4511  df-mpt 4512  df-tr 4546  df-eprel 4796  df-id 4800  df-po 4805  df-so 4806  df-fr 4843  df-we 4845  df-ord 4886  df-on 4887  df-lim 4888  df-suc 4889  df-xp 5010  df-rel 5011  df-cnv 5012  df-co 5013  df-dm 5014  df-rn 5015  df-res 5016  df-ima 5017  df-iota 5556  df-fun 5595  df-fn 5596  df-f 5597  df-f1 5598  df-fo 5599  df-f1o 5600  df-fv 5601  df-om 6701  df-recs 7061  df-rdg 7095  df-nn 10562
  Copyright terms: Public domain W3C validator