Step | Hyp | Ref
| Expression |
1 | | cqpa 34634 |
. 2
class
_Qp |
2 | | vp |
. . 3
setvar š |
3 | | cprime 16607 |
. . 3
class
ā |
4 | | vr |
. . . 4
setvar š |
5 | 2 | cv 1540 |
. . . . 5
class š |
6 | | cqp 34632 |
. . . . 5
class
Qp |
7 | 5, 6 | cfv 6543 |
. . . 4
class
(Qpāš) |
8 | 4 | cv 1540 |
. . . . 5
class š |
9 | | vn |
. . . . . 6
setvar š |
10 | | cn 12211 |
. . . . . 6
class
ā |
11 | | vf |
. . . . . . . . . . 11
setvar š |
12 | 11 | cv 1540 |
. . . . . . . . . 10
class š |
13 | | cdg1 25568 |
. . . . . . . . . 10
class
deg1 |
14 | 8, 12, 13 | co 7408 |
. . . . . . . . 9
class (š deg1 š) |
15 | 9 | cv 1540 |
. . . . . . . . 9
class š |
16 | | cle 11248 |
. . . . . . . . 9
class
ā¤ |
17 | 14, 15, 16 | wbr 5148 |
. . . . . . . 8
wff (š deg1 š) ā¤ š |
18 | | vd |
. . . . . . . . . . . . 13
setvar š |
19 | 18 | cv 1540 |
. . . . . . . . . . . 12
class š |
20 | 19 | ccnv 5675 |
. . . . . . . . . . 11
class ā”š |
21 | | cz 12557 |
. . . . . . . . . . . 12
class
ā¤ |
22 | | cc0 11109 |
. . . . . . . . . . . . 13
class
0 |
23 | 22 | csn 4628 |
. . . . . . . . . . . 12
class
{0} |
24 | 21, 23 | cdif 3945 |
. . . . . . . . . . 11
class (ā¤
ā {0}) |
25 | 20, 24 | cima 5679 |
. . . . . . . . . 10
class (ā”š ā (ā¤ ā
{0})) |
26 | | cfz 13483 |
. . . . . . . . . . 11
class
... |
27 | 22, 15, 26 | co 7408 |
. . . . . . . . . 10
class
(0...š) |
28 | 25, 27 | wss 3948 |
. . . . . . . . 9
wff (ā”š ā (ā¤ ā {0})) ā
(0...š) |
29 | | cco1 21701 |
. . . . . . . . . . 11
class
coe1 |
30 | 12, 29 | cfv 6543 |
. . . . . . . . . 10
class
(coe1āš) |
31 | 30 | crn 5677 |
. . . . . . . . 9
class ran
(coe1āš) |
32 | 28, 18, 31 | wral 3061 |
. . . . . . . 8
wff
āš ā ran
(coe1āš)(ā”š ā (ā¤ ā {0})) ā
(0...š) |
33 | 17, 32 | wa 396 |
. . . . . . 7
wff ((š deg1 š) ā¤ š ā§ āš ā ran (coe1āš)(ā”š ā (ā¤ ā {0})) ā
(0...š)) |
34 | | cpl1 21700 |
. . . . . . . 8
class
Poly1 |
35 | 8, 34 | cfv 6543 |
. . . . . . 7
class
(Poly1āš) |
36 | 33, 11, 35 | crab 3432 |
. . . . . 6
class {š ā
(Poly1āš)
ā£ ((š deg1
š) ā¤ š ā§ āš ā ran (coe1āš)(ā”š ā (ā¤ ā {0})) ā
(0...š))} |
37 | 9, 10, 36 | cmpt 5231 |
. . . . 5
class (š ā ā ā¦ {š ā
(Poly1āš)
ā£ ((š deg1
š) ā¤ š ā§ āš ā ran (coe1āš)(ā”š ā (ā¤ ā {0})) ā
(0...š))}) |
38 | | cpsl 34619 |
. . . . 5
class
polySplitLim |
39 | 8, 37, 38 | co 7408 |
. . . 4
class (š polySplitLim (š ā ā ā¦ {š ā
(Poly1āš)
ā£ ((š deg1
š) ā¤ š ā§ āš ā ran (coe1āš)(ā”š ā (ā¤ ā {0})) ā
(0...š))})) |
40 | 4, 7, 39 | csb 3893 |
. . 3
class
ā¦(Qpāš) / šā¦(š polySplitLim (š ā ā ā¦ {š ā (Poly1āš) ā£ ((š deg1 š) ā¤ š ā§ āš ā ran (coe1āš)(ā”š ā (ā¤ ā {0})) ā
(0...š))})) |
41 | 2, 3, 40 | cmpt 5231 |
. 2
class (š ā ā ā¦
ā¦(Qpāš)
/ šā¦(š polySplitLim (š ā ā ā¦ {š ā
(Poly1āš)
ā£ ((š deg1
š) ā¤ š ā§ āš ā ran (coe1āš)(ā”š ā (ā¤ ā {0})) ā
(0...š))}))) |
42 | 1, 41 | wceq 1541 |
1
wff _Qp =
(š ā ā ā¦
ā¦(Qpāš)
/ šā¦(š polySplitLim (š ā ā ā¦ {š ā
(Poly1āš)
ā£ ((š deg1
š) ā¤ š ā§ āš ā ran (coe1āš)(ā”š ā (ā¤ ā {0})) ā
(0...š))}))) |