Nuprl Lemma : multiply_functionality_wrt_le

[i1,i2:ℕ]. ∀[j1,j2:ℤ].  ((i1 i2) ≤ (j1 j2)) supposing ((i2 ≤ j2) and (i1 ≤ j1))


Definitions occuring in Statement :  nat: uimplies: supposing a uall: [x:A]. B[x] le: A ≤ B multiply: m int:
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a le: A ≤ B and: P ∧ Q not: ¬A implies:  Q false: False nat: prop: ge: i ≥  all: x:A. B[x] decidable: Dec(P) or: P ∨ Q satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] top: Top
Lemmas referenced :  int_term_value_mul_lemma itermMultiply_wf int_formula_prop_wf int_term_value_var_lemma int_term_value_constant_lemma int_formula_prop_le_lemma int_formula_prop_not_lemma int_formula_prop_and_lemma itermVar_wf itermConstant_wf intformle_wf intformnot_wf intformand_wf satisfiable-full-omega-tt decidable__le nat_properties mul_preserves_le nat_wf le_wf less_than'_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule sqequalHypSubstitution productElimination thin independent_pairEquality lambdaEquality dependent_functionElimination hypothesisEquality because_Cache lemma_by_obid isectElimination multiplyEquality setElimination rename hypothesis axiomEquality equalityTransitivity equalitySymmetry isect_memberEquality intEquality voidElimination independent_isectElimination dependent_set_memberEquality natural_numberEquality unionElimination dependent_pairFormation int_eqEquality voidEquality independent_pairFormation computeAll

\mforall{}[i1,i2:\mBbbN{}].  \mforall{}[j1,j2:\mBbbZ{}].    ((i1  *  i2)  \mleq{}  (j1  *  j2))  supposing  ((i2  \mleq{}  j2)  and  (i1  \mleq{}  j1))

Date html generated: 2016_05_14-AM-07_20_33
Last ObjectModification: 2016_01_07-PM-03_59_57

Theory : int_2

Home Index