Proof of Theorem pellexlem6
Step | Hyp | Ref
| Expression |
1 | | pellex.ann |
. . . . . . . . 9
|
2 | 1 | nncnd 11036 |
. . . . . . . 8
|
3 | | pellex.enn |
. . . . . . . . 9
|
4 | 3 | nncnd 11036 |
. . . . . . . 8
|
5 | 2, 4 | mulcld 10060 |
. . . . . . 7
|
6 | | pellex.dnn |
. . . . . . . . 9
|
7 | 6 | nncnd 11036 |
. . . . . . . 8
|
8 | | pellex.bnn |
. . . . . . . . . 10
|
9 | 8 | nncnd 11036 |
. . . . . . . . 9
|
10 | | pellex.fnn |
. . . . . . . . . 10
|
11 | 10 | nncnd 11036 |
. . . . . . . . 9
|
12 | 9, 11 | mulcld 10060 |
. . . . . . . 8
|
13 | 7, 12 | mulcld 10060 |
. . . . . . 7
|
14 | 5, 13 | subcld 10392 |
. . . . . 6
|
15 | | pellex.cz |
. . . . . . 7
|
16 | 15 | zcnd 11483 |
. . . . . 6
|
17 | | pellex.cn0 |
. . . . . 6
|
18 | 14, 16, 17 | absdivd 14194 |
. . . . 5
|
19 | 5, 13 | negsubd 10398 |
. . . . . . . . . . 11
|
20 | 19 | eqcomd 2628 |
. . . . . . . . . 10
|
21 | 20 | oveq1d 6665 |
. . . . . . . . 9
|
22 | 1 | nnred 11035 |
. . . . . . . . . . 11
|
23 | 3 | nnred 11035 |
. . . . . . . . . . 11
|
24 | 22, 23 | remulcld 10070 |
. . . . . . . . . 10
|
25 | 6 | nnred 11035 |
. . . . . . . . . . 11
|
26 | 8 | nnred 11035 |
. . . . . . . . . . . 12
|
27 | 10 | nnred 11035 |
. . . . . . . . . . . 12
|
28 | 26, 27 | remulcld 10070 |
. . . . . . . . . . 11
|
29 | 25, 28 | remulcld 10070 |
. . . . . . . . . 10
|
30 | 29 | renegcld 10457 |
. . . . . . . . . 10
|
31 | 16, 17 | absrpcld 14187 |
. . . . . . . . . 10
|
32 | 3 | nnzd 11481 |
. . . . . . . . . . . 12
|
33 | | pellex.xcg |
. . . . . . . . . . . 12
|
34 | | modmul1 12723 |
. . . . . . . . . . . 12
|
35 | 22, 23, 32, 31, 33, 34 | syl221anc 1337 |
. . . . . . . . . . 11
|
36 | 4 | sqcld 13006 |
. . . . . . . . . . . . . . 15
|
37 | 11 | sqcld 13006 |
. . . . . . . . . . . . . . . 16
|
38 | 7, 37 | mulcld 10060 |
. . . . . . . . . . . . . . 15
|
39 | 36, 38 | npcand 10396 |
. . . . . . . . . . . . . 14
|
40 | 4 | sqvald 13005 |
. . . . . . . . . . . . . 14
|
41 | 39, 40 | eqtr2d 2657 |
. . . . . . . . . . . . 13
|
42 | 41 | oveq1d 6665 |
. . . . . . . . . . . 12
|
43 | 23 | resqcld 13035 |
. . . . . . . . . . . . . 14
|
44 | 27 | resqcld 13035 |
. . . . . . . . . . . . . . 15
|
45 | 25, 44 | remulcld 10070 |
. . . . . . . . . . . . . 14
|
46 | 43, 45 | resubcld 10458 |
. . . . . . . . . . . . 13
|
47 | | 0red 10041 |
. . . . . . . . . . . . 13
|
48 | 16 | abscld 14175 |
. . . . . . . . . . . . . . . . . . 19
|
49 | 48 | recnd 10068 |
. . . . . . . . . . . . . . . . . 18
|
50 | 16, 17 | absne0d 14186 |
. . . . . . . . . . . . . . . . . 18
|
51 | 49, 50 | dividd 10799 |
. . . . . . . . . . . . . . . . 17
|
52 | | 1zzd 11408 |
. . . . . . . . . . . . . . . . 17
|
53 | 51, 52 | eqeltrd 2701 |
. . . . . . . . . . . . . . . 16
|
54 | | mod0 12675 |
. . . . . . . . . . . . . . . . 17
|
55 | 48, 31, 54 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
|
56 | 53, 55 | mpbird 247 |
. . . . . . . . . . . . . . 15
|
57 | 15 | zred 11482 |
. . . . . . . . . . . . . . . 16
|
58 | | absmod0 14043 |
. . . . . . . . . . . . . . . 16
|
59 | 57, 31, 58 | syl2anc 693 |
. . . . . . . . . . . . . . 15
|
60 | 56, 59 | mpbird 247 |
. . . . . . . . . . . . . 14
|
61 | | pellex.no2 |
. . . . . . . . . . . . . . 15
|
62 | 61 | oveq1d 6665 |
. . . . . . . . . . . . . 14
|
63 | | 0mod 12701 |
. . . . . . . . . . . . . . 15
|
64 | 31, 63 | syl 17 |
. . . . . . . . . . . . . 14
|
65 | 60, 62, 64 | 3eqtr4d 2666 |
. . . . . . . . . . . . 13
|
66 | | modadd1 12707 |
. . . . . . . . . . . . 13
|
67 | 46, 47, 45, 31, 65, 66 | syl221anc 1337 |
. . . . . . . . . . . 12
|
68 | 38 | addid2d 10237 |
. . . . . . . . . . . . . 14
|
69 | 11 | sqvald 13005 |
. . . . . . . . . . . . . . 15
|
70 | 69 | oveq2d 6666 |
. . . . . . . . . . . . . 14
|
71 | 7, 11, 11 | mul12d 10245 |
. . . . . . . . . . . . . 14
|
72 | 68, 70, 71 | 3eqtrd 2660 |
. . . . . . . . . . . . 13
|
73 | 72 | oveq1d 6665 |
. . . . . . . . . . . 12
|
74 | 42, 67, 73 | 3eqtrd 2660 |
. . . . . . . . . . 11
|
75 | 6 | nnzd 11481 |
. . . . . . . . . . . . . 14
|
76 | 10 | nnzd 11481 |
. . . . . . . . . . . . . 14
|
77 | 75, 76 | zmulcld 11488 |
. . . . . . . . . . . . 13
|
78 | | pellex.ycg |
. . . . . . . . . . . . . 14
|
79 | 78 | eqcomd 2628 |
. . . . . . . . . . . . 13
|
80 | | modmul1 12723 |
. . . . . . . . . . . . 13
|
81 | 27, 26, 77, 31, 79, 80 | syl221anc 1337 |
. . . . . . . . . . . 12
|
82 | 9, 7, 11 | mul12d 10245 |
. . . . . . . . . . . . 13
|
83 | 82 | oveq1d 6665 |
. . . . . . . . . . . 12
|
84 | 81, 83 | eqtrd 2656 |
. . . . . . . . . . 11
|
85 | 35, 74, 84 | 3eqtrd 2660 |
. . . . . . . . . 10
|
86 | | modadd1 12707 |
. . . . . . . . . 10
|
87 | 24, 29, 30, 31, 85, 86 | syl221anc 1337 |
. . . . . . . . 9
|
88 | 13 | negidd 10382 |
. . . . . . . . . 10
|
89 | 88 | oveq1d 6665 |
. . . . . . . . 9
|
90 | 21, 87, 89 | 3eqtrd 2660 |
. . . . . . . 8
|
91 | 90, 64 | eqtrd 2656 |
. . . . . . 7
|
92 | 24, 29 | resubcld 10458 |
. . . . . . . 8
|
93 | | absmod0 14043 |
. . . . . . . 8
|
94 | 92, 31, 93 | syl2anc 693 |
. . . . . . 7
|
95 | 91, 94 | mpbid 222 |
. . . . . 6
|
96 | 14 | abscld 14175 |
. . . . . . 7
|
97 | | mod0 12675 |
. . . . . . 7
|
98 | 96, 31, 97 | syl2anc 693 |
. . . . . 6
|
99 | 95, 98 | mpbid 222 |
. . . . 5
|
100 | 18, 99 | eqeltrd 2701 |
. . . 4
|
101 | 92, 57, 17 | redivcld 10853 |
. . . . 5
|
102 | | absz 14051 |
. . . . 5
|
103 | 101, 102 | syl 17 |
. . . 4
|
104 | 100, 103 | mpbird 247 |
. . 3
|
105 | | 0lt1 10550 |
. . . . . . . 8
|
106 | | 0re 10040 |
. . . . . . . . 9
|
107 | | 1re 10039 |
. . . . . . . . 9
|
108 | 106, 107 | ltnlei 10158 |
. . . . . . . 8
|
109 | 105, 108 | mpbi 220 |
. . . . . . 7
|
110 | 9, 4 | mulcld 10060 |
. . . . . . . . . . . . . 14
|
111 | 2, 11 | mulcld 10060 |
. . . . . . . . . . . . . 14
|
112 | 110, 111 | subcld 10392 |
. . . . . . . . . . . . 13
|
113 | 112, 16, 17 | divcld 10801 |
. . . . . . . . . . . 12
|
114 | 113 | abscld 14175 |
. . . . . . . . . . 11
|
115 | 114 | resqcld 13035 |
. . . . . . . . . 10
|
116 | 6 | nnnn0d 11351 |
. . . . . . . . . . 11
|
117 | 116 | nn0ge0d 11354 |
. . . . . . . . . 10
|
118 | 114 | sqge0d 13036 |
. . . . . . . . . 10
|
119 | 25, 115, 117, 118 | mulge0d 10604 |
. . . . . . . . 9
|
120 | 25, 115 | remulcld 10070 |
. . . . . . . . . 10
|
121 | 47, 120 | suble0d 10618 |
. . . . . . . . 9
|
122 | 119, 121 | mpbird 247 |
. . . . . . . 8
|
123 | | breq1 4656 |
. . . . . . . 8
|
124 | 122, 123 | syl5ibrcom 237 |
. . . . . . 7
|
125 | 109, 124 | mtoi 190 |
. . . . . 6
|
126 | | absresq 14042 |
. . . . . . . . . . . 12
|
127 | 101, 126 | syl 17 |
. . . . . . . . . . 11
|
128 | 14, 16, 17 | sqdivd 13021 |
. . . . . . . . . . 11
|
129 | 14 | sqvald 13005 |
. . . . . . . . . . . 12
|
130 | 129 | oveq1d 6665 |
. . . . . . . . . . 11
|
131 | 127, 128,
130 | 3eqtrd 2660 |
. . . . . . . . . 10
|
132 | 26, 23 | remulcld 10070 |
. . . . . . . . . . . . . . . 16
|
133 | 22, 27 | remulcld 10070 |
. . . . . . . . . . . . . . . 16
|
134 | 132, 133 | resubcld 10458 |
. . . . . . . . . . . . . . 15
|
135 | 134, 57, 17 | redivcld 10853 |
. . . . . . . . . . . . . 14
|
136 | | absresq 14042 |
. . . . . . . . . . . . . 14
|
137 | 135, 136 | syl 17 |
. . . . . . . . . . . . 13
|
138 | 112, 16, 17 | sqdivd 13021 |
. . . . . . . . . . . . 13
|
139 | 137, 138 | eqtrd 2656 |
. . . . . . . . . . . 12
|
140 | 139 | oveq2d 6666 |
. . . . . . . . . . 11
|
141 | 112 | sqcld 13006 |
. . . . . . . . . . . 12
|
142 | 16 | sqcld 13006 |
. . . . . . . . . . . 12
|
143 | | sqne0 12930 |
. . . . . . . . . . . . . 14
|
144 | 16, 143 | syl 17 |
. . . . . . . . . . . . 13
|
145 | 17, 144 | mpbird 247 |
. . . . . . . . . . . 12
|
146 | 7, 141, 142, 145 | divassd 10836 |
. . . . . . . . . . 11
|
147 | 112 | sqvald 13005 |
. . . . . . . . . . . . 13
|
148 | 147 | oveq2d 6666 |
. . . . . . . . . . . 12
|
149 | 148 | oveq1d 6665 |
. . . . . . . . . . 11
|
150 | 140, 146,
149 | 3eqtr2d 2662 |
. . . . . . . . . 10
|
151 | 131, 150 | oveq12d 6668 |
. . . . . . . . 9
|
152 | 14, 14 | mulcld 10060 |
. . . . . . . . . 10
|
153 | 112, 112 | mulcld 10060 |
. . . . . . . . . . 11
|
154 | 7, 153 | mulcld 10060 |
. . . . . . . . . 10
|
155 | 152, 154,
142, 145 | divsubdird 10840 |
. . . . . . . . 9
|
156 | 5, 13, 5, 13 | mulsubd 10490 |
. . . . . . . . . . . 12
|
157 | 110, 111,
110, 111 | mulsubd 10490 |
. . . . . . . . . . . . . 14
|
158 | 157 | oveq2d 6666 |
. . . . . . . . . . . . 13
|
159 | 110, 110 | mulcld 10060 |
. . . . . . . . . . . . . . 15
|
160 | 111, 111 | mulcld 10060 |
. . . . . . . . . . . . . . 15
|
161 | 159, 160 | addcld 10059 |
. . . . . . . . . . . . . 14
|
162 | 110, 111 | mulcld 10060 |
. . . . . . . . . . . . . . 15
|
163 | 162, 162 | addcld 10059 |
. . . . . . . . . . . . . 14
|
164 | 7, 161, 163 | subdid 10486 |
. . . . . . . . . . . . 13
|
165 | 7, 159, 160 | adddid 10064 |
. . . . . . . . . . . . . 14
|
166 | 7, 162, 162 | adddid 10064 |
. . . . . . . . . . . . . 14
|
167 | 165, 166 | oveq12d 6668 |
. . . . . . . . . . . . 13
|
168 | 158, 164,
167 | 3eqtrd 2660 |
. . . . . . . . . . . 12
|
169 | 156, 168 | oveq12d 6668 |
. . . . . . . . . . 11
|
170 | 169 | oveq1d 6665 |
. . . . . . . . . 10
|
171 | 5, 13 | mulcomd 10061 |
. . . . . . . . . . . . . . . 16
|
172 | 7, 12, 5 | mulassd 10063 |
. . . . . . . . . . . . . . . 16
|
173 | 2, 4 | mulcomd 10061 |
. . . . . . . . . . . . . . . . . . 19
|
174 | 173 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . 18
|
175 | 9, 11, 4, 2 | mul4d 10248 |
. . . . . . . . . . . . . . . . . 18
|
176 | 11, 2 | mulcomd 10061 |
. . . . . . . . . . . . . . . . . . 19
|
177 | 176 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . 18
|
178 | 174, 175,
177 | 3eqtrd 2660 |
. . . . . . . . . . . . . . . . 17
|
179 | 178 | oveq2d 6666 |
. . . . . . . . . . . . . . . 16
|
180 | 171, 172,
179 | 3eqtrd 2660 |
. . . . . . . . . . . . . . 15
|
181 | 180, 180 | oveq12d 6668 |
. . . . . . . . . . . . . 14
|
182 | 181 | oveq2d 6666 |
. . . . . . . . . . . . 13
|
183 | 182 | oveq1d 6665 |
. . . . . . . . . . . 12
|
184 | 5, 5 | mulcld 10060 |
. . . . . . . . . . . . . 14
|
185 | 13, 13 | mulcld 10060 |
. . . . . . . . . . . . . 14
|
186 | 184, 185 | addcld 10059 |
. . . . . . . . . . . . 13
|
187 | 7, 159 | mulcld 10060 |
. . . . . . . . . . . . . 14
|
188 | 7, 160 | mulcld 10060 |
. . . . . . . . . . . . . 14
|
189 | 187, 188 | addcld 10059 |
. . . . . . . . . . . . 13
|
190 | 7, 162 | mulcld 10060 |
. . . . . . . . . . . . . 14
|
191 | 190, 190 | addcld 10059 |
. . . . . . . . . . . . 13
|
192 | 186, 189,
191 | nnncan2d 10427 |
. . . . . . . . . . . 12
|
193 | 184, 185,
187, 188 | addsub4d 10439 |
. . . . . . . . . . . . 13
|
194 | 5 | sqvald 13005 |
. . . . . . . . . . . . . . 15
|
195 | 110 | sqvald 13005 |
. . . . . . . . . . . . . . . 16
|
196 | 195 | oveq2d 6666 |
. . . . . . . . . . . . . . 15
|
197 | 194, 196 | oveq12d 6668 |
. . . . . . . . . . . . . 14
|
198 | 13 | sqvald 13005 |
. . . . . . . . . . . . . . 15
|
199 | 111 | sqvald 13005 |
. . . . . . . . . . . . . . . 16
|
200 | 199 | oveq2d 6666 |
. . . . . . . . . . . . . . 15
|
201 | 198, 200 | oveq12d 6668 |
. . . . . . . . . . . . . 14
|
202 | 197, 201 | oveq12d 6668 |
. . . . . . . . . . . . 13
|
203 | 2, 4 | sqmuld 13020 |
. . . . . . . . . . . . . . . 16
|
204 | 9, 4 | sqmuld 13020 |
. . . . . . . . . . . . . . . . . 18
|
205 | 204 | oveq2d 6666 |
. . . . . . . . . . . . . . . . 17
|
206 | 9 | sqcld 13006 |
. . . . . . . . . . . . . . . . . 18
|
207 | 7, 206, 36 | mulassd 10063 |
. . . . . . . . . . . . . . . . 17
|
208 | 205, 207 | eqtr4d 2659 |
. . . . . . . . . . . . . . . 16
|
209 | 203, 208 | oveq12d 6668 |
. . . . . . . . . . . . . . 15
|
210 | 7 | sqvald 13005 |
. . . . . . . . . . . . . . . . . 18
|
211 | 9, 11 | sqmuld 13020 |
. . . . . . . . . . . . . . . . . 18
|
212 | 210, 211 | oveq12d 6668 |
. . . . . . . . . . . . . . . . 17
|
213 | 7, 12 | sqmuld 13020 |
. . . . . . . . . . . . . . . . 17
|
214 | 7, 7 | mulcld 10060 |
. . . . . . . . . . . . . . . . . 18
|
215 | 214, 206,
37 | mulassd 10063 |
. . . . . . . . . . . . . . . . 17
|
216 | 212, 213,
215 | 3eqtr4d 2666 |
. . . . . . . . . . . . . . . 16
|
217 | 2, 11 | sqmuld 13020 |
. . . . . . . . . . . . . . . . . 18
|
218 | 217 | oveq2d 6666 |
. . . . . . . . . . . . . . . . 17
|
219 | 2 | sqcld 13006 |
. . . . . . . . . . . . . . . . . 18
|
220 | 7, 219, 37 | mulassd 10063 |
. . . . . . . . . . . . . . . . 17
|
221 | 218, 220 | eqtr4d 2659 |
. . . . . . . . . . . . . . . 16
|
222 | 216, 221 | oveq12d 6668 |
. . . . . . . . . . . . . . 15
|
223 | 209, 222 | oveq12d 6668 |
. . . . . . . . . . . . . 14
|
224 | 7, 206 | mulcld 10060 |
. . . . . . . . . . . . . . . . 17
|
225 | 219, 224,
36 | subdird 10487 |
. . . . . . . . . . . . . . . 16
|
226 | | pellex.no1 |
. . . . . . . . . . . . . . . . 17
|
227 | 226 | oveq1d 6665 |
. . . . . . . . . . . . . . . 16
|
228 | 225, 227 | eqtr3d 2658 |
. . . . . . . . . . . . . . 15
|
229 | 7, 7, 206 | mulassd 10063 |
. . . . . . . . . . . . . . . . . 18
|
230 | 229 | oveq1d 6665 |
. . . . . . . . . . . . . . . . 17
|
231 | 230 | oveq1d 6665 |
. . . . . . . . . . . . . . . 16
|
232 | 214, 206 | mulcld 10060 |
. . . . . . . . . . . . . . . . 17
|
233 | 7, 219 | mulcld 10060 |
. . . . . . . . . . . . . . . . 17
|
234 | 232, 233,
37 | subdird 10487 |
. . . . . . . . . . . . . . . 16
|
235 | | subdi 10463 |
. . . . . . . . . . . . . . . . . . . 20
|
236 | 235 | eqcomd 2628 |
. . . . . . . . . . . . . . . . . . 19
|
237 | 7, 224, 219, 236 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . 18
|
238 | | negsubdi2 10340 |
. . . . . . . . . . . . . . . . . . . . . 22
|
239 | 238 | eqcomd 2628 |
. . . . . . . . . . . . . . . . . . . . 21
|
240 | 219, 224,
239 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . 20
|
241 | 226 | negeqd 10275 |
. . . . . . . . . . . . . . . . . . . 20
|
242 | 240, 241 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . 19
|
243 | 242 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . 18
|
244 | 7, 16 | mulneg2d 10484 |
. . . . . . . . . . . . . . . . . 18
|
245 | 237, 243,
244 | 3eqtrd 2660 |
. . . . . . . . . . . . . . . . 17
|
246 | 245 | oveq1d 6665 |
. . . . . . . . . . . . . . . 16
|
247 | 231, 234,
246 | 3eqtr3d 2664 |
. . . . . . . . . . . . . . 15
|
248 | 228, 247 | oveq12d 6668 |
. . . . . . . . . . . . . 14
|
249 | 7, 16 | mulcld 10060 |
. . . . . . . . . . . . . . . . . 18
|
250 | 249, 37 | mulneg1d 10483 |
. . . . . . . . . . . . . . . . 17
|
251 | 7, 16 | mulcomd 10061 |
. . . . . . . . . . . . . . . . . . . 20
|
252 | 251 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . 19
|
253 | 16, 7, 37 | mulassd 10063 |
. . . . . . . . . . . . . . . . . . 19
|
254 | 252, 253 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . 18
|
255 | 254 | negeqd 10275 |
. . . . . . . . . . . . . . . . 17
|
256 | 250, 255 | eqtrd 2656 |
. . . . . . . . . . . . . . . 16
|
257 | 256 | oveq2d 6666 |
. . . . . . . . . . . . . . 15
|
258 | 16, 36 | mulcld 10060 |
. . . . . . . . . . . . . . . 16
|
259 | 16, 38 | mulcld 10060 |
. . . . . . . . . . . . . . . 16
|
260 | 258, 259 | negsubd 10398 |
. . . . . . . . . . . . . . 15
|
261 | 61 | oveq2d 6666 |
. . . . . . . . . . . . . . . 16
|
262 | | subdi 10463 |
. . . . . . . . . . . . . . . . . 18
|
263 | 262 | eqcomd 2628 |
. . . . . . . . . . . . . . . . 17
|
264 | 16, 36, 38, 263 | syl3anc 1326 |
. . . . . . . . . . . . . . . 16
|
265 | 16 | sqvald 13005 |
. . . . . . . . . . . . . . . 16
|
266 | 261, 264,
265 | 3eqtr4d 2666 |
. . . . . . . . . . . . . . 15
|
267 | 257, 260,
266 | 3eqtrd 2660 |
. . . . . . . . . . . . . 14
|
268 | 223, 248,
267 | 3eqtrd 2660 |
. . . . . . . . . . . . 13
|
269 | 193, 202,
268 | 3eqtr2d 2662 |
. . . . . . . . . . . 12
|
270 | 183, 192,
269 | 3eqtrd 2660 |
. . . . . . . . . . 11
|
271 | 270 | oveq1d 6665 |
. . . . . . . . . 10
|
272 | 142, 145 | dividd 10799 |
. . . . . . . . . 10
|
273 | 170, 271,
272 | 3eqtrd 2660 |
. . . . . . . . 9
|
274 | 151, 155,
273 | 3eqtr2d 2662 |
. . . . . . . 8
|
275 | 274 | adantr 481 |
. . . . . . 7
|
276 | | simpr 477 |
. . . . . . . . . . . 12
|
277 | 276 | oveq1d 6665 |
. . . . . . . . . . 11
|
278 | 277 | fveq2d 6195 |
. . . . . . . . . 10
|
279 | 16, 17 | div0d 10800 |
. . . . . . . . . . . 12
|
280 | 279 | abs00bd 14031 |
. . . . . . . . . . 11
|
281 | 280 | adantr 481 |
. . . . . . . . . 10
|
282 | 278, 281 | eqtrd 2656 |
. . . . . . . . 9
|
283 | 282 | sq0id 12957 |
. . . . . . . 8
|
284 | 283 | oveq1d 6665 |
. . . . . . 7
|
285 | 275, 284 | eqtr3d 2658 |
. . . . . 6
|
286 | 125, 285 | mtand 691 |
. . . . 5
|
287 | 286 | neqned 2801 |
. . . 4
|
288 | 14, 16, 287, 17 | divne0d 10817 |
. . 3
|
289 | | nnabscl 14065 |
. . 3
|
290 | 104, 288,
289 | syl2anc 693 |
. 2
|
291 | 112, 16, 17 | absdivd 14194 |
. . . . 5
|
292 | | negsub 10329 |
. . . . . . . . . . . 12
|
293 | 292 | eqcomd 2628 |
. . . . . . . . . . 11
|
294 | 110, 111,
293 | syl2anc 693 |
. . . . . . . . . 10
|
295 | 294 | oveq1d 6665 |
. . . . . . . . 9
|
296 | 133 | renegcld 10457 |
. . . . . . . . . 10
|
297 | 11, 4 | mulcomd 10061 |
. . . . . . . . . . . 12
|
298 | 297 | oveq1d 6665 |
. . . . . . . . . . 11
|
299 | | modmul1 12723 |
. . . . . . . . . . . 12
|
300 | 26, 27, 32, 31, 78, 299 | syl221anc 1337 |
. . . . . . . . . . 11
|
301 | | modmul1 12723 |
. . . . . . . . . . . 12
|
302 | 22, 23, 76, 31, 33, 301 | syl221anc 1337 |
. . . . . . . . . . 11
|
303 | 298, 300,
302 | 3eqtr4d 2666 |
. . . . . . . . . 10
|
304 | | modadd1 12707 |
. . . . . . . . . 10
|
305 | 132, 133,
296, 31, 303, 304 | syl221anc 1337 |
. . . . . . . . 9
|
306 | 111 | negidd 10382 |
. . . . . . . . . 10
|
307 | 306 | oveq1d 6665 |
. . . . . . . . 9
|
308 | 295, 305,
307 | 3eqtrd 2660 |
. . . . . . . 8
|
309 | 308, 64 | eqtrd 2656 |
. . . . . . 7
|
310 | | absmod0 14043 |
. . . . . . . 8
|
311 | 134, 31, 310 | syl2anc 693 |
. . . . . . 7
|
312 | 309, 311 | mpbid 222 |
. . . . . 6
|
313 | 112 | abscld 14175 |
. . . . . . 7
|
314 | | mod0 12675 |
. . . . . . 7
|
315 | 313, 31, 314 | syl2anc 693 |
. . . . . 6
|
316 | 312, 315 | mpbid 222 |
. . . . 5
|
317 | 291, 316 | eqeltrd 2701 |
. . . 4
|
318 | | absz 14051 |
. . . . 5
|
319 | 135, 318 | syl 17 |
. . . 4
|
320 | 317, 319 | mpbird 247 |
. . 3
|
321 | | pellex.neq |
. . . . . . 7
|
322 | 10 | nnne0d 11065 |
. . . . . . . . 9
|
323 | 3 | nnne0d 11065 |
. . . . . . . . 9
|
324 | 9, 11, 2, 4, 322, 323 | divmuleqd 10847 |
. . . . . . . 8
|
325 | 61 | adantr 481 |
. . . . . . . . . . . . . . 15
|
326 | 325 | eqcomd 2628 |
. . . . . . . . . . . . . 14
|
327 | 326 | oveq2d 6666 |
. . . . . . . . . . . . 13
|
328 | 9, 11, 322 | divcld 10801 |
. . . . . . . . . . . . . . . 16
|
329 | 328 | sqcld 13006 |
. . . . . . . . . . . . . . 15
|
330 | 329 | adantr 481 |
. . . . . . . . . . . . . 14
|
331 | 36 | adantr 481 |
. . . . . . . . . . . . . 14
|
332 | 38 | adantr 481 |
. . . . . . . . . . . . . 14
|
333 | 330, 331,
332 | subdid 10486 |
. . . . . . . . . . . . 13
|
334 | | oveq1 6657 |
. . . . . . . . . . . . . . . . 17
|
335 | 334 | oveq1d 6665 |
. . . . . . . . . . . . . . . 16
|
336 | 335 | adantl 482 |
. . . . . . . . . . . . . . 15
|
337 | 2 | adantr 481 |
. . . . . . . . . . . . . . . . 17
|
338 | 4 | adantr 481 |
. . . . . . . . . . . . . . . . 17
|
339 | 323 | adantr 481 |
. . . . . . . . . . . . . . . . 17
|
340 | 337, 338,
339 | sqdivd 13021 |
. . . . . . . . . . . . . . . 16
|
341 | 340 | oveq1d 6665 |
. . . . . . . . . . . . . . 15
|
342 | 219 | adantr 481 |
. . . . . . . . . . . . . . . 16
|
343 | | sqne0 12930 |
. . . . . . . . . . . . . . . . . . 19
|
344 | 4, 343 | syl 17 |
. . . . . . . . . . . . . . . . . 18
|
345 | 323, 344 | mpbird 247 |
. . . . . . . . . . . . . . . . 17
|
346 | 345 | adantr 481 |
. . . . . . . . . . . . . . . 16
|
347 | 342, 331,
346 | divcan1d 10802 |
. . . . . . . . . . . . . . 15
|
348 | 336, 341,
347 | 3eqtrd 2660 |
. . . . . . . . . . . . . 14
|
349 | 7 | adantr 481 |
. . . . . . . . . . . . . . . 16
|
350 | 37 | adantr 481 |
. . . . . . . . . . . . . . . 16
|
351 | 330, 349,
350 | mul12d 10245 |
. . . . . . . . . . . . . . 15
|
352 | 9 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
|
353 | 11 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
|
354 | 322 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
|
355 | 352, 353,
354 | sqdivd 13021 |
. . . . . . . . . . . . . . . . 17
|
356 | 355 | oveq1d 6665 |
. . . . . . . . . . . . . . . 16
|
357 | 356 | oveq2d 6666 |
. . . . . . . . . . . . . . 15
|
358 | 206 | adantr 481 |
. . . . . . . . . . . . . . . . 17
|
359 | | sqne0 12930 |
. . . . . . . . . . . . . . . . . . . 20
|
360 | 11, 359 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
|
361 | 322, 360 | mpbird 247 |
. . . . . . . . . . . . . . . . . 18
|
362 | 361 | adantr 481 |
. . . . . . . . . . . . . . . . 17
|
363 | 358, 350,
362 | divcan1d 10802 |
. . . . . . . . . . . . . . . 16
|
364 | 363 | oveq2d 6666 |
. . . . . . . . . . . . . . 15
|
365 | 351, 357,
364 | 3eqtrd 2660 |
. . . . . . . . . . . . . 14
|
366 | 348, 365 | oveq12d 6668 |
. . . . . . . . . . . . 13
|
367 | 327, 333,
366 | 3eqtrd 2660 |
. . . . . . . . . . . 12
|
368 | 226 | eqcomd 2628 |
. . . . . . . . . . . . 13
|
369 | 368 | adantr 481 |
. . . . . . . . . . . 12
|
370 | 367, 369 | oveq12d 6668 |
. . . . . . . . . . 11
|
371 | 16 | adantr 481 |
. . . . . . . . . . . 12
|
372 | 17 | adantr 481 |
. . . . . . . . . . . 12
|
373 | 330, 371,
372 | divcan4d 10807 |
. . . . . . . . . . 11
|
374 | 226, 226 | oveq12d 6668 |
. . . . . . . . . . . . 13
|
375 | 16, 17 | dividd 10799 |
. . . . . . . . . . . . 13
|
376 | 374, 375 | eqtrd 2656 |
. . . . . . . . . . . 12
|
377 | 376 | adantr 481 |
. . . . . . . . . . 11
|
378 | 370, 373,
377 | 3eqtr3d 2664 |
. . . . . . . . . 10
|
379 | 26, 27, 322 | redivcld 10853 |
. . . . . . . . . . . . . . . 16
|
380 | 8 | nnnn0d 11351 |
. . . . . . . . . . . . . . . . . 18
|
381 | 380 | nn0ge0d 11354 |
. . . . . . . . . . . . . . . . 17
|
382 | 10 | nngt0d 11064 |
. . . . . . . . . . . . . . . . 17
|
383 | | divge0 10892 |
. . . . . . . . . . . . . . . . 17
|
384 | 26, 381, 27, 382, 383 | syl22anc 1327 |
. . . . . . . . . . . . . . . 16
|
385 | 379, 384 | sqrtsqd 14158 |
. . . . . . . . . . . . . . 15
|
386 | 385 | eqcomd 2628 |
. . . . . . . . . . . . . 14
|
387 | 386 | ad2antrr 762 |
. . . . . . . . . . . . 13
|
388 | | fveq2 6191 |
. . . . . . . . . . . . . 14
|
389 | 388 | adantl 482 |
. . . . . . . . . . . . 13
|
390 | | sqrt1 14012 |
. . . . . . . . . . . . . 14
|
391 | 390 | a1i 11 |
. . . . . . . . . . . . 13
|
392 | 387, 389,
391 | 3eqtrd 2660 |
. . . . . . . . . . . 12
|
393 | 392 | ex 450 |
. . . . . . . . . . 11
|
394 | | simplr 792 |
. . . . . . . . . . . . . . . 16
|
395 | | simpr 477 |
. . . . . . . . . . . . . . . 16
|
396 | 394, 395 | eqtr3d 2658 |
. . . . . . . . . . . . . . 15
|
397 | 396 | oveq1d 6665 |
. . . . . . . . . . . . . 14
|
398 | 2, 4, 323 | divcan1d 10802 |
. . . . . . . . . . . . . . 15
|
399 | 398 | ad2antrr 762 |
. . . . . . . . . . . . . 14
|
400 | 4 | mulid2d 10058 |
. . . . . . . . . . . . . . 15
|
401 | 400 | ad2antrr 762 |
. . . . . . . . . . . . . 14
|
402 | 397, 399,
401 | 3eqtr3d 2664 |
. . . . . . . . . . . . 13
|
403 | 395 | oveq1d 6665 |
. . . . . . . . . . . . . 14
|
404 | 9, 11, 322 | divcan1d 10802 |
. . . . . . . . . . . . . . 15
|
405 | 404 | ad2antrr 762 |
. . . . . . . . . . . . . 14
|
406 | 11 | mulid2d 10058 |
. . . . . . . . . . . . . . 15
|
407 | 406 | ad2antrr 762 |
. . . . . . . . . . . . . 14
|
408 | 403, 405,
407 | 3eqtr3d 2664 |
. . . . . . . . . . . . 13
|
409 | 402, 408 | jca 554 |
. . . . . . . . . . . 12
|
410 | 409 | ex 450 |
. . . . . . . . . . 11
|
411 | 393, 410 | syld 47 |
. . . . . . . . . 10
|
412 | 378, 411 | mpd 15 |
. . . . . . . . 9
|
413 | 412 | ex 450 |
. . . . . . . 8
|
414 | 324, 413 | sylbird 250 |
. . . . . . 7
|
415 | 321, 414 | mtod 189 |
. . . . . 6
|
416 | 415 | neqned 2801 |
. . . . 5
|
417 | 110, 111,
416 | subne0d 10401 |
. . . 4
|
418 | 112, 16, 417, 17 | divne0d 10817 |
. . 3
|
419 | | nnabscl 14065 |
. . 3
|
420 | 320, 418,
419 | syl2anc 693 |
. 2
|
421 | | oveq1 6657 |
. . . . 5
|
422 | 421 | oveq1d 6665 |
. . . 4
|
423 | 422 | eqeq1d 2624 |
. . 3
|
424 | | oveq1 6657 |
. . . . . 6
|
425 | 424 | oveq2d 6666 |
. . . . 5
|
426 | 425 | oveq2d 6666 |
. . . 4
|
427 | 426 | eqeq1d 2624 |
. . 3
|
428 | 423, 427 | rspc2ev 3324 |
. 2
|
429 | 290, 420,
274, 428 | syl3anc 1326 |
1
|