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