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 syl5eq
 |-  ( 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 ) ) )