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	|- ( ( P e. Prime /\ N e. NN0 ) -> ( N < P -> -. P || ( ! ` N ) ) )

Proof

Step	Hyp	Ref	Expression
1		nn0re	|- ( N e. NN0 -> N e. RR )
2		prmnn	|- ( P e. Prime -> P e. NN )
3	2	nnred	|- ( P e. Prime -> P e. RR )
4		ltnle	|- ( ( N e. RR /\ P e. RR ) -> ( N < P <-> -. P <_ N ) )
5	1 3 4	syl2anr	|- ( ( P e. Prime /\ N e. NN0 ) -> ( N < P <-> -. P <_ N ) )
6		prmfac1	|- ( ( N e. NN0 /\ P e. Prime /\ P || ( ! ` N ) ) -> P <_ N )
7	6	3exp	|- ( N e. NN0 -> ( P e. Prime -> ( P || ( ! ` N ) -> P <_ N ) ) )
8	7	impcom	|- ( ( P e. Prime /\ N e. NN0 ) -> ( P || ( ! ` N ) -> P <_ N ) )
9	8	con3d	|- ( ( P e. Prime /\ N e. NN0 ) -> ( -. P <_ N -> -. P || ( ! ` N ) ) )
10	5 9	sylbid	|- ( ( P e. Prime /\ N e. NN0 ) -> ( N < P -> -. P || ( ! ` N ) ) )