Nuprl Lemma : qexp-positive-iff
∀n:ℕ. ∀r:ℚ.  (0 < r ↑ n 
⇐⇒ (n = 0 ∈ ℤ) ∨ 0 < r ∨ (r < 0 ∧ (↑isEven(n))))
Proof
Definitions occuring in Statement : 
qexp: r ↑ n
, 
qless: r < s
, 
rationals: ℚ
, 
isEven: isEven(n)
, 
nat: ℕ
, 
assert: ↑b
, 
all: ∀x:A. B[x]
, 
iff: P 
⇐⇒ Q
, 
or: P ∨ Q
, 
and: P ∧ Q
, 
natural_number: $n
, 
int: ℤ
, 
equal: s = t ∈ T
Definitions unfolded in proof : 
all: ∀x:A. B[x]
, 
member: t ∈ T
, 
and: P ∧ Q
, 
cand: A c∧ B
, 
iff: P 
⇐⇒ Q
, 
implies: P 
⇒ Q
, 
prop: ℙ
, 
uall: ∀[x:A]. B[x]
, 
nat: ℕ
, 
subtype_rel: A ⊆r B
, 
rev_implies: P 
⇐ Q
, 
or: P ∨ Q
Lemmas referenced : 
nat_wf, 
rationals_wf, 
equal-wf-T-base, 
iff_wf, 
qexp_wf, 
int-subtype-rationals, 
isEven_wf, 
assert_wf, 
and_wf, 
qless_wf, 
equal_wf, 
or_wf, 
qexp-sign
Rules used in proof : 
cut, 
lemma_by_obid, 
sqequalSubstitution, 
sqequalTransitivity, 
computationStep, 
sqequalReflexivity, 
lambdaFormation, 
hypothesis, 
sqequalHypSubstitution, 
dependent_functionElimination, 
thin, 
hypothesisEquality, 
productElimination, 
independent_pairFormation, 
isectElimination, 
intEquality, 
setElimination, 
rename, 
natural_numberEquality, 
applyEquality, 
because_Cache, 
sqequalRule, 
addLevel, 
impliesFunctionality, 
independent_functionElimination, 
baseClosed, 
productEquality
Latex:
\mforall{}n:\mBbbN{}.  \mforall{}r:\mBbbQ{}.    (0  <  r  \muparrow{}  n  \mLeftarrow{}{}\mRightarrow{}  (n  =  0)  \mvee{}  0  <  r  \mvee{}  (r  <  0  \mwedge{}  (\muparrow{}isEven(n))))
Date html generated:
2016_05_15-PM-11_09_10
Last ObjectModification:
2016_01_16-PM-09_25_50
Theory : rationals
Home
Index