`∀[r:Rng]. ∀[a1,a2:ℤ].  (int-to-ring(r;a1 + a2) = (int-to-ring(r;a1) +r int-to-ring(r;a2)) ∈ |r|)`

Proof

Definitions occuring in Statement :  int-to-ring: `int-to-ring(r;n)` rng: `Rng` rng_plus: `+r` rng_car: `|r|` uall: `∀[x:A]. B[x]` infix_ap: `x f y` add: `n + m` int: `ℤ` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` all: `∀x:A. B[x]` decidable: `Dec(P)` or: `P ∨ Q` uimplies: `b supposing a` sq_type: `SQType(T)` implies: `P `` Q` guard: `{T}` squash: `↓T` prop: `ℙ` rng: `Rng` top: `Top` infix_ap: `x f y` true: `True` subtype_rel: `A ⊆r B` iff: `P `⇐⇒` Q` and: `P ∧ Q` rev_implies: `P `` Q` int-to-ring: `int-to-ring(r;n)` bool: `𝔹` unit: `Unit` it: `⋅` btrue: `tt` uiff: `uiff(P;Q)` ifthenelse: `if b then t else f fi ` bfalse: `ff` exists: `∃x:A. B[x]` bnot: `¬bb` assert: `↑b` false: `False` not: `¬A` satisfiable_int_formula: `satisfiable_int_formula(fmla)` nat: `ℕ` le: `A ≤ B` less_than': `less_than'(a;b)` ge: `i ≥ j ` less_than: `a < b` subtract: `n - m`
Lemmas referenced :  rng_wf decidable__equal_int subtype_base_sq int_subtype_base equal_wf squash_wf true_wf rng_car_wf int-to-ring-zero rng_zero_wf rng_plus_wf int-to-ring-minus-one rng_one_wf subtype_rel_self iff_weakening_equal rng_plus_inv lt_int_wf bool_wf eqtt_to_assert assert_of_lt_int eqff_to_assert bool_cases_sqequal bool_subtype_base assert-bnot less_than_wf full-omega-unsat intformand_wf intformless_wf itermAdd_wf itermVar_wf itermConstant_wf intformnot_wf int_formula_prop_and_lemma int_formula_prop_less_lemma int_term_value_add_lemma int_term_value_var_lemma int_term_value_constant_lemma int_formula_prop_not_lemma int_formula_prop_wf intformeq_wf int_formula_prop_eq_lemma rng_nat_op_add decidable__le intformle_wf int_formula_prop_le_lemma le_wf false_wf infix_ap_wf rng_nat_op_wf rng_nat_op_one itermMinus_wf int_term_value_minus_lemma rng_minus_wf rng_minus_over_plus rng_plus_assoc rng_plus_comm rng_plus_inv_assoc decidable__lt subtract_wf subtract-add-cancel int-to-ring_wf rng_plus_zero nat_properties ge_wf absval_wf itermSubtract_wf int_term_value_subtract_lemma nat_wf add_nat_wf add-is-int-iff absval_unfold top_wf add-associates add-swap add-commutes zero-add rng_plus_ac_1
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut hypothesis intEquality sqequalRule sqequalHypSubstitution isect_memberEquality isectElimination thin hypothesisEquality axiomEquality because_Cache extract_by_obid lambdaFormation dependent_functionElimination minusEquality natural_numberEquality unionElimination instantiate cumulativity independent_isectElimination equalityTransitivity equalitySymmetry independent_functionElimination applyEquality lambdaEquality imageElimination universeEquality setElimination rename voidElimination voidEquality imageMemberEquality baseClosed productElimination addEquality equalityElimination dependent_pairFormation promote_hyp approximateComputation int_eqEquality independent_pairFormation dependent_set_memberEquality equalityUniverse levelHypothesis hyp_replacement applyLambdaEquality intWeakElimination pointwiseFunctionality baseApply closedConclusion lessCases sqequalAxiom

Latex:
\mforall{}[r:Rng].  \mforall{}[a1,a2:\mBbbZ{}].    (int-to-ring(r;a1  +  a2)  =  (int-to-ring(r;a1)  +r  int-to-ring(r;a2)))

Date html generated: 2018_05_21-PM-03_14_58
Last ObjectModification: 2018_05_19-AM-08_08_28

Theory : rings_1

Home Index