Nuprl Lemma : exp-non-neg
∀[n,x:ℕ]. (0 ≤ x^n)
Proof
Definitions occuring in Statement :
exp: i^n,
nat: ℕ,
uall: ∀[x:A]. B[x],
le: A ≤ B,
natural_number: $n
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
le: A ≤ B,
and: P ∧ Q,
uimplies: b supposing a
Lemmas referenced :
zero-le-nat,
exp_wf4,
le_witness_for_triv,
istype-nat
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
Error :isect_memberFormation_alt,
introduction,
cut,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
hypothesisEquality,
hypothesis,
productElimination,
equalityTransitivity,
equalitySymmetry,
independent_isectElimination,
Error :inhabitedIsType,
sqequalRule,
Error :isect_memberEquality_alt,
Error :isectIsTypeImplies
Latex:
\mforall{}[n,x:\mBbbN{}]. (0 \mleq{} x\^{}n)
Date html generated:
2019_06_20-PM-02_26_35
Last ObjectModification:
2019_03_19-AM-11_50_29
Theory : num_thy_1
Home
Index