Metamath Proof Explorer

Theorem lgsquadlem3

Description: Lemma for lgsquad . (Contributed by Mario Carneiro, 18-Jun-2015)

Ref Expression
Hypotheses 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 lgsquadlem3 
|- ( ph -> ( ( P /L Q ) x. ( Q /L P ) ) = ( -u 1 ^ ( M x. N ) ) )

Proof

Step Hyp Ref Expression
1 lgseisen.1 
 |-  ( ph -> P e. ( Prime \ { 2 } ) )
2 lgseisen.2 
 |-  ( ph -> Q e. ( Prime \ { 2 } ) )
3 lgseisen.3 
 |-  ( ph -> P =/= Q )
4 lgsquad.4 
 |-  M = ( ( P - 1 ) / 2 )
5 lgsquad.5 
 |-  N = ( ( Q - 1 ) / 2 )
6 lgsquad.6 
 |-  S = { <. x , y >. | ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( y x. P ) < ( x x. Q ) ) }
7 3 necomd 
 |-  ( ph -> Q =/= P )
8 eleq1w 
 |-  ( x = z -> ( x e. ( 1 ... M ) <-> z e. ( 1 ... M ) ) )
9 eleq1w 
 |-  ( y = w -> ( y e. ( 1 ... N ) <-> w e. ( 1 ... N ) ) )
10 8 9 bi2anan9 
 |-  ( ( x = z /\ y = w ) -> ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) <-> ( z e. ( 1 ... M ) /\ w e. ( 1 ... N ) ) ) )
11 10 biancomd 
 |-  ( ( x = z /\ y = w ) -> ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) <-> ( w e. ( 1 ... N ) /\ z e. ( 1 ... M ) ) ) )
12 oveq1 
 |-  ( x = z -> ( x x. Q ) = ( z x. Q ) )
13 oveq1 
 |-  ( y = w -> ( y x. P ) = ( w x. P ) )
14 12 13 breqan12d 
 |-  ( ( x = z /\ y = w ) -> ( ( x x. Q ) < ( y x. P ) <-> ( z x. Q ) < ( w x. P ) ) )
15 11 14 anbi12d 
 |-  ( ( 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 ) ) ) )
16 15 ancoms 
 |-  ( ( 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 ) ) ) )
17 16 cbvopabv 
 |-  { <. 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 ) ) }
18 2 1 7 5 4 17 lgsquadlem2 
 |-  ( ph -> ( P /L Q ) = ( -u 1 ^ ( # ` { <. y , x >. | ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( x x. Q ) < ( y x. P ) ) } ) ) )
19 relopabv 
 |-  Rel { <. x , y >. | ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( x x. Q ) < ( y x. P ) ) }
20 fzfid 
 |-  ( ph -> ( 1 ... M ) e. Fin )
21 fzfid 
 |-  ( ph -> ( 1 ... N ) e. Fin )
22 xpfi 
 |-  ( ( ( 1 ... M ) e. Fin /\ ( 1 ... N ) e. Fin ) -> ( ( 1 ... M ) X. ( 1 ... N ) ) e. Fin )
23 20 21 22 syl2anc 
 |-  ( ph -> ( ( 1 ... M ) X. ( 1 ... N ) ) e. Fin )
24 opabssxp 
 |-  { <. x , y >. | ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( x x. Q ) < ( y x. P ) ) } C_ ( ( 1 ... M ) X. ( 1 ... N ) )
25 ssfi 
 |-  ( ( ( ( 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 )
26 23 24 25 sylancl 
 |-  ( ph -> { <. x , y >. | ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( x x. Q ) < ( y x. P ) ) } e. Fin )
27 cnven 
 |-  ( ( 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 ) ) } )
28 19 26 27 sylancr 
 |-  ( 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 
 |-  `' { <. 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 ) ) }
30 28 29 breqtrdi 
 |-  ( 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 
 |-  ( { <. 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 ) ) } ) )
32 30 31 syl 
 |-  ( 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 ) ) } ) )
33 32 oveq2d 
 |-  ( 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 ) ) } ) ) )
34 18 33 eqtr4d 
 |-  ( ph -> ( P /L Q ) = ( -u 1 ^ ( # ` { <. x , y >. | ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( x x. Q ) < ( y x. P ) ) } ) ) )
35 1 2 3 4 5 6 lgsquadlem2 
 |-  ( ph -> ( Q /L P ) = ( -u 1 ^ ( # ` S ) ) )
36 34 35 oveq12d 
 |-  ( 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 ) ) ) )
37 neg1cn 
 |-  -u 1 e. CC
38 37 a1i 
 |-  ( ph -> -u 1 e. CC )
39 opabssxp 
 |-  { <. x , y >. | ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( y x. P ) < ( x x. Q ) ) } C_ ( ( 1 ... M ) X. ( 1 ... N ) )
40 6 39 eqsstri 
 |-  S C_ ( ( 1 ... M ) X. ( 1 ... N ) )
41 ssfi 
 |-  ( ( ( ( 1 ... M ) X. ( 1 ... N ) ) e. Fin /\ S C_ ( ( 1 ... M ) X. ( 1 ... N ) ) ) -> S e. Fin )
42 23 40 41 sylancl 
 |-  ( ph -> S e. Fin )
43 hashcl 
 |-  ( S e. Fin -> ( # ` S ) e. NN0 )
44 42 43 syl 
 |-  ( ph -> ( # ` S ) e. NN0 )
45 hashcl 
 |-  ( { <. 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 )
46 26 45 syl 
 |-  ( ph -> ( # ` { <. x , y >. | ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( x x. Q ) < ( y x. P ) ) } ) e. NN0 )
47 38 44 46 expaddd 
 |-  ( 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 ) ) ) )
48 2 eldifad 
 |-  ( ph -> Q e. Prime )
49 48 adantr 
 |-  ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> Q e. Prime )
50 prmnn 
 |-  ( Q e. Prime -> Q e. NN )
51 49 50 syl 
 |-  ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> Q e. NN )
52 2 5 gausslemma2dlem0b 
 |-  ( ph -> N e. NN )
53 52 adantr 
 |-  ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> N e. NN )
54 53 nnzd 
 |-  ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> N e. ZZ )
55 prmz 
 |-  ( Q e. Prime -> Q e. ZZ )
56 49 55 syl 
 |-  ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> Q e. ZZ )
57 peano2zm 
 |-  ( Q e. ZZ -> ( Q - 1 ) e. ZZ )
58 56 57 syl 
 |-  ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> ( Q - 1 ) e. ZZ )
59 53 nnred 
 |-  ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> N e. RR )
60 58 zred 
 |-  ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> ( Q - 1 ) e. RR )
61 prmuz2 
 |-  ( Q e. Prime -> Q e. ( ZZ>= ` 2 ) )
62 49 61 syl 
 |-  ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> Q e. ( ZZ>= ` 2 ) )
63 uz2m1nn 
 |-  ( Q e. ( ZZ>= ` 2 ) -> ( Q - 1 ) e. NN )
64 62 63 syl 
 |-  ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> ( Q - 1 ) e. NN )
65 64 nnrpd 
 |-  ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> ( Q - 1 ) e. RR+ )
66 rphalflt 
 |-  ( ( Q - 1 ) e. RR+ -> ( ( Q - 1 ) / 2 ) < ( Q - 1 ) )
67 65 66 syl 
 |-  ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> ( ( Q - 1 ) / 2 ) < ( Q - 1 ) )
68 5 67 eqbrtrid 
 |-  ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> N < ( Q - 1 ) )
69 59 60 68 ltled 
 |-  ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> N <_ ( Q - 1 ) )
70 eluz2 
 |-  ( ( Q - 1 ) e. ( ZZ>= ` N ) <-> ( N e. ZZ /\ ( Q - 1 ) e. ZZ /\ N <_ ( Q - 1 ) ) )
71 54 58 69 70 syl3anbrc 
 |-  ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> ( Q - 1 ) e. ( ZZ>= ` N ) )
72 fzss2 
 |-  ( ( Q - 1 ) e. ( ZZ>= ` N ) -> ( 1 ... N ) C_ ( 1 ... ( Q - 1 ) ) )
73 71 72 syl 
 |-  ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> ( 1 ... N ) C_ ( 1 ... ( Q - 1 ) ) )
74 simprr 
 |-  ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> y e. ( 1 ... N ) )
75 73 74 sseldd 
 |-  ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> y e. ( 1 ... ( Q - 1 ) ) )
76 fzm1ndvds 
 |-  ( ( Q e. NN /\ y e. ( 1 ... ( Q - 1 ) ) ) -> -. Q || y )
77 51 75 76 syl2anc 
 |-  ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> -. Q || y )
78 7 adantr 
 |-  ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> Q =/= P )
79 1 eldifad 
 |-  ( ph -> P e. Prime )
80 79 adantr 
 |-  ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> P e. Prime )
81 prmrp 
 |-  ( ( Q e. Prime /\ P e. Prime ) -> ( ( Q gcd P ) = 1 <-> Q =/= P ) )
82 49 80 81 syl2anc 
 |-  ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> ( ( Q gcd P ) = 1 <-> Q =/= P ) )
83 78 82 mpbird 
 |-  ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> ( Q gcd P ) = 1 )
84 prmz 
 |-  ( P e. Prime -> P e. ZZ )
85 80 84 syl 
 |-  ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> P e. ZZ )
86 elfzelz 
 |-  ( y e. ( 1 ... N ) -> y e. ZZ )
87 86 ad2antll 
 |-  ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> y e. ZZ )
88 coprmdvds 
 |-  ( ( Q e. ZZ /\ P e. ZZ /\ y e. ZZ ) -> ( ( Q || ( P x. y ) /\ ( Q gcd P ) = 1 ) -> Q || y ) )
89 56 85 87 88 syl3anc 
 |-  ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> ( ( Q || ( P x. y ) /\ ( Q gcd P ) = 1 ) -> Q || y ) )
90 83 89 mpan2d 
 |-  ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> ( Q || ( P x. y ) -> Q || y ) )
91 77 90 mtod 
 |-  ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> -. Q || ( P x. y ) )
92 prmnn 
 |-  ( P e. Prime -> P e. NN )
93 80 92 syl 
 |-  ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> P e. NN )
94 93 nncnd 
 |-  ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> P e. CC )
95 elfznn 
 |-  ( y e. ( 1 ... N ) -> y e. NN )
96 95 ad2antll 
 |-  ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> y e. NN )
97 96 nncnd 
 |-  ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> y e. CC )
98 94 97 mulcomd 
 |-  ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> ( P x. y ) = ( y x. P ) )
99 98 breq2d 
 |-  ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> ( Q || ( P x. y ) <-> Q || ( y x. P ) ) )
100 91 99 mtbid 
 |-  ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> -. Q || ( y x. P ) )
101 elfzelz 
 |-  ( x e. ( 1 ... M ) -> x e. ZZ )
102 101 ad2antrl 
 |-  ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> x e. ZZ )
103 dvdsmul2 
 |-  ( ( x e. ZZ /\ Q e. ZZ ) -> Q || ( x x. Q ) )
104 102 56 103 syl2anc 
 |-  ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> Q || ( x x. Q ) )
105 breq2 
 |-  ( ( x x. Q ) = ( y x. P ) -> ( Q || ( x x. Q ) <-> Q || ( y x. P ) ) )
106 104 105 syl5ibcom 
 |-  ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> ( ( x x. Q ) = ( y x. P ) -> Q || ( y x. P ) ) )
107 106 necon3bd 
 |-  ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> ( -. Q || ( y x. P ) -> ( x x. Q ) =/= ( y x. P ) ) )
108 100 107 mpd 
 |-  ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> ( x x. Q ) =/= ( y x. P ) )
109 elfznn 
 |-  ( x e. ( 1 ... M ) -> x e. NN )
110 109 ad2antrl 
 |-  ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> x e. NN )
111 110 51 nnmulcld 
 |-  ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> ( x x. Q ) e. NN )
112 111 nnred 
 |-  ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> ( x x. Q ) e. RR )
113 96 93 nnmulcld 
 |-  ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> ( y x. P ) e. NN )
114 113 nnred 
 |-  ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> ( y x. P ) e. RR )
115 112 114 lttri2d 
 |-  ( ( 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 ) ) ) )
116 108 115 mpbid 
 |-  ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> ( ( x x. Q ) < ( y x. P ) \/ ( y x. P ) < ( x x. Q ) ) )
117 116 ex 
 |-  ( ph -> ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) -> ( ( x x. Q ) < ( y x. P ) \/ ( y x. P ) < ( x x. Q ) ) ) )
118 117 pm4.71rd 
 |-  ( 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 ) ) ) ) )
119 ancom 
 |-  ( ( ( ( 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 ) ) ) )
120 118 119 bitr2di 
 |-  ( 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 ) ) ) )
121 120 opabbidv 
 |-  ( 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 ) ) } )
122 unopab 
 |-  ( { <. 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 ) ) ) }
123 6 uneq2i 
 |-  ( { <. 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 ) ) } )
124 andi 
 |-  ( ( ( 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 ) ) ) )
125 124 opabbii 
 |-  { <. 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 ) ) ) }
126 122 123 125 3eqtr4i 
 |-  ( { <. 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 ) ) ) }
127 df-xp 
 |-  ( ( 1 ... M ) X. ( 1 ... N ) ) = { <. x , y >. | ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) }
128 121 126 127 3eqtr4g 
 |-  ( ph -> ( { <. x , y >. | ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( x x. Q ) < ( y x. P ) ) } u. S ) = ( ( 1 ... M ) X. ( 1 ... N ) ) )
129 128 fveq2d 
 |-  ( ph -> ( # ` ( { <. x , y >. | ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( x x. Q ) < ( y x. P ) ) } u. S ) ) = ( # ` ( ( 1 ... M ) X. ( 1 ... N ) ) ) )
130 inopab 
 |-  ( { <. 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 ) ) ) }
131 6 ineq2i 
 |-  ( { <. 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 ) ) } )
132 anandi 
 |-  ( ( ( 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 ) ) ) )
133 132 opabbii 
 |-  { <. 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 ) ) ) }
134 130 131 133 3eqtr4i 
 |-  ( { <. 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 ) ) ) }
135 ltnsym2 
 |-  ( ( ( x x. Q ) e. RR /\ ( y x. P ) e. RR ) -> -. ( ( x x. Q ) < ( y x. P ) /\ ( y x. P ) < ( x x. Q ) ) )
136 112 114 135 syl2anc 
 |-  ( ( ph /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) ) -> -. ( ( x x. Q ) < ( y x. P ) /\ ( y x. P ) < ( x x. Q ) ) )
137 136 ex 
 |-  ( ph -> ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) -> -. ( ( x x. Q ) < ( y x. P ) /\ ( y x. P ) < ( x x. Q ) ) ) )
138 imnan 
 |-  ( ( ( 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 ) ) ) )
139 137 138 sylib 
 |-  ( ph -> -. ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( ( x x. Q ) < ( y x. P ) /\ ( y x. P ) < ( x x. Q ) ) ) )
140 139 nexdv 
 |-  ( ph -> -. E. y ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( ( x x. Q ) < ( y x. P ) /\ ( y x. P ) < ( x x. Q ) ) ) )
141 140 nexdv 
 |-  ( 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 ) ) ) )
142 opabn0 
 |-  ( { <. 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 ) ) ) )
143 142 necon1bbii 
 |-  ( -. 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 ) ) ) } = (/) )
144 141 143 sylib 
 |-  ( ph -> { <. x , y >. | ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( ( x x. Q ) < ( y x. P ) /\ ( y x. P ) < ( x x. Q ) ) ) } = (/) )
145 134 144 eqtrid 
 |-  ( ph -> ( { <. x , y >. | ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( x x. Q ) < ( y x. P ) ) } i^i S ) = (/) )
146 hashun 
 |-  ( ( { <. 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 ) ) )
147 26 42 145 146 syl3anc 
 |-  ( 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 ) ) )
148 hashxp 
 |-  ( ( ( 1 ... M ) e. Fin /\ ( 1 ... N ) e. Fin ) -> ( # ` ( ( 1 ... M ) X. ( 1 ... N ) ) ) = ( ( # ` ( 1 ... M ) ) x. ( # ` ( 1 ... N ) ) ) )
149 20 21 148 syl2anc 
 |-  ( ph -> ( # ` ( ( 1 ... M ) X. ( 1 ... N ) ) ) = ( ( # ` ( 1 ... M ) ) x. ( # ` ( 1 ... N ) ) ) )
150 1 4 gausslemma2dlem0b 
 |-  ( ph -> M e. NN )
151 150 nnnn0d 
 |-  ( ph -> M e. NN0 )
152 hashfz1 
 |-  ( M e. NN0 -> ( # ` ( 1 ... M ) ) = M )
153 151 152 syl 
 |-  ( ph -> ( # ` ( 1 ... M ) ) = M )
154 52 nnnn0d 
 |-  ( ph -> N e. NN0 )
155 hashfz1 
 |-  ( N e. NN0 -> ( # ` ( 1 ... N ) ) = N )
156 154 155 syl 
 |-  ( ph -> ( # ` ( 1 ... N ) ) = N )
157 153 156 oveq12d 
 |-  ( ph -> ( ( # ` ( 1 ... M ) ) x. ( # ` ( 1 ... N ) ) ) = ( M x. N ) )
158 149 157 eqtrd 
 |-  ( ph -> ( # ` ( ( 1 ... M ) X. ( 1 ... N ) ) ) = ( M x. N ) )
159 129 147 158 3eqtr3d 
 |-  ( ph -> ( ( # ` { <. x , y >. | ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( x x. Q ) < ( y x. P ) ) } ) + ( # ` S ) ) = ( M x. N ) )
160 159 oveq2d 
 |-  ( 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 ) ) )
161 36 47 160 3eqtr2d 
 |-  ( ph -> ( ( P /L Q ) x. ( Q /L P ) ) = ( -u 1 ^ ( M x. N ) ) )