Step |
Hyp |
Ref |
Expression |
0 |
|
cquot |
|- quot |
1 |
|
vf |
|- f |
2 |
|
cply |
|- Poly |
3 |
|
cc |
|- CC |
4 |
3 2
|
cfv |
|- ( Poly ` CC ) |
5 |
|
vg |
|- g |
6 |
|
c0p |
|- 0p |
7 |
6
|
csn |
|- { 0p } |
8 |
4 7
|
cdif |
|- ( ( Poly ` CC ) \ { 0p } ) |
9 |
|
vq |
|- q |
10 |
1
|
cv |
|- f |
11 |
|
cmin |
|- - |
12 |
11
|
cof |
|- oF - |
13 |
5
|
cv |
|- g |
14 |
|
cmul |
|- x. |
15 |
14
|
cof |
|- oF x. |
16 |
9
|
cv |
|- q |
17 |
13 16 15
|
co |
|- ( g oF x. q ) |
18 |
10 17 12
|
co |
|- ( f oF - ( g oF x. q ) ) |
19 |
|
vr |
|- r |
20 |
19
|
cv |
|- r |
21 |
20 6
|
wceq |
|- r = 0p |
22 |
|
cdgr |
|- deg |
23 |
20 22
|
cfv |
|- ( deg ` r ) |
24 |
|
clt |
|- < |
25 |
13 22
|
cfv |
|- ( deg ` g ) |
26 |
23 25 24
|
wbr |
|- ( deg ` r ) < ( deg ` g ) |
27 |
21 26
|
wo |
|- ( r = 0p \/ ( deg ` r ) < ( deg ` g ) ) |
28 |
27 19 18
|
wsbc |
|- [. ( f oF - ( g oF x. q ) ) / r ]. ( r = 0p \/ ( deg ` r ) < ( deg ` g ) ) |
29 |
28 9 4
|
crio |
|- ( iota_ q e. ( Poly ` CC ) [. ( f oF - ( g oF x. q ) ) / r ]. ( r = 0p \/ ( deg ` r ) < ( deg ` g ) ) ) |
30 |
1 5 4 8 29
|
cmpo |
|- ( f e. ( Poly ` CC ) , g e. ( ( Poly ` CC ) \ { 0p } ) |-> ( iota_ q e. ( Poly ` CC ) [. ( f oF - ( g oF x. q ) ) / r ]. ( r = 0p \/ ( deg ` r ) < ( deg ` g ) ) ) ) |
31 |
0 30
|
wceq |
|- quot = ( f e. ( Poly ` CC ) , g e. ( ( Poly ` CC ) \ { 0p } ) |-> ( iota_ q e. ( Poly ` CC ) [. ( f oF - ( g oF x. q ) ) / r ]. ( r = 0p \/ ( deg ` r ) < ( deg ` g ) ) ) ) |