Metamath Proof Explorer

Theorem wilth

Description: Wilson's theorem. A number is prime iff it is greater than or equal to 2 and ( N - 1 ) ! is congruent to -u 1 , mod N , or alternatively if N divides ( N - 1 ) ! + 1 . In this part of the proof we show the relatively simple reverse implication; see wilthlem3 for the forward implication. This is Metamath 100 proof #51. (Contributed by Mario Carneiro, 24-Jan-2015) (Proof shortened by Fan Zheng, 16-Jun-2016)

Ref Expression
Assertion wilth ( 𝑁 ∈ ℙ ↔ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∥ ( ( ! ‘ ( 𝑁 − 1 ) ) + 1 ) ) )

Proof

Step Hyp Ref Expression
1 prmuz2 ⊢ ( 𝑁 ∈ ℙ → 𝑁 ∈ ( ℤ≥ ‘ 2 ) )
2 eqid ⊢ ( mulGrp ‘ ℂfld ) = ( mulGrp ‘ ℂfld )
3 eleq2w ⊢ ( 𝑧 = 𝑥 → ( ( 𝑁 − 1 ) ∈ 𝑧 ↔ ( 𝑁 − 1 ) ∈ 𝑥 ) )
4 oveq1 ⊢ ( 𝑛 = 𝑦 → ( 𝑛 ↑ ( 𝑁 − 2 ) ) = ( 𝑦 ↑ ( 𝑁 − 2 ) ) )
5 4 oveq1d ⊢ ( 𝑛 = 𝑦 → ( ( 𝑛 ↑ ( 𝑁 − 2 ) ) mod 𝑁 ) = ( ( 𝑦 ↑ ( 𝑁 − 2 ) ) mod 𝑁 ) )
6 5 eleq1d ⊢ ( 𝑛 = 𝑦 → ( ( ( 𝑛 ↑ ( 𝑁 − 2 ) ) mod 𝑁 ) ∈ 𝑧 ↔ ( ( 𝑦 ↑ ( 𝑁 − 2 ) ) mod 𝑁 ) ∈ 𝑧 ) )
7 6 cbvralvw ⊢ ( ∀ 𝑛 ∈ 𝑧 ( ( 𝑛 ↑ ( 𝑁 − 2 ) ) mod 𝑁 ) ∈ 𝑧 ↔ ∀ 𝑦 ∈ 𝑧 ( ( 𝑦 ↑ ( 𝑁 − 2 ) ) mod 𝑁 ) ∈ 𝑧 )
8 eleq2w ⊢ ( 𝑧 = 𝑥 → ( ( ( 𝑦 ↑ ( 𝑁 − 2 ) ) mod 𝑁 ) ∈ 𝑧 ↔ ( ( 𝑦 ↑ ( 𝑁 − 2 ) ) mod 𝑁 ) ∈ 𝑥 ) )
9 8 raleqbi1dv ⊢ ( 𝑧 = 𝑥 → ( ∀ 𝑦 ∈ 𝑧 ( ( 𝑦 ↑ ( 𝑁 − 2 ) ) mod 𝑁 ) ∈ 𝑧 ↔ ∀ 𝑦 ∈ 𝑥 ( ( 𝑦 ↑ ( 𝑁 − 2 ) ) mod 𝑁 ) ∈ 𝑥 ) )
10 7 9 bitrid ⊢ ( 𝑧 = 𝑥 → ( ∀ 𝑛 ∈ 𝑧 ( ( 𝑛 ↑ ( 𝑁 − 2 ) ) mod 𝑁 ) ∈ 𝑧 ↔ ∀ 𝑦 ∈ 𝑥 ( ( 𝑦 ↑ ( 𝑁 − 2 ) ) mod 𝑁 ) ∈ 𝑥 ) )
11 3 10 anbi12d ⊢ ( 𝑧 = 𝑥 → ( ( ( 𝑁 − 1 ) ∈ 𝑧 ∧ ∀ 𝑛 ∈ 𝑧 ( ( 𝑛 ↑ ( 𝑁 − 2 ) ) mod 𝑁 ) ∈ 𝑧 ) ↔ ( ( 𝑁 − 1 ) ∈ 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( ( 𝑦 ↑ ( 𝑁 − 2 ) ) mod 𝑁 ) ∈ 𝑥 ) ) )
12 11 cbvrabv ⊢ { 𝑧 ∈ 𝒫 ( 1 ... ( 𝑁 − 1 ) ) ∣ ( ( 𝑁 − 1 ) ∈ 𝑧 ∧ ∀ 𝑛 ∈ 𝑧 ( ( 𝑛 ↑ ( 𝑁 − 2 ) ) mod 𝑁 ) ∈ 𝑧 ) } = { 𝑥 ∈ 𝒫 ( 1 ... ( 𝑁 − 1 ) ) ∣ ( ( 𝑁 − 1 ) ∈ 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( ( 𝑦 ↑ ( 𝑁 − 2 ) ) mod 𝑁 ) ∈ 𝑥 ) }
13 2 12 wilthlem3 ⊢ ( 𝑁 ∈ ℙ → 𝑁 ∥ ( ( ! ‘ ( 𝑁 − 1 ) ) + 1 ) )
14 1 13 jca ⊢ ( 𝑁 ∈ ℙ → ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∥ ( ( ! ‘ ( 𝑁 − 1 ) ) + 1 ) ) )
15 simpl ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∥ ( ( ! ‘ ( 𝑁 − 1 ) ) + 1 ) ) → 𝑁 ∈ ( ℤ≥ ‘ 2 ) )
16 elfzuz ⊢ ( 𝑛 ∈ ( 2 ... ( 𝑁 − 1 ) ) → 𝑛 ∈ ( ℤ≥ ‘ 2 ) )
17 16 adantl ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∥ ( ( ! ‘ ( 𝑁 − 1 ) ) + 1 ) ) ∧ 𝑛 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) → 𝑛 ∈ ( ℤ≥ ‘ 2 ) )
18 eluz2nn ⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 2 ) → 𝑛 ∈ ℕ )
19 17 18 syl ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∥ ( ( ! ‘ ( 𝑁 − 1 ) ) + 1 ) ) ∧ 𝑛 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) → 𝑛 ∈ ℕ )
20 elfzuz3 ⊢ ( 𝑛 ∈ ( 2 ... ( 𝑁 − 1 ) ) → ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑛 ) )
21 20 adantl ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∥ ( ( ! ‘ ( 𝑁 − 1 ) ) + 1 ) ) ∧ 𝑛 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) → ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑛 ) )
22 dvdsfac ⊢ ( ( 𝑛 ∈ ℕ ∧ ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑛 ) ) → 𝑛 ∥ ( ! ‘ ( 𝑁 − 1 ) ) )
23 19 21 22 syl2anc ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∥ ( ( ! ‘ ( 𝑁 − 1 ) ) + 1 ) ) ∧ 𝑛 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) → 𝑛 ∥ ( ! ‘ ( 𝑁 − 1 ) ) )
24 eluz2nn ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 𝑁 ∈ ℕ )
25 24 ad2antrr ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∥ ( ( ! ‘ ( 𝑁 − 1 ) ) + 1 ) ) ∧ 𝑛 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) → 𝑁 ∈ ℕ )
26 nnm1nn0 ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 − 1 ) ∈ ℕ0 )
27 faccl ⊢ ( ( 𝑁 − 1 ) ∈ ℕ0 → ( ! ‘ ( 𝑁 − 1 ) ) ∈ ℕ )
28 25 26 27 3syl ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∥ ( ( ! ‘ ( 𝑁 − 1 ) ) + 1 ) ) ∧ 𝑛 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) → ( ! ‘ ( 𝑁 − 1 ) ) ∈ ℕ )
29 28 nnzd ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∥ ( ( ! ‘ ( 𝑁 − 1 ) ) + 1 ) ) ∧ 𝑛 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) → ( ! ‘ ( 𝑁 − 1 ) ) ∈ ℤ )
30 eluz2gt1 ⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 2 ) → 1 < 𝑛 )
31 17 30 syl ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∥ ( ( ! ‘ ( 𝑁 − 1 ) ) + 1 ) ) ∧ 𝑛 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) → 1 < 𝑛 )
32 ndvdsp1 ⊢ ( ( ( ! ‘ ( 𝑁 − 1 ) ) ∈ ℤ ∧ 𝑛 ∈ ℕ ∧ 1 < 𝑛 ) → ( 𝑛 ∥ ( ! ‘ ( 𝑁 − 1 ) ) → ¬ 𝑛 ∥ ( ( ! ‘ ( 𝑁 − 1 ) ) + 1 ) ) )
33 29 19 31 32 syl3anc ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∥ ( ( ! ‘ ( 𝑁 − 1 ) ) + 1 ) ) ∧ 𝑛 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) → ( 𝑛 ∥ ( ! ‘ ( 𝑁 − 1 ) ) → ¬ 𝑛 ∥ ( ( ! ‘ ( 𝑁 − 1 ) ) + 1 ) ) )
34 23 33 mpd ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∥ ( ( ! ‘ ( 𝑁 − 1 ) ) + 1 ) ) ∧ 𝑛 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) → ¬ 𝑛 ∥ ( ( ! ‘ ( 𝑁 − 1 ) ) + 1 ) )
35 simplr ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∥ ( ( ! ‘ ( 𝑁 − 1 ) ) + 1 ) ) ∧ 𝑛 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) → 𝑁 ∥ ( ( ! ‘ ( 𝑁 − 1 ) ) + 1 ) )
36 19 nnzd ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∥ ( ( ! ‘ ( 𝑁 − 1 ) ) + 1 ) ) ∧ 𝑛 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) → 𝑛 ∈ ℤ )
37 25 nnzd ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∥ ( ( ! ‘ ( 𝑁 − 1 ) ) + 1 ) ) ∧ 𝑛 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) → 𝑁 ∈ ℤ )
38 29 peano2zd ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∥ ( ( ! ‘ ( 𝑁 − 1 ) ) + 1 ) ) ∧ 𝑛 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) → ( ( ! ‘ ( 𝑁 − 1 ) ) + 1 ) ∈ ℤ )
39 dvdstr ⊢ ( ( 𝑛 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ( ( ! ‘ ( 𝑁 − 1 ) ) + 1 ) ∈ ℤ ) → ( ( 𝑛 ∥ 𝑁 ∧ 𝑁 ∥ ( ( ! ‘ ( 𝑁 − 1 ) ) + 1 ) ) → 𝑛 ∥ ( ( ! ‘ ( 𝑁 − 1 ) ) + 1 ) ) )
40 36 37 38 39 syl3anc ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∥ ( ( ! ‘ ( 𝑁 − 1 ) ) + 1 ) ) ∧ 𝑛 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) → ( ( 𝑛 ∥ 𝑁 ∧ 𝑁 ∥ ( ( ! ‘ ( 𝑁 − 1 ) ) + 1 ) ) → 𝑛 ∥ ( ( ! ‘ ( 𝑁 − 1 ) ) + 1 ) ) )
41 35 40 mpan2d ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∥ ( ( ! ‘ ( 𝑁 − 1 ) ) + 1 ) ) ∧ 𝑛 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) → ( 𝑛 ∥ 𝑁 → 𝑛 ∥ ( ( ! ‘ ( 𝑁 − 1 ) ) + 1 ) ) )
42 34 41 mtod ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∥ ( ( ! ‘ ( 𝑁 − 1 ) ) + 1 ) ) ∧ 𝑛 ∈ ( 2 ... ( 𝑁 − 1 ) ) ) → ¬ 𝑛 ∥ 𝑁 )
43 42 ralrimiva ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∥ ( ( ! ‘ ( 𝑁 − 1 ) ) + 1 ) ) → ∀ 𝑛 ∈ ( 2 ... ( 𝑁 − 1 ) ) ¬ 𝑛 ∥ 𝑁 )
44 isprm3 ⊢ ( 𝑁 ∈ ℙ ↔ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ ∀ 𝑛 ∈ ( 2 ... ( 𝑁 − 1 ) ) ¬ 𝑛 ∥ 𝑁 ) )
45 15 43 44 sylanbrc ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∥ ( ( ! ‘ ( 𝑁 − 1 ) ) + 1 ) ) → 𝑁 ∈ ℙ )
46 14 45 impbii ⊢ ( 𝑁 ∈ ℙ ↔ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∥ ( ( ! ‘ ( 𝑁 − 1 ) ) + 1 ) ) )