Nuprl Lemma : exp-divides-exp
∀x,y:ℤ. (x | y ⇐⇒ ∀n:ℕ+. (x^n | y^n))
Proof
Definitions occuring in Statement :
divides: b | a,
exp: i^n,
nat_plus: ℕ+,
all: ∀x:A. B[x],
iff: P ⇐⇒ Q,
int: ℤ
Definitions unfolded in proof :
all: ∀x:A. B[x],
iff: P ⇐⇒ Q,
and: P ∧ Q,
implies: P ⇒ Q,
member: t ∈ T,
prop: ℙ,
uall: ∀[x:A]. B[x],
rev_implies: P ⇐ Q,
so_lambda: λ2x.t[x],
subtype_rel: A ⊆r B,
so_apply: x[s],
uimplies: b 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