Metamath Proof Explorer

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 
|- Z = { x e. ZZ | ( abs ` x ) <_ 1 }
Assertion lgslem4 
|- ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) -> ( ( ( ( A ^ ( ( P - 1 ) / 2 ) ) + 1 ) mod P ) - 1 ) e. Z )

Proof

Step Hyp Ref Expression
1 lgslem2.z 
 |-  Z = { x e. ZZ | ( abs ` x ) <_ 1 }
2 eldifi 
 |-  ( P e. ( Prime \ { 2 } ) -> P e. Prime )
3 2 adantl 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) -> P e. Prime )
4 simpl 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) -> A e. ZZ )
5 oddprm 
 |-  ( P e. ( Prime \ { 2 } ) -> ( ( P - 1 ) / 2 ) e. NN )
6 5 adantl 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) -> ( ( P - 1 ) / 2 ) e. NN )
7 prmdvdsexp 
 |-  ( ( P e. Prime /\ A e. ZZ /\ ( ( P - 1 ) / 2 ) e. NN ) -> ( P || ( A ^ ( ( P - 1 ) / 2 ) ) <-> P || A ) )
8 3 4 6 7 syl3anc 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) -> ( P || ( A ^ ( ( P - 1 ) / 2 ) ) <-> P || A ) )
9 8 biimpar 
 |-  ( ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) /\ P || A ) -> P || ( A ^ ( ( P - 1 ) / 2 ) ) )
10 prmgt1 
 |-  ( P e. Prime -> 1 < P )
11 2 10 syl 
 |-  ( P e. ( Prime \ { 2 } ) -> 1 < P )
12 11 ad2antlr 
 |-  ( ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) /\ P || A ) -> 1 < P )
13 p1modz1 
 |-  ( ( P || ( A ^ ( ( P - 1 ) / 2 ) ) /\ 1 < P ) -> ( ( ( A ^ ( ( P - 1 ) / 2 ) ) + 1 ) mod P ) = 1 )
14 9 12 13 syl2anc 
 |-  ( ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) /\ P || A ) -> ( ( ( A ^ ( ( P - 1 ) / 2 ) ) + 1 ) mod P ) = 1 )
15 14 oveq1d 
 |-  ( ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) /\ P || A ) -> ( ( ( ( A ^ ( ( P - 1 ) / 2 ) ) + 1 ) mod P ) - 1 ) = ( 1 - 1 ) )
16 1m1e0 
 |-  ( 1 - 1 ) = 0
17 1 lgslem2 
 |-  ( -u 1 e. Z /\ 0 e. Z /\ 1 e. Z )
18 17 simp2i 
 |-  0 e. Z
19 16 18 eqeltri 
 |-  ( 1 - 1 ) e. Z
20 15 19 eqeltrdi 
 |-  ( ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) /\ P || A ) -> ( ( ( ( A ^ ( ( P - 1 ) / 2 ) ) + 1 ) mod P ) - 1 ) e. Z )
21 lgslem1 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) /\ -. P || A ) -> ( ( ( A ^ ( ( P - 1 ) / 2 ) ) + 1 ) mod P ) e. { 0 , 2 } )
22 elpri 
 |-  ( ( ( ( A ^ ( ( P - 1 ) / 2 ) ) + 1 ) mod P ) e. { 0 , 2 } -> ( ( ( ( A ^ ( ( P - 1 ) / 2 ) ) + 1 ) mod P ) = 0 \/ ( ( ( A ^ ( ( P - 1 ) / 2 ) ) + 1 ) mod P ) = 2 ) )
23 oveq1 
 |-  ( ( ( ( A ^ ( ( P - 1 ) / 2 ) ) + 1 ) mod P ) = 0 -> ( ( ( ( A ^ ( ( P - 1 ) / 2 ) ) + 1 ) mod P ) - 1 ) = ( 0 - 1 ) )
24 df-neg 
 |-  -u 1 = ( 0 - 1 )
25 17 simp1i 
 |-  -u 1 e. Z
26 24 25 eqeltrri 
 |-  ( 0 - 1 ) e. Z
27 23 26 eqeltrdi 
 |-  ( ( ( ( A ^ ( ( P - 1 ) / 2 ) ) + 1 ) mod P ) = 0 -> ( ( ( ( A ^ ( ( P - 1 ) / 2 ) ) + 1 ) mod P ) - 1 ) e. Z )
28 oveq1 
 |-  ( ( ( ( A ^ ( ( P - 1 ) / 2 ) ) + 1 ) mod P ) = 2 -> ( ( ( ( A ^ ( ( P - 1 ) / 2 ) ) + 1 ) mod P ) - 1 ) = ( 2 - 1 ) )
29 2m1e1 
 |-  ( 2 - 1 ) = 1
30 17 simp3i 
 |-  1 e. Z
31 29 30 eqeltri 
 |-  ( 2 - 1 ) e. Z
32 28 31 eqeltrdi 
 |-  ( ( ( ( A ^ ( ( P - 1 ) / 2 ) ) + 1 ) mod P ) = 2 -> ( ( ( ( A ^ ( ( P - 1 ) / 2 ) ) + 1 ) mod P ) - 1 ) e. Z )
33 27 32 jaoi 
 |-  ( ( ( ( ( A ^ ( ( P - 1 ) / 2 ) ) + 1 ) mod P ) = 0 \/ ( ( ( A ^ ( ( P - 1 ) / 2 ) ) + 1 ) mod P ) = 2 ) -> ( ( ( ( A ^ ( ( P - 1 ) / 2 ) ) + 1 ) mod P ) - 1 ) e. Z )
34 21 22 33 3syl 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) /\ -. P || A ) -> ( ( ( ( A ^ ( ( P - 1 ) / 2 ) ) + 1 ) mod P ) - 1 ) e. Z )
35 34 3expa 
 |-  ( ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) /\ -. P || A ) -> ( ( ( ( A ^ ( ( P - 1 ) / 2 ) ) + 1 ) mod P ) - 1 ) e. Z )
36 20 35 pm2.61dan 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) -> ( ( ( ( A ^ ( ( P - 1 ) / 2 ) ) + 1 ) mod P ) - 1 ) e. Z )