lgslem4

Description: Lemma for lgsfcl2 . (Contributed by Mario Carneiro, 4-Feb-2015) (Proof shortened by AV, 19-Mar-2022)

		Ref	Expression
	Hypothesis	lgslem2.z	$⊢ Z = \{x \in ℤ \| \|x\| \leq 1\}$
	Assertion	lgslem4	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\})) \to ((A^{\frac{P - 1}{2}} + 1) \mod P) - 1 \in Z$

Proof

Step	Hyp	Ref	Expression
1		lgslem2.z	$⊢ Z = \{x \in ℤ \| \|x\| \leq 1\}$
2		eldifi	$⊢ P \in (ℙ ∖ \{2\}) \to P \in ℙ$
3	2	adantl	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\})) \to P \in ℙ$
4		simpl	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\})) \to A \in ℤ$
5		oddprm	$⊢ P \in (ℙ ∖ \{2\}) \to \frac{P - 1}{2} \in ℕ$
6	5	adantl	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\})) \to \frac{P - 1}{2} \in ℕ$
7		prmdvdsexp	$⊢ (P \in ℙ \land A \in ℤ \land \frac{P - 1}{2} \in ℕ) \to (P ∥ A^{\frac{P - 1}{2}} \leftrightarrow P ∥ A)$
8	3 4 6 7	syl3anc	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\})) \to (P ∥ A^{\frac{P - 1}{2}} \leftrightarrow P ∥ A)$
9	8	biimpar	$⊢ ((A \in ℤ \land P \in (ℙ ∖ \{2\})) \land P ∥ A) \to P ∥ A^{\frac{P - 1}{2}}$
10		prmgt1	$⊢ P \in ℙ \to 1 < P$
11	2 10	syl	$⊢ P \in (ℙ ∖ \{2\}) \to 1 < P$
12	11	ad2antlr	$⊢ ((A \in ℤ \land P \in (ℙ ∖ \{2\})) \land P ∥ A) \to 1 < P$
13		p1modz1	$⊢ (P ∥ A^{\frac{P - 1}{2}} \land 1 < P) \to (A^{\frac{P - 1}{2}} + 1) \mod P = 1$
14	9 12 13	syl2anc	$⊢ ((A \in ℤ \land P \in (ℙ ∖ \{2\})) \land P ∥ A) \to (A^{\frac{P - 1}{2}} + 1) \mod P = 1$
15	14	oveq1d	$⊢ ((A \in ℤ \land P \in (ℙ ∖ \{2\})) \land P ∥ A) \to ((A^{\frac{P - 1}{2}} + 1) \mod P) - 1 = 1 - 1$
16		1m1e0	$⊢ 1 - 1 = 0$
17	1	lgslem2	$⊢ (- 1 \in Z \land 0 \in Z \land 1 \in Z)$
18	17	simp2i	$⊢ 0 \in Z$
19	16 18	eqeltri	$⊢ 1 - 1 \in Z$
20	15 19	eqeltrdi	$⊢ ((A \in ℤ \land P \in (ℙ ∖ \{2\})) \land P ∥ A) \to ((A^{\frac{P - 1}{2}} + 1) \mod P) - 1 \in Z$
21		lgslem1	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\}) \land \neg P ∥ A) \to (A^{\frac{P - 1}{2}} + 1) \mod P \in \{0, 2\}$
22		elpri	$⊢ (A^{\frac{P - 1}{2}} + 1) \mod P \in \{0, 2\} \to ((A^{\frac{P - 1}{2}} + 1) \mod P = 0 \lor (A^{\frac{P - 1}{2}} + 1) \mod P = 2)$
23		oveq1	$⊢ (A^{\frac{P - 1}{2}} + 1) \mod P = 0 \to ((A^{\frac{P - 1}{2}} + 1) \mod P) - 1 = 0 - 1$
24		df-neg	$⊢ - 1 = 0 - 1$
25	17	simp1i	$⊢ - 1 \in Z$
26	24 25	eqeltrri	$⊢ 0 - 1 \in Z$
27	23 26	eqeltrdi	$⊢ (A^{\frac{P - 1}{2}} + 1) \mod P = 0 \to ((A^{\frac{P - 1}{2}} + 1) \mod P) - 1 \in Z$
28		oveq1	$⊢ (A^{\frac{P - 1}{2}} + 1) \mod P = 2 \to ((A^{\frac{P - 1}{2}} + 1) \mod P) - 1 = 2 - 1$
29		2m1e1	$⊢ 2 - 1 = 1$
30	17	simp3i	$⊢ 1 \in Z$
31	29 30	eqeltri	$⊢ 2 - 1 \in Z$
32	28 31	eqeltrdi	$⊢ (A^{\frac{P - 1}{2}} + 1) \mod P = 2 \to ((A^{\frac{P - 1}{2}} + 1) \mod P) - 1 \in Z$
33	27 32	jaoi	$⊢ ((A^{\frac{P - 1}{2}} + 1) \mod P = 0 \lor (A^{\frac{P - 1}{2}} + 1) \mod P = 2) \to ((A^{\frac{P - 1}{2}} + 1) \mod P) - 1 \in Z$
34	21 22 33	3syl	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\}) \land \neg P ∥ A) \to ((A^{\frac{P - 1}{2}} + 1) \mod P) - 1 \in Z$
35	34	3expa	$⊢ ((A \in ℤ \land P \in (ℙ ∖ \{2\})) \land \neg P ∥ A) \to ((A^{\frac{P - 1}{2}} + 1) \mod P) - 1 \in Z$
36	20 35	pm2.61dan	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\})) \to ((A^{\frac{P - 1}{2}} + 1) \mod P) - 1 \in Z$

Metamath Proof Explorer

Theorem lgslem4

Proof