Nuprl Lemma : add-div-when-divides2

a,b,x,y:ℤ. ∀c:ℤ-o.  ((((a ÷ c) x) ((b ÷ c) y)) (((a x) (b y)) ÷ c) ∈ ℤsupposing ((c a) and (c b))


Proof




Definitions occuring in Statement :  divides: a int_nzero: -o uimplies: supposing a all: x:A. B[x] divide: n ÷ m multiply: m add: m int: equal: t ∈ T
Definitions unfolded in proof :  all: x:A. B[x] uimplies: supposing a member: t ∈ T divides: a exists: x:A. B[x] uall: [x:A]. B[x] int_nzero: -o prop: true: True nequal: a ≠ b ∈  decidable: Dec(P) or: P ∨ Q not: ¬A implies:  Q satisfiable_int_formula: satisfiable_int_formula(fmla) false: False top: Top sq_type: SQType(T) guard: {T} squash: T subtype_rel: A ⊆B iff: ⇐⇒ Q and: P ∧ Q rev_implies:  Q
Lemmas referenced :  divides_wf int_nzero_wf istype-int divide_wfa subtype_base_sq int_subtype_base int_nzero_properties decidable__equal_int full-omega-unsat intformnot_wf intformeq_wf itermAdd_wf itermMultiply_wf itermVar_wf int_formula_prop_not_lemma istype-void int_formula_prop_eq_lemma int_term_value_add_lemma int_term_value_mul_lemma int_term_value_var_lemma int_formula_prop_wf divide-exact equal_wf squash_wf true_wf istype-universe add_functionality_wrt_eq subtype_rel_self iff_weakening_equal div-cancel2
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :lambdaFormation_alt,  Error :isect_memberFormation_alt,  introduction cut sqequalHypSubstitution productElimination thin hypothesis Error :universeIsType,  extract_by_obid isectElimination setElimination rename hypothesisEquality sqequalRule Error :isect_memberEquality_alt,  axiomEquality Error :isectIsTypeImplies,  Error :inhabitedIsType,  intEquality multiplyEquality because_Cache natural_numberEquality instantiate cumulativity independent_isectElimination dependent_functionElimination unionElimination approximateComputation independent_functionElimination Error :dependent_pairFormation_alt,  Error :lambdaEquality_alt,  int_eqEquality voidElimination equalityTransitivity equalitySymmetry addEquality applyEquality imageElimination universeEquality imageMemberEquality baseClosed

Latex:
\mforall{}a,b,x,y:\mBbbZ{}.  \mforall{}c:\mBbbZ{}\msupminus{}\msupzero{}.
    ((((a  \mdiv{}  c)  *  x)  +  ((b  \mdiv{}  c)  *  y))  =  (((a  *  x)  +  (b  *  y))  \mdiv{}  c))  supposing  ((c  |  a)  and  (c  |  b))



Date html generated: 2019_06_20-PM-02_20_38
Last ObjectModification: 2019_03_06-AM-11_06_00

Theory : num_thy_1


Home Index