---

Step * 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. r1 ≡ ipolynomial-term(v4)/ipolynomial-term(v5)
11. r2 ≡ ipolynomial-term(v2)/ipolynomial-term(v3)
12. ↑null(add-ipoly(mul-ipoly(v4;v3);mul-ipoly(minus-poly(v2);v5)))
13. f : ℤ ⟶ ℝ
⊢ let p,x = rat_term_to_real(f;r1) 
  in let q,y = rat_term_to_real(f;r2) 
     in p ⇒ q ⇒ (x = y)
BY
{ (((D -4 With ⌜f⌝  THENA Auto) THEN MoveToConcl (-1))
   THEN (D -3 With ⌜f⌝  THENA Auto)
   THEN MoveToConcl (-1)
   THEN GenConclTerms Auto [⌜rat_term_to_real(f;r2)⌝;⌜rat_term_to_real(f;r1)⌝]⋅
   THEN DProdsAndUnions
   THEN Reduce 0
   THEN Auto) }

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. ℝ
25. ℝ
⊢ v7 = v8

---

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.  r1  \mequiv{}  ipolynomial-term(v4)/ipolynomial-term(v5)
11.  r2  \mequiv{}  ipolynomial-term(v2)/ipolynomial-term(v3)
12.  \muparrow{}null(add-ipoly(mul-ipoly(v4;v3);mul-ipoly(minus-poly(v2);v5)))
13.  f  :  \mBbbZ{}  {}\mrightarrow{}  \mBbbR{}
\mvdash{}  let  p,x  =  rat\_term\_to\_real(f;r1) 
    in  let  q,y  =  rat\_term\_to\_real(f;r2) 
          in  p  {}\mRightarrow{}  q  {}\mRightarrow{}  (x  =  y)


By

---

Latex:
(((D  -4  With  \mkleeneopen{}f\mkleeneclose{}    THENA  Auto)  THEN  MoveToConcl  (-1))
  THEN  (D  -3  With  \mkleeneopen{}f\mkleeneclose{}    THENA  Auto)
  THEN  MoveToConcl  (-1)
  THEN  GenConclTerms  Auto  [\mkleeneopen{}rat\_term\_to\_real(f;r2)\mkleeneclose{};\mkleeneopen{}rat\_term\_to\_real(f;r1)\mkleeneclose{}]\mcdot{}
  THEN  DProdsAndUnions
  THEN  Reduce  0
  THEN  Auto)

---

Home Index