Metamath Proof Explorer

Theorem lgsqrlem5

Description: Lemma for lgsqr . (Contributed by Mario Carneiro, 15-Jun-2015)

Ref Expression
Assertion lgsqrlem5 
|- ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) /\ ( A /L P ) = 1 ) -> E. x e. ZZ P || ( ( x ^ 2 ) - A ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( Z/nZ ` P ) = ( Z/nZ ` P )
2 eqid 
 |-  ( Poly1 ` ( Z/nZ ` P ) ) = ( Poly1 ` ( Z/nZ ` P ) )
3 eqid 
 |-  ( Base ` ( Poly1 ` ( Z/nZ ` P ) ) ) = ( Base ` ( Poly1 ` ( Z/nZ ` P ) ) )
4 eqid 
 |-  ( deg1 ` ( Z/nZ ` P ) ) = ( deg1 ` ( Z/nZ ` P ) )
5 eqid 
 |-  ( eval1 ` ( Z/nZ ` P ) ) = ( eval1 ` ( Z/nZ ` P ) )
6 eqid 
 |-  ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` P ) ) ) ) = ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` P ) ) ) )
7 eqid 
 |-  ( var1 ` ( Z/nZ ` P ) ) = ( var1 ` ( Z/nZ ` P ) )
8 eqid 
 |-  ( -g ` ( Poly1 ` ( Z/nZ ` P ) ) ) = ( -g ` ( Poly1 ` ( Z/nZ ` P ) ) )
9 eqid 
 |-  ( 1r ` ( Poly1 ` ( Z/nZ ` P ) ) ) = ( 1r ` ( Poly1 ` ( Z/nZ ` P ) ) )
10 eqid 
 |-  ( ( ( ( P - 1 ) / 2 ) ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` P ) ) ) ) ( var1 ` ( Z/nZ ` P ) ) ) ( -g ` ( Poly1 ` ( Z/nZ ` P ) ) ) ( 1r ` ( Poly1 ` ( Z/nZ ` P ) ) ) ) = ( ( ( ( P - 1 ) / 2 ) ( .g ` ( mulGrp ` ( Poly1 ` ( Z/nZ ` P ) ) ) ) ( var1 ` ( Z/nZ ` P ) ) ) ( -g ` ( Poly1 ` ( Z/nZ ` P ) ) ) ( 1r ` ( Poly1 ` ( Z/nZ ` P ) ) ) )
11 eqid 
 |-  ( ZRHom ` ( Z/nZ ` P ) ) = ( ZRHom ` ( Z/nZ ` P ) )
12 simp2 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) /\ ( A /L P ) = 1 ) -> P e. ( Prime \ { 2 } ) )
13 eqid 
 |-  ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( ( ZRHom ` ( Z/nZ ` P ) ) ` ( y ^ 2 ) ) ) = ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( ( ZRHom ` ( Z/nZ ` P ) ) ` ( y ^ 2 ) ) )
14 simp1 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) /\ ( A /L P ) = 1 ) -> A e. ZZ )
15 simp3 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) /\ ( A /L P ) = 1 ) -> ( A /L P ) = 1 )
16 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 lgsqrlem4 
 |-  ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) /\ ( A /L P ) = 1 ) -> E. x e. ZZ P || ( ( x ^ 2 ) - A ) )