---

Step * of Lemma int-rmul_wf

∀[k:ℤ]. ∀[a:ℝ].  (k * a ∈ ℝ)
BY
{ TACTIC:(Auto THEN D -1 THEN Unfold `int-rmul` 0 THEN (CallByValueReduce 0 THENA Auto) THEN MemTypeCD⋅ THEN Auto) }

1
.....set predicate..... 
1. k : ℤ
2. a : ℕ+ ⟶ ℤ
3. regular-seq(a)
⊢ regular-seq(λn.if (k) < (0)  then -(a ((-k) * n))  else if (0) < (k)  then a (k * n)  else 0)

---

Latex:

---

Latex:
\mforall{}[k:\mBbbZ{}].  \mforall{}[a:\mBbbR{}].    (k  *  a  \mmember{}  \mBbbR{})


By

---

Latex:
TACTIC:(Auto
                THEN  D  -1
                THEN  Unfold  `int-rmul`  0
                THEN  (CallByValueReduce  0  THENA  Auto)
                THEN  MemTypeCD\mcdot{}
                THEN  Auto)

---

Home Index