Nuprl Lemma : rsqrt-positive-iff
∀x:{x:ℝ| r0 ≤ x} . (r0 < rsqrt(x) ⇐⇒ r0 < x)
Proof
Definitions occuring in Statement :
rsqrt: rsqrt(x),
rleq: x ≤ y,
rless: x < y,
int-to-real: r(n),
real: ℝ,
all: ∀x:A. B[x],
iff: P ⇐⇒ Q,
set: {x:A| B[x]} ,
natural_number: $n
Definitions unfolded in proof :
all: ∀x:A. B[x],
iff: P ⇐⇒ Q,
and: P ∧ Q,
implies: P ⇒ Q,
member: t ∈ T,
uall: ∀[x:A]. B[x],
subtype_rel: A ⊆r B,
prop: ℙ,
rev_implies: P ⇐ Q,
uimplies: b supposing a,
nat_plus: ℕ+,
rless: x < y,
sq_exists: ∃x:A [B[x]],
decidable: Dec(P),
or: P ∨ Q,
not: ¬A,
satisfiable_int_formula: satisfiable_int_formula(fmla),
exists: ∃x:A. B[x],
top: Top,
false: False,
nat: ℕ
Lemmas referenced :
rless_wf,
int-to-real_wf,
rsqrt_wf,
rsqrt-positive,
real_wf,
rleq_wf,
rnexp-rless,
rleq_weakening_equal,
nat_plus_properties,
decidable__lt,
full-omega-unsat,
intformnot_wf,
intformless_wf,
itermConstant_wf,
istype-int,
int_formula_prop_not_lemma,
istype-void,
int_formula_prop_less_lemma,
int_term_value_constant_lemma,
int_formula_prop_wf,
istype-less_than,
rnexp_wf,
decidable__le,
intformle_wf,
int_formula_prop_le_lemma,
istype-le,
rless_functionality,
req_weakening,
rsqrt-rnexp-2,
rnexp0
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation_alt,
independent_pairFormation,
universeIsType,
cut,
introduction,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
natural_numberEquality,
hypothesis,
hypothesisEquality,
applyEquality,
lambdaEquality_alt,
setElimination,
rename,
inhabitedIsType,
equalityTransitivity,
equalitySymmetry,
sqequalRule,
dependent_functionElimination,
dependent_set_memberEquality_alt,
setIsType,
because_Cache,
independent_functionElimination,
independent_isectElimination,
unionElimination,
approximateComputation,
dependent_pairFormation_alt,
isect_memberEquality_alt,
voidElimination,
productElimination
Latex:
\mforall{}x:\{x:\mBbbR{}| r0 \mleq{} x\} . (r0 < rsqrt(x) \mLeftarrow{}{}\mRightarrow{} r0 < x)
Date html generated:
2019_10_30-AM-07_57_40
Last ObjectModification:
2019_03_20-PM-00_31_33
Theory : reals
Home
Index