Theorem prmndvdsfaclt

Description: A prime number does not divide the factorial of a nonnegative integer less than the prime number. (Contributed by AV, 13-Jul-2021)

	Ref	Expression
Assertion	prmndvdsfaclt	$$⊢\left(P\in \mathbb{P}\wedge N\in {\mathbb{N}}_0\right)\to \left(N<P\to \neg P\parallel N!\right)$$

Proof

Step	Hyp	Ref	Expression
1		nn0re	$$⊢N\in {\mathbb{N}}_0\to N\in ℝ$$
2		prmnn	$$⊢P\in \mathbb{P}\to P\in \mathbb{N}$$
3	2	nnred	$$⊢P\in \mathbb{P}\to P\in ℝ$$
4		ltnle	$$⊢\left(N\in ℝ\wedge P\in ℝ\right)\to \left(N<P\leftrightarrow \neg P\le N\right)$$
5	1 3 4	syl2anr	$$⊢\left(P\in \mathbb{P}\wedge N\in {\mathbb{N}}_0\right)\to \left(N<P\leftrightarrow \neg P\le N\right)$$
6		prmfac1	$$⊢\left(N\in {\mathbb{N}}_0\wedge P\in \mathbb{P}\wedge P\parallel N!\right)\to P\le N$$
7	6	3exp	$$⊢N\in {\mathbb{N}}_0\to \left(P\in \mathbb{P}\to \left(P\parallel N!\to P\le N\right)\right)$$
8	7	impcom	$$⊢\left(P\in \mathbb{P}\wedge N\in {\mathbb{N}}_0\right)\to \left(P\parallel N!\to P\le N\right)$$
9	8	con3d	$$⊢\left(P\in \mathbb{P}\wedge N\in {\mathbb{N}}_0\right)\to \left(\neg P\le N\to \neg P\parallel N!\right)$$
10	5 9	sylbid	$$⊢\left(P\in \mathbb{P}\wedge N\in {\mathbb{N}}_0\right)\to \left(N<P\to \neg P\parallel N!\right)$$