MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-quot Structured version   Visualization version   GIF version

Definition df-quot 23767
Description: Define the quotient function on polynomials. This is the 𝑞 of the expression 𝑓 = 𝑔 · 𝑞 + 𝑟 in the division algorithm. (Contributed by Mario Carneiro, 23-Jul-2014.)
Assertion
Ref Expression
df-quot quot = (𝑓 ∈ (Poly‘ℂ), 𝑔 ∈ ((Poly‘ℂ) ∖ {0𝑝}) ↦ (𝑞 ∈ (Poly‘ℂ)[(𝑓𝑓 − (𝑔𝑓 · 𝑞)) / 𝑟](𝑟 = 0𝑝 ∨ (deg‘𝑟) < (deg‘𝑔))))
Distinct variable group:   𝑓,𝑔,𝑞,𝑟

Detailed syntax breakdown of Definition df-quot
StepHypRef Expression
1 cquot 23766 . 2 class quot
2 vf . . 3 setvar 𝑓
3 vg . . 3 setvar 𝑔
4 cc 9790 . . . 4 class
5 cply 23661 . . . 4 class Poly
64, 5cfv 5790 . . 3 class (Poly‘ℂ)
7 c0p 23159 . . . . 5 class 0𝑝
87csn 4124 . . . 4 class {0𝑝}
96, 8cdif 3536 . . 3 class ((Poly‘ℂ) ∖ {0𝑝})
10 vr . . . . . . . 8 setvar 𝑟
1110cv 1473 . . . . . . 7 class 𝑟
1211, 7wceq 1474 . . . . . 6 wff 𝑟 = 0𝑝
13 cdgr 23664 . . . . . . . 8 class deg
1411, 13cfv 5790 . . . . . . 7 class (deg‘𝑟)
153cv 1473 . . . . . . . 8 class 𝑔
1615, 13cfv 5790 . . . . . . 7 class (deg‘𝑔)
17 clt 9930 . . . . . . 7 class <
1814, 16, 17wbr 4577 . . . . . 6 wff (deg‘𝑟) < (deg‘𝑔)
1912, 18wo 381 . . . . 5 wff (𝑟 = 0𝑝 ∨ (deg‘𝑟) < (deg‘𝑔))
202cv 1473 . . . . . 6 class 𝑓
21 vq . . . . . . . 8 setvar 𝑞
2221cv 1473 . . . . . . 7 class 𝑞
23 cmul 9797 . . . . . . . 8 class ·
2423cof 6770 . . . . . . 7 class 𝑓 ·
2515, 22, 24co 6527 . . . . . 6 class (𝑔𝑓 · 𝑞)
26 cmin 10117 . . . . . . 7 class
2726cof 6770 . . . . . 6 class 𝑓
2820, 25, 27co 6527 . . . . 5 class (𝑓𝑓 − (𝑔𝑓 · 𝑞))
2919, 10, 28wsbc 3401 . . . 4 wff [(𝑓𝑓 − (𝑔𝑓 · 𝑞)) / 𝑟](𝑟 = 0𝑝 ∨ (deg‘𝑟) < (deg‘𝑔))
3029, 21, 6crio 6488 . . 3 class (𝑞 ∈ (Poly‘ℂ)[(𝑓𝑓 − (𝑔𝑓 · 𝑞)) / 𝑟](𝑟 = 0𝑝 ∨ (deg‘𝑟) < (deg‘𝑔)))
312, 3, 6, 9, 30cmpt2 6529 . 2 class (𝑓 ∈ (Poly‘ℂ), 𝑔 ∈ ((Poly‘ℂ) ∖ {0𝑝}) ↦ (𝑞 ∈ (Poly‘ℂ)[(𝑓𝑓 − (𝑔𝑓 · 𝑞)) / 𝑟](𝑟 = 0𝑝 ∨ (deg‘𝑟) < (deg‘𝑔))))
321, 31wceq 1474 1 wff quot = (𝑓 ∈ (Poly‘ℂ), 𝑔 ∈ ((Poly‘ℂ) ∖ {0𝑝}) ↦ (𝑞 ∈ (Poly‘ℂ)[(𝑓𝑓 − (𝑔𝑓 · 𝑞)) / 𝑟](𝑟 = 0𝑝 ∨ (deg‘𝑟) < (deg‘𝑔))))
Colors of variables: wff setvar class
This definition is referenced by:  quotval  23768
  Copyright terms: Public domain W3C validator