Nuprl Lemma : rmul-int-rdiv

[x:ℝ]. ∀[a,b:ℤ].  ((r(a) (r(b)/x)) (r(a b)/x)) supposing x ≠ r0


Proof




Definitions occuring in Statement :  rdiv: (x/y) rneq: x ≠ y req: y rmul: b int-to-real: r(n) real: uimplies: supposing a uall: [x:A]. B[x] multiply: m natural_number: $n int:
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a uiff: uiff(P;Q) and: P ∧ Q rev_uimplies: rev_uimplies(P;Q) implies:  Q prop: all: x:A. B[x] decidable: Dec(P) or: P ∨ Q satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] false: False not: ¬A top: Top
Lemmas referenced :  rmul-int rmul-rdiv-cancel2 rmul-rdiv-cancel rmul_comm rmul_functionality rmul-ac req_transitivity rmul-assoc req_inversion req_functionality uiff_transitivity int_formula_prop_wf int_term_value_var_lemma int_term_value_mul_lemma int_formula_prop_eq_lemma int_formula_prop_not_lemma itermVar_wf itermMultiply_wf intformeq_wf intformnot_wf satisfiable-full-omega-tt decidable__equal_int req-int req_weakening req_wf real_wf rneq_wf req_witness rdiv_wf int-to-real_wf rmul_wf rmul_preserves_req
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis independent_isectElimination because_Cache multiplyEquality productElimination independent_functionElimination intEquality sqequalRule isect_memberEquality natural_numberEquality equalityTransitivity equalitySymmetry dependent_functionElimination unionElimination dependent_pairFormation lambdaEquality int_eqEquality voidElimination voidEquality computeAll

Latex:
\mforall{}[x:\mBbbR{}].  \mforall{}[a,b:\mBbbZ{}].    ((r(a)  *  (r(b)/x))  =  (r(a  *  b)/x))  supposing  x  \mneq{}  r0



Date html generated: 2016_05_18-AM-07_27_53
Last ObjectModification: 2016_01_17-AM-01_58_17

Theory : reals


Home Index