---

Step * of Lemma case-real2_wf

∀[P:ℙ]. ∀[a,b:ℝ]. ∀[f:a ≠ b ⟶ ((↓P) ∨ (↓¬P))].  (case-real2(a;b;f) ∈ {z:ℝ| (P ⇒ (z = a)) ∧ ((¬P) ⇒ (z = b))} )
BY
{ ((InstLemma `case-real_wf` [] THEN RepeatFor 3 (ParallelLast'))
   THEN Intro
   THEN Unhide
   THEN Unfold `case-real2` 0
   THEN MemCD
   THEN Try (Trivial)
   THEN (MemCD THENA Auto)
   THEN (D -1 THEN (RWO "absval_lbound" (-1) THENA Auto))
   THEN (BoolCase ⌜(a n) + 4 <z b n⌝⋅ THENA Auto)
   THEN MemCD
   THEN Try (Trivial)
   THEN Unfold `rneq` 0
   THEN MemCD
   THEN Try (MemTypeCD)
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[P:\mBbbP{}].  \mforall{}[a,b:\mBbbR{}].  \mforall{}[f:a  \mneq{}  b  {}\mrightarrow{}  ((\mdownarrow{}P)  \mvee{}  (\mdownarrow{}\mneg{}P))].
    (case-real2(a;b;f)  \mmember{}  \{z:\mBbbR{}|  (P  {}\mRightarrow{}  (z  =  a))  \mwedge{}  ((\mneg{}P)  {}\mRightarrow{}  (z  =  b))\}  )


By

---

Latex:
((InstLemma  `case-real\_wf`  []  THEN  RepeatFor  3  (ParallelLast'))
  THEN  Intro
  THEN  Unhide
  THEN  Unfold  `case-real2`  0
  THEN  MemCD
  THEN  Try  (Trivial)
  THEN  (MemCD  THENA  Auto)
  THEN  (D  -1  THEN  (RWO  "absval\_lbound"  (-1)  THENA  Auto))
  THEN  (BoolCase  \mkleeneopen{}(a  n)  +  4  <z  b  n\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  MemCD
  THEN  Try  (Trivial)
  THEN  Unfold  `rneq`  0
  THEN  MemCD
  THEN  Try  (MemTypeCD)
  THEN  Auto)

---

Home Index