### Nuprl Lemma : rnonneg2_wf

[x:ℕ+ ⟶ ℤ]. (rnonneg2(x) ∈ ℙ)

Proof

Definitions occuring in Statement :  rnonneg2: rnonneg2(x) nat_plus: + uall: [x:A]. B[x] prop: member: t ∈ T function: x:A ⟶ B[x] int:
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T rnonneg2: rnonneg2(x) so_lambda: λ2x.t[x] nat_plus: + int_upper: {i...} le: A ≤ B and: P ∧ Q guard: {T} uimplies: supposing a prop: so_apply: x[s]
Lemmas referenced :  all_wf nat_plus_wf exists_wf int_upper_wf le_wf less_than_transitivity1 less_than_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesis lambdaEquality because_Cache setElimination rename hypothesisEquality multiplyEquality minusEquality natural_numberEquality applyEquality dependent_set_memberEquality productElimination independent_isectElimination axiomEquality equalityTransitivity equalitySymmetry functionEquality intEquality

Latex:
\mforall{}[x:\mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}].  (rnonneg2(x)  \mmember{}  \mBbbP{})

Date html generated: 2016_05_18-AM-07_01_26
Last ObjectModification: 2015_12_28-AM-00_33_57

Theory : reals

Home Index