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 
|- ( ( 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 ) ) )