Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  r1pval Structured version   Unicode version

Theorem r1pval 20079
 Description: Value of the polynomial remainder function. (Contributed by Stefan O'Rear, 28-Mar-2015.)
Hypotheses
Ref Expression
r1pval.e rem1p
r1pval.p Poly1
r1pval.b
r1pval.q quot1p
r1pval.t
r1pval.m
Assertion
Ref Expression
r1pval

Proof of Theorem r1pval
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 r1pval.p . . . . 5 Poly1
2 r1pval.b . . . . 5
31, 2elbasfv 13512 . . . 4
5 r1pval.e . . . 4 rem1p
6 fveq2 5728 . . . . . . . . . 10 Poly1 Poly1
76, 1syl6eqr 2486 . . . . . . . . 9 Poly1
87fveq2d 5732 . . . . . . . 8 Poly1
98, 2syl6eqr 2486 . . . . . . 7 Poly1
109csbeq1d 3257 . . . . . 6 Poly1 Poly1quot1pPoly1 Poly1quot1pPoly1
11 fvex 5742 . . . . . . . . 9
122, 11eqeltri 2506 . . . . . . . 8
1312a1i 11 . . . . . . 7
14 simpr 448 . . . . . . . 8
157fveq2d 5732 . . . . . . . . . . 11 Poly1
16 r1pval.m . . . . . . . . . . 11
1715, 16syl6eqr 2486 . . . . . . . . . 10 Poly1
18 eqidd 2437 . . . . . . . . . 10
197fveq2d 5732 . . . . . . . . . . . 12 Poly1
20 r1pval.t . . . . . . . . . . . 12
2119, 20syl6eqr 2486 . . . . . . . . . . 11 Poly1
22 fveq2 5728 . . . . . . . . . . . . 13 quot1p quot1p
23 r1pval.q . . . . . . . . . . . . 13 quot1p
2422, 23syl6eqr 2486 . . . . . . . . . . . 12 quot1p
2524oveqd 6098 . . . . . . . . . . 11 quot1p
26 eqidd 2437 . . . . . . . . . . 11
2721, 25, 26oveq123d 6102 . . . . . . . . . 10 quot1pPoly1
2817, 18, 27oveq123d 6102 . . . . . . . . 9 Poly1quot1pPoly1
2928adantr 452 . . . . . . . 8 Poly1quot1pPoly1
3014, 14, 29mpt2eq123dv 6136 . . . . . . 7 Poly1quot1pPoly1
3113, 30csbied 3293 . . . . . 6 Poly1quot1pPoly1
3210, 31eqtrd 2468 . . . . 5 Poly1 Poly1quot1pPoly1
33 df-r1p 20056 . . . . 5 rem1p Poly1 Poly1quot1pPoly1
3412, 12mpt2ex 6425 . . . . 5
3532, 33, 34fvmpt 5806 . . . 4 rem1p
365, 35syl5eq 2480 . . 3
374, 36syl 16 . 2
38 simpl 444 . . . 4
39 oveq12 6090 . . . . 5
40 simpr 448 . . . . 5
4139, 40oveq12d 6099 . . . 4
4238, 41oveq12d 6099 . . 3