### Nuprl Lemma : rational-form-has-value

`∀[r:ℤ ⋃ (ℤ × ℤ-o)]. has-valueall(r)`

Proof

Definitions occuring in Statement :  int_nzero: `ℤ-o` has-valueall: `has-valueall(a)` b-union: `A ⋃ B` uall: `∀[x:A]. B[x]` product: `x:A × B[x]` int: `ℤ`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` so_lambda: `λ2x.t[x]` so_apply: `x[s]` implies: `P `` Q` all: `∀x:A. B[x]` int_nzero: `ℤ-o` has-valueall: `has-valueall(a)` has-value: `(a)↓`
Lemmas referenced :  valueall-type-has-valueall b-union_wf int_nzero_wf bunion-valueall-type int-valueall-type product-valueall-type set-valueall-type nequal_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lemma_by_obid sqequalHypSubstitution isectElimination thin intEquality productEquality hypothesis independent_isectElimination because_Cache sqequalRule lambdaEquality independent_functionElimination lambdaFormation hypothesisEquality natural_numberEquality axiomSqleEquality

Latex:
\mforall{}[r:\mBbbZ{}  \mcup{}  (\mBbbZ{}  \mtimes{}  \mBbbZ{}\msupminus{}\msupzero{})].  has-valueall(r)

Date html generated: 2016_05_15-PM-10_37_09
Last ObjectModification: 2015_12_27-PM-08_00_42

Theory : rationals

Home Index