---

Step * 2 2 1 of Lemma stamps-example


1. n : ℤ
2. [%1] : 0 < n
3. i : ℕ
4. j : ℕ
5. ((n - 1) + 8) = ((3 * i) + (5 * j)) ∈ ℤ
6. ¬(3 ≤ i)
7. i' : ℤ
8. i' = (i + 2) ∈ ℤ
9. j' : ℤ
10. j' = (j - 1) ∈ ℤ
⊢ ∃i:ℕ. (∃j:ℕ [((n + 8) = ((3 * i) + (5 * j)) ∈ ℤ)])
BY
{ (InstConcl [⌜i'⌝;⌜j'⌝]⋅ THEN Auto') }

---

Latex:

---

Latex:

1.  n  :  \mBbbZ{}
2.  [\%1]  :  0  <  n
3.  i  :  \mBbbN{}
4.  j  :  \mBbbN{}
5.  ((n  -  1)  +  8)  =  ((3  *  i)  +  (5  *  j))
6.  \mneg{}(3  \mleq{}  i)
7.  i'  :  \mBbbZ{}
8.  i'  =  (i  +  2)
9.  j'  :  \mBbbZ{}
10.  j'  =  (j  -  1)
\mvdash{}  \mexists{}i:\mBbbN{}.  (\mexists{}j:\mBbbN{}  [((n  +  8)  =  ((3  *  i)  +  (5  *  j)))])


By

---

Latex:
(InstConcl  [\mkleeneopen{}i'\mkleeneclose{};\mkleeneopen{}j'\mkleeneclose{}]\mcdot{}  THEN  Auto')

---

Home Index