### Nuprl Lemma : req-int-fractions

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

Proof

Definitions occuring in Statement :  rdiv: `(x/y)` req: `x = y` int-to-real: `r(n)` int_nzero: `ℤ-o` uiff: `uiff(P;Q)` uall: `∀[x:A]. B[x]` multiply: `n * m` int: `ℤ` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uiff: `uiff(P;Q)` and: `P ∧ Q` uimplies: `b supposing a` int_nzero: `ℤ-o` all: `∀x:A. B[x]` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` implies: `P `` Q` not: `¬A` nequal: `a ≠ b ∈ T ` satisfiable_int_formula: `satisfiable_int_formula(fmla)` exists: `∃x:A. B[x]` false: `False` top: `Top` prop: `ℙ` subtype_rel: `A ⊆r 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 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 rmul-int 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 equalityTransitivity baseApply closedConclusion independent_pairEquality axiomEquality isectIsTypeImplies multiplyEquality

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

Date html generated: 2019_10_29-AM-09_58_26
Last ObjectModification: 2019_01_10-PM-00_20_48

Theory : reals

Home Index