Metamath Proof Explorer

Theorem lgsqrlem2

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 ) ) )
Assertion lgsqrlem2 
|- ( ph -> G : ( 1 ... ( ( P - 1 ) / 2 ) ) -1-1-> ( `' ( O ` T ) " { ( 0g ` Y ) } ) )

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 12 eldifad 
 |-  ( ph -> P e. Prime )
15 1 znfld 
 |-  ( P e. Prime -> Y e. Field )
16 14 15 syl 
 |-  ( ph -> Y e. Field )
17 fldidom 
 |-  ( Y e. Field -> Y e. IDomn )
18 16 17 syl 
 |-  ( ph -> Y e. IDomn )
19 isidom 
 |-  ( Y e. IDomn <-> ( Y e. CRing /\ Y e. Domn ) )
20 19 simplbi 
 |-  ( Y e. IDomn -> Y e. CRing )
21 18 20 syl 
 |-  ( ph -> Y e. CRing )
22 crngring 
 |-  ( Y e. CRing -> Y e. Ring )
23 21 22 syl 
 |-  ( ph -> Y e. Ring )
24 11 zrhrhm 
 |-  ( Y e. Ring -> L e. ( ZZring RingHom Y ) )
25 23 24 syl 
 |-  ( ph -> L e. ( ZZring RingHom Y ) )
26 zringbas 
 |-  ZZ = ( Base ` ZZring )
27 eqid 
 |-  ( Base ` Y ) = ( Base ` Y )
28 26 27 rhmf 
 |-  ( L e. ( ZZring RingHom Y ) -> L : ZZ --> ( Base ` Y ) )
29 25 28 syl 
 |-  ( ph -> L : ZZ --> ( Base ` Y ) )
30 29 adantr 
 |-  ( ( ph /\ y e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> L : ZZ --> ( Base ` Y ) )
31 elfzelz 
 |-  ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) -> y e. ZZ )
32 31 adantl 
 |-  ( ( ph /\ y e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> y e. ZZ )
33 zsqcl 
 |-  ( y e. ZZ -> ( y ^ 2 ) e. ZZ )
34 32 33 syl 
 |-  ( ( ph /\ y e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( y ^ 2 ) e. ZZ )
35 30 34 ffvelrnd 
 |-  ( ( ph /\ y e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( L ` ( y ^ 2 ) ) e. ( Base ` Y ) )
36 12 adantr 
 |-  ( ( ph /\ y e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> P e. ( Prime \ { 2 } ) )
37 elfznn 
 |-  ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) -> y e. NN )
38 37 adantl 
 |-  ( ( ph /\ y e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> y e. NN )
39 38 nncnd 
 |-  ( ( ph /\ y e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> y e. CC )
40 oddprm 
 |-  ( P e. ( Prime \ { 2 } ) -> ( ( P - 1 ) / 2 ) e. NN )
41 12 40 syl 
 |-  ( ph -> ( ( P - 1 ) / 2 ) e. NN )
42 41 nnnn0d 
 |-  ( ph -> ( ( P - 1 ) / 2 ) e. NN0 )
43 42 adantr 
 |-  ( ( ph /\ y e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( ( P - 1 ) / 2 ) e. NN0 )
44 2nn0 
 |-  2 e. NN0
45 44 a1i 
 |-  ( ( ph /\ y e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> 2 e. NN0 )
46 39 43 45 expmuld 
 |-  ( ( ph /\ y e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( y ^ ( 2 x. ( ( P - 1 ) / 2 ) ) ) = ( ( y ^ 2 ) ^ ( ( P - 1 ) / 2 ) ) )
47 prmnn 
 |-  ( P e. Prime -> P e. NN )
48 14 47 syl 
 |-  ( ph -> P e. NN )
49 48 nnred 
 |-  ( ph -> P e. RR )
50 peano2rem 
 |-  ( P e. RR -> ( P - 1 ) e. RR )
51 49 50 syl 
 |-  ( ph -> ( P - 1 ) e. RR )
52 51 recnd 
 |-  ( ph -> ( P - 1 ) e. CC )
53 2cnd 
 |-  ( ph -> 2 e. CC )
54 2ne0 
 |-  2 =/= 0
55 54 a1i 
 |-  ( ph -> 2 =/= 0 )
56 52 53 55 divcan2d 
 |-  ( ph -> ( 2 x. ( ( P - 1 ) / 2 ) ) = ( P - 1 ) )
57 phiprm 
 |-  ( P e. Prime -> ( phi ` P ) = ( P - 1 ) )
58 14 57 syl 
 |-  ( ph -> ( phi ` P ) = ( P - 1 ) )
59 56 58 eqtr4d 
 |-  ( ph -> ( 2 x. ( ( P - 1 ) / 2 ) ) = ( phi ` P ) )
60 59 adantr 
 |-  ( ( ph /\ y e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( 2 x. ( ( P - 1 ) / 2 ) ) = ( phi ` P ) )
61 60 oveq2d 
 |-  ( ( ph /\ y e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( y ^ ( 2 x. ( ( P - 1 ) / 2 ) ) ) = ( y ^ ( phi ` P ) ) )
62 46 61 eqtr3d 
 |-  ( ( ph /\ y e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( ( y ^ 2 ) ^ ( ( P - 1 ) / 2 ) ) = ( y ^ ( phi ` P ) ) )
63 62 oveq1d 
 |-  ( ( ph /\ y e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( ( ( y ^ 2 ) ^ ( ( P - 1 ) / 2 ) ) mod P ) = ( ( y ^ ( phi ` P ) ) mod P ) )
64 14 adantr 
 |-  ( ( ph /\ y e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> P e. Prime )
65 64 47 syl 
 |-  ( ( ph /\ y e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> P e. NN )
66 48 nnzd 
 |-  ( ph -> P e. ZZ )
67 66 adantr 
 |-  ( ( ph /\ y e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> P e. ZZ )
68 32 67 gcdcomd 
 |-  ( ( ph /\ y e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( y gcd P ) = ( P gcd y ) )
69 38 nnred 
 |-  ( ( ph /\ y e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> y e. RR )
70 51 rehalfcld 
 |-  ( ph -> ( ( P - 1 ) / 2 ) e. RR )
71 70 adantr 
 |-  ( ( ph /\ y e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( ( P - 1 ) / 2 ) e. RR )
72 49 adantr 
 |-  ( ( ph /\ y e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> P e. RR )
73 elfzle2 
 |-  ( y e. ( 1 ... ( ( P - 1 ) / 2 ) ) -> y <_ ( ( P - 1 ) / 2 ) )
74 73 adantl 
 |-  ( ( ph /\ y e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> y <_ ( ( P - 1 ) / 2 ) )
75 prmuz2 
 |-  ( P e. Prime -> P e. ( ZZ>= ` 2 ) )
76 14 75 syl 
 |-  ( ph -> P e. ( ZZ>= ` 2 ) )
77 uz2m1nn 
 |-  ( P e. ( ZZ>= ` 2 ) -> ( P - 1 ) e. NN )
78 76 77 syl 
 |-  ( ph -> ( P - 1 ) e. NN )
79 78 nnrpd 
 |-  ( ph -> ( P - 1 ) e. RR+ )
80 rphalflt 
 |-  ( ( P - 1 ) e. RR+ -> ( ( P - 1 ) / 2 ) < ( P - 1 ) )
81 79 80 syl 
 |-  ( ph -> ( ( P - 1 ) / 2 ) < ( P - 1 ) )
82 49 ltm1d 
 |-  ( ph -> ( P - 1 ) < P )
83 70 51 49 81 82 lttrd 
 |-  ( ph -> ( ( P - 1 ) / 2 ) < P )
84 83 adantr 
 |-  ( ( ph /\ y e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( ( P - 1 ) / 2 ) < P )
85 69 71 72 74 84 lelttrd 
 |-  ( ( ph /\ y e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> y < P )
86 69 72 ltnled 
 |-  ( ( ph /\ y e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( y < P <-> -. P <_ y ) )
87 85 86 mpbid 
 |-  ( ( ph /\ y e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> -. P <_ y )
88 dvdsle 
 |-  ( ( P e. ZZ /\ y e. NN ) -> ( P || y -> P <_ y ) )
89 67 38 88 syl2anc 
 |-  ( ( ph /\ y e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( P || y -> P <_ y ) )
90 87 89 mtod 
 |-  ( ( ph /\ y e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> -. P || y )
91 coprm 
 |-  ( ( P e. Prime /\ y e. ZZ ) -> ( -. P || y <-> ( P gcd y ) = 1 ) )
92 64 32 91 syl2anc 
 |-  ( ( ph /\ y e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( -. P || y <-> ( P gcd y ) = 1 ) )
93 90 92 mpbid 
 |-  ( ( ph /\ y e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( P gcd y ) = 1 )
94 68 93 eqtrd 
 |-  ( ( ph /\ y e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( y gcd P ) = 1 )
95 eulerth 
 |-  ( ( P e. NN /\ y e. ZZ /\ ( y gcd P ) = 1 ) -> ( ( y ^ ( phi ` P ) ) mod P ) = ( 1 mod P ) )
96 65 32 94 95 syl3anc 
 |-  ( ( ph /\ y e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( ( y ^ ( phi ` P ) ) mod P ) = ( 1 mod P ) )
97 63 96 eqtrd 
 |-  ( ( ph /\ y e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( ( ( y ^ 2 ) ^ ( ( P - 1 ) / 2 ) ) mod P ) = ( 1 mod P ) )
98 1 2 3 4 5 6 7 8 9 10 11 36 34 97 lgsqrlem1 
 |-  ( ( ph /\ y e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( ( O ` T ) ` ( L ` ( y ^ 2 ) ) ) = ( 0g ` Y ) )
99 eqid 
 |-  ( Y ^s ( Base ` Y ) ) = ( Y ^s ( Base ` Y ) )
100 eqid 
 |-  ( Base ` ( Y ^s ( Base ` Y ) ) ) = ( Base ` ( Y ^s ( Base ` Y ) ) )
101 fvexd 
 |-  ( ph -> ( Base ` Y ) e. _V )
102 5 2 99 27 evl1rhm 
 |-  ( Y e. CRing -> O e. ( S RingHom ( Y ^s ( Base ` Y ) ) ) )
103 21 102 syl 
 |-  ( ph -> O e. ( S RingHom ( Y ^s ( Base ` Y ) ) ) )
104 3 100 rhmf 
 |-  ( O e. ( S RingHom ( Y ^s ( Base ` Y ) ) ) -> O : B --> ( Base ` ( Y ^s ( Base ` Y ) ) ) )
105 103 104 syl 
 |-  ( ph -> O : B --> ( Base ` ( Y ^s ( Base ` Y ) ) ) )
106 2 ply1ring 
 |-  ( Y e. Ring -> S e. Ring )
107 23 106 syl 
 |-  ( ph -> S e. Ring )
108 ringgrp 
 |-  ( S e. Ring -> S e. Grp )
109 107 108 syl 
 |-  ( ph -> S e. Grp )
110 eqid 
 |-  ( mulGrp ` S ) = ( mulGrp ` S )
111 110 ringmgp 
 |-  ( S e. Ring -> ( mulGrp ` S ) e. Mnd )
112 107 111 syl 
 |-  ( ph -> ( mulGrp ` S ) e. Mnd )
113 7 2 3 vr1cl 
 |-  ( Y e. Ring -> X e. B )
114 23 113 syl 
 |-  ( ph -> X e. B )
115 110 3 mgpbas 
 |-  B = ( Base ` ( mulGrp ` S ) )
116 115 6 mulgnn0cl 
 |-  ( ( ( mulGrp ` S ) e. Mnd /\ ( ( P - 1 ) / 2 ) e. NN0 /\ X e. B ) -> ( ( ( P - 1 ) / 2 ) .^ X ) e. B )
117 112 42 114 116 syl3anc 
 |-  ( ph -> ( ( ( P - 1 ) / 2 ) .^ X ) e. B )
118 3 9 ringidcl 
 |-  ( S e. Ring -> .1. e. B )
119 107 118 syl 
 |-  ( ph -> .1. e. B )
120 3 8 grpsubcl 
 |-  ( ( S e. Grp /\ ( ( ( P - 1 ) / 2 ) .^ X ) e. B /\ .1. e. B ) -> ( ( ( ( P - 1 ) / 2 ) .^ X ) .- .1. ) e. B )
121 109 117 119 120 syl3anc 
 |-  ( ph -> ( ( ( ( P - 1 ) / 2 ) .^ X ) .- .1. ) e. B )
122 10 121 eqeltrid 
 |-  ( ph -> T e. B )
123 105 122 ffvelrnd 
 |-  ( ph -> ( O ` T ) e. ( Base ` ( Y ^s ( Base ` Y ) ) ) )
124 99 27 100 16 101 123 pwselbas 
 |-  ( ph -> ( O ` T ) : ( Base ` Y ) --> ( Base ` Y ) )
125 124 ffnd 
 |-  ( ph -> ( O ` T ) Fn ( Base ` Y ) )
126 125 adantr 
 |-  ( ( ph /\ y e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( O ` T ) Fn ( Base ` Y ) )
127 fniniseg 
 |-  ( ( O ` T ) Fn ( Base ` Y ) -> ( ( L ` ( y ^ 2 ) ) e. ( `' ( O ` T ) " { ( 0g ` Y ) } ) <-> ( ( L ` ( y ^ 2 ) ) e. ( Base ` Y ) /\ ( ( O ` T ) ` ( L ` ( y ^ 2 ) ) ) = ( 0g ` Y ) ) ) )
128 126 127 syl 
 |-  ( ( ph /\ y e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( ( L ` ( y ^ 2 ) ) e. ( `' ( O ` T ) " { ( 0g ` Y ) } ) <-> ( ( L ` ( y ^ 2 ) ) e. ( Base ` Y ) /\ ( ( O ` T ) ` ( L ` ( y ^ 2 ) ) ) = ( 0g ` Y ) ) ) )
129 35 98 128 mpbir2and 
 |-  ( ( ph /\ y e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( L ` ( y ^ 2 ) ) e. ( `' ( O ` T ) " { ( 0g ` Y ) } ) )
130 129 13 fmptd 
 |-  ( ph -> G : ( 1 ... ( ( P - 1 ) / 2 ) ) --> ( `' ( O ` T ) " { ( 0g ` Y ) } ) )
131 fvoveq1 
 |-  ( y = x -> ( L ` ( y ^ 2 ) ) = ( L ` ( x ^ 2 ) ) )
132 fvex 
 |-  ( L ` ( x ^ 2 ) ) e. _V
133 131 13 132 fvmpt 
 |-  ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) -> ( G ` x ) = ( L ` ( x ^ 2 ) ) )
134 133 ad2antrl 
 |-  ( ( ph /\ ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ z e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( G ` x ) = ( L ` ( x ^ 2 ) ) )
135 fvoveq1 
 |-  ( y = z -> ( L ` ( y ^ 2 ) ) = ( L ` ( z ^ 2 ) ) )
136 fvex 
 |-  ( L ` ( z ^ 2 ) ) e. _V
137 135 13 136 fvmpt 
 |-  ( z e. ( 1 ... ( ( P - 1 ) / 2 ) ) -> ( G ` z ) = ( L ` ( z ^ 2 ) ) )
138 137 ad2antll 
 |-  ( ( ph /\ ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ z e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( G ` z ) = ( L ` ( z ^ 2 ) ) )
139 134 138 eqeq12d 
 |-  ( ( ph /\ ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ z e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( G ` x ) = ( G ` z ) <-> ( L ` ( x ^ 2 ) ) = ( L ` ( z ^ 2 ) ) ) )
140 48 nnnn0d 
 |-  ( ph -> P e. NN0 )
141 140 adantr 
 |-  ( ( ph /\ ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ z e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> P e. NN0 )
142 elfzelz 
 |-  ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) -> x e. ZZ )
143 142 ad2antrl 
 |-  ( ( ph /\ ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ z e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> x e. ZZ )
144 zsqcl 
 |-  ( x e. ZZ -> ( x ^ 2 ) e. ZZ )
145 143 144 syl 
 |-  ( ( ph /\ ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ z e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( x ^ 2 ) e. ZZ )
146 elfzelz 
 |-  ( z e. ( 1 ... ( ( P - 1 ) / 2 ) ) -> z e. ZZ )
147 146 ad2antll 
 |-  ( ( ph /\ ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ z e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> z e. ZZ )
148 zsqcl 
 |-  ( z e. ZZ -> ( z ^ 2 ) e. ZZ )
149 147 148 syl 
 |-  ( ( ph /\ ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ z e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( z ^ 2 ) e. ZZ )
150 1 11 zndvds 
 |-  ( ( P e. NN0 /\ ( x ^ 2 ) e. ZZ /\ ( z ^ 2 ) e. ZZ ) -> ( ( L ` ( x ^ 2 ) ) = ( L ` ( z ^ 2 ) ) <-> P || ( ( x ^ 2 ) - ( z ^ 2 ) ) ) )
151 141 145 149 150 syl3anc 
 |-  ( ( ph /\ ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ z e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( L ` ( x ^ 2 ) ) = ( L ` ( z ^ 2 ) ) <-> P || ( ( x ^ 2 ) - ( z ^ 2 ) ) ) )
152 elfznn 
 |-  ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) -> x e. NN )
153 152 ad2antrl 
 |-  ( ( ph /\ ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ z e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> x e. NN )
154 153 nncnd 
 |-  ( ( ph /\ ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ z e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> x e. CC )
155 elfznn 
 |-  ( z e. ( 1 ... ( ( P - 1 ) / 2 ) ) -> z e. NN )
156 155 ad2antll 
 |-  ( ( ph /\ ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ z e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> z e. NN )
157 156 nncnd 
 |-  ( ( ph /\ ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ z e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> z e. CC )
158 subsq 
 |-  ( ( x e. CC /\ z e. CC ) -> ( ( x ^ 2 ) - ( z ^ 2 ) ) = ( ( x + z ) x. ( x - z ) ) )
159 154 157 158 syl2anc 
 |-  ( ( ph /\ ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ z e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( x ^ 2 ) - ( z ^ 2 ) ) = ( ( x + z ) x. ( x - z ) ) )
160 159 breq2d 
 |-  ( ( ph /\ ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ z e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( P || ( ( x ^ 2 ) - ( z ^ 2 ) ) <-> P || ( ( x + z ) x. ( x - z ) ) ) )
161 139 151 160 3bitrd 
 |-  ( ( ph /\ ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ z e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( G ` x ) = ( G ` z ) <-> P || ( ( x + z ) x. ( x - z ) ) ) )
162 14 adantr 
 |-  ( ( ph /\ ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ z e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> P e. Prime )
163 143 147 zaddcld 
 |-  ( ( ph /\ ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ z e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( x + z ) e. ZZ )
164 143 147 zsubcld 
 |-  ( ( ph /\ ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ z e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( x - z ) e. ZZ )
165 euclemma 
 |-  ( ( P e. Prime /\ ( x + z ) e. ZZ /\ ( x - z ) e. ZZ ) -> ( P || ( ( x + z ) x. ( x - z ) ) <-> ( P || ( x + z ) \/ P || ( x - z ) ) ) )
166 162 163 164 165 syl3anc 
 |-  ( ( ph /\ ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ z e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( P || ( ( x + z ) x. ( x - z ) ) <-> ( P || ( x + z ) \/ P || ( x - z ) ) ) )
167 162 47 syl 
 |-  ( ( ph /\ ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ z e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> P e. NN )
168 167 nnzd 
 |-  ( ( ph /\ ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ z e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> P e. ZZ )
169 153 156 nnaddcld 
 |-  ( ( ph /\ ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ z e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( x + z ) e. NN )
170 dvdsle 
 |-  ( ( P e. ZZ /\ ( x + z ) e. NN ) -> ( P || ( x + z ) -> P <_ ( x + z ) ) )
171 168 169 170 syl2anc 
 |-  ( ( ph /\ ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ z e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( P || ( x + z ) -> P <_ ( x + z ) ) )
172 169 nnred 
 |-  ( ( ph /\ ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ z e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( x + z ) e. RR )
173 167 nnred 
 |-  ( ( ph /\ ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ z e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> P e. RR )
174 173 50 syl 
 |-  ( ( ph /\ ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ z e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( P - 1 ) e. RR )
175 153 nnred 
 |-  ( ( ph /\ ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ z e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> x e. RR )
176 156 nnred 
 |-  ( ( ph /\ ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ z e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> z e. RR )
177 70 adantr 
 |-  ( ( ph /\ ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ z e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( P - 1 ) / 2 ) e. RR )
178 elfzle2 
 |-  ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) -> x <_ ( ( P - 1 ) / 2 ) )
179 178 ad2antrl 
 |-  ( ( ph /\ ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ z e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> x <_ ( ( P - 1 ) / 2 ) )
180 elfzle2 
 |-  ( z e. ( 1 ... ( ( P - 1 ) / 2 ) ) -> z <_ ( ( P - 1 ) / 2 ) )
181 180 ad2antll 
 |-  ( ( ph /\ ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ z e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> z <_ ( ( P - 1 ) / 2 ) )
182 175 176 177 177 179 181 le2addd 
 |-  ( ( ph /\ ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ z e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( x + z ) <_ ( ( ( P - 1 ) / 2 ) + ( ( P - 1 ) / 2 ) ) )
183 52 adantr 
 |-  ( ( ph /\ ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ z e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( P - 1 ) e. CC )
184 183 2halvesd 
 |-  ( ( ph /\ ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ z e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( ( P - 1 ) / 2 ) + ( ( P - 1 ) / 2 ) ) = ( P - 1 ) )
185 182 184 breqtrd 
 |-  ( ( ph /\ ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ z e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( x + z ) <_ ( P - 1 ) )
186 173 ltm1d 
 |-  ( ( ph /\ ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ z e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( P - 1 ) < P )
187 172 174 173 185 186 lelttrd 
 |-  ( ( ph /\ ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ z e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( x + z ) < P )
188 172 173 ltnled 
 |-  ( ( ph /\ ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ z e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( x + z ) < P <-> -. P <_ ( x + z ) ) )
189 187 188 mpbid 
 |-  ( ( ph /\ ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ z e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> -. P <_ ( x + z ) )
190 189 pm2.21d 
 |-  ( ( ph /\ ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ z e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( P <_ ( x + z ) -> x = z ) )
191 171 190 syld 
 |-  ( ( ph /\ ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ z e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( P || ( x + z ) -> x = z ) )
192 moddvds 
 |-  ( ( P e. NN /\ x e. ZZ /\ z e. ZZ ) -> ( ( x mod P ) = ( z mod P ) <-> P || ( x - z ) ) )
193 167 143 147 192 syl3anc 
 |-  ( ( ph /\ ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ z e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( x mod P ) = ( z mod P ) <-> P || ( x - z ) ) )
194 167 nnrpd 
 |-  ( ( ph /\ ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ z e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> P e. RR+ )
195 153 nnnn0d 
 |-  ( ( ph /\ ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ z e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> x e. NN0 )
196 195 nn0ge0d 
 |-  ( ( ph /\ ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ z e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> 0 <_ x )
197 83 adantr 
 |-  ( ( ph /\ ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ z e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( P - 1 ) / 2 ) < P )
198 175 177 173 179 197 lelttrd 
 |-  ( ( ph /\ ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ z e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> x < P )
199 modid 
 |-  ( ( ( x e. RR /\ P e. RR+ ) /\ ( 0 <_ x /\ x < P ) ) -> ( x mod P ) = x )
200 175 194 196 198 199 syl22anc 
 |-  ( ( ph /\ ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ z e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( x mod P ) = x )
201 156 nnnn0d 
 |-  ( ( ph /\ ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ z e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> z e. NN0 )
202 201 nn0ge0d 
 |-  ( ( ph /\ ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ z e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> 0 <_ z )
203 176 177 173 181 197 lelttrd 
 |-  ( ( ph /\ ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ z e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> z < P )
204 modid 
 |-  ( ( ( z e. RR /\ P e. RR+ ) /\ ( 0 <_ z /\ z < P ) ) -> ( z mod P ) = z )
205 176 194 202 203 204 syl22anc 
 |-  ( ( ph /\ ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ z e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( z mod P ) = z )
206 200 205 eqeq12d 
 |-  ( ( ph /\ ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ z e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( x mod P ) = ( z mod P ) <-> x = z ) )
207 193 206 bitr3d 
 |-  ( ( ph /\ ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ z e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( P || ( x - z ) <-> x = z ) )
208 207 biimpd 
 |-  ( ( ph /\ ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ z e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( P || ( x - z ) -> x = z ) )
209 191 208 jaod 
 |-  ( ( ph /\ ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ z e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( P || ( x + z ) \/ P || ( x - z ) ) -> x = z ) )
210 166 209 sylbid 
 |-  ( ( ph /\ ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ z e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( P || ( ( x + z ) x. ( x - z ) ) -> x = z ) )
211 161 210 sylbid 
 |-  ( ( ph /\ ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ z e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( G ` x ) = ( G ` z ) -> x = z ) )
212 211 ralrimivva 
 |-  ( ph -> A. x e. ( 1 ... ( ( P - 1 ) / 2 ) ) A. z e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( ( G ` x ) = ( G ` z ) -> x = z ) )
213 dff13 
 |-  ( G : ( 1 ... ( ( P - 1 ) / 2 ) ) -1-1-> ( `' ( O ` T ) " { ( 0g ` Y ) } ) <-> ( G : ( 1 ... ( ( P - 1 ) / 2 ) ) --> ( `' ( O ` T ) " { ( 0g ` Y ) } ) /\ A. x e. ( 1 ... ( ( P - 1 ) / 2 ) ) A. z e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( ( G ` x ) = ( G ` z ) -> x = z ) ) )
214 130 212 213 sylanbrc 
 |-  ( ph -> G : ( 1 ... ( ( P - 1 ) / 2 ) ) -1-1-> ( `' ( O ` T ) " { ( 0g ` Y ) } ) )