Theorem faccld 14246

Description: Closure of the factorial function, deduction version of faccl 14245. (Contributed by Glauco Siliprandi, 5-Apr-2020.)

Hypothesis

Ref	Expression
faccld.1	⊢ (𝜑 → 𝑁 ∈ ℕ0)

Assertion

Ref	Expression
faccld	⊢ (𝜑 → (!‘𝑁) ∈ ℕ)

Proof of Theorem faccld

Step	Hyp	Ref	Expression
1		faccld.1	. 2 ⊢ (𝜑 → 𝑁 ∈ ℕ0)
2		faccl 14245	. 2 ⊢ (𝑁 ∈ ℕ0 → (!‘𝑁) ∈ ℕ)
3	1, 2	syl 17	1 ⊢ (𝜑 → (!‘𝑁) ∈ ℕ)

Syntax hints:   → wi 4   ∈ wcel 2114  ‘cfv 6498  ℕcn 12174  ℕ₀cn0 12437  !cfa 14235

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708  ax-sep 5231  ax-nul 5241  ax-pow 5307  ax-pr 5375  ax-un 7689  ax-cnex 11094  ax-resscn 11095  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-addrcl 11099  ax-mulcl 11100  ax-mulrcl 11101  ax-mulcom 11102  ax-addass 11103  ax-mulass 11104  ax-distr 11105  ax-i2m1 11106  ax-1ne0 11107  ax-1rid 11108  ax-rnegex 11109  ax-rrecex 11110  ax-cnre 11111  ax-pre-lttri 11112  ax-pre-lttrn 11113  ax-pre-ltadd 11114  ax-pre-mulgt0 11115

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3062  df-reu 3343  df-rab 3390  df-v 3431  df-sbc 3729  df-csb 3838  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-pss 3909  df-nul 4274  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-iun 4935  df-br 5086  df-opab 5148  df-mpt 5167  df-tr 5193  df-id 5526  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5584  df-we 5586  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6265  df-ord 6326  df-on 6327  df-lim 6328  df-suc 6329  df-iota 6454  df-fun 6500  df-fn 6501  df-f 6502  df-f1 6503  df-fo 6504  df-f1o 6505  df-fv 6506  df-riota 7324  df-ov 7370  df-oprab 7371  df-mpo 7372  df-om 7818  df-2nd 7943  df-frecs 8231  df-wrecs 8262  df-recs 8311  df-rdg 8349  df-er 8643  df-en 8894  df-dom 8895  df-sdom 8896  df-pnf 11181  df-mnf 11182  df-xr 11183  df-ltxr 11184  df-le 11185  df-sub 11379  df-neg 11380  df-nn 12175  df-n0 12438  df-z 12525  df-uz 12789  df-seq 13964  df-fac 14236

This theorem is referenced by:  facmapnn  14247  facwordi  14251  faclbnd  14252  faclbnd6  14261  facavg  14263  bcrpcl  14270  bccmpl  14271  bcn1  14275  bcm1k  14277  bcp1n  14278  bcval5  14280  permnn  14288  hashf1  14419  hashfac  14420  bcfallfac  16009  efcllem  16042  eftlub  16076  eirrlem  16171  dvdsfac  16295  lcmflefac  16617  prmdvdsbc  16696  pcbc  16871  infpnlem1  16881  infpnlem2  16882  prmgaplem1  17020  prmgaplem2  17021  2expltfac  17063  gexcl3  19562  aaliou3lem1  26308  aaliou3lem2  26309  aaliou3lem3  26310  aaliou3lem8  26311  aaliou3lem5  26313  aaliou3lem6  26314  taylfvallem1  26322  tayl0  26327  taylply2  26333  taylply  26334  dvtaylp  26335  taylthlem2  26339  advlogexp  26619  birthdaylem2  26916  wilthlem3  27033  wilthimp  27035  chtublem  27174  logfacubnd  27184  logfaclbnd  27185  logfacbnd3  27186  logexprlim  27188  bposlem3  27249  gausslemma2dlem0c  27321  gausslemma2dlem6  27335  gausslemma2dlem7  27336  2np3bcnp1  42583  bcled  42617  bcle2d  42618  mccllem  46027  dvnprodlem2  46375  etransclem14  46676  etransclem15  46677  etransclem20  46682  etransclem21  46683  etransclem22  46684  etransclem23  46685  etransclem24  46686  etransclem25  46687  etransclem28  46690  etransclem31  46693  etransclem32  46694  etransclem33  46695  etransclem34  46696  etransclem35  46697  etransclem37  46699  etransclem38  46700  etransclem41  46703  etransclem44  46706  etransclem45  46707  etransclem47  46709  etransclem48  46710  nthrucw  47316  muldvdsfacm1  47835  nprmdvdsfacm1lem4  48086  ppivalnnprm  48088  ppivalnnnprmge6  48089