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	$⊢ P \in ℙ \to (P - 1)! \mod P = -1 \mod P$

Proof

Step	Hyp	Ref	Expression
1		wilth	$⊢ P \in ℙ \leftrightarrow (P \in ℤ_{\geq 2} \land P ∥ ((P - 1)! + 1))$
2		eluz2nn	$⊢ P \in ℤ_{\geq 2} \to P \in ℕ$
3		nnm1nn0	$⊢ P \in ℕ \to P - 1 \in ℕ_{0}$
4	2 3	syl	$⊢ P \in ℤ_{\geq 2} \to P - 1 \in ℕ_{0}$
5	4	faccld	$⊢ P \in ℤ_{\geq 2} \to (P - 1)! \in ℕ$
6	5	nnzd	$⊢ P \in ℤ_{\geq 2} \to (P - 1)! \in ℤ$
7	6	peano2zd	$⊢ P \in ℤ_{\geq 2} \to (P - 1)! + 1 \in ℤ$
8		dvdsval3	$⊢ (P \in ℕ \land (P - 1)! + 1 \in ℤ) \to (P ∥ ((P - 1)! + 1) \leftrightarrow ((P - 1)! + 1) \mod P = 0)$
9	2 7 8	syl2anc	$⊢ P \in ℤ_{\geq 2} \to (P ∥ ((P - 1)! + 1) \leftrightarrow ((P - 1)! + 1) \mod P = 0)$
10	9	biimpar	$⊢ (P \in ℤ_{\geq 2} \land ((P - 1)! + 1) \mod P = 0) \to P ∥ ((P - 1)! + 1)$
11	5	nncnd	$⊢ P \in ℤ_{\geq 2} \to (P - 1)! \in ℂ$
12		1cnd	$⊢ P \in ℤ_{\geq 2} \to 1 \in ℂ$
13	11 12	jca	$⊢ P \in ℤ_{\geq 2} \to ((P - 1)! \in ℂ \land 1 \in ℂ)$
14	13	adantr	$⊢ (P \in ℤ_{\geq 2} \land ((P - 1)! + 1) \mod P = 0) \to ((P - 1)! \in ℂ \land 1 \in ℂ)$
15		subneg	$⊢ ((P - 1)! \in ℂ \land 1 \in ℂ) \to (P - 1)! - -1 = (P - 1)! + 1$
16	14 15	syl	$⊢ (P \in ℤ_{\geq 2} \land ((P - 1)! + 1) \mod P = 0) \to (P - 1)! - -1 = (P - 1)! + 1$
17	10 16	breqtrrd	$⊢ (P \in ℤ_{\geq 2} \land ((P - 1)! + 1) \mod P = 0) \to P ∥ ((P - 1)! - -1)$
18		neg1z	$⊢ - 1 \in ℤ$
19	18	a1i	$⊢ P \in ℤ_{\geq 2} \to - 1 \in ℤ$
20	2 6 19	3jca	$⊢ P \in ℤ_{\geq 2} \to (P \in ℕ \land (P - 1)! \in ℤ \land - 1 \in ℤ)$
21	20	adantr	$⊢ (P \in ℤ_{\geq 2} \land ((P - 1)! + 1) \mod P = 0) \to (P \in ℕ \land (P - 1)! \in ℤ \land - 1 \in ℤ)$
22		moddvds	$⊢ (P \in ℕ \land (P - 1)! \in ℤ \land - 1 \in ℤ) \to ((P - 1)! \mod P = -1 \mod P \leftrightarrow P ∥ ((P - 1)! - -1))$
23	21 22	syl	$⊢ (P \in ℤ_{\geq 2} \land ((P - 1)! + 1) \mod P = 0) \to ((P - 1)! \mod P = -1 \mod P \leftrightarrow P ∥ ((P - 1)! - -1))$
24	17 23	mpbird	$⊢ (P \in ℤ_{\geq 2} \land ((P - 1)! + 1) \mod P = 0) \to (P - 1)! \mod P = -1 \mod P$
25	24	ex	$⊢ P \in ℤ_{\geq 2} \to (((P - 1)! + 1) \mod P = 0 \to (P - 1)! \mod P = -1 \mod P)$
26	9 25	sylbid	$⊢ P \in ℤ_{\geq 2} \to (P ∥ ((P - 1)! + 1) \to (P - 1)! \mod P = -1 \mod P)$
27	26	imp	$⊢ (P \in ℤ_{\geq 2} \land P ∥ ((P - 1)! + 1)) \to (P - 1)! \mod P = -1 \mod P$
28	1 27	sylbi	$⊢ P \in ℙ \to (P - 1)! \mod P = -1 \mod P$

Metamath Proof Explorer

Theorem wilthimp

Proof