Nuprl Lemma : mul-imax

[n:ℕ]. ∀[a,b:ℤ].  ((n imax(a;b)) imax(n a;n b) ∈ ℤ)


Proof




Definitions occuring in Statement :  imax: imax(a;b) nat: uall: [x:A]. B[x] multiply: m int: equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T squash: T prop: nat: true: True subtype_rel: A ⊆B uimplies: supposing a guard: {T} iff: ⇐⇒ Q and: P ∧ Q rev_implies:  Q implies:  Q all: x:A. B[x] bool: 𝔹 unit: Unit it: btrue: tt uiff: uiff(P;Q) ifthenelse: if then else fi  bfalse: ff exists: x:A. B[x] or: P ∨ Q sq_type: SQType(T) bnot: ¬bb assert: b false: False not: ¬A ge: i ≥  decidable: Dec(P) satisfiable_int_formula: satisfiable_int_formula(fmla) top: Top
Lemmas referenced :  equal_wf squash_wf true_wf imax_unfold iff_weakening_equal le_int_wf bool_wf eqtt_to_assert assert_of_le_int eqff_to_assert bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot le_wf nat_wf mul_preserves_le nat_properties decidable__le satisfiable-full-omega-tt intformand_wf intformnot_wf intformle_wf itermVar_wf int_formula_prop_and_lemma int_formula_prop_not_lemma int_formula_prop_le_lemma int_term_value_var_lemma int_formula_prop_wf decidable__equal_int intformeq_wf itermMultiply_wf int_formula_prop_eq_lemma int_term_value_mul_lemma
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut applyEquality thin lambdaEquality sqequalHypSubstitution imageElimination extract_by_obid isectElimination hypothesisEquality equalityTransitivity hypothesis equalitySymmetry universeEquality because_Cache multiplyEquality setElimination rename natural_numberEquality sqequalRule imageMemberEquality baseClosed independent_isectElimination productElimination independent_functionElimination lambdaFormation unionElimination equalityElimination dependent_pairFormation promote_hyp dependent_functionElimination instantiate voidElimination cumulativity intEquality isect_memberEquality axiomEquality int_eqEquality voidEquality independent_pairFormation computeAll

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[a,b:\mBbbZ{}].    ((n  *  imax(a;b))  =  imax(n  *  a;n  *  b))



Date html generated: 2017_04_14-AM-09_13_24
Last ObjectModification: 2017_02_27-PM-03_51_07

Theory : int_2


Home Index