Theorem nn0mulcld 12519

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 12490	. 2 ⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0) → (𝐴 · 𝐵) ∈ ℕ0)
4	1, 2, 3	syl2anc 584	1 ⊢ (𝜑 → (𝐴 · 𝐵) ∈ ℕ0)

Syntax hints:   → wi 4   ∈ wcel 2106  (class class class)co 7393   · cmul 11097  ℕ₀cn0 12454

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2702  ax-sep 5292  ax-nul 5299  ax-pow 5356  ax-pr 5420  ax-un 7708  ax-resscn 11149  ax-1cn 11150  ax-icn 11151  ax-addcl 11152  ax-addrcl 11153  ax-mulcl 11154  ax-mulrcl 11155  ax-mulcom 11156  ax-addass 11157  ax-mulass 11158  ax-distr 11159  ax-i2m1 11160  ax-1ne0 11161  ax-1rid 11162  ax-rnegex 11163  ax-rrecex 11164  ax-cnre 11165  ax-pre-lttri 11166  ax-pre-lttrn 11167  ax-pre-ltadd 11168

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-reu 3376  df-rab 3432  df-v 3475  df-sbc 3774  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3963  df-nul 4319  df-if 4523  df-pw 4598  df-sn 4623  df-pr 4625  df-op 4629  df-uni 4902  df-iun 4992  df-br 5142  df-opab 5204  df-mpt 5225  df-tr 5259  df-id 5567  df-eprel 5573  df-po 5581  df-so 5582  df-fr 5624  df-we 5626  df-xp 5675  df-rel 5676  df-cnv 5677  df-co 5678  df-dm 5679  df-rn 5680  df-res 5681  df-ima 5682  df-pred 6289  df-ord 6356  df-on 6357  df-lim 6358  df-suc 6359  df-iota 6484  df-fun 6534  df-fn 6535  df-f 6536  df-f1 6537  df-fo 6538  df-f1o 6539  df-fv 6540  df-ov 7396  df-om 7839  df-2nd 7958  df-frecs 8248  df-wrecs 8279  df-recs 8353  df-rdg 8392  df-er 8686  df-en 8923  df-dom 8924  df-sdom 8925  df-pnf 11232  df-mnf 11233  df-ltxr 11235  df-nn 12195  df-n0 12455

This theorem is referenced by:  quoremnn0ALT  13804  expmulz  14056  faclbnd4lem3  14237  oddge22np1  16274  mulgcd  16472  rpmulgcd2  16575  hashgcdlem  16703  odzdvds  16710  prmreclem3  16833  vdwapf  16887  vdwlem5  16900  vdwlem6  16901  smndex2dbas  18770  odmodnn0  19372  odmulg  19388  odadd  19678  ablfacrplem  19894  ablfacrp2  19896  mhppwdeg  21622  2lgslem1c  26823  2lgslem3a  26826  2lgslem3b  26827  2lgslem3c  26828  2lgslem3d  26829  dchrisumlem1  26919  eulerpartlemsv2  33188  eulerpartlemsf  33189  eulerpartlems  33190  eulerpartlemv  33194  eulerpartlemb  33198  breprexplemc  33475  erdsze2lem1  34025  erdsze2lem2  34026  lcmineqlem17  40715  lcmineqlem18  40716  lcmineqlem20  40718  lcmineqlem21  40719  lcmineqlem22  40720  2np3bcnp1  40765  2ap1caineq  40766  3cubeslem3l  41195  3cubeslem3r  41196  pell1qrge1  41379  jm2.27c  41517  rmxdiophlem  41525  stoweidlem1  44490  wallispilem4  44557  wallispilem5  44558  wallispi2lem2  44561  stirlinglem3  44565  stirlinglem5  44567  stirlinglem7  44569  stirlinglem10  44572  stirlinglem11  44573  etransclem32  44755  etransclem44  44767  etransclem46  44769  fmtnofac2lem  46008  fmtnofac1  46010  2pwp1prm  46029  lighneallem3  46047  fppr2odd  46171  ply1mulgsumlem2  46716  itcovalpclem2  47005  itcovalt2lem2lem1  47007  itcovalt2lem2lem2  47008