### Nuprl Lemma : radd-int-fractions

`∀[a,b:ℤ]. ∀[c,d:ℕ+].  (((r(a)/r(c)) + (r(b)/r(d))) = (r((a * d) + (b * c))/r(c * d)))`

Proof

Definitions occuring in Statement :  rdiv: `(x/y)` req: `x = y` radd: `a + b` int-to-real: `r(n)` nat_plus: `ℕ+` uall: `∀[x:A]. B[x]` multiply: `n * m` add: `n + m` int: `ℤ`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` nat_plus: `ℕ+` uimplies: `b supposing a` rneq: `x ≠ y` guard: `{T}` or: `P ∨ Q` all: `∀x:A. B[x]` iff: `P `⇐⇒` Q` and: `P ∧ Q` rev_implies: `P `` Q` implies: `P `` Q` decidable: `Dec(P)` satisfiable_int_formula: `satisfiable_int_formula(fmla)` exists: `∃x:A. B[x]` false: `False` not: `¬A` top: `Top` prop: `ℙ` uiff: `uiff(P;Q)` rev_uimplies: `rev_uimplies(P;Q)` itermConstant: `"const"` req_int_terms: `t1 ≡ t2` rdiv: `(x/y)`
Lemmas referenced :  req_witness radd_wf rdiv_wf int-to-real_wf rless-int nat_plus_properties decidable__lt satisfiable-full-omega-tt intformand_wf intformnot_wf intformless_wf itermConstant_wf itermVar_wf int_formula_prop_and_lemma int_formula_prop_not_lemma int_formula_prop_less_lemma int_term_value_constant_lemma int_term_value_var_lemma int_formula_prop_wf rless_wf mul_bounds_1b nat_plus_wf rmul_wf rneq_functionality rmul-int req_weakening rmul_preserves_req req_wf rinv_wf2 real_term_polynomial itermSubtract_wf itermMultiply_wf itermAdd_wf real_term_value_const_lemma real_term_value_sub_lemma real_term_value_mul_lemma real_term_value_add_lemma real_term_value_var_lemma req-iff-rsub-is-0 uiff_transitivity req_functionality rmul_functionality rdiv_functionality req_transitivity req_inversion radd-int radd_functionality rinv-of-rmul rmul-rinv rmul-rinv3 rmul-int-rdiv
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis setElimination rename because_Cache independent_isectElimination sqequalRule inrFormation dependent_functionElimination productElimination independent_functionElimination natural_numberEquality unionElimination dependent_pairFormation lambdaEquality int_eqEquality intEquality isect_memberEquality voidElimination voidEquality independent_pairFormation computeAll addEquality multiplyEquality

Latex:
\mforall{}[a,b:\mBbbZ{}].  \mforall{}[c,d:\mBbbN{}\msupplus{}].    (((r(a)/r(c))  +  (r(b)/r(d)))  =  (r((a  *  d)  +  (b  *  c))/r(c  *  d)))

Date html generated: 2017_10_03-AM-08_38_00
Last ObjectModification: 2017_07_28-AM-07_30_25

Theory : reals

Home Index