Metamath Proof Explorer


Theorem lgsquad2lem2

Description: Lemma for lgsquad2 . (Contributed by Mario Carneiro, 19-Jun-2015)

Ref Expression
Hypotheses lgsquad2.1 φ M
lgsquad2.2 φ ¬ 2 M
lgsquad2.3 φ N
lgsquad2.4 φ ¬ 2 N
lgsquad2.5 φ M gcd N = 1
lgsquad2lem2.f φ m 2 m gcd N = 1 m / L N N / L m = 1 m 1 2 N 1 2
lgsquad2lem2.s ψ x 1 k x gcd 2 N = 1 x / L N N / L x = 1 x 1 2 N 1 2
Assertion lgsquad2lem2 φ M / L N N / L M = 1 M 1 2 N 1 2

Proof

Step Hyp Ref Expression
1 lgsquad2.1 φ M
2 lgsquad2.2 φ ¬ 2 M
3 lgsquad2.3 φ N
4 lgsquad2.4 φ ¬ 2 N
5 lgsquad2.5 φ M gcd N = 1
6 lgsquad2lem2.f φ m 2 m gcd N = 1 m / L N N / L m = 1 m 1 2 N 1 2
7 lgsquad2lem2.s ψ x 1 k x gcd 2 N = 1 x / L N N / L x = 1 x 1 2 N 1 2
8 2nn 2
9 8 a1i φ 2
10 1 nnzd φ M
11 2z 2
12 gcdcom M 2 M gcd 2 = 2 gcd M
13 10 11 12 sylancl φ M gcd 2 = 2 gcd M
14 2prm 2
15 coprm 2 M ¬ 2 M 2 gcd M = 1
16 14 10 15 sylancr φ ¬ 2 M 2 gcd M = 1
17 2 16 mpbid φ 2 gcd M = 1
18 13 17 eqtrd φ M gcd 2 = 1
19 rpmulgcd M 2 N M gcd 2 = 1 M gcd 2 N = M gcd N
20 1 9 3 18 19 syl31anc φ M gcd 2 N = M gcd N
21 20 5 eqtrd φ M gcd 2 N = 1
22 oveq1 m = 1 m / L N = 1 / L N
23 oveq2 m = 1 N / L m = N / L 1
24 22 23 oveq12d m = 1 m / L N N / L m = 1 / L N N / L 1
25 oveq1 m = 1 m 1 = 1 1
26 1m1e0 1 1 = 0
27 25 26 eqtrdi m = 1 m 1 = 0
28 27 oveq1d m = 1 m 1 2 = 0 2
29 2cn 2
30 2ne0 2 0
31 29 30 div0i 0 2 = 0
32 28 31 eqtrdi m = 1 m 1 2 = 0
33 32 oveq1d m = 1 m 1 2 N 1 2 = 0 N 1 2
34 33 oveq2d m = 1 1 m 1 2 N 1 2 = 1 0 N 1 2
35 24 34 eqeq12d m = 1 m / L N N / L m = 1 m 1 2 N 1 2 1 / L N N / L 1 = 1 0 N 1 2
36 35 imbi2d m = 1 m gcd 2 N = 1 m / L N N / L m = 1 m 1 2 N 1 2 m gcd 2 N = 1 1 / L N N / L 1 = 1 0 N 1 2
37 36 imbi2d m = 1 φ m gcd 2 N = 1 m / L N N / L m = 1 m 1 2 N 1 2 φ m gcd 2 N = 1 1 / L N N / L 1 = 1 0 N 1 2
38 oveq1 m = x m gcd 2 N = x gcd 2 N
39 38 eqeq1d m = x m gcd 2 N = 1 x gcd 2 N = 1
40 oveq1 m = x m / L N = x / L N
41 oveq2 m = x N / L m = N / L x
42 40 41 oveq12d m = x m / L N N / L m = x / L N N / L x
43 oveq1 m = x m 1 = x 1
44 43 oveq1d m = x m 1 2 = x 1 2
45 44 oveq1d m = x m 1 2 N 1 2 = x 1 2 N 1 2
46 45 oveq2d m = x 1 m 1 2 N 1 2 = 1 x 1 2 N 1 2
47 42 46 eqeq12d m = x m / L N N / L m = 1 m 1 2 N 1 2 x / L N N / L x = 1 x 1 2 N 1 2
48 39 47 imbi12d m = x m gcd 2 N = 1 m / L N N / L m = 1 m 1 2 N 1 2 x gcd 2 N = 1 x / L N N / L x = 1 x 1 2 N 1 2
49 48 imbi2d m = x φ m gcd 2 N = 1 m / L N N / L m = 1 m 1 2 N 1 2 φ x gcd 2 N = 1 x / L N N / L x = 1 x 1 2 N 1 2
50 oveq1 m = y m gcd 2 N = y gcd 2 N
51 50 eqeq1d m = y m gcd 2 N = 1 y gcd 2 N = 1
52 oveq1 m = y m / L N = y / L N
53 oveq2 m = y N / L m = N / L y
54 52 53 oveq12d m = y m / L N N / L m = y / L N N / L y
55 oveq1 m = y m 1 = y 1
56 55 oveq1d m = y m 1 2 = y 1 2
57 56 oveq1d m = y m 1 2 N 1 2 = y 1 2 N 1 2
58 57 oveq2d m = y 1 m 1 2 N 1 2 = 1 y 1 2 N 1 2
59 54 58 eqeq12d m = y m / L N N / L m = 1 m 1 2 N 1 2 y / L N N / L y = 1 y 1 2 N 1 2
60 51 59 imbi12d m = y m gcd 2 N = 1 m / L N N / L m = 1 m 1 2 N 1 2 y gcd 2 N = 1 y / L N N / L y = 1 y 1 2 N 1 2
61 60 imbi2d m = y φ m gcd 2 N = 1 m / L N N / L m = 1 m 1 2 N 1 2 φ y gcd 2 N = 1 y / L N N / L y = 1 y 1 2 N 1 2
62 oveq1 m = x y m gcd 2 N = x y gcd 2 N
63 62 eqeq1d m = x y m gcd 2 N = 1 x y gcd 2 N = 1
64 oveq1 m = x y m / L N = x y / L N
65 oveq2 m = x y N / L m = N / L x y
66 64 65 oveq12d m = x y m / L N N / L m = x y / L N N / L x y
67 oveq1 m = x y m 1 = x y 1
68 67 oveq1d m = x y m 1 2 = x y 1 2
69 68 oveq1d m = x y m 1 2 N 1 2 = x y 1 2 N 1 2
70 69 oveq2d m = x y 1 m 1 2 N 1 2 = 1 x y 1 2 N 1 2
71 66 70 eqeq12d m = x y m / L N N / L m = 1 m 1 2 N 1 2 x y / L N N / L x y = 1 x y 1 2 N 1 2
72 63 71 imbi12d m = x y m gcd 2 N = 1 m / L N N / L m = 1 m 1 2 N 1 2 x y gcd 2 N = 1 x y / L N N / L x y = 1 x y 1 2 N 1 2
73 72 imbi2d m = x y φ m gcd 2 N = 1 m / L N N / L m = 1 m 1 2 N 1 2 φ x y gcd 2 N = 1 x y / L N N / L x y = 1 x y 1 2 N 1 2
74 oveq1 m = M m gcd 2 N = M gcd 2 N
75 74 eqeq1d m = M m gcd 2 N = 1 M gcd 2 N = 1
76 oveq1 m = M m / L N = M / L N
77 oveq2 m = M N / L m = N / L M
78 76 77 oveq12d m = M m / L N N / L m = M / L N N / L M
79 oveq1 m = M m 1 = M 1
80 79 oveq1d m = M m 1 2 = M 1 2
81 80 oveq1d m = M m 1 2 N 1 2 = M 1 2 N 1 2
82 81 oveq2d m = M 1 m 1 2 N 1 2 = 1 M 1 2 N 1 2
83 78 82 eqeq12d m = M m / L N N / L m = 1 m 1 2 N 1 2 M / L N N / L M = 1 M 1 2 N 1 2
84 75 83 imbi12d m = M m gcd 2 N = 1 m / L N N / L m = 1 m 1 2 N 1 2 M gcd 2 N = 1 M / L N N / L M = 1 M 1 2 N 1 2
85 84 imbi2d m = M φ m gcd 2 N = 1 m / L N N / L m = 1 m 1 2 N 1 2 φ M gcd 2 N = 1 M / L N N / L M = 1 M 1 2 N 1 2
86 1t1e1 1 1 = 1
87 neg1cn 1
88 exp0 1 1 0 = 1
89 87 88 ax-mp 1 0 = 1
90 86 89 eqtr4i 1 1 = 1 0
91 sq1 1 2 = 1
92 91 oveq1i 1 2 / L N = 1 / L N
93 1z 1
94 ax-1ne0 1 0
95 93 94 pm3.2i 1 1 0
96 3 nnzd φ N
97 1gcd N 1 gcd N = 1
98 96 97 syl φ 1 gcd N = 1
99 lgssq 1 1 0 N 1 gcd N = 1 1 2 / L N = 1
100 95 96 98 99 mp3an2i φ 1 2 / L N = 1
101 92 100 syl5eqr φ 1 / L N = 1
102 91 oveq2i N / L 1 2 = N / L 1
103 1nn 1
104 103 a1i φ 1
105 gcd1 N N gcd 1 = 1
106 96 105 syl φ N gcd 1 = 1
107 lgssq2 N 1 N gcd 1 = 1 N / L 1 2 = 1
108 96 104 106 107 syl3anc φ N / L 1 2 = 1
109 102 108 syl5eqr φ N / L 1 = 1
110 101 109 oveq12d φ 1 / L N N / L 1 = 1 1
111 nnm1nn0 N N 1 0
112 3 111 syl φ N 1 0
113 112 nn0cnd φ N 1
114 113 halfcld φ N 1 2
115 114 mul02d φ 0 N 1 2 = 0
116 115 oveq2d φ 1 0 N 1 2 = 1 0
117 90 110 116 3eqtr4a φ 1 / L N N / L 1 = 1 0 N 1 2
118 117 a1d φ m gcd 2 N = 1 1 / L N N / L 1 = 1 0 N 1 2
119 simprl φ m m gcd 2 N = 1 m
120 prmz m m
121 120 ad2antrl φ m m gcd 2 N = 1 m
122 11 a1i φ m m gcd 2 N = 1 2
123 3 adantr φ m m gcd 2 N = 1 N
124 123 nnzd φ m m gcd 2 N = 1 N
125 zmulcl 2 N 2 N
126 11 124 125 sylancr φ m m gcd 2 N = 1 2 N
127 simprr φ m m gcd 2 N = 1 m gcd 2 N = 1
128 dvdsmul1 2 N 2 2 N
129 11 124 128 sylancr φ m m gcd 2 N = 1 2 2 N
130 rpdvds m 2 2 N m gcd 2 N = 1 2 2 N m gcd 2 = 1
131 121 122 126 127 129 130 syl32anc φ m m gcd 2 N = 1 m gcd 2 = 1
132 prmrp m 2 m gcd 2 = 1 m 2
133 119 14 132 sylancl φ m m gcd 2 N = 1 m gcd 2 = 1 m 2
134 131 133 mpbid φ m m gcd 2 N = 1 m 2
135 eldifsn m 2 m m 2
136 119 134 135 sylanbrc φ m m gcd 2 N = 1 m 2
137 prmnn m m
138 137 ad2antrl φ m m gcd 2 N = 1 m
139 8 a1i φ m m gcd 2 N = 1 2
140 rpmulgcd m 2 N m gcd 2 = 1 m gcd 2 N = m gcd N
141 138 139 123 131 140 syl31anc φ m m gcd 2 N = 1 m gcd 2 N = m gcd N
142 141 127 eqtr3d φ m m gcd 2 N = 1 m gcd N = 1
143 136 142 jca φ m m gcd 2 N = 1 m 2 m gcd N = 1
144 143 6 syldan φ m m gcd 2 N = 1 m / L N N / L m = 1 m 1 2 N 1 2
145 144 exp32 φ m m gcd 2 N = 1 m / L N N / L m = 1 m 1 2 N 1 2
146 145 com12 m φ m gcd 2 N = 1 m / L N N / L m = 1 m 1 2 N 1 2
147 jcab φ x gcd 2 N = 1 x / L N N / L x = 1 x 1 2 N 1 2 y gcd 2 N = 1 y / L N N / L y = 1 y 1 2 N 1 2 φ x gcd 2 N = 1 x / L N N / L x = 1 x 1 2 N 1 2 φ y gcd 2 N = 1 y / L N N / L y = 1 y 1 2 N 1 2
148 simplrl φ x 2 y 2 x y gcd 2 N = 1 x gcd 2 N = 1 x / L N N / L x = 1 x 1 2 N 1 2 y gcd 2 N = 1 y / L N N / L y = 1 y 1 2 N 1 2 x 2
149 eluz2nn x 2 x
150 148 149 syl φ x 2 y 2 x y gcd 2 N = 1 x gcd 2 N = 1 x / L N N / L x = 1 x 1 2 N 1 2 y gcd 2 N = 1 y / L N N / L y = 1 y 1 2 N 1 2 x
151 simplrr φ x 2 y 2 x y gcd 2 N = 1 x gcd 2 N = 1 x / L N N / L x = 1 x 1 2 N 1 2 y gcd 2 N = 1 y / L N N / L y = 1 y 1 2 N 1 2 y 2
152 eluz2nn y 2 y
153 151 152 syl φ x 2 y 2 x y gcd 2 N = 1 x gcd 2 N = 1 x / L N N / L x = 1 x 1 2 N 1 2 y gcd 2 N = 1 y / L N N / L y = 1 y 1 2 N 1 2 y
154 150 153 nnmulcld φ x 2 y 2 x y gcd 2 N = 1 x gcd 2 N = 1 x / L N N / L x = 1 x 1 2 N 1 2 y gcd 2 N = 1 y / L N N / L y = 1 y 1 2 N 1 2 x y
155 n2dvds1 ¬ 2 1
156 96 ad2antrr φ x 2 y 2 x y gcd 2 N = 1 N
157 11 156 128 sylancr φ x 2 y 2 x y gcd 2 N = 1 2 2 N
158 eluzelz x 2 x
159 eluzelz y 2 y
160 158 159 anim12i x 2 y 2 x y
161 160 ad2antlr φ x 2 y 2 x y gcd 2 N = 1 x y
162 zmulcl x y x y
163 161 162 syl φ x 2 y 2 x y gcd 2 N = 1 x y
164 11 156 125 sylancr φ x 2 y 2 x y gcd 2 N = 1 2 N
165 dvdsgcd 2 x y 2 N 2 x y 2 2 N 2 x y gcd 2 N
166 11 163 164 165 mp3an2i φ x 2 y 2 x y gcd 2 N = 1 2 x y 2 2 N 2 x y gcd 2 N
167 157 166 mpan2d φ x 2 y 2 x y gcd 2 N = 1 2 x y 2 x y gcd 2 N
168 simpr φ x 2 y 2 x y gcd 2 N = 1 x y gcd 2 N = 1
169 168 breq2d φ x 2 y 2 x y gcd 2 N = 1 2 x y gcd 2 N 2 1
170 167 169 sylibd φ x 2 y 2 x y gcd 2 N = 1 2 x y 2 1
171 155 170 mtoi φ x 2 y 2 x y gcd 2 N = 1 ¬ 2 x y
172 171 adantrr φ x 2 y 2 x y gcd 2 N = 1 x gcd 2 N = 1 x / L N N / L x = 1 x 1 2 N 1 2 y gcd 2 N = 1 y / L N N / L y = 1 y 1 2 N 1 2 ¬ 2 x y
173 3 ad2antrr φ x 2 y 2 x y gcd 2 N = 1 x gcd 2 N = 1 x / L N N / L x = 1 x 1 2 N 1 2 y gcd 2 N = 1 y / L N N / L y = 1 y 1 2 N 1 2 N
174 4 ad2antrr φ x 2 y 2 x y gcd 2 N = 1 x gcd 2 N = 1 x / L N N / L x = 1 x 1 2 N 1 2 y gcd 2 N = 1 y / L N N / L y = 1 y 1 2 N 1 2 ¬ 2 N
175 dvdsmul2 2 N N 2 N
176 11 156 175 sylancr φ x 2 y 2 x y gcd 2 N = 1 N 2 N
177 rpdvds x y N 2 N x y gcd 2 N = 1 N 2 N x y gcd N = 1
178 163 156 164 168 176 177 syl32anc φ x 2 y 2 x y gcd 2 N = 1 x y gcd N = 1
179 178 adantrr φ x 2 y 2 x y gcd 2 N = 1 x gcd 2 N = 1 x / L N N / L x = 1 x 1 2 N 1 2 y gcd 2 N = 1 y / L N N / L y = 1 y 1 2 N 1 2 x y gcd N = 1
180 eqidd φ x 2 y 2 x y gcd 2 N = 1 x gcd 2 N = 1 x / L N N / L x = 1 x 1 2 N 1 2 y gcd 2 N = 1 y / L N N / L y = 1 y 1 2 N 1 2 x y = x y
181 161 simpld φ x 2 y 2 x y gcd 2 N = 1 x
182 gcdcom x 2 N x gcd 2 N = 2 N gcd x
183 181 164 182 syl2anc φ x 2 y 2 x y gcd 2 N = 1 x gcd 2 N = 2 N gcd x
184 gcdcom 2 N x y 2 N gcd x y = x y gcd 2 N
185 164 163 184 syl2anc φ x 2 y 2 x y gcd 2 N = 1 2 N gcd x y = x y gcd 2 N
186 185 168 eqtrd φ x 2 y 2 x y gcd 2 N = 1 2 N gcd x y = 1
187 dvdsmul1 x y x x y
188 161 187 syl φ x 2 y 2 x y gcd 2 N = 1 x x y
189 rpdvds 2 N x x y 2 N gcd x y = 1 x x y 2 N gcd x = 1
190 164 181 163 186 188 189 syl32anc φ x 2 y 2 x y gcd 2 N = 1 2 N gcd x = 1
191 183 190 eqtrd φ x 2 y 2 x y gcd 2 N = 1 x gcd 2 N = 1
192 191 adantrr φ x 2 y 2 x y gcd 2 N = 1 x gcd 2 N = 1 x / L N N / L x = 1 x 1 2 N 1 2 y gcd 2 N = 1 y / L N N / L y = 1 y 1 2 N 1 2 x gcd 2 N = 1
193 simprrl φ x 2 y 2 x y gcd 2 N = 1 x gcd 2 N = 1 x / L N N / L x = 1 x 1 2 N 1 2 y gcd 2 N = 1 y / L N N / L y = 1 y 1 2 N 1 2 x gcd 2 N = 1 x / L N N / L x = 1 x 1 2 N 1 2
194 192 193 mpd φ x 2 y 2 x y gcd 2 N = 1 x gcd 2 N = 1 x / L N N / L x = 1 x 1 2 N 1 2 y gcd 2 N = 1 y / L N N / L y = 1 y 1 2 N 1 2 x / L N N / L x = 1 x 1 2 N 1 2
195 161 simprd φ x 2 y 2 x y gcd 2 N = 1 y
196 gcdcom y 2 N y gcd 2 N = 2 N gcd y
197 195 164 196 syl2anc φ x 2 y 2 x y gcd 2 N = 1 y gcd 2 N = 2 N gcd y
198 dvdsmul2 x y y x y
199 161 198 syl φ x 2 y 2 x y gcd 2 N = 1 y x y
200 rpdvds 2 N y x y 2 N gcd x y = 1 y x y 2 N gcd y = 1
201 164 195 163 186 199 200 syl32anc φ x 2 y 2 x y gcd 2 N = 1 2 N gcd y = 1
202 197 201 eqtrd φ x 2 y 2 x y gcd 2 N = 1 y gcd 2 N = 1
203 202 adantrr φ x 2 y 2 x y gcd 2 N = 1 x gcd 2 N = 1 x / L N N / L x = 1 x 1 2 N 1 2 y gcd 2 N = 1 y / L N N / L y = 1 y 1 2 N 1 2 y gcd 2 N = 1
204 simprrr φ x 2 y 2 x y gcd 2 N = 1 x gcd 2 N = 1 x / L N N / L x = 1 x 1 2 N 1 2 y gcd 2 N = 1 y / L N N / L y = 1 y 1 2 N 1 2 y gcd 2 N = 1 y / L N N / L y = 1 y 1 2 N 1 2
205 203 204 mpd φ x 2 y 2 x y gcd 2 N = 1 x gcd 2 N = 1 x / L N N / L x = 1 x 1 2 N 1 2 y gcd 2 N = 1 y / L N N / L y = 1 y 1 2 N 1 2 y / L N N / L y = 1 y 1 2 N 1 2
206 154 172 173 174 179 150 153 180 194 205 lgsquad2lem1 φ x 2 y 2 x y gcd 2 N = 1 x gcd 2 N = 1 x / L N N / L x = 1 x 1 2 N 1 2 y gcd 2 N = 1 y / L N N / L y = 1 y 1 2 N 1 2 x y / L N N / L x y = 1 x y 1 2 N 1 2
207 206 exp32 φ x 2 y 2 x y gcd 2 N = 1 x gcd 2 N = 1 x / L N N / L x = 1 x 1 2 N 1 2 y gcd 2 N = 1 y / L N N / L y = 1 y 1 2 N 1 2 x y / L N N / L x y = 1 x y 1 2 N 1 2
208 207 com23 φ x 2 y 2 x gcd 2 N = 1 x / L N N / L x = 1 x 1 2 N 1 2 y gcd 2 N = 1 y / L N N / L y = 1 y 1 2 N 1 2 x y gcd 2 N = 1 x y / L N N / L x y = 1 x y 1 2 N 1 2
209 208 expcom x 2 y 2 φ x gcd 2 N = 1 x / L N N / L x = 1 x 1 2 N 1 2 y gcd 2 N = 1 y / L N N / L y = 1 y 1 2 N 1 2 x y gcd 2 N = 1 x y / L N N / L x y = 1 x y 1 2 N 1 2
210 209 a2d x 2 y 2 φ x gcd 2 N = 1 x / L N N / L x = 1 x 1 2 N 1 2 y gcd 2 N = 1 y / L N N / L y = 1 y 1 2 N 1 2 φ x y gcd 2 N = 1 x y / L N N / L x y = 1 x y 1 2 N 1 2
211 147 210 syl5bir x 2 y 2 φ x gcd 2 N = 1 x / L N N / L x = 1 x 1 2 N 1 2 φ y gcd 2 N = 1 y / L N N / L y = 1 y 1 2 N 1 2 φ x y gcd 2 N = 1 x y / L N N / L x y = 1 x y 1 2 N 1 2
212 37 49 61 73 85 118 146 211 prmind M φ M gcd 2 N = 1 M / L N N / L M = 1 M 1 2 N 1 2
213 1 212 mpcom φ M gcd 2 N = 1 M / L N N / L M = 1 M 1 2 N 1 2
214 21 213 mpd φ M / L N N / L M = 1 M 1 2 N 1 2