---

Step * of Lemma rv-Gsep

∀n:ℕ. ∀a,b,c:ℝ^n. ∀d:{d:ℝ^n| ¬¬(∃u,v,w:ℝ^n. ((¬(u ≠ v ∧ v ≠ w ∧ (¬u-v-w))) ∧ ab=uv ∧ cd=uw))} .  (a ≠ b ⇒ c ≠ d)
BY
{ (InstLemma `rv-Tsep-alt` [] THEN RepeatFor 5 (ParallelLast') THEN D -1 THEN Try (Trivial)) }

1
.....antecedent..... 
1. n : ℕ
2. a : ℝ^n
3. b : ℝ^n
4. c : ℝ^n
5. d : {d:ℝ^n| ¬¬(∃u,v,w:ℝ^n. ((¬(u ≠ v ∧ v ≠ w ∧ (¬u-v-w))) ∧ ab=uv ∧ cd=uw))} 
⊢ ¬¬(∃u,v,w:ℝ^n. (rv-T(n;u;v;w) ∧ ab=uv ∧ cd=uw))

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}.  \mforall{}a,b,c:\mBbbR{}\^{}n.  \mforall{}d:\{d:\mBbbR{}\^{}n|  \mneg{}\mneg{}(\mexists{}u,v,w:\mBbbR{}\^{}n.  ((\mneg{}(u  \mneq{}  v  \mwedge{}  v  \mneq{}  w  \mwedge{}  (\mneg{}u-v-w)))  \mwedge{}  ab=uv  \mwedge{}  cd=uw))\}  .
    (a  \mneq{}  b  {}\mRightarrow{}  c  \mneq{}  d)


By

---

Latex:
(InstLemma  `rv-Tsep-alt`  []  THEN  RepeatFor  5  (ParallelLast')  THEN  D  -1  THEN  Try  (Trivial))

---

Home Index