---

Step * of Lemma un-ctrex1_wf

∀[x:{x:ℝ| r(-1) ≤ x} ]. (un-ctrex1(x) ∈ ℝ)
BY
{ ProveWfLemma }

1
1. x : ℝ
2. r(-1) ≤ x
⊢ x + r1 ∈ {x:ℝ| (↑isEven(2)) ⇒ (r0 ≤ x)} 

2
1. x : ℝ
2. r(-1) ≤ x
⊢ r1 + ((r(3))/4 * x) ∈ {x:ℝ| (↑isEven(3)) ⇒ (r0 ≤ x)} 

---

Latex:

---

Latex:
\mforall{}[x:\{x:\mBbbR{}|  r(-1)  \mleq{}  x\}  ].  (un-ctrex1(x)  \mmember{}  \mBbbR{})


By

---

Latex:
ProveWfLemma

---

Home Index