Step
*
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)))
24. real_term_value(f;ipolynomial-term(mul-ipoly(v4;v3)))
= (real_term_value(f;ipolynomial-term(v4)) * real_term_value(f;ipolynomial-term(v3)))
25. 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)))
26. 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))))
27. real_term_value(f;ipolynomial-term(minus-poly(v2))) = -(real_term_value(f;ipolynomial-term(v2)))
⊢ (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
{ (Assert real_term_value(f;ipolynomial-term(add-ipoly(mul-ipoly(v4;v3);mul-ipoly(minus-poly(v2);v5)))) = r0 BY
(MoveToConcl 10
THEN GenConclTerm ⌜add-ipoly(mul-ipoly(v4;v3);mul-ipoly(minus-poly(v2);v5))⌝⋅
THEN Auto
THEN RepeatFor 2 (DVar `v')
THEN Reduce -1
THEN Try (Trivial)
THEN RepUR ``ipolynomial-term`` 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. real_term_value(f;ipolynomial-term(mul-ipoly(v4;v3)))
= (real_term_value(f;ipolynomial-term(v4)) * real_term_value(f;ipolynomial-term(v3)))
25. 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)))
26. 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))))
27. real_term_value(f;ipolynomial-term(minus-poly(v2))) = -(real_term_value(f;ipolynomial-term(v2)))
28. 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)))
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)))
24. real\_term\_value(f;ipolynomial-term(mul-ipoly(v4;v3)))
= (real\_term\_value(f;ipolynomial-term(v4)) * real\_term\_value(f;ipolynomial-term(v3)))
25. 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)))
26. 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))))
27. real\_term\_value(f;ipolynomial-term(minus-poly(v2))) = -(real\_term\_value(f;ipolynomial-term(v2)))
\mvdash{} (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:
(Assert real\_term\_value(f;ipolynomial-term(add-ipoly(mul-ipoly(v4;v3);mul-ipoly(...;v5))))
= r0 BY
(MoveToConcl 10
THEN GenConclTerm \mkleeneopen{}add-ipoly(mul-ipoly(v4;v3);mul-ipoly(minus-poly(v2);v5))\mkleeneclose{}\mcdot{}
THEN Auto
THEN RepeatFor 2 (DVar `v')
THEN Reduce -1
THEN Try (Trivial)
THEN RepUR ``ipolynomial-term`` 0
THEN Auto))
Home
Index