### Nuprl Lemma : nat_op_wf

`∀[g:IMonoid]. ∀[n:ℕ]. ∀[e:|g|].  (n x(*;e) e ∈ |g|)`

Proof

Definitions occuring in Statement :  nat_op: `n x(op;id) e` imon: `IMonoid` grp_id: `e` grp_op: `*` grp_car: `|g|` nat: `ℕ` uall: `∀[x:A]. B[x]` member: `t ∈ T`
Definitions unfolded in proof :  nat_op: `n x(op;id) e` uall: `∀[x:A]. B[x]` member: `t ∈ T` imon: `IMonoid` nat: `ℕ` so_lambda: `λ2x.t[x]` so_apply: `x[s]`
Lemmas referenced :  itop_wf grp_car_wf grp_op_wf grp_id_wf int_seg_wf nat_wf imon_wf
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep isect_memberFormation introduction cut lemma_by_obid sqequalHypSubstitution isectElimination thin setElimination rename hypothesisEquality hypothesis natural_numberEquality lambdaEquality axiomEquality equalityTransitivity equalitySymmetry isect_memberEquality because_Cache

Latex:
\mforall{}[g:IMonoid].  \mforall{}[n:\mBbbN{}].  \mforall{}[e:|g|].    (n  x(*;e)  e  \mmember{}  |g|)

Date html generated: 2016_05_15-PM-00_15_13
Last ObjectModification: 2015_12_26-PM-11_40_35

Theory : groups_1

Home Index