Nuprl Lemma : ratmul_wf
∀[a,b:ℤ × ℕ+]. (ratmul(a;b) ∈ {r:ℤ × ℕ+| ratreal(r) = (ratreal(a) * ratreal(b))} )
Proof
Definitions occuring in Statement :
ratmul: ratmul(a;b),
ratreal: ratreal(r),
req: x = y,
rmul: a * b,
nat_plus: ℕ+,
uall: ∀[x:A]. B[x],
member: t ∈ T,
set: {x:A| B[x]} ,
product: x:A × B[x],
int: ℤ
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
ratmul: ratmul(a;b),
all: ∀x:A. B[x],
implies: P ⇒ Q,
subtype_rel: A ⊆r B,
so_lambda: λ2x.t[x],
so_apply: x[s],
uimplies: b supposing a,
guard: {T},
prop: ℙ
Lemmas referenced :
rat-mul_wf,
ratreduce_wf,
subtype_rel_sets_simple,
nat_plus_wf,
req_wf,
ratreal_wf,
rmul_wf,
req_inversion,
req_transitivity,
istype-int
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation_alt,
cut,
introduction,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
hypothesisEquality,
hypothesis,
inhabitedIsType,
lambdaFormation_alt,
setElimination,
rename,
applyEquality,
productEquality,
intEquality,
sqequalRule,
lambdaEquality_alt,
independent_isectElimination,
universeIsType,
because_Cache,
equalityIstype,
equalityTransitivity,
equalitySymmetry,
dependent_functionElimination,
independent_functionElimination,
productIsType
Latex:
\mforall{}[a,b:\mBbbZ{} \mtimes{} \mBbbN{}\msupplus{}]. (ratmul(a;b) \mmember{} \{r:\mBbbZ{} \mtimes{} \mBbbN{}\msupplus{}| ratreal(r) = (ratreal(a) * ratreal(b))\} )
Date html generated:
2019_10_30-AM-09_22_13
Last ObjectModification:
2019_01_10-PM-01_47_54
Theory : reals
Home
Index