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 mullidd ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 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 ) ) ) )