Nuprl Lemma : qdiv-int-elim
∀[p:ℤ]. ∀[q:ℤ-o]. ((p/q) ~ <p, q>)
Proof
Definitions occuring in Statement :
qdiv: (r/s),
int_nzero: ℤ-o,
uall: ∀[x:A]. B[x],
pair: <a, b>,
int: ℤ,
sqequal: s ~ t
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],
all: ∀x:A. B[x],
int_nzero: ℤ-o,
qdiv: (r/s),
qinv: 1/r,
qmul: r * s,
callbyvalueall: callbyvalueall,
has-value: (a)↓,
has-valueall: has-valueall(a),
ifthenelse: if b then t else f fi ,
btrue: tt,
implies: P ⇒ Q,
subtype_rel: A ⊆r B,
sq_type: SQType(T),
guard: {T},
top: Top,
bfalse: ff
Lemmas referenced :
one-mul,
mul-commutes,
evalall-sqequal,
product-valueall-type,
nequal_wf,
set-valueall-type,
int_nzero_wf,
evalall-reduce,
int-valueall-type,
valueall-type-has-valueall,
set_subtype_base,
int_subtype_base,
product_subtype_base,
subtype_base_sq
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation,
introduction,
cut,
thin,
instantiate,
lemma_by_obid,
sqequalHypSubstitution,
isectElimination,
because_Cache,
independent_isectElimination,
sqequalRule,
hypothesis,
lambdaFormation,
intEquality,
hypothesisEquality,
callbyvalueReduce,
lambdaEquality,
natural_numberEquality,
isintReduceTrue,
setElimination,
rename,
productEquality,
independent_functionElimination,
independent_pairEquality,
baseApply,
closedConclusion,
baseClosed,
applyEquality,
dependent_functionElimination,
equalityTransitivity,
equalitySymmetry,
sqequalAxiom,
isect_memberEquality,
voidElimination,
voidEquality
Latex:
\mforall{}[p:\mBbbZ{}]. \mforall{}[q:\mBbbZ{}\msupminus{}\msupzero{}]. ((p/q) \msim{} <p, q>)
Date html generated:
2016_05_15-PM-10_39_46
Last ObjectModification:
2016_01_16-PM-09_36_33
Theory : rationals
Home
Index