Step
*
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
⊢ ∃i:ℕ. (∃j:ℕ [((n + 8) = ((3 * i) + (5 * j)) ∈ ℤ)])
BY
{ TACTIC:((Evaluate ⌜i' = (i - 3) ∈ ℤ⌝⋅ THENA Auto) THEN (Evaluate ⌜j' = (j + 2) ∈ ℤ⌝⋅ 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 - 3) ∈ ℤ
9. j' : ℤ
10. j' = (j + 2) ∈ ℤ
⊢ ∃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.  3  \mleq{}  i
\mvdash{}  \mexists{}i:\mBbbN{}.  (\mexists{}j:\mBbbN{}  [((n  +  8)  =  ((3  *  i)  +  (5  *  j)))])
By
Latex:
TACTIC:((Evaluate  \mkleeneopen{}i'  =  (i  -  3)\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  (Evaluate  \mkleeneopen{}j'  =  (j  +  2)\mkleeneclose{}\mcdot{}  THENA  Auto))
Home
Index