Nuprl Lemma : rless-iff8

x,y:ℝ.  (x < ⇐⇒ ∃m:{ℕ+(x m) 8 < m})


Proof




Definitions occuring in Statement :  rless: x < y real: nat_plus: + less_than: a < b all: x:A. B[x] sq_exists: x:{A| B[x]} iff: ⇐⇒ Q apply: a add: m natural_number: $n
Definitions unfolded in proof :  rless: x < y all: x:A. B[x] iff: ⇐⇒ Q and: P ∧ Q implies:  Q member: t ∈ T prop: uall: [x:A]. B[x] so_lambda: λ2x.t[x] real: so_apply: x[s] rev_implies:  Q sq_exists: x:{A| B[x]} nat_plus: + decidable: Dec(P) or: P ∨ Q uimplies: supposing a satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] false: False not: ¬A top: Top regular-int-seq: k-regular-seq(f) le: A ≤ B sq_stable: SqStable(P) squash: T guard: {T} subtype_rel: A ⊆B uiff: uiff(P;Q) less_than: a < b nat: ifthenelse: if then else fi  btrue: tt sq_type: SQType(T) bfalse: ff
Lemmas referenced :  sq_exists_wf nat_plus_wf less_than_wf real_wf nat_plus_properties decidable__lt satisfiable-full-omega-tt intformand_wf intformnot_wf intformless_wf itermConstant_wf itermAdd_wf itermMultiply_wf itermVar_wf int_formula_prop_and_lemma int_formula_prop_not_lemma int_formula_prop_less_lemma int_term_value_constant_lemma int_term_value_add_lemma int_term_value_mul_lemma int_term_value_var_lemma int_formula_prop_wf equal_wf sq_stable__le intformeq_wf int_formula_prop_eq_lemma decidable__le multiply-is-int-iff int_subtype_base add-is-int-iff intformle_wf int_formula_prop_le_lemma false_wf mul_preserves_le le_wf mul_cancel_in_lt absval_ifthenelse subtract_wf lt_int_wf subtract-is-int-iff itermSubtract_wf int_term_value_subtract_lemma assert_wf bnot_wf not_wf minus-is-int-iff itermMinus_wf int_term_value_minus_lemma bool_cases subtype_base_sq bool_wf bool_subtype_base eqtt_to_assert assert_of_lt_int eqff_to_assert iff_transitivity iff_weakening_uiff assert_of_bnot
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep lambdaFormation independent_pairFormation cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin hypothesis lambdaEquality addEquality applyEquality setElimination rename hypothesisEquality natural_numberEquality because_Cache dependent_set_memberFormation dependent_set_memberEquality multiplyEquality dependent_functionElimination unionElimination independent_isectElimination dependent_pairFormation int_eqEquality intEquality isect_memberEquality voidElimination voidEquality computeAll equalityTransitivity equalitySymmetry independent_functionElimination productElimination imageMemberEquality baseClosed imageElimination baseApply closedConclusion pointwiseFunctionality promote_hyp instantiate cumulativity impliesFunctionality

Latex:
\mforall{}x,y:\mBbbR{}.    (x  <  y  \mLeftarrow{}{}\mRightarrow{}  \mexists{}m:\{\mBbbN{}\msupplus{}|  (x  m)  +  8  <  y  m\})



Date html generated: 2017_10_03-AM-08_24_57
Last ObjectModification: 2017_07_28-AM-07_23_32

Theory : reals


Home Index