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	$⊢ N \in ℙ \leftrightarrow (N \in ℤ_{\geq 2} \land N ∥ ((N - 1)! + 1))$

Proof

Step	Hyp	Ref	Expression
1		prmuz2	$⊢ N \in ℙ \to N \in ℤ_{\geq 2}$
2		eqid	$⊢ {mulGrp}_{ℂ_{fld}} = {mulGrp}_{ℂ_{fld}}$
3		eleq2w	$⊢ z = x \to (N - 1 \in z \leftrightarrow N - 1 \in x)$
4		oveq1	$⊢ n = y \to n^{N - 2} = y^{N - 2}$
5	4	oveq1d	$⊢ n = y \to n^{N - 2} \mod N = y^{N - 2} \mod N$
6	5	eleq1d	$⊢ n = y \to (n^{N - 2} \mod N \in z \leftrightarrow y^{N - 2} \mod N \in z)$
7	6	cbvralvw	$⊢ \forall n \in z n^{N - 2} \mod N \in z \leftrightarrow \forall y \in z y^{N - 2} \mod N \in z$
8		eleq2w	$⊢ z = x \to (y^{N - 2} \mod N \in z \leftrightarrow y^{N - 2} \mod N \in x)$
9	8	raleqbi1dv	$⊢ z = x \to (\forall y \in z y^{N - 2} \mod N \in z \leftrightarrow \forall y \in x y^{N - 2} \mod N \in x)$
10	7 9	bitrid	$⊢ z = x \to (\forall n \in z n^{N - 2} \mod N \in z \leftrightarrow \forall y \in x y^{N - 2} \mod N \in x)$
11	3 10	anbi12d	$⊢ z = x \to ((N - 1 \in z \land \forall n \in z n^{N - 2} \mod N \in z) \leftrightarrow (N - 1 \in x \land \forall y \in x y^{N - 2} \mod N \in x))$
12	11	cbvrabv	$⊢ \{z \in 𝒫 (1 \dots N - 1) \| (N - 1 \in z \land \forall n \in z n^{N - 2} \mod N \in z)\} = \{x \in 𝒫 (1 \dots N - 1) \| (N - 1 \in x \land \forall y \in x y^{N - 2} \mod N \in x)\}$
13	2 12	wilthlem3	$⊢ N \in ℙ \to N ∥ ((N - 1)! + 1)$
14	1 13	jca	$⊢ N \in ℙ \to (N \in ℤ_{\geq 2} \land N ∥ ((N - 1)! + 1))$
15		simpl	$⊢ (N \in ℤ_{\geq 2} \land N ∥ ((N - 1)! + 1)) \to N \in ℤ_{\geq 2}$
16		elfzuz	$⊢ n \in (2 \dots N - 1) \to n \in ℤ_{\geq 2}$
17	16	adantl	$⊢ ((N \in ℤ_{\geq 2} \land N ∥ ((N - 1)! + 1)) \land n \in (2 \dots N - 1)) \to n \in ℤ_{\geq 2}$
18		eluz2nn	$⊢ n \in ℤ_{\geq 2} \to n \in ℕ$
19	17 18	syl	$⊢ ((N \in ℤ_{\geq 2} \land N ∥ ((N - 1)! + 1)) \land n \in (2 \dots N - 1)) \to n \in ℕ$
20		elfzuz3	$⊢ n \in (2 \dots N - 1) \to N - 1 \in ℤ_{\geq n}$
21	20	adantl	$⊢ ((N \in ℤ_{\geq 2} \land N ∥ ((N - 1)! + 1)) \land n \in (2 \dots N - 1)) \to N - 1 \in ℤ_{\geq n}$
22		dvdsfac	$⊢ (n \in ℕ \land N - 1 \in ℤ_{\geq n}) \to n ∥ (N - 1)!$
23	19 21 22	syl2anc	$⊢ ((N \in ℤ_{\geq 2} \land N ∥ ((N - 1)! + 1)) \land n \in (2 \dots N - 1)) \to n ∥ (N - 1)!$
24		eluz2nn	$⊢ N \in ℤ_{\geq 2} \to N \in ℕ$
25	24	ad2antrr	$⊢ ((N \in ℤ_{\geq 2} \land N ∥ ((N - 1)! + 1)) \land n \in (2 \dots N - 1)) \to N \in ℕ$
26		nnm1nn0	$⊢ N \in ℕ \to N - 1 \in ℕ_{0}$
27		faccl	$⊢ N - 1 \in ℕ_{0} \to (N - 1)! \in ℕ$
28	25 26 27	3syl	$⊢ ((N \in ℤ_{\geq 2} \land N ∥ ((N - 1)! + 1)) \land n \in (2 \dots N - 1)) \to (N - 1)! \in ℕ$
29	28	nnzd	$⊢ ((N \in ℤ_{\geq 2} \land N ∥ ((N - 1)! + 1)) \land n \in (2 \dots N - 1)) \to (N - 1)! \in ℤ$
30		eluz2gt1	$⊢ n \in ℤ_{\geq 2} \to 1 < n$
31	17 30	syl	$⊢ ((N \in ℤ_{\geq 2} \land N ∥ ((N - 1)! + 1)) \land n \in (2 \dots N - 1)) \to 1 < n$
32		ndvdsp1	$⊢ ((N - 1)! \in ℤ \land n \in ℕ \land 1 < n) \to (n ∥ (N - 1)! \to \neg n ∥ ((N - 1)! + 1))$
33	29 19 31 32	syl3anc	$⊢ ((N \in ℤ_{\geq 2} \land N ∥ ((N - 1)! + 1)) \land n \in (2 \dots N - 1)) \to (n ∥ (N - 1)! \to \neg n ∥ ((N - 1)! + 1))$
34	23 33	mpd	$⊢ ((N \in ℤ_{\geq 2} \land N ∥ ((N - 1)! + 1)) \land n \in (2 \dots N - 1)) \to \neg n ∥ ((N - 1)! + 1)$
35		simplr	$⊢ ((N \in ℤ_{\geq 2} \land N ∥ ((N - 1)! + 1)) \land n \in (2 \dots N - 1)) \to N ∥ ((N - 1)! + 1)$
36	19	nnzd	$⊢ ((N \in ℤ_{\geq 2} \land N ∥ ((N - 1)! + 1)) \land n \in (2 \dots N - 1)) \to n \in ℤ$
37	25	nnzd	$⊢ ((N \in ℤ_{\geq 2} \land N ∥ ((N - 1)! + 1)) \land n \in (2 \dots N - 1)) \to N \in ℤ$
38	29	peano2zd	$⊢ ((N \in ℤ_{\geq 2} \land N ∥ ((N - 1)! + 1)) \land n \in (2 \dots N - 1)) \to (N - 1)! + 1 \in ℤ$
39		dvdstr	$⊢ (n \in ℤ \land N \in ℤ \land (N - 1)! + 1 \in ℤ) \to ((n ∥ N \land N ∥ ((N - 1)! + 1)) \to n ∥ ((N - 1)! + 1))$
40	36 37 38 39	syl3anc	$⊢ ((N \in ℤ_{\geq 2} \land N ∥ ((N - 1)! + 1)) \land n \in (2 \dots N - 1)) \to ((n ∥ N \land N ∥ ((N - 1)! + 1)) \to n ∥ ((N - 1)! + 1))$
41	35 40	mpan2d	$⊢ ((N \in ℤ_{\geq 2} \land N ∥ ((N - 1)! + 1)) \land n \in (2 \dots N - 1)) \to (n ∥ N \to n ∥ ((N - 1)! + 1))$
42	34 41	mtod	$⊢ ((N \in ℤ_{\geq 2} \land N ∥ ((N - 1)! + 1)) \land n \in (2 \dots N - 1)) \to \neg n ∥ N$
43	42	ralrimiva	$⊢ (N \in ℤ_{\geq 2} \land N ∥ ((N - 1)! + 1)) \to \forall n \in (2 \dots N - 1) \neg n ∥ N$
44		isprm3	$⊢ N \in ℙ \leftrightarrow (N \in ℤ_{\geq 2} \land \forall n \in (2 \dots N - 1) \neg n ∥ N)$
45	15 43 44	sylanbrc	$⊢ (N \in ℤ_{\geq 2} \land N ∥ ((N - 1)! + 1)) \to N \in ℙ$
46	14 45	impbii	$⊢ N \in ℙ \leftrightarrow (N \in ℤ_{\geq 2} \land N ∥ ((N - 1)! + 1))$

Metamath Proof Explorer

Theorem wilth

Proof