Metamath Proof Explorer

Theorem lgsqrlem4

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

Ref Expression
Hypotheses lgsqr.y 
|- Y = ( Z/nZ ` P )
lgsqr.s 
|- S = ( Poly1 ` Y )
lgsqr.b 
|- B = ( Base ` S )
lgsqr.d 
|- D = ( deg1 ` Y )
lgsqr.o 
|- O = ( eval1 ` Y )
lgsqr.e 
|- .^ = ( .g ` ( mulGrp ` S ) )
lgsqr.x 
|- X = ( var1 ` Y )
lgsqr.m 
|- .- = ( -g ` S )
lgsqr.u 
|- .1. = ( 1r ` S )
lgsqr.t 
|- T = ( ( ( ( P - 1 ) / 2 ) .^ X ) .- .1. )
lgsqr.l 
|- L = ( ZRHom ` Y )
lgsqr.1 
|- ( ph -> P e. ( Prime \ { 2 } ) )
lgsqr.g 
|- G = ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` ( y ^ 2 ) ) )
lgsqr.3 
|- ( ph -> A e. ZZ )
lgsqr.4 
|- ( ph -> ( A /L P ) = 1 )
Assertion lgsqrlem4 
|- ( ph -> E. x e. ZZ P || ( ( x ^ 2 ) - A ) )

Proof

Step Hyp Ref Expression
1 lgsqr.y 
 |-  Y = ( Z/nZ ` P )
2 lgsqr.s 
 |-  S = ( Poly1 ` Y )
3 lgsqr.b 
 |-  B = ( Base ` S )
4 lgsqr.d 
 |-  D = ( deg1 ` Y )
5 lgsqr.o 
 |-  O = ( eval1 ` Y )
6 lgsqr.e 
 |-  .^ = ( .g ` ( mulGrp ` S ) )
7 lgsqr.x 
 |-  X = ( var1 ` Y )
8 lgsqr.m 
 |-  .- = ( -g ` S )
9 lgsqr.u 
 |-  .1. = ( 1r ` S )
10 lgsqr.t 
 |-  T = ( ( ( ( P - 1 ) / 2 ) .^ X ) .- .1. )
11 lgsqr.l 
 |-  L = ( ZRHom ` Y )
12 lgsqr.1 
 |-  ( ph -> P e. ( Prime \ { 2 } ) )
13 lgsqr.g 
 |-  G = ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` ( y ^ 2 ) ) )
14 lgsqr.3 
 |-  ( ph -> A e. ZZ )
15 lgsqr.4 
 |-  ( ph -> ( A /L P ) = 1 )
16 1 2 3 4 5 6 7 8 9 10 11 12 13 lgsqrlem2 
 |-  ( ph -> G : ( 1 ... ( ( P - 1 ) / 2 ) ) -1-1-> ( `' ( O ` T ) " { ( 0g ` Y ) } ) )
17 fvex 
 |-  ( O ` T ) e. _V
18 17 cnvex 
 |-  `' ( O ` T ) e. _V
19 18 imaex 
 |-  ( `' ( O ` T ) " { ( 0g ` Y ) } ) e. _V
20 19 f1dom 
 |-  ( G : ( 1 ... ( ( P - 1 ) / 2 ) ) -1-1-> ( `' ( O ` T ) " { ( 0g ` Y ) } ) -> ( 1 ... ( ( P - 1 ) / 2 ) ) ~<_ ( `' ( O ` T ) " { ( 0g ` Y ) } ) )
21 16 20 syl 
 |-  ( ph -> ( 1 ... ( ( P - 1 ) / 2 ) ) ~<_ ( `' ( O ` T ) " { ( 0g ` Y ) } ) )
22 eqid 
 |-  ( 0g ` Y ) = ( 0g ` Y )
23 eqid 
 |-  ( 0g ` S ) = ( 0g ` S )
24 12 eldifad 
 |-  ( ph -> P e. Prime )
25 1 znfld 
 |-  ( P e. Prime -> Y e. Field )
26 24 25 syl 
 |-  ( ph -> Y e. Field )
27 fldidom 
 |-  ( Y e. Field -> Y e. IDomn )
28 26 27 syl 
 |-  ( ph -> Y e. IDomn )
29 isidom 
 |-  ( Y e. IDomn <-> ( Y e. CRing /\ Y e. Domn ) )
30 29 simplbi 
 |-  ( Y e. IDomn -> Y e. CRing )
31 28 30 syl 
 |-  ( ph -> Y e. CRing )
32 crngring 
 |-  ( Y e. CRing -> Y e. Ring )
33 31 32 syl 
 |-  ( ph -> Y e. Ring )
34 2 ply1ring 
 |-  ( Y e. Ring -> S e. Ring )
35 33 34 syl 
 |-  ( ph -> S e. Ring )
36 ringgrp 
 |-  ( S e. Ring -> S e. Grp )
37 35 36 syl 
 |-  ( ph -> S e. Grp )
38 eqid 
 |-  ( mulGrp ` S ) = ( mulGrp ` S )
39 38 ringmgp 
 |-  ( S e. Ring -> ( mulGrp ` S ) e. Mnd )
40 35 39 syl 
 |-  ( ph -> ( mulGrp ` S ) e. Mnd )
41 oddprm 
 |-  ( P e. ( Prime \ { 2 } ) -> ( ( P - 1 ) / 2 ) e. NN )
42 12 41 syl 
 |-  ( ph -> ( ( P - 1 ) / 2 ) e. NN )
43 42 nnnn0d 
 |-  ( ph -> ( ( P - 1 ) / 2 ) e. NN0 )
44 7 2 3 vr1cl 
 |-  ( Y e. Ring -> X e. B )
45 33 44 syl 
 |-  ( ph -> X e. B )
46 38 3 mgpbas 
 |-  B = ( Base ` ( mulGrp ` S ) )
47 46 6 mulgnn0cl 
 |-  ( ( ( mulGrp ` S ) e. Mnd /\ ( ( P - 1 ) / 2 ) e. NN0 /\ X e. B ) -> ( ( ( P - 1 ) / 2 ) .^ X ) e. B )
48 40 43 45 47 syl3anc 
 |-  ( ph -> ( ( ( P - 1 ) / 2 ) .^ X ) e. B )
49 3 9 ringidcl 
 |-  ( S e. Ring -> .1. e. B )
50 35 49 syl 
 |-  ( ph -> .1. e. B )
51 3 8 grpsubcl 
 |-  ( ( S e. Grp /\ ( ( ( P - 1 ) / 2 ) .^ X ) e. B /\ .1. e. B ) -> ( ( ( ( P - 1 ) / 2 ) .^ X ) .- .1. ) e. B )
52 37 48 50 51 syl3anc 
 |-  ( ph -> ( ( ( ( P - 1 ) / 2 ) .^ X ) .- .1. ) e. B )
53 10 52 eqeltrid 
 |-  ( ph -> T e. B )
54 10 fveq2i 
 |-  ( D ` T ) = ( D ` ( ( ( ( P - 1 ) / 2 ) .^ X ) .- .1. ) )
55 42 nngt0d 
 |-  ( ph -> 0 < ( ( P - 1 ) / 2 ) )
56 eqid 
 |-  ( algSc ` S ) = ( algSc ` S )
57 eqid 
 |-  ( 1r ` Y ) = ( 1r ` Y )
58 2 56 57 9 ply1scl1 
 |-  ( Y e. Ring -> ( ( algSc ` S ) ` ( 1r ` Y ) ) = .1. )
59 33 58 syl 
 |-  ( ph -> ( ( algSc ` S ) ` ( 1r ` Y ) ) = .1. )
60 59 fveq2d 
 |-  ( ph -> ( D ` ( ( algSc ` S ) ` ( 1r ` Y ) ) ) = ( D ` .1. ) )
61 eqid 
 |-  ( Base ` Y ) = ( Base ` Y )
62 61 57 ringidcl 
 |-  ( Y e. Ring -> ( 1r ` Y ) e. ( Base ` Y ) )
63 33 62 syl 
 |-  ( ph -> ( 1r ` Y ) e. ( Base ` Y ) )
64 domnnzr 
 |-  ( Y e. Domn -> Y e. NzRing )
65 29 64 simplbiim 
 |-  ( Y e. IDomn -> Y e. NzRing )
66 28 65 syl 
 |-  ( ph -> Y e. NzRing )
67 57 22 nzrnz 
 |-  ( Y e. NzRing -> ( 1r ` Y ) =/= ( 0g ` Y ) )
68 66 67 syl 
 |-  ( ph -> ( 1r ` Y ) =/= ( 0g ` Y ) )
69 4 2 61 56 22 deg1scl 
 |-  ( ( Y e. Ring /\ ( 1r ` Y ) e. ( Base ` Y ) /\ ( 1r ` Y ) =/= ( 0g ` Y ) ) -> ( D ` ( ( algSc ` S ) ` ( 1r ` Y ) ) ) = 0 )
70 33 63 68 69 syl3anc 
 |-  ( ph -> ( D ` ( ( algSc ` S ) ` ( 1r ` Y ) ) ) = 0 )
71 60 70 eqtr3d 
 |-  ( ph -> ( D ` .1. ) = 0 )
72 4 2 7 38 6 deg1pw 
 |-  ( ( Y e. NzRing /\ ( ( P - 1 ) / 2 ) e. NN0 ) -> ( D ` ( ( ( P - 1 ) / 2 ) .^ X ) ) = ( ( P - 1 ) / 2 ) )
73 66 43 72 syl2anc 
 |-  ( ph -> ( D ` ( ( ( P - 1 ) / 2 ) .^ X ) ) = ( ( P - 1 ) / 2 ) )
74 55 71 73 3brtr4d 
 |-  ( ph -> ( D ` .1. ) < ( D ` ( ( ( P - 1 ) / 2 ) .^ X ) ) )
75 2 4 33 3 8 48 50 74 deg1sub 
 |-  ( ph -> ( D ` ( ( ( ( P - 1 ) / 2 ) .^ X ) .- .1. ) ) = ( D ` ( ( ( P - 1 ) / 2 ) .^ X ) ) )
76 54 75 syl5eq 
 |-  ( ph -> ( D ` T ) = ( D ` ( ( ( P - 1 ) / 2 ) .^ X ) ) )
77 76 73 eqtrd 
 |-  ( ph -> ( D ` T ) = ( ( P - 1 ) / 2 ) )
78 77 43 eqeltrd 
 |-  ( ph -> ( D ` T ) e. NN0 )
79 4 2 23 3 deg1nn0clb 
 |-  ( ( Y e. Ring /\ T e. B ) -> ( T =/= ( 0g ` S ) <-> ( D ` T ) e. NN0 ) )
80 33 53 79 syl2anc 
 |-  ( ph -> ( T =/= ( 0g ` S ) <-> ( D ` T ) e. NN0 ) )
81 78 80 mpbird 
 |-  ( ph -> T =/= ( 0g ` S ) )
82 2 3 4 5 22 23 28 53 81 fta1g 
 |-  ( ph -> ( # ` ( `' ( O ` T ) " { ( 0g ` Y ) } ) ) <_ ( D ` T ) )
83 82 77 breqtrd 
 |-  ( ph -> ( # ` ( `' ( O ` T ) " { ( 0g ` Y ) } ) ) <_ ( ( P - 1 ) / 2 ) )
84 hashfz1 
 |-  ( ( ( P - 1 ) / 2 ) e. NN0 -> ( # ` ( 1 ... ( ( P - 1 ) / 2 ) ) ) = ( ( P - 1 ) / 2 ) )
85 43 84 syl 
 |-  ( ph -> ( # ` ( 1 ... ( ( P - 1 ) / 2 ) ) ) = ( ( P - 1 ) / 2 ) )
86 83 85 breqtrrd 
 |-  ( ph -> ( # ` ( `' ( O ` T ) " { ( 0g ` Y ) } ) ) <_ ( # ` ( 1 ... ( ( P - 1 ) / 2 ) ) ) )
87 hashbnd 
 |-  ( ( ( `' ( O ` T ) " { ( 0g ` Y ) } ) e. _V /\ ( ( P - 1 ) / 2 ) e. NN0 /\ ( # ` ( `' ( O ` T ) " { ( 0g ` Y ) } ) ) <_ ( ( P - 1 ) / 2 ) ) -> ( `' ( O ` T ) " { ( 0g ` Y ) } ) e. Fin )
88 19 43 83 87 mp3an2i 
 |-  ( ph -> ( `' ( O ` T ) " { ( 0g ` Y ) } ) e. Fin )
89 fzfid 
 |-  ( ph -> ( 1 ... ( ( P - 1 ) / 2 ) ) e. Fin )
90 hashdom 
 |-  ( ( ( `' ( O ` T ) " { ( 0g ` Y ) } ) e. Fin /\ ( 1 ... ( ( P - 1 ) / 2 ) ) e. Fin ) -> ( ( # ` ( `' ( O ` T ) " { ( 0g ` Y ) } ) ) <_ ( # ` ( 1 ... ( ( P - 1 ) / 2 ) ) ) <-> ( `' ( O ` T ) " { ( 0g ` Y ) } ) ~<_ ( 1 ... ( ( P - 1 ) / 2 ) ) ) )
91 88 89 90 syl2anc 
 |-  ( ph -> ( ( # ` ( `' ( O ` T ) " { ( 0g ` Y ) } ) ) <_ ( # ` ( 1 ... ( ( P - 1 ) / 2 ) ) ) <-> ( `' ( O ` T ) " { ( 0g ` Y ) } ) ~<_ ( 1 ... ( ( P - 1 ) / 2 ) ) ) )
92 86 91 mpbid 
 |-  ( ph -> ( `' ( O ` T ) " { ( 0g ` Y ) } ) ~<_ ( 1 ... ( ( P - 1 ) / 2 ) ) )
93 sbth 
 |-  ( ( ( 1 ... ( ( P - 1 ) / 2 ) ) ~<_ ( `' ( O ` T ) " { ( 0g ` Y ) } ) /\ ( `' ( O ` T ) " { ( 0g ` Y ) } ) ~<_ ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( 1 ... ( ( P - 1 ) / 2 ) ) ~~ ( `' ( O ` T ) " { ( 0g ` Y ) } ) )
94 21 92 93 syl2anc 
 |-  ( ph -> ( 1 ... ( ( P - 1 ) / 2 ) ) ~~ ( `' ( O ` T ) " { ( 0g ` Y ) } ) )
95 f1finf1o 
 |-  ( ( ( 1 ... ( ( P - 1 ) / 2 ) ) ~~ ( `' ( O ` T ) " { ( 0g ` Y ) } ) /\ ( `' ( O ` T ) " { ( 0g ` Y ) } ) e. Fin ) -> ( G : ( 1 ... ( ( P - 1 ) / 2 ) ) -1-1-> ( `' ( O ` T ) " { ( 0g ` Y ) } ) <-> G : ( 1 ... ( ( P - 1 ) / 2 ) ) -1-1-onto-> ( `' ( O ` T ) " { ( 0g ` Y ) } ) ) )
96 94 88 95 syl2anc 
 |-  ( ph -> ( G : ( 1 ... ( ( P - 1 ) / 2 ) ) -1-1-> ( `' ( O ` T ) " { ( 0g ` Y ) } ) <-> G : ( 1 ... ( ( P - 1 ) / 2 ) ) -1-1-onto-> ( `' ( O ` T ) " { ( 0g ` Y ) } ) ) )
97 16 96 mpbid 
 |-  ( ph -> G : ( 1 ... ( ( P - 1 ) / 2 ) ) -1-1-onto-> ( `' ( O ` T ) " { ( 0g ` Y ) } ) )
98 f1ocnv 
 |-  ( G : ( 1 ... ( ( P - 1 ) / 2 ) ) -1-1-onto-> ( `' ( O ` T ) " { ( 0g ` Y ) } ) -> `' G : ( `' ( O ` T ) " { ( 0g ` Y ) } ) -1-1-onto-> ( 1 ... ( ( P - 1 ) / 2 ) ) )
99 f1of 
 |-  ( `' G : ( `' ( O ` T ) " { ( 0g ` Y ) } ) -1-1-onto-> ( 1 ... ( ( P - 1 ) / 2 ) ) -> `' G : ( `' ( O ` T ) " { ( 0g ` Y ) } ) --> ( 1 ... ( ( P - 1 ) / 2 ) ) )
100 97 98 99 3syl 
 |-  ( ph -> `' G : ( `' ( O ` T ) " { ( 0g ` Y ) } ) --> ( 1 ... ( ( P - 1 ) / 2 ) ) )
101 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 lgsqrlem3 
 |-  ( ph -> ( L ` A ) e. ( `' ( O ` T ) " { ( 0g ` Y ) } ) )
102 100 101 ffvelrnd 
 |-  ( ph -> ( `' G ` ( L ` A ) ) e. ( 1 ... ( ( P - 1 ) / 2 ) ) )
103 elfzelz 
 |-  ( ( `' G ` ( L ` A ) ) e. ( 1 ... ( ( P - 1 ) / 2 ) ) -> ( `' G ` ( L ` A ) ) e. ZZ )
104 102 103 syl 
 |-  ( ph -> ( `' G ` ( L ` A ) ) e. ZZ )
105 fvoveq1 
 |-  ( x = ( `' G ` ( L ` A ) ) -> ( L ` ( x ^ 2 ) ) = ( L ` ( ( `' G ` ( L ` A ) ) ^ 2 ) ) )
106 fvoveq1 
 |-  ( y = x -> ( L ` ( y ^ 2 ) ) = ( L ` ( x ^ 2 ) ) )
107 106 cbvmptv 
 |-  ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` ( y ^ 2 ) ) ) = ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` ( x ^ 2 ) ) )
108 13 107 eqtri 
 |-  G = ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) |-> ( L ` ( x ^ 2 ) ) )
109 fvex 
 |-  ( L ` ( ( `' G ` ( L ` A ) ) ^ 2 ) ) e. _V
110 105 108 109 fvmpt 
 |-  ( ( `' G ` ( L ` A ) ) e. ( 1 ... ( ( P - 1 ) / 2 ) ) -> ( G ` ( `' G ` ( L ` A ) ) ) = ( L ` ( ( `' G ` ( L ` A ) ) ^ 2 ) ) )
111 102 110 syl 
 |-  ( ph -> ( G ` ( `' G ` ( L ` A ) ) ) = ( L ` ( ( `' G ` ( L ` A ) ) ^ 2 ) ) )
112 f1ocnvfv2 
 |-  ( ( G : ( 1 ... ( ( P - 1 ) / 2 ) ) -1-1-onto-> ( `' ( O ` T ) " { ( 0g ` Y ) } ) /\ ( L ` A ) e. ( `' ( O ` T ) " { ( 0g ` Y ) } ) ) -> ( G ` ( `' G ` ( L ` A ) ) ) = ( L ` A ) )
113 97 101 112 syl2anc 
 |-  ( ph -> ( G ` ( `' G ` ( L ` A ) ) ) = ( L ` A ) )
114 111 113 eqtr3d 
 |-  ( ph -> ( L ` ( ( `' G ` ( L ` A ) ) ^ 2 ) ) = ( L ` A ) )
115 prmnn 
 |-  ( P e. Prime -> P e. NN )
116 24 115 syl 
 |-  ( ph -> P e. NN )
117 116 nnnn0d 
 |-  ( ph -> P e. NN0 )
118 zsqcl 
 |-  ( ( `' G ` ( L ` A ) ) e. ZZ -> ( ( `' G ` ( L ` A ) ) ^ 2 ) e. ZZ )
119 104 118 syl 
 |-  ( ph -> ( ( `' G ` ( L ` A ) ) ^ 2 ) e. ZZ )
120 1 11 zndvds 
 |-  ( ( P e. NN0 /\ ( ( `' G ` ( L ` A ) ) ^ 2 ) e. ZZ /\ A e. ZZ ) -> ( ( L ` ( ( `' G ` ( L ` A ) ) ^ 2 ) ) = ( L ` A ) <-> P || ( ( ( `' G ` ( L ` A ) ) ^ 2 ) - A ) ) )
121 117 119 14 120 syl3anc 
 |-  ( ph -> ( ( L ` ( ( `' G ` ( L ` A ) ) ^ 2 ) ) = ( L ` A ) <-> P || ( ( ( `' G ` ( L ` A ) ) ^ 2 ) - A ) ) )
122 114 121 mpbid 
 |-  ( ph -> P || ( ( ( `' G ` ( L ` A ) ) ^ 2 ) - A ) )
123 oveq1 
 |-  ( x = ( `' G ` ( L ` A ) ) -> ( x ^ 2 ) = ( ( `' G ` ( L ` A ) ) ^ 2 ) )
124 123 oveq1d 
 |-  ( x = ( `' G ` ( L ` A ) ) -> ( ( x ^ 2 ) - A ) = ( ( ( `' G ` ( L ` A ) ) ^ 2 ) - A ) )
125 124 breq2d 
 |-  ( x = ( `' G ` ( L ` A ) ) -> ( P || ( ( x ^ 2 ) - A ) <-> P || ( ( ( `' G ` ( L ` A ) ) ^ 2 ) - A ) ) )
126 125 rspcev 
 |-  ( ( ( `' G ` ( L ` A ) ) e. ZZ /\ P || ( ( ( `' G ` ( L ` A ) ) ^ 2 ) - A ) ) -> E. x e. ZZ P || ( ( x ^ 2 ) - A ) )
127 104 122 126 syl2anc 
 |-  ( ph -> E. x e. ZZ P || ( ( x ^ 2 ) - A ) )