Metamath Proof Explorer


Theorem wilthlem1

Description: The only elements that are equal to their own inverses in the multiplicative group of nonzero elements in ZZ / P ZZ are 1 and -u 1 == P - 1 . (Note that from prmdiveq , ( N ^ ( P - 2 ) ) mod P is the modular inverse of N in ZZ / P ZZ . (Contributed by Mario Carneiro, 24-Jan-2015)

Ref Expression
Assertion wilthlem1
|- ( ( P e. Prime /\ N e. ( 1 ... ( P - 1 ) ) ) -> ( N = ( ( N ^ ( P - 2 ) ) mod P ) <-> ( N = 1 \/ N = ( P - 1 ) ) ) )

Proof

Step Hyp Ref Expression
1 elfzelz
 |-  ( N e. ( 1 ... ( P - 1 ) ) -> N e. ZZ )
2 1 adantl
 |-  ( ( P e. Prime /\ N e. ( 1 ... ( P - 1 ) ) ) -> N e. ZZ )
3 peano2zm
 |-  ( N e. ZZ -> ( N - 1 ) e. ZZ )
4 2 3 syl
 |-  ( ( P e. Prime /\ N e. ( 1 ... ( P - 1 ) ) ) -> ( N - 1 ) e. ZZ )
5 4 zcnd
 |-  ( ( P e. Prime /\ N e. ( 1 ... ( P - 1 ) ) ) -> ( N - 1 ) e. CC )
6 2 peano2zd
 |-  ( ( P e. Prime /\ N e. ( 1 ... ( P - 1 ) ) ) -> ( N + 1 ) e. ZZ )
7 6 zcnd
 |-  ( ( P e. Prime /\ N e. ( 1 ... ( P - 1 ) ) ) -> ( N + 1 ) e. CC )
8 5 7 mulcomd
 |-  ( ( P e. Prime /\ N e. ( 1 ... ( P - 1 ) ) ) -> ( ( N - 1 ) x. ( N + 1 ) ) = ( ( N + 1 ) x. ( N - 1 ) ) )
9 2 zcnd
 |-  ( ( P e. Prime /\ N e. ( 1 ... ( P - 1 ) ) ) -> N e. CC )
10 ax-1cn
 |-  1 e. CC
11 subsq
 |-  ( ( N e. CC /\ 1 e. CC ) -> ( ( N ^ 2 ) - ( 1 ^ 2 ) ) = ( ( N + 1 ) x. ( N - 1 ) ) )
12 9 10 11 sylancl
 |-  ( ( P e. Prime /\ N e. ( 1 ... ( P - 1 ) ) ) -> ( ( N ^ 2 ) - ( 1 ^ 2 ) ) = ( ( N + 1 ) x. ( N - 1 ) ) )
13 9 sqvald
 |-  ( ( P e. Prime /\ N e. ( 1 ... ( P - 1 ) ) ) -> ( N ^ 2 ) = ( N x. N ) )
14 sq1
 |-  ( 1 ^ 2 ) = 1
15 14 a1i
 |-  ( ( P e. Prime /\ N e. ( 1 ... ( P - 1 ) ) ) -> ( 1 ^ 2 ) = 1 )
16 13 15 oveq12d
 |-  ( ( P e. Prime /\ N e. ( 1 ... ( P - 1 ) ) ) -> ( ( N ^ 2 ) - ( 1 ^ 2 ) ) = ( ( N x. N ) - 1 ) )
17 8 12 16 3eqtr2d
 |-  ( ( P e. Prime /\ N e. ( 1 ... ( P - 1 ) ) ) -> ( ( N - 1 ) x. ( N + 1 ) ) = ( ( N x. N ) - 1 ) )
18 17 breq2d
 |-  ( ( P e. Prime /\ N e. ( 1 ... ( P - 1 ) ) ) -> ( P || ( ( N - 1 ) x. ( N + 1 ) ) <-> P || ( ( N x. N ) - 1 ) ) )
19 fz1ssfz0
 |-  ( 1 ... ( P - 1 ) ) C_ ( 0 ... ( P - 1 ) )
20 simpr
 |-  ( ( P e. Prime /\ N e. ( 1 ... ( P - 1 ) ) ) -> N e. ( 1 ... ( P - 1 ) ) )
21 19 20 sselid
 |-  ( ( P e. Prime /\ N e. ( 1 ... ( P - 1 ) ) ) -> N e. ( 0 ... ( P - 1 ) ) )
22 21 biantrurd
 |-  ( ( P e. Prime /\ N e. ( 1 ... ( P - 1 ) ) ) -> ( P || ( ( N x. N ) - 1 ) <-> ( N e. ( 0 ... ( P - 1 ) ) /\ P || ( ( N x. N ) - 1 ) ) ) )
23 18 22 bitrd
 |-  ( ( P e. Prime /\ N e. ( 1 ... ( P - 1 ) ) ) -> ( P || ( ( N - 1 ) x. ( N + 1 ) ) <-> ( N e. ( 0 ... ( P - 1 ) ) /\ P || ( ( N x. N ) - 1 ) ) ) )
24 simpl
 |-  ( ( P e. Prime /\ N e. ( 1 ... ( P - 1 ) ) ) -> P e. Prime )
25 euclemma
 |-  ( ( P e. Prime /\ ( N - 1 ) e. ZZ /\ ( N + 1 ) e. ZZ ) -> ( P || ( ( N - 1 ) x. ( N + 1 ) ) <-> ( P || ( N - 1 ) \/ P || ( N + 1 ) ) ) )
26 24 4 6 25 syl3anc
 |-  ( ( P e. Prime /\ N e. ( 1 ... ( P - 1 ) ) ) -> ( P || ( ( N - 1 ) x. ( N + 1 ) ) <-> ( P || ( N - 1 ) \/ P || ( N + 1 ) ) ) )
27 prmnn
 |-  ( P e. Prime -> P e. NN )
28 fzm1ndvds
 |-  ( ( P e. NN /\ N e. ( 1 ... ( P - 1 ) ) ) -> -. P || N )
29 27 28 sylan
 |-  ( ( P e. Prime /\ N e. ( 1 ... ( P - 1 ) ) ) -> -. P || N )
30 eqid
 |-  ( ( N ^ ( P - 2 ) ) mod P ) = ( ( N ^ ( P - 2 ) ) mod P )
31 30 prmdiveq
 |-  ( ( P e. Prime /\ N e. ZZ /\ -. P || N ) -> ( ( N e. ( 0 ... ( P - 1 ) ) /\ P || ( ( N x. N ) - 1 ) ) <-> N = ( ( N ^ ( P - 2 ) ) mod P ) ) )
32 24 2 29 31 syl3anc
 |-  ( ( P e. Prime /\ N e. ( 1 ... ( P - 1 ) ) ) -> ( ( N e. ( 0 ... ( P - 1 ) ) /\ P || ( ( N x. N ) - 1 ) ) <-> N = ( ( N ^ ( P - 2 ) ) mod P ) ) )
33 23 26 32 3bitr3rd
 |-  ( ( P e. Prime /\ N e. ( 1 ... ( P - 1 ) ) ) -> ( N = ( ( N ^ ( P - 2 ) ) mod P ) <-> ( P || ( N - 1 ) \/ P || ( N + 1 ) ) ) )
34 24 27 syl
 |-  ( ( P e. Prime /\ N e. ( 1 ... ( P - 1 ) ) ) -> P e. NN )
35 1zzd
 |-  ( ( P e. Prime /\ N e. ( 1 ... ( P - 1 ) ) ) -> 1 e. ZZ )
36 moddvds
 |-  ( ( P e. NN /\ N e. ZZ /\ 1 e. ZZ ) -> ( ( N mod P ) = ( 1 mod P ) <-> P || ( N - 1 ) ) )
37 34 2 35 36 syl3anc
 |-  ( ( P e. Prime /\ N e. ( 1 ... ( P - 1 ) ) ) -> ( ( N mod P ) = ( 1 mod P ) <-> P || ( N - 1 ) ) )
38 elfznn
 |-  ( N e. ( 1 ... ( P - 1 ) ) -> N e. NN )
39 38 adantl
 |-  ( ( P e. Prime /\ N e. ( 1 ... ( P - 1 ) ) ) -> N e. NN )
40 39 nnred
 |-  ( ( P e. Prime /\ N e. ( 1 ... ( P - 1 ) ) ) -> N e. RR )
41 34 nnrpd
 |-  ( ( P e. Prime /\ N e. ( 1 ... ( P - 1 ) ) ) -> P e. RR+ )
42 39 nnnn0d
 |-  ( ( P e. Prime /\ N e. ( 1 ... ( P - 1 ) ) ) -> N e. NN0 )
43 42 nn0ge0d
 |-  ( ( P e. Prime /\ N e. ( 1 ... ( P - 1 ) ) ) -> 0 <_ N )
44 elfzle2
 |-  ( N e. ( 1 ... ( P - 1 ) ) -> N <_ ( P - 1 ) )
45 44 adantl
 |-  ( ( P e. Prime /\ N e. ( 1 ... ( P - 1 ) ) ) -> N <_ ( P - 1 ) )
46 prmz
 |-  ( P e. Prime -> P e. ZZ )
47 zltlem1
 |-  ( ( N e. ZZ /\ P e. ZZ ) -> ( N < P <-> N <_ ( P - 1 ) ) )
48 1 46 47 syl2anr
 |-  ( ( P e. Prime /\ N e. ( 1 ... ( P - 1 ) ) ) -> ( N < P <-> N <_ ( P - 1 ) ) )
49 45 48 mpbird
 |-  ( ( P e. Prime /\ N e. ( 1 ... ( P - 1 ) ) ) -> N < P )
50 modid
 |-  ( ( ( N e. RR /\ P e. RR+ ) /\ ( 0 <_ N /\ N < P ) ) -> ( N mod P ) = N )
51 40 41 43 49 50 syl22anc
 |-  ( ( P e. Prime /\ N e. ( 1 ... ( P - 1 ) ) ) -> ( N mod P ) = N )
52 34 nnred
 |-  ( ( P e. Prime /\ N e. ( 1 ... ( P - 1 ) ) ) -> P e. RR )
53 prmuz2
 |-  ( P e. Prime -> P e. ( ZZ>= ` 2 ) )
54 24 53 syl
 |-  ( ( P e. Prime /\ N e. ( 1 ... ( P - 1 ) ) ) -> P e. ( ZZ>= ` 2 ) )
55 eluz2gt1
 |-  ( P e. ( ZZ>= ` 2 ) -> 1 < P )
56 54 55 syl
 |-  ( ( P e. Prime /\ N e. ( 1 ... ( P - 1 ) ) ) -> 1 < P )
57 1mod
 |-  ( ( P e. RR /\ 1 < P ) -> ( 1 mod P ) = 1 )
58 52 56 57 syl2anc
 |-  ( ( P e. Prime /\ N e. ( 1 ... ( P - 1 ) ) ) -> ( 1 mod P ) = 1 )
59 51 58 eqeq12d
 |-  ( ( P e. Prime /\ N e. ( 1 ... ( P - 1 ) ) ) -> ( ( N mod P ) = ( 1 mod P ) <-> N = 1 ) )
60 37 59 bitr3d
 |-  ( ( P e. Prime /\ N e. ( 1 ... ( P - 1 ) ) ) -> ( P || ( N - 1 ) <-> N = 1 ) )
61 35 znegcld
 |-  ( ( P e. Prime /\ N e. ( 1 ... ( P - 1 ) ) ) -> -u 1 e. ZZ )
62 moddvds
 |-  ( ( P e. NN /\ N e. ZZ /\ -u 1 e. ZZ ) -> ( ( N mod P ) = ( -u 1 mod P ) <-> P || ( N - -u 1 ) ) )
63 34 2 61 62 syl3anc
 |-  ( ( P e. Prime /\ N e. ( 1 ... ( P - 1 ) ) ) -> ( ( N mod P ) = ( -u 1 mod P ) <-> P || ( N - -u 1 ) ) )
64 34 nncnd
 |-  ( ( P e. Prime /\ N e. ( 1 ... ( P - 1 ) ) ) -> P e. CC )
65 64 mulid2d
 |-  ( ( P e. Prime /\ N e. ( 1 ... ( P - 1 ) ) ) -> ( 1 x. P ) = P )
66 65 oveq2d
 |-  ( ( P e. Prime /\ N e. ( 1 ... ( P - 1 ) ) ) -> ( -u 1 + ( 1 x. P ) ) = ( -u 1 + P ) )
67 neg1cn
 |-  -u 1 e. CC
68 addcom
 |-  ( ( -u 1 e. CC /\ P e. CC ) -> ( -u 1 + P ) = ( P + -u 1 ) )
69 67 64 68 sylancr
 |-  ( ( P e. Prime /\ N e. ( 1 ... ( P - 1 ) ) ) -> ( -u 1 + P ) = ( P + -u 1 ) )
70 negsub
 |-  ( ( P e. CC /\ 1 e. CC ) -> ( P + -u 1 ) = ( P - 1 ) )
71 64 10 70 sylancl
 |-  ( ( P e. Prime /\ N e. ( 1 ... ( P - 1 ) ) ) -> ( P + -u 1 ) = ( P - 1 ) )
72 66 69 71 3eqtrd
 |-  ( ( P e. Prime /\ N e. ( 1 ... ( P - 1 ) ) ) -> ( -u 1 + ( 1 x. P ) ) = ( P - 1 ) )
73 72 oveq1d
 |-  ( ( P e. Prime /\ N e. ( 1 ... ( P - 1 ) ) ) -> ( ( -u 1 + ( 1 x. P ) ) mod P ) = ( ( P - 1 ) mod P ) )
74 neg1rr
 |-  -u 1 e. RR
75 74 a1i
 |-  ( ( P e. Prime /\ N e. ( 1 ... ( P - 1 ) ) ) -> -u 1 e. RR )
76 modcyc
 |-  ( ( -u 1 e. RR /\ P e. RR+ /\ 1 e. ZZ ) -> ( ( -u 1 + ( 1 x. P ) ) mod P ) = ( -u 1 mod P ) )
77 75 41 35 76 syl3anc
 |-  ( ( P e. Prime /\ N e. ( 1 ... ( P - 1 ) ) ) -> ( ( -u 1 + ( 1 x. P ) ) mod P ) = ( -u 1 mod P ) )
78 peano2rem
 |-  ( P e. RR -> ( P - 1 ) e. RR )
79 52 78 syl
 |-  ( ( P e. Prime /\ N e. ( 1 ... ( P - 1 ) ) ) -> ( P - 1 ) e. RR )
80 nnm1nn0
 |-  ( P e. NN -> ( P - 1 ) e. NN0 )
81 34 80 syl
 |-  ( ( P e. Prime /\ N e. ( 1 ... ( P - 1 ) ) ) -> ( P - 1 ) e. NN0 )
82 81 nn0ge0d
 |-  ( ( P e. Prime /\ N e. ( 1 ... ( P - 1 ) ) ) -> 0 <_ ( P - 1 ) )
83 52 ltm1d
 |-  ( ( P e. Prime /\ N e. ( 1 ... ( P - 1 ) ) ) -> ( P - 1 ) < P )
84 modid
 |-  ( ( ( ( P - 1 ) e. RR /\ P e. RR+ ) /\ ( 0 <_ ( P - 1 ) /\ ( P - 1 ) < P ) ) -> ( ( P - 1 ) mod P ) = ( P - 1 ) )
85 79 41 82 83 84 syl22anc
 |-  ( ( P e. Prime /\ N e. ( 1 ... ( P - 1 ) ) ) -> ( ( P - 1 ) mod P ) = ( P - 1 ) )
86 73 77 85 3eqtr3d
 |-  ( ( P e. Prime /\ N e. ( 1 ... ( P - 1 ) ) ) -> ( -u 1 mod P ) = ( P - 1 ) )
87 51 86 eqeq12d
 |-  ( ( P e. Prime /\ N e. ( 1 ... ( P - 1 ) ) ) -> ( ( N mod P ) = ( -u 1 mod P ) <-> N = ( P - 1 ) ) )
88 subneg
 |-  ( ( N e. CC /\ 1 e. CC ) -> ( N - -u 1 ) = ( N + 1 ) )
89 9 10 88 sylancl
 |-  ( ( P e. Prime /\ N e. ( 1 ... ( P - 1 ) ) ) -> ( N - -u 1 ) = ( N + 1 ) )
90 89 breq2d
 |-  ( ( P e. Prime /\ N e. ( 1 ... ( P - 1 ) ) ) -> ( P || ( N - -u 1 ) <-> P || ( N + 1 ) ) )
91 63 87 90 3bitr3rd
 |-  ( ( P e. Prime /\ N e. ( 1 ... ( P - 1 ) ) ) -> ( P || ( N + 1 ) <-> N = ( P - 1 ) ) )
92 60 91 orbi12d
 |-  ( ( P e. Prime /\ N e. ( 1 ... ( P - 1 ) ) ) -> ( ( P || ( N - 1 ) \/ P || ( N + 1 ) ) <-> ( N = 1 \/ N = ( P - 1 ) ) ) )
93 33 92 bitrd
 |-  ( ( P e. Prime /\ N e. ( 1 ... ( P - 1 ) ) ) -> ( N = ( ( N ^ ( P - 2 ) ) mod P ) <-> ( N = 1 \/ N = ( P - 1 ) ) ) )