Nuprl Lemma : rless-int-fractions2

a,b:ℤ. ∀d:ℕ+.  (r(a) < (r(b)/r(d)) ⇐⇒ d < b)


Proof




Definitions occuring in Statement :  rdiv: (x/y) rless: x < y int-to-real: r(n) nat_plus: + less_than: a < b all: x:A. B[x] iff: ⇐⇒ Q multiply: m int:
Definitions unfolded in proof :  all: x:A. B[x] iff: ⇐⇒ Q and: P ∧ Q implies:  Q member: t ∈ T prop: uall: [x:A]. B[x] nat_plus: + uimplies: supposing a rneq: x ≠ y guard: {T} or: P ∨ Q rev_implies:  Q decidable: Dec(P) satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] false: False not: ¬A top: Top rless: x < y sq_exists: x:{A| B[x]}
Lemmas referenced :  rmul-rdiv-cancel2 req_weakening rmul-int rless_functionality rmul_wf rmul_preserves_rless nat_plus_wf less_than_wf int_formula_prop_wf int_term_value_var_lemma int_term_value_constant_lemma int_formula_prop_less_lemma int_formula_prop_not_lemma int_formula_prop_and_lemma itermVar_wf itermConstant_wf intformless_wf intformnot_wf intformand_wf satisfiable-full-omega-tt decidable__lt nat_plus_properties rless-int rdiv_wf int-to-real_wf rless_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation independent_pairFormation cut hypothesis lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality setElimination rename independent_isectElimination sqequalRule inrFormation dependent_functionElimination because_Cache productElimination independent_functionElimination natural_numberEquality unionElimination dependent_pairFormation lambdaEquality int_eqEquality intEquality isect_memberEquality voidElimination voidEquality computeAll multiplyEquality promote_hyp addLevel

Latex:
\mforall{}a,b:\mBbbZ{}.  \mforall{}d:\mBbbN{}\msupplus{}.    (r(a)  <  (r(b)/r(d))  \mLeftarrow{}{}\mRightarrow{}  a  *  d  <  b)



Date html generated: 2016_05_18-AM-07_27_47
Last ObjectModification: 2016_01_17-AM-01_59_13

Theory : reals


Home Index