Nuprl Lemma : less-efficient-exp-ext
∀i:ℤ. ∀n:ℕ.  (∃j:{ℤ| (j = i^n ∈ ℤ)})
Proof
Definitions occuring in Statement : 
exp: i^n
, 
nat: ℕ
, 
all: ∀x:A. B[x]
, 
sq_exists: ∃x:{A| B[x]}
, 
int: ℤ
, 
equal: s = t ∈ T
Definitions unfolded in proof : 
squash: ↓T
, 
or: P ∨ Q
, 
guard: {T}
, 
prop: ℙ
, 
has-value: (a)↓
, 
implies: P 
⇒ Q
, 
all: ∀x:A. B[x]
, 
and: P ∧ Q
, 
strict4: strict4(F)
, 
uimplies: b supposing a
, 
so_apply: x[s]
, 
top: Top
, 
so_lambda: λ2x.t[x]
, 
so_apply: x[s1;s2;s3;s4]
, 
so_lambda: so_lambda(x,y,z,w.t[x; y; z; w])
, 
uall: ∀[x:A]. B[x]
, 
decidable__int_equal, 
decidable__equal_int, 
so_apply: x[s1;s2]
, 
genrec: genrec, 
natrec: natrec, 
less-efficient-exp, 
member: t ∈ T
Lemmas referenced : 
decidable__int_equal, 
decidable__equal_int, 
less-efficient-exp
Rules used in proof : 
inlFormation, 
exceptionSqequal, 
imageElimination, 
imageMemberEquality, 
because_Cache, 
inrFormation, 
decideExceptionCases, 
closedConclusion, 
baseApply, 
independent_functionElimination, 
dependent_functionElimination, 
equalityEquality, 
sqleReflexivity, 
unionElimination, 
unionEquality, 
equalitySymmetry, 
equalityTransitivity, 
hypothesisEquality, 
callbyvalueDecide, 
lambdaFormation, 
independent_pairFormation, 
independent_isectElimination, 
voidEquality, 
voidElimination, 
isect_memberEquality, 
baseClosed, 
isectElimination, 
sqequalHypSubstitution, 
thin, 
sqequalRule, 
hypothesis, 
extract_by_obid, 
instantiate, 
cut, 
sqequalReflexivity, 
computationStep, 
sqequalTransitivity, 
sqequalSubstitution, 
introduction
Latex:
\mforall{}i:\mBbbZ{}.  \mforall{}n:\mBbbN{}.    (\mexists{}j:\{\mBbbZ{}|  (j  =  i\^{}n)\})
Date html generated:
2016_07_08-PM-05_05_04
Last ObjectModification:
2016_07_05-PM-02_44_11
Theory : general
Home
Index