---

Step * of Lemma rv-nontrivial

∀n:{2...}. ∃a,b,c:ℝ^n. (a ≠ b ∧ b ≠ c ∧ c ≠ a ∧ (¬a-b-c) ∧ (¬b-c-a) ∧ (¬c-a-b))
BY
{ (Auto
   THEN InstConcl [⌜λi.r0⌝;⌜λi.if (i =z 0) then r1 else r0 fi ⌝;⌜λi.if (i =z 1) then r1 else r0 fi ⌝]⋅
   THEN Auto
   THEN Try (((DNot 0 THENA Auto)
              THEN D -1
              THEN D -2
              THEN ExRepD
              THEN All Reduce
              THEN DupHyp (-2)
              THEN (D -1 With ⌜0⌝  THENA Auto)
              THEN RepUR ``real-vec-mul real-vec-add`` -1
              THEN nRNorm (-1)
              THEN Auto
              THEN (D -3 With ⌜1⌝  THENA Auto)
              THEN RepUR ``real-vec-mul real-vec-add`` -1
              THEN nRNorm (-1)
              THEN Auto))) }

1
1. n : {2...}
⊢ λi.r0 ≠ λi.if (i =z 0) then r1 else r0 fi 

2
1. n : {2...}
2. λi.r0 ≠ λi.if (i =z 0) then r1 else r0 fi 
⊢ λi.if (i =z 0) then r1 else r0 fi  ≠ λi.if (i =z 1) then r1 else r0 fi 

3
1. n : {2...}
2. λi.r0 ≠ λi.if (i =z 0) then r1 else r0 fi 
3. λi.if (i =z 0) then r1 else r0 fi  ≠ λi.if (i =z 1) then r1 else r0 fi 
⊢ λi.if (i =z 1) then r1 else r0 fi  ≠ λi.r0

---

Latex:

---

Latex:
\mforall{}n:\{2...\}.  \mexists{}a,b,c:\mBbbR{}\^{}n.  (a  \mneq{}  b  \mwedge{}  b  \mneq{}  c  \mwedge{}  c  \mneq{}  a  \mwedge{}  (\mneg{}a-b-c)  \mwedge{}  (\mneg{}b-c-a)  \mwedge{}  (\mneg{}c-a-b))


By

---

Latex:
(Auto
  THEN  InstConcl  [\mkleeneopen{}\mlambda{}i.r0\mkleeneclose{};\mkleeneopen{}\mlambda{}i.if  (i  =\msubz{}  0)  then  r1  else  r0  fi  \mkleeneclose{};\mkleeneopen{}\mlambda{}i.if  (i  =\msubz{}  1)  then  r1  else  r0  fi  \mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  Try  (((DNot  0  THENA  Auto)
                        THEN  D  -1
                        THEN  D  -2
                        THEN  ExRepD
                        THEN  All  Reduce
                        THEN  DupHyp  (-2)
                        THEN  (D  -1  With  \mkleeneopen{}0\mkleeneclose{}    THENA  Auto)
                        THEN  RepUR  ``real-vec-mul  real-vec-add``  -1
                        THEN  nRNorm  (-1)
                        THEN  Auto
                        THEN  (D  -3  With  \mkleeneopen{}1\mkleeneclose{}    THENA  Auto)
                        THEN  RepUR  ``real-vec-mul  real-vec-add``  -1
                        THEN  nRNorm  (-1)
                        THEN  Auto)))

---

Home Index