Nuprl Lemma : zero-le-nat

[i:ℕ]. (0 ≤ i)


Proof




Definitions occuring in Statement :  nat: uall: [x:A]. B[x] le: A ≤ B natural_number: $n
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T nat: implies:  Q all: x:A. B[x] sq_stable: SqStable(P) squash: T le: A ≤ B and: P ∧ Q not: ¬A false: False prop:
Lemmas referenced :  nat_wf less_than'_wf decidable__le le_wf sq_stable_from_decidable
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalHypSubstitution setElimination thin rename lemma_by_obid isectElimination natural_numberEquality hypothesisEquality hypothesis independent_functionElimination dependent_functionElimination sqequalRule imageMemberEquality baseClosed imageElimination productElimination independent_pairEquality lambdaEquality voidElimination axiomEquality equalityTransitivity equalitySymmetry

Latex:
\mforall{}[i:\mBbbN{}].  (0  \mleq{}  i)



Date html generated: 2016_05_13-PM-03_32_06
Last ObjectModification: 2016_01_14-PM-06_40_54

Theory : arithmetic


Home Index