Nuprl Lemma : runop_wf
∀[op:ℤ]. ∀[p:ℝ].
(runop(op;p) ∈ ℝ) supposing
(((op = 5 ∈ ℤ) ⇒ (r0 < p)) and
((op = 6 ∈ ℤ) ⇒ (p ∈ (r(-1), r1))) and
((op = 9 ∈ ℤ) ⇒ (r1 ≤ p)) and
((op = 11 ∈ ℤ) ⇒ p ≠ r0) and
((op = 12 ∈ ℤ) ⇒ ((-(π/2) < p) ∧ (p < π/2))))
Proof
Definitions occuring in Statement :
runop: runop(op;p),
halfpi: π/2,
rooint: (l, u),
i-member: r ∈ I,
rneq: x ≠ y,
rleq: x ≤ y,
rless: x < y,
rminus: -(x),
int-to-real: r(n),
real: ℝ,
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
implies: P ⇒ Q,
and: P ∧ Q,
member: t ∈ T,
minus: -n,
natural_number: $n,
int: ℤ,
equal: s = t ∈ T
Definitions unfolded in proof :
prop: ℙ,
and: P ∧ Q,
top: Top,
all: ∀x:A. B[x],
subtype_rel: A ⊆r B,
not: ¬A,
implies: P ⇒ Q,
false: False,
runop: runop(op;p),
uimplies: b supposing a,
member: t ∈ T,
uall: ∀[x:A]. B[x]
Lemmas referenced :
real_wf,
rneq_wf,
rleq_wf,
rooint_wf,
i-member_wf,
int-to-real_wf,
int_subtype_base,
equal-wf-base,
arctan_wf,
halfpi_wf,
rless_wf,
member_rooint_lemma,
rtan_wf,
rinv_wf2,
inv-sinh_wf,
inv-cosh_wf,
sinh_wf,
cosh_wf,
arcsin_wf,
ln_wf,
expr_wf,
rabs_wf,
rcos_wf,
rsin_wf,
rminus_wf
Rules used in proof :
minusEquality,
baseClosed,
intEquality,
functionEquality,
equalitySymmetry,
equalityTransitivity,
axiomEquality,
productEquality,
productElimination,
independent_pairFormation,
voidEquality,
voidElimination,
isect_memberEquality,
independent_functionElimination,
dependent_set_memberEquality,
dependent_functionElimination,
applyEquality,
because_Cache,
hypothesis,
thin,
isectElimination,
sqequalHypSubstitution,
extract_by_obid,
natural_numberEquality,
hypothesisEquality,
int_eqEquality,
sqequalRule,
cut,
introduction,
isect_memberFormation,
sqequalReflexivity,
computationStep,
sqequalTransitivity,
sqequalSubstitution
Latex:
\mforall{}[op:\mBbbZ{}]. \mforall{}[p:\mBbbR{}].
(runop(op;p) \mmember{} \mBbbR{}) supposing
(((op = 5) {}\mRightarrow{} (r0 < p)) and
((op = 6) {}\mRightarrow{} (p \mmember{} (r(-1), r1))) and
((op = 9) {}\mRightarrow{} (r1 \mleq{} p)) and
((op = 11) {}\mRightarrow{} p \mneq{} r0) and
((op = 12) {}\mRightarrow{} ((-(\mpi{}/2) < p) \mwedge{} (p < \mpi{}/2))))
Date html generated:
2018_05_22-PM-03_08_31
Last ObjectModification:
2018_05_20-PM-11_36_17
Theory : reals_2
Home
Index