### Nuprl Lemma : 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`
Definitions unfolded in proof :  all: `∀x:A. B[x]` uall: `∀[x:A]. B[x]` member: `t ∈ T` prop: `ℙ` so_lambda: `λ2x.t[x]` cand: `A c∧ B` subtype_rel: `A ⊆r B` nat_plus: `ℕ+` so_apply: `x[s]` uimplies: `b supposing a` implies: `P `` Q` 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` bfalse: `ff` exists: `∃x:A. B[x]` not: `¬A` satisfiable_int_formula: `satisfiable_int_formula(fmla)` false: `False` top: `Top` and: `P ∧ Q` uiff: `uiff(P;Q)`
Lemmas referenced :  equals-qrep exists_wf nat_plus_wf not_wf equal-wf-T-base subtype_rel_set rationals_wf less_than_wf int-subtype-rationals equal_wf qdiv_wf qrep_wf valueall-type-has-valueall int-valueall-type evalall-reduce set-valueall-type product-valueall-type mul-one nat_plus_properties satisfiable-full-omega-tt intformand_wf intformeq_wf itermVar_wf itermConstant_wf intformless_wf int_formula_prop_and_lemma int_formula_prop_eq_lemma int_term_value_var_lemma int_term_value_constant_lemma int_formula_prop_less_lemma int_formula_prop_wf int-equal-in-rationals
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality equalitySymmetry hypothesis hyp_replacement applyLambdaEquality intEquality sqequalRule lambdaEquality productEquality because_Cache applyEquality natural_numberEquality independent_isectElimination baseClosed productElimination equalityTransitivity dependent_functionElimination independent_functionElimination callbyvalueReduce isintReduceTrue setElimination rename independent_pairEquality dependent_pairFormation int_eqEquality isect_memberEquality voidElimination voidEquality independent_pairFormation computeAll addLevel impliesFunctionality

Latex:
\mforall{}r:\mBbbQ{}.  \mexists{}p:\mBbbZ{}.  \mexists{}q:\mBbbN{}\msupplus{}.  ((\mneg{}(q  =  0))  c\mwedge{}  (r  =  (p/q)))

Date html generated: 2018_05_21-PM-11_47_42
Last ObjectModification: 2017_07_26-PM-06_43_12

Theory : rationals

Home Index