Nuprl Lemma : un-ctrex1_wf

[x:{x:ℝr(-1) ≤ x} ]. (un-ctrex1(x) ∈ ℝ)


Proof




Definitions occuring in Statement :  un-ctrex1: un-ctrex1(x) rleq: x ≤ y int-to-real: r(n) real: uall: [x:A]. B[x] member: t ∈ T set: {x:A| B[x]}  minus: -n natural_number: $n
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T un-ctrex1: un-ctrex1(x) int_upper: {i...} le: A ≤ B and: P ∧ Q less_than': less_than'(a;b) false: False not: ¬A implies:  Q prop: subtype_rel: A ⊆B nat: int_nzero: -o true: True nequal: a ≠ b ∈  uimplies: supposing a sq_type: SQType(T) all: x:A. B[x] guard: {T} so_lambda: λ2x.t[x] so_apply: x[s] rev_uimplies: rev_uimplies(P;Q) rge: x ≥ y iff: ⇐⇒ Q rev_implies:  Q uiff: uiff(P;Q) isEven: isEven(n) modulus: mod n absval: |i| eq_int: (i =z j) assert: b ifthenelse: if then else fi  bfalse: ff
Lemmas referenced :  radd_wf rsub_wf rroot_wf false_wf le_wf rmul_wf int-to-real_wf real_wf assert_wf isEven_wf rleq_wf req_wf rnexp_wf int-rdiv_wf subtype_base_sq int_subtype_base equal_wf true_wf nequal_wf set_wf rleq_functionality_wrt_implies rleq_weakening_equal radd_functionality_wrt_rleq rleq-int rleq_functionality req_weakening radd-int
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut setElimination thin rename sqequalRule lemma_by_obid sqequalHypSubstitution isectElimination dependent_set_memberEquality natural_numberEquality independent_pairFormation lambdaFormation hypothesis hypothesisEquality applyEquality because_Cache lambdaEquality setEquality productEquality functionEquality addLevel instantiate cumulativity intEquality independent_isectElimination dependent_functionElimination equalityTransitivity equalitySymmetry independent_functionElimination voidElimination axiomEquality minusEquality addEquality productElimination callbyvalueReduce sqleReflexivity

Latex:
\mforall{}[x:\{x:\mBbbR{}|  r(-1)  \mleq{}  x\}  ].  (un-ctrex1(x)  \mmember{}  \mBbbR{})



Date html generated: 2016_05_18-AM-10_47_47
Last ObjectModification: 2015_12_27-PM-10_46_31

Theory : reals


Home Index