Nuprl Lemma : square-rless-implies

x,y:ℝ.  ((r0 ≤ y)  (x^2 < y^2)  (x < y))


Proof




Definitions occuring in Statement :  rleq: x ≤ y rless: x < y rnexp: x^k1 int-to-real: r(n) real: all: x:A. B[x] implies:  Q natural_number: $n
Definitions unfolded in proof :  all: x:A. B[x] implies:  Q member: t ∈ T uall: [x:A]. B[x] iff: ⇐⇒ Q and: P ∧ Q prop: nat: le: A ≤ B less_than': less_than'(a;b) false: False not: ¬A itermConstant: "const" req_int_terms: t1 ≡ t2 top: Top uiff: uiff(P;Q) uimplies: supposing a or: P ∨ Q rev_uimplies: rev_uimplies(P;Q) guard: {T} rge: x ≥ y
Lemmas referenced :  radd-preserves-rless rnexp_wf rminus_wf rless_wf false_wf le_wf rleq_wf int-to-real_wf real_wf radd_wf rmul_wf rsub_wf real_term_polynomial itermSubtract_wf itermAdd_wf itermMinus_wf itermMultiply_wf itermVar_wf real_term_value_const_lemma real_term_value_sub_lemma real_term_value_add_lemma real_term_value_minus_lemma real_term_value_mul_lemma real_term_value_var_lemma req-iff-rsub-is-0 rmul-is-positive rless-implies-rless itermConstant_wf rless_functionality req_transitivity radd_functionality req_weakening req_functionality rnexp2 rminus_functionality rless_transitivity1 rless_functionality_wrt_implies radd_functionality_wrt_rleq rleq_weakening_equal
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut introduction extract_by_obid sqequalHypSubstitution dependent_functionElimination thin isectElimination because_Cache hypothesis productElimination independent_functionElimination dependent_set_memberEquality natural_numberEquality sqequalRule independent_pairFormation hypothesisEquality computeAll lambdaEquality int_eqEquality intEquality isect_memberEquality voidElimination voidEquality independent_isectElimination unionElimination equalityTransitivity equalitySymmetry

Latex:
\mforall{}x,y:\mBbbR{}.    ((r0  \mleq{}  y)  {}\mRightarrow{}  (x\^{}2  <  y\^{}2)  {}\mRightarrow{}  (x  <  y))



Date html generated: 2017_10_03-AM-08_49_51
Last ObjectModification: 2017_07_28-AM-07_33_55

Theory : reals


Home Index