---

Step * 2 2 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)
⊢ ∃i:ℕ. (∃j:ℕ [((n + 8) = ((3 * i) + (5 * j)) ∈ ℤ)])
BY
{ ((Evaluate ⌜i' = (i + 2) ∈ ℤ⌝⋅ THENA Auto) THEN (Evaluate ⌜j' = (j - 1) ∈ ℤ⌝⋅ THENA Auto)) }

1
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)) ∈ ℤ)])

---

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)
\mvdash{}  \mexists{}i:\mBbbN{}.  (\mexists{}j:\mBbbN{}  [((n  +  8)  =  ((3  *  i)  +  (5  *  j)))])


By

---

Latex:
((Evaluate  \mkleeneopen{}i'  =  (i  +  2)\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  (Evaluate  \mkleeneopen{}j'  =  (j  -  1)\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index