Nuprl Lemma : req-int-fractions2

[a,b:ℤ]. ∀[c:ℤ-o].  uiff((r(a)/r(c)) r(b);a (b c) ∈ ℤ)


Proof




Definitions occuring in Statement :  rdiv: (x/y) req: y int-to-real: r(n) int_nzero: -o uiff: uiff(P;Q) uall: [x:A]. B[x] multiply: m int: equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uiff: uiff(P;Q) and: P ∧ Q uimplies: supposing a int_nzero: -o all: x:A. B[x] iff: ⇐⇒ Q rev_implies:  Q implies:  Q not: ¬A nequal: a ≠ b ∈  satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] false: False top: Top prop: subtype_rel: A ⊆B so_lambda: λ2x.t[x] so_apply: x[s] rdiv: (x/y) req_int_terms: t1 ≡ t2 rev_uimplies: rev_uimplies(P;Q)
Lemmas referenced :  req_wf rdiv_wf int-to-real_wf rneq-int int_nzero_properties full-omega-unsat intformand_wf intformeq_wf itermVar_wf itermConstant_wf intformnot_wf istype-int int_formula_prop_and_lemma istype-void int_formula_prop_eq_lemma int_term_value_var_lemma int_term_value_constant_lemma int_formula_prop_not_lemma int_formula_prop_wf set_subtype_base nequal_wf int_subtype_base req_witness int_nzero_wf rmul_preserves_req rmul_wf rinv_wf2 itermSubtract_wf itermMultiply_wf req_functionality req_transitivity rmul_functionality req_weakening rmul-rinv rmul-int req-iff-rsub-is-0 real_polynomial_null real_term_value_sub_lemma real_term_value_mul_lemma real_term_value_var_lemma real_term_value_const_lemma req-int
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt introduction cut independent_pairFormation hypothesis universeIsType extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality setElimination rename because_Cache independent_isectElimination dependent_functionElimination natural_numberEquality productElimination independent_functionElimination lambdaFormation_alt approximateComputation dependent_pairFormation_alt lambdaEquality_alt int_eqEquality isect_memberEquality_alt voidElimination sqequalRule equalityIstype inhabitedIsType applyEquality intEquality baseClosed sqequalBase equalitySymmetry baseApply closedConclusion independent_pairEquality axiomEquality isectIsTypeImplies multiplyEquality equalityTransitivity

Latex:
\mforall{}[a,b:\mBbbZ{}].  \mforall{}[c:\mBbbZ{}\msupminus{}\msupzero{}].    uiff((r(a)/r(c))  =  r(b);a  =  (b  *  c))



Date html generated: 2019_10_29-AM-09_58_37
Last ObjectModification: 2019_01_10-PM-00_24_20

Theory : reals


Home Index