Nuprl Lemma : radd_functionality

[a1,a2,b1,b2:ℝ].  ((a1 b1) (a2 b2)) supposing ((a1 a2) and (b1 b2))


Definitions occuring in Statement :  req: y radd: b real: uimplies: supposing a uall: [x:A]. B[x]
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a squash: T prop: true: True subtype_rel: A ⊆B guard: {T} iff: ⇐⇒ Q and: P ∧ Q rev_implies:  Q implies:  Q cand: c∧ B length: ||as|| list_ind: list_ind cons: [a b] nil: [] it: all: x:A. B[x] top: Top int_seg: {i..j-} decidable: Dec(P) or: P ∨ Q sq_type: SQType(T) select: L[n] le: A ≤ B less_than': less_than'(a;b) false: False not: ¬A subtract: m lelt: i ≤ j < k satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x]
Lemmas referenced :  radd_wf req_witness int_seg_wf int_formula_prop_wf int_formula_prop_le_lemma int_term_value_constant_lemma int_term_value_var_lemma int_formula_prop_less_lemma int_formula_prop_and_lemma intformle_wf itermConstant_wf itermVar_wf intformless_wf intformand_wf satisfiable-full-omega-tt int_seg_cases false_wf int_seg_subtype int_seg_properties int_subtype_base subtype_base_sq decidable__equal_int length_of_nil_lemma length_of_cons_lemma length_wf nil_wf real_wf cons_wf radd-list_functionality iff_weakening_equal radd-as-radd-list true_wf squash_wf req_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut applyEquality thin lambdaEquality sqequalHypSubstitution imageElimination lemma_by_obid isectElimination hypothesisEquality equalityTransitivity hypothesis equalitySymmetry because_Cache natural_numberEquality sqequalRule imageMemberEquality baseClosed universeEquality independent_isectElimination productElimination independent_functionElimination independent_pairFormation lambdaFormation dependent_functionElimination isect_memberEquality voidElimination voidEquality setElimination rename unionElimination instantiate cumulativity intEquality hypothesis_subsumption addEquality dependent_pairFormation int_eqEquality computeAll

\mforall{}[a1,a2,b1,b2:\mBbbR{}].    ((a1  +  b1)  =  (a2  +  b2))  supposing  ((a1  =  a2)  and  (b1  =  b2))

Date html generated: 2016_05_18-AM-06_51_00
Last ObjectModification: 2016_01_17-AM-01_46_23

Theory : reals

Home Index