---

Step * 7 of Lemma rat_term_polynomial


1. num : rat_term()
2. v1 : iPolynomial()
3. v2 : iPolynomial()
4. rat_term_to_ipolys(num) = <v1, v2> ∈ (iPolynomial() × iPolynomial())
⊢ num ≡ ipolynomial-term(v1)/ipolynomial-term(v2)
⇒ rtermMinus(num) ≡ ipolynomial-term(minus-poly(v1))/ipolynomial-term(v2)
BY
{ (Intros
   THEN RepeatFor 2 (ParallelLast)
   THEN Unfold `rat_term_to_real` 0
   THEN Reduce 0
   THEN Try (Fold `rat_term_to_real` 0)
   THEN MoveToConcl (-1)
   THEN GenConclTerms Auto [⌜rat_term_to_real(f;num)⌝]⋅
   THEN DProdsAndUnions
   THEN Reduce 0
   THEN Auto) }

1
1. num : rat_term()
2. v1 : iPolynomial()
3. v2 : iPolynomial()
4. rat_term_to_ipolys(num) = <v1, v2> ∈ (iPolynomial() × iPolynomial())
5. ∀f:ℤ ⟶ ℝ
     let P,x = rat_term_to_real(f;num) 
     in P
        ⇒ (real_term_value(f;ipolynomial-term(v2)) ≠ r0
           ∧ (x = (real_term_value(f;ipolynomial-term(v1))/real_term_value(f;ipolynomial-term(v2)))))
6. f : ℤ ⟶ ℝ
7. P : ℙ
8. v3 : ⋂:P. ℝ
9. rat_term_to_real(f;num) = <P, v3> ∈ (P:ℙ × ℝ supposing P)
10. P
11. real_term_value(f;ipolynomial-term(v2)) ≠ r0
12. real_term_value(f;ipolynomial-term(v2)) ≠ r0
13. v3 = (real_term_value(f;ipolynomial-term(v1))/real_term_value(f;ipolynomial-term(v2)))
14. ℝ
⊢ -(v3) = (real_term_value(f;ipolynomial-term(minus-poly(v1)))/real_term_value(f;ipolynomial-term(v2)))

---

Latex:

---

Latex:

1.  num  :  rat\_term()
2.  v1  :  iPolynomial()
3.  v2  :  iPolynomial()
4.  rat\_term\_to\_ipolys(num)  =  <v1,  v2>
\mvdash{}  num  \mequiv{}  ipolynomial-term(v1)/ipolynomial-term(v2)
{}\mRightarrow{}  rtermMinus(num)  \mequiv{}  ipolynomial-term(minus-poly(v1))/ipolynomial-term(v2)


By

---

Latex:
(Intros
  THEN  RepeatFor  2  (ParallelLast)
  THEN  Unfold  `rat\_term\_to\_real`  0
  THEN  Reduce  0
  THEN  Try  (Fold  `rat\_term\_to\_real`  0)
  THEN  MoveToConcl  (-1)
  THEN  GenConclTerms  Auto  [\mkleeneopen{}rat\_term\_to\_real(f;num)\mkleeneclose{}]\mcdot{}
  THEN  DProdsAndUnions
  THEN  Reduce  0
  THEN  Auto)

---

Home Index