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	$⊢ (P \in ℙ \land N \in (1 \dots P - 1)) \to (N = N^{P - 2} \mod P \leftrightarrow (N = 1 \lor N = P - 1))$

Proof

Step	Hyp	Ref	Expression
1		elfzelz	$⊢ N \in (1 \dots P - 1) \to N \in ℤ$
2	1	adantl	$⊢ (P \in ℙ \land N \in (1 \dots P - 1)) \to N \in ℤ$
3		peano2zm	$⊢ N \in ℤ \to N - 1 \in ℤ$
4	2 3	syl	$⊢ (P \in ℙ \land N \in (1 \dots P - 1)) \to N - 1 \in ℤ$
5	4	zcnd	$⊢ (P \in ℙ \land N \in (1 \dots P - 1)) \to N - 1 \in ℂ$
6	2	peano2zd	$⊢ (P \in ℙ \land N \in (1 \dots P - 1)) \to N + 1 \in ℤ$
7	6	zcnd	$⊢ (P \in ℙ \land N \in (1 \dots P - 1)) \to N + 1 \in ℂ$
8	5 7	mulcomd	$⊢ (P \in ℙ \land N \in (1 \dots P - 1)) \to (N - 1) (N + 1) = (N + 1) (N - 1)$
9	2	zcnd	$⊢ (P \in ℙ \land N \in (1 \dots P - 1)) \to N \in ℂ$
10		ax-1cn	$⊢ 1 \in ℂ$
11		subsq	$⊢ (N \in ℂ \land 1 \in ℂ) \to N^{2} - 1^{2} = (N + 1) (N - 1)$
12	9 10 11	sylancl	$⊢ (P \in ℙ \land N \in (1 \dots P - 1)) \to N^{2} - 1^{2} = (N + 1) (N - 1)$
13	9	sqvald	$⊢ (P \in ℙ \land N \in (1 \dots P - 1)) \to N^{2} = N \cdot N$
14		sq1	$⊢ 1^{2} = 1$
15	14	a1i	$⊢ (P \in ℙ \land N \in (1 \dots P - 1)) \to 1^{2} = 1$
16	13 15	oveq12d	$⊢ (P \in ℙ \land N \in (1 \dots P - 1)) \to N^{2} - 1^{2} = N \cdot N - 1$
17	8 12 16	3eqtr2d	$⊢ (P \in ℙ \land N \in (1 \dots P - 1)) \to (N - 1) (N + 1) = N \cdot N - 1$
18	17	breq2d	$⊢ (P \in ℙ \land N \in (1 \dots P - 1)) \to (P ∥ (N - 1) (N + 1) \leftrightarrow P ∥ (N \cdot N - 1))$
19		fz1ssfz0	$⊢ (1 \dots P - 1) \subseteq (0 \dots P - 1)$
20		simpr	$⊢ (P \in ℙ \land N \in (1 \dots P - 1)) \to N \in (1 \dots P - 1)$
21	19 20	sselid	$⊢ (P \in ℙ \land N \in (1 \dots P - 1)) \to N \in (0 \dots P - 1)$
22	21	biantrurd	$⊢ (P \in ℙ \land N \in (1 \dots P - 1)) \to (P ∥ (N \cdot N - 1) \leftrightarrow (N \in (0 \dots P - 1) \land P ∥ (N \cdot N - 1)))$
23	18 22	bitrd	$⊢ (P \in ℙ \land N \in (1 \dots P - 1)) \to (P ∥ (N - 1) (N + 1) \leftrightarrow (N \in (0 \dots P - 1) \land P ∥ (N \cdot N - 1)))$
24		simpl	$⊢ (P \in ℙ \land N \in (1 \dots P - 1)) \to P \in ℙ$
25		euclemma	$⊢ (P \in ℙ \land N - 1 \in ℤ \land N + 1 \in ℤ) \to (P ∥ (N - 1) (N + 1) \leftrightarrow (P ∥ (N - 1) \lor P ∥ (N + 1)))$
26	24 4 6 25	syl3anc	$⊢ (P \in ℙ \land N \in (1 \dots P - 1)) \to (P ∥ (N - 1) (N + 1) \leftrightarrow (P ∥ (N - 1) \lor P ∥ (N + 1)))$
27		prmnn	$⊢ P \in ℙ \to P \in ℕ$
28		fzm1ndvds	$⊢ (P \in ℕ \land N \in (1 \dots P - 1)) \to \neg P ∥ N$
29	27 28	sylan	$⊢ (P \in ℙ \land N \in (1 \dots P - 1)) \to \neg P ∥ N$
30		eqid	$⊢ N^{P - 2} \mod P = N^{P - 2} \mod P$
31	30	prmdiveq	$⊢ (P \in ℙ \land N \in ℤ \land \neg P ∥ N) \to ((N \in (0 \dots P - 1) \land P ∥ (N \cdot N - 1)) \leftrightarrow N = N^{P - 2} \mod P)$
32	24 2 29 31	syl3anc	$⊢ (P \in ℙ \land N \in (1 \dots P - 1)) \to ((N \in (0 \dots P - 1) \land P ∥ (N \cdot N - 1)) \leftrightarrow N = N^{P - 2} \mod P)$
33	23 26 32	3bitr3rd	$⊢ (P \in ℙ \land N \in (1 \dots P - 1)) \to (N = N^{P - 2} \mod P \leftrightarrow (P ∥ (N - 1) \lor P ∥ (N + 1)))$
34	24 27	syl	$⊢ (P \in ℙ \land N \in (1 \dots P - 1)) \to P \in ℕ$
35		1zzd	$⊢ (P \in ℙ \land N \in (1 \dots P - 1)) \to 1 \in ℤ$
36		moddvds	$⊢ (P \in ℕ \land N \in ℤ \land 1 \in ℤ) \to (N \mod P = 1 \mod P \leftrightarrow P ∥ (N - 1))$
37	34 2 35 36	syl3anc	$⊢ (P \in ℙ \land N \in (1 \dots P - 1)) \to (N \mod P = 1 \mod P \leftrightarrow P ∥ (N - 1))$
38		elfznn	$⊢ N \in (1 \dots P - 1) \to N \in ℕ$
39	38	adantl	$⊢ (P \in ℙ \land N \in (1 \dots P - 1)) \to N \in ℕ$
40	39	nnred	$⊢ (P \in ℙ \land N \in (1 \dots P - 1)) \to N \in ℝ$
41	34	nnrpd	$⊢ (P \in ℙ \land N \in (1 \dots P - 1)) \to P \in ℝ^{+}$
42	39	nnnn0d	$⊢ (P \in ℙ \land N \in (1 \dots P - 1)) \to N \in ℕ_{0}$
43	42	nn0ge0d	$⊢ (P \in ℙ \land N \in (1 \dots P - 1)) \to 0 \leq N$
44		elfzle2	$⊢ N \in (1 \dots P - 1) \to N \leq P - 1$
45	44	adantl	$⊢ (P \in ℙ \land N \in (1 \dots P - 1)) \to N \leq P - 1$
46		prmz	$⊢ P \in ℙ \to P \in ℤ$
47		zltlem1	$⊢ (N \in ℤ \land P \in ℤ) \to (N < P \leftrightarrow N \leq P - 1)$
48	1 46 47	syl2anr	$⊢ (P \in ℙ \land N \in (1 \dots P - 1)) \to (N < P \leftrightarrow N \leq P - 1)$
49	45 48	mpbird	$⊢ (P \in ℙ \land N \in (1 \dots P - 1)) \to N < P$
50		modid	$⊢ ((N \in ℝ \land P \in ℝ^{+}) \land (0 \leq N \land N < P)) \to N \mod P = N$
51	40 41 43 49 50	syl22anc	$⊢ (P \in ℙ \land N \in (1 \dots P - 1)) \to N \mod P = N$
52	34	nnred	$⊢ (P \in ℙ \land N \in (1 \dots P - 1)) \to P \in ℝ$
53		prmuz2	$⊢ P \in ℙ \to P \in ℤ_{\geq 2}$
54	24 53	syl	$⊢ (P \in ℙ \land N \in (1 \dots P - 1)) \to P \in ℤ_{\geq 2}$
55		eluz2gt1	$⊢ P \in ℤ_{\geq 2} \to 1 < P$
56	54 55	syl	$⊢ (P \in ℙ \land N \in (1 \dots P - 1)) \to 1 < P$
57		1mod	$⊢ (P \in ℝ \land 1 < P) \to 1 \mod P = 1$
58	52 56 57	syl2anc	$⊢ (P \in ℙ \land N \in (1 \dots P - 1)) \to 1 \mod P = 1$
59	51 58	eqeq12d	$⊢ (P \in ℙ \land N \in (1 \dots P - 1)) \to (N \mod P = 1 \mod P \leftrightarrow N = 1)$
60	37 59	bitr3d	$⊢ (P \in ℙ \land N \in (1 \dots P - 1)) \to (P ∥ (N - 1) \leftrightarrow N = 1)$
61	35	znegcld	$⊢ (P \in ℙ \land N \in (1 \dots P - 1)) \to - 1 \in ℤ$
62		moddvds	$⊢ (P \in ℕ \land N \in ℤ \land - 1 \in ℤ) \to (N \mod P = -1 \mod P \leftrightarrow P ∥ (N - -1))$
63	34 2 61 62	syl3anc	$⊢ (P \in ℙ \land N \in (1 \dots P - 1)) \to (N \mod P = -1 \mod P \leftrightarrow P ∥ (N - -1))$
64	34	nncnd	$⊢ (P \in ℙ \land N \in (1 \dots P - 1)) \to P \in ℂ$
65	64	mulid2d	$⊢ (P \in ℙ \land N \in (1 \dots P - 1)) \to 1 P = P$
66	65	oveq2d	$⊢ (P \in ℙ \land N \in (1 \dots P - 1)) \to - 1 + 1 P = - 1 + P$
67		neg1cn	$⊢ - 1 \in ℂ$
68		addcom	$⊢ (- 1 \in ℂ \land P \in ℂ) \to - 1 + P = P + -1$
69	67 64 68	sylancr	$⊢ (P \in ℙ \land N \in (1 \dots P - 1)) \to - 1 + P = P + -1$
70		negsub	$⊢ (P \in ℂ \land 1 \in ℂ) \to P + -1 = P - 1$
71	64 10 70	sylancl	$⊢ (P \in ℙ \land N \in (1 \dots P - 1)) \to P + -1 = P - 1$
72	66 69 71	3eqtrd	$⊢ (P \in ℙ \land N \in (1 \dots P - 1)) \to - 1 + 1 P = P - 1$
73	72	oveq1d	$⊢ (P \in ℙ \land N \in (1 \dots P - 1)) \to (- 1 + 1 P) \mod P = (P - 1) \mod P$
74		neg1rr	$⊢ - 1 \in ℝ$
75	74	a1i	$⊢ (P \in ℙ \land N \in (1 \dots P - 1)) \to - 1 \in ℝ$
76		modcyc	$⊢ (- 1 \in ℝ \land P \in ℝ^{+} \land 1 \in ℤ) \to (- 1 + 1 P) \mod P = -1 \mod P$
77	75 41 35 76	syl3anc	$⊢ (P \in ℙ \land N \in (1 \dots P - 1)) \to (- 1 + 1 P) \mod P = -1 \mod P$
78		peano2rem	$⊢ P \in ℝ \to P - 1 \in ℝ$
79	52 78	syl	$⊢ (P \in ℙ \land N \in (1 \dots P - 1)) \to P - 1 \in ℝ$
80		nnm1nn0	$⊢ P \in ℕ \to P - 1 \in ℕ_{0}$
81	34 80	syl	$⊢ (P \in ℙ \land N \in (1 \dots P - 1)) \to P - 1 \in ℕ_{0}$
82	81	nn0ge0d	$⊢ (P \in ℙ \land N \in (1 \dots P - 1)) \to 0 \leq P - 1$
83	52	ltm1d	$⊢ (P \in ℙ \land N \in (1 \dots P - 1)) \to P - 1 < P$
84		modid	$⊢ ((P - 1 \in ℝ \land P \in ℝ^{+}) \land (0 \leq P - 1 \land P - 1 < P)) \to (P - 1) \mod P = P - 1$
85	79 41 82 83 84	syl22anc	$⊢ (P \in ℙ \land N \in (1 \dots P - 1)) \to (P - 1) \mod P = P - 1$
86	73 77 85	3eqtr3d	$⊢ (P \in ℙ \land N \in (1 \dots P - 1)) \to -1 \mod P = P - 1$
87	51 86	eqeq12d	$⊢ (P \in ℙ \land N \in (1 \dots P - 1)) \to (N \mod P = -1 \mod P \leftrightarrow N = P - 1)$
88		subneg	$⊢ (N \in ℂ \land 1 \in ℂ) \to N - -1 = N + 1$
89	9 10 88	sylancl	$⊢ (P \in ℙ \land N \in (1 \dots P - 1)) \to N - -1 = N + 1$
90	89	breq2d	$⊢ (P \in ℙ \land N \in (1 \dots P - 1)) \to (P ∥ (N - -1) \leftrightarrow P ∥ (N + 1))$
91	63 87 90	3bitr3rd	$⊢ (P \in ℙ \land N \in (1 \dots P - 1)) \to (P ∥ (N + 1) \leftrightarrow N = P - 1)$
92	60 91	orbi12d	$⊢ (P \in ℙ \land N \in (1 \dots P - 1)) \to ((P ∥ (N - 1) \lor P ∥ (N + 1)) \leftrightarrow (N = 1 \lor N = P - 1))$
93	33 92	bitrd	$⊢ (P \in ℙ \land N \in (1 \dots P - 1)) \to (N = N^{P - 2} \mod P \leftrightarrow (N = 1 \lor N = P - 1))$

Metamath Proof Explorer

Theorem wilthlem1

Proof