Metamath Proof Explorer

Theorem wilth

Description: Wilson's theorem. A number is prime iff it is greater than or equal to 2 and ( N - 1 ) ! is congruent to -u 1 , mod N , or alternatively if N divides ( N - 1 ) ! + 1 . In this part of the proof we show the relatively simple reverse implication; see wilthlem3 for the forward implication. This is Metamath 100 proof #51. (Contributed by Mario Carneiro, 24-Jan-2015) (Proof shortened by Fan Zheng, 16-Jun-2016)

Ref Expression
Assertion wilth 
|- ( N e. Prime <-> ( N e. ( ZZ>= ` 2 ) /\ N || ( ( ! ` ( N - 1 ) ) + 1 ) ) )

Proof

Step Hyp Ref Expression
1 prmuz2 
 |-  ( N e. Prime -> N e. ( ZZ>= ` 2 ) )
2 eqid 
 |-  ( mulGrp ` CCfld ) = ( mulGrp ` CCfld )
3 eleq2w 
 |-  ( z = x -> ( ( N - 1 ) e. z <-> ( N - 1 ) e. x ) )
4 oveq1 
 |-  ( n = y -> ( n ^ ( N - 2 ) ) = ( y ^ ( N - 2 ) ) )
5 4 oveq1d 
 |-  ( n = y -> ( ( n ^ ( N - 2 ) ) mod N ) = ( ( y ^ ( N - 2 ) ) mod N ) )
6 5 eleq1d 
 |-  ( n = y -> ( ( ( n ^ ( N - 2 ) ) mod N ) e. z <-> ( ( y ^ ( N - 2 ) ) mod N ) e. z ) )
7 6 cbvralvw 
 |-  ( A. n e. z ( ( n ^ ( N - 2 ) ) mod N ) e. z <-> A. y e. z ( ( y ^ ( N - 2 ) ) mod N ) e. z )
8 eleq2w 
 |-  ( z = x -> ( ( ( y ^ ( N - 2 ) ) mod N ) e. z <-> ( ( y ^ ( N - 2 ) ) mod N ) e. x ) )
9 8 raleqbi1dv 
 |-  ( z = x -> ( A. y e. z ( ( y ^ ( N - 2 ) ) mod N ) e. z <-> A. y e. x ( ( y ^ ( N - 2 ) ) mod N ) e. x ) )
10 7 9 bitrid 
 |-  ( z = x -> ( A. n e. z ( ( n ^ ( N - 2 ) ) mod N ) e. z <-> A. y e. x ( ( y ^ ( N - 2 ) ) mod N ) e. x ) )
11 3 10 anbi12d 
 |-  ( z = x -> ( ( ( N - 1 ) e. z /\ A. n e. z ( ( n ^ ( N - 2 ) ) mod N ) e. z ) <-> ( ( N - 1 ) e. x /\ A. y e. x ( ( y ^ ( N - 2 ) ) mod N ) e. x ) ) )
12 11 cbvrabv 
 |-  { z e. ~P ( 1 ... ( N - 1 ) ) | ( ( N - 1 ) e. z /\ A. n e. z ( ( n ^ ( N - 2 ) ) mod N ) e. z ) } = { x e. ~P ( 1 ... ( N - 1 ) ) | ( ( N - 1 ) e. x /\ A. y e. x ( ( y ^ ( N - 2 ) ) mod N ) e. x ) }
13 2 12 wilthlem3 
 |-  ( N e. Prime -> N || ( ( ! ` ( N - 1 ) ) + 1 ) )
14 1 13 jca 
 |-  ( N e. Prime -> ( N e. ( ZZ>= ` 2 ) /\ N || ( ( ! ` ( N - 1 ) ) + 1 ) ) )
15 simpl 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ N || ( ( ! ` ( N - 1 ) ) + 1 ) ) -> N e. ( ZZ>= ` 2 ) )
16 elfzuz 
 |-  ( n e. ( 2 ... ( N - 1 ) ) -> n e. ( ZZ>= ` 2 ) )
17 16 adantl 
 |-  ( ( ( N e. ( ZZ>= ` 2 ) /\ N || ( ( ! ` ( N - 1 ) ) + 1 ) ) /\ n e. ( 2 ... ( N - 1 ) ) ) -> n e. ( ZZ>= ` 2 ) )
18 eluz2nn 
 |-  ( n e. ( ZZ>= ` 2 ) -> n e. NN )
19 17 18 syl 
 |-  ( ( ( N e. ( ZZ>= ` 2 ) /\ N || ( ( ! ` ( N - 1 ) ) + 1 ) ) /\ n e. ( 2 ... ( N - 1 ) ) ) -> n e. NN )
20 elfzuz3 
 |-  ( n e. ( 2 ... ( N - 1 ) ) -> ( N - 1 ) e. ( ZZ>= ` n ) )
21 20 adantl 
 |-  ( ( ( N e. ( ZZ>= ` 2 ) /\ N || ( ( ! ` ( N - 1 ) ) + 1 ) ) /\ n e. ( 2 ... ( N - 1 ) ) ) -> ( N - 1 ) e. ( ZZ>= ` n ) )
22 dvdsfac 
 |-  ( ( n e. NN /\ ( N - 1 ) e. ( ZZ>= ` n ) ) -> n || ( ! ` ( N - 1 ) ) )
23 19 21 22 syl2anc 
 |-  ( ( ( N e. ( ZZ>= ` 2 ) /\ N || ( ( ! ` ( N - 1 ) ) + 1 ) ) /\ n e. ( 2 ... ( N - 1 ) ) ) -> n || ( ! ` ( N - 1 ) ) )
24 eluz2nn 
 |-  ( N e. ( ZZ>= ` 2 ) -> N e. NN )
25 24 ad2antrr 
 |-  ( ( ( N e. ( ZZ>= ` 2 ) /\ N || ( ( ! ` ( N - 1 ) ) + 1 ) ) /\ n e. ( 2 ... ( N - 1 ) ) ) -> N e. NN )
26 nnm1nn0 
 |-  ( N e. NN -> ( N - 1 ) e. NN0 )
27 faccl 
 |-  ( ( N - 1 ) e. NN0 -> ( ! ` ( N - 1 ) ) e. NN )
28 25 26 27 3syl 
 |-  ( ( ( N e. ( ZZ>= ` 2 ) /\ N || ( ( ! ` ( N - 1 ) ) + 1 ) ) /\ n e. ( 2 ... ( N - 1 ) ) ) -> ( ! ` ( N - 1 ) ) e. NN )
29 28 nnzd 
 |-  ( ( ( N e. ( ZZ>= ` 2 ) /\ N || ( ( ! ` ( N - 1 ) ) + 1 ) ) /\ n e. ( 2 ... ( N - 1 ) ) ) -> ( ! ` ( N - 1 ) ) e. ZZ )
30 eluz2gt1 
 |-  ( n e. ( ZZ>= ` 2 ) -> 1 < n )
31 17 30 syl 
 |-  ( ( ( N e. ( ZZ>= ` 2 ) /\ N || ( ( ! ` ( N - 1 ) ) + 1 ) ) /\ n e. ( 2 ... ( N - 1 ) ) ) -> 1 < n )
32 ndvdsp1 
 |-  ( ( ( ! ` ( N - 1 ) ) e. ZZ /\ n e. NN /\ 1 < n ) -> ( n || ( ! ` ( N - 1 ) ) -> -. n || ( ( ! ` ( N - 1 ) ) + 1 ) ) )
33 29 19 31 32 syl3anc 
 |-  ( ( ( N e. ( ZZ>= ` 2 ) /\ N || ( ( ! ` ( N - 1 ) ) + 1 ) ) /\ n e. ( 2 ... ( N - 1 ) ) ) -> ( n || ( ! ` ( N - 1 ) ) -> -. n || ( ( ! ` ( N - 1 ) ) + 1 ) ) )
34 23 33 mpd 
 |-  ( ( ( N e. ( ZZ>= ` 2 ) /\ N || ( ( ! ` ( N - 1 ) ) + 1 ) ) /\ n e. ( 2 ... ( N - 1 ) ) ) -> -. n || ( ( ! ` ( N - 1 ) ) + 1 ) )
35 simplr 
 |-  ( ( ( N e. ( ZZ>= ` 2 ) /\ N || ( ( ! ` ( N - 1 ) ) + 1 ) ) /\ n e. ( 2 ... ( N - 1 ) ) ) -> N || ( ( ! ` ( N - 1 ) ) + 1 ) )
36 19 nnzd 
 |-  ( ( ( N e. ( ZZ>= ` 2 ) /\ N || ( ( ! ` ( N - 1 ) ) + 1 ) ) /\ n e. ( 2 ... ( N - 1 ) ) ) -> n e. ZZ )
37 25 nnzd 
 |-  ( ( ( N e. ( ZZ>= ` 2 ) /\ N || ( ( ! ` ( N - 1 ) ) + 1 ) ) /\ n e. ( 2 ... ( N - 1 ) ) ) -> N e. ZZ )
38 29 peano2zd 
 |-  ( ( ( N e. ( ZZ>= ` 2 ) /\ N || ( ( ! ` ( N - 1 ) ) + 1 ) ) /\ n e. ( 2 ... ( N - 1 ) ) ) -> ( ( ! ` ( N - 1 ) ) + 1 ) e. ZZ )
39 dvdstr 
 |-  ( ( n e. ZZ /\ N e. ZZ /\ ( ( ! ` ( N - 1 ) ) + 1 ) e. ZZ ) -> ( ( n || N /\ N || ( ( ! ` ( N - 1 ) ) + 1 ) ) -> n || ( ( ! ` ( N - 1 ) ) + 1 ) ) )
40 36 37 38 39 syl3anc 
 |-  ( ( ( N e. ( ZZ>= ` 2 ) /\ N || ( ( ! ` ( N - 1 ) ) + 1 ) ) /\ n e. ( 2 ... ( N - 1 ) ) ) -> ( ( n || N /\ N || ( ( ! ` ( N - 1 ) ) + 1 ) ) -> n || ( ( ! ` ( N - 1 ) ) + 1 ) ) )
41 35 40 mpan2d 
 |-  ( ( ( N e. ( ZZ>= ` 2 ) /\ N || ( ( ! ` ( N - 1 ) ) + 1 ) ) /\ n e. ( 2 ... ( N - 1 ) ) ) -> ( n || N -> n || ( ( ! ` ( N - 1 ) ) + 1 ) ) )
42 34 41 mtod 
 |-  ( ( ( N e. ( ZZ>= ` 2 ) /\ N || ( ( ! ` ( N - 1 ) ) + 1 ) ) /\ n e. ( 2 ... ( N - 1 ) ) ) -> -. n || N )
43 42 ralrimiva 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ N || ( ( ! ` ( N - 1 ) ) + 1 ) ) -> A. n e. ( 2 ... ( N - 1 ) ) -. n || N )
44 isprm3 
 |-  ( N e. Prime <-> ( N e. ( ZZ>= ` 2 ) /\ A. n e. ( 2 ... ( N - 1 ) ) -. n || N ) )
45 15 43 44 sylanbrc 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ N || ( ( ! ` ( N - 1 ) ) + 1 ) ) -> N e. Prime )
46 14 45 impbii 
 |-  ( N e. Prime <-> ( N e. ( ZZ>= ` 2 ) /\ N || ( ( ! ` ( N - 1 ) ) + 1 ) ) )