Metamath Proof Explorer

Theorem wilthimp

Description: The forward implication of Wilson's theorem wilth (see wilthlem3 ), expressed using the modulo operation: For any prime p we have ( p - 1 ) ! == - 1 (mod p ), see theorem 5.24 in ApostolNT p. 116. (Contributed by AV, 21-Jul-2021)

Ref Expression
Assertion wilthimp ( 𝑃 ∈ ℙ → ( ( ! ‘ ( 𝑃 − 1 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) )

Proof

Step Hyp Ref Expression
1 wilth ⊢ ( 𝑃 ∈ ℙ ↔ ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑃 ∥ ( ( ! ‘ ( 𝑃 − 1 ) ) + 1 ) ) )
2 eluz2nn ⊢ ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) → 𝑃 ∈ ℕ )
3 nnm1nn0 ⊢ ( 𝑃 ∈ ℕ → ( 𝑃 − 1 ) ∈ ℕ0 )
4 2 3 syl ⊢ ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑃 − 1 ) ∈ ℕ0 )
5 4 faccld ⊢ ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) → ( ! ‘ ( 𝑃 − 1 ) ) ∈ ℕ )
6 5 nnzd ⊢ ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) → ( ! ‘ ( 𝑃 − 1 ) ) ∈ ℤ )
7 6 peano2zd ⊢ ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) → ( ( ! ‘ ( 𝑃 − 1 ) ) + 1 ) ∈ ℤ )
8 dvdsval3 ⊢ ( ( 𝑃 ∈ ℕ ∧ ( ( ! ‘ ( 𝑃 − 1 ) ) + 1 ) ∈ ℤ ) → ( 𝑃 ∥ ( ( ! ‘ ( 𝑃 − 1 ) ) + 1 ) ↔ ( ( ( ! ‘ ( 𝑃 − 1 ) ) + 1 ) mod 𝑃 ) = 0 ) )
9 2 7 8 syl2anc ⊢ ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑃 ∥ ( ( ! ‘ ( 𝑃 − 1 ) ) + 1 ) ↔ ( ( ( ! ‘ ( 𝑃 − 1 ) ) + 1 ) mod 𝑃 ) = 0 ) )
10 9 biimpar ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( ( ( ! ‘ ( 𝑃 − 1 ) ) + 1 ) mod 𝑃 ) = 0 ) → 𝑃 ∥ ( ( ! ‘ ( 𝑃 − 1 ) ) + 1 ) )
11 5 nncnd ⊢ ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) → ( ! ‘ ( 𝑃 − 1 ) ) ∈ ℂ )
12 1cnd ⊢ ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) → 1 ∈ ℂ )
13 11 12 jca ⊢ ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) → ( ( ! ‘ ( 𝑃 − 1 ) ) ∈ ℂ ∧ 1 ∈ ℂ ) )
14 13 adantr ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( ( ( ! ‘ ( 𝑃 − 1 ) ) + 1 ) mod 𝑃 ) = 0 ) → ( ( ! ‘ ( 𝑃 − 1 ) ) ∈ ℂ ∧ 1 ∈ ℂ ) )
15 subneg ⊢ ( ( ( ! ‘ ( 𝑃 − 1 ) ) ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( ! ‘ ( 𝑃 − 1 ) ) − - 1 ) = ( ( ! ‘ ( 𝑃 − 1 ) ) + 1 ) )
16 14 15 syl ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( ( ( ! ‘ ( 𝑃 − 1 ) ) + 1 ) mod 𝑃 ) = 0 ) → ( ( ! ‘ ( 𝑃 − 1 ) ) − - 1 ) = ( ( ! ‘ ( 𝑃 − 1 ) ) + 1 ) )
17 10 16 breqtrrd ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( ( ( ! ‘ ( 𝑃 − 1 ) ) + 1 ) mod 𝑃 ) = 0 ) → 𝑃 ∥ ( ( ! ‘ ( 𝑃 − 1 ) ) − - 1 ) )
18 neg1z ⊢ - 1 ∈ ℤ
19 18 a1i ⊢ ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) → - 1 ∈ ℤ )
20 2 6 19 3jca ⊢ ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑃 ∈ ℕ ∧ ( ! ‘ ( 𝑃 − 1 ) ) ∈ ℤ ∧ - 1 ∈ ℤ ) )
21 20 adantr ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( ( ( ! ‘ ( 𝑃 − 1 ) ) + 1 ) mod 𝑃 ) = 0 ) → ( 𝑃 ∈ ℕ ∧ ( ! ‘ ( 𝑃 − 1 ) ) ∈ ℤ ∧ - 1 ∈ ℤ ) )
22 moddvds ⊢ ( ( 𝑃 ∈ ℕ ∧ ( ! ‘ ( 𝑃 − 1 ) ) ∈ ℤ ∧ - 1 ∈ ℤ ) → ( ( ( ! ‘ ( 𝑃 − 1 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ↔ 𝑃 ∥ ( ( ! ‘ ( 𝑃 − 1 ) ) − - 1 ) ) )
23 21 22 syl ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( ( ( ! ‘ ( 𝑃 − 1 ) ) + 1 ) mod 𝑃 ) = 0 ) → ( ( ( ! ‘ ( 𝑃 − 1 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ↔ 𝑃 ∥ ( ( ! ‘ ( 𝑃 − 1 ) ) − - 1 ) ) )
24 17 23 mpbird ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( ( ( ! ‘ ( 𝑃 − 1 ) ) + 1 ) mod 𝑃 ) = 0 ) → ( ( ! ‘ ( 𝑃 − 1 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) )
25 24 ex ⊢ ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) → ( ( ( ( ! ‘ ( 𝑃 − 1 ) ) + 1 ) mod 𝑃 ) = 0 → ( ( ! ‘ ( 𝑃 − 1 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ) )
26 9 25 sylbid ⊢ ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑃 ∥ ( ( ! ‘ ( 𝑃 − 1 ) ) + 1 ) → ( ( ! ‘ ( 𝑃 − 1 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ) )
27 26 imp ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑃 ∥ ( ( ! ‘ ( 𝑃 − 1 ) ) + 1 ) ) → ( ( ! ‘ ( 𝑃 − 1 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) )
28 1 27 sylbi ⊢ ( 𝑃 ∈ ℙ → ( ( ! ‘ ( 𝑃 − 1 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) )