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	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ0 ) → ( 𝑁 < 𝑃 → ¬ 𝑃 ∥ ( ! ‘ 𝑁 ) ) )

Proof

Step	Hyp	Ref	Expression
1		nn0re	⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℝ )
2		prmnn	⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ )
3	2	nnred	⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℝ )
4		ltnle	⊢ ( ( 𝑁 ∈ ℝ ∧ 𝑃 ∈ ℝ ) → ( 𝑁 < 𝑃 ↔ ¬ 𝑃 ≤ 𝑁 ) )
5	1 3 4	syl2anr	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ0 ) → ( 𝑁 < 𝑃 ↔ ¬ 𝑃 ≤ 𝑁 ) )
6		prmfac1	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( ! ‘ 𝑁 ) ) → 𝑃 ≤ 𝑁 )
7	6	3exp	⊢ ( 𝑁 ∈ ℕ0 → ( 𝑃 ∈ ℙ → ( 𝑃 ∥ ( ! ‘ 𝑁 ) → 𝑃 ≤ 𝑁 ) ) )
8	7	impcom	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ0 ) → ( 𝑃 ∥ ( ! ‘ 𝑁 ) → 𝑃 ≤ 𝑁 ) )
9	8	con3d	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ0 ) → ( ¬ 𝑃 ≤ 𝑁 → ¬ 𝑃 ∥ ( ! ‘ 𝑁 ) ) )
10	5 9	sylbid	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ0 ) → ( 𝑁 < 𝑃 → ¬ 𝑃 ∥ ( ! ‘ 𝑁 ) ) )