---

Step * 2 2 1 1 1 1 3 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 < ||v||
⊢ imonomial-less(m;v[0])
BY
{ ((InstHyp [⌜1⌝;⌜0⌝] 10⋅ 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 < ||v||
19. imonomial-less(<u2, u3>;v[0])
⊢ imonomial-less(m;v[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  <  ||v||
\mvdash{}  imonomial-less(m;v[0])


By

---

Latex:
((InstHyp  [\mkleeneopen{}1\mkleeneclose{};\mkleeneopen{}0\mkleeneclose{}]  10\mcdot{}  THENA  Auto)  THEN  Reduce  (-1))

---

Home Index