### Nuprl Lemma : rounded-numerator_wf

`∀[r:ℚ]. ∀[k:ℕ+].  (rounded-numerator(r;k) ∈ ℤ)`

Proof

Definitions occuring in Statement :  rounded-numerator: `rounded-numerator(r;k)` rationals: `ℚ` nat_plus: `ℕ+` uall: `∀[x:A]. B[x]` member: `t ∈ T` int: `ℤ`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` rationals: `ℚ` quotient: `x,y:A//B[x; y]` and: `P ∧ Q` all: `∀x:A. B[x]` implies: `P `` Q` prop: `ℙ` qeq: `qeq(r;s)` uimplies: `b supposing a` so_lambda: `λ2x.t[x]` so_apply: `x[s]` int_nzero: `ℤ-o` callbyvalueall: callbyvalueall has-value: `(a)↓` has-valueall: `has-valueall(a)` rounded-numerator: `rounded-numerator(r;k)` b-union: `A ⋃ B` tunion: `⋃x:A.B[x]` bool: `𝔹` unit: `Unit` ifthenelse: `if b then t else f fi ` pi2: `snd(t)` btrue: `tt` uiff: `uiff(P;Q)` nat_plus: `ℕ+` bfalse: `ff` sq_type: `SQType(T)` guard: `{T}` nequal: `a ≠ b ∈ T ` decidable: `Dec(P)` or: `P ∨ Q` satisfiable_int_formula: `satisfiable_int_formula(fmla)` exists: `∃x:A. B[x]` false: `False` not: `¬A` top: `Top`
Lemmas referenced :  b-union_wf int_nzero_wf equal-wf-T-base bool_wf qeq_wf equal_wf equal-wf-base nat_plus_wf rationals_wf valueall-type-has-valueall bunion-valueall-type int-valueall-type product-valueall-type set-valueall-type nequal_wf evalall-reduce eqtt_to_assert assert_of_eq_int and_wf subtype_base_sq int_subtype_base int_nzero_properties nat_plus_properties decidable__equal_int satisfiable-full-omega-tt intformnot_wf intformeq_wf itermMultiply_wf itermVar_wf int_formula_prop_not_lemma int_formula_prop_eq_lemma int_term_value_mul_lemma int_term_value_var_lemma int_formula_prop_wf div-cancel mul_preserves_eq mul_nzero intformand_wf int_formula_prop_and_lemma mul-associates mul-commutes mul-swap div-mul-cancel
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalHypSubstitution pointwiseFunctionalityForEquality intEquality sqequalRule pertypeElimination productElimination thin equalityTransitivity hypothesis equalitySymmetry extract_by_obid isectElimination productEquality lambdaFormation because_Cache hypothesisEquality baseClosed dependent_functionElimination independent_functionElimination axiomEquality isect_memberEquality independent_isectElimination lambdaEquality natural_numberEquality callbyvalueReduce imageElimination unionElimination equalityElimination isintReduceTrue addLevel levelHypothesis dependent_set_memberEquality independent_pairFormation applyLambdaEquality setElimination rename multiplyEquality instantiate cumulativity dependent_pairFormation int_eqEquality voidElimination voidEquality computeAll divideEquality

Latex:
\mforall{}[r:\mBbbQ{}].  \mforall{}[k:\mBbbN{}\msupplus{}].    (rounded-numerator(r;k)  \mmember{}  \mBbbZ{})

Date html generated: 2018_05_21-PM-11_44_18
Last ObjectModification: 2017_07_26-PM-06_43_00

Theory : rationals

Home Index