---

Step * 4 1 of Lemma rat_term_polynomial


1. left : rat_term()
2. right : rat_term()
3. v4 : iPolynomial()
4. v5 : iPolynomial()
5. rat_term_to_ipolys(left) = <v4, v5> ∈ (iPolynomial() × iPolynomial())
6. v2 : iPolynomial()
7. v3 : iPolynomial()
8. rat_term_to_ipolys(right) = <v2, v3> ∈ (iPolynomial() × iPolynomial())
9. f : ℤ ⟶ ℝ
10. P1 : ℙ
11. v8 : ℝ supposing P1
12. rat_term_to_real(f;right) = <P1, v8> ∈ (P:ℙ × ℝ supposing P)
13. P : ℙ
14. v7 : ⋂:P. ℝ
15. rat_term_to_real(f;left) = <P, v7> ∈ (P:ℙ × ℝ supposing P)
16. P
17. P1
18. real_term_value(f;ipolynomial-term(v3)) ≠ r0
19. v8 = (real_term_value(f;ipolynomial-term(v2))/real_term_value(f;ipolynomial-term(v3)))
20. real_term_value(f;ipolynomial-term(v5)) ≠ r0
21. v7 = (real_term_value(f;ipolynomial-term(v4))/real_term_value(f;ipolynomial-term(v5)))
22. real_term_value(f;ipolynomial-term(minus-poly(v2))) = real_term_value(f;"-"ipolynomial-term(v2))
⊢ real_term_value(f;ipolynomial-term(mul-ipoly(v5;v3))) ≠ r0
∧ ((v7 - v8)
  = (real_term_value(f;ipolynomial-term(add-ipoly(mul-ipoly(v4;v3);mul-ipoly(minus-poly(v2);v5))))/...))
BY
{ (((InstLemma `mul-ipoly-req` [⌜v5⌝;⌜v3⌝]⋅ THENA Auto) THEN (D -1 With ⌜f⌝  THENA Auto))
   THEN ((InstLemma `mul-ipoly-req` [⌜minus-poly(v2)⌝;⌜v5⌝]⋅ THENA Auto) THEN (D -1 With ⌜f⌝  THENA Auto))
   THEN (InstLemma `mul-ipoly-req` [⌜v4⌝;⌜v3⌝]⋅ THENA Auto)
   THEN (D -1 With ⌜f⌝  THENA Auto)
   THEN (InstLemma `add-ipoly-req` [⌜mul-ipoly(v4;v3)⌝;⌜mul-ipoly(minus-poly(v2);v5)⌝]⋅ THENA Auto)
   THEN (D -1 With ⌜f⌝  THENA Auto)
   THEN All (Unfold `real_term_value`)
   THEN All Reduce
   THEN All (Fold `real_term_value`)
   THEN RepeatFor 9 (MoveToConcl (-1))
   THEN GenConclTerms Auto [⌜real_term_value(f;ipolynomial-term(v3))⌝;⌜real_term_value(f;ipolynomial-term(v5))⌝;
   ⌜real_term_value(f;ipolynomial-term(v2))⌝;⌜real_term_value(f;ipolynomial-term(v4))⌝]⋅
   THEN GenConclTerms Auto [
   ⌜real_term_value(f;ipolynomial-term(add-ipoly(mul-ipoly(v4;v3);mul-ipoly(minus-poly(v2);v5))))⌝]⋅
   THEN GenConclTerms Auto [⌜real_term_value(f;ipolynomial-term(mul-ipoly(v5;v3)))⌝;
   ⌜real_term_value(f;ipolynomial-term(mul-ipoly(minus-poly(v2);v5)))⌝;
   ⌜real_term_value(f;ipolynomial-term(mul-ipoly(v4;v3)))⌝]⋅
   THEN (GenConclTerm ⌜real_term_value(f;ipolynomial-term(minus-poly(v2)))⌝⋅ THENA Auto)
   THEN ((GenConcl ⌜v7 = r ∈ ℝ⌝⋅ THENA Auto) THEN (GenConcl ⌜v8 = q ∈ ℝ⌝⋅ THENA Auto))
   THEN All Thin) }

1
1. v : ℝ
2. v9 : ℝ
3. v10 : ℝ
4. v11 : ℝ
5. v12 : ℝ
6. v13 : ℝ
7. v14 : ℝ
8. v15 : ℝ
9. v16 : ℝ
10. r : ℝ
11. q : ℝ
⊢ v ≠ r0
⇒ (q = (v10/v))
⇒ v9 ≠ r0
⇒ (r = (v11/v9))
⇒ (v16 = -(v10))
⇒ (v13 = (v9 * v))
⇒ (v14 = (v16 * v9))
⇒ (v15 = (v11 * v))
⇒ (v12 = (v15 + v14))
⇒ (v13 ≠ r0 ∧ ((r - q) = (v12/v13)))

---

Latex:

---

Latex:

1.  left  :  rat\_term()
2.  right  :  rat\_term()
3.  v4  :  iPolynomial()
4.  v5  :  iPolynomial()
5.  rat\_term\_to\_ipolys(left)  =  <v4,  v5>
6.  v2  :  iPolynomial()
7.  v3  :  iPolynomial()
8.  rat\_term\_to\_ipolys(right)  =  <v2,  v3>
9.  f  :  \mBbbZ{}  {}\mrightarrow{}  \mBbbR{}
10.  P1  :  \mBbbP{}
11.  v8  :  \mBbbR{}  supposing  P1
12.  rat\_term\_to\_real(f;right)  =  <P1,  v8>
13.  P  :  \mBbbP{}
14.  v7  :  \mcap{}:P.  \mBbbR{}
15.  rat\_term\_to\_real(f;left)  =  <P,  v7>
16.  P
17.  P1
18.  real\_term\_value(f;ipolynomial-term(v3))  \mneq{}  r0
19.  v8  =  (real\_term\_value(f;ipolynomial-term(v2))/real\_term\_value(f;ipolynomial-term(v3)))
20.  real\_term\_value(f;ipolynomial-term(v5))  \mneq{}  r0
21.  v7  =  (real\_term\_value(f;ipolynomial-term(v4))/real\_term\_value(f;ipolynomial-term(v5)))
22.  real\_term\_value(f;ipolynomial-term(minus-poly(v2)))  =  real\_term\_value(f;"-"ipolynomial-term(v2))
\mvdash{}  real\_term\_value(f;ipolynomial-term(mul-ipoly(v5;v3)))  \mneq{}  r0
\mwedge{}  ((v7  -  v8)
    =  (real\_term\_value(f;ipolynomial-term(add-ipoly(mul-ipoly(v4;v3);mul-ipoly(...;v5))))/...))


By

---

Latex:
(((InstLemma  `mul-ipoly-req`  [\mkleeneopen{}v5\mkleeneclose{};\mkleeneopen{}v3\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  (D  -1  With  \mkleeneopen{}f\mkleeneclose{}    THENA  Auto))
  THEN  ((InstLemma  `mul-ipoly-req`  [\mkleeneopen{}minus-poly(v2)\mkleeneclose{};\mkleeneopen{}v5\mkleeneclose{}]\mcdot{}  THENA  Auto)
              THEN  (D  -1  With  \mkleeneopen{}f\mkleeneclose{}    THENA  Auto)
              )
  THEN  (InstLemma  `mul-ipoly-req`  [\mkleeneopen{}v4\mkleeneclose{};\mkleeneopen{}v3\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (D  -1  With  \mkleeneopen{}f\mkleeneclose{}    THENA  Auto)
  THEN  (InstLemma  `add-ipoly-req`  [\mkleeneopen{}mul-ipoly(v4;v3)\mkleeneclose{};\mkleeneopen{}mul-ipoly(minus-poly(v2);v5)\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (D  -1  With  \mkleeneopen{}f\mkleeneclose{}    THENA  Auto)
  THEN  All  (Unfold  `real\_term\_value`)
  THEN  All  Reduce
  THEN  All  (Fold  `real\_term\_value`)
  THEN  RepeatFor  9  (MoveToConcl  (-1))
  THEN  GenConclTerms  Auto  [\mkleeneopen{}real\_term\_value(f;ipolynomial-term(v3))\mkleeneclose{};
  \mkleeneopen{}real\_term\_value(f;ipolynomial-term(v5))\mkleeneclose{};\mkleeneopen{}real\_term\_value(f;ipolynomial-term(v2))\mkleeneclose{};
  \mkleeneopen{}real\_term\_value(f;ipolynomial-term(v4))\mkleeneclose{}]\mcdot{}
  THEN  GenConclTerms  Auto  [
  \mkleeneopen{}real\_term\_value(f;ipolynomial-term(add-ipoly(mul-ipoly(v4;v3);mul-ipoly(minus-poly(v2);v5))))\mkleeneclose{}]\mcdot{}
  THEN  GenConclTerms  Auto  [\mkleeneopen{}real\_term\_value(f;ipolynomial-term(mul-ipoly(v5;v3)))\mkleeneclose{};
  \mkleeneopen{}real\_term\_value(f;ipolynomial-term(mul-ipoly(minus-poly(v2);v5)))\mkleeneclose{};
  \mkleeneopen{}real\_term\_value(f;ipolynomial-term(mul-ipoly(v4;v3)))\mkleeneclose{}]\mcdot{}
  THEN  (GenConclTerm  \mkleeneopen{}real\_term\_value(f;ipolynomial-term(minus-poly(v2)))\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  ((GenConcl  \mkleeneopen{}v7  =  r\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  (GenConcl  \mkleeneopen{}v8  =  q\mkleeneclose{}\mcdot{}  THENA  Auto))
  THEN  All  Thin)

---

Home Index