Theorem nn0mulcld 12034

Description: Closure of multiplication of nonnegative integers, inference form. (Contributed by Mario Carneiro, 27-May-2016.)

Hypotheses

Ref	Expression
nn0red.1	⊢ (𝜑 → 𝐴 ∈ ℕ0)
nn0addcld.2	⊢ (𝜑 → 𝐵 ∈ ℕ0)

Assertion

Ref	Expression
nn0mulcld	⊢ (𝜑 → (𝐴 · 𝐵) ∈ ℕ0)

Proof of Theorem nn0mulcld

Step	Hyp	Ref	Expression
1		nn0red.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℕ0)
2		nn0addcld.2	. 2 ⊢ (𝜑 → 𝐵 ∈ ℕ0)
3		nn0mulcl 12005	. 2 ⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0) → (𝐴 · 𝐵) ∈ ℕ0)
4	1, 2, 3	syl2anc 587	1 ⊢ (𝜑 → (𝐴 · 𝐵) ∈ ℕ0)

Syntax hints:   → wi 4   ∈ wcel 2113  (class class class)co 7164   · cmul 10613  ℕ₀cn0 11969

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1916  ax-6 1974  ax-7 2019  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2161  ax-12 2178  ax-ext 2710  ax-sep 5164  ax-nul 5171  ax-pow 5229  ax-pr 5293  ax-un 7473  ax-resscn 10665  ax-1cn 10666  ax-icn 10667  ax-addcl 10668  ax-addrcl 10669  ax-mulcl 10670  ax-mulrcl 10671  ax-mulcom 10672  ax-addass 10673  ax-mulass 10674  ax-distr 10675  ax-i2m1 10676  ax-1ne0 10677  ax-1rid 10678  ax-rnegex 10679  ax-rrecex 10680  ax-cnre 10681  ax-pre-lttri 10682  ax-pre-lttrn 10683  ax-pre-ltadd 10684

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2540  df-eu 2570  df-clab 2717  df-cleq 2730  df-clel 2811  df-nfc 2881  df-ne 2935  df-nel 3039  df-ral 3058  df-rex 3059  df-reu 3060  df-rab 3062  df-v 3399  df-sbc 3680  df-csb 3789  df-dif 3844  df-un 3846  df-in 3848  df-ss 3858  df-pss 3860  df-nul 4210  df-if 4412  df-pw 4487  df-sn 4514  df-pr 4516  df-tp 4518  df-op 4520  df-uni 4794  df-iun 4880  df-br 5028  df-opab 5090  df-mpt 5108  df-tr 5134  df-id 5425  df-eprel 5430  df-po 5438  df-so 5439  df-fr 5478  df-we 5480  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-pred 6123  df-ord 6169  df-on 6170  df-lim 6171  df-suc 6172  df-iota 6291  df-fun 6335  df-fn 6336  df-f 6337  df-f1 6338  df-fo 6339  df-f1o 6340  df-fv 6341  df-ov 7167  df-om 7594  df-wrecs 7969  df-recs 8030  df-rdg 8068  df-er 8313  df-en 8549  df-dom 8550  df-sdom 8551  df-pnf 10748  df-mnf 10749  df-ltxr 10751  df-nn 11710  df-n0 11970

This theorem is referenced by:  quoremnn0ALT  13309  expmulz  13560  faclbnd4lem3  13740  oddge22np1  15787  mulgcd  15985  rpmulgcd2  16090  hashgcdlem  16218  odzdvds  16225  prmreclem3  16347  vdwapf  16401  vdwlem5  16414  vdwlem6  16415  smndex2dbas  18188  odmodnn0  18779  odmulg  18794  odadd  19082  ablfacrplem  19299  ablfacrp2  19301  mhppwdeg  20937  2lgslem1c  26121  2lgslem3a  26124  2lgslem3b  26125  2lgslem3c  26126  2lgslem3d  26127  dchrisumlem1  26217  eulerpartlemsv2  31887  eulerpartlemsf  31888  eulerpartlems  31889  eulerpartlemv  31893  eulerpartlemb  31897  breprexplemc  32174  erdsze2lem1  32728  erdsze2lem2  32729  lcmineqlem17  39662  lcmineqlem18  39663  lcmineqlem20  39665  lcmineqlem21  39666  lcmineqlem22  39667  2np3bcnp1  39695  2ap1caineq  39696  3cubeslem3l  40064  3cubeslem3r  40065  pell1qrge1  40248  jm2.27c  40385  rmxdiophlem  40393  stoweidlem1  43068  wallispilem4  43135  wallispilem5  43136  wallispi2lem2  43139  stirlinglem3  43143  stirlinglem5  43145  stirlinglem7  43147  stirlinglem10  43150  stirlinglem11  43151  etransclem32  43333  etransclem44  43345  etransclem46  43347  fmtnofac2lem  44538  fmtnofac1  44540  2pwp1prm  44559  lighneallem3  44577  fppr2odd  44701  ply1mulgsumlem2  45246  itcovalpclem2  45535  itcovalt2lem2lem1  45537  itcovalt2lem2lem2  45538