Step | Hyp | Ref
| Expression |
1 | | fzfi 12771 |
. . . . . 6
|
2 | | ssrab2 3687 |
. . . . . 6
|
3 | | ssfi 8180 |
. . . . . 6
|
4 | 1, 2, 3 | mp2an 708 |
. . . . 5
|
5 | 4 | a1i 11 |
. . . 4
|
6 | | nnnn0 11299 |
. . . . . . . 8
|
7 | 6 | 3ad2ant3 1084 |
. . . . . . 7
|
8 | 2 | sseli 3599 |
. . . . . . . 8
|
9 | | elfzelz 12342 |
. . . . . . . 8
|
10 | 8, 9 | syl 17 |
. . . . . . 7
|
11 | | bccl 13109 |
. . . . . . 7
|
12 | 7, 10, 11 | syl2an 494 |
. . . . . 6
|
13 | 12 | nn0zd 11480 |
. . . . 5
|
14 | | simpl1 1064 |
. . . . . . . . 9
|
15 | | simpl2 1065 |
. . . . . . . . 9
|
16 | | frmx 37478 |
. . . . . . . . . 10
Xrm
|
17 | 16 | fovcl 6765 |
. . . . . . . . 9
Xrm |
18 | 14, 15, 17 | syl2anc 693 |
. . . . . . . 8
Xrm |
19 | 18 | nn0zd 11480 |
. . . . . . 7
Xrm |
20 | 8 | adantl 482 |
. . . . . . . 8
|
21 | | fznn0sub 12373 |
. . . . . . . 8
|
22 | 20, 21 | syl 17 |
. . . . . . 7
|
23 | | zexpcl 12875 |
. . . . . . 7
Xrm
Xrm |
24 | 19, 22, 23 | syl2anc 693 |
. . . . . 6
Xrm |
25 | | rmspecnonsq 37472 |
. . . . . . . . . . 11
◻NN |
26 | 25 | eldifad 3586 |
. . . . . . . . . 10
|
27 | 26 | nnzd 11481 |
. . . . . . . . 9
|
28 | 27 | 3ad2ant1 1082 |
. . . . . . . 8
|
29 | | breq2 4657 |
. . . . . . . . . . . . . 14
|
30 | 29 | notbid 308 |
. . . . . . . . . . . . 13
|
31 | 30 | elrab 3363 |
. . . . . . . . . . . 12
|
32 | 31 | simprbi 480 |
. . . . . . . . . . 11
|
33 | | 1zzd 11408 |
. . . . . . . . . . 11
|
34 | | n2dvds1 15104 |
. . . . . . . . . . . 12
|
35 | 34 | a1i 11 |
. . . . . . . . . . 11
|
36 | | omoe 15088 |
. . . . . . . . . . 11
|
37 | 10, 32, 33, 35, 36 | syl22anc 1327 |
. . . . . . . . . 10
|
38 | | 2z 11409 |
. . . . . . . . . . . 12
|
39 | 38 | a1i 11 |
. . . . . . . . . . 11
|
40 | | 2ne0 11113 |
. . . . . . . . . . . 12
|
41 | 40 | a1i 11 |
. . . . . . . . . . 11
|
42 | | peano2zm 11420 |
. . . . . . . . . . . 12
|
43 | 10, 42 | syl 17 |
. . . . . . . . . . 11
|
44 | | dvdsval2 14986 |
. . . . . . . . . . 11
|
45 | 39, 41, 43, 44 | syl3anc 1326 |
. . . . . . . . . 10
|
46 | 37, 45 | mpbid 222 |
. . . . . . . . 9
|
47 | 43 | zred 11482 |
. . . . . . . . . 10
|
48 | | 0red 10041 |
. . . . . . . . . . . . . . 15
|
49 | | 3re 11094 |
. . . . . . . . . . . . . . . 16
|
50 | 49 | a1i 11 |
. . . . . . . . . . . . . . 15
|
51 | 9 | zred 11482 |
. . . . . . . . . . . . . . 15
|
52 | | 3pos 11114 |
. . . . . . . . . . . . . . . 16
|
53 | 52 | a1i 11 |
. . . . . . . . . . . . . . 15
|
54 | | elfzle1 12344 |
. . . . . . . . . . . . . . 15
|
55 | 48, 50, 51, 53, 54 | ltletrd 10197 |
. . . . . . . . . . . . . 14
|
56 | | elnnz 11387 |
. . . . . . . . . . . . . 14
|
57 | 9, 55, 56 | sylanbrc 698 |
. . . . . . . . . . . . 13
|
58 | | nnm1nn0 11334 |
. . . . . . . . . . . . 13
|
59 | 57, 58 | syl 17 |
. . . . . . . . . . . 12
|
60 | 59 | nn0ge0d 11354 |
. . . . . . . . . . 11
|
61 | 8, 60 | syl 17 |
. . . . . . . . . 10
|
62 | | 2re 11090 |
. . . . . . . . . . 11
|
63 | 62 | a1i 11 |
. . . . . . . . . 10
|
64 | | 2pos 11112 |
. . . . . . . . . . 11
|
65 | 64 | a1i 11 |
. . . . . . . . . 10
|
66 | | divge0 10892 |
. . . . . . . . . 10
|
67 | 47, 61, 63, 65, 66 | syl22anc 1327 |
. . . . . . . . 9
|
68 | | elnn0z 11390 |
. . . . . . . . 9
|
69 | 46, 67, 68 | sylanbrc 698 |
. . . . . . . 8
|
70 | | zexpcl 12875 |
. . . . . . . 8
|
71 | 28, 69, 70 | syl2an 494 |
. . . . . . 7
|
72 | | frmy 37479 |
. . . . . . . . . 10
Yrm
|
73 | 72 | fovcl 6765 |
. . . . . . . . 9
Yrm |
74 | 14, 15, 73 | syl2anc 693 |
. . . . . . . 8
Yrm |
75 | | elfzel1 12341 |
. . . . . . . . . . . 12
|
76 | 9, 75 | zsubcld 11487 |
. . . . . . . . . . 11
|
77 | | subge0 10541 |
. . . . . . . . . . . . 13
|
78 | 51, 49, 77 | sylancl 694 |
. . . . . . . . . . . 12
|
79 | 54, 78 | mpbird 247 |
. . . . . . . . . . 11
|
80 | | elnn0z 11390 |
. . . . . . . . . . 11
|
81 | 76, 79, 80 | sylanbrc 698 |
. . . . . . . . . 10
|
82 | 8, 81 | syl 17 |
. . . . . . . . 9
|
83 | 82 | adantl 482 |
. . . . . . . 8
|
84 | | zexpcl 12875 |
. . . . . . . 8
Yrm
Yrm |
85 | 74, 83, 84 | syl2anc 693 |
. . . . . . 7
Yrm |
86 | 71, 85 | zmulcld 11488 |
. . . . . 6
Yrm |
87 | 24, 86 | zmulcld 11488 |
. . . . 5
Xrm
Yrm |
88 | 13, 87 | zmulcld 11488 |
. . . 4
Xrm Yrm |
89 | 5, 88 | fsumzcl 14466 |
. . 3
Xrm Yrm |
90 | 73 | 3adant3 1081 |
. . . 4
Yrm |
91 | | 3nn0 11310 |
. . . 4
|
92 | | zexpcl 12875 |
. . . 4
Yrm
Yrm |
93 | 90, 91, 92 | sylancl 694 |
. . 3
Yrm |
94 | | dvdsmul2 15004 |
. . 3
Xrm Yrm Yrm
Yrm
Xrm Yrm Yrm |
95 | 89, 93, 94 | syl2anc 693 |
. 2
Yrm
Xrm Yrm Yrm |
96 | | jm2.22 37562 |
. . . . . 6
Yrm
Xrm
Yrm |
97 | 6, 96 | syl3an3 1361 |
. . . . 5
Yrm
Xrm
Yrm |
98 | | 1lt3 11196 |
. . . . . . . . . . . 12
|
99 | | 1re 10039 |
. . . . . . . . . . . . 13
|
100 | 99, 49 | ltnlei 10158 |
. . . . . . . . . . . 12
|
101 | 98, 100 | mpbi 220 |
. . . . . . . . . . 11
|
102 | | elfzle1 12344 |
. . . . . . . . . . 11
|
103 | 101, 102 | mto 188 |
. . . . . . . . . 10
|
104 | 103 | a1i 11 |
. . . . . . . . 9
|
105 | 104 | intnanrd 963 |
. . . . . . . 8
|
106 | | breq2 4657 |
. . . . . . . . . 10
|
107 | 106 | notbid 308 |
. . . . . . . . 9
|
108 | 107 | elrab 3363 |
. . . . . . . 8
|
109 | 105, 108 | sylnibr 319 |
. . . . . . 7
|
110 | | disjsn 4246 |
. . . . . . 7
|
111 | 109, 110 | sylibr 224 |
. . . . . 6
|
112 | | simpr 477 |
. . . . . . . . . . 11
|
113 | 112 | olcd 408 |
. . . . . . . . . 10
|
114 | | elfznn0 12433 |
. . . . . . . . . . . . . . . 16
|
115 | 114 | adantr 481 |
. . . . . . . . . . . . . . 15
|
116 | 115 | ad2antlr 763 |
. . . . . . . . . . . . . 14
|
117 | | simplrr 801 |
. . . . . . . . . . . . . 14
|
118 | | simpr 477 |
. . . . . . . . . . . . . 14
|
119 | | elnn1uz2 11765 |
. . . . . . . . . . . . . . . 16
|
120 | | df-ne 2795 |
. . . . . . . . . . . . . . . . . . . . 21
|
121 | 120 | biimpi 206 |
. . . . . . . . . . . . . . . . . . . 20
|
122 | 121 | 3ad2ant3 1084 |
. . . . . . . . . . . . . . . . . . 19
|
123 | 122 | pm2.21d 118 |
. . . . . . . . . . . . . . . . . 18
|
124 | 123 | imp 445 |
. . . . . . . . . . . . . . . . 17
|
125 | | uzp1 11721 |
. . . . . . . . . . . . . . . . . 18
|
126 | | 1z 11407 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
127 | | dvdsmul1 15003 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
128 | 38, 126, 127 | mp2an 708 |
. . . . . . . . . . . . . . . . . . . . . 22
|
129 | | 2t1e2 11176 |
. . . . . . . . . . . . . . . . . . . . . 22
|
130 | 128, 129 | breqtri 4678 |
. . . . . . . . . . . . . . . . . . . . 21
|
131 | | breq2 4657 |
. . . . . . . . . . . . . . . . . . . . . 22
|
132 | 131 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . 21
|
133 | 130, 132 | mpbiri 248 |
. . . . . . . . . . . . . . . . . . . 20
|
134 | | simpl2 1065 |
. . . . . . . . . . . . . . . . . . . 20
|
135 | 133, 134 | pm2.21dd 186 |
. . . . . . . . . . . . . . . . . . 19
|
136 | | eluzle 11700 |
. . . . . . . . . . . . . . . . . . . . 21
|
137 | | 2p1e3 11151 |
. . . . . . . . . . . . . . . . . . . . . 22
|
138 | 137 | fveq2i 6194 |
. . . . . . . . . . . . . . . . . . . . 21
|
139 | 136, 138 | eleq2s 2719 |
. . . . . . . . . . . . . . . . . . . 20
|
140 | 139 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
|
141 | 135, 140 | jaodan 826 |
. . . . . . . . . . . . . . . . . 18
|
142 | 125, 141 | sylan2 491 |
. . . . . . . . . . . . . . . . 17
|
143 | 124, 142 | jaodan 826 |
. . . . . . . . . . . . . . . 16
|
144 | 119, 143 | sylan2b 492 |
. . . . . . . . . . . . . . 15
|
145 | | dvds0 14997 |
. . . . . . . . . . . . . . . . . . 19
|
146 | 38, 145 | ax-mp 5 |
. . . . . . . . . . . . . . . . . 18
|
147 | | breq2 4657 |
. . . . . . . . . . . . . . . . . 18
|
148 | 146, 147 | mpbiri 248 |
. . . . . . . . . . . . . . . . 17
|
149 | 148 | adantl 482 |
. . . . . . . . . . . . . . . 16
|
150 | | simpl2 1065 |
. . . . . . . . . . . . . . . 16
|
151 | 149, 150 | pm2.21dd 186 |
. . . . . . . . . . . . . . 15
|
152 | | elnn0 11294 |
. . . . . . . . . . . . . . . . 17
|
153 | 152 | biimpi 206 |
. . . . . . . . . . . . . . . 16
|
154 | 153 | 3ad2ant1 1082 |
. . . . . . . . . . . . . . 15
|
155 | 144, 151,
154 | mpjaodan 827 |
. . . . . . . . . . . . . 14
|
156 | 116, 117,
118, 155 | syl3anc 1326 |
. . . . . . . . . . . . 13
|
157 | | elfzle2 12345 |
. . . . . . . . . . . . . . 15
|
158 | 157 | adantr 481 |
. . . . . . . . . . . . . 14
|
159 | 158 | ad2antlr 763 |
. . . . . . . . . . . . 13
|
160 | | elfzelz 12342 |
. . . . . . . . . . . . . . . 16
|
161 | 160 | adantr 481 |
. . . . . . . . . . . . . . 15
|
162 | 161 | ad2antlr 763 |
. . . . . . . . . . . . . 14
|
163 | | 3z 11410 |
. . . . . . . . . . . . . . 15
|
164 | 163 | a1i 11 |
. . . . . . . . . . . . . 14
|
165 | | nnz 11399 |
. . . . . . . . . . . . . . . 16
|
166 | 165 | 3ad2ant3 1084 |
. . . . . . . . . . . . . . 15
|
167 | 166 | ad2antrr 762 |
. . . . . . . . . . . . . 14
|
168 | | elfz 12332 |
. . . . . . . . . . . . . 14
|
169 | 162, 164,
167, 168 | syl3anc 1326 |
. . . . . . . . . . . . 13
|
170 | 156, 159,
169 | mpbir2and 957 |
. . . . . . . . . . . 12
|
171 | 170, 117 | jca 554 |
. . . . . . . . . . 11
|
172 | 171 | orcd 407 |
. . . . . . . . . 10
|
173 | 113, 172 | pm2.61dane 2881 |
. . . . . . . . 9
|
174 | | nn0uz 11722 |
. . . . . . . . . . . . . . 15
|
175 | 91, 174 | eleqtri 2699 |
. . . . . . . . . . . . . 14
|
176 | | fzss1 12380 |
. . . . . . . . . . . . . 14
|
177 | 175, 176 | ax-mp 5 |
. . . . . . . . . . . . 13
|
178 | 177 | sseli 3599 |
. . . . . . . . . . . 12
|
179 | 178 | anim1i 592 |
. . . . . . . . . . 11
|
180 | 179 | adantl 482 |
. . . . . . . . . 10
|
181 | | 0le1 10551 |
. . . . . . . . . . . . 13
|
182 | 181 | a1i 11 |
. . . . . . . . . . . 12
|
183 | | nnge1 11046 |
. . . . . . . . . . . . . 14
|
184 | 183 | 3ad2ant3 1084 |
. . . . . . . . . . . . 13
|
185 | 184 | adantr 481 |
. . . . . . . . . . . 12
|
186 | | 1zzd 11408 |
. . . . . . . . . . . . 13
|
187 | | 0zd 11389 |
. . . . . . . . . . . . 13
|
188 | 166 | adantr 481 |
. . . . . . . . . . . . 13
|
189 | | elfz 12332 |
. . . . . . . . . . . . 13
|
190 | 186, 187,
188, 189 | syl3anc 1326 |
. . . . . . . . . . . 12
|
191 | 182, 185,
190 | mpbir2and 957 |
. . . . . . . . . . 11
|
192 | 34 | a1i 11 |
. . . . . . . . . . 11
|
193 | | eleq1 2689 |
. . . . . . . . . . . . 13
|
194 | | breq2 4657 |
. . . . . . . . . . . . . 14
|
195 | 194 | notbid 308 |
. . . . . . . . . . . . 13
|
196 | 193, 195 | anbi12d 747 |
. . . . . . . . . . . 12
|
197 | 196 | adantl 482 |
. . . . . . . . . . 11
|
198 | 191, 192,
197 | mpbir2and 957 |
. . . . . . . . . 10
|
199 | 180, 198 | jaodan 826 |
. . . . . . . . 9
|
200 | 173, 199 | impbida 877 |
. . . . . . . 8
|
201 | 30 | elrab 3363 |
. . . . . . . 8
|
202 | | elun 3753 |
. . . . . . . . 9
|
203 | | velsn 4193 |
. . . . . . . . . 10
|
204 | 31, 203 | orbi12i 543 |
. . . . . . . . 9
|
205 | 202, 204 | bitri 264 |
. . . . . . . 8
|
206 | 200, 201,
205 | 3bitr4g 303 |
. . . . . . 7
|
207 | 206 | eqrdv 2620 |
. . . . . 6
|
208 | | fzfi 12771 |
. . . . . . . 8
|
209 | | ssrab2 3687 |
. . . . . . . 8
|
210 | | ssfi 8180 |
. . . . . . . 8
|
211 | 208, 209,
210 | mp2an 708 |
. . . . . . 7
|
212 | 211 | a1i 11 |
. . . . . 6
|
213 | 209 | sseli 3599 |
. . . . . . . . . 10
|
214 | 213, 160 | syl 17 |
. . . . . . . . 9
|
215 | 7, 214, 11 | syl2an 494 |
. . . . . . . 8
|
216 | 215 | nn0cnd 11353 |
. . . . . . 7
|
217 | 17 | 3adant3 1081 |
. . . . . . . . . . 11
Xrm |
218 | 217 | nn0cnd 11353 |
. . . . . . . . . 10
Xrm |
219 | 218 | adantr 481 |
. . . . . . . . 9
Xrm |
220 | 213 | adantl 482 |
. . . . . . . . . 10
|
221 | | fznn0sub 12373 |
. . . . . . . . . 10
|
222 | 220, 221 | syl 17 |
. . . . . . . . 9
|
223 | 219, 222 | expcld 13008 |
. . . . . . . 8
Xrm |
224 | 90 | zcnd 11483 |
. . . . . . . . . 10
Yrm |
225 | 213, 114 | syl 17 |
. . . . . . . . . 10
|
226 | | expcl 12878 |
. . . . . . . . . 10
Yrm
Yrm |
227 | 224, 225,
226 | syl2an 494 |
. . . . . . . . 9
Yrm |
228 | | rmspecpos 37481 |
. . . . . . . . . . . 12
|
229 | 228 | rpcnd 11874 |
. . . . . . . . . . 11
|
230 | 229 | 3ad2ant1 1082 |
. . . . . . . . . 10
|
231 | 201 | simprbi 480 |
. . . . . . . . . . . . 13
|
232 | | 1zzd 11408 |
. . . . . . . . . . . . 13
|
233 | 34 | a1i 11 |
. . . . . . . . . . . . 13
|
234 | 214, 231,
232, 233, 36 | syl22anc 1327 |
. . . . . . . . . . . 12
|
235 | 38 | a1i 11 |
. . . . . . . . . . . . 13
|
236 | 40 | a1i 11 |
. . . . . . . . . . . . 13
|
237 | 214, 42 | syl 17 |
. . . . . . . . . . . . 13
|
238 | 235, 236,
237, 44 | syl3anc 1326 |
. . . . . . . . . . . 12
|
239 | 234, 238 | mpbid 222 |
. . . . . . . . . . 11
|
240 | 237 | zred 11482 |
. . . . . . . . . . . 12
|
241 | 148 | a1i 11 |
. . . . . . . . . . . . . . . . 17
|
242 | 241 | con3dimp 457 |
. . . . . . . . . . . . . . . 16
|
243 | 201, 242 | sylbi 207 |
. . . . . . . . . . . . . . 15
|
244 | 225, 153 | syl 17 |
. . . . . . . . . . . . . . 15
|
245 | | orel2 398 |
. . . . . . . . . . . . . . 15
|
246 | 243, 244,
245 | sylc 65 |
. . . . . . . . . . . . . 14
|
247 | 246, 58 | syl 17 |
. . . . . . . . . . . . 13
|
248 | 247 | nn0ge0d 11354 |
. . . . . . . . . . . 12
|
249 | 62 | a1i 11 |
. . . . . . . . . . . 12
|
250 | 64 | a1i 11 |
. . . . . . . . . . . 12
|
251 | 240, 248,
249, 250, 66 | syl22anc 1327 |
. . . . . . . . . . 11
|
252 | 239, 251,
68 | sylanbrc 698 |
. . . . . . . . . 10
|
253 | | expcl 12878 |
. . . . . . . . . 10
|
254 | 230, 252,
253 | syl2an 494 |
. . . . . . . . 9
|
255 | 227, 254 | mulcld 10060 |
. . . . . . . 8
Yrm |
256 | 223, 255 | mulcld 10060 |
. . . . . . 7
Xrm Yrm |
257 | 216, 256 | mulcld 10060 |
. . . . . 6
Xrm Yrm |
258 | 111, 207,
212, 257 | fsumsplit 14471 |
. . . . 5
Xrm Yrm Xrm Yrm
Xrm Yrm |
259 | | expcl 12878 |
. . . . . . . . 9
Yrm
Yrm |
260 | 224, 91, 259 | sylancl 694 |
. . . . . . . 8
Yrm |
261 | 88 | zcnd 11483 |
. . . . . . . 8
Xrm Yrm |
262 | 5, 260, 261 | fsummulc1 14517 |
. . . . . . 7
Xrm Yrm Yrm
Xrm Yrm Yrm |
263 | 12 | nn0cnd 11353 |
. . . . . . . . . 10
|
264 | 218 | adantr 481 |
. . . . . . . . . . . 12
Xrm |
265 | 264, 22 | expcld 13008 |
. . . . . . . . . . 11
Xrm |
266 | 230, 69, 253 | syl2an 494 |
. . . . . . . . . . . 12
|
267 | | expcl 12878 |
. . . . . . . . . . . . 13
Yrm
Yrm |
268 | 224, 82, 267 | syl2an 494 |
. . . . . . . . . . . 12
Yrm |
269 | 266, 268 | mulcld 10060 |
. . . . . . . . . . 11
Yrm |
270 | 265, 269 | mulcld 10060 |
. . . . . . . . . 10
Xrm
Yrm |
271 | 260 | adantr 481 |
. . . . . . . . . 10
Yrm |
272 | 263, 270,
271 | mulassd 10063 |
. . . . . . . . 9
Xrm
Yrm Yrm Xrm
Yrm Yrm |
273 | 265, 269,
271 | mulassd 10063 |
. . . . . . . . . . 11
Xrm Yrm Yrm Xrm Yrm Yrm |
274 | 266, 268,
271 | mulassd 10063 |
. . . . . . . . . . . . 13
Yrm Yrm Yrm Yrm |
275 | 268, 271 | mulcld 10060 |
. . . . . . . . . . . . . 14
Yrm Yrm |
276 | 266, 275 | mulcomd 10061 |
. . . . . . . . . . . . 13
Yrm
Yrm
Yrm
Yrm |
277 | 224 | adantr 481 |
. . . . . . . . . . . . . . . 16
Yrm |
278 | 91 | a1i 11 |
. . . . . . . . . . . . . . . 16
|
279 | 277, 278,
83 | expaddd 13010 |
. . . . . . . . . . . . . . 15
Yrm Yrm Yrm |
280 | 10 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
|
281 | 280 | zcnd 11483 |
. . . . . . . . . . . . . . . . 17
|
282 | | 3cn 11095 |
. . . . . . . . . . . . . . . . 17
|
283 | | npcan 10290 |
. . . . . . . . . . . . . . . . 17
|
284 | 281, 282,
283 | sylancl 694 |
. . . . . . . . . . . . . . . 16
|
285 | 284 | oveq2d 6666 |
. . . . . . . . . . . . . . 15
Yrm
Yrm |
286 | 279, 285 | eqtr3d 2658 |
. . . . . . . . . . . . . 14
Yrm Yrm Yrm |
287 | 286 | oveq1d 6665 |
. . . . . . . . . . . . 13
Yrm Yrm Yrm |
288 | 274, 276,
287 | 3eqtrd 2660 |
. . . . . . . . . . . 12
Yrm Yrm Yrm |
289 | 288 | oveq2d 6666 |
. . . . . . . . . . 11
Xrm Yrm Yrm Xrm Yrm |
290 | 273, 289 | eqtrd 2656 |
. . . . . . . . . 10
Xrm Yrm Yrm Xrm Yrm |
291 | 290 | oveq2d 6666 |
. . . . . . . . 9
Xrm
Yrm Yrm
Xrm Yrm |
292 | 272, 291 | eqtrd 2656 |
. . . . . . . 8
Xrm
Yrm Yrm
Xrm Yrm |
293 | 292 | sumeq2dv 14433 |
. . . . . . 7
Xrm Yrm Yrm
Xrm Yrm |
294 | 262, 293 | eqtr2d 2657 |
. . . . . 6
Xrm Yrm Xrm Yrm
Yrm |
295 | | 1nn 11031 |
. . . . . . 7
|
296 | | bccl 13109 |
. . . . . . . . . . 11
|
297 | 6, 126, 296 | sylancl 694 |
. . . . . . . . . 10
|
298 | 297 | nn0cnd 11353 |
. . . . . . . . 9
|
299 | 298 | 3ad2ant3 1084 |
. . . . . . . 8
|
300 | | nnm1nn0 11334 |
. . . . . . . . . . 11
|
301 | 300 | 3ad2ant3 1084 |
. . . . . . . . . 10
|
302 | 218, 301 | expcld 13008 |
. . . . . . . . 9
Xrm |
303 | | 1nn0 11308 |
. . . . . . . . . . 11
|
304 | | expcl 12878 |
. . . . . . . . . . 11
Yrm
Yrm |
305 | 224, 303,
304 | sylancl 694 |
. . . . . . . . . 10
Yrm |
306 | | 1m1e0 11089 |
. . . . . . . . . . . . . 14
|
307 | 306 | oveq1i 6660 |
. . . . . . . . . . . . 13
|
308 | | 2cn 11091 |
. . . . . . . . . . . . . 14
|
309 | 308, 40 | div0i 10759 |
. . . . . . . . . . . . 13
|
310 | 307, 309 | eqtri 2644 |
. . . . . . . . . . . 12
|
311 | | 0nn0 11307 |
. . . . . . . . . . . 12
|
312 | 310, 311 | eqeltri 2697 |
. . . . . . . . . . 11
|
313 | | expcl 12878 |
. . . . . . . . . . 11
|
314 | 230, 312,
313 | sylancl 694 |
. . . . . . . . . 10
|
315 | 305, 314 | mulcld 10060 |
. . . . . . . . 9
Yrm |
316 | 302, 315 | mulcld 10060 |
. . . . . . . 8
Xrm Yrm |
317 | 299, 316 | mulcld 10060 |
. . . . . . 7
Xrm Yrm |
318 | | oveq2 6658 |
. . . . . . . . 9
|
319 | | oveq2 6658 |
. . . . . . . . . . 11
|
320 | 319 | oveq2d 6666 |
. . . . . . . . . 10
Xrm
Xrm |
321 | | oveq2 6658 |
. . . . . . . . . . 11
Yrm
Yrm |
322 | | oveq1 6657 |
. . . . . . . . . . . . 13
|
323 | 322 | oveq1d 6665 |
. . . . . . . . . . . 12
|
324 | 323 | oveq2d 6666 |
. . . . . . . . . . 11
|
325 | 321, 324 | oveq12d 6668 |
. . . . . . . . . 10
Yrm Yrm |
326 | 320, 325 | oveq12d 6668 |
. . . . . . . . 9
Xrm Yrm Xrm
Yrm |
327 | 318, 326 | oveq12d 6668 |
. . . . . . . 8
Xrm Yrm Xrm Yrm |
328 | 327 | sumsn 14475 |
. . . . . . 7
Xrm Yrm Xrm
Yrm Xrm Yrm |
329 | 295, 317,
328 | sylancr 695 |
. . . . . 6
Xrm Yrm Xrm Yrm |
330 | 294, 329 | oveq12d 6668 |
. . . . 5
Xrm Yrm Xrm
Yrm
Xrm
Yrm Yrm Xrm Yrm |
331 | 97, 258, 330 | 3eqtrd 2660 |
. . . 4
Yrm Xrm Yrm
Yrm Xrm Yrm |
332 | | bcn1 13100 |
. . . . . . 7
|
333 | 7, 332 | syl 17 |
. . . . . 6
|
334 | 333 | eqcomd 2628 |
. . . . 5
|
335 | 224 | exp1d 13003 |
. . . . . . . 8
Yrm Yrm |
336 | 310 | a1i 11 |
. . . . . . . . . 10
|
337 | 336 | oveq2d 6666 |
. . . . . . . . 9
|
338 | 230 | exp0d 13002 |
. . . . . . . . 9
|
339 | 337, 338 | eqtrd 2656 |
. . . . . . . 8
|
340 | 335, 339 | oveq12d 6668 |
. . . . . . 7
Yrm
Yrm |
341 | 224 | mulid1d 10057 |
. . . . . . 7
Yrm Yrm |
342 | 340, 341 | eqtr2d 2657 |
. . . . . 6
Yrm Yrm |
343 | 342 | oveq2d 6666 |
. . . . 5
Xrm
Yrm Xrm
Yrm |
344 | 334, 343 | oveq12d 6668 |
. . . 4
Xrm Yrm Xrm Yrm |
345 | 331, 344 | oveq12d 6668 |
. . 3
Yrm
Xrm
Yrm
Xrm Yrm
Yrm Xrm Yrm
Xrm Yrm |
346 | 5, 261 | fsumcl 14464 |
. . . . 5
Xrm Yrm |
347 | 346, 260 | mulcld 10060 |
. . . 4
Xrm Yrm Yrm |
348 | 347, 317 | pncand 10393 |
. . 3
Xrm Yrm
Yrm Xrm Yrm
Xrm Yrm
Xrm
Yrm Yrm |
349 | 345, 348 | eqtrd 2656 |
. 2
Yrm
Xrm
Yrm Xrm Yrm
Yrm |
350 | 95, 349 | breqtrrd 4681 |
1
Yrm
Yrm
Xrm
Yrm |