Theorem lgslem4

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

	Ref	Expression
Hypothesis	lgslem2.z	⊢ 𝑍 = { 𝑥 ∈ ℤ ∣ ( abs ‘ 𝑥 ) ≤ 1 }
Assertion	lgslem4	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → ( ( ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) + 1 ) mod 𝑃 ) − 1 ) ∈ 𝑍 )

Proof

Step	Hyp	Ref	Expression
1		lgslem2.z	⊢ 𝑍 = { 𝑥 ∈ ℤ ∣ ( abs ‘ 𝑥 ) ≤ 1 }
2		eldifi	⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → 𝑃 ∈ ℙ )
3	2	adantl	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → 𝑃 ∈ ℙ )
4		simpl	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → 𝐴 ∈ ℤ )
5		oddprm	⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → ( ( 𝑃 − 1 ) / 2 ) ∈ ℕ )
6	5	adantl	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → ( ( 𝑃 − 1 ) / 2 ) ∈ ℕ )
7		prmdvdsexp	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ( ( 𝑃 − 1 ) / 2 ) ∈ ℕ ) → ( 𝑃 ∥ ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) ↔ 𝑃 ∥ 𝐴 ) )
8	3 4 6 7	syl3anc	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → ( 𝑃 ∥ ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) ↔ 𝑃 ∥ 𝐴 ) )
9	8	biimpar	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ 𝑃 ∥ 𝐴 ) → 𝑃 ∥ ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) )
10		prmgt1	⊢ ( 𝑃 ∈ ℙ → 1 < 𝑃 )
11	2 10	syl	⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → 1 < 𝑃 )
12	11	ad2antlr	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ 𝑃 ∥ 𝐴 ) → 1 < 𝑃 )
13		p1modz1	⊢ ( ( 𝑃 ∥ ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) ∧ 1 < 𝑃 ) → ( ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) + 1 ) mod 𝑃 ) = 1 )
14	9 12 13	syl2anc	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ 𝑃 ∥ 𝐴 ) → ( ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) + 1 ) mod 𝑃 ) = 1 )
15	14	oveq1d	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ 𝑃 ∥ 𝐴 ) → ( ( ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) + 1 ) mod 𝑃 ) − 1 ) = ( 1 − 1 ) )
16		1m1e0	⊢ ( 1 − 1 ) = 0
17	1	lgslem2	⊢ ( - 1 ∈ 𝑍 ∧ 0 ∈ 𝑍 ∧ 1 ∈ 𝑍 )
18	17	simp2i	⊢ 0 ∈ 𝑍
19	16 18	eqeltri	⊢ ( 1 − 1 ) ∈ 𝑍
20	15 19	eqeltrdi	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ 𝑃 ∥ 𝐴 ) → ( ( ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) + 1 ) mod 𝑃 ) − 1 ) ∈ 𝑍 )
21		lgslem1	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 𝑃 ∥ 𝐴 ) → ( ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) + 1 ) mod 𝑃 ) ∈ { 0 , 2 } )
22		elpri	⊢ ( ( ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) + 1 ) mod 𝑃 ) ∈ { 0 , 2 } → ( ( ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) + 1 ) mod 𝑃 ) = 0 ∨ ( ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) + 1 ) mod 𝑃 ) = 2 ) )
23		oveq1	⊢ ( ( ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) + 1 ) mod 𝑃 ) = 0 → ( ( ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) + 1 ) mod 𝑃 ) − 1 ) = ( 0 − 1 ) )
24		df-neg	⊢ - 1 = ( 0 − 1 )
25	17	simp1i	⊢ - 1 ∈ 𝑍
26	24 25	eqeltrri	⊢ ( 0 − 1 ) ∈ 𝑍
27	23 26	eqeltrdi	⊢ ( ( ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) + 1 ) mod 𝑃 ) = 0 → ( ( ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) + 1 ) mod 𝑃 ) − 1 ) ∈ 𝑍 )
28		oveq1	⊢ ( ( ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) + 1 ) mod 𝑃 ) = 2 → ( ( ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) + 1 ) mod 𝑃 ) − 1 ) = ( 2 − 1 ) )
29		2m1e1	⊢ ( 2 − 1 ) = 1
30	17	simp3i	⊢ 1 ∈ 𝑍
31	29 30	eqeltri	⊢ ( 2 − 1 ) ∈ 𝑍
32	28 31	eqeltrdi	⊢ ( ( ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) + 1 ) mod 𝑃 ) = 2 → ( ( ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) + 1 ) mod 𝑃 ) − 1 ) ∈ 𝑍 )
33	27 32	jaoi	⊢ ( ( ( ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) + 1 ) mod 𝑃 ) = 0 ∨ ( ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) + 1 ) mod 𝑃 ) = 2 ) → ( ( ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) + 1 ) mod 𝑃 ) − 1 ) ∈ 𝑍 )
34	21 22 33	3syl	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 𝑃 ∥ 𝐴 ) → ( ( ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) + 1 ) mod 𝑃 ) − 1 ) ∈ 𝑍 )
35	34	3expa	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ¬ 𝑃 ∥ 𝐴 ) → ( ( ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) + 1 ) mod 𝑃 ) − 1 ) ∈ 𝑍 )
36	20 35	pm2.61dan	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → ( ( ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) + 1 ) mod 𝑃 ) − 1 ) ∈ 𝑍 )