Step | Hyp | Ref
| Expression |
1 | | pntlem1.r |
. . . . . . . . . 10
ψ |
2 | | pntlem1.a |
. . . . . . . . . 10
|
3 | | pntlem1.b |
. . . . . . . . . 10
|
4 | | pntlem1.l |
. . . . . . . . . 10
|
5 | | pntlem1.d |
. . . . . . . . . 10
|
6 | | pntlem1.f |
. . . . . . . . . 10
; |
7 | | pntlem1.u |
. . . . . . . . . 10
|
8 | | pntlem1.u2 |
. . . . . . . . . 10
|
9 | | pntlem1.e |
. . . . . . . . . 10
|
10 | | pntlem1.k |
. . . . . . . . . 10
|
11 | | pntlem1.y |
. . . . . . . . . 10
|
12 | | pntlem1.x |
. . . . . . . . . 10
|
13 | | pntlem1.c |
. . . . . . . . . 10
|
14 | | pntlem1.w |
. . . . . . . . . 10
; |
15 | | pntlem1.z |
. . . . . . . . . 10
|
16 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 13, 14, 15 | pntlemb 25286 |
. . . . . . . . 9
; |
17 | 16 | simp1d 1073 |
. . . . . . . 8
|
18 | 1 | pntrf 25252 |
. . . . . . . . 9
|
19 | 18 | ffvelrni 6358 |
. . . . . . . 8
|
20 | 17, 19 | syl 17 |
. . . . . . 7
|
21 | 20, 17 | rerpdivcld 11903 |
. . . . . 6
|
22 | 21 | recnd 10068 |
. . . . 5
|
23 | 22 | abscld 14175 |
. . . 4
|
24 | 17 | relogcld 24369 |
. . . 4
|
25 | 23, 24 | remulcld 10070 |
. . 3
|
26 | 7 | rpred 11872 |
. . . . . 6
|
27 | | 3re 11094 |
. . . . . . . 8
|
28 | 27 | a1i 11 |
. . . . . . 7
|
29 | 24, 28 | readdcld 10069 |
. . . . . 6
|
30 | 26, 29 | remulcld 10070 |
. . . . 5
|
31 | | 2re 11090 |
. . . . . . 7
|
32 | 31 | a1i 11 |
. . . . . 6
|
33 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10 | pntlemc 25284 |
. . . . . . . . . . 11
|
34 | 33 | simp3d 1075 |
. . . . . . . . . 10
|
35 | 34 | simp3d 1075 |
. . . . . . . . 9
|
36 | 35 | rpred 11872 |
. . . . . . . 8
|
37 | 1, 2, 3, 4, 5, 6 | pntlemd 25283 |
. . . . . . . . . . . 12
|
38 | 37 | simp1d 1073 |
. . . . . . . . . . 11
|
39 | 33 | simp1d 1073 |
. . . . . . . . . . . 12
|
40 | | 2z 11409 |
. . . . . . . . . . . 12
|
41 | | rpexpcl 12879 |
. . . . . . . . . . . 12
|
42 | 39, 40, 41 | sylancl 694 |
. . . . . . . . . . 11
|
43 | 38, 42 | rpmulcld 11888 |
. . . . . . . . . 10
|
44 | | 3nn0 11310 |
. . . . . . . . . . . . 13
|
45 | | 2nn 11185 |
. . . . . . . . . . . . 13
|
46 | 44, 45 | decnncl 11518 |
. . . . . . . . . . . 12
; |
47 | | nnrp 11842 |
. . . . . . . . . . . 12
; ; |
48 | 46, 47 | ax-mp 5 |
. . . . . . . . . . 11
; |
49 | | rpmulcl 11855 |
. . . . . . . . . . 11
; ; |
50 | 48, 3, 49 | sylancr 695 |
. . . . . . . . . 10
; |
51 | 43, 50 | rpdivcld 11889 |
. . . . . . . . 9
; |
52 | 51 | rpred 11872 |
. . . . . . . 8
; |
53 | 36, 52 | remulcld 10070 |
. . . . . . 7
; |
54 | 53, 24 | remulcld 10070 |
. . . . . 6
; |
55 | 32, 54 | remulcld 10070 |
. . . . 5
; |
56 | 30, 55 | resubcld 10458 |
. . . 4
; |
57 | 13 | rpred 11872 |
. . . 4
|
58 | 56, 57 | readdcld 10069 |
. . 3
; |
59 | 7 | rpcnd 11874 |
. . . . . 6
|
60 | 53 | recnd 10068 |
. . . . . 6
; |
61 | 24 | recnd 10068 |
. . . . . 6
|
62 | 59, 60, 61 | subdird 10487 |
. . . . 5
; ; |
63 | 38 | rpcnd 11874 |
. . . . . . . . . . 11
|
64 | 42 | rpcnd 11874 |
. . . . . . . . . . 11
|
65 | 50 | rpcnne0d 11881 |
. . . . . . . . . . 11
; ; |
66 | | div23 10704 |
. . . . . . . . . . 11
; ; ; ; |
67 | 63, 64, 65, 66 | syl3anc 1326 |
. . . . . . . . . 10
; ; |
68 | 9 | oveq1i 6660 |
. . . . . . . . . . . 12
|
69 | 37 | simp2d 1074 |
. . . . . . . . . . . . . 14
|
70 | 69 | rpcnd 11874 |
. . . . . . . . . . . . 13
|
71 | 69 | rpne0d 11877 |
. . . . . . . . . . . . 13
|
72 | 59, 70, 71 | sqdivd 13021 |
. . . . . . . . . . . 12
|
73 | 68, 72 | syl5eq 2668 |
. . . . . . . . . . 11
|
74 | 73 | oveq2d 6666 |
. . . . . . . . . 10
; ; |
75 | 38, 50 | rpdivcld 11889 |
. . . . . . . . . . . 12
; |
76 | 75 | rpcnd 11874 |
. . . . . . . . . . 11
; |
77 | 59 | sqcld 13006 |
. . . . . . . . . . 11
|
78 | | rpexpcl 12879 |
. . . . . . . . . . . . 13
|
79 | 69, 40, 78 | sylancl 694 |
. . . . . . . . . . . 12
|
80 | 79 | rpcnne0d 11881 |
. . . . . . . . . . 11
|
81 | | divass 10703 |
. . . . . . . . . . . 12
; ; ; |
82 | | div23 10704 |
. . . . . . . . . . . 12
; ; ; |
83 | 81, 82 | eqtr3d 2658 |
. . . . . . . . . . 11
; ; ; |
84 | 76, 77, 80, 83 | syl3anc 1326 |
. . . . . . . . . 10
; ; |
85 | 67, 74, 84 | 3eqtrd 2660 |
. . . . . . . . 9
; ; |
86 | 85 | oveq2d 6666 |
. . . . . . . 8
; ; |
87 | | df-3 11080 |
. . . . . . . . . . . . 13
|
88 | 87 | oveq2i 6661 |
. . . . . . . . . . . 12
|
89 | | 2nn0 11309 |
. . . . . . . . . . . . 13
|
90 | | expp1 12867 |
. . . . . . . . . . . . 13
|
91 | 59, 89, 90 | sylancl 694 |
. . . . . . . . . . . 12
|
92 | 88, 91 | syl5eq 2668 |
. . . . . . . . . . 11
|
93 | 77, 59 | mulcomd 10061 |
. . . . . . . . . . 11
|
94 | 92, 93 | eqtrd 2656 |
. . . . . . . . . 10
|
95 | 94 | oveq2d 6666 |
. . . . . . . . 9
|
96 | 37 | simp3d 1075 |
. . . . . . . . . . 11
|
97 | 96 | rpcnd 11874 |
. . . . . . . . . 10
|
98 | 97, 59, 77 | mulassd 10063 |
. . . . . . . . 9
|
99 | | 1cnd 10056 |
. . . . . . . . . . . . . . 15
|
100 | 69 | rpreccld 11882 |
. . . . . . . . . . . . . . . 16
|
101 | 100 | rpcnd 11874 |
. . . . . . . . . . . . . . 15
|
102 | 99, 101, 59 | subdird 10487 |
. . . . . . . . . . . . . 14
|
103 | 59 | mulid2d 10058 |
. . . . . . . . . . . . . . 15
|
104 | 59, 70, 71 | divrec2d 10805 |
. . . . . . . . . . . . . . . 16
|
105 | 9, 104 | syl5req 2669 |
. . . . . . . . . . . . . . 15
|
106 | 103, 105 | oveq12d 6668 |
. . . . . . . . . . . . . 14
|
107 | 102, 106 | eqtr2d 2657 |
. . . . . . . . . . . . 13
|
108 | 107 | oveq1d 6665 |
. . . . . . . . . . . 12
; ; |
109 | 6 | oveq1i 6660 |
. . . . . . . . . . . . 13
; |
110 | 99, 101 | subcld 10392 |
. . . . . . . . . . . . . 14
|
111 | 75, 79 | rpdivcld 11889 |
. . . . . . . . . . . . . . 15
; |
112 | 111 | rpcnd 11874 |
. . . . . . . . . . . . . 14
; |
113 | 110, 112,
59 | mul32d 10246 |
. . . . . . . . . . . . 13
; ; |
114 | 109, 113 | syl5eq 2668 |
. . . . . . . . . . . 12
; |
115 | 108, 114 | eqtr4d 2659 |
. . . . . . . . . . 11
; |
116 | 115 | oveq1d 6665 |
. . . . . . . . . 10
; |
117 | 35 | rpcnd 11874 |
. . . . . . . . . . 11
|
118 | 117, 112,
77 | mulassd 10063 |
. . . . . . . . . 10
; ; |
119 | 116, 118 | eqtr3d 2658 |
. . . . . . . . 9
; |
120 | 95, 98, 119 | 3eqtr2d 2662 |
. . . . . . . 8
; |
121 | 86, 120 | eqtr4d 2659 |
. . . . . . 7
; |
122 | 121 | oveq2d 6666 |
. . . . . 6
;
|
123 | 122 | oveq1d 6665 |
. . . . 5
;
|
124 | 62, 123 | eqtr3d 2658 |
. . . 4
;
|
125 | 26, 24 | remulcld 10070 |
. . . . 5
|
126 | 125, 54 | resubcld 10458 |
. . . 4
; |
127 | 124, 126 | eqeltrrd 2702 |
. . 3
|
128 | 17 | rpred 11872 |
. . . . . . . 8
|
129 | 16 | simp2d 1074 |
. . . . . . . . 9
|
130 | 129 | simp1d 1073 |
. . . . . . . 8
|
131 | 128, 130 | rplogcld 24375 |
. . . . . . 7
|
132 | 32, 131 | rerpdivcld 11903 |
. . . . . 6
|
133 | | fzfid 12772 |
. . . . . . 7
|
134 | 17 | adantr 481 |
. . . . . . . . . . . . 13
|
135 | | elfznn 12370 |
. . . . . . . . . . . . . . 15
|
136 | 135 | adantl 482 |
. . . . . . . . . . . . . 14
|
137 | 136 | nnrpd 11870 |
. . . . . . . . . . . . 13
|
138 | 134, 137 | rpdivcld 11889 |
. . . . . . . . . . . 12
|
139 | 18 | ffvelrni 6358 |
. . . . . . . . . . . 12
|
140 | 138, 139 | syl 17 |
. . . . . . . . . . 11
|
141 | 140, 134 | rerpdivcld 11903 |
. . . . . . . . . 10
|
142 | 141 | recnd 10068 |
. . . . . . . . 9
|
143 | 142 | abscld 14175 |
. . . . . . . 8
|
144 | 137 | relogcld 24369 |
. . . . . . . 8
|
145 | 143, 144 | remulcld 10070 |
. . . . . . 7
|
146 | 133, 145 | fsumrecl 14465 |
. . . . . 6
|
147 | 132, 146 | remulcld 10070 |
. . . . 5
|
148 | 147, 57 | readdcld 10069 |
. . . 4
|
149 | 20 | recnd 10068 |
. . . . . . . . . . 11
|
150 | 149 | abscld 14175 |
. . . . . . . . . 10
|
151 | 150 | recnd 10068 |
. . . . . . . . 9
|
152 | 151, 61 | mulcld 10060 |
. . . . . . . 8
|
153 | 132 | recnd 10068 |
. . . . . . . . 9
|
154 | 140 | recnd 10068 |
. . . . . . . . . . . . 13
|
155 | 154 | abscld 14175 |
. . . . . . . . . . . 12
|
156 | 155, 144 | remulcld 10070 |
. . . . . . . . . . 11
|
157 | 133, 156 | fsumrecl 14465 |
. . . . . . . . . 10
|
158 | 157 | recnd 10068 |
. . . . . . . . 9
|
159 | 153, 158 | mulcld 10060 |
. . . . . . . 8
|
160 | 17 | rpcnd 11874 |
. . . . . . . 8
|
161 | 17 | rpne0d 11877 |
. . . . . . . 8
|
162 | 152, 159,
160, 161 | divsubdird 10840 |
. . . . . . 7
|
163 | 151, 61, 160, 161 | div23d 10838 |
. . . . . . . . 9
|
164 | 149, 160,
161 | absdivd 14194 |
. . . . . . . . . . 11
|
165 | 17 | rprege0d 11879 |
. . . . . . . . . . . . 13
|
166 | | absid 14036 |
. . . . . . . . . . . . 13
|
167 | 165, 166 | syl 17 |
. . . . . . . . . . . 12
|
168 | 167 | oveq2d 6666 |
. . . . . . . . . . 11
|
169 | 164, 168 | eqtrd 2656 |
. . . . . . . . . 10
|
170 | 169 | oveq1d 6665 |
. . . . . . . . 9
|
171 | 163, 170 | eqtr4d 2659 |
. . . . . . . 8
|
172 | 153, 158,
160, 161 | divassd 10836 |
. . . . . . . . 9
|
173 | 160 | adantr 481 |
. . . . . . . . . . . . . . . 16
|
174 | 161 | adantr 481 |
. . . . . . . . . . . . . . . 16
|
175 | 154, 173,
174 | absdivd 14194 |
. . . . . . . . . . . . . . 15
|
176 | 167 | adantr 481 |
. . . . . . . . . . . . . . . 16
|
177 | 176 | oveq2d 6666 |
. . . . . . . . . . . . . . 15
|
178 | 175, 177 | eqtrd 2656 |
. . . . . . . . . . . . . 14
|
179 | 178 | oveq1d 6665 |
. . . . . . . . . . . . 13
|
180 | 155 | recnd 10068 |
. . . . . . . . . . . . . 14
|
181 | 144 | recnd 10068 |
. . . . . . . . . . . . . 14
|
182 | 17 | rpcnne0d 11881 |
. . . . . . . . . . . . . . 15
|
183 | 182 | adantr 481 |
. . . . . . . . . . . . . 14
|
184 | | div23 10704 |
. . . . . . . . . . . . . 14
|
185 | 180, 181,
183, 184 | syl3anc 1326 |
. . . . . . . . . . . . 13
|
186 | 179, 185 | eqtr4d 2659 |
. . . . . . . . . . . 12
|
187 | 186 | sumeq2dv 14433 |
. . . . . . . . . . 11
|
188 | 156 | recnd 10068 |
. . . . . . . . . . . 12
|
189 | 133, 160,
188, 161 | fsumdivc 14518 |
. . . . . . . . . . 11
|
190 | 187, 189 | eqtr4d 2659 |
. . . . . . . . . 10
|
191 | 190 | oveq2d 6666 |
. . . . . . . . 9
|
192 | 172, 191 | eqtr4d 2659 |
. . . . . . . 8
|
193 | 171, 192 | oveq12d 6668 |
. . . . . . 7
|
194 | 162, 193 | eqtrd 2656 |
. . . . . 6
|
195 | | 1re 10039 |
. . . . . . . . 9
|
196 | | rexr 10085 |
. . . . . . . . 9
|
197 | | elioopnf 12267 |
. . . . . . . . 9
|
198 | 195, 196,
197 | mp2b 10 |
. . . . . . . 8
|
199 | 128, 130,
198 | sylanbrc 698 |
. . . . . . 7
|
200 | | pntlem1.C |
. . . . . . 7
|
201 | | fveq2 6191 |
. . . . . . . . . . . . 13
|
202 | 201 | fveq2d 6195 |
. . . . . . . . . . . 12
|
203 | | fveq2 6191 |
. . . . . . . . . . . 12
|
204 | 202, 203 | oveq12d 6668 |
. . . . . . . . . . 11
|
205 | 203 | oveq2d 6666 |
. . . . . . . . . . . 12
|
206 | | oveq2 6658 |
. . . . . . . . . . . . . . . . 17
|
207 | 206 | fveq2d 6195 |
. . . . . . . . . . . . . . . 16
|
208 | 207 | fveq2d 6195 |
. . . . . . . . . . . . . . 15
|
209 | | fveq2 6191 |
. . . . . . . . . . . . . . 15
|
210 | 208, 209 | oveq12d 6668 |
. . . . . . . . . . . . . 14
|
211 | 210 | cbvsumv 14426 |
. . . . . . . . . . . . 13
|
212 | | oveq1 6657 |
. . . . . . . . . . . . . . . 16
|
213 | 212 | fveq2d 6195 |
. . . . . . . . . . . . . . 15
|
214 | 213 | oveq2d 6666 |
. . . . . . . . . . . . . 14
|
215 | | simpl 473 |
. . . . . . . . . . . . . . . . . 18
|
216 | 215 | oveq1d 6665 |
. . . . . . . . . . . . . . . . 17
|
217 | 216 | fveq2d 6195 |
. . . . . . . . . . . . . . . 16
|
218 | 217 | fveq2d 6195 |
. . . . . . . . . . . . . . 15
|
219 | 218 | oveq1d 6665 |
. . . . . . . . . . . . . 14
|
220 | 214, 219 | sumeq12rdv 14438 |
. . . . . . . . . . . . 13
|
221 | 211, 220 | syl5eq 2668 |
. . . . . . . . . . . 12
|
222 | 205, 221 | oveq12d 6668 |
. . . . . . . . . . 11
|
223 | 204, 222 | oveq12d 6668 |
. . . . . . . . . 10
|
224 | | id 22 |
. . . . . . . . . 10
|
225 | 223, 224 | oveq12d 6668 |
. . . . . . . . 9
|
226 | 225 | breq1d 4663 |
. . . . . . . 8
|
227 | 226 | rspcv 3305 |
. . . . . . 7
|
228 | 199, 200,
227 | sylc 65 |
. . . . . 6
|
229 | 194, 228 | eqbrtrrd 4677 |
. . . . 5
|
230 | 25, 147, 57 | lesubadd2d 10626 |
. . . . 5
|
231 | 229, 230 | mpbid 222 |
. . . 4
|
232 | | 2cnd 11093 |
. . . . . . 7
|
233 | 143 | recnd 10068 |
. . . . . . . . 9
|
234 | 233, 181 | mulcld 10060 |
. . . . . . . 8
|
235 | 133, 234 | fsumcl 14464 |
. . . . . . 7
|
236 | 131 | rpne0d 11877 |
. . . . . . 7
|
237 | 232, 235,
61, 236 | div23d 10838 |
. . . . . 6
|
238 | 24 | resqcld 13035 |
. . . . . . . . . . . 12
|
239 | 52, 238 | remulcld 10070 |
. . . . . . . . . . 11
; |
240 | 36, 239 | remulcld 10070 |
. . . . . . . . . 10
; |
241 | | remulcl 10021 |
. . . . . . . . . 10
; ; |
242 | 31, 240, 241 | sylancr 695 |
. . . . . . . . 9
; |
243 | 30, 24 | remulcld 10070 |
. . . . . . . . 9
|
244 | | remulcl 10021 |
. . . . . . . . . 10
|
245 | 31, 146, 244 | sylancr 695 |
. . . . . . . . 9
|
246 | 26 | adantr 481 |
. . . . . . . . . . . . . . 15
|
247 | 246, 136 | nndivred 11069 |
. . . . . . . . . . . . . 14
|
248 | 247, 143 | resubcld 10458 |
. . . . . . . . . . . . 13
|
249 | 248, 144 | remulcld 10070 |
. . . . . . . . . . . 12
|
250 | 133, 249 | fsumrecl 14465 |
. . . . . . . . . . 11
|
251 | 32, 250 | remulcld 10070 |
. . . . . . . . . 10
|
252 | 243, 245 | resubcld 10458 |
. . . . . . . . . 10
|
253 | | pntlem1.m |
. . . . . . . . . . . 12
|
254 | | pntlem1.n |
. . . . . . . . . . . 12
|
255 | | pntlem1.U |
. . . . . . . . . . . 12
|
256 | | pntlem1.K |
. . . . . . . . . . . 12
|
257 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 13, 14, 15, 253, 254, 255, 256 | pntlemf 25294 |
. . . . . . . . . . 11
; |
258 | | 2pos 11112 |
. . . . . . . . . . . . 13
|
259 | 258 | a1i 11 |
. . . . . . . . . . . 12
|
260 | | lemul2 10876 |
. . . . . . . . . . . 12
;
;
; |
261 | 240, 250,
32, 259, 260 | syl112anc 1330 |
. . . . . . . . . . 11
;
; |
262 | 257, 261 | mpbid 222 |
. . . . . . . . . 10
; |
263 | 247 | recnd 10068 |
. . . . . . . . . . . . . . . 16
|
264 | 263, 233,
181 | subdird 10487 |
. . . . . . . . . . . . . . 15
|
265 | 264 | sumeq2dv 14433 |
. . . . . . . . . . . . . 14
|
266 | 247, 144 | remulcld 10070 |
. . . . . . . . . . . . . . . 16
|
267 | 266 | recnd 10068 |
. . . . . . . . . . . . . . 15
|
268 | 133, 267,
234 | fsumsub 14520 |
. . . . . . . . . . . . . 14
|
269 | 265, 268 | eqtrd 2656 |
. . . . . . . . . . . . 13
|
270 | 269 | oveq2d 6666 |
. . . . . . . . . . . 12
|
271 | 133, 266 | fsumrecl 14465 |
. . . . . . . . . . . . . 14
|
272 | 271 | recnd 10068 |
. . . . . . . . . . . . 13
|
273 | 232, 272,
235 | subdid 10486 |
. . . . . . . . . . . 12
|
274 | 270, 273 | eqtrd 2656 |
. . . . . . . . . . 11
|
275 | | remulcl 10021 |
. . . . . . . . . . . . 13
|
276 | 31, 271, 275 | sylancr 695 |
. . . . . . . . . . . 12
|
277 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 13, 14, 15, 253, 254, 255, 256 | pntlemk 25295 |
. . . . . . . . . . . 12
|
278 | 276, 243,
245, 277 | lesub1dd 10643 |
. . . . . . . . . . 11
|
279 | 274, 278 | eqbrtrd 4675 |
. . . . . . . . . 10
|
280 | 242, 251,
252, 262, 279 | letrd 10194 |
. . . . . . . . 9
;
|
281 | 242, 243,
245, 280 | lesubd 10631 |
. . . . . . . 8
; |
282 | 30 | recnd 10068 |
. . . . . . . . . 10
|
283 | 55 | recnd 10068 |
. . . . . . . . . 10
; |
284 | 282, 283,
61 | subdird 10487 |
. . . . . . . . 9
; ; |
285 | 54 | recnd 10068 |
. . . . . . . . . . . 12
; |
286 | 232, 285,
61 | mulassd 10063 |
. . . . . . . . . . 11
; ; |
287 | 60, 61, 61 | mulassd 10063 |
. . . . . . . . . . . . 13
; ; |
288 | 61 | sqvald 13005 |
. . . . . . . . . . . . . 14
|
289 | 288 | oveq2d 6666 |
. . . . . . . . . . . . 13
; ; |
290 | 51 | rpcnd 11874 |
. . . . . . . . . . . . . 14
; |
291 | 238 | recnd 10068 |
. . . . . . . . . . . . . 14
|
292 | 117, 290,
291 | mulassd 10063 |
. . . . . . . . . . . . 13
; ; |
293 | 287, 289,
292 | 3eqtr2d 2662 |
. . . . . . . . . . . 12
; ; |
294 | 293 | oveq2d 6666 |
. . . . . . . . . . 11
; ; |
295 | 286, 294 | eqtrd 2656 |
. . . . . . . . . 10
; ; |
296 | 295 | oveq2d 6666 |
. . . . . . . . 9
; ; |
297 | 284, 296 | eqtrd 2656 |
. . . . . . . 8
; ; |
298 | 281, 297 | breqtrrd 4681 |
. . . . . . 7
; |
299 | 245, 56, 131 | ledivmul2d 11926 |
. . . . . . 7
;
; |
300 | 298, 299 | mpbird 247 |
. . . . . 6
; |
301 | 237, 300 | eqbrtrrd 4677 |
. . . . 5
; |
302 | 147, 56, 57, 301 | leadd1dd 10641 |
. . . 4
; |
303 | 25, 148, 58, 231, 302 | letrd 10194 |
. . 3
; |
304 | | remulcl 10021 |
. . . . . . . . 9
|
305 | 26, 27, 304 | sylancl 694 |
. . . . . . . 8
|
306 | 305, 57 | readdcld 10069 |
. . . . . . 7
|
307 | 16 | simp3d 1075 |
. . . . . . . 8
; |
308 | 307 | simp3d 1075 |
. . . . . . 7
; |
309 | 306, 54, 125, 308 | leadd2dd 10642 |
. . . . . 6
; |
310 | 28 | recnd 10068 |
. . . . . . . . 9
|
311 | 59, 61, 310 | adddid 10064 |
. . . . . . . 8
|
312 | 311 | oveq1d 6665 |
. . . . . . 7
|
313 | 125 | recnd 10068 |
. . . . . . . 8
|
314 | 59, 310 | mulcld 10060 |
. . . . . . . 8
|
315 | 13 | rpcnd 11874 |
. . . . . . . 8
|
316 | 313, 314,
315 | addassd 10062 |
. . . . . . 7
|
317 | 312, 316 | eqtrd 2656 |
. . . . . 6
|
318 | 285 | 2timesd 11275 |
. . . . . . . 8
; ; ; |
319 | 318 | oveq2d 6666 |
. . . . . . 7
; ; ; ; ; |
320 | 313, 285,
285 | nppcan3d 10419 |
. . . . . . 7
; ; ; ; |
321 | 319, 320 | eqtrd 2656 |
. . . . . 6
; ; ; |
322 | 309, 317,
321 | 3brtr4d 4685 |
. . . . 5
; ; |
323 | 30, 57 | readdcld 10069 |
. . . . . 6
|
324 | 323, 55, 126 | lesubaddd 10624 |
. . . . 5
; ;
; ; |
325 | 322, 324 | mpbird 247 |
. . . 4
; ; |
326 | 282, 315,
283 | addsubd 10413 |
. . . 4
; ; |
327 | 325, 326,
124 | 3brtr3d 4684 |
. . 3
;
|
328 | 25, 58, 127, 303, 327 | letrd 10194 |
. 2
|
329 | | 3z 11410 |
. . . . . . 7
|
330 | | rpexpcl 12879 |
. . . . . . 7
|
331 | 7, 329, 330 | sylancl 694 |
. . . . . 6
|
332 | 96, 331 | rpmulcld 11888 |
. . . . 5
|
333 | 332 | rpred 11872 |
. . . 4
|
334 | 26, 333 | resubcld 10458 |
. . 3
|
335 | 23, 334, 131 | lemul1d 11915 |
. 2
|
336 | 328, 335 | mpbird 247 |
1
|