---

Step * 3 1 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. v : ℝ
19. real_term_value(f;ipolynomial-term(v3)) = v ∈ ℝ
20. v9 : ℝ
21. real_term_value(f;ipolynomial-term(v5)) = v9 ∈ ℝ
22. v10 : ℝ
23. real_term_value(f;ipolynomial-term(v2)) = v10 ∈ ℝ
24. v11 : ℝ
25. real_term_value(f;ipolynomial-term(v4)) = v11 ∈ ℝ
26. v12 : ℝ
27. real_term_value(f;ipolynomial-term(add-ipoly(mul-ipoly(v4;v3);mul-ipoly(v2;v5)))) = v12 ∈ ℝ
28. v13 : ℝ
29. real_term_value(f;ipolynomial-term(mul-ipoly(v5;v3))) = v13 ∈ ℝ
30. v14 : ℝ
31. real_term_value(f;ipolynomial-term(mul-ipoly(v2;v5))) = v14 ∈ ℝ
32. v15 : ℝ
33. real_term_value(f;ipolynomial-term(mul-ipoly(v4;v3))) = v15 ∈ ℝ
34. r : ℝ
35. v7 = r ∈ ℝ
36. q : ℝ
37. v8 = q ∈ ℝ
⊢ v ≠ r0
⇒ (q = (v10/v))
⇒ v9 ≠ r0
⇒ (r = (v11/v9))
⇒ (v13 = (v9 * v))
⇒ (v14 = (v10 * v9))
⇒ (v15 = (v11 * v))
⇒ (v12 = (v15 + v14))
⇒ (v13 ≠ r0 ∧ ((r + q) = (v12/v13)))
BY
{ (All Thin THEN RepeatFor 8 ((D 0 THENA Auto))) }

1
1. v : ℝ
2. v9 : ℝ
3. v10 : ℝ
4. v11 : ℝ
5. v12 : ℝ
6. v13 : ℝ
7. v14 : ℝ
8. v15 : ℝ
9. r : ℝ
10. q : ℝ
11. v ≠ r0
12. q = (v10/v)
13. v9 ≠ r0
14. r = (v11/v9)
15. v13 = (v9 * v)
16. v14 = (v10 * v9)
17. v15 = (v11 * v)
18. 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.  v  :  \mBbbR{}
19.  real\_term\_value(f;ipolynomial-term(v3))  =  v
20.  v9  :  \mBbbR{}
21.  real\_term\_value(f;ipolynomial-term(v5))  =  v9
22.  v10  :  \mBbbR{}
23.  real\_term\_value(f;ipolynomial-term(v2))  =  v10
24.  v11  :  \mBbbR{}
25.  real\_term\_value(f;ipolynomial-term(v4))  =  v11
26.  v12  :  \mBbbR{}
27.  real\_term\_value(f;ipolynomial-term(add-ipoly(mul-ipoly(v4;v3);mul-ipoly(v2;v5))))  =  v12
28.  v13  :  \mBbbR{}
29.  real\_term\_value(f;ipolynomial-term(mul-ipoly(v5;v3)))  =  v13
30.  v14  :  \mBbbR{}
31.  real\_term\_value(f;ipolynomial-term(mul-ipoly(v2;v5)))  =  v14
32.  v15  :  \mBbbR{}
33.  real\_term\_value(f;ipolynomial-term(mul-ipoly(v4;v3)))  =  v15
34.  r  :  \mBbbR{}
35.  v7  =  r
36.  q  :  \mBbbR{}
37.  v8  =  q
\mvdash{}  v  \mneq{}  r0
{}\mRightarrow{}  (q  =  (v10/v))
{}\mRightarrow{}  v9  \mneq{}  r0
{}\mRightarrow{}  (r  =  (v11/v9))
{}\mRightarrow{}  (v13  =  (v9  *  v))
{}\mRightarrow{}  (v14  =  (v10  *  v9))
{}\mRightarrow{}  (v15  =  (v11  *  v))
{}\mRightarrow{}  (v12  =  (v15  +  v14))
{}\mRightarrow{}  (v13  \mneq{}  r0  \mwedge{}  ((r  +  q)  =  (v12/v13)))


By

---

Latex:
(All  Thin  THEN  RepeatFor  8  ((D  0  THENA  Auto)))

---

Home Index