### Nuprl Lemma : proportional-round_wf

`∀[r:ℚ]. ∀[k:ℤ]. ∀[l:ℤ-o].  (proportional-round(r;k;l) ∈ ℤ)`

Proof

Definitions occuring in Statement :  proportional-round: `proportional-round(r;k;l)` rationals: `ℚ` int_nzero: `ℤ-o` 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` 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)` proportional-round: `proportional-round(r;k;l)` 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)` prop: `ℙ` nequal: `a ≠ b ∈ T ` not: `¬A` satisfiable_int_formula: `satisfiable_int_formula(fmla)` exists: `∃x:A. B[x]` false: `False` top: `Top` subtype_rel: `A ⊆r B` bfalse: `ff` sq_type: `SQType(T)` guard: `{T}` decidable: `Dec(P)` or: `P ∨ Q`
Lemmas referenced :  b-union_wf int_nzero_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 equal_wf int_nzero_properties satisfiable-full-omega-tt intformand_wf intformeq_wf itermVar_wf itermConstant_wf intformnot_wf int_formula_prop_and_lemma int_formula_prop_eq_lemma int_term_value_var_lemma int_term_value_constant_lemma int_formula_prop_not_lemma int_formula_prop_wf equal-wf-base int_subtype_base equal-wf-T-base bool_wf qeq_wf rationals_wf subtype_base_sq decidable__equal_int itermMultiply_wf int_term_value_mul_lemma div_div div-cancel mul_nzero mul_preserves_eq 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 independent_isectElimination lambdaEquality independent_functionElimination hypothesisEquality natural_numberEquality callbyvalueReduce imageElimination unionElimination equalityElimination isintReduceTrue addLevel levelHypothesis dependent_set_memberEquality independent_pairFormation applyLambdaEquality setElimination rename multiplyEquality divideEquality dependent_pairFormation int_eqEquality dependent_functionElimination isect_memberEquality voidElimination voidEquality computeAll applyEquality baseClosed axiomEquality instantiate cumulativity

Latex:
\mforall{}[r:\mBbbQ{}].  \mforall{}[k:\mBbbZ{}].  \mforall{}[l:\mBbbZ{}\msupminus{}\msupzero{}].    (proportional-round(r;k;l)  \mmember{}  \mBbbZ{})

Date html generated: 2018_05_21-PM-11_44_13
Last ObjectModification: 2017_07_26-PM-06_42_59

Theory : rationals

Home Index