### Nuprl Lemma : assert-is-qrep

`∀p:ℤ × ℕ+. (↑is-qrep(p) `⇐⇒` ∃q:ℚ. (qrep(q) = p ∈ (ℤ × ℕ+)))`

Proof

Definitions occuring in Statement :  is-qrep: `is-qrep(p)` qrep: `qrep(r)` rationals: `ℚ` nat_plus: `ℕ+` assert: `↑b` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` iff: `P `⇐⇒` Q` product: `x:A × B[x]` int: `ℤ` equal: `s = t ∈ T`
Definitions unfolded in proof :  all: `∀x:A. B[x]` iff: `P `⇐⇒` Q` and: `P ∧ Q` implies: `P `` Q` member: `t ∈ T` prop: `ℙ` uall: `∀[x:A]. B[x]` rev_implies: `P `` Q` exists: `∃x:A. B[x]` so_lambda: `λ2x.t[x]` so_apply: `x[s]` mk-rational: `mk-rational(a;b)` subtype_rel: `A ⊆r B` nat_plus: `ℕ+` int_nzero: `ℤ-o` uimplies: `b supposing a` nequal: `a ≠ b ∈ T ` not: `¬A` false: `False` guard: `{T}` satisfiable_int_formula: `satisfiable_int_formula(fmla)` top: `Top` is-qrep: `is-qrep(p)` has-value: `(a)↓` uiff: `uiff(P;Q)` qrep: `qrep(r)` callbyvalueall: callbyvalueall has-valueall: `has-valueall(a)` ifthenelse: `if b then t else f fi ` bfalse: `ff` spreadn: spread3 nat: `ℕ` or: `P ∨ Q` sq_type: `SQType(T)` assoced: `a ~ b` divides: `b | a` ge: `i ≥ j ` decidable: `Dec(P)` bool: `𝔹` unit: `Unit` it: `⋅` btrue: `tt` bnot: `¬bb` assert: `↑b` pi1: `fst(t)` pi2: `snd(t)`
Lemmas referenced :  assert_wf is-qrep_wf exists_wf rationals_wf equal_wf nat_plus_wf qrep_wf mk-rational_wf subtype_rel_sets less_than_wf nequal_wf 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 equal-wf-base int_subtype_base value-type-has-value int-value-type better-gcd_wf bor_wf eq_int_wf gcd_wf or_wf equal-wf-T-base better-gcd-gcd iff_transitivity iff_weakening_uiff assert_of_bor assert_of_eq_int valueall-type-has-valueall product-valueall-type int-valueall-type set-valueall-type evalall-reduce gcd_reduce_property gcd_reduce_wf nat_wf equal-wf-base-T coprime_wf coprime_elim_a subtype_base_sq divides_invar_1 minus-minus divides_reflexivity one_divs_any coprime_elim nat_properties decidable__equal_int intformnot_wf itermMultiply_wf int_formula_prop_not_lemma int_term_value_mul_lemma assoced_elim le_int_wf bool_wf eqtt_to_assert assert_of_le_int eqff_to_assert bool_cases_sqequal bool_subtype_base assert-bnot le_wf intformle_wf int_formula_prop_le_lemma decidable__lt product_subtype_base set_subtype_base qrep-coprime absval_wf absval_ifthenelse lt_int_wf bnot_wf not_wf minus-is-int-iff itermMinus_wf int_term_value_minus_lemma false_wf bool_cases assert_of_lt_int assert_of_bnot
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation independent_pairFormation cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin dependent_functionElimination productElimination independent_pairEquality hypothesisEquality hypothesis sqequalRule lambdaEquality productEquality intEquality dependent_pairFormation applyEquality because_Cache natural_numberEquality independent_isectElimination setElimination rename setEquality applyLambdaEquality int_eqEquality isect_memberEquality voidElimination voidEquality computeAll baseClosed independent_functionElimination callbyvalueReduce minusEquality equalityTransitivity equalitySymmetry orFunctionality multiplyEquality baseApply closedConclusion unionElimination instantiate cumulativity equalityElimination promote_hyp dependent_set_memberEquality inlFormation inrFormation pointwiseFunctionality impliesFunctionality

Latex:
\mforall{}p:\mBbbZ{}  \mtimes{}  \mBbbN{}\msupplus{}.  (\muparrow{}is-qrep(p)  \mLeftarrow{}{}\mRightarrow{}  \mexists{}q:\mBbbQ{}.  (qrep(q)  =  p))

Date html generated: 2018_05_21-PM-11_48_55
Last ObjectModification: 2017_07_26-PM-06_43_15

Theory : rationals

Home Index