---

Step * of Lemma not-all-nonneg-or-nonpos

¬(∀x:ℝ. ((r0 ≤ x) ∨ (x ≤ r0)))
BY
{ ((D 0 THENA Auto)
   THEN (Assert ∃P:ℝ ⟶ 𝔹. ∀x:ℝ. ((P x = tt ⇒ (r0 ≤ x)) ∧ (P x = ff ⇒ (x ≤ r0))) BY
               (RenameVar `t' (-1)
                THEN D 0 With ⌜λx.isl(t x)⌝ 
                THEN Reduce 0
                THEN Try (Complete (Auto))
                THEN (D 0 THENA Auto)
                THEN (GenConclTerm ⌜t x⌝⋅ THENA Auto)
                THEN D -2
                THEN Reduce 0
                THEN Auto))
   THEN Thin 1
   THEN D -1) }

1
1. P : ℝ ⟶ 𝔹
2. ∀x:ℝ. ((P x = tt ⇒ (r0 ≤ x)) ∧ (P x = ff ⇒ (x ≤ r0)))
⊢ False

---

Latex:

---

Latex:
\mneg{}(\mforall{}x:\mBbbR{}.  ((r0  \mleq{}  x)  \mvee{}  (x  \mleq{}  r0)))


By

---

Latex:
((D  0  THENA  Auto)
  THEN  (Assert  \mexists{}P:\mBbbR{}  {}\mrightarrow{}  \mBbbB{}.  \mforall{}x:\mBbbR{}.  ((P  x  =  tt  {}\mRightarrow{}  (r0  \mleq{}  x))  \mwedge{}  (P  x  =  ff  {}\mRightarrow{}  (x  \mleq{}  r0)))  BY
                          (RenameVar  `t'  (-1)
                            THEN  D  0  With  \mkleeneopen{}\mlambda{}x.isl(t  x)\mkleeneclose{} 
                            THEN  Reduce  0
                            THEN  Try  (Complete  (Auto))
                            THEN  (D  0  THENA  Auto)
                            THEN  (GenConclTerm  \mkleeneopen{}t  x\mkleeneclose{}\mcdot{}  THENA  Auto)
                            THEN  D  -2
                            THEN  Reduce  0
                            THEN  Auto))
  THEN  Thin  1
  THEN  D  -1)

---

Home Index