Nuprl Lemma : rng_times_nat_op_r

[r:Rng]. ∀[a,b:|r|]. ∀[n:ℕ].  (((n ⋅b) a) (n ⋅(b a)) ∈ |r|)


Proof




Definitions occuring in Statement :  rng_nat_op: n ⋅e rng: Rng rng_times: * rng_car: |r| nat: uall: [x:A]. B[x] infix_ap: y equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T rng_nat_op: n ⋅e mon_nat_op: n ⋅ e nat_op: x(op;id) e mon_itop: Π lb ≤ i < ub. E[i] rng_sum: rng_sum rng: Rng nat: uimplies: supposing a 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] false: False implies:  Q not: ¬A top: Top and: P ∧ Q prop: so_lambda: λ2x.t[x] so_apply: x[s]
Lemmas referenced :  int_seg_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 rng_times_sum_r rng_wf rng_car_wf nat_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut hypothesis lemma_by_obid sqequalRule sqequalHypSubstitution isect_memberEquality isectElimination thin hypothesisEquality axiomEquality because_Cache setElimination rename natural_numberEquality independent_isectElimination dependent_functionElimination unionElimination dependent_pairFormation lambdaEquality int_eqEquality intEquality voidElimination voidEquality independent_pairFormation computeAll

Latex:
\mforall{}[r:Rng].  \mforall{}[a,b:|r|].  \mforall{}[n:\mBbbN{}].    (((n  \mcdot{}r  b)  *  a)  =  (n  \mcdot{}r  (b  *  a)))



Date html generated: 2016_05_15-PM-00_28_30
Last ObjectModification: 2016_01_15-AM-08_51_25

Theory : rings_1


Home Index