Metamath Proof Explorer

Theorem wilthimp

Description: The forward implication of Wilson's theorem wilth (see wilthlem3 ), expressed using the modulo operation: For any prime p we have ( p - 1 ) ! == - 1 (mod p ), see theorem 5.24 in ApostolNT p. 116. (Contributed by AV, 21-Jul-2021)

Ref Expression
Assertion wilthimp 
|- ( P e. Prime -> ( ( ! ` ( P - 1 ) ) mod P ) = ( -u 1 mod P ) )

Proof

Step Hyp Ref Expression
1 wilth 
 |-  ( P e. Prime <-> ( P e. ( ZZ>= ` 2 ) /\ P || ( ( ! ` ( P - 1 ) ) + 1 ) ) )
2 eluz2nn 
 |-  ( P e. ( ZZ>= ` 2 ) -> P e. NN )
3 nnm1nn0 
 |-  ( P e. NN -> ( P - 1 ) e. NN0 )
4 2 3 syl 
 |-  ( P e. ( ZZ>= ` 2 ) -> ( P - 1 ) e. NN0 )
5 4 faccld 
 |-  ( P e. ( ZZ>= ` 2 ) -> ( ! ` ( P - 1 ) ) e. NN )
6 5 nnzd 
 |-  ( P e. ( ZZ>= ` 2 ) -> ( ! ` ( P - 1 ) ) e. ZZ )
7 6 peano2zd 
 |-  ( P e. ( ZZ>= ` 2 ) -> ( ( ! ` ( P - 1 ) ) + 1 ) e. ZZ )
8 dvdsval3 
 |-  ( ( P e. NN /\ ( ( ! ` ( P - 1 ) ) + 1 ) e. ZZ ) -> ( P || ( ( ! ` ( P - 1 ) ) + 1 ) <-> ( ( ( ! ` ( P - 1 ) ) + 1 ) mod P ) = 0 ) )
9 2 7 8 syl2anc 
 |-  ( P e. ( ZZ>= ` 2 ) -> ( P || ( ( ! ` ( P - 1 ) ) + 1 ) <-> ( ( ( ! ` ( P - 1 ) ) + 1 ) mod P ) = 0 ) )
10 9 biimpar 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ ( ( ( ! ` ( P - 1 ) ) + 1 ) mod P ) = 0 ) -> P || ( ( ! ` ( P - 1 ) ) + 1 ) )
11 5 nncnd 
 |-  ( P e. ( ZZ>= ` 2 ) -> ( ! ` ( P - 1 ) ) e. CC )
12 1cnd 
 |-  ( P e. ( ZZ>= ` 2 ) -> 1 e. CC )
13 11 12 jca 
 |-  ( P e. ( ZZ>= ` 2 ) -> ( ( ! ` ( P - 1 ) ) e. CC /\ 1 e. CC ) )
14 13 adantr 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ ( ( ( ! ` ( P - 1 ) ) + 1 ) mod P ) = 0 ) -> ( ( ! ` ( P - 1 ) ) e. CC /\ 1 e. CC ) )
15 subneg 
 |-  ( ( ( ! ` ( P - 1 ) ) e. CC /\ 1 e. CC ) -> ( ( ! ` ( P - 1 ) ) - -u 1 ) = ( ( ! ` ( P - 1 ) ) + 1 ) )
16 14 15 syl 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ ( ( ( ! ` ( P - 1 ) ) + 1 ) mod P ) = 0 ) -> ( ( ! ` ( P - 1 ) ) - -u 1 ) = ( ( ! ` ( P - 1 ) ) + 1 ) )
17 10 16 breqtrrd 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ ( ( ( ! ` ( P - 1 ) ) + 1 ) mod P ) = 0 ) -> P || ( ( ! ` ( P - 1 ) ) - -u 1 ) )
18 neg1z 
 |-  -u 1 e. ZZ
19 18 a1i 
 |-  ( P e. ( ZZ>= ` 2 ) -> -u 1 e. ZZ )
20 2 6 19 3jca 
 |-  ( P e. ( ZZ>= ` 2 ) -> ( P e. NN /\ ( ! ` ( P - 1 ) ) e. ZZ /\ -u 1 e. ZZ ) )
21 20 adantr 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ ( ( ( ! ` ( P - 1 ) ) + 1 ) mod P ) = 0 ) -> ( P e. NN /\ ( ! ` ( P - 1 ) ) e. ZZ /\ -u 1 e. ZZ ) )
22 moddvds 
 |-  ( ( P e. NN /\ ( ! ` ( P - 1 ) ) e. ZZ /\ -u 1 e. ZZ ) -> ( ( ( ! ` ( P - 1 ) ) mod P ) = ( -u 1 mod P ) <-> P || ( ( ! ` ( P - 1 ) ) - -u 1 ) ) )
23 21 22 syl 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ ( ( ( ! ` ( P - 1 ) ) + 1 ) mod P ) = 0 ) -> ( ( ( ! ` ( P - 1 ) ) mod P ) = ( -u 1 mod P ) <-> P || ( ( ! ` ( P - 1 ) ) - -u 1 ) ) )
24 17 23 mpbird 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ ( ( ( ! ` ( P - 1 ) ) + 1 ) mod P ) = 0 ) -> ( ( ! ` ( P - 1 ) ) mod P ) = ( -u 1 mod P ) )
25 24 ex 
 |-  ( P e. ( ZZ>= ` 2 ) -> ( ( ( ( ! ` ( P - 1 ) ) + 1 ) mod P ) = 0 -> ( ( ! ` ( P - 1 ) ) mod P ) = ( -u 1 mod P ) ) )
26 9 25 sylbid 
 |-  ( P e. ( ZZ>= ` 2 ) -> ( P || ( ( ! ` ( P - 1 ) ) + 1 ) -> ( ( ! ` ( P - 1 ) ) mod P ) = ( -u 1 mod P ) ) )
27 26 imp 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ P || ( ( ! ` ( P - 1 ) ) + 1 ) ) -> ( ( ! ` ( P - 1 ) ) mod P ) = ( -u 1 mod P ) )
28 1 27 sylbi 
 |-  ( P e. Prime -> ( ( ! ` ( P - 1 ) ) mod P ) = ( -u 1 mod P ) )