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 ) } ) )