Nuprl Lemma : rnexp1

[x:ℝ]. (x^1 x)


Proof




Definitions occuring in Statement :  rnexp: x^k1 req: y real: uall: [x:A]. B[x] natural_number: $n
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T nat: le: A ≤ B and: P ∧ Q less_than': less_than'(a;b) false: False not: ¬A implies:  Q prop: all: x:A. B[x] bool: 𝔹 unit: Unit it: btrue: tt ifthenelse: if then else fi  uiff: uiff(P;Q) uimplies: supposing a bfalse: ff exists: x:A. B[x] or: P ∨ Q sq_type: SQType(T) guard: {T} bnot: ¬bb assert: b nequal: a ≠ b ∈  satisfiable_int_formula: satisfiable_int_formula(fmla) top: Top true: True eq_int: (i =z j) subtract: m rev_uimplies: rev_uimplies(P;Q)
Lemmas referenced :  req_witness rnexp_wf false_wf le_wf real_wf eq_int_wf bool_wf eqtt_to_assert assert_of_eq_int int-to-real_wf eqff_to_assert equal_wf bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot neg_assert_of_eq_int rmul_wf satisfiable-full-omega-tt intformnot_wf intformeq_wf itermConstant_wf int_formula_prop_not_lemma int_formula_prop_eq_lemma int_term_value_constant_lemma int_formula_prop_wf int_subtype_base req_weakening req_functionality rnexp_unroll
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut extract_by_obid sqequalHypSubstitution isectElimination thin dependent_set_memberEquality natural_numberEquality sqequalRule independent_pairFormation lambdaFormation hypothesis hypothesisEquality independent_functionElimination unionElimination equalityElimination productElimination independent_isectElimination because_Cache equalityTransitivity equalitySymmetry dependent_pairFormation promote_hyp dependent_functionElimination instantiate cumulativity voidElimination lambdaEquality intEquality isect_memberEquality voidEquality computeAll

Latex:
\mforall{}[x:\mBbbR{}].  (x\^{}1  =  x)



Date html generated: 2017_10_03-AM-08_32_06
Last ObjectModification: 2017_07_28-AM-07_27_29

Theory : reals


Home Index