MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  lgsqrlem2 Structured version   Unicode version

Theorem lgsqrlem2 22684
Description: Lemma for lgsqr 22688. (Contributed by Mario Carneiro, 15-Jun-2015.)
Hypotheses
Ref Expression
lgsqr.y  |-  Y  =  (ℤ/n `  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
Ref Expression
lgsqrlem2  |-  ( ph  ->  G : ( 1 ... ( ( P  -  1 )  / 
2 ) ) -1-1-> ( `' ( O `  T ) " {
( 0g `  Y
) } ) )
Distinct variable groups:    y, O    y, P    ph, y    y, T   
y, L    y, Y
Allowed substitution hints:    B( y)    D( y)    S( y)    .1. ( y)    .^ ( y)    G( y)    .- ( y)    X( y)

Proof of Theorem lgsqrlem2
Dummy variables  x  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 lgsqr.1 . . . . . . . . . . . . 13  |-  ( ph  ->  P  e.  ( Prime  \  { 2 } ) )
21eldifad 3343 . . . . . . . . . . . 12  |-  ( ph  ->  P  e.  Prime )
3 lgsqr.y . . . . . . . . . . . . 13  |-  Y  =  (ℤ/n `  P )
43znfld 17996 . . . . . . . . . . . 12  |-  ( P  e.  Prime  ->  Y  e. Field
)
52, 4syl 16 . . . . . . . . . . 11  |-  ( ph  ->  Y  e. Field )
6 fldidom 17380 . . . . . . . . . . 11  |-  ( Y  e. Field  ->  Y  e. IDomn )
75, 6syl 16 . . . . . . . . . 10  |-  ( ph  ->  Y  e. IDomn )
8 isidom 17379 . . . . . . . . . . 11  |-  ( Y  e. IDomn 
<->  ( Y  e.  CRing  /\  Y  e. Domn ) )
98simplbi 460 . . . . . . . . . 10  |-  ( Y  e. IDomn  ->  Y  e.  CRing )
107, 9syl 16 . . . . . . . . 9  |-  ( ph  ->  Y  e.  CRing )
11 crngrng 16658 . . . . . . . . 9  |-  ( Y  e.  CRing  ->  Y  e.  Ring )
1210, 11syl 16 . . . . . . . 8  |-  ( ph  ->  Y  e.  Ring )
13 lgsqr.l . . . . . . . . 9  |-  L  =  ( ZRHom `  Y
)
1413zrhrhm 17946 . . . . . . . 8  |-  ( Y  e.  Ring  ->  L  e.  (ring RingHom  Y ) )
1512, 14syl 16 . . . . . . 7  |-  ( ph  ->  L  e.  (ring RingHom  Y ) )
16 zringbas 17892 . . . . . . . 8  |-  ZZ  =  ( Base ` ring )
17 eqid 2443 . . . . . . . 8  |-  ( Base `  Y )  =  (
Base `  Y )
1816, 17rhmf 16819 . . . . . . 7  |-  ( L  e.  (ring RingHom  Y )  ->  L : ZZ --> ( Base `  Y
) )
1915, 18syl 16 . . . . . 6  |-  ( ph  ->  L : ZZ --> ( Base `  Y ) )
2019adantr 465 . . . . 5  |-  ( (
ph  /\  y  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  L : ZZ --> ( Base `  Y
) )
21 elfzelz 11456 . . . . . . 7  |-  ( y  e.  ( 1 ... ( ( P  - 
1 )  /  2
) )  ->  y  e.  ZZ )
2221adantl 466 . . . . . 6  |-  ( (
ph  /\  y  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  y  e.  ZZ )
23 zsqcl 11939 . . . . . 6  |-  ( y  e.  ZZ  ->  (
y ^ 2 )  e.  ZZ )
2422, 23syl 16 . . . . 5  |-  ( (
ph  /\  y  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
y ^ 2 )  e.  ZZ )
2520, 24ffvelrnd 5847 . . . 4  |-  ( (
ph  /\  y  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( L `  ( y ^ 2 ) )  e.  ( Base `  Y
) )
26 lgsqr.s . . . . 5  |-  S  =  (Poly1 `  Y )
27 lgsqr.b . . . . 5  |-  B  =  ( Base `  S
)
28 lgsqr.d . . . . 5  |-  D  =  ( deg1  `  Y )
29 lgsqr.o . . . . 5  |-  O  =  (eval1 `  Y )
30 lgsqr.e . . . . 5  |-  .^  =  (.g
`  (mulGrp `  S )
)
31 lgsqr.x . . . . 5  |-  X  =  (var1 `  Y )
32 lgsqr.m . . . . 5  |-  .-  =  ( -g `  S )
33 lgsqr.u . . . . 5  |-  .1.  =  ( 1r `  S )
34 lgsqr.t . . . . 5  |-  T  =  ( ( ( ( P  -  1 )  /  2 )  .^  X )  .-  .1.  )
351adantr 465 . . . . 5  |-  ( (
ph  /\  y  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  P  e.  ( Prime  \  { 2 } ) )
36 elfznn 11481 . . . . . . . . . . 11  |-  ( y  e.  ( 1 ... ( ( P  - 
1 )  /  2
) )  ->  y  e.  NN )
3736adantl 466 . . . . . . . . . 10  |-  ( (
ph  /\  y  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  y  e.  NN )
3837nncnd 10341 . . . . . . . . 9  |-  ( (
ph  /\  y  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  y  e.  CC )
39 oddprm 13885 . . . . . . . . . . . 12  |-  ( P  e.  ( Prime  \  {
2 } )  -> 
( ( P  - 
1 )  /  2
)  e.  NN )
401, 39syl 16 . . . . . . . . . . 11  |-  ( ph  ->  ( ( P  - 
1 )  /  2
)  e.  NN )
4140nnnn0d 10639 . . . . . . . . . 10  |-  ( ph  ->  ( ( P  - 
1 )  /  2
)  e.  NN0 )
4241adantr 465 . . . . . . . . 9  |-  ( (
ph  /\  y  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
( P  -  1 )  /  2 )  e.  NN0 )
43 2nn0 10599 . . . . . . . . . 10  |-  2  e.  NN0
4443a1i 11 . . . . . . . . 9  |-  ( (
ph  /\  y  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  2  e.  NN0 )
4538, 42, 44expmuld 12014 . . . . . . . 8  |-  ( (
ph  /\  y  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
y ^ ( 2  x.  ( ( P  -  1 )  / 
2 ) ) )  =  ( ( y ^ 2 ) ^
( ( P  - 
1 )  /  2
) ) )
46 prmnn 13769 . . . . . . . . . . . . . . . 16  |-  ( P  e.  Prime  ->  P  e.  NN )
472, 46syl 16 . . . . . . . . . . . . . . 15  |-  ( ph  ->  P  e.  NN )
4847nnred 10340 . . . . . . . . . . . . . 14  |-  ( ph  ->  P  e.  RR )
49 peano2rem 9678 . . . . . . . . . . . . . 14  |-  ( P  e.  RR  ->  ( P  -  1 )  e.  RR )
5048, 49syl 16 . . . . . . . . . . . . 13  |-  ( ph  ->  ( P  -  1 )  e.  RR )
5150recnd 9415 . . . . . . . . . . . 12  |-  ( ph  ->  ( P  -  1 )  e.  CC )
52 2cnd 10397 . . . . . . . . . . . 12  |-  ( ph  ->  2  e.  CC )
53 2ne0 10417 . . . . . . . . . . . . 13  |-  2  =/=  0
5453a1i 11 . . . . . . . . . . . 12  |-  ( ph  ->  2  =/=  0 )
5551, 52, 54divcan2d 10112 . . . . . . . . . . 11  |-  ( ph  ->  ( 2  x.  (
( P  -  1 )  /  2 ) )  =  ( P  -  1 ) )
56 phiprm 13855 . . . . . . . . . . . 12  |-  ( P  e.  Prime  ->  ( phi `  P )  =  ( P  -  1 ) )
572, 56syl 16 . . . . . . . . . . 11  |-  ( ph  ->  ( phi `  P
)  =  ( P  -  1 ) )
5855, 57eqtr4d 2478 . . . . . . . . . 10  |-  ( ph  ->  ( 2  x.  (
( P  -  1 )  /  2 ) )  =  ( phi `  P ) )
5958adantr 465 . . . . . . . . 9  |-  ( (
ph  /\  y  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
2  x.  ( ( P  -  1 )  /  2 ) )  =  ( phi `  P ) )
6059oveq2d 6110 . . . . . . . 8  |-  ( (
ph  /\  y  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
y ^ ( 2  x.  ( ( P  -  1 )  / 
2 ) ) )  =  ( y ^
( phi `  P
) ) )
6145, 60eqtr3d 2477 . . . . . . 7  |-  ( (
ph  /\  y  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
( y ^ 2 ) ^ ( ( P  -  1 )  /  2 ) )  =  ( y ^
( phi `  P
) ) )
6261oveq1d 6109 . . . . . 6  |-  ( (
ph  /\  y  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
( ( y ^
2 ) ^ (
( P  -  1 )  /  2 ) )  mod  P )  =  ( ( y ^ ( phi `  P ) )  mod 
P ) )
632adantr 465 . . . . . . . 8  |-  ( (
ph  /\  y  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  P  e.  Prime )
6463, 46syl 16 . . . . . . 7  |-  ( (
ph  /\  y  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  P  e.  NN )
6547nnzd 10749 . . . . . . . . . 10  |-  ( ph  ->  P  e.  ZZ )
6665adantr 465 . . . . . . . . 9  |-  ( (
ph  /\  y  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  P  e.  ZZ )
67 gcdcom 13707 . . . . . . . . 9  |-  ( ( y  e.  ZZ  /\  P  e.  ZZ )  ->  ( y  gcd  P
)  =  ( P  gcd  y ) )
6822, 66, 67syl2anc 661 . . . . . . . 8  |-  ( (
ph  /\  y  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
y  gcd  P )  =  ( P  gcd  y ) )
6937nnred 10340 . . . . . . . . . . . 12  |-  ( (
ph  /\  y  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  y  e.  RR )
7050rehalfcld 10574 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( P  - 
1 )  /  2
)  e.  RR )
7170adantr 465 . . . . . . . . . . . 12  |-  ( (
ph  /\  y  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
( P  -  1 )  /  2 )  e.  RR )
7248adantr 465 . . . . . . . . . . . 12  |-  ( (
ph  /\  y  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  P  e.  RR )
73 elfzle2 11458 . . . . . . . . . . . . 13  |-  ( y  e.  ( 1 ... ( ( P  - 
1 )  /  2
) )  ->  y  <_  ( ( P  - 
1 )  /  2
) )
7473adantl 466 . . . . . . . . . . . 12  |-  ( (
ph  /\  y  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  y  <_  ( ( P  - 
1 )  /  2
) )
75 prmuz2 13784 . . . . . . . . . . . . . . . . . 18  |-  ( P  e.  Prime  ->  P  e.  ( ZZ>= `  2 )
)
762, 75syl 16 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  P  e.  ( ZZ>= ` 
2 ) )
77 uz2m1nn 10932 . . . . . . . . . . . . . . . . 17  |-  ( P  e.  ( ZZ>= `  2
)  ->  ( P  -  1 )  e.  NN )
7876, 77syl 16 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( P  -  1 )  e.  NN )
7978nnrpd 11029 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( P  -  1 )  e.  RR+ )
80 rphalflt 11020 . . . . . . . . . . . . . . 15  |-  ( ( P  -  1 )  e.  RR+  ->  ( ( P  -  1 )  /  2 )  < 
( P  -  1 ) )
8179, 80syl 16 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( P  - 
1 )  /  2
)  <  ( P  -  1 ) )
8248ltm1d 10268 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( P  -  1 )  <  P )
8370, 50, 48, 81, 82lttrd 9535 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( P  - 
1 )  /  2
)  <  P )
8483adantr 465 . . . . . . . . . . . 12  |-  ( (
ph  /\  y  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
( P  -  1 )  /  2 )  <  P )
8569, 71, 72, 74, 84lelttrd 9532 . . . . . . . . . . 11  |-  ( (
ph  /\  y  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  y  <  P )
8669, 72ltnled 9524 . . . . . . . . . . 11  |-  ( (
ph  /\  y  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
y  <  P  <->  -.  P  <_  y ) )
8785, 86mpbid 210 . . . . . . . . . 10  |-  ( (
ph  /\  y  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  -.  P  <_  y )
88 dvdsle 13581 . . . . . . . . . . 11  |-  ( ( P  e.  ZZ  /\  y  e.  NN )  ->  ( P  ||  y  ->  P  <_  y )
)
8966, 37, 88syl2anc 661 . . . . . . . . . 10  |-  ( (
ph  /\  y  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( P  ||  y  ->  P  <_  y ) )
9087, 89mtod 177 . . . . . . . . 9  |-  ( (
ph  /\  y  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  -.  P  ||  y )
91 coprm 13789 . . . . . . . . . 10  |-  ( ( P  e.  Prime  /\  y  e.  ZZ )  ->  ( -.  P  ||  y  <->  ( P  gcd  y )  =  1 ) )
9263, 22, 91syl2anc 661 . . . . . . . . 9  |-  ( (
ph  /\  y  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( -.  P  ||  y  <->  ( P  gcd  y )  =  1 ) )
9390, 92mpbid 210 . . . . . . . 8  |-  ( (
ph  /\  y  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( P  gcd  y )  =  1 )
9468, 93eqtrd 2475 . . . . . . 7  |-  ( (
ph  /\  y  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
y  gcd  P )  =  1 )
95 eulerth 13861 . . . . . . 7  |-  ( ( P  e.  NN  /\  y  e.  ZZ  /\  (
y  gcd  P )  =  1 )  -> 
( ( y ^
( phi `  P
) )  mod  P
)  =  ( 1  mod  P ) )
9664, 22, 94, 95syl3anc 1218 . . . . . 6  |-  ( (
ph  /\  y  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
( y ^ ( phi `  P ) )  mod  P )  =  ( 1  mod  P
) )
9762, 96eqtrd 2475 . . . . 5  |-  ( (
ph  /\  y  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
( ( y ^
2 ) ^ (
( P  -  1 )  /  2 ) )  mod  P )  =  ( 1  mod 
P ) )
983, 26, 27, 28, 29, 30, 31, 32, 33, 34, 13, 35, 24, 97lgsqrlem1 22683 . . . 4  |-  ( (
ph  /\  y  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
( O `  T
) `  ( L `  ( y ^ 2 ) ) )  =  ( 0g `  Y
) )
99 eqid 2443 . . . . . . . 8  |-  ( Y  ^s  ( Base `  Y
) )  =  ( Y  ^s  ( Base `  Y
) )
100 eqid 2443 . . . . . . . 8  |-  ( Base `  ( Y  ^s  ( Base `  Y ) ) )  =  ( Base `  ( Y  ^s  ( Base `  Y
) ) )
101 fvex 5704 . . . . . . . . 9  |-  ( Base `  Y )  e.  _V
102101a1i 11 . . . . . . . 8  |-  ( ph  ->  ( Base `  Y
)  e.  _V )
10329, 26, 99, 17evl1rhm 17769 . . . . . . . . . . 11  |-  ( Y  e.  CRing  ->  O  e.  ( S RingHom  ( Y  ^s  ( Base `  Y ) ) ) )
10410, 103syl 16 . . . . . . . . . 10  |-  ( ph  ->  O  e.  ( S RingHom 
( Y  ^s  ( Base `  Y ) ) ) )
10527, 100rhmf 16819 . . . . . . . . . 10  |-  ( O  e.  ( S RingHom  ( Y  ^s  ( Base `  Y
) ) )  ->  O : B --> ( Base `  ( Y  ^s  ( Base `  Y ) ) ) )
106104, 105syl 16 . . . . . . . . 9  |-  ( ph  ->  O : B --> ( Base `  ( Y  ^s  ( Base `  Y ) ) ) )
10726ply1rng 17706 . . . . . . . . . . . . 13  |-  ( Y  e.  Ring  ->  S  e. 
Ring )
10812, 107syl 16 . . . . . . . . . . . 12  |-  ( ph  ->  S  e.  Ring )
109 rnggrp 16653 . . . . . . . . . . . 12  |-  ( S  e.  Ring  ->  S  e. 
Grp )
110108, 109syl 16 . . . . . . . . . . 11  |-  ( ph  ->  S  e.  Grp )
111 eqid 2443 . . . . . . . . . . . . . 14  |-  (mulGrp `  S )  =  (mulGrp `  S )
112111rngmgp 16654 . . . . . . . . . . . . 13  |-  ( S  e.  Ring  ->  (mulGrp `  S )  e.  Mnd )
113108, 112syl 16 . . . . . . . . . . . 12  |-  ( ph  ->  (mulGrp `  S )  e.  Mnd )
11431, 26, 27vr1cl 17674 . . . . . . . . . . . . 13  |-  ( Y  e.  Ring  ->  X  e.  B )
11512, 114syl 16 . . . . . . . . . . . 12  |-  ( ph  ->  X  e.  B )
116111, 27mgpbas 16600 . . . . . . . . . . . . 13  |-  B  =  ( Base `  (mulGrp `  S ) )
117116, 30mulgnn0cl 15646 . . . . . . . . . . . 12  |-  ( ( (mulGrp `  S )  e.  Mnd  /\  ( ( P  -  1 )  /  2 )  e. 
NN0  /\  X  e.  B )  ->  (
( ( P  - 
1 )  /  2
)  .^  X )  e.  B )
118113, 41, 115, 117syl3anc 1218 . . . . . . . . . . 11  |-  ( ph  ->  ( ( ( P  -  1 )  / 
2 )  .^  X
)  e.  B )
11927, 33rngidcl 16668 . . . . . . . . . . . 12  |-  ( S  e.  Ring  ->  .1.  e.  B )
120108, 119syl 16 . . . . . . . . . . 11  |-  ( ph  ->  .1.  e.  B )
12127, 32grpsubcl 15609 . . . . . . . . . . 11  |-  ( ( S  e.  Grp  /\  ( ( ( P  -  1 )  / 
2 )  .^  X
)  e.  B  /\  .1.  e.  B )  -> 
( ( ( ( P  -  1 )  /  2 )  .^  X )  .-  .1.  )  e.  B )
122110, 118, 120, 121syl3anc 1218 . . . . . . . . . 10  |-  ( ph  ->  ( ( ( ( P  -  1 )  /  2 )  .^  X )  .-  .1.  )  e.  B )
12334, 122syl5eqel 2527 . . . . . . . . 9  |-  ( ph  ->  T  e.  B )
124106, 123ffvelrnd 5847 . . . . . . . 8  |-  ( ph  ->  ( O `  T
)  e.  ( Base `  ( Y  ^s  ( Base `  Y ) ) ) )
12599, 17, 100, 5, 102, 124pwselbas 14430 . . . . . . 7  |-  ( ph  ->  ( O `  T
) : ( Base `  Y ) --> ( Base `  Y ) )
126 ffn 5562 . . . . . . 7  |-  ( ( O `  T ) : ( Base `  Y
) --> ( Base `  Y
)  ->  ( O `  T )  Fn  ( Base `  Y ) )
127125, 126syl 16 . . . . . 6  |-  ( ph  ->  ( O `  T
)  Fn  ( Base `  Y ) )
128127adantr 465 . . . . 5  |-  ( (
ph  /\  y  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( O `  T )  Fn  ( Base `  Y
) )
129 fniniseg 5827 . . . . 5  |-  ( ( 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 ) ) ) )
130128, 129syl 16 . . . 4  |-  ( (
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 ) ) ) )
13125, 98, 130mpbir2and 913 . . 3  |-  ( (
ph  /\  y  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  ( L `  ( y ^ 2 ) )  e.  ( `' ( O `  T )
" { ( 0g
`  Y ) } ) )
132 lgsqr.g . . 3  |-  G  =  ( y  e.  ( 1 ... ( ( P  -  1 )  /  2 ) ) 
|->  ( L `  (
y ^ 2 ) ) )
133131, 132fmptd 5870 . 2  |-  ( ph  ->  G : ( 1 ... ( ( P  -  1 )  / 
2 ) ) --> ( `' ( O `  T ) " {
( 0g `  Y
) } ) )
134 oveq1 6101 . . . . . . . . 9  |-  ( y  =  x  ->  (
y ^ 2 )  =  ( x ^
2 ) )
135134fveq2d 5698 . . . . . . . 8  |-  ( y  =  x  ->  ( L `  ( y ^ 2 ) )  =  ( L `  ( x ^ 2 ) ) )
136 fvex 5704 . . . . . . . 8  |-  ( L `
 ( x ^
2 ) )  e. 
_V
137135, 132, 136fvmpt 5777 . . . . . . 7  |-  ( x  e.  ( 1 ... ( ( P  - 
1 )  /  2
) )  ->  ( G `  x )  =  ( L `  ( x ^ 2 ) ) )
138137ad2antrl 727 . . . . . 6  |-  ( (
ph  /\  ( x  e.  ( 1 ... (
( P  -  1 )  /  2 ) )  /\  z  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) ) )  -> 
( G `  x
)  =  ( L `
 ( x ^
2 ) ) )
139 oveq1 6101 . . . . . . . . 9  |-  ( y  =  z  ->  (
y ^ 2 )  =  ( z ^
2 ) )
140139fveq2d 5698 . . . . . . . 8  |-  ( y  =  z  ->  ( L `  ( y ^ 2 ) )  =  ( L `  ( z ^ 2 ) ) )
141 fvex 5704 . . . . . . . 8  |-  ( L `
 ( z ^
2 ) )  e. 
_V
142140, 132, 141fvmpt 5777 . . . . . . 7  |-  ( z  e.  ( 1 ... ( ( P  - 
1 )  /  2
) )  ->  ( G `  z )  =  ( L `  ( z ^ 2 ) ) )
143142ad2antll 728 . . . . . 6  |-  ( (
ph  /\  ( x  e.  ( 1 ... (
( P  -  1 )  /  2 ) )  /\  z  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) ) )  -> 
( G `  z
)  =  ( L `
 ( z ^
2 ) ) )
144138, 143eqeq12d 2457 . . . . 5  |-  ( (
ph  /\  ( x  e.  ( 1 ... (
( P  -  1 )  /  2 ) )  /\  z  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) ) )  -> 
( ( G `  x )  =  ( G `  z )  <-> 
( L `  (
x ^ 2 ) )  =  ( L `
 ( z ^
2 ) ) ) )
14547nnnn0d 10639 . . . . . . 7  |-  ( ph  ->  P  e.  NN0 )
146145adantr 465 . . . . . 6  |-  ( (
ph  /\  ( x  e.  ( 1 ... (
( P  -  1 )  /  2 ) )  /\  z  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) ) )  ->  P  e.  NN0 )
147 elfzelz 11456 . . . . . . . 8  |-  ( x  e.  ( 1 ... ( ( P  - 
1 )  /  2
) )  ->  x  e.  ZZ )
148147ad2antrl 727 . . . . . . 7  |-  ( (
ph  /\  ( x  e.  ( 1 ... (
( P  -  1 )  /  2 ) )  /\  z  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) ) )  ->  x  e.  ZZ )
149 zsqcl 11939 . . . . . . 7  |-  ( x  e.  ZZ  ->  (
x ^ 2 )  e.  ZZ )
150148, 149syl 16 . . . . . 6  |-  ( (
ph  /\  ( x  e.  ( 1 ... (
( P  -  1 )  /  2 ) )  /\  z  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) ) )  -> 
( x ^ 2 )  e.  ZZ )
151 elfzelz 11456 . . . . . . . 8  |-  ( z  e.  ( 1 ... ( ( P  - 
1 )  /  2
) )  ->  z  e.  ZZ )
152151ad2antll 728 . . . . . . 7  |-  ( (
ph  /\  ( x  e.  ( 1 ... (
( P  -  1 )  /  2 ) )  /\  z  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) ) )  -> 
z  e.  ZZ )
153 zsqcl 11939 . . . . . . 7  |-  ( z  e.  ZZ  ->  (
z ^ 2 )  e.  ZZ )
154152, 153syl 16 . . . . . 6  |-  ( (
ph  /\  ( x  e.  ( 1 ... (
( P  -  1 )  /  2 ) )  /\  z  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) ) )  -> 
( z ^ 2 )  e.  ZZ )
1553, 13zndvds 17985 . . . . . 6  |-  ( ( P  e.  NN0  /\  ( x ^ 2 )  e.  ZZ  /\  ( z ^ 2 )  e.  ZZ )  ->  ( ( L `
 ( x ^
2 ) )  =  ( L `  (
z ^ 2 ) )  <->  P  ||  ( ( x ^ 2 )  -  ( z ^
2 ) ) ) )
156146, 150, 154, 155syl3anc 1218 . . . . 5  |-  ( (
ph  /\  ( x  e.  ( 1 ... (
( P  -  1 )  /  2 ) )  /\  z  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) ) )  -> 
( ( L `  ( x ^ 2 ) )  =  ( L `  ( z ^ 2 ) )  <-> 
P  ||  ( (
x ^ 2 )  -  ( z ^
2 ) ) ) )
157 elfznn 11481 . . . . . . . . 9  |-  ( x  e.  ( 1 ... ( ( P  - 
1 )  /  2
) )  ->  x  e.  NN )
158157ad2antrl 727 . . . . . . . 8  |-  ( (
ph  /\  ( x  e.  ( 1 ... (
( P  -  1 )  /  2 ) )  /\  z  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) ) )  ->  x  e.  NN )
159158nncnd 10341 . . . . . . 7  |-  ( (
ph  /\  ( x  e.  ( 1 ... (
( P  -  1 )  /  2 ) )  /\  z  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) ) )  ->  x  e.  CC )
160 elfznn 11481 . . . . . . . . 9  |-  ( z  e.  ( 1 ... ( ( P  - 
1 )  /  2
) )  ->  z  e.  NN )
161160ad2antll 728 . . . . . . . 8  |-  ( (
ph  /\  ( x  e.  ( 1 ... (
( P  -  1 )  /  2 ) )  /\  z  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) ) )  -> 
z  e.  NN )
162161nncnd 10341 . . . . . . 7  |-  ( (
ph  /\  ( x  e.  ( 1 ... (
( P  -  1 )  /  2 ) )  /\  z  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) ) )  -> 
z  e.  CC )
163 subsq 11976 . . . . . . 7  |-  ( ( x  e.  CC  /\  z  e.  CC )  ->  ( ( x ^
2 )  -  (
z ^ 2 ) )  =  ( ( x  +  z )  x.  ( x  -  z ) ) )
164159, 162, 163syl2anc 661 . . . . . 6  |-  ( (
ph  /\  ( x  e.  ( 1 ... (
( P  -  1 )  /  2 ) )  /\  z  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) ) )  -> 
( ( x ^
2 )  -  (
z ^ 2 ) )  =  ( ( x  +  z )  x.  ( x  -  z ) ) )
165164breq2d 4307 . . . . 5  |-  ( (
ph  /\  ( x  e.  ( 1 ... (
( P  -  1 )  /  2 ) )  /\  z  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) ) )  -> 
( P  ||  (
( x ^ 2 )  -  ( z ^ 2 ) )  <-> 
P  ||  ( (
x  +  z )  x.  ( x  -  z ) ) ) )
166144, 156, 1653bitrd 279 . . . 4  |-  ( (
ph  /\  ( x  e.  ( 1 ... (
( P  -  1 )  /  2 ) )  /\  z  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) ) )  -> 
( ( G `  x )  =  ( G `  z )  <-> 
P  ||  ( (
x  +  z )  x.  ( x  -  z ) ) ) )
1672adantr 465 . . . . . 6  |-  ( (
ph  /\  ( x  e.  ( 1 ... (
( P  -  1 )  /  2 ) )  /\  z  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) ) )  ->  P  e.  Prime )
168148, 152zaddcld 10754 . . . . . 6  |-  ( (
ph  /\  ( x  e.  ( 1 ... (
( P  -  1 )  /  2 ) )  /\  z  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) ) )  -> 
( x  +  z )  e.  ZZ )
169148, 152zsubcld 10755 . . . . . 6  |-  ( (
ph  /\  ( x  e.  ( 1 ... (
( P  -  1 )  /  2 ) )  /\  z  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) ) )  -> 
( x  -  z
)  e.  ZZ )
170 euclemma 13797 . . . . . 6  |-  ( ( P  e.  Prime  /\  (
x  +  z )  e.  ZZ  /\  (
x  -  z )  e.  ZZ )  -> 
( P  ||  (
( x  +  z )  x.  ( x  -  z ) )  <-> 
( P  ||  (
x  +  z )  \/  P  ||  (
x  -  z ) ) ) )
171167, 168, 169, 170syl3anc 1218 . . . . 5  |-  ( (
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 ) ) ) )
172167, 46syl 16 . . . . . . . . 9  |-  ( (
ph  /\  ( x  e.  ( 1 ... (
( P  -  1 )  /  2 ) )  /\  z  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) ) )  ->  P  e.  NN )
173172nnzd 10749 . . . . . . . 8  |-  ( (
ph  /\  ( x  e.  ( 1 ... (
( P  -  1 )  /  2 ) )  /\  z  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) ) )  ->  P  e.  ZZ )
174158, 161nnaddcld 10371 . . . . . . . 8  |-  ( (
ph  /\  ( x  e.  ( 1 ... (
( P  -  1 )  /  2 ) )  /\  z  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) ) )  -> 
( x  +  z )  e.  NN )
175 dvdsle 13581 . . . . . . . 8  |-  ( ( P  e.  ZZ  /\  ( x  +  z
)  e.  NN )  ->  ( P  ||  ( x  +  z
)  ->  P  <_  ( x  +  z ) ) )
176173, 174, 175syl2anc 661 . . . . . . 7  |-  ( (
ph  /\  ( x  e.  ( 1 ... (
( P  -  1 )  /  2 ) )  /\  z  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) ) )  -> 
( P  ||  (
x  +  z )  ->  P  <_  (
x  +  z ) ) )
177174nnred 10340 . . . . . . . . . 10  |-  ( (
ph  /\  ( x  e.  ( 1 ... (
( P  -  1 )  /  2 ) )  /\  z  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) ) )  -> 
( x  +  z )  e.  RR )
178172nnred 10340 . . . . . . . . . . 11  |-  ( (
ph  /\  ( x  e.  ( 1 ... (
( P  -  1 )  /  2 ) )  /\  z  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) ) )  ->  P  e.  RR )
179178, 49syl 16 . . . . . . . . . 10  |-  ( (
ph  /\  ( x  e.  ( 1 ... (
( P  -  1 )  /  2 ) )  /\  z  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) ) )  -> 
( P  -  1 )  e.  RR )
180158nnred 10340 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( x  e.  ( 1 ... (
( P  -  1 )  /  2 ) )  /\  z  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) ) )  ->  x  e.  RR )
181161nnred 10340 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( x  e.  ( 1 ... (
( P  -  1 )  /  2 ) )  /\  z  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) ) )  -> 
z  e.  RR )
18270adantr 465 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( x  e.  ( 1 ... (
( P  -  1 )  /  2 ) )  /\  z  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) ) )  -> 
( ( P  - 
1 )  /  2
)  e.  RR )
183 elfzle2 11458 . . . . . . . . . . . . 13  |-  ( x  e.  ( 1 ... ( ( P  - 
1 )  /  2
) )  ->  x  <_  ( ( P  - 
1 )  /  2
) )
184183ad2antrl 727 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( x  e.  ( 1 ... (
( P  -  1 )  /  2 ) )  /\  z  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) ) )  ->  x  <_  ( ( P  -  1 )  / 
2 ) )
185 elfzle2 11458 . . . . . . . . . . . . 13  |-  ( z  e.  ( 1 ... ( ( P  - 
1 )  /  2
) )  ->  z  <_  ( ( P  - 
1 )  /  2
) )
186185ad2antll 728 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( x  e.  ( 1 ... (
( P  -  1 )  /  2 ) )  /\  z  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) ) )  -> 
z  <_  ( ( P  -  1 )  /  2 ) )
187180, 181, 182, 182, 184, 186le2addd 9960 . . . . . . . . . . 11  |-  ( (
ph  /\  ( x  e.  ( 1 ... (
( P  -  1 )  /  2 ) )  /\  z  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) ) )  -> 
( x  +  z )  <_  ( (
( P  -  1 )  /  2 )  +  ( ( P  -  1 )  / 
2 ) ) )
18851adantr 465 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( x  e.  ( 1 ... (
( P  -  1 )  /  2 ) )  /\  z  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) ) )  -> 
( P  -  1 )  e.  CC )
1891882halvesd 10573 . . . . . . . . . . 11  |-  ( (
ph  /\  ( x  e.  ( 1 ... (
( P  -  1 )  /  2 ) )  /\  z  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) ) )  -> 
( ( ( P  -  1 )  / 
2 )  +  ( ( P  -  1 )  /  2 ) )  =  ( P  -  1 ) )
190187, 189breqtrd 4319 . . . . . . . . . 10  |-  ( (
ph  /\  ( x  e.  ( 1 ... (
( P  -  1 )  /  2 ) )  /\  z  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) ) )  -> 
( x  +  z )  <_  ( P  -  1 ) )
191178ltm1d 10268 . . . . . . . . . 10  |-  ( (
ph  /\  ( x  e.  ( 1 ... (
( P  -  1 )  /  2 ) )  /\  z  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) ) )  -> 
( P  -  1 )  <  P )
192177, 179, 178, 190, 191lelttrd 9532 . . . . . . . . 9  |-  ( (
ph  /\  ( x  e.  ( 1 ... (
( P  -  1 )  /  2 ) )  /\  z  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) ) )  -> 
( x  +  z )  <  P )
193177, 178ltnled 9524 . . . . . . . . 9  |-  ( (
ph  /\  ( x  e.  ( 1 ... (
( P  -  1 )  /  2 ) )  /\  z  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) ) )  -> 
( ( x  +  z )  <  P  <->  -.  P  <_  ( x  +  z ) ) )
194192, 193mpbid 210 . . . . . . . 8  |-  ( (
ph  /\  ( x  e.  ( 1 ... (
( P  -  1 )  /  2 ) )  /\  z  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) ) )  ->  -.  P  <_  ( x  +  z ) )
195194pm2.21d 106 . . . . . . 7  |-  ( (
ph  /\  ( x  e.  ( 1 ... (
( P  -  1 )  /  2 ) )  /\  z  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) ) )  -> 
( P  <_  (
x  +  z )  ->  x  =  z ) )
196176, 195syld 44 . . . . . 6  |-  ( (
ph  /\  ( x  e.  ( 1 ... (
( P  -  1 )  /  2 ) )  /\  z  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) ) )  -> 
( P  ||  (
x  +  z )  ->  x  =  z ) )
197 moddvds 13545 . . . . . . . . 9  |-  ( ( P  e.  NN  /\  x  e.  ZZ  /\  z  e.  ZZ )  ->  (
( x  mod  P
)  =  ( z  mod  P )  <->  P  ||  (
x  -  z ) ) )
198172, 148, 152, 197syl3anc 1218 . . . . . . . 8  |-  ( (
ph  /\  ( x  e.  ( 1 ... (
( P  -  1 )  /  2 ) )  /\  z  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) ) )  -> 
( ( x  mod  P )  =  ( z  mod  P )  <->  P  ||  (
x  -  z ) ) )
199172nnrpd 11029 . . . . . . . . . 10  |-  ( (
ph  /\  ( x  e.  ( 1 ... (
( P  -  1 )  /  2 ) )  /\  z  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) ) )  ->  P  e.  RR+ )
200158nnnn0d 10639 . . . . . . . . . . 11  |-  ( (
ph  /\  ( x  e.  ( 1 ... (
( P  -  1 )  /  2 ) )  /\  z  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) ) )  ->  x  e.  NN0 )
201200nn0ge0d 10642 . . . . . . . . . 10  |-  ( (
ph  /\  ( x  e.  ( 1 ... (
( P  -  1 )  /  2 ) )  /\  z  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) ) )  -> 
0  <_  x )
20283adantr 465 . . . . . . . . . . 11  |-  ( (
ph  /\  ( x  e.  ( 1 ... (
( P  -  1 )  /  2 ) )  /\  z  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) ) )  -> 
( ( P  - 
1 )  /  2
)  <  P )
203180, 182, 178, 184, 202lelttrd 9532 . . . . . . . . . 10  |-  ( (
ph  /\  ( x  e.  ( 1 ... (
( P  -  1 )  /  2 ) )  /\  z  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) ) )  ->  x  <  P )
204 modid 11735 . . . . . . . . . 10  |-  ( ( ( x  e.  RR  /\  P  e.  RR+ )  /\  ( 0  <_  x  /\  x  <  P ) )  ->  ( x  mod  P )  =  x )
205180, 199, 201, 203, 204syl22anc 1219 . . . . . . . . 9  |-  ( (
ph  /\  ( x  e.  ( 1 ... (
( P  -  1 )  /  2 ) )  /\  z  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) ) )  -> 
( x  mod  P
)  =  x )
206161nnnn0d 10639 . . . . . . . . . . 11  |-  ( (
ph  /\  ( x  e.  ( 1 ... (
( P  -  1 )  /  2 ) )  /\  z  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) ) )  -> 
z  e.  NN0 )
207206nn0ge0d 10642 . . . . . . . . . 10  |-  ( (
ph  /\  ( x  e.  ( 1 ... (
( P  -  1 )  /  2 ) )  /\  z  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) ) )  -> 
0  <_  z )
208181, 182, 178, 186, 202lelttrd 9532 . . . . . . . . . 10  |-  ( (
ph  /\  ( x  e.  ( 1 ... (
( P  -  1 )  /  2 ) )  /\  z  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) ) )  -> 
z  <  P )
209 modid 11735 . . . . . . . . . 10  |-  ( ( ( z  e.  RR  /\  P  e.  RR+ )  /\  ( 0  <_  z  /\  z  <  P ) )  ->  ( z  mod  P )  =  z )
210181, 199, 207, 208, 209syl22anc 1219 . . . . . . . . 9  |-  ( (
ph  /\  ( x  e.  ( 1 ... (
( P  -  1 )  /  2 ) )  /\  z  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) ) )  -> 
( z  mod  P
)  =  z )
211205, 210eqeq12d 2457 . . . . . . . 8  |-  ( (
ph  /\  ( x  e.  ( 1 ... (
( P  -  1 )  /  2 ) )  /\  z  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) ) )  -> 
( ( x  mod  P )  =  ( z  mod  P )  <->  x  =  z ) )
212198, 211bitr3d 255 . . . . . . 7  |-  ( (
ph  /\  ( x  e.  ( 1 ... (
( P  -  1 )  /  2 ) )  /\  z  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) ) )  -> 
( P  ||  (
x  -  z )  <-> 
x  =  z ) )
213212biimpd 207 . . . . . 6  |-  ( (
ph  /\  ( x  e.  ( 1 ... (
( P  -  1 )  /  2 ) )  /\  z  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) ) )  -> 
( P  ||  (
x  -  z )  ->  x  =  z ) )
214196, 213jaod 380 . . . . 5  |-  ( (
ph  /\  ( x  e.  ( 1 ... (
( P  -  1 )  /  2 ) )  /\  z  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) ) )  -> 
( ( P  ||  ( x  +  z
)  \/  P  ||  ( x  -  z
) )  ->  x  =  z ) )
215171, 214sylbid 215 . . . 4  |-  ( (
ph  /\  ( x  e.  ( 1 ... (
( P  -  1 )  /  2 ) )  /\  z  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) ) )  -> 
( P  ||  (
( x  +  z )  x.  ( x  -  z ) )  ->  x  =  z ) )
216166, 215sylbid 215 . . 3  |-  ( (
ph  /\  ( x  e.  ( 1 ... (
( P  -  1 )  /  2 ) )  /\  z  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) ) )  -> 
( ( G `  x )  =  ( G `  z )  ->  x  =  z ) )
217216ralrimivva 2811 . 2  |-  ( ph  ->  A. x  e.  ( 1 ... ( ( P  -  1 )  /  2 ) ) A. z  e.  ( 1 ... ( ( P  -  1 )  /  2 ) ) ( ( G `  x )  =  ( G `  z )  ->  x  =  z ) )
218 dff13 5974 . 2  |-  ( 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 )
) )
219133, 217, 218sylanbrc 664 1  |-  ( ph  ->  G : ( 1 ... ( ( P  -  1 )  / 
2 ) ) -1-1-> ( `' ( O `  T ) " {
( 0g `  Y
) } ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184    \/ wo 368    /\ wa 369    = wceq 1369    e. wcel 1756    =/= wne 2609   A.wral 2718   _Vcvv 2975    \ cdif 3328   {csn 3880   class class class wbr 4295    e. cmpt 4353   `'ccnv 4842   "cima 4846    Fn wfn 5416   -->wf 5417   -1-1->wf1 5418   ` cfv 5421  (class class class)co 6094   CCcc 9283   RRcr 9284   0cc0 9285   1c1 9286    + caddc 9288    x. cmul 9290    < clt 9421    <_ cle 9422    - cmin 9598    / cdiv 9996   NNcn 10325   2c2 10374   NN0cn0 10582   ZZcz 10649   ZZ>=cuz 10864   RR+crp 10994   ...cfz 11440    mod cmo 11711   ^cexp 11868    || cdivides 13538    gcd cgcd 13693   Primecprime 13766   phicphi 13842   Basecbs 14177   0gc0g 14381    ^s cpws 14388   Mndcmnd 15412   Grpcgrp 15413   -gcsg 15416  .gcmg 15417  mulGrpcmgp 16594   1rcur 16606   Ringcrg 16648   CRingccrg 16649   RingHom crh 16807  Fieldcfield 16836  Domncdomn 17354  IDomncidom 17355  var1cv1 17635  Poly1cpl1 17636  eval1ce1 17752  ℤringzring 17886   ZRHomczrh 17934  ℤ/nczn 17937   deg1 cdg1 21526
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-rep 4406  ax-sep 4416  ax-nul 4424  ax-pow 4473  ax-pr 4534  ax-un 6375  ax-inf2 7850  ax-cnex 9341  ax-resscn 9342  ax-1cn 9343  ax-icn 9344  ax-addcl 9345  ax-addrcl 9346  ax-mulcl 9347  ax-mulrcl 9348  ax-mulcom 9349  ax-addass 9350  ax-mulass 9351  ax-distr 9352  ax-i2m1 9353  ax-1ne0 9354  ax-1rid 9355  ax-rnegex 9356  ax-rrecex 9357  ax-cnre 9358  ax-pre-lttri 9359  ax-pre-lttrn 9360  ax-pre-ltadd 9361  ax-pre-mulgt0 9362  ax-pre-sup 9363  ax-addf 9364  ax-mulf 9365
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2571  df-ne 2611  df-nel 2612  df-ral 2723  df-rex 2724  df-reu 2725  df-rmo 2726  df-rab 2727  df-v 2977  df-sbc 3190  df-csb 3292  df-dif 3334  df-un 3336  df-in 3338  df-ss 3345  df-pss 3347  df-nul 3641  df-if 3795  df-pw 3865  df-sn 3881  df-pr 3883  df-tp 3885  df-op 3887  df-uni 4095  df-int 4132  df-iun 4176  df-iin 4177  df-br 4296  df-opab 4354  df-mpt 4355  df-tr 4389  df-eprel 4635  df-id 4639  df-po 4644  df-so 4645  df-fr 4682  df-se 4683  df-we 4684  df-ord 4725  df-on 4726  df-lim 4727  df-suc 4728  df-xp 4849  df-rel 4850  df-cnv 4851  df-co 4852  df-dm 4853  df-rn 4854  df-res 4855  df-ima 4856  df-iota 5384  df-fun 5423  df-fn 5424  df-f 5425  df-f1 5426  df-fo 5427  df-f1o 5428  df-fv 5429  df-isom 5430  df-riota 6055  df-ov 6097  df-oprab 6098  df-mpt2 6099  df-of 6323  df-ofr 6324  df-om 6480  df-1st 6580  df-2nd 6581  df-supp 6694  df-tpos 6748  df-recs 6835  df-rdg 6869  df-1o 6923  df-2o 6924  df-oadd 6927  df-er 7104  df-ec 7106  df-qs 7110  df-map 7219  df-pm 7220  df-ixp 7267  df-en 7314  df-dom 7315  df-sdom 7316  df-fin 7317  df-fsupp 7624  df-sup 7694  df-oi 7727  df-card 8112  df-cda 8340  df-pnf 9423  df-mnf 9424  df-xr 9425  df-ltxr 9426  df-le 9427  df-sub 9600  df-neg 9601  df-div 9997  df-nn 10326  df-2 10383  df-3 10384  df-4 10385  df-5 10386  df-6 10387  df-7 10388  df-8 10389  df-9 10390  df-10 10391  df-n0 10583  df-z 10650  df-dec 10759  df-uz 10865  df-rp 10995  df-fz 11441  df-fzo 11552  df-fl 11645  df-mod 11712  df-seq 11810  df-exp 11869  df-hash 12107  df-cj 12591  df-re 12592  df-im 12593  df-sqr 12727  df-abs 12728  df-dvds 13539  df-gcd 13694  df-prm 13767  df-phi 13844  df-struct 14179  df-ndx 14180  df-slot 14181  df-base 14182  df-sets 14183  df-ress 14184  df-plusg 14254  df-mulr 14255  df-starv 14256  df-sca 14257  df-vsca 14258  df-ip 14259  df-tset 14260  df-ple 14261  df-ds 14263  df-unif 14264  df-hom 14265  df-cco 14266  df-0g 14383  df-gsum 14384  df-prds 14389  df-pws 14391  df-imas 14449  df-divs 14450  df-mre 14527  df-mrc 14528  df-acs 14530  df-mnd 15418  df-mhm 15467  df-submnd 15468  df-grp 15548  df-minusg 15549  df-sbg 15550  df-mulg 15551  df-subg 15681  df-nsg 15682  df-eqg 15683  df-ghm 15748  df-cntz 15838  df-cmn 16282  df-abl 16283  df-mgp 16595  df-ur 16607  df-srg 16611  df-rng 16650  df-cring 16651  df-oppr 16718  df-dvdsr 16736  df-unit 16737  df-invr 16767  df-dvr 16778  df-rnghom 16809  df-drng 16837  df-field 16838  df-subrg 16866  df-lmod 16953  df-lss 17017  df-lsp 17056  df-sra 17256  df-rgmod 17257  df-lidl 17258  df-rsp 17259  df-2idl 17317  df-nzr 17343  df-rlreg 17357  df-domn 17358  df-idom 17359  df-assa 17387  df-asp 17388  df-ascl 17389  df-psr 17426  df-mvr 17427  df-mpl 17428  df-opsr 17430  df-evls 17591  df-evl 17592  df-psr1 17639  df-vr1 17640  df-ply1 17641  df-evl1 17754  df-cnfld 17822  df-zring 17887  df-zrh 17938  df-zn 17941
This theorem is referenced by:  lgsqrlem4  22686
  Copyright terms: Public domain W3C validator