Metamath Proof Explorer
Description: Closure of the factorial function, deduction version of faccl .
(Contributed by Glauco Siliprandi, 5Apr2020)


Ref 
Expression 

Hypothesis 
faccld.1 
$${\u22a2}{\phi}\to {N}\in {\mathbb{N}}_{0}$$ 

Assertion 
faccld 
$${\u22a2}{\phi}\to {N}!\in \mathbb{N}$$ 
Proof
Step 
Hyp 
Ref 
Expression 
1 

faccld.1 
$${\u22a2}{\phi}\to {N}\in {\mathbb{N}}_{0}$$ 
2 

faccl 
$${\u22a2}{N}\in {\mathbb{N}}_{0}\to {N}!\in \mathbb{N}$$ 
3 
1 2

syl 
$${\u22a2}{\phi}\to {N}!\in \mathbb{N}$$ 