Nuprl Lemma : better-q-elim
∀r:ℚ. ∃p:ℤ. ∃q:ℕ+. ((¬(q = 0 ∈ ℚ)) c∧ (r = (p/q) ∈ ℚ))
Proof
Definitions occuring in Statement :
qdiv: (r/s),
rationals: ℚ,
nat_plus: ℕ+,
cand: A c∧ B,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
not: ¬A,
natural_number: $n,
int: ℤ,
equal: s = t ∈ T
Lemmas referenced :
q-elim
Rules used in proof :
cut,
lemma_by_obid,
hypothesis
Latex:
\mforall{}r:\mBbbQ{}. \mexists{}p:\mBbbZ{}. \mexists{}q:\mBbbN{}\msupplus{}. ((\mneg{}(q = 0)) c\mwedge{} (r = (p/q)))
Date html generated:
2016_05_15-PM-10_39_54
Last ObjectModification:
2015_12_27-PM-07_58_40
Theory : rationals
Home
Index