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	$⊢ (P \in ℙ \land N \in ℕ_{0}) \to (N < P \to \neg P ∥ N!)$

Step	Hyp	Ref	Expression
1		nn0re	$⊢ N \in ℕ_{0} \to N \in ℝ$
2		prmnn	$⊢ P \in ℙ \to P \in ℕ$
3	2	nnred	$⊢ P \in ℙ \to P \in ℝ$
4		ltnle	$⊢ (N \in ℝ \land P \in ℝ) \to (N < P \leftrightarrow \neg P \leq N)$
5	1 3 4	syl2anr	$⊢ (P \in ℙ \land N \in ℕ_{0}) \to (N < P \leftrightarrow \neg P \leq N)$
6		prmfac1	$⊢ (N \in ℕ_{0} \land P \in ℙ \land P ∥ N!) \to P \leq N$
7	6	3exp	$⊢ N \in ℕ_{0} \to (P \in ℙ \to (P ∥ N! \to P \leq N))$
8	7	impcom	$⊢ (P \in ℙ \land N \in ℕ_{0}) \to (P ∥ N! \to P \leq N)$
9	8	con3d	$⊢ (P \in ℙ \land N \in ℕ_{0}) \to (\neg P \leq N \to \neg P ∥ N!)$
10	5 9	sylbid	$⊢ (P \in ℙ \land N \in ℕ_{0}) \to (N < P \to \neg P ∥ N!)$

Metamath Proof Explorer