---

Step * 1 1 1 1 1 1 1 1 of Lemma assert-rat-term-eq


1. ∀r:rat_term(). let p,q = rat_term_to_ipolys(r) in r ≡ ipolynomial-term(p)/ipolynomial-term(q)
2. r1 : rat_term()
3. r2 : rat_term()
4. v4 : iPolynomial()
5. v5 : iPolynomial()
6. rat_term_to_ipolys(r1) = <v4, v5> ∈ (iPolynomial() × iPolynomial())
7. v2 : iPolynomial()
8. v3 : iPolynomial()
9. rat_term_to_ipolys(r2) = <v2, v3> ∈ (iPolynomial() × iPolynomial())
10. ↑null(add-ipoly(mul-ipoly(v4;v3);mul-ipoly(minus-poly(v2);v5)))
11. f : ℤ ⟶ ℝ
12. P1 : ℙ
13. v8 : ⋂:P1. ℝ
14. rat_term_to_real(f;r2) = <P1, v8> ∈ (P:ℙ × ℝ supposing P)
15. P : ℙ
16. v7 : ⋂:P. ℝ
17. rat_term_to_real(f;r1) = <P, v7> ∈ (P:ℙ × ℝ supposing P)
18. P
19. P1
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(v3)) ≠ r0
23. v8 = (real_term_value(f;ipolynomial-term(v2))/real_term_value(f;ipolynomial-term(v3)))
⊢ (real_term_value(f;ipolynomial-term(mul-ipoly(v4;v3)))
  = (real_term_value(f;ipolynomial-term(v4)) * real_term_value(f;ipolynomial-term(v3))))
⇒ (real_term_value(f;ipolynomial-term(mul-ipoly(minus-poly(v2);v5)))
   = (real_term_value(f;ipolynomial-term(minus-poly(v2))) * real_term_value(f;ipolynomial-term(v5))))
⇒ (real_term_value(f;ipolynomial-term(add-ipoly(mul-ipoly(v4;v3);mul-ipoly(minus-poly(v2);v5))))
   = (real_term_value(f;ipolynomial-term(mul-ipoly(v4;v3)))
     + real_term_value(f;ipolynomial-term(mul-ipoly(minus-poly(v2);v5)))))
⇒ (real_term_value(f;ipolynomial-term(minus-poly(v2))) = -(real_term_value(f;ipolynomial-term(v2))))
⇒ (real_term_value(f;ipolynomial-term(add-ipoly(mul-ipoly(v4;v3);mul-ipoly(minus-poly(v2);v5)))) = r0)
⇒ ((real_term_value(f;ipolynomial-term(v3)) * real_term_value(f;ipolynomial-term(v4)))
   = (real_term_value(f;ipolynomial-term(v2)) * real_term_value(f;ipolynomial-term(v5))))
BY
{ (GenConclTerms Auto [⌜real_term_value(f;ipolynomial-term(v3))⌝;⌜real_term_value(f;ipolynomial-term(v4))⌝;
   ⌜real_term_value(f;ipolynomial-term(v2))⌝;⌜real_term_value(f;ipolynomial-term(v5))⌝]⋅
   THEN GenConclTerms Auto [⌜real_term_value(f;ipolynomial-term(mul-ipoly(v4;v3)))⌝;
        ⌜real_term_value(f;ipolynomial-term(mul-ipoly(minus-poly(v2);v5)))⌝;
        ⌜real_term_value(f;ipolynomial-term(add-ipoly(mul-ipoly(v4;v3);mul-ipoly(minus-poly(v2);v5))))⌝]⋅
   ) }

1
1. ∀r:rat_term(). let p,q = rat_term_to_ipolys(r) in r ≡ ipolynomial-term(p)/ipolynomial-term(q)
2. r1 : rat_term()
3. r2 : rat_term()
4. v4 : iPolynomial()
5. v5 : iPolynomial()
6. rat_term_to_ipolys(r1) = <v4, v5> ∈ (iPolynomial() × iPolynomial())
7. v2 : iPolynomial()
8. v3 : iPolynomial()
9. rat_term_to_ipolys(r2) = <v2, v3> ∈ (iPolynomial() × iPolynomial())
10. ↑null(add-ipoly(mul-ipoly(v4;v3);mul-ipoly(minus-poly(v2);v5)))
11. f : ℤ ⟶ ℝ
12. P1 : ℙ
13. v8 : ⋂:P1. ℝ
14. rat_term_to_real(f;r2) = <P1, v8> ∈ (P:ℙ × ℝ supposing P)
15. P : ℙ
16. v7 : ⋂:P. ℝ
17. rat_term_to_real(f;r1) = <P, v7> ∈ (P:ℙ × ℝ supposing P)
18. P
19. P1
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(v3)) ≠ r0
23. v8 = (real_term_value(f;ipolynomial-term(v2))/real_term_value(f;ipolynomial-term(v3)))
24. v : ℝ
25. real_term_value(f;ipolynomial-term(v3)) = v ∈ ℝ
26. v9 : ℝ
27. real_term_value(f;ipolynomial-term(v4)) = v9 ∈ ℝ
28. v10 : ℝ
29. real_term_value(f;ipolynomial-term(v2)) = v10 ∈ ℝ
30. v11 : ℝ
31. real_term_value(f;ipolynomial-term(v5)) = v11 ∈ ℝ
32. v12 : ℝ
33. real_term_value(f;ipolynomial-term(mul-ipoly(v4;v3))) = v12 ∈ ℝ
34. v13 : ℝ
35. real_term_value(f;ipolynomial-term(mul-ipoly(minus-poly(v2);v5))) = v13 ∈ ℝ
36. v14 : ℝ
37. real_term_value(f;ipolynomial-term(add-ipoly(mul-ipoly(v4;v3);mul-ipoly(minus-poly(v2);v5)))) = v14 ∈ ℝ
⊢ (v12 = (v9 * v))
⇒ (v13 = (real_term_value(f;ipolynomial-term(minus-poly(v2))) * v11))
⇒ (v14 = (v12 + v13))
⇒ (real_term_value(f;ipolynomial-term(minus-poly(v2))) = -(v10))
⇒ (v14 = r0)
⇒ ((v * v9) = (v10 * v11))

---

Latex:

---

Latex:

1.  \mforall{}r:rat\_term().  let  p,q  =  rat\_term\_to\_ipolys(r)  in  r  \mequiv{}  ipolynomial-term(p)/ipolynomial-term(q)
2.  r1  :  rat\_term()
3.  r2  :  rat\_term()
4.  v4  :  iPolynomial()
5.  v5  :  iPolynomial()
6.  rat\_term\_to\_ipolys(r1)  =  <v4,  v5>
7.  v2  :  iPolynomial()
8.  v3  :  iPolynomial()
9.  rat\_term\_to\_ipolys(r2)  =  <v2,  v3>
10.  \muparrow{}null(add-ipoly(mul-ipoly(v4;v3);mul-ipoly(minus-poly(v2);v5)))
11.  f  :  \mBbbZ{}  {}\mrightarrow{}  \mBbbR{}
12.  P1  :  \mBbbP{}
13.  v8  :  \mcap{}:P1.  \mBbbR{}
14.  rat\_term\_to\_real(f;r2)  =  <P1,  v8>
15.  P  :  \mBbbP{}
16.  v7  :  \mcap{}:P.  \mBbbR{}
17.  rat\_term\_to\_real(f;r1)  =  <P,  v7>
18.  P
19.  P1
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(v3))  \mneq{}  r0
23.  v8  =  (real\_term\_value(f;ipolynomial-term(v2))/real\_term\_value(f;ipolynomial-term(v3)))
\mvdash{}  (real\_term\_value(f;ipolynomial-term(mul-ipoly(v4;v3)))
    =  (real\_term\_value(f;ipolynomial-term(v4))  *  real\_term\_value(f;ipolynomial-term(v3))))
{}\mRightarrow{}  (real\_term\_value(f;ipolynomial-term(mul-ipoly(minus-poly(v2);v5)))
      =  (real\_term\_value(f;ipolynomial-term(minus-poly(v2)))
          *  real\_term\_value(f;ipolynomial-term(v5))))
{}\mRightarrow{}  (real\_term\_value(f;ipolynomial-term(add-ipoly(mul-ipoly(v4;v3);mul-ipoly(minus-poly(v2);v5))))
      =  (real\_term\_value(f;ipolynomial-term(mul-ipoly(v4;v3)))
          +  real\_term\_value(f;ipolynomial-term(mul-ipoly(minus-poly(v2);v5)))))
{}\mRightarrow{}  (real\_term\_value(f;ipolynomial-term(minus-poly(v2)))
      =  -(real\_term\_value(f;ipolynomial-term(v2))))
{}\mRightarrow{}  (real\_term\_value(f;ipolynomial-term(add-ipoly(mul-ipoly(v4;v3);mul-ipoly(minus-poly(v2);v5))))
      =  r0)
{}\mRightarrow{}  ((real\_term\_value(f;ipolynomial-term(v3))  *  real\_term\_value(f;ipolynomial-term(v4)))
      =  (real\_term\_value(f;ipolynomial-term(v2))  *  real\_term\_value(f;ipolynomial-term(v5))))


By

---

Latex:
(GenConclTerms  Auto  [\mkleeneopen{}real\_term\_value(f;ipolynomial-term(v3))\mkleeneclose{};
  \mkleeneopen{}real\_term\_value(f;ipolynomial-term(v4))\mkleeneclose{};\mkleeneopen{}real\_term\_value(f;ipolynomial-term(v2))\mkleeneclose{};
  \mkleeneopen{}real\_term\_value(f;ipolynomial-term(v5))\mkleeneclose{}]\mcdot{}
  THEN  GenConclTerms  Auto  [\mkleeneopen{}real\_term\_value(f;ipolynomial-term(mul-ipoly(v4;v3)))\mkleeneclose{};
            \mkleeneopen{}real\_term\_value(f;ipolynomial-term(mul-ipoly(minus-poly(v2);v5)))\mkleeneclose{};
            ...]\mcdot{}
  )

---

Home Index