Nuprl Lemma : rnexp2-nonneg

x:ℝ(r0 ≤ x^2)


Proof




Definitions occuring in Statement :  rleq: x ≤ y rnexp: x^k1 int-to-real: r(n) real: all: x:A. B[x] natural_number: $n
Definitions unfolded in proof :  all: 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: uall: [x:A]. B[x] squash: T nat_plus: + less_than: a < b true: True subtype_rel: A ⊆B uimplies: supposing a guard: {T} iff: ⇐⇒ Q rev_implies:  Q
Lemmas referenced :  rnexp-even-nonneg false_wf le_wf equal_wf squash_wf true_wf rem_eq_args less_than_wf iff_weakening_equal real_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut introduction extract_by_obid sqequalHypSubstitution dependent_functionElimination thin dependent_set_memberEquality natural_numberEquality sqequalRule independent_pairFormation hypothesis isectElimination hypothesisEquality independent_functionElimination applyEquality lambdaEquality imageElimination equalityTransitivity equalitySymmetry universeEquality intEquality imageMemberEquality baseClosed independent_isectElimination productElimination because_Cache

Latex:
\mforall{}x:\mBbbR{}.  (r0  \mleq{}  x\^{}2)



Date html generated: 2017_10_03-AM-08_32_51
Last ObjectModification: 2017_07_28-AM-07_27_58

Theory : reals


Home Index