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

Theorem lgsqrlem2 22650
Description: Lemma for lgsqr 22654. (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 3333 . . . . . . . . . . . 12  |-  ( ph  ->  P  e.  Prime )
3 lgsqr.y . . . . . . . . . . . . 13  |-  Y  =  (ℤ/n `  P )
43znfld 17962 . . . . . . . . . . . 12  |-  ( P  e.  Prime  ->  Y  e. Field
)
52, 4syl 16 . . . . . . . . . . 11  |-  ( ph  ->  Y  e. Field )
6 fldidom 17351 . . . . . . . . . . 11  |-  ( Y  e. Field  ->  Y  e. IDomn )
75, 6syl 16 . . . . . . . . . 10  |-  ( ph  ->  Y  e. IDomn )
8 isidom 17350 . . . . . . . . . . 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 16641 . . . . . . . . 9  |-  ( Y  e.  CRing  ->  Y  e.  Ring )
1210, 11syl 16 . . . . . . . 8  |-  ( ph  ->  Y  e.  Ring )
13 lgsqr.l . . . . . . . . 9  |-  L  =  ( ZRHom `  Y
)
1413zrhrhm 17912 . . . . . . . 8  |-  ( Y  e.  Ring  ->  L  e.  (ring RingHom  Y ) )
1512, 14syl 16 . . . . . . 7  |-  ( ph  ->  L  e.  (ring RingHom  Y ) )
16 zringbas 17858 . . . . . . . 8  |-  ZZ  =  ( Base ` ring )
17 eqid 2437 . . . . . . . 8  |-  ( Base `  Y )  =  (
Base `  Y )
1816, 17rhmf 16800 . . . . . . 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 11445 . . . . . . 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 11928 . . . . . 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 5837 . . . 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 11470 . . . . . . . . . . 11  |-  ( y  e.  ( 1 ... ( ( P  - 
1 )  /  2
) )  ->  y  e.  NN )
3736adantl 466 . . . . . . . . . 10  |-  ( (
ph  /\  y  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  y  e.  NN )
3837nncnd 10330 . . . . . . . . 9  |-  ( (
ph  /\  y  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  y  e.  CC )
39 oddprm 13874 . . . . . . . . . . . 12  |-  ( P  e.  ( Prime  \  {
2 } )  -> 
( ( P  - 
1 )  /  2
)  e.  NN )
401, 39syl 16 . . . . . . . . . . 11  |-  ( ph  ->  ( ( P  - 
1 )  /  2
)  e.  NN )
4140nnnn0d 10628 . . . . . . . . . 10  |-  ( ph  ->  ( ( P  - 
1 )  /  2
)  e.  NN0 )
4241adantr 465 . . . . . . . . 9  |-  ( (
ph  /\  y  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
( P  -  1 )  /  2 )  e.  NN0 )
43 2nn0 10588 . . . . . . . . . 10  |-  2  e.  NN0
4443a1i 11 . . . . . . . . 9  |-  ( (
ph  /\  y  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  2  e.  NN0 )
4538, 42, 44expmuld 12003 . . . . . . . 8  |-  ( (
ph  /\  y  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
y ^ ( 2  x.  ( ( P  -  1 )  / 
2 ) ) )  =  ( ( y ^ 2 ) ^
( ( P  - 
1 )  /  2
) ) )
46 prmnn 13758 . . . . . . . . . . . . . . . 16  |-  ( P  e.  Prime  ->  P  e.  NN )
472, 46syl 16 . . . . . . . . . . . . . . 15  |-  ( ph  ->  P  e.  NN )
4847nnred 10329 . . . . . . . . . . . . . 14  |-  ( ph  ->  P  e.  RR )
49 peano2rem 9667 . . . . . . . . . . . . . 14  |-  ( P  e.  RR  ->  ( P  -  1 )  e.  RR )
5048, 49syl 16 . . . . . . . . . . . . 13  |-  ( ph  ->  ( P  -  1 )  e.  RR )
5150recnd 9404 . . . . . . . . . . . 12  |-  ( ph  ->  ( P  -  1 )  e.  CC )
52 2cnd 10386 . . . . . . . . . . . 12  |-  ( ph  ->  2  e.  CC )
53 2ne0 10406 . . . . . . . . . . . . 13  |-  2  =/=  0
5453a1i 11 . . . . . . . . . . . 12  |-  ( ph  ->  2  =/=  0 )
5551, 52, 54divcan2d 10101 . . . . . . . . . . 11  |-  ( ph  ->  ( 2  x.  (
( P  -  1 )  /  2 ) )  =  ( P  -  1 ) )
56 phiprm 13844 . . . . . . . . . . . 12  |-  ( P  e.  Prime  ->  ( phi `  P )  =  ( P  -  1 ) )
572, 56syl 16 . . . . . . . . . . 11  |-  ( ph  ->  ( phi `  P
)  =  ( P  -  1 ) )
5855, 57eqtr4d 2472 . . . . . . . . . 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 6102 . . . . . . . 8  |-  ( (
ph  /\  y  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
y ^ ( 2  x.  ( ( P  -  1 )  / 
2 ) ) )  =  ( y ^
( phi `  P
) ) )
6145, 60eqtr3d 2471 . . . . . . 7  |-  ( (
ph  /\  y  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
( y ^ 2 ) ^ ( ( P  -  1 )  /  2 ) )  =  ( y ^
( phi `  P
) ) )
6261oveq1d 6101 . . . . . 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 10738 . . . . . . . . . 10  |-  ( ph  ->  P  e.  ZZ )
6665adantr 465 . . . . . . . . 9  |-  ( (
ph  /\  y  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  P  e.  ZZ )
67 gcdcom 13696 . . . . . . . . 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 10329 . . . . . . . . . . . 12  |-  ( (
ph  /\  y  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  y  e.  RR )
7050rehalfcld 10563 . . . . . . . . . . . . 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 11447 . . . . . . . . . . . . 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 13773 . . . . . . . . . . . . . . . . . 18  |-  ( P  e.  Prime  ->  P  e.  ( ZZ>= `  2 )
)
762, 75syl 16 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  P  e.  ( ZZ>= ` 
2 ) )
77 uz2m1nn 10921 . . . . . . . . . . . . . . . . 17  |-  ( P  e.  ( ZZ>= `  2
)  ->  ( P  -  1 )  e.  NN )
7876, 77syl 16 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( P  -  1 )  e.  NN )
7978nnrpd 11018 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( P  -  1 )  e.  RR+ )
80 rphalflt 11009 . . . . . . . . . . . . . . 15  |-  ( ( P  -  1 )  e.  RR+  ->  ( ( P  -  1 )  /  2 )  < 
( P  -  1 ) )
8179, 80syl 16 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( P  - 
1 )  /  2
)  <  ( P  -  1 ) )
8248ltm1d 10257 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( P  -  1 )  <  P )
8370, 50, 48, 81, 82lttrd 9524 . . . . . . . . . . . . 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 9521 . . . . . . . . . . 11  |-  ( (
ph  /\  y  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  y  <  P )
8669, 72ltnled 9513 . . . . . . . . . . 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 13570 . . . . . . . . . . 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 13778 . . . . . . . . . 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 2469 . . . . . . 7  |-  ( (
ph  /\  y  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
y  gcd  P )  =  1 )
95 eulerth 13850 . . . . . . 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 2469 . . . . 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 22649 . . . 4  |-  ( (
ph  /\  y  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) )  ->  (
( O `  T
) `  ( L `  ( y ^ 2 ) ) )  =  ( 0g `  Y
) )
99 eqid 2437 . . . . . . . 8  |-  ( Y  ^s  ( Base `  Y
) )  =  ( Y  ^s  ( Base `  Y
) )
100 eqid 2437 . . . . . . . 8  |-  ( Base `  ( Y  ^s  ( Base `  Y ) ) )  =  ( Base `  ( Y  ^s  ( Base `  Y
) ) )
101 fvex 5694 . . . . . . . . 9  |-  ( Base `  Y )  e.  _V
102101a1i 11 . . . . . . . 8  |-  ( ph  ->  ( Base `  Y
)  e.  _V )
10329, 26, 99, 17evl1rhm 17735 . . . . . . . . . . 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 16800 . . . . . . . . . 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 17674 . . . . . . . . . . . . 13  |-  ( Y  e.  Ring  ->  S  e. 
Ring )
10812, 107syl 16 . . . . . . . . . . . 12  |-  ( ph  ->  S  e.  Ring )
109 rnggrp 16636 . . . . . . . . . . . 12  |-  ( S  e.  Ring  ->  S  e. 
Grp )
110108, 109syl 16 . . . . . . . . . . 11  |-  ( ph  ->  S  e.  Grp )
111 eqid 2437 . . . . . . . . . . . . . 14  |-  (mulGrp `  S )  =  (mulGrp `  S )
112111rngmgp 16637 . . . . . . . . . . . . 13  |-  ( S  e.  Ring  ->  (mulGrp `  S )  e.  Mnd )
113108, 112syl 16 . . . . . . . . . . . 12  |-  ( ph  ->  (mulGrp `  S )  e.  Mnd )
11431, 26, 27vr1cl 17643 . . . . . . . . . . . . 13  |-  ( Y  e.  Ring  ->  X  e.  B )
11512, 114syl 16 . . . . . . . . . . . 12  |-  ( ph  ->  X  e.  B )
116111, 27mgpbas 16583 . . . . . . . . . . . . 13  |-  B  =  ( Base `  (mulGrp `  S ) )
117116, 30mulgnn0cl 15632 . . . . . . . . . . . 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 16651 . . . . . . . . . . . 12  |-  ( S  e.  Ring  ->  .1.  e.  B )
120108, 119syl 16 . . . . . . . . . . 11  |-  ( ph  ->  .1.  e.  B )
12127, 32grpsubcl 15595 . . . . . . . . . . 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 2521 . . . . . . . . 9  |-  ( ph  ->  T  e.  B )
124106, 123ffvelrnd 5837 . . . . . . . 8  |-  ( ph  ->  ( O `  T
)  e.  ( Base `  ( Y  ^s  ( Base `  Y ) ) ) )
12599, 17, 100, 5, 102, 124pwselbas 14419 . . . . . . 7  |-  ( ph  ->  ( O `  T
) : ( Base `  Y ) --> ( Base `  Y ) )
126 ffn 5552 . . . . . . 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 5817 . . . . 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 5860 . 2  |-  ( ph  ->  G : ( 1 ... ( ( P  -  1 )  / 
2 ) ) --> ( `' ( O `  T ) " {
( 0g `  Y
) } ) )
134 oveq1 6093 . . . . . . . . 9  |-  ( y  =  x  ->  (
y ^ 2 )  =  ( x ^
2 ) )
135134fveq2d 5688 . . . . . . . 8  |-  ( y  =  x  ->  ( L `  ( y ^ 2 ) )  =  ( L `  ( x ^ 2 ) ) )
136 fvex 5694 . . . . . . . 8  |-  ( L `
 ( x ^
2 ) )  e. 
_V
137135, 132, 136fvmpt 5767 . . . . . . 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 6093 . . . . . . . . 9  |-  ( y  =  z  ->  (
y ^ 2 )  =  ( z ^
2 ) )
140139fveq2d 5688 . . . . . . . 8  |-  ( y  =  z  ->  ( L `  ( y ^ 2 ) )  =  ( L `  ( z ^ 2 ) ) )
141 fvex 5694 . . . . . . . 8  |-  ( L `
 ( z ^
2 ) )  e. 
_V
142140, 132, 141fvmpt 5767 . . . . . . 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 2451 . . . . 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 10628 . . . . . . 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 11445 . . . . . . . 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 11928 . . . . . . 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 11445 . . . . . . . 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 11928 . . . . . . 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 17951 . . . . . 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 11470 . . . . . . . . 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 10330 . . . . . . 7  |-  ( (
ph  /\  ( x  e.  ( 1 ... (
( P  -  1 )  /  2 ) )  /\  z  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) ) )  ->  x  e.  CC )
160 elfznn 11470 . . . . . . . . 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 10330 . . . . . . 7  |-  ( (
ph  /\  ( x  e.  ( 1 ... (
( P  -  1 )  /  2 ) )  /\  z  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) ) )  -> 
z  e.  CC )
163 subsq 11965 . . . . . . 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 4297 . . . . 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 10743 . . . . . 6  |-  ( (
ph  /\  ( x  e.  ( 1 ... (
( P  -  1 )  /  2 ) )  /\  z  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) ) )  -> 
( x  +  z )  e.  ZZ )
169148, 152zsubcld 10744 . . . . . 6  |-  ( (
ph  /\  ( x  e.  ( 1 ... (
( P  -  1 )  /  2 ) )  /\  z  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) ) )  -> 
( x  -  z
)  e.  ZZ )
170 euclemma 13786 . . . . . 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 10738 . . . . . . . 8  |-  ( (
ph  /\  ( x  e.  ( 1 ... (
( P  -  1 )  /  2 ) )  /\  z  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) ) )  ->  P  e.  ZZ )
174158, 161nnaddcld 10360 . . . . . . . 8  |-  ( (
ph  /\  ( x  e.  ( 1 ... (
( P  -  1 )  /  2 ) )  /\  z  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) ) )  -> 
( x  +  z )  e.  NN )
175 dvdsle 13570 . . . . . . . 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 10329 . . . . . . . . . 10  |-  ( (
ph  /\  ( x  e.  ( 1 ... (
( P  -  1 )  /  2 ) )  /\  z  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) ) )  -> 
( x  +  z )  e.  RR )
178172nnred 10329 . . . . . . . . . . 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 10329 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( x  e.  ( 1 ... (
( P  -  1 )  /  2 ) )  /\  z  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) ) )  ->  x  e.  RR )
181161nnred 10329 . . . . . . . . . . . 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 11447 . . . . . . . . . . . . 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 11447 . . . . . . . . . . . . 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 9949 . . . . . . . . . . 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 10562 . . . . . . . . . . 11  |-  ( (
ph  /\  ( x  e.  ( 1 ... (
( P  -  1 )  /  2 ) )  /\  z  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) ) )  -> 
( ( ( P  -  1 )  / 
2 )  +  ( ( P  -  1 )  /  2 ) )  =  ( P  -  1 ) )
190187, 189breqtrd 4309 . . . . . . . . . 10  |-  ( (
ph  /\  ( x  e.  ( 1 ... (
( P  -  1 )  /  2 ) )  /\  z  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) ) )  -> 
( x  +  z )  <_  ( P  -  1 ) )
191178ltm1d 10257 . . . . . . . . . 10  |-  ( (
ph  /\  ( x  e.  ( 1 ... (
( P  -  1 )  /  2 ) )  /\  z  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) ) )  -> 
( P  -  1 )  <  P )
192177, 179, 178, 190, 191lelttrd 9521 . . . . . . . . 9  |-  ( (
ph  /\  ( x  e.  ( 1 ... (
( P  -  1 )  /  2 ) )  /\  z  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) ) )  -> 
( x  +  z )  <  P )
193177, 178ltnled 9513 . . . . . . . . 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 13534 . . . . . . . . 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 11018 . . . . . . . . . 10  |-  ( (
ph  /\  ( x  e.  ( 1 ... (
( P  -  1 )  /  2 ) )  /\  z  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) ) )  ->  P  e.  RR+ )
200158nnnn0d 10628 . . . . . . . . . . 11  |-  ( (
ph  /\  ( x  e.  ( 1 ... (
( P  -  1 )  /  2 ) )  /\  z  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) ) )  ->  x  e.  NN0 )
201200nn0ge0d 10631 . . . . . . . . . 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 9521 . . . . . . . . . 10  |-  ( (
ph  /\  ( x  e.  ( 1 ... (
( P  -  1 )  /  2 ) )  /\  z  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) ) )  ->  x  <  P )
204 modid 11724 . . . . . . . . . 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 10628 . . . . . . . . . . 11  |-  ( (
ph  /\  ( x  e.  ( 1 ... (
( P  -  1 )  /  2 ) )  /\  z  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) ) )  -> 
z  e.  NN0 )
207206nn0ge0d 10631 . . . . . . . . . 10  |-  ( (
ph  /\  ( x  e.  ( 1 ... (
( P  -  1 )  /  2 ) )  /\  z  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) ) )  -> 
0  <_  z )
208181, 182, 178, 186, 202lelttrd 9521 . . . . . . . . . 10  |-  ( (
ph  /\  ( x  e.  ( 1 ... (
( P  -  1 )  /  2 ) )  /\  z  e.  ( 1 ... (
( P  -  1 )  /  2 ) ) ) )  -> 
z  <  P )
209 modid 11724 . . . . . . . . . 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 2451 . . . . . . . 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 2802 . 2  |-  ( ph  ->  A. x  e.  ( 1 ... ( ( P  -  1 )  /  2 ) ) A. z  e.  ( 1 ... ( ( P  -  1 )  /  2 ) ) ( ( G `  x )  =  ( G `  z )  ->  x  =  z ) )
218 dff13 5964 . 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 2600   A.wral 2709   _Vcvv 2966    \ cdif 3318   {csn 3870   class class class wbr 4285    e. cmpt 4343   `'ccnv 4831   "cima 4835    Fn wfn 5406   -->wf 5407   -1-1->wf1 5408   ` cfv 5411  (class class class)co 6086   CCcc 9272   RRcr 9273   0cc0 9274   1c1 9275    + caddc 9277    x. cmul 9279    < clt 9410    <_ cle 9411    - cmin 9587    / cdiv 9985   NNcn 10314   2c2 10363   NN0cn0 10571   ZZcz 10638   ZZ>=cuz 10853   RR+crp 10983   ...cfz 11429    mod cmo 11700   ^cexp 11857    || cdivides 13527    gcd cgcd 13682   Primecprime 13755   phicphi 13831   Basecbs 14166   0gc0g 14370    ^s cpws 14377   Mndcmnd 15401   Grpcgrp 15402   -gcsg 15405  .gcmg 15406  mulGrpcmgp 16577   1rcur 16589   Ringcrg 16631   CRingccrg 16632   RingHom crh 16790  Fieldcfield 16809  Domncdomn 17325  IDomncidom 17326  var1cv1 17604  Poly1cpl1 17605  eval1ce1 17718  ℤringzring 17852   ZRHomczrh 17900  ℤ/nczn 17903   deg1 cdg1 21492
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 2418  ax-rep 4396  ax-sep 4406  ax-nul 4414  ax-pow 4463  ax-pr 4524  ax-un 6367  ax-inf2 7839  ax-cnex 9330  ax-resscn 9331  ax-1cn 9332  ax-icn 9333  ax-addcl 9334  ax-addrcl 9335  ax-mulcl 9336  ax-mulrcl 9337  ax-mulcom 9338  ax-addass 9339  ax-mulass 9340  ax-distr 9341  ax-i2m1 9342  ax-1ne0 9343  ax-1rid 9344  ax-rnegex 9345  ax-rrecex 9346  ax-cnre 9347  ax-pre-lttri 9348  ax-pre-lttrn 9349  ax-pre-ltadd 9350  ax-pre-mulgt0 9351  ax-pre-sup 9352  ax-addf 9353  ax-mulf 9354
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 2256  df-mo 2257  df-clab 2424  df-cleq 2430  df-clel 2433  df-nfc 2562  df-ne 2602  df-nel 2603  df-ral 2714  df-rex 2715  df-reu 2716  df-rmo 2717  df-rab 2718  df-v 2968  df-sbc 3180  df-csb 3282  df-dif 3324  df-un 3326  df-in 3328  df-ss 3335  df-pss 3337  df-nul 3631  df-if 3785  df-pw 3855  df-sn 3871  df-pr 3873  df-tp 3875  df-op 3877  df-uni 4085  df-int 4122  df-iun 4166  df-iin 4167  df-br 4286  df-opab 4344  df-mpt 4345  df-tr 4379  df-eprel 4624  df-id 4628  df-po 4633  df-so 4634  df-fr 4671  df-se 4672  df-we 4673  df-ord 4714  df-on 4715  df-lim 4716  df-suc 4717  df-xp 4838  df-rel 4839  df-cnv 4840  df-co 4841  df-dm 4842  df-rn 4843  df-res 4844  df-ima 4845  df-iota 5374  df-fun 5413  df-fn 5414  df-f 5415  df-f1 5416  df-fo 5417  df-f1o 5418  df-fv 5419  df-isom 5420  df-riota 6045  df-ov 6089  df-oprab 6090  df-mpt2 6091  df-of 6315  df-ofr 6316  df-om 6472  df-1st 6572  df-2nd 6573  df-supp 6686  df-tpos 6740  df-recs 6824  df-rdg 6858  df-1o 6912  df-2o 6913  df-oadd 6916  df-er 7093  df-ec 7095  df-qs 7099  df-map 7208  df-pm 7209  df-ixp 7256  df-en 7303  df-dom 7304  df-sdom 7305  df-fin 7306  df-fsupp 7613  df-sup 7683  df-oi 7716  df-card 8101  df-cda 8329  df-pnf 9412  df-mnf 9413  df-xr 9414  df-ltxr 9415  df-le 9416  df-sub 9589  df-neg 9590  df-div 9986  df-nn 10315  df-2 10372  df-3 10373  df-4 10374  df-5 10375  df-6 10376  df-7 10377  df-8 10378  df-9 10379  df-10 10380  df-n0 10572  df-z 10639  df-dec 10748  df-uz 10854  df-rp 10984  df-fz 11430  df-fzo 11541  df-fl 11634  df-mod 11701  df-seq 11799  df-exp 11858  df-hash 12096  df-cj 12580  df-re 12581  df-im 12582  df-sqr 12716  df-abs 12717  df-dvds 13528  df-gcd 13683  df-prm 13756  df-phi 13833  df-struct 14168  df-ndx 14169  df-slot 14170  df-base 14171  df-sets 14172  df-ress 14173  df-plusg 14243  df-mulr 14244  df-starv 14245  df-sca 14246  df-vsca 14247  df-ip 14248  df-tset 14249  df-ple 14250  df-ds 14252  df-unif 14253  df-hom 14254  df-cco 14255  df-0g 14372  df-gsum 14373  df-prds 14378  df-pws 14380  df-imas 14438  df-divs 14439  df-mre 14516  df-mrc 14517  df-acs 14519  df-mnd 15407  df-mhm 15456  df-submnd 15457  df-grp 15534  df-minusg 15535  df-sbg 15536  df-mulg 15537  df-subg 15667  df-nsg 15668  df-eqg 15669  df-ghm 15734  df-cntz 15824  df-cmn 16268  df-abl 16269  df-mgp 16578  df-ur 16590  df-rng 16633  df-cring 16634  df-oppr 16701  df-dvdsr 16719  df-unit 16720  df-invr 16750  df-dvr 16761  df-rnghom 16792  df-drng 16810  df-field 16811  df-subrg 16839  df-lmod 16926  df-lss 16988  df-lsp 17027  df-sra 17227  df-rgmod 17228  df-lidl 17229  df-rsp 17230  df-2idl 17288  df-nzr 17314  df-rlreg 17328  df-domn 17329  df-idom 17330  df-assa 17358  df-asp 17359  df-ascl 17360  df-psr 17397  df-mvr 17398  df-mpl 17399  df-opsr 17401  df-evls 17560  df-evl 17561  df-psr1 17608  df-vr1 17609  df-ply1 17610  df-evl1 17720  df-cnfld 17788  df-zring 17853  df-zrh 17904  df-zn 17907
This theorem is referenced by:  lgsqrlem4  22652
  Copyright terms: Public domain W3C validator