Metamath Proof Explorer

Theorem nprmdvdsfacm1

Description: A non-prime integer greater than 5 divides the factorial of the integer decreased by 1 (see remark in Ribenboim p. 181). Note: not valid for N = 4 , but for N = 1 ! (Contributed by AV, 7-Apr-2026)

Ref Expression
Assertion nprmdvdsfacm1 
|- ( ( N e. ( ZZ>= ` 6 ) /\ N e/ Prime ) -> N || ( ! ` ( N - 1 ) ) )

Proof

Step Hyp Ref Expression
1 4z 
 |-  4 e. ZZ
2 6nn 
 |-  6 e. NN
3 2 nnzi 
 |-  6 e. ZZ
4 4re 
 |-  4 e. RR
5 6re 
 |-  6 e. RR
6 4lt6 
 |-  4 < 6
7 4 5 6 ltleii 
 |-  4 <_ 6
8 eluz2 
 |-  ( 6 e. ( ZZ>= ` 4 ) <-> ( 4 e. ZZ /\ 6 e. ZZ /\ 4 <_ 6 ) )
9 1 3 7 8 mpbir3an 
 |-  6 e. ( ZZ>= ` 4 )
10 uzss 
 |-  ( 6 e. ( ZZ>= ` 4 ) -> ( ZZ>= ` 6 ) C_ ( ZZ>= ` 4 ) )
11 9 10 ax-mp 
 |-  ( ZZ>= ` 6 ) C_ ( ZZ>= ` 4 )
12 11 sseli 
 |-  ( N e. ( ZZ>= ` 6 ) -> N e. ( ZZ>= ` 4 ) )
13 nprmmul3 
 |-  ( N e. ( ZZ>= ` 4 ) -> ( N e/ Prime <-> ( E. a e. ( 2 ..^ N ) E. b e. ( 2 ..^ N ) ( a < b /\ N = ( a x. b ) ) \/ E. a e. ( 2 ..^ N ) N = ( a ^ 2 ) ) ) )
14 12 13 syl 
 |-  ( N e. ( ZZ>= ` 6 ) -> ( N e/ Prime <-> ( E. a e. ( 2 ..^ N ) E. b e. ( 2 ..^ N ) ( a < b /\ N = ( a x. b ) ) \/ E. a e. ( 2 ..^ N ) N = ( a ^ 2 ) ) ) )
15 elfzo2nn 
 |-  ( a e. ( 2 ..^ N ) -> a e. NN )
16 15 ad2antrl 
 |-  ( ( N e. ( ZZ>= ` 6 ) /\ ( a e. ( 2 ..^ N ) /\ b e. ( 2 ..^ N ) ) ) -> a e. NN )
17 16 adantr 
 |-  ( ( ( N e. ( ZZ>= ` 6 ) /\ ( a e. ( 2 ..^ N ) /\ b e. ( 2 ..^ N ) ) ) /\ ( a < b /\ N = ( a x. b ) ) ) -> a e. NN )
18 elfzo2nn 
 |-  ( b e. ( 2 ..^ N ) -> b e. NN )
19 18 ad2antll 
 |-  ( ( N e. ( ZZ>= ` 6 ) /\ ( a e. ( 2 ..^ N ) /\ b e. ( 2 ..^ N ) ) ) -> b e. NN )
20 19 adantr 
 |-  ( ( ( N e. ( ZZ>= ` 6 ) /\ ( a e. ( 2 ..^ N ) /\ b e. ( 2 ..^ N ) ) ) /\ ( a < b /\ N = ( a x. b ) ) ) -> b e. NN )
21 simprl 
 |-  ( ( ( N e. ( ZZ>= ` 6 ) /\ ( a e. ( 2 ..^ N ) /\ b e. ( 2 ..^ N ) ) ) /\ ( a < b /\ N = ( a x. b ) ) ) -> a < b )
22 elfzo1 
 |-  ( a e. ( 1 ..^ b ) <-> ( a e. NN /\ b e. NN /\ a < b ) )
23 17 20 21 22 syl3anbrc 
 |-  ( ( ( N e. ( ZZ>= ` 6 ) /\ ( a e. ( 2 ..^ N ) /\ b e. ( 2 ..^ N ) ) ) /\ ( a < b /\ N = ( a x. b ) ) ) -> a e. ( 1 ..^ b ) )
24 2eluzge1 
 |-  2 e. ( ZZ>= ` 1 )
25 fzoss1 
 |-  ( 2 e. ( ZZ>= ` 1 ) -> ( 2 ..^ N ) C_ ( 1 ..^ N ) )
26 24 25 ax-mp 
 |-  ( 2 ..^ N ) C_ ( 1 ..^ N )
27 26 sseli 
 |-  ( b e. ( 2 ..^ N ) -> b e. ( 1 ..^ N ) )
28 27 ad2antll 
 |-  ( ( N e. ( ZZ>= ` 6 ) /\ ( a e. ( 2 ..^ N ) /\ b e. ( 2 ..^ N ) ) ) -> b e. ( 1 ..^ N ) )
29 28 adantr 
 |-  ( ( ( N e. ( ZZ>= ` 6 ) /\ ( a e. ( 2 ..^ N ) /\ b e. ( 2 ..^ N ) ) ) /\ ( a < b /\ N = ( a x. b ) ) ) -> b e. ( 1 ..^ N ) )
30 muldvdsfacm1 
 |-  ( ( a e. ( 1 ..^ b ) /\ b e. ( 1 ..^ N ) ) -> ( a x. b ) || ( ! ` ( N - 1 ) ) )
31 23 29 30 syl2anc 
 |-  ( ( ( N e. ( ZZ>= ` 6 ) /\ ( a e. ( 2 ..^ N ) /\ b e. ( 2 ..^ N ) ) ) /\ ( a < b /\ N = ( a x. b ) ) ) -> ( a x. b ) || ( ! ` ( N - 1 ) ) )
32 breq1 
 |-  ( N = ( a x. b ) -> ( N || ( ! ` ( N - 1 ) ) <-> ( a x. b ) || ( ! ` ( N - 1 ) ) ) )
33 32 ad2antll 
 |-  ( ( ( N e. ( ZZ>= ` 6 ) /\ ( a e. ( 2 ..^ N ) /\ b e. ( 2 ..^ N ) ) ) /\ ( a < b /\ N = ( a x. b ) ) ) -> ( N || ( ! ` ( N - 1 ) ) <-> ( a x. b ) || ( ! ` ( N - 1 ) ) ) )
34 31 33 mpbird 
 |-  ( ( ( N e. ( ZZ>= ` 6 ) /\ ( a e. ( 2 ..^ N ) /\ b e. ( 2 ..^ N ) ) ) /\ ( a < b /\ N = ( a x. b ) ) ) -> N || ( ! ` ( N - 1 ) ) )
35 34 ex 
 |-  ( ( N e. ( ZZ>= ` 6 ) /\ ( a e. ( 2 ..^ N ) /\ b e. ( 2 ..^ N ) ) ) -> ( ( a < b /\ N = ( a x. b ) ) -> N || ( ! ` ( N - 1 ) ) ) )
36 35 rexlimdvva 
 |-  ( N e. ( ZZ>= ` 6 ) -> ( E. a e. ( 2 ..^ N ) E. b e. ( 2 ..^ N ) ( a < b /\ N = ( a x. b ) ) -> N || ( ! ` ( N - 1 ) ) ) )
37 nprmdvdsfacm1lem4 
 |-  ( ( N e. ( ZZ>= ` 6 ) /\ a e. ( 2 ..^ N ) /\ N = ( a ^ 2 ) ) -> N || ( ! ` ( N - 1 ) ) )
38 37 3expia 
 |-  ( ( N e. ( ZZ>= ` 6 ) /\ a e. ( 2 ..^ N ) ) -> ( N = ( a ^ 2 ) -> N || ( ! ` ( N - 1 ) ) ) )
39 38 rexlimdva 
 |-  ( N e. ( ZZ>= ` 6 ) -> ( E. a e. ( 2 ..^ N ) N = ( a ^ 2 ) -> N || ( ! ` ( N - 1 ) ) ) )
40 36 39 jaod 
 |-  ( N e. ( ZZ>= ` 6 ) -> ( ( E. a e. ( 2 ..^ N ) E. b e. ( 2 ..^ N ) ( a < b /\ N = ( a x. b ) ) \/ E. a e. ( 2 ..^ N ) N = ( a ^ 2 ) ) -> N || ( ! ` ( N - 1 ) ) ) )
41 14 40 sylbid 
 |-  ( N e. ( ZZ>= ` 6 ) -> ( N e/ Prime -> N || ( ! ` ( N - 1 ) ) ) )
42 41 imp 
 |-  ( ( N e. ( ZZ>= ` 6 ) /\ N e/ Prime ) -> N || ( ! ` ( N - 1 ) ) )