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 ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 1 ... ( 𝑃 − 1 ) ) ) → ( 𝑁 = ( ( 𝑁 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ↔ ( 𝑁 = 1 ∨ 𝑁 = ( 𝑃 − 1 ) ) ) )

Proof

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