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 ffvelcdmd 
 |-  ( ( 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 3 mgpbas 
 |-  B = ( Base ` ( mulGrp ` S ) )
112 110 ringmgp 
 |-  ( S e. Ring -> ( mulGrp ` S ) e. Mnd )
113 107 112 syl 
 |-  ( ph -> ( mulGrp ` S ) e. Mnd )
114 7 2 3 vr1cl 
 |-  ( Y e. Ring -> X e. B )
115 23 114 syl 
 |-  ( ph -> X e. B )
116 111 6 113 42 115 mulgnn0cld 
 |-  ( ph -> ( ( ( P - 1 ) / 2 ) .^ X ) e. B )
117 3 9 ringidcl 
 |-  ( S e. Ring -> .1. e. B )
118 107 117 syl 
 |-  ( ph -> .1. e. B )
119 3 8 grpsubcl 
 |-  ( ( S e. Grp /\ ( ( ( P - 1 ) / 2 ) .^ X ) e. B /\ .1. e. B ) -> ( ( ( ( P - 1 ) / 2 ) .^ X ) .- .1. ) e. B )
120 109 116 118 119 syl3anc 
 |-  ( ph -> ( ( ( ( P - 1 ) / 2 ) .^ X ) .- .1. ) e. B )
121 10 120 eqeltrid 
 |-  ( ph -> T e. B )
122 105 121 ffvelcdmd 
 |-  ( ph -> ( O ` T ) e. ( Base ` ( Y ^s ( Base ` Y ) ) ) )
123 99 27 100 16 101 122 pwselbas 
 |-  ( ph -> ( O ` T ) : ( Base ` Y ) --> ( Base ` Y ) )
124 123 ffnd 
 |-  ( ph -> ( O ` T ) Fn ( Base ` Y ) )
125 124 adantr 
 |-  ( ( ph /\ y e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( O ` T ) Fn ( Base ` Y ) )
126 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 ) ) ) )
127 125 126 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 ) ) ) )
128 35 98 127 mpbir2and 
 |-  ( ( ph /\ y e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) -> ( L ` ( y ^ 2 ) ) e. ( `' ( O ` T ) " { ( 0g ` Y ) } ) )
129 128 13 fmptd 
 |-  ( ph -> G : ( 1 ... ( ( P - 1 ) / 2 ) ) --> ( `' ( O ` T ) " { ( 0g ` Y ) } ) )
130 fvoveq1 
 |-  ( y = x -> ( L ` ( y ^ 2 ) ) = ( L ` ( x ^ 2 ) ) )
131 fvex 
 |-  ( L ` ( x ^ 2 ) ) e. _V
132 130 13 131 fvmpt 
 |-  ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) -> ( G ` x ) = ( L ` ( x ^ 2 ) ) )
133 132 ad2antrl 
 |-  ( ( ph /\ ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ z e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( G ` x ) = ( L ` ( x ^ 2 ) ) )
134 fvoveq1 
 |-  ( y = z -> ( L ` ( y ^ 2 ) ) = ( L ` ( z ^ 2 ) ) )
135 fvex 
 |-  ( L ` ( z ^ 2 ) ) e. _V
136 134 13 135 fvmpt 
 |-  ( z e. ( 1 ... ( ( P - 1 ) / 2 ) ) -> ( G ` z ) = ( L ` ( z ^ 2 ) ) )
137 136 ad2antll 
 |-  ( ( ph /\ ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ z e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( G ` z ) = ( L ` ( z ^ 2 ) ) )
138 133 137 eqeq12d 
 |-  ( ( ph /\ ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ z e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( G ` x ) = ( G ` z ) <-> ( L ` ( x ^ 2 ) ) = ( L ` ( z ^ 2 ) ) ) )
139 48 nnnn0d 
 |-  ( ph -> P e. NN0 )
140 139 adantr 
 |-  ( ( ph /\ ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ z e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> P e. NN0 )
141 elfzelz 
 |-  ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) -> x e. ZZ )
142 141 ad2antrl 
 |-  ( ( ph /\ ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ z e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> x e. ZZ )
143 zsqcl 
 |-  ( x e. ZZ -> ( x ^ 2 ) e. ZZ )
144 142 143 syl 
 |-  ( ( ph /\ ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ z e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( x ^ 2 ) e. ZZ )
145 elfzelz 
 |-  ( z e. ( 1 ... ( ( P - 1 ) / 2 ) ) -> z e. ZZ )
146 145 ad2antll 
 |-  ( ( ph /\ ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ z e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> z e. ZZ )
147 zsqcl 
 |-  ( z e. ZZ -> ( z ^ 2 ) e. ZZ )
148 146 147 syl 
 |-  ( ( ph /\ ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ z e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( z ^ 2 ) e. ZZ )
149 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 ) ) ) )
150 140 144 148 149 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 ) ) ) )
151 elfznn 
 |-  ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) -> x e. NN )
152 151 ad2antrl 
 |-  ( ( ph /\ ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ z e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> x e. NN )
153 152 nncnd 
 |-  ( ( ph /\ ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ z e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> x e. CC )
154 elfznn 
 |-  ( z e. ( 1 ... ( ( P - 1 ) / 2 ) ) -> z e. NN )
155 154 ad2antll 
 |-  ( ( ph /\ ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ z e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> z e. NN )
156 155 nncnd 
 |-  ( ( ph /\ ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ z e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> z e. CC )
157 subsq 
 |-  ( ( x e. CC /\ z e. CC ) -> ( ( x ^ 2 ) - ( z ^ 2 ) ) = ( ( x + z ) x. ( x - z ) ) )
158 153 156 157 syl2anc 
 |-  ( ( ph /\ ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ z e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( x ^ 2 ) - ( z ^ 2 ) ) = ( ( x + z ) x. ( x - z ) ) )
159 158 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 ) ) ) )
160 138 150 159 3bitrd 
 |-  ( ( ph /\ ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ z e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( G ` x ) = ( G ` z ) <-> P || ( ( x + z ) x. ( x - z ) ) ) )
161 14 adantr 
 |-  ( ( ph /\ ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ z e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> P e. Prime )
162 142 146 zaddcld 
 |-  ( ( ph /\ ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ z e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( x + z ) e. ZZ )
163 142 146 zsubcld 
 |-  ( ( ph /\ ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ z e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( x - z ) e. ZZ )
164 euclemma 
 |-  ( ( P e. Prime /\ ( x + z ) e. ZZ /\ ( x - z ) e. ZZ ) -> ( P || ( ( x + z ) x. ( x - z ) ) <-> ( P || ( x + z ) \/ P || ( x - z ) ) ) )
165 161 162 163 164 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 ) ) ) )
166 161 47 syl 
 |-  ( ( ph /\ ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ z e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> P e. NN )
167 166 nnzd 
 |-  ( ( ph /\ ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ z e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> P e. ZZ )
168 152 155 nnaddcld 
 |-  ( ( ph /\ ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ z e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( x + z ) e. NN )
169 dvdsle 
 |-  ( ( P e. ZZ /\ ( x + z ) e. NN ) -> ( P || ( x + z ) -> P <_ ( x + z ) ) )
170 167 168 169 syl2anc 
 |-  ( ( ph /\ ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ z e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( P || ( x + z ) -> P <_ ( x + z ) ) )
171 168 nnred 
 |-  ( ( ph /\ ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ z e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( x + z ) e. RR )
172 166 nnred 
 |-  ( ( ph /\ ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ z e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> P e. RR )
173 172 50 syl 
 |-  ( ( ph /\ ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ z e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( P - 1 ) e. RR )
174 152 nnred 
 |-  ( ( ph /\ ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ z e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> x e. RR )
175 155 nnred 
 |-  ( ( ph /\ ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ z e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> z e. RR )
176 70 adantr 
 |-  ( ( ph /\ ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ z e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( P - 1 ) / 2 ) e. RR )
177 elfzle2 
 |-  ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) -> x <_ ( ( P - 1 ) / 2 ) )
178 177 ad2antrl 
 |-  ( ( ph /\ ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ z e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> x <_ ( ( P - 1 ) / 2 ) )
179 elfzle2 
 |-  ( z e. ( 1 ... ( ( P - 1 ) / 2 ) ) -> z <_ ( ( P - 1 ) / 2 ) )
180 179 ad2antll 
 |-  ( ( ph /\ ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ z e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> z <_ ( ( P - 1 ) / 2 ) )
181 174 175 176 176 178 180 le2addd 
 |-  ( ( ph /\ ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ z e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( x + z ) <_ ( ( ( P - 1 ) / 2 ) + ( ( P - 1 ) / 2 ) ) )
182 52 adantr 
 |-  ( ( ph /\ ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ z e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( P - 1 ) e. CC )
183 182 2halvesd 
 |-  ( ( ph /\ ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ z e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( ( P - 1 ) / 2 ) + ( ( P - 1 ) / 2 ) ) = ( P - 1 ) )
184 181 183 breqtrd 
 |-  ( ( ph /\ ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ z e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( x + z ) <_ ( P - 1 ) )
185 172 ltm1d 
 |-  ( ( ph /\ ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ z e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( P - 1 ) < P )
186 171 173 172 184 185 lelttrd 
 |-  ( ( ph /\ ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ z e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( x + z ) < P )
187 171 172 ltnled 
 |-  ( ( ph /\ ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ z e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( x + z ) < P <-> -. P <_ ( x + z ) ) )
188 186 187 mpbid 
 |-  ( ( ph /\ ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ z e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> -. P <_ ( x + z ) )
189 188 pm2.21d 
 |-  ( ( ph /\ ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ z e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( P <_ ( x + z ) -> x = z ) )
190 170 189 syld 
 |-  ( ( ph /\ ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ z e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( P || ( x + z ) -> x = z ) )
191 moddvds 
 |-  ( ( P e. NN /\ x e. ZZ /\ z e. ZZ ) -> ( ( x mod P ) = ( z mod P ) <-> P || ( x - z ) ) )
192 166 142 146 191 syl3anc 
 |-  ( ( ph /\ ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ z e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( x mod P ) = ( z mod P ) <-> P || ( x - z ) ) )
193 166 nnrpd 
 |-  ( ( ph /\ ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ z e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> P e. RR+ )
194 152 nnnn0d 
 |-  ( ( ph /\ ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ z e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> x e. NN0 )
195 194 nn0ge0d 
 |-  ( ( ph /\ ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ z e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> 0 <_ x )
196 83 adantr 
 |-  ( ( ph /\ ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ z e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( P - 1 ) / 2 ) < P )
197 174 176 172 178 196 lelttrd 
 |-  ( ( ph /\ ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ z e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> x < P )
198 modid 
 |-  ( ( ( x e. RR /\ P e. RR+ ) /\ ( 0 <_ x /\ x < P ) ) -> ( x mod P ) = x )
199 174 193 195 197 198 syl22anc 
 |-  ( ( ph /\ ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ z e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( x mod P ) = x )
200 155 nnnn0d 
 |-  ( ( ph /\ ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ z e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> z e. NN0 )
201 200 nn0ge0d 
 |-  ( ( ph /\ ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ z e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> 0 <_ z )
202 175 176 172 180 196 lelttrd 
 |-  ( ( ph /\ ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ z e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> z < P )
203 modid 
 |-  ( ( ( z e. RR /\ P e. RR+ ) /\ ( 0 <_ z /\ z < P ) ) -> ( z mod P ) = z )
204 175 193 201 202 203 syl22anc 
 |-  ( ( ph /\ ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ z e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( z mod P ) = z )
205 199 204 eqeq12d 
 |-  ( ( ph /\ ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ z e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( x mod P ) = ( z mod P ) <-> x = z ) )
206 192 205 bitr3d 
 |-  ( ( ph /\ ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ z e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( P || ( x - z ) <-> x = z ) )
207 206 biimpd 
 |-  ( ( ph /\ ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ z e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( P || ( x - z ) -> x = z ) )
208 190 207 jaod 
 |-  ( ( ph /\ ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ z e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( P || ( x + z ) \/ P || ( x - z ) ) -> x = z ) )
209 165 208 sylbid 
 |-  ( ( ph /\ ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ z e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( P || ( ( x + z ) x. ( x - z ) ) -> x = z ) )
210 160 209 sylbid 
 |-  ( ( ph /\ ( x e. ( 1 ... ( ( P - 1 ) / 2 ) ) /\ z e. ( 1 ... ( ( P - 1 ) / 2 ) ) ) ) -> ( ( G ` x ) = ( G ` z ) -> x = z ) )
211 210 ralrimivva 
 |-  ( ph -> A. x e. ( 1 ... ( ( P - 1 ) / 2 ) ) A. z e. ( 1 ... ( ( P - 1 ) / 2 ) ) ( ( G ` x ) = ( G ` z ) -> x = z ) )
212 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 ) ) )
213 129 211 212 sylanbrc 
 |-  ( ph -> G : ( 1 ... ( ( P - 1 ) / 2 ) ) -1-1-> ( `' ( O ` T ) " { ( 0g ` Y ) } ) )