---

Step * 7 1 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())
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)))
BY
{ ((RWO "-2" 0 THENA Auto) THEN (nRMul ⌜real_term_value(f;ipolynomial-term(v2))⌝ 0⋅ THENA 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. ℝ
⊢ -(real_term_value(f;ipolynomial-term(v1))) = real_term_value(f;ipolynomial-term(minus-poly(v1)))

---

Latex:

---

Latex:

1.  num  :  rat\_term()
2.  v1  :  iPolynomial()
3.  v2  :  iPolynomial()
4.  rat\_term\_to\_ipolys(num)  =  <v1,  v2>
5.  \mforall{}f:\mBbbZ{}  {}\mrightarrow{}  \mBbbR{}
          let  P,x  =  rat\_term\_to\_real(f;num) 
          in  P
                {}\mRightarrow{}  (real\_term\_value(f;ipolynomial-term(v2))  \mneq{}  r0
                      \mwedge{}  (x
                          =  (real\_term\_value(f;ipolynomial-term(v1))/real\_term\_value(f;ipolynomial-term(v2)))))
6.  f  :  \mBbbZ{}  {}\mrightarrow{}  \mBbbR{}
7.  P  :  \mBbbP{}
8.  v3  :  \mcap{}:P.  \mBbbR{}
9.  rat\_term\_to\_real(f;num)  =  <P,  v3>
10.  P
11.  real\_term\_value(f;ipolynomial-term(v2))  \mneq{}  r0
12.  real\_term\_value(f;ipolynomial-term(v2))  \mneq{}  r0
13.  v3  =  (real\_term\_value(f;ipolynomial-term(v1))/real\_term\_value(f;ipolynomial-term(v2)))
14.  \mBbbR{}
\mvdash{}  -(v3)
=  (real\_term\_value(f;ipolynomial-term(minus-poly(v1)))/real\_term\_value(f;ipolynomial-term(v2)))


By

---

Latex:
((RWO  "-2"  0  THENA  Auto)  THEN  (nRMul  \mkleeneopen{}real\_term\_value(f;ipolynomial-term(v2))\mkleeneclose{}  0\mcdot{}  THENA  Auto))

---

Home Index