Nuprl Lemma : integer-part-decomp
∀q:ℚ. (∃p:{ℤ × {r:ℚ| (0 ≤ r) ∧ r < 1} | let x,r = p in q = (x + r) ∈ ℚ})
Proof
Definitions occuring in Statement :
qle: r ≤ s,
qless: r < s,
qadd: r + s,
rationals: ℚ,
all: ∀x:A. B[x],
sq_exists: ∃x:{A| B[x]},
and: P ∧ Q,
set: {x:A| B[x]} ,
spread: spread def,
product: x:A × B[x],
natural_number: $n,
int: ℤ,
equal: s = t ∈ T
Definitions unfolded in proof :
all: ∀x:A. B[x],
member: t ∈ T,
and: P ∧ Q,
sq_exists: ∃x:{A| B[x]}
Lemmas referenced :
rat-int-part_wf2,
rationals_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation,
introduction,
cut,
lemma_by_obid,
sqequalHypSubstitution,
dependent_functionElimination,
thin,
hypothesisEquality,
sqequalRule,
hypothesis
Latex:
\mforall{}q:\mBbbQ{}. (\mexists{}p:\{\mBbbZ{} \mtimes{} \{r:\mBbbQ{}| (0 \mleq{} r) \mwedge{} r < 1\} | let x,r = p in q = (x + r)\})
Date html generated:
2016_05_15-PM-11_39_53
Last ObjectModification:
2015_12_27-PM-07_25_28
Theory : rationals
Home
Index