Nuprl Lemma : exp_unroll_q

[n:ℕ+]. ∀[e:ℚ].  (e ↑ (e ↑ e) ∈ ℚ)


Proof




Definitions occuring in Statement :  qexp: r ↑ n qmul: s rationals: nat_plus: + uall: [x:A]. B[x] subtract: m natural_number: $n equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T subtype_rel: A ⊆B qrng: <ℚ+*> rng_car: |r| pi1: fst(t) rng_times: * pi2: snd(t) infix_ap: y q-rng-nexp: q-rng-nexp(r;n) nat: nat_plus: + all: x:A. B[x] decidable: Dec(P) or: P ∨ Q uimplies: supposing a not: ¬A implies:  Q satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] false: False and: P ∧ Q prop: true: True rev_implies:  Q squash: T guard: {T} iff: ⇐⇒ Q
Lemmas referenced :  rng_nexp_unroll qrng_wf crng_subtype_rng rationals_wf nat_plus_subtype_nat subtract_wf nat_plus_properties decidable__le full-omega-unsat intformand_wf intformnot_wf intformle_wf itermConstant_wf itermSubtract_wf itermVar_wf intformless_wf istype-int int_formula_prop_and_lemma int_formula_prop_not_lemma int_formula_prop_le_lemma int_term_value_constant_lemma int_term_value_subtract_lemma int_term_value_var_lemma int_formula_prop_less_lemma int_formula_prop_wf istype-le nat_plus_wf equal_wf squash_wf true_wf istype-universe qexp-eq-q-rng-nexp qmul_wf subtype_rel_self iff_weakening_equal
Rules used in proof :  cut introduction extract_by_obid sqequalHypSubstitution sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isectElimination thin hypothesis applyEquality sqequalRule hypothesisEquality dependent_set_memberEquality_alt setElimination rename natural_numberEquality dependent_functionElimination unionElimination independent_isectElimination approximateComputation independent_functionElimination dependent_pairFormation_alt lambdaEquality_alt int_eqEquality Error :memTop,  independent_pairFormation universeIsType voidElimination because_Cache isect_memberFormation_alt imageElimination equalityTransitivity equalitySymmetry instantiate universeEquality inhabitedIsType imageMemberEquality baseClosed productElimination

Latex:
\mforall{}[n:\mBbbN{}\msupplus{}].  \mforall{}[e:\mBbbQ{}].    (e  \muparrow{}  n  =  (e  \muparrow{}  n  -  1  *  e))



Date html generated: 2020_05_20-AM-09_24_39
Last ObjectModification: 2020_01_25-AM-11_48_52

Theory : rationals


Home Index