Metamath Proof Explorer


Theorem lgsquadlem3

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

Ref Expression
Hypotheses lgseisen.1 φ P 2
lgseisen.2 φ Q 2
lgseisen.3 φ P Q
lgsquad.4 M = P 1 2
lgsquad.5 N = Q 1 2
lgsquad.6 S = x y | x 1 M y 1 N y P < x Q
Assertion lgsquadlem3 φ P / L Q Q / L P = 1 M N

Proof

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