Nuprl Lemma : exp_assoced

n:ℕ+. ∀x,y:ℤ.  (x^n y^n ⇐⇒ y)


Proof




Definitions occuring in Statement :  assoced: b exp: i^n nat_plus: + all: x:A. B[x] iff: ⇐⇒ Q int:
Definitions unfolded in proof :  all: x:A. B[x] iff: ⇐⇒ Q and: P ∧ Q implies:  Q member: t ∈ T prop: uall: [x:A]. B[x] subtype_rel: A ⊆B rev_implies:  Q assoced: b exists: x:A. B[x] uimplies: supposing a
Lemmas referenced :  assoced_wf exp_wf2 nat_plus_subtype_nat nat_plus_wf exp-divides-exp2 divides_wf assoced_functionality_wrt_assoced exp_functionality_wrt_assoced assoced_weakening
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation independent_pairFormation cut lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality applyEquality hypothesis sqequalRule because_Cache intEquality productElimination promote_hyp dependent_functionElimination independent_functionElimination dependent_pairFormation independent_isectElimination

Latex:
\mforall{}n:\mBbbN{}\msupplus{}.  \mforall{}x,y:\mBbbZ{}.    (x\^{}n  \msim{}  y\^{}n  \mLeftarrow{}{}\mRightarrow{}  x  \msim{}  y)



Date html generated: 2018_05_21-PM-01_11_05
Last ObjectModification: 2018_01_28-PM-02_04_05

Theory : num_thy_1


Home Index