lgslem1

Description: When a is coprime to the prime p , a ^ ( ( p - 1 ) / 2 ) is equivalent mod p to 1 or -u 1 , and so adding 1 makes it equivalent to 0 or 2 . (Contributed by Mario Carneiro, 4-Feb-2015)

		Ref	Expression
	Assertion	lgslem1	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\}) \land \neg P ∥ A) \to (A^{\frac{P - 1}{2}} + 1) \mod P \in \{0, 2\}$

Proof

Step	Hyp	Ref	Expression
1		eldifi	$⊢ P \in (ℙ ∖ \{2\}) \to P \in ℙ$
2	1	3ad2ant2	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\}) \land \neg P ∥ A) \to P \in ℙ$
3		prmnn	$⊢ P \in ℙ \to P \in ℕ$
4	2 3	syl	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\}) \land \neg P ∥ A) \to P \in ℕ$
5		simp1	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\}) \land \neg P ∥ A) \to A \in ℤ$
6		prmz	$⊢ P \in ℙ \to P \in ℤ$
7	2 6	syl	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\}) \land \neg P ∥ A) \to P \in ℤ$
8	5 7	gcdcomd	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\}) \land \neg P ∥ A) \to A \gcd P = P \gcd A$
9		simp3	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\}) \land \neg P ∥ A) \to \neg P ∥ A$
10		coprm	$⊢ (P \in ℙ \land A \in ℤ) \to (\neg P ∥ A \leftrightarrow P \gcd A = 1)$
11	2 5 10	syl2anc	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\}) \land \neg P ∥ A) \to (\neg P ∥ A \leftrightarrow P \gcd A = 1)$
12	9 11	mpbid	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\}) \land \neg P ∥ A) \to P \gcd A = 1$
13	8 12	eqtrd	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\}) \land \neg P ∥ A) \to A \gcd P = 1$
14		eulerth	$⊢ (P \in ℕ \land A \in ℤ \land A \gcd P = 1) \to A^{ϕ (P)} \mod P = 1 \mod P$
15	4 5 13 14	syl3anc	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\}) \land \neg P ∥ A) \to A^{ϕ (P)} \mod P = 1 \mod P$
16		phiprm	$⊢ P \in ℙ \to ϕ (P) = P - 1$
17	2 16	syl	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\}) \land \neg P ∥ A) \to ϕ (P) = P - 1$
18		nnm1nn0	$⊢ P \in ℕ \to P - 1 \in ℕ_{0}$
19	4 18	syl	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\}) \land \neg P ∥ A) \to P - 1 \in ℕ_{0}$
20	17 19	eqeltrd	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\}) \land \neg P ∥ A) \to ϕ (P) \in ℕ_{0}$
21		zexpcl	$⊢ (A \in ℤ \land ϕ (P) \in ℕ_{0}) \to A^{ϕ (P)} \in ℤ$
22	5 20 21	syl2anc	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\}) \land \neg P ∥ A) \to A^{ϕ (P)} \in ℤ$
23		1zzd	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\}) \land \neg P ∥ A) \to 1 \in ℤ$
24		moddvds	$⊢ (P \in ℕ \land A^{ϕ (P)} \in ℤ \land 1 \in ℤ) \to (A^{ϕ (P)} \mod P = 1 \mod P \leftrightarrow P ∥ (A^{ϕ (P)} - 1))$
25	4 22 23 24	syl3anc	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\}) \land \neg P ∥ A) \to (A^{ϕ (P)} \mod P = 1 \mod P \leftrightarrow P ∥ (A^{ϕ (P)} - 1))$
26	15 25	mpbid	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\}) \land \neg P ∥ A) \to P ∥ (A^{ϕ (P)} - 1)$
27	19	nn0cnd	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\}) \land \neg P ∥ A) \to P - 1 \in ℂ$
28		2cnd	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\}) \land \neg P ∥ A) \to 2 \in ℂ$
29		2ne0	$⊢ 2 \neq 0$
30	29	a1i	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\}) \land \neg P ∥ A) \to 2 \neq 0$
31	27 28 30	divcan1d	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\}) \land \neg P ∥ A) \to (\frac{P - 1}{2}) \cdot 2 = P - 1$
32	17 31	eqtr4d	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\}) \land \neg P ∥ A) \to ϕ (P) = (\frac{P - 1}{2}) \cdot 2$
33	32	oveq2d	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\}) \land \neg P ∥ A) \to A^{ϕ (P)} = A^{(\frac{P - 1}{2}) \cdot 2}$
34	5	zcnd	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\}) \land \neg P ∥ A) \to A \in ℂ$
35		2nn0	$⊢ 2 \in ℕ_{0}$
36	35	a1i	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\}) \land \neg P ∥ A) \to 2 \in ℕ_{0}$
37		oddprm	$⊢ P \in (ℙ ∖ \{2\}) \to \frac{P - 1}{2} \in ℕ$
38	37	3ad2ant2	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\}) \land \neg P ∥ A) \to \frac{P - 1}{2} \in ℕ$
39	38	nnnn0d	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\}) \land \neg P ∥ A) \to \frac{P - 1}{2} \in ℕ_{0}$
40	34 36 39	expmuld	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\}) \land \neg P ∥ A) \to A^{(\frac{P - 1}{2}) \cdot 2} = {(A^{\frac{P - 1}{2}})}^{2}$
41	33 40	eqtrd	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\}) \land \neg P ∥ A) \to A^{ϕ (P)} = {(A^{\frac{P - 1}{2}})}^{2}$
42	41	oveq1d	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\}) \land \neg P ∥ A) \to A^{ϕ (P)} - 1 = {(A^{\frac{P - 1}{2}})}^{2} - 1$
43		sq1	$⊢ 1^{2} = 1$
44	43	oveq2i	$⊢ {(A^{\frac{P - 1}{2}})}^{2} - 1^{2} = {(A^{\frac{P - 1}{2}})}^{2} - 1$
45	42 44	eqtr4di	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\}) \land \neg P ∥ A) \to A^{ϕ (P)} - 1 = {(A^{\frac{P - 1}{2}})}^{2} - 1^{2}$
46		zexpcl	$⊢ (A \in ℤ \land \frac{P - 1}{2} \in ℕ_{0}) \to A^{\frac{P - 1}{2}} \in ℤ$
47	5 39 46	syl2anc	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\}) \land \neg P ∥ A) \to A^{\frac{P - 1}{2}} \in ℤ$
48	47	zcnd	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\}) \land \neg P ∥ A) \to A^{\frac{P - 1}{2}} \in ℂ$
49		ax-1cn	$⊢ 1 \in ℂ$
50		subsq	$⊢ (A^{\frac{P - 1}{2}} \in ℂ \land 1 \in ℂ) \to {(A^{\frac{P - 1}{2}})}^{2} - 1^{2} = (A^{\frac{P - 1}{2}} + 1) (A^{\frac{P - 1}{2}} - 1)$
51	48 49 50	sylancl	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\}) \land \neg P ∥ A) \to {(A^{\frac{P - 1}{2}})}^{2} - 1^{2} = (A^{\frac{P - 1}{2}} + 1) (A^{\frac{P - 1}{2}} - 1)$
52	45 51	eqtrd	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\}) \land \neg P ∥ A) \to A^{ϕ (P)} - 1 = (A^{\frac{P - 1}{2}} + 1) (A^{\frac{P - 1}{2}} - 1)$
53	26 52	breqtrd	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\}) \land \neg P ∥ A) \to P ∥ (A^{\frac{P - 1}{2}} + 1) (A^{\frac{P - 1}{2}} - 1)$
54	47	peano2zd	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\}) \land \neg P ∥ A) \to A^{\frac{P - 1}{2}} + 1 \in ℤ$
55		peano2zm	$⊢ A^{\frac{P - 1}{2}} \in ℤ \to A^{\frac{P - 1}{2}} - 1 \in ℤ$
56	47 55	syl	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\}) \land \neg P ∥ A) \to A^{\frac{P - 1}{2}} - 1 \in ℤ$
57		euclemma	$⊢ (P \in ℙ \land A^{\frac{P - 1}{2}} + 1 \in ℤ \land A^{\frac{P - 1}{2}} - 1 \in ℤ) \to (P ∥ (A^{\frac{P - 1}{2}} + 1) (A^{\frac{P - 1}{2}} - 1) \leftrightarrow (P ∥ (A^{\frac{P - 1}{2}} + 1) \lor P ∥ (A^{\frac{P - 1}{2}} - 1)))$
58	2 54 56 57	syl3anc	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\}) \land \neg P ∥ A) \to (P ∥ (A^{\frac{P - 1}{2}} + 1) (A^{\frac{P - 1}{2}} - 1) \leftrightarrow (P ∥ (A^{\frac{P - 1}{2}} + 1) \lor P ∥ (A^{\frac{P - 1}{2}} - 1)))$
59	53 58	mpbid	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\}) \land \neg P ∥ A) \to (P ∥ (A^{\frac{P - 1}{2}} + 1) \lor P ∥ (A^{\frac{P - 1}{2}} - 1))$
60		dvdsval3	$⊢ (P \in ℕ \land A^{\frac{P - 1}{2}} + 1 \in ℤ) \to (P ∥ (A^{\frac{P - 1}{2}} + 1) \leftrightarrow (A^{\frac{P - 1}{2}} + 1) \mod P = 0)$
61	4 54 60	syl2anc	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\}) \land \neg P ∥ A) \to (P ∥ (A^{\frac{P - 1}{2}} + 1) \leftrightarrow (A^{\frac{P - 1}{2}} + 1) \mod P = 0)$
62		2z	$⊢ 2 \in ℤ$
63	62	a1i	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\}) \land \neg P ∥ A) \to 2 \in ℤ$
64		moddvds	$⊢ (P \in ℕ \land A^{\frac{P - 1}{2}} + 1 \in ℤ \land 2 \in ℤ) \to ((A^{\frac{P - 1}{2}} + 1) \mod P = 2 \mod P \leftrightarrow P ∥ (A^{\frac{P - 1}{2}} + 1 - 2))$
65	4 54 63 64	syl3anc	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\}) \land \neg P ∥ A) \to ((A^{\frac{P - 1}{2}} + 1) \mod P = 2 \mod P \leftrightarrow P ∥ (A^{\frac{P - 1}{2}} + 1 - 2))$
66		2re	$⊢ 2 \in ℝ$
67	66	a1i	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\}) \land \neg P ∥ A) \to 2 \in ℝ$
68	4	nnrpd	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\}) \land \neg P ∥ A) \to P \in ℝ^{+}$
69		0le2	$⊢ 0 \leq 2$
70	69	a1i	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\}) \land \neg P ∥ A) \to 0 \leq 2$
71	4	nnred	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\}) \land \neg P ∥ A) \to P \in ℝ$
72		prmuz2	$⊢ P \in ℙ \to P \in ℤ_{\geq 2}$
73	2 72	syl	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\}) \land \neg P ∥ A) \to P \in ℤ_{\geq 2}$
74		eluzle	$⊢ P \in ℤ_{\geq 2} \to 2 \leq P$
75	73 74	syl	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\}) \land \neg P ∥ A) \to 2 \leq P$
76		eldifsni	$⊢ P \in (ℙ ∖ \{2\}) \to P \neq 2$
77	76	3ad2ant2	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\}) \land \neg P ∥ A) \to P \neq 2$
78	67 71 75 77	leneltd	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\}) \land \neg P ∥ A) \to 2 < P$
79		modid	$⊢ ((2 \in ℝ \land P \in ℝ^{+}) \land (0 \leq 2 \land 2 < P)) \to 2 \mod P = 2$
80	67 68 70 78 79	syl22anc	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\}) \land \neg P ∥ A) \to 2 \mod P = 2$
81	80	eqeq2d	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\}) \land \neg P ∥ A) \to ((A^{\frac{P - 1}{2}} + 1) \mod P = 2 \mod P \leftrightarrow (A^{\frac{P - 1}{2}} + 1) \mod P = 2)$
82		df-2	$⊢ 2 = 1 + 1$
83	82	oveq2i	$⊢ A^{\frac{P - 1}{2}} + 1 - 2 = A^{\frac{P - 1}{2}} + 1 - (1 + 1)$
84	49	a1i	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\}) \land \neg P ∥ A) \to 1 \in ℂ$
85	48 84 84	pnpcan2d	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\}) \land \neg P ∥ A) \to A^{\frac{P - 1}{2}} + 1 - (1 + 1) = A^{\frac{P - 1}{2}} - 1$
86	83 85	syl5eq	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\}) \land \neg P ∥ A) \to A^{\frac{P - 1}{2}} + 1 - 2 = A^{\frac{P - 1}{2}} - 1$
87	86	breq2d	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\}) \land \neg P ∥ A) \to (P ∥ (A^{\frac{P - 1}{2}} + 1 - 2) \leftrightarrow P ∥ (A^{\frac{P - 1}{2}} - 1))$
88	65 81 87	3bitr3rd	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\}) \land \neg P ∥ A) \to (P ∥ (A^{\frac{P - 1}{2}} - 1) \leftrightarrow (A^{\frac{P - 1}{2}} + 1) \mod P = 2)$
89	61 88	orbi12d	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\}) \land \neg P ∥ A) \to ((P ∥ (A^{\frac{P - 1}{2}} + 1) \lor P ∥ (A^{\frac{P - 1}{2}} - 1)) \leftrightarrow ((A^{\frac{P - 1}{2}} + 1) \mod P = 0 \lor (A^{\frac{P - 1}{2}} + 1) \mod P = 2))$
90	59 89	mpbid	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\}) \land \neg P ∥ A) \to ((A^{\frac{P - 1}{2}} + 1) \mod P = 0 \lor (A^{\frac{P - 1}{2}} + 1) \mod P = 2)$
91		ovex	$⊢ (A^{\frac{P - 1}{2}} + 1) \mod P \in V$
92	91	elpr	$⊢ (A^{\frac{P - 1}{2}} + 1) \mod P \in \{0, 2\} \leftrightarrow ((A^{\frac{P - 1}{2}} + 1) \mod P = 0 \lor (A^{\frac{P - 1}{2}} + 1) \mod P = 2)$
93	90 92	sylibr	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\}) \land \neg P ∥ A) \to (A^{\frac{P - 1}{2}} + 1) \mod P \in \{0, 2\}$

Metamath Proof Explorer

Theorem lgslem1

Proof