Theorem nnmulcld 9115

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

Hypotheses

Ref	Expression
nnge1d.1	⊢ (𝜑 → 𝐴 ∈ ℕ)
nnmulcld.2	⊢ (𝜑 → 𝐵 ∈ ℕ)

Assertion

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

Proof of Theorem nnmulcld

Step	Hyp	Ref	Expression
1		nnge1d.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℕ)
2		nnmulcld.2	. 2 ⊢ (𝜑 → 𝐵 ∈ ℕ)
3		nnmulcl 9087	. 2 ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (𝐴 · 𝐵) ∈ ℕ)
4	1, 2, 3	syl2anc 411	1 ⊢ (𝜑 → (𝐴 · 𝐵) ∈ ℕ)

Syntax hints:   → wi 4   ∈ wcel 2177  (class class class)co 5962   · cmul 7960  ℕcn 9066

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188  ax-sep 4173  ax-cnex 8046  ax-resscn 8047  ax-1cn 8048  ax-1re 8049  ax-icn 8050  ax-addcl 8051  ax-addrcl 8052  ax-mulcl 8053  ax-mulcom 8056  ax-addass 8057  ax-mulass 8058  ax-distr 8059  ax-1rid 8062  ax-cnre 8066

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-ral 2490  df-rex 2491  df-rab 2494  df-v 2775  df-un 3174  df-in 3176  df-ss 3183  df-sn 3644  df-pr 3645  df-op 3647  df-uni 3860  df-int 3895  df-br 4055  df-iota 5246  df-fv 5293  df-ov 5965  df-inn 9067

This theorem is referenced by:  qbtwnre  10431  bcval  10926  bcm1k  10937  bcp1n  10938  permnn  10948  cvg1nlemcxze  11378  cvg1nlemf  11379  cvg1nlemcau  11380  cvg1nlemres  11381  trireciplem  11896  efaddlem  12070  eftlub  12086  eirraplem  12173  modmulconst  12219  lcmval  12470  oddpwdclemxy  12576  oddpwdclemdc  12580  sqpweven  12582  2sqpwodd  12583  crth  12631  phimullem  12632  modprm0  12662  pcqmul  12711  pcaddlem  12747  pcbc  12759  oddprmdvds  12762  pockthlem  12764  pockthg  12765  4sqlem13m  12811  4sqlem14  12812  4sqlem17  12815  4sqlem18  12816  evenennn  12849  mpodvdsmulf1o  15547  fsumdvdsmul  15548  sgmmul  15553  gausslemma2dlem1a  15620  lgseisenlem2  15633  lgseisenlem4  15635  lgsquadlemsfi  15637  lgsquadlem2  15640  lgsquadlem3  15641  lgsquad2lem2  15644  2sqlem6  15682