Nuprl Lemma : qexp-zero
∀[r:ℚ]. (r ↑ 0 = 1 ∈ ℚ)
Proof
Definitions occuring in Statement :
qexp: r ↑ n,
rationals: ℚ,
uall: ∀[x:A]. B[x],
natural_number: $n,
equal: s = t ∈ T
Lemmas referenced :
exp_zero_q
Rules used in proof :
cut,
lemma_by_obid,
hypothesis
Latex:
\mforall{}[r:\mBbbQ{}]. (r \muparrow{} 0 = 1)
Date html generated:
2016_05_15-PM-11_08_44
Last ObjectModification:
2015_12_27-PM-07_42_49
Theory : rationals
Home
Index