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

Theorem lgsquadlem3 20701
Description: Lemma for lgsquad 20702. (Contributed by Mario Carneiro, 18-Jun-2015.)
Hypotheses
Ref Expression
lgseisen.1  |-  ( ph  ->  P  e.  ( Prime  \  { 2 } ) )
lgseisen.2  |-  ( ph  ->  Q  e.  ( Prime  \  { 2 } ) )
lgseisen.3  |-  ( ph  ->  P  =/=  Q )
lgsquad.4  |-  M  =  ( ( P  - 
1 )  /  2
)
lgsquad.5  |-  N  =  ( ( Q  - 
1 )  /  2
)
lgsquad.6  |-  S  =  { <. x ,  y
>.  |  ( (
x  e.  ( 1 ... M )  /\  y  e.  ( 1 ... N ) )  /\  ( y  x.  P )  <  (
x  x.  Q ) ) }
Assertion
Ref Expression
lgsquadlem3  |-  ( ph  ->  ( ( P  / L Q )  x.  ( Q  / L P ) )  =  ( -u
1 ^ ( M  x.  N ) ) )
Distinct variable groups:    x, y, P    ph, x, y    y, M    x, N, y    x, Q, y    x, S    x, M    y, S

Proof of Theorem lgsquadlem3
Dummy variables  w  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 lgseisen.2 . . . . 5  |-  ( ph  ->  Q  e.  ( Prime  \  { 2 } ) )
2 lgseisen.1 . . . . 5  |-  ( ph  ->  P  e.  ( Prime  \  { 2 } ) )
3 lgseisen.3 . . . . . 6  |-  ( ph  ->  P  =/=  Q )
43necomd 2604 . . . . 5  |-  ( ph  ->  Q  =/=  P )
5 lgsquad.5 . . . . 5  |-  N  =  ( ( Q  - 
1 )  /  2
)
6 lgsquad.4 . . . . 5  |-  M  =  ( ( P  - 
1 )  /  2
)
7 eleq1 2418 . . . . . . . . . 10  |-  ( x  =  z  ->  (
x  e.  ( 1 ... M )  <->  z  e.  ( 1 ... M
) ) )
8 eleq1 2418 . . . . . . . . . 10  |-  ( y  =  w  ->  (
y  e.  ( 1 ... N )  <->  w  e.  ( 1 ... N
) ) )
97, 8bi2anan9 843 . . . . . . . . 9  |-  ( ( x  =  z  /\  y  =  w )  ->  ( ( x  e.  ( 1 ... M
)  /\  y  e.  ( 1 ... N
) )  <->  ( z  e.  ( 1 ... M
)  /\  w  e.  ( 1 ... N
) ) ) )
10 ancom 437 . . . . . . . . 9  |-  ( ( z  e.  ( 1 ... M )  /\  w  e.  ( 1 ... N ) )  <-> 
( w  e.  ( 1 ... N )  /\  z  e.  ( 1 ... M ) ) )
119, 10syl6bb 252 . . . . . . . 8  |-  ( ( x  =  z  /\  y  =  w )  ->  ( ( x  e.  ( 1 ... M
)  /\  y  e.  ( 1 ... N
) )  <->  ( w  e.  ( 1 ... N
)  /\  z  e.  ( 1 ... M
) ) ) )
12 oveq1 5949 . . . . . . . . 9  |-  ( x  =  z  ->  (
x  x.  Q )  =  ( z  x.  Q ) )
13 oveq1 5949 . . . . . . . . 9  |-  ( y  =  w  ->  (
y  x.  P )  =  ( w  x.  P ) )
1412, 13breqan12d 4117 . . . . . . . 8  |-  ( ( x  =  z  /\  y  =  w )  ->  ( ( x  x.  Q )  <  (
y  x.  P )  <-> 
( z  x.  Q
)  <  ( w  x.  P ) ) )
1511, 14anbi12d 691 . . . . . . 7  |-  ( ( x  =  z  /\  y  =  w )  ->  ( ( ( x  e.  ( 1 ... M )  /\  y  e.  ( 1 ... N
) )  /\  (
x  x.  Q )  <  ( y  x.  P ) )  <->  ( (
w  e.  ( 1 ... N )  /\  z  e.  ( 1 ... M ) )  /\  ( z  x.  Q )  <  (
w  x.  P ) ) ) )
1615ancoms 439 . . . . . 6  |-  ( ( y  =  w  /\  x  =  z )  ->  ( ( ( x  e.  ( 1 ... M )  /\  y  e.  ( 1 ... N
) )  /\  (
x  x.  Q )  <  ( y  x.  P ) )  <->  ( (
w  e.  ( 1 ... N )  /\  z  e.  ( 1 ... M ) )  /\  ( z  x.  Q )  <  (
w  x.  P ) ) ) )
1716cbvopabv 4167 . . . . 5  |-  { <. y ,  x >.  |  ( ( x  e.  ( 1 ... M )  /\  y  e.  ( 1 ... N ) )  /\  ( x  x.  Q )  < 
( y  x.  P
) ) }  =  { <. w ,  z
>.  |  ( (
w  e.  ( 1 ... N )  /\  z  e.  ( 1 ... M ) )  /\  ( z  x.  Q )  <  (
w  x.  P ) ) }
181, 2, 4, 5, 6, 17lgsquadlem2 20700 . . . 4  |-  ( ph  ->  ( P  / L Q )  =  (
-u 1 ^ ( # `
 { <. y ,  x >.  |  (
( x  e.  ( 1 ... M )  /\  y  e.  ( 1 ... N ) )  /\  ( x  x.  Q )  < 
( y  x.  P
) ) } ) ) )
19 relopab 4891 . . . . . . . 8  |-  Rel  { <. x ,  y >.  |  ( ( x  e.  ( 1 ... M )  /\  y  e.  ( 1 ... N
) )  /\  (
x  x.  Q )  <  ( y  x.  P ) ) }
20 fzfid 11124 . . . . . . . . . 10  |-  ( ph  ->  ( 1 ... M
)  e.  Fin )
21 fzfid 11124 . . . . . . . . . 10  |-  ( ph  ->  ( 1 ... N
)  e.  Fin )
22 xpfi 7215 . . . . . . . . . 10  |-  ( ( ( 1 ... M
)  e.  Fin  /\  ( 1 ... N
)  e.  Fin )  ->  ( ( 1 ... M )  X.  (
1 ... N ) )  e.  Fin )
2320, 21, 22syl2anc 642 . . . . . . . . 9  |-  ( ph  ->  ( ( 1 ... M )  X.  (
1 ... N ) )  e.  Fin )
24 opabssxp 4841 . . . . . . . . 9  |-  { <. x ,  y >.  |  ( ( x  e.  ( 1 ... M )  /\  y  e.  ( 1 ... N ) )  /\  ( x  x.  Q )  < 
( y  x.  P
) ) }  C_  ( ( 1 ... M )  X.  (
1 ... N ) )
25 ssfi 7168 . . . . . . . . 9  |-  ( ( ( ( 1 ... M )  X.  (
1 ... N ) )  e.  Fin  /\  { <. x ,  y >.  |  ( ( x  e.  ( 1 ... M )  /\  y  e.  ( 1 ... N
) )  /\  (
x  x.  Q )  <  ( y  x.  P ) ) } 
C_  ( ( 1 ... M )  X.  ( 1 ... N
) ) )  ->  { <. x ,  y
>.  |  ( (
x  e.  ( 1 ... M )  /\  y  e.  ( 1 ... N ) )  /\  ( x  x.  Q )  <  (
y  x.  P ) ) }  e.  Fin )
2623, 24, 25sylancl 643 . . . . . . . 8  |-  ( ph  ->  { <. x ,  y
>.  |  ( (
x  e.  ( 1 ... M )  /\  y  e.  ( 1 ... N ) )  /\  ( x  x.  Q )  <  (
y  x.  P ) ) }  e.  Fin )
27 cnven 7021 . . . . . . . 8  |-  ( ( Rel  { <. x ,  y >.  |  ( ( x  e.  ( 1 ... M )  /\  y  e.  ( 1 ... N ) )  /\  ( x  x.  Q )  < 
( y  x.  P
) ) }  /\  {
<. x ,  y >.  |  ( ( x  e.  ( 1 ... M )  /\  y  e.  ( 1 ... N
) )  /\  (
x  x.  Q )  <  ( y  x.  P ) ) }  e.  Fin )  ->  { <. x ,  y
>.  |  ( (
x  e.  ( 1 ... M )  /\  y  e.  ( 1 ... N ) )  /\  ( x  x.  Q )  <  (
y  x.  P ) ) }  ~~  `' { <. x ,  y
>.  |  ( (
x  e.  ( 1 ... M )  /\  y  e.  ( 1 ... N ) )  /\  ( x  x.  Q )  <  (
y  x.  P ) ) } )
2819, 26, 27sylancr 644 . . . . . . 7  |-  ( ph  ->  { <. x ,  y
>.  |  ( (
x  e.  ( 1 ... M )  /\  y  e.  ( 1 ... N ) )  /\  ( x  x.  Q )  <  (
y  x.  P ) ) }  ~~  `' { <. x ,  y
>.  |  ( (
x  e.  ( 1 ... M )  /\  y  e.  ( 1 ... N ) )  /\  ( x  x.  Q )  <  (
y  x.  P ) ) } )
29 cnvopab 5162 . . . . . . 7  |-  `' { <. x ,  y >.  |  ( ( x  e.  ( 1 ... M )  /\  y  e.  ( 1 ... N
) )  /\  (
x  x.  Q )  <  ( y  x.  P ) ) }  =  { <. y ,  x >.  |  (
( x  e.  ( 1 ... M )  /\  y  e.  ( 1 ... N ) )  /\  ( x  x.  Q )  < 
( y  x.  P
) ) }
3028, 29syl6breq 4141 . . . . . 6  |-  ( ph  ->  { <. x ,  y
>.  |  ( (
x  e.  ( 1 ... M )  /\  y  e.  ( 1 ... N ) )  /\  ( x  x.  Q )  <  (
y  x.  P ) ) }  ~~  { <. y ,  x >.  |  ( ( x  e.  ( 1 ... M
)  /\  y  e.  ( 1 ... N
) )  /\  (
x  x.  Q )  <  ( y  x.  P ) ) } )
31 hasheni 11437 . . . . . 6  |-  ( {
<. x ,  y >.  |  ( ( x  e.  ( 1 ... M )  /\  y  e.  ( 1 ... N
) )  /\  (
x  x.  Q )  <  ( y  x.  P ) ) } 
~~  { <. y ,  x >.  |  (
( x  e.  ( 1 ... M )  /\  y  e.  ( 1 ... N ) )  /\  ( x  x.  Q )  < 
( y  x.  P
) ) }  ->  (
# `  { <. x ,  y >.  |  ( ( x  e.  ( 1 ... M )  /\  y  e.  ( 1 ... N ) )  /\  ( x  x.  Q )  < 
( y  x.  P
) ) } )  =  ( # `  { <. y ,  x >.  |  ( ( x  e.  ( 1 ... M
)  /\  y  e.  ( 1 ... N
) )  /\  (
x  x.  Q )  <  ( y  x.  P ) ) } ) )
3230, 31syl 15 . . . . 5  |-  ( ph  ->  ( # `  { <. x ,  y >.  |  ( ( x  e.  ( 1 ... M )  /\  y  e.  ( 1 ... N
) )  /\  (
x  x.  Q )  <  ( y  x.  P ) ) } )  =  ( # `  { <. y ,  x >.  |  ( ( x  e.  ( 1 ... M )  /\  y  e.  ( 1 ... N
) )  /\  (
x  x.  Q )  <  ( y  x.  P ) ) } ) )
3332oveq2d 5958 . . . 4  |-  ( ph  ->  ( -u 1 ^ ( # `  { <. x ,  y >.  |  ( ( x  e.  ( 1 ... M )  /\  y  e.  ( 1 ... N
) )  /\  (
x  x.  Q )  <  ( y  x.  P ) ) } ) )  =  (
-u 1 ^ ( # `
 { <. y ,  x >.  |  (
( x  e.  ( 1 ... M )  /\  y  e.  ( 1 ... N ) )  /\  ( x  x.  Q )  < 
( y  x.  P
) ) } ) ) )
3418, 33eqtr4d 2393 . . 3  |-  ( ph  ->  ( P  / L Q )  =  (
-u 1 ^ ( # `
 { <. x ,  y >.  |  ( ( x  e.  ( 1 ... M )  /\  y  e.  ( 1 ... N ) )  /\  ( x  x.  Q )  < 
( y  x.  P
) ) } ) ) )
35 lgsquad.6 . . . 4  |-  S  =  { <. x ,  y
>.  |  ( (
x  e.  ( 1 ... M )  /\  y  e.  ( 1 ... N ) )  /\  ( y  x.  P )  <  (
x  x.  Q ) ) }
362, 1, 3, 6, 5, 35lgsquadlem2 20700 . . 3  |-  ( ph  ->  ( Q  / L P )  =  (
-u 1 ^ ( # `
 S ) ) )
3734, 36oveq12d 5960 . 2  |-  ( ph  ->  ( ( P  / L Q )  x.  ( Q  / L P ) )  =  ( (
-u 1 ^ ( # `
 { <. x ,  y >.  |  ( ( x  e.  ( 1 ... M )  /\  y  e.  ( 1 ... N ) )  /\  ( x  x.  Q )  < 
( y  x.  P
) ) } ) )  x.  ( -u
1 ^ ( # `  S ) ) ) )
38 neg1cn 9900 . . . 4  |-  -u 1  e.  CC
3938a1i 10 . . 3  |-  ( ph  -> 
-u 1  e.  CC )
40 opabssxp 4841 . . . . . 6  |-  { <. x ,  y >.  |  ( ( x  e.  ( 1 ... M )  /\  y  e.  ( 1 ... N ) )  /\  ( y  x.  P )  < 
( x  x.  Q
) ) }  C_  ( ( 1 ... M )  X.  (
1 ... N ) )
4135, 40eqsstri 3284 . . . . 5  |-  S  C_  ( ( 1 ... M )  X.  (
1 ... N ) )
42 ssfi 7168 . . . . 5  |-  ( ( ( ( 1 ... M )  X.  (
1 ... N ) )  e.  Fin  /\  S  C_  ( ( 1 ... M )  X.  (
1 ... N ) ) )  ->  S  e.  Fin )
4323, 41, 42sylancl 643 . . . 4  |-  ( ph  ->  S  e.  Fin )
44 hashcl 11440 . . . 4  |-  ( S  e.  Fin  ->  ( # `
 S )  e. 
NN0 )
4543, 44syl 15 . . 3  |-  ( ph  ->  ( # `  S
)  e.  NN0 )
46 hashcl 11440 . . . 4  |-  ( {
<. x ,  y >.  |  ( ( x  e.  ( 1 ... M )  /\  y  e.  ( 1 ... N
) )  /\  (
x  x.  Q )  <  ( y  x.  P ) ) }  e.  Fin  ->  ( # `
 { <. x ,  y >.  |  ( ( x  e.  ( 1 ... M )  /\  y  e.  ( 1 ... N ) )  /\  ( x  x.  Q )  < 
( y  x.  P
) ) } )  e.  NN0 )
4726, 46syl 15 . . 3  |-  ( ph  ->  ( # `  { <. x ,  y >.  |  ( ( x  e.  ( 1 ... M )  /\  y  e.  ( 1 ... N
) )  /\  (
x  x.  Q )  <  ( y  x.  P ) ) } )  e.  NN0 )
4839, 45, 47expaddd 11337 . 2  |-  ( ph  ->  ( -u 1 ^ ( ( # `  { <. x ,  y >.  |  ( ( x  e.  ( 1 ... M )  /\  y  e.  ( 1 ... N
) )  /\  (
x  x.  Q )  <  ( y  x.  P ) ) } )  +  ( # `  S ) ) )  =  ( ( -u
1 ^ ( # `  { <. x ,  y
>.  |  ( (
x  e.  ( 1 ... M )  /\  y  e.  ( 1 ... N ) )  /\  ( x  x.  Q )  <  (
y  x.  P ) ) } ) )  x.  ( -u 1 ^ ( # `  S
) ) ) )
49 eldifi 3374 . . . . . . . . . . . . . . . . . 18  |-  ( Q  e.  ( Prime  \  {
2 } )  ->  Q  e.  Prime )
501, 49syl 15 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  Q  e.  Prime )
5150adantr 451 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( x  e.  ( 1 ... M
)  /\  y  e.  ( 1 ... N
) ) )  ->  Q  e.  Prime )
52 prmnn 12852 . . . . . . . . . . . . . . . 16  |-  ( Q  e.  Prime  ->  Q  e.  NN )
5351, 52syl 15 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( x  e.  ( 1 ... M
)  /\  y  e.  ( 1 ... N
) ) )  ->  Q  e.  NN )
54 oddprm 12959 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( Q  e.  ( Prime  \  {
2 } )  -> 
( ( Q  - 
1 )  /  2
)  e.  NN )
551, 54syl 15 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( ( Q  - 
1 )  /  2
)  e.  NN )
565, 55syl5eqel 2442 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  N  e.  NN )
5756adantr 451 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( x  e.  ( 1 ... M
)  /\  y  e.  ( 1 ... N
) ) )  ->  N  e.  NN )
5857nnzd 10205 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( x  e.  ( 1 ... M
)  /\  y  e.  ( 1 ... N
) ) )  ->  N  e.  ZZ )
59 prmz 12853 . . . . . . . . . . . . . . . . . . . 20  |-  ( Q  e.  Prime  ->  Q  e.  ZZ )
6051, 59syl 15 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( x  e.  ( 1 ... M
)  /\  y  e.  ( 1 ... N
) ) )  ->  Q  e.  ZZ )
61 peano2zm 10151 . . . . . . . . . . . . . . . . . . 19  |-  ( Q  e.  ZZ  ->  ( Q  -  1 )  e.  ZZ )
6260, 61syl 15 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( x  e.  ( 1 ... M
)  /\  y  e.  ( 1 ... N
) ) )  -> 
( Q  -  1 )  e.  ZZ )
6357nnred 9848 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( x  e.  ( 1 ... M
)  /\  y  e.  ( 1 ... N
) ) )  ->  N  e.  RR )
6462zred 10206 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( x  e.  ( 1 ... M
)  /\  y  e.  ( 1 ... N
) ) )  -> 
( Q  -  1 )  e.  RR )
65 prmuz2 12867 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( Q  e.  Prime  ->  Q  e.  ( ZZ>= `  2 )
)
6651, 65syl 15 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  ( x  e.  ( 1 ... M
)  /\  y  e.  ( 1 ... N
) ) )  ->  Q  e.  ( ZZ>= ` 
2 ) )
67 uz2m1nn 10381 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( Q  e.  ( ZZ>= `  2
)  ->  ( Q  -  1 )  e.  NN )
6866, 67syl 15 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  ( x  e.  ( 1 ... M
)  /\  y  e.  ( 1 ... N
) ) )  -> 
( Q  -  1 )  e.  NN )
6968nnrpd 10478 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  ( x  e.  ( 1 ... M
)  /\  y  e.  ( 1 ... N
) ) )  -> 
( Q  -  1 )  e.  RR+ )
70 rphalflt 10469 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( Q  -  1 )  e.  RR+  ->  ( ( Q  -  1 )  /  2 )  < 
( Q  -  1 ) )
7169, 70syl 15 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( x  e.  ( 1 ... M
)  /\  y  e.  ( 1 ... N
) ) )  -> 
( ( Q  - 
1 )  /  2
)  <  ( Q  -  1 ) )
725, 71syl5eqbr 4135 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( x  e.  ( 1 ... M
)  /\  y  e.  ( 1 ... N
) ) )  ->  N  <  ( Q  - 
1 ) )
7363, 64, 72ltled 9054 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( x  e.  ( 1 ... M
)  /\  y  e.  ( 1 ... N
) ) )  ->  N  <_  ( Q  - 
1 ) )
74 eluz2 10325 . . . . . . . . . . . . . . . . . 18  |-  ( ( Q  -  1 )  e.  ( ZZ>= `  N
)  <->  ( N  e.  ZZ  /\  ( Q  -  1 )  e.  ZZ  /\  N  <_ 
( Q  -  1 ) ) )
7558, 62, 73, 74syl3anbrc 1136 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( x  e.  ( 1 ... M
)  /\  y  e.  ( 1 ... N
) ) )  -> 
( Q  -  1 )  e.  ( ZZ>= `  N ) )
76 fzss2 10920 . . . . . . . . . . . . . . . . 17  |-  ( ( Q  -  1 )  e.  ( ZZ>= `  N
)  ->  ( 1 ... N )  C_  ( 1 ... ( Q  -  1 ) ) )
7775, 76syl 15 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( x  e.  ( 1 ... M
)  /\  y  e.  ( 1 ... N
) ) )  -> 
( 1 ... N
)  C_  ( 1 ... ( Q  - 
1 ) ) )
78 simprr 733 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( x  e.  ( 1 ... M
)  /\  y  e.  ( 1 ... N
) ) )  -> 
y  e.  ( 1 ... N ) )
7977, 78sseldd 3257 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( x  e.  ( 1 ... M
)  /\  y  e.  ( 1 ... N
) ) )  -> 
y  e.  ( 1 ... ( Q  - 
1 ) ) )
80 fzm1ndvds 12671 . . . . . . . . . . . . . . 15  |-  ( ( Q  e.  NN  /\  y  e.  ( 1 ... ( Q  - 
1 ) ) )  ->  -.  Q  ||  y
)
8153, 79, 80syl2anc 642 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( x  e.  ( 1 ... M
)  /\  y  e.  ( 1 ... N
) ) )  ->  -.  Q  ||  y )
824adantr 451 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( x  e.  ( 1 ... M
)  /\  y  e.  ( 1 ... N
) ) )  ->  Q  =/=  P )
83 eldifi 3374 . . . . . . . . . . . . . . . . . . 19  |-  ( P  e.  ( Prime  \  {
2 } )  ->  P  e.  Prime )
842, 83syl 15 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  P  e.  Prime )
8584adantr 451 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( x  e.  ( 1 ... M
)  /\  y  e.  ( 1 ... N
) ) )  ->  P  e.  Prime )
86 prmrp 12871 . . . . . . . . . . . . . . . . 17  |-  ( ( Q  e.  Prime  /\  P  e.  Prime )  ->  (
( Q  gcd  P
)  =  1  <->  Q  =/=  P ) )
8751, 85, 86syl2anc 642 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( x  e.  ( 1 ... M
)  /\  y  e.  ( 1 ... N
) ) )  -> 
( ( Q  gcd  P )  =  1  <->  Q  =/=  P ) )
8882, 87mpbird 223 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( x  e.  ( 1 ... M
)  /\  y  e.  ( 1 ... N
) ) )  -> 
( Q  gcd  P
)  =  1 )
89 prmz 12853 . . . . . . . . . . . . . . . . 17  |-  ( P  e.  Prime  ->  P  e.  ZZ )
9085, 89syl 15 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( x  e.  ( 1 ... M
)  /\  y  e.  ( 1 ... N
) ) )  ->  P  e.  ZZ )
91 elfzelz 10887 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  ( 1 ... N )  ->  y  e.  ZZ )
9291ad2antll 709 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( x  e.  ( 1 ... M
)  /\  y  e.  ( 1 ... N
) ) )  -> 
y  e.  ZZ )
93 coprmdvds 12872 . . . . . . . . . . . . . . . 16  |-  ( ( Q  e.  ZZ  /\  P  e.  ZZ  /\  y  e.  ZZ )  ->  (
( Q  ||  ( P  x.  y )  /\  ( Q  gcd  P
)  =  1 )  ->  Q  ||  y
) )
9460, 90, 92, 93syl3anc 1182 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( x  e.  ( 1 ... M
)  /\  y  e.  ( 1 ... N
) ) )  -> 
( ( Q  ||  ( P  x.  y
)  /\  ( Q  gcd  P )  =  1 )  ->  Q  ||  y
) )
9588, 94mpan2d 655 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( x  e.  ( 1 ... M
)  /\  y  e.  ( 1 ... N
) ) )  -> 
( Q  ||  ( P  x.  y )  ->  Q  ||  y ) )
9681, 95mtod 168 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( x  e.  ( 1 ... M
)  /\  y  e.  ( 1 ... N
) ) )  ->  -.  Q  ||  ( P  x.  y ) )
97 prmnn 12852 . . . . . . . . . . . . . . . . 17  |-  ( P  e.  Prime  ->  P  e.  NN )
9885, 97syl 15 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( x  e.  ( 1 ... M
)  /\  y  e.  ( 1 ... N
) ) )  ->  P  e.  NN )
9998nncnd 9849 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( x  e.  ( 1 ... M
)  /\  y  e.  ( 1 ... N
) ) )  ->  P  e.  CC )
100 elfznn 10908 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  ( 1 ... N )  ->  y  e.  NN )
101100ad2antll 709 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( x  e.  ( 1 ... M
)  /\  y  e.  ( 1 ... N
) ) )  -> 
y  e.  NN )
102101nncnd 9849 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( x  e.  ( 1 ... M
)  /\  y  e.  ( 1 ... N
) ) )  -> 
y  e.  CC )
10399, 102mulcomd 8943 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( x  e.  ( 1 ... M
)  /\  y  e.  ( 1 ... N
) ) )  -> 
( P  x.  y
)  =  ( y  x.  P ) )
104103breq2d 4114 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( x  e.  ( 1 ... M
)  /\  y  e.  ( 1 ... N
) ) )  -> 
( Q  ||  ( P  x.  y )  <->  Q 
||  ( y  x.  P ) ) )
10596, 104mtbid 291 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( x  e.  ( 1 ... M
)  /\  y  e.  ( 1 ... N
) ) )  ->  -.  Q  ||  ( y  x.  P ) )
106 elfzelz 10887 . . . . . . . . . . . . . . . 16  |-  ( x  e.  ( 1 ... M )  ->  x  e.  ZZ )
107106ad2antrl 708 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( x  e.  ( 1 ... M
)  /\  y  e.  ( 1 ... N
) ) )  ->  x  e.  ZZ )
108 dvdsmul2 12642 . . . . . . . . . . . . . . 15  |-  ( ( x  e.  ZZ  /\  Q  e.  ZZ )  ->  Q  ||  ( x  x.  Q ) )
109107, 60, 108syl2anc 642 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( x  e.  ( 1 ... M
)  /\  y  e.  ( 1 ... N
) ) )  ->  Q  ||  ( x  x.  Q ) )
110 breq2 4106 . . . . . . . . . . . . . 14  |-  ( ( x  x.  Q )  =  ( y  x.  P )  ->  ( Q  ||  ( x  x.  Q )  <->  Q  ||  (
y  x.  P ) ) )
111109, 110syl5ibcom 211 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( x  e.  ( 1 ... M
)  /\  y  e.  ( 1 ... N
) ) )  -> 
( ( x  x.  Q )  =  ( y  x.  P )  ->  Q  ||  (
y  x.  P ) ) )
112111necon3bd 2558 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( x  e.  ( 1 ... M
)  /\  y  e.  ( 1 ... N
) ) )  -> 
( -.  Q  ||  ( y  x.  P
)  ->  ( x  x.  Q )  =/=  (
y  x.  P ) ) )
113105, 112mpd 14 . . . . . . . . . . 11  |-  ( (
ph  /\  ( x  e.  ( 1 ... M
)  /\  y  e.  ( 1 ... N
) ) )  -> 
( x  x.  Q
)  =/=  ( y  x.  P ) )
114 elfznn 10908 . . . . . . . . . . . . . . 15  |-  ( x  e.  ( 1 ... M )  ->  x  e.  NN )
115114ad2antrl 708 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( x  e.  ( 1 ... M
)  /\  y  e.  ( 1 ... N
) ) )  ->  x  e.  NN )
116115, 53nnmulcld 9880 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( x  e.  ( 1 ... M
)  /\  y  e.  ( 1 ... N
) ) )  -> 
( x  x.  Q
)  e.  NN )
117116nnred 9848 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( x  e.  ( 1 ... M
)  /\  y  e.  ( 1 ... N
) ) )  -> 
( x  x.  Q
)  e.  RR )
118101, 98nnmulcld 9880 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( x  e.  ( 1 ... M
)  /\  y  e.  ( 1 ... N
) ) )  -> 
( y  x.  P
)  e.  NN )
119118nnred 9848 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( x  e.  ( 1 ... M
)  /\  y  e.  ( 1 ... N
) ) )  -> 
( y  x.  P
)  e.  RR )
120117, 119lttri2d 9045 . . . . . . . . . . 11  |-  ( (
ph  /\  ( x  e.  ( 1 ... M
)  /\  y  e.  ( 1 ... N
) ) )  -> 
( ( x  x.  Q )  =/=  (
y  x.  P )  <-> 
( ( x  x.  Q )  <  (
y  x.  P )  \/  ( y  x.  P )  <  (
x  x.  Q ) ) ) )
121113, 120mpbid 201 . . . . . . . . . 10  |-  ( (
ph  /\  ( x  e.  ( 1 ... M
)  /\  y  e.  ( 1 ... N
) ) )  -> 
( ( x  x.  Q )  <  (
y  x.  P )  \/  ( y  x.  P )  <  (
x  x.  Q ) ) )
122121ex 423 . . . . . . . . 9  |-  ( ph  ->  ( ( x  e.  ( 1 ... M
)  /\  y  e.  ( 1 ... N
) )  ->  (
( x  x.  Q
)  <  ( y  x.  P )  \/  (
y  x.  P )  <  ( x  x.  Q ) ) ) )
123122pm4.71rd 616 . . . . . . . 8  |-  ( ph  ->  ( ( x  e.  ( 1 ... M
)  /\  y  e.  ( 1 ... N
) )  <->  ( (
( x  x.  Q
)  <  ( y  x.  P )  \/  (
y  x.  P )  <  ( x  x.  Q ) )  /\  ( x  e.  (
1 ... M )  /\  y  e.  ( 1 ... N ) ) ) ) )
124 ancom 437 . . . . . . . 8  |-  ( ( ( ( x  x.  Q )  <  (
y  x.  P )  \/  ( y  x.  P )  <  (
x  x.  Q ) )  /\  ( x  e.  ( 1 ... M )  /\  y  e.  ( 1 ... N
) ) )  <->  ( (
x  e.  ( 1 ... M )  /\  y  e.  ( 1 ... N ) )  /\  ( ( x  x.  Q )  < 
( y  x.  P
)  \/  ( y  x.  P )  < 
( x  x.  Q
) ) ) )
125123, 124syl6rbb 253 . . . . . . 7  |-  ( ph  ->  ( ( ( x  e.  ( 1 ... M )  /\  y  e.  ( 1 ... N
) )  /\  (
( x  x.  Q
)  <  ( y  x.  P )  \/  (
y  x.  P )  <  ( x  x.  Q ) ) )  <-> 
( x  e.  ( 1 ... M )  /\  y  e.  ( 1 ... N ) ) ) )
126125opabbidv 4161 . . . . . 6  |-  ( ph  ->  { <. x ,  y
>.  |  ( (
x  e.  ( 1 ... M )  /\  y  e.  ( 1 ... N ) )  /\  ( ( x  x.  Q )  < 
( y  x.  P
)  \/  ( y  x.  P )  < 
( x  x.  Q
) ) ) }  =  { <. x ,  y >.  |  ( x  e.  ( 1 ... M )  /\  y  e.  ( 1 ... N ) ) } )
127 unopab 4174 . . . . . . 7  |-  ( {
<. x ,  y >.  |  ( ( x  e.  ( 1 ... M )  /\  y  e.  ( 1 ... N
) )  /\  (
x  x.  Q )  <  ( y  x.  P ) ) }  u.  { <. x ,  y >.  |  ( ( x  e.  ( 1 ... M )  /\  y  e.  ( 1 ... N ) )  /\  ( y  x.  P )  < 
( x  x.  Q
) ) } )  =  { <. x ,  y >.  |  ( ( ( x  e.  ( 1 ... M
)  /\  y  e.  ( 1 ... N
) )  /\  (
x  x.  Q )  <  ( y  x.  P ) )  \/  ( ( x  e.  ( 1 ... M
)  /\  y  e.  ( 1 ... N
) )  /\  (
y  x.  P )  <  ( x  x.  Q ) ) ) }
12835uneq2i 3402 . . . . . . 7  |-  ( {
<. x ,  y >.  |  ( ( x  e.  ( 1 ... M )  /\  y  e.  ( 1 ... N
) )  /\  (
x  x.  Q )  <  ( y  x.  P ) ) }  u.  S )  =  ( { <. x ,  y >.  |  ( ( x  e.  ( 1 ... M )  /\  y  e.  ( 1 ... N ) )  /\  ( x  x.  Q )  < 
( y  x.  P
) ) }  u.  {
<. x ,  y >.  |  ( ( x  e.  ( 1 ... M )  /\  y  e.  ( 1 ... N
) )  /\  (
y  x.  P )  <  ( x  x.  Q ) ) } )
129 andi 837 . . . . . . . 8  |-  ( ( ( x  e.  ( 1 ... M )  /\  y  e.  ( 1 ... N ) )  /\  ( ( x  x.  Q )  <  ( y  x.  P )  \/  (
y  x.  P )  <  ( x  x.  Q ) ) )  <-> 
( ( ( x  e.  ( 1 ... M )  /\  y  e.  ( 1 ... N
) )  /\  (
x  x.  Q )  <  ( y  x.  P ) )  \/  ( ( x  e.  ( 1 ... M
)  /\  y  e.  ( 1 ... N
) )  /\  (
y  x.  P )  <  ( x  x.  Q ) ) ) )
130129opabbii 4162 . . . . . . 7  |-  { <. x ,  y >.  |  ( ( x  e.  ( 1 ... M )  /\  y  e.  ( 1 ... N ) )  /\  ( ( x  x.  Q )  <  ( y  x.  P )  \/  (
y  x.  P )  <  ( x  x.  Q ) ) ) }  =  { <. x ,  y >.  |  ( ( ( x  e.  ( 1 ... M
)  /\  y  e.  ( 1 ... N
) )  /\  (
x  x.  Q )  <  ( y  x.  P ) )  \/  ( ( x  e.  ( 1 ... M
)  /\  y  e.  ( 1 ... N
) )  /\  (
y  x.  P )  <  ( x  x.  Q ) ) ) }
131127, 128, 1303eqtr4i 2388 . . . . . 6  |-  ( {
<. x ,  y >.  |  ( ( x  e.  ( 1 ... M )  /\  y  e.  ( 1 ... N
) )  /\  (
x  x.  Q )  <  ( y  x.  P ) ) }  u.  S )  =  { <. x ,  y
>.  |  ( (
x  e.  ( 1 ... M )  /\  y  e.  ( 1 ... N ) )  /\  ( ( x  x.  Q )  < 
( y  x.  P
)  \/  ( y  x.  P )  < 
( x  x.  Q
) ) ) }
132 df-xp 4774 . . . . . 6  |-  ( ( 1 ... M )  X.  ( 1 ... N ) )  =  { <. x ,  y
>.  |  ( x  e.  ( 1 ... M
)  /\  y  e.  ( 1 ... N
) ) }
133126, 131, 1323eqtr4g 2415 . . . . 5  |-  ( ph  ->  ( { <. x ,  y >.  |  ( ( x  e.  ( 1 ... M )  /\  y  e.  ( 1 ... N ) )  /\  ( x  x.  Q )  < 
( y  x.  P
) ) }  u.  S )  =  ( ( 1 ... M
)  X.  ( 1 ... N ) ) )
134133fveq2d 5609 . . . 4  |-  ( ph  ->  ( # `  ( { <. x ,  y
>.  |  ( (
x  e.  ( 1 ... M )  /\  y  e.  ( 1 ... N ) )  /\  ( x  x.  Q )  <  (
y  x.  P ) ) }  u.  S
) )  =  (
# `  ( (
1 ... M )  X.  ( 1 ... N
) ) ) )
135 inopab 4895 . . . . . . 7  |-  ( {
<. x ,  y >.  |  ( ( x  e.  ( 1 ... M )  /\  y  e.  ( 1 ... N
) )  /\  (
x  x.  Q )  <  ( y  x.  P ) ) }  i^i  { <. x ,  y >.  |  ( ( x  e.  ( 1 ... M )  /\  y  e.  ( 1 ... N ) )  /\  ( y  x.  P )  < 
( x  x.  Q
) ) } )  =  { <. x ,  y >.  |  ( ( ( x  e.  ( 1 ... M
)  /\  y  e.  ( 1 ... N
) )  /\  (
x  x.  Q )  <  ( y  x.  P ) )  /\  ( ( x  e.  ( 1 ... M
)  /\  y  e.  ( 1 ... N
) )  /\  (
y  x.  P )  <  ( x  x.  Q ) ) ) }
13635ineq2i 3443 . . . . . . 7  |-  ( {
<. x ,  y >.  |  ( ( x  e.  ( 1 ... M )  /\  y  e.  ( 1 ... N
) )  /\  (
x  x.  Q )  <  ( y  x.  P ) ) }  i^i  S )  =  ( { <. x ,  y >.  |  ( ( x  e.  ( 1 ... M )  /\  y  e.  ( 1 ... N ) )  /\  ( x  x.  Q )  < 
( y  x.  P
) ) }  i^i  {
<. x ,  y >.  |  ( ( x  e.  ( 1 ... M )  /\  y  e.  ( 1 ... N
) )  /\  (
y  x.  P )  <  ( x  x.  Q ) ) } )
137 anandi 801 . . . . . . . 8  |-  ( ( ( x  e.  ( 1 ... M )  /\  y  e.  ( 1 ... N ) )  /\  ( ( x  x.  Q )  <  ( y  x.  P )  /\  (
y  x.  P )  <  ( x  x.  Q ) ) )  <-> 
( ( ( x  e.  ( 1 ... M )  /\  y  e.  ( 1 ... N
) )  /\  (
x  x.  Q )  <  ( y  x.  P ) )  /\  ( ( x  e.  ( 1 ... M
)  /\  y  e.  ( 1 ... N
) )  /\  (
y  x.  P )  <  ( x  x.  Q ) ) ) )
138137opabbii 4162 . . . . . . 7  |-  { <. x ,  y >.  |  ( ( x  e.  ( 1 ... M )  /\  y  e.  ( 1 ... N ) )  /\  ( ( x  x.  Q )  <  ( y  x.  P )  /\  (
y  x.  P )  <  ( x  x.  Q ) ) ) }  =  { <. x ,  y >.  |  ( ( ( x  e.  ( 1 ... M
)  /\  y  e.  ( 1 ... N
) )  /\  (
x  x.  Q )  <  ( y  x.  P ) )  /\  ( ( x  e.  ( 1 ... M
)  /\  y  e.  ( 1 ... N
) )  /\  (
y  x.  P )  <  ( x  x.  Q ) ) ) }
139135, 136, 1383eqtr4i 2388 . . . . . 6  |-  ( {
<. x ,  y >.  |  ( ( x  e.  ( 1 ... M )  /\  y  e.  ( 1 ... N
) )  /\  (
x  x.  Q )  <  ( y  x.  P ) ) }  i^i  S )  =  { <. x ,  y
>.  |  ( (
x  e.  ( 1 ... M )  /\  y  e.  ( 1 ... N ) )  /\  ( ( x  x.  Q )  < 
( y  x.  P
)  /\  ( y  x.  P )  <  (
x  x.  Q ) ) ) }
140 ltnsym2 9007 . . . . . . . . . . . 12  |-  ( ( ( x  x.  Q
)  e.  RR  /\  ( y  x.  P
)  e.  RR )  ->  -.  ( (
x  x.  Q )  <  ( y  x.  P )  /\  (
y  x.  P )  <  ( x  x.  Q ) ) )
141117, 119, 140syl2anc 642 . . . . . . . . . . 11  |-  ( (
ph  /\  ( x  e.  ( 1 ... M
)  /\  y  e.  ( 1 ... N
) ) )  ->  -.  ( ( x  x.  Q )  <  (
y  x.  P )  /\  ( y  x.  P )  <  (
x  x.  Q ) ) )
142141ex 423 . . . . . . . . . 10  |-  ( ph  ->  ( ( x  e.  ( 1 ... M
)  /\  y  e.  ( 1 ... N
) )  ->  -.  ( ( x  x.  Q )  <  (
y  x.  P )  /\  ( y  x.  P )  <  (
x  x.  Q ) ) ) )
143 imnan 411 . . . . . . . . . 10  |-  ( ( ( x  e.  ( 1 ... M )  /\  y  e.  ( 1 ... N ) )  ->  -.  (
( x  x.  Q
)  <  ( y  x.  P )  /\  (
y  x.  P )  <  ( x  x.  Q ) ) )  <->  -.  ( ( x  e.  ( 1 ... M
)  /\  y  e.  ( 1 ... N
) )  /\  (
( x  x.  Q
)  <  ( y  x.  P )  /\  (
y  x.  P )  <  ( x  x.  Q ) ) ) )
144142, 143sylib 188 . . . . . . . . 9  |-  ( ph  ->  -.  ( ( x  e.  ( 1 ... M )  /\  y  e.  ( 1 ... N
) )  /\  (
( x  x.  Q
)  <  ( y  x.  P )  /\  (
y  x.  P )  <  ( x  x.  Q ) ) ) )
145144nexdv 1921 . . . . . . . 8  |-  ( ph  ->  -.  E. y ( ( x  e.  ( 1 ... M )  /\  y  e.  ( 1 ... N ) )  /\  ( ( x  x.  Q )  <  ( y  x.  P )  /\  (
y  x.  P )  <  ( x  x.  Q ) ) ) )
146145nexdv 1921 . . . . . . 7  |-  ( ph  ->  -.  E. x E. y ( ( x  e.  ( 1 ... M )  /\  y  e.  ( 1 ... N
) )  /\  (
( x  x.  Q
)  <  ( y  x.  P )  /\  (
y  x.  P )  <  ( x  x.  Q ) ) ) )
147 opabn0 4374 . . . . . . . 8  |-  ( {
<. x ,  y >.  |  ( ( x  e.  ( 1 ... M )  /\  y  e.  ( 1 ... N
) )  /\  (
( x  x.  Q
)  <  ( y  x.  P )  /\  (
y  x.  P )  <  ( x  x.  Q ) ) ) }  =/=  (/)  <->  E. x E. y ( ( x  e.  ( 1 ... M )  /\  y  e.  ( 1 ... N
) )  /\  (
( x  x.  Q
)  <  ( y  x.  P )  /\  (
y  x.  P )  <  ( x  x.  Q ) ) ) )
148147necon1bbii 2573 . . . . . . 7  |-  ( -. 
E. x E. y
( ( x  e.  ( 1 ... M
)  /\  y  e.  ( 1 ... N
) )  /\  (
( x  x.  Q
)  <  ( y  x.  P )  /\  (
y  x.  P )  <  ( x  x.  Q ) ) )  <->  { <. x ,  y
>.  |  ( (
x  e.  ( 1 ... M )  /\  y  e.  ( 1 ... N ) )  /\  ( ( x  x.  Q )  < 
( y  x.  P
)  /\  ( y  x.  P )  <  (
x  x.  Q ) ) ) }  =  (/) )
149146, 148sylib 188 . . . . . 6  |-  ( ph  ->  { <. x ,  y
>.  |  ( (
x  e.  ( 1 ... M )  /\  y  e.  ( 1 ... N ) )  /\  ( ( x  x.  Q )  < 
( y  x.  P
)  /\  ( y  x.  P )  <  (
x  x.  Q ) ) ) }  =  (/) )
150139, 149syl5eq 2402 . . . . 5  |-  ( ph  ->  ( { <. x ,  y >.  |  ( ( x  e.  ( 1 ... M )  /\  y  e.  ( 1 ... N ) )  /\  ( x  x.  Q )  < 
( y  x.  P
) ) }  i^i  S )  =  (/) )
151 hashun 11454 . . . . 5  |-  ( ( { <. x ,  y
>.  |  ( (
x  e.  ( 1 ... M )  /\  y  e.  ( 1 ... N ) )  /\  ( x  x.  Q )  <  (
y  x.  P ) ) }  e.  Fin  /\  S  e.  Fin  /\  ( { <. x ,  y
>.  |  ( (
x  e.  ( 1 ... M )  /\  y  e.  ( 1 ... N ) )  /\  ( x  x.  Q )  <  (
y  x.  P ) ) }  i^i  S
)  =  (/) )  -> 
( # `  ( {
<. x ,  y >.  |  ( ( x  e.  ( 1 ... M )  /\  y  e.  ( 1 ... N
) )  /\  (
x  x.  Q )  <  ( y  x.  P ) ) }  u.  S ) )  =  ( ( # `  { <. x ,  y
>.  |  ( (
x  e.  ( 1 ... M )  /\  y  e.  ( 1 ... N ) )  /\  ( x  x.  Q )  <  (
y  x.  P ) ) } )  +  ( # `  S
) ) )
15226, 43, 150, 151syl3anc 1182 . . . 4  |-  ( ph  ->  ( # `  ( { <. x ,  y
>.  |  ( (
x  e.  ( 1 ... M )  /\  y  e.  ( 1 ... N ) )  /\  ( x  x.  Q )  <  (
y  x.  P ) ) }  u.  S
) )  =  ( ( # `  { <. x ,  y >.  |  ( ( x  e.  ( 1 ... M )  /\  y  e.  ( 1 ... N
) )  /\  (
x  x.  Q )  <  ( y  x.  P ) ) } )  +  ( # `  S ) ) )
153 hashxp 11476 . . . . . 6  |-  ( ( ( 1 ... M
)  e.  Fin  /\  ( 1 ... N
)  e.  Fin )  ->  ( # `  (
( 1 ... M
)  X.  ( 1 ... N ) ) )  =  ( (
# `  ( 1 ... M ) )  x.  ( # `  (
1 ... N ) ) ) )
15420, 21, 153syl2anc 642 . . . . 5  |-  ( ph  ->  ( # `  (
( 1 ... M
)  X.  ( 1 ... N ) ) )  =  ( (
# `  ( 1 ... M ) )  x.  ( # `  (
1 ... N ) ) ) )
155 oddprm 12959 . . . . . . . . . 10  |-  ( P  e.  ( Prime  \  {
2 } )  -> 
( ( P  - 
1 )  /  2
)  e.  NN )
1562, 155syl 15 . . . . . . . . 9  |-  ( ph  ->  ( ( P  - 
1 )  /  2
)  e.  NN )
1576, 156syl5eqel 2442 . . . . . . . 8  |-  ( ph  ->  M  e.  NN )
158157nnnn0d 10107 . . . . . . 7  |-  ( ph  ->  M  e.  NN0 )
159 hashfz1 11435 . . . . . . 7  |-  ( M  e.  NN0  ->  ( # `  ( 1 ... M
) )  =  M )
160158, 159syl 15 . . . . . 6  |-  ( ph  ->  ( # `  (
1 ... M ) )  =  M )
16156nnnn0d 10107 . . . . . . 7  |-  ( ph  ->  N  e.  NN0 )
162 hashfz1 11435 . . . . . . 7  |-  ( N  e.  NN0  ->  ( # `  ( 1 ... N
) )  =  N )
163161, 162syl 15 . . . . . 6  |-  ( ph  ->  ( # `  (
1 ... N ) )  =  N )
164160, 163oveq12d 5960 . . . . 5  |-  ( ph  ->  ( ( # `  (
1 ... M ) )  x.  ( # `  (
1 ... N ) ) )  =  ( M  x.  N ) )
165154, 164eqtrd 2390 . . . 4  |-  ( ph  ->  ( # `  (
( 1 ... M
)  X.  ( 1 ... N ) ) )  =  ( M  x.  N ) )
166134, 152, 1653eqtr3d 2398 . . 3  |-  ( ph  ->  ( ( # `  { <. x ,  y >.  |  ( ( x  e.  ( 1 ... M )  /\  y  e.  ( 1 ... N
) )  /\  (
x  x.  Q )  <  ( y  x.  P ) ) } )  +  ( # `  S ) )  =  ( M  x.  N
) )
167166oveq2d 5958 . 2  |-  ( ph  ->  ( -u 1 ^ ( ( # `  { <. x ,  y >.  |  ( ( x  e.  ( 1 ... M )  /\  y  e.  ( 1 ... N
) )  /\  (
x  x.  Q )  <  ( y  x.  P ) ) } )  +  ( # `  S ) ) )  =  ( -u 1 ^ ( M  x.  N ) ) )
16837, 48, 1673eqtr2d 2396 1  |-  ( ph  ->  ( ( P  / L Q )  x.  ( Q  / L P ) )  =  ( -u
1 ^ ( M  x.  N ) ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 176    \/ wo 357    /\ wa 358   E.wex 1541    = wceq 1642    e. wcel 1710    =/= wne 2521    \ cdif 3225    u. cun 3226    i^i cin 3227    C_ wss 3228   (/)c0 3531   {csn 3716   class class class wbr 4102   {copab 4155    X. cxp 4766   `'ccnv 4767   Rel wrel 4773   ` cfv 5334  (class class class)co 5942    ~~ cen 6945   Fincfn 6948   CCcc 8822   RRcr 8823   1c1 8825    + caddc 8827    x. cmul 8829    < clt 8954    <_ cle 8955    - cmin 9124   -ucneg 9125    / cdiv 9510   NNcn 9833   2c2 9882   NN0cn0 10054   ZZcz 10113   ZZ>=cuz 10319   RR+crp 10443   ...cfz 10871   ^cexp 11194   #chash 11427    || cdivides 12622    gcd cgcd 12776   Primecprime 12849    / Lclgs 20639
This theorem is referenced by:  lgsquad  20702
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-13 1712  ax-14 1714  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339  ax-rep 4210  ax-sep 4220  ax-nul 4228  ax-pow 4267  ax-pr 4293  ax-un 4591  ax-inf2 7429  ax-cnex 8880  ax-resscn 8881  ax-1cn 8882  ax-icn 8883  ax-addcl 8884  ax-addrcl 8885  ax-mulcl 8886  ax-mulrcl 8887  ax-mulcom 8888  ax-addass 8889  ax-mulass 8890  ax-distr 8891  ax-i2m1 8892  ax-1ne0 8893  ax-1rid 8894  ax-rnegex 8895  ax-rrecex 8896  ax-cnre 8897  ax-pre-lttri 8898  ax-pre-lttrn 8899  ax-pre-ltadd 8900  ax-pre-mulgt0 8901  ax-pre-sup 8902  ax-addf 8903  ax-mulf 8904
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-eu 2213  df-mo 2214  df-clab 2345  df-cleq 2351  df-clel 2354  df-nfc 2483  df-ne 2523  df-nel 2524  df-ral 2624  df-rex 2625  df-reu 2626  df-rmo 2627  df-rab 2628  df-v 2866  df-sbc 3068  df-csb 3158  df-dif 3231  df-un 3233  df-in 3235  df-ss 3242  df-pss 3244  df-nul 3532  df-if 3642  df-pw 3703  df-sn 3722  df-pr 3723  df-tp 3724  df-op 3725  df-uni 3907  df-int 3942  df-iun 3986  df-disj 4073  df-br 4103  df-opab 4157  df-mpt 4158  df-tr 4193  df-eprel 4384  df-id 4388  df-po 4393  df-so 4394  df-fr 4431  df-se 4432  df-we 4433  df-ord 4474  df-on 4475  df-lim 4476  df-suc 4477  df-om 4736  df-xp 4774  df-rel 4775  df-cnv 4776  df-co 4777  df-dm 4778  df-rn 4779  df-res 4780  df-ima 4781  df-iota 5298  df-fun 5336  df-fn 5337  df-f 5338  df-f1 5339  df-fo 5340  df-f1o 5341  df-fv 5342  df-isom 5343  df-ov 5945  df-oprab 5946  df-mpt2 5947  df-of 6162  df-1st 6206  df-2nd 6207  df-tpos 6318  df-riota 6388  df-recs 6472  df-rdg 6507  df-1o 6563  df-2o 6564  df-oadd 6567  df-er 6744  df-ec 6746  df-qs 6750  df-map 6859  df-en 6949  df-dom 6950  df-sdom 6951  df-fin 6952  df-sup 7281  df-oi 7312  df-card 7659  df-cda 7881  df-pnf 8956  df-mnf 8957  df-xr 8958  df-ltxr 8959  df-le 8960  df-sub 9126  df-neg 9127  df-div 9511  df-nn 9834  df-2 9891  df-3 9892  df-4 9893  df-5 9894  df-6 9895  df-7 9896  df-8 9897  df-9 9898  df-10 9899  df-n0 10055  df-z 10114  df-dec 10214  df-uz 10320  df-q 10406  df-rp 10444  df-fz 10872  df-fzo 10960  df-fl 11014  df-mod 11063  df-seq 11136  df-exp 11195  df-hash 11428  df-cj 11674  df-re 11675  df-im 11676  df-sqr 11810  df-abs 11811  df-clim 12052  df-sum 12250  df-dvds 12623  df-gcd 12777  df-prm 12850  df-phi 12925  df-pc 12981  df-struct 13241  df-ndx 13242  df-slot 13243  df-base 13244  df-sets 13245  df-ress 13246  df-plusg 13312  df-mulr 13313  df-starv 13314  df-sca 13315  df-vsca 13316  df-tset 13318  df-ple 13319  df-ds 13321  df-unif 13322  df-0g 13497  df-gsum 13498  df-imas 13504  df-divs 13505  df-mnd 14460  df-mhm 14508  df-submnd 14509  df-grp 14582  df-minusg 14583  df-sbg 14584  df-mulg 14585  df-subg 14711  df-nsg 14712  df-eqg 14713  df-ghm 14774  df-cntz 14886  df-cmn 15184  df-abl 15185  df-mgp 15419  df-rng 15433  df-cring 15434  df-ur 15435  df-oppr 15498  df-dvdsr 15516  df-unit 15517  df-invr 15547  df-dvr 15558  df-rnghom 15589  df-drng 15607  df-field 15608  df-subrg 15636  df-lmod 15722  df-lss 15783  df-lsp 15822  df-sra 16018  df-rgmod 16019  df-lidl 16020  df-rsp 16021  df-2idl 16077  df-nzr 16103  df-rlreg 16117  df-domn 16118  df-idom 16119  df-cnfld 16477  df-zrh 16555  df-zn 16558  df-lgs 20640
  Copyright terms: Public domain W3C validator