This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) → ( 𝑁 < 𝑃 → ¬ 𝑃 ∥ ( ! ‘ 𝑁 ) ) )