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

Theorem nn0addcld 10897
Description: Closure of addition of nonnegative integers, inference form. (Contributed by Mario Carneiro, 27-May-2016.)
Hypotheses
Ref Expression
nn0red.1  |-  ( ph  ->  A  e.  NN0 )
nn0addcld.2  |-  ( ph  ->  B  e.  NN0 )
Assertion
Ref Expression
nn0addcld  |-  ( ph  ->  ( A  +  B
)  e.  NN0 )

Proof of Theorem nn0addcld
StepHypRef Expression
1 nn0red.1 . 2  |-  ( ph  ->  A  e.  NN0 )
2 nn0addcld.2 . 2  |-  ( ph  ->  B  e.  NN0 )
3 nn0addcl 10872 . 2  |-  ( ( A  e.  NN0  /\  B  e.  NN0 )  -> 
( A  +  B
)  e.  NN0 )
41, 2, 3syl2anc 659 1  |-  ( ph  ->  ( A  +  B
)  e.  NN0 )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1842  (class class class)co 6278    + caddc 9525   NN0cn0 10836
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-8 1844  ax-9 1846  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380  ax-sep 4517  ax-nul 4525  ax-pow 4572  ax-pr 4630  ax-un 6574  ax-resscn 9579  ax-1cn 9580  ax-icn 9581  ax-addcl 9582  ax-addrcl 9583  ax-mulcl 9584  ax-mulrcl 9585  ax-mulcom 9586  ax-addass 9587  ax-mulass 9588  ax-distr 9589  ax-i2m1 9590  ax-1ne0 9591  ax-1rid 9592  ax-rnegex 9593  ax-rrecex 9594  ax-cnre 9595  ax-pre-lttri 9596  ax-pre-lttrn 9597  ax-pre-ltadd 9598
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 975  df-3an 976  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-eu 2242  df-mo 2243  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ne 2600  df-nel 2601  df-ral 2759  df-rex 2760  df-reu 2761  df-rab 2763  df-v 3061  df-sbc 3278  df-csb 3374  df-dif 3417  df-un 3419  df-in 3421  df-ss 3428  df-pss 3430  df-nul 3739  df-if 3886  df-pw 3957  df-sn 3973  df-pr 3975  df-tp 3977  df-op 3979  df-uni 4192  df-iun 4273  df-br 4396  df-opab 4454  df-mpt 4455  df-tr 4490  df-eprel 4734  df-id 4738  df-po 4744  df-so 4745  df-fr 4782  df-we 4784  df-xp 4829  df-rel 4830  df-cnv 4831  df-co 4832  df-dm 4833  df-rn 4834  df-res 4835  df-ima 4836  df-pred 5367  df-ord 5413  df-on 5414  df-lim 5415  df-suc 5416  df-iota 5533  df-fun 5571  df-fn 5572  df-f 5573  df-f1 5574  df-fo 5575  df-f1o 5576  df-fv 5577  df-ov 6281  df-om 6684  df-wrecs 7013  df-recs 7075  df-rdg 7113  df-er 7348  df-en 7555  df-dom 7556  df-sdom 7557  df-pnf 9660  df-mnf 9661  df-ltxr 9663  df-nn 10577  df-n0 10837
This theorem is referenced by:  expaddz  12254  bccl  12444  ccatrn  12660  swrdccat2  12739  splval2  12789  relexpaddg  13035  rtrclreclem3  13042  mertenslem1  13845  bitsmod  14295  bitsinv1lem  14300  sadcaddlem  14316  sadadd2lem  14318  sadadd  14326  sadass  14330  smupp1  14339  smumul  14352  pcpremul  14576  gzabssqcl  14668  mul4sq  14681  4sqlem12  14683  4sqlem14  14685  4sqlem16  14687  sylow1lem1  16942  efgcpbllemb  17097  coe1tmmul2fv  18639  coe1pwmulfv  18641  chfacfscmulgsum  19653  chfacfpmmulfsupp  19656  chfacfpmmulgsum  19657  cpmadugsumlemF  19669  mdegmullem  22770  coe1mul3  22792  deg1mul2  22807  ply1domn  22816  ply1divex  22829  plymullem  22905  coeeulem  22913  dgrmul  22959  dvntaylp  23058  taylthlem2  23061  dmgmaddnn0  23682  mumullem2  23835  lgseisenlem2  24006  2sqlem8  24028  wwlkext2clwwlk  25220  vdgrfif  25316  numclwwlk2lem1  25519  numclwlk2lem2f  25520  numclwlk2lem2f1o  25522  omndmul2  28154  oddpwdc  28799  iwrdsplit  28832  fiblem  28843  fibp1  28846  signshlen  29053  subfacp1lem6  29482  faclim2  29957  mon1psubm  35530  itgpowd  35546  radcnvrat  36043  binomcxplemnn0  36102  binomcxplemfrat  36104  itgsinexp  37121  wallispilem5  37219  wallispi2lem2  37222  stirlinglem5  37228  stirlinglem7  37230  fourierdlem48  37305  elaa2lem  37384  etransclem32  37417  etransclem46  37431  dignn0flhalflem2  38747
  Copyright terms: Public domain W3C validator