Nuprl Lemma : exp-divides-exp

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


Proof




Definitions occuring in Statement :  divides: a 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] rev_implies:  Q so_lambda: λ2x.t[x] subtype_rel: A ⊆B so_apply: x[s] uimplies: supposing a guard: {T} nat_plus: + less_than: a < b squash: T less_than': less_than'(a;b) true: True exp: i^n top: Top
Lemmas referenced :  one-mul mul-commutes primrec1_lemma less_than_wf assoced_transitivity assoced_weakening exp_functionality_wrt_assoced assoced_functionality_wrt_assoced gcd_wf gcd-exp divides-iff-gcd-assoced nat_plus_subtype_nat exp_wf2 all_wf divides_wf nat_plus_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation independent_pairFormation cut lemma_by_obid hypothesis sqequalHypSubstitution isectElimination thin hypothesisEquality sqequalRule lambdaEquality applyEquality because_Cache intEquality dependent_functionElimination productElimination independent_functionElimination independent_isectElimination dependent_set_memberEquality natural_numberEquality introduction imageMemberEquality baseClosed isect_memberEquality voidElimination voidEquality

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



Date html generated: 2016_05_15-PM-04_51_09
Last ObjectModification: 2016_01_16-AM-11_27_29

Theory : general


Home Index