Step
*
2
2
1
1
1
1
4
of Lemma
add-poly-lemma1
1. u2 : ℤ-o
2. u3 : {vs:ℤ List| sorted(vs)}
3. v : iMonomial() List
4. ∀q:iMonomial() List. ∀m:iMonomial().
((∀i:ℕ||v||. ∀j:ℕi. imonomial-less(v[j];v[i]))
⇒ (∀i:ℕ||q||. ∀j:ℕi. imonomial-less(q[j];q[i]))
⇒ (0 < ||v|| ⇒ imonomial-less(m;v[0]))
⇒ (0 < ||q|| ⇒ imonomial-less(m;q[0]))
⇒ 0 < ||add-ipoly(v;q)||
⇒ imonomial-less(m;add-ipoly(v;q)[0]))
5. u4 : ℤ-o
6. u5 : {vs:ℤ List| sorted(vs)}
7. v1 : iMonomial() List
8. ∀m:iMonomial()
((∀i:ℕ||v|| + 1. ∀j:ℕi. imonomial-less([<u2, u3> / v][j];[<u2, u3> / v][i]))
⇒ (∀i:ℕ||v1||. ∀j:ℕi. imonomial-less(v1[j];v1[i]))
⇒ (0 < ||v|| + 1 ⇒ imonomial-less(m;<u2, u3>))
⇒ (0 < ||v1|| ⇒ imonomial-less(m;v1[0]))
⇒ 0 < ||add-ipoly([<u2, u3> / v];v1)||
⇒ imonomial-less(m;add-ipoly([<u2, u3> / v];v1)[0]))
9. m : iMonomial()
10. ∀i:ℕ||v|| + 1. ∀j:ℕi. imonomial-less([<u2, u3> / v][j];[<u2, u3> / v][i])
11. ∀i:ℕ||v1|| + 1. ∀j:ℕi. imonomial-less([<u4, u5> / v1][j];[<u4, u5> / v1][i])
12. 0 < ||v|| + 1 ⇒ imonomial-less(m;<u2, u3>)
13. 0 < ||v1|| + 1 ⇒ imonomial-less(m;<u4, u5>)
14. ↑imonomial-le(<u2, u3>;<u4, u5>)
15. ↑imonomial-le(<u4, u5>;<u2, u3>)
16. (u2 + u4) = 0 ∈ ℤ
17. 0 < ||add-ipoly(v;v1)||
18. 0 < ||v1||
⊢ imonomial-less(m;v1[0])
BY
{ ((InstHyp [⌜1⌝;⌜0⌝] 11⋅ THENA Auto) THEN Reduce (-1)) }
1
1. u2 : ℤ-o
2. u3 : {vs:ℤ List| sorted(vs)}
3. v : iMonomial() List
4. ∀q:iMonomial() List. ∀m:iMonomial().
((∀i:ℕ||v||. ∀j:ℕi. imonomial-less(v[j];v[i]))
⇒ (∀i:ℕ||q||. ∀j:ℕi. imonomial-less(q[j];q[i]))
⇒ (0 < ||v|| ⇒ imonomial-less(m;v[0]))
⇒ (0 < ||q|| ⇒ imonomial-less(m;q[0]))
⇒ 0 < ||add-ipoly(v;q)||
⇒ imonomial-less(m;add-ipoly(v;q)[0]))
5. u4 : ℤ-o
6. u5 : {vs:ℤ List| sorted(vs)}
7. v1 : iMonomial() List
8. ∀m:iMonomial()
((∀i:ℕ||v|| + 1. ∀j:ℕi. imonomial-less([<u2, u3> / v][j];[<u2, u3> / v][i]))
⇒ (∀i:ℕ||v1||. ∀j:ℕi. imonomial-less(v1[j];v1[i]))
⇒ (0 < ||v|| + 1 ⇒ imonomial-less(m;<u2, u3>))
⇒ (0 < ||v1|| ⇒ imonomial-less(m;v1[0]))
⇒ 0 < ||add-ipoly([<u2, u3> / v];v1)||
⇒ imonomial-less(m;add-ipoly([<u2, u3> / v];v1)[0]))
9. m : iMonomial()
10. ∀i:ℕ||v|| + 1. ∀j:ℕi. imonomial-less([<u2, u3> / v][j];[<u2, u3> / v][i])
11. ∀i:ℕ||v1|| + 1. ∀j:ℕi. imonomial-less([<u4, u5> / v1][j];[<u4, u5> / v1][i])
12. 0 < ||v|| + 1 ⇒ imonomial-less(m;<u2, u3>)
13. 0 < ||v1|| + 1 ⇒ imonomial-less(m;<u4, u5>)
14. ↑imonomial-le(<u2, u3>;<u4, u5>)
15. ↑imonomial-le(<u4, u5>;<u2, u3>)
16. (u2 + u4) = 0 ∈ ℤ
17. 0 < ||add-ipoly(v;v1)||
18. 0 < ||v1||
19. imonomial-less(<u4, u5>;v1[0])
⊢ imonomial-less(m;v1[0])
Latex:
Latex:
1. u2 : \mBbbZ{}\msupminus{}\msupzero{}
2. u3 : \{vs:\mBbbZ{} List| sorted(vs)\}
3. v : iMonomial() List
4. \mforall{}q:iMonomial() List. \mforall{}m:iMonomial().
((\mforall{}i:\mBbbN{}||v||. \mforall{}j:\mBbbN{}i. imonomial-less(v[j];v[i]))
{}\mRightarrow{} (\mforall{}i:\mBbbN{}||q||. \mforall{}j:\mBbbN{}i. imonomial-less(q[j];q[i]))
{}\mRightarrow{} (0 < ||v|| {}\mRightarrow{} imonomial-less(m;v[0]))
{}\mRightarrow{} (0 < ||q|| {}\mRightarrow{} imonomial-less(m;q[0]))
{}\mRightarrow{} 0 < ||add-ipoly(v;q)||
{}\mRightarrow{} imonomial-less(m;add-ipoly(v;q)[0]))
5. u4 : \mBbbZ{}\msupminus{}\msupzero{}
6. u5 : \{vs:\mBbbZ{} List| sorted(vs)\}
7. v1 : iMonomial() List
8. \mforall{}m:iMonomial()
((\mforall{}i:\mBbbN{}||v|| + 1. \mforall{}j:\mBbbN{}i. imonomial-less([<u2, u3> / v][j];[<u2, u3> / v][i]))
{}\mRightarrow{} (\mforall{}i:\mBbbN{}||v1||. \mforall{}j:\mBbbN{}i. imonomial-less(v1[j];v1[i]))
{}\mRightarrow{} (0 < ||v|| + 1 {}\mRightarrow{} imonomial-less(m;<u2, u3>))
{}\mRightarrow{} (0 < ||v1|| {}\mRightarrow{} imonomial-less(m;v1[0]))
{}\mRightarrow{} 0 < ||add-ipoly([<u2, u3> / v];v1)||
{}\mRightarrow{} imonomial-less(m;add-ipoly([<u2, u3> / v];v1)[0]))
9. m : iMonomial()
10. \mforall{}i:\mBbbN{}||v|| + 1. \mforall{}j:\mBbbN{}i. imonomial-less([<u2, u3> / v][j];[<u2, u3> / v][i])
11. \mforall{}i:\mBbbN{}||v1|| + 1. \mforall{}j:\mBbbN{}i. imonomial-less([<u4, u5> / v1][j];[<u4, u5> / v1][i])
12. 0 < ||v|| + 1 {}\mRightarrow{} imonomial-less(m;<u2, u3>)
13. 0 < ||v1|| + 1 {}\mRightarrow{} imonomial-less(m;<u4, u5>)
14. \muparrow{}imonomial-le(<u2, u3><u4, u5>)
15. \muparrow{}imonomial-le(<u4, u5><u2, u3>)
16. (u2 + u4) = 0
17. 0 < ||add-ipoly(v;v1)||
18. 0 < ||v1||
\mvdash{} imonomial-less(m;v1[0])
By
Latex:
((InstHyp [\mkleeneopen{}1\mkleeneclose{};\mkleeneopen{}0\mkleeneclose{}] 11\mcdot{} THENA Auto) THEN Reduce (-1))
Home
Index