Step | Hyp | Ref
| Expression |
1 | | cqpa 34670 |
. 2
class
_Qp |
2 | | vp |
. . 3
setvar š |
3 | | cprime 16608 |
. . 3
class
ā |
4 | | vr |
. . . 4
setvar š |
5 | 2 | cv 1541 |
. . . . 5
class š |
6 | | cqp 34668 |
. . . . 5
class
Qp |
7 | 5, 6 | cfv 6544 |
. . . 4
class
(Qpāš) |
8 | 4 | cv 1541 |
. . . . 5
class š |
9 | | vn |
. . . . . 6
setvar š |
10 | | cn 12212 |
. . . . . 6
class
ā |
11 | | vf |
. . . . . . . . . . 11
setvar š |
12 | 11 | cv 1541 |
. . . . . . . . . 10
class š |
13 | | cdg1 25569 |
. . . . . . . . . 10
class
deg1 |
14 | 8, 12, 13 | co 7409 |
. . . . . . . . 9
class (š deg1 š) |
15 | 9 | cv 1541 |
. . . . . . . . 9
class š |
16 | | cle 11249 |
. . . . . . . . 9
class
ā¤ |
17 | 14, 15, 16 | wbr 5149 |
. . . . . . . 8
wff (š deg1 š) ā¤ š |
18 | | vd |
. . . . . . . . . . . . 13
setvar š |
19 | 18 | cv 1541 |
. . . . . . . . . . . 12
class š |
20 | 19 | ccnv 5676 |
. . . . . . . . . . 11
class ā”š |
21 | | cz 12558 |
. . . . . . . . . . . 12
class
ā¤ |
22 | | cc0 11110 |
. . . . . . . . . . . . 13
class
0 |
23 | 22 | csn 4629 |
. . . . . . . . . . . 12
class
{0} |
24 | 21, 23 | cdif 3946 |
. . . . . . . . . . 11
class (ā¤
ā {0}) |
25 | 20, 24 | cima 5680 |
. . . . . . . . . 10
class (ā”š ā (ā¤ ā
{0})) |
26 | | cfz 13484 |
. . . . . . . . . . 11
class
... |
27 | 22, 15, 26 | co 7409 |
. . . . . . . . . 10
class
(0...š) |
28 | 25, 27 | wss 3949 |
. . . . . . . . 9
wff (ā”š ā (ā¤ ā {0})) ā
(0...š) |
29 | | cco1 21702 |
. . . . . . . . . . 11
class
coe1 |
30 | 12, 29 | cfv 6544 |
. . . . . . . . . 10
class
(coe1āš) |
31 | 30 | crn 5678 |
. . . . . . . . 9
class ran
(coe1āš) |
32 | 28, 18, 31 | wral 3062 |
. . . . . . . 8
wff
āš ā ran
(coe1āš)(ā”š ā (ā¤ ā {0})) ā
(0...š) |
33 | 17, 32 | wa 397 |
. . . . . . 7
wff ((š deg1 š) ā¤ š ā§ āš ā ran (coe1āš)(ā”š ā (ā¤ ā {0})) ā
(0...š)) |
34 | | cpl1 21701 |
. . . . . . . 8
class
Poly1 |
35 | 8, 34 | cfv 6544 |
. . . . . . 7
class
(Poly1āš) |
36 | 33, 11, 35 | crab 3433 |
. . . . . 6
class {š ā
(Poly1āš)
ā£ ((š deg1
š) ā¤ š ā§ āš ā ran (coe1āš)(ā”š ā (ā¤ ā {0})) ā
(0...š))} |
37 | 9, 10, 36 | cmpt 5232 |
. . . . 5
class (š ā ā ā¦ {š ā
(Poly1āš)
ā£ ((š deg1
š) ā¤ š ā§ āš ā ran (coe1āš)(ā”š ā (ā¤ ā {0})) ā
(0...š))}) |
38 | | cpsl 34655 |
. . . . 5
class
polySplitLim |
39 | 8, 37, 38 | co 7409 |
. . . 4
class (š polySplitLim (š ā ā ā¦ {š ā
(Poly1āš)
ā£ ((š deg1
š) ā¤ š ā§ āš ā ran (coe1āš)(ā”š ā (ā¤ ā {0})) ā
(0...š))})) |
40 | 4, 7, 39 | csb 3894 |
. . 3
class
ā¦(Qpāš) / šā¦(š polySplitLim (š ā ā ā¦ {š ā (Poly1āš) ā£ ((š deg1 š) ā¤ š ā§ āš ā ran (coe1āš)(ā”š ā (ā¤ ā {0})) ā
(0...š))})) |
41 | 2, 3, 40 | cmpt 5232 |
. 2
class (š ā ā ā¦
ā¦(Qpāš)
/ šā¦(š polySplitLim (š ā ā ā¦ {š ā
(Poly1āš)
ā£ ((š deg1
š) ā¤ š ā§ āš ā ran (coe1āš)(ā”š ā (ā¤ ā {0})) ā
(0...š))}))) |
42 | 1, 41 | wceq 1542 |
1
wff _Qp =
(š ā ā ā¦
ā¦(Qpāš)
/ šā¦(š polySplitLim (š ā ā ā¦ {š ā
(Poly1āš)
ā£ ((š deg1
š) ā¤ š ā§ āš ā ran (coe1āš)(ā”š ā (ā¤ ā {0})) ā
(0...š))}))) |