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

Theorem 4nn 10477
Description: 4 is a positive integer. (Contributed by NM, 8-Jan-2006.)
Assertion
Ref Expression
4nn  |-  4  e.  NN

Proof of Theorem 4nn
StepHypRef Expression
1 df-4 10378 . 2  |-  4  =  ( 3  +  1 )
2 3nn 10476 . . 3  |-  3  e.  NN
3 peano2nn 10330 . . 3  |-  ( 3  e.  NN  ->  (
3  +  1 )  e.  NN )
42, 3ax-mp 5 . 2  |-  ( 3  +  1 )  e.  NN
51, 4eqeltri 2511 1  |-  4  e.  NN
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1761  (class class class)co 6090   1c1 9279    + caddc 9281   NNcn 10318   3c3 10368   4c4 10369
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-8 1763  ax-9 1765  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422  ax-sep 4410  ax-nul 4418  ax-pow 4467  ax-pr 4528  ax-un 6371  ax-1cn 9336
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 961  df-3an 962  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-eu 2263  df-mo 2264  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-ne 2606  df-ral 2718  df-rex 2719  df-reu 2720  df-rab 2722  df-v 2972  df-sbc 3184  df-csb 3286  df-dif 3328  df-un 3330  df-in 3332  df-ss 3339  df-pss 3341  df-nul 3635  df-if 3789  df-pw 3859  df-sn 3875  df-pr 3877  df-tp 3879  df-op 3881  df-uni 4089  df-iun 4170  df-br 4290  df-opab 4348  df-mpt 4349  df-tr 4383  df-eprel 4628  df-id 4632  df-po 4637  df-so 4638  df-fr 4675  df-we 4677  df-ord 4718  df-on 4719  df-lim 4720  df-suc 4721  df-xp 4842  df-rel 4843  df-cnv 4844  df-co 4845  df-dm 4846  df-rn 4847  df-res 4848  df-ima 4849  df-iota 5378  df-fun 5417  df-fn 5418  df-f 5419  df-f1 5420  df-fo 5421  df-f1o 5422  df-fv 5423  df-ov 6093  df-om 6476  df-recs 6828  df-rdg 6862  df-nn 10319  df-2 10376  df-3 10377  df-4 10378
This theorem is referenced by:  5nn  10478  4nn0  10594  iexpcyc  11966  ef01bndlem  13464  sin01bnd  13465  cos01bnd  13466  2expltfac  14115  8nprm  14135  37prm  14144  43prm  14145  83prm  14146  139prm  14147  631prm  14150  1259lem3  14153  1259prm  14156  2503lem2  14158  starvndx  14285  starvid  14286  ressstarv  14288  srngfn  14289  homndx  14349  homid  14350  resshom  14353  prdsvalstr  14387  oppchomfval  14649  oppcbas  14653  rescco  14741  catstr  14863  lt6abl  16364  pcoass  20496  minveclem3  20816  iblitg  21146  dveflem  21351  tan4thpi  21919  atan1  22266  log2tlbnd  22283  log2ub  22287  ppiub  22486  bclbnd  22562  bpos1  22565  bposlem6  22571  bposlem7  22572  bposlem8  22573  bposlem9  22574  lgsdir2lem2  22606  m1lgs  22644  chebbnd1lem1  22661  chebbnd1lem2  22662  chebbnd1lem3  22663  pntibndlem1  22781  pntibndlem2  22783  pntibndlem3  22784  pntlema  22788  pntlemb  22789  pntlemg  22790  pntlemf  22797  usgraexvlem  23232  4cycl4dv  23472  fib5  26702  4bc2eq6  27304  fsumcube  28116  rmydioph  29272  rmxdioph  29274  expdiophlem2  29280  zlmodzxzequa  30862  zlmodzxznm  30863  zlmodzxzequap  30865  zlmodzxzldeplem3  30868  zlmodzxzldep  30870  ldepsnlinclem1  30871  ldepsnlinc  30874
  Copyright terms: Public domain W3C validator