---

Step * of Lemma rv-between-simple

∀n:ℕ. ∀c,d:ℝ^n.  ((r0 < ||d||) ⇒ c - d-c-c + d)
BY
{ (Auto THEN Assert ⌜c - d-c-c + d⌝⋅) }

1
.....assertion..... 
1. n : ℕ
2. c : ℝ^n
3. d : ℝ^n
4. r0 < ||d||
⊢ c - d-c-c + d

2
1. n : ℕ
2. c : ℝ^n
3. d : ℝ^n
4. r0 < ||d||
5. c - d-c-c + d
⊢ c - d-c-c + d

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}.  \mforall{}c,d:\mBbbR{}\^{}n.    ((r0  <  ||d||)  {}\mRightarrow{}  c  -  d-c-c  +  d)


By

---

Latex:
(Auto  THEN  Assert  \mkleeneopen{}c  -  d-c-c  +  d\mkleeneclose{}\mcdot{})

---

Home Index