Nuprl Lemma : p-shift-0

∀p,n:ℕ⁺. (p-shift(p;0(p);n) = 0(p) ∈ p-adics(p))

Proof

Definitions occuring in Statement : p-shift: p-shift(p;a;k), p-int: k(p), p-adics: p-adics(p), nat_plus: ℕ⁺, all: ∀x:A. B[x], natural_number: $n, equal: s = t ∈ T
Definitions unfolded in proof : all: ∀x:A. B[x], uall: ∀[x:A]. B[x], member: t ∈ T, uimplies: b supposing a, uiff: uiff(P;Q), and: P ∧ Q, rev_uimplies: rev_uimplies(P;Q), p-int: k(p), p-reduce: i mod(p^n), nat: ℕ, nat_plus: ℕ⁺, decidable: Dec(P), or: P ∨ Q, not: ¬A, implies: P ⇒ Q, satisfiable_int_formula: satisfiable_int_formula(fmla), exists: ∃x:A. B[x], false: False, prop: ℙ, int_seg: {i..j^-}, lelt: i ≤ j < k, le: A ≤ B, less_than': less_than'(a;b), p-shift: p-shift(p;a;k), subtype_rel: A ⊆r B
Lemmas referenced : equal-p-adics, p-shift_wf, p-int_wf, nat_plus_wf, modulus_base, exp_wf_nat_plus, nat_plus_properties, decidable__le, full-omega-unsat, intformand_wf, intformnot_wf, intformle_wf, itermConstant_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_var_lemma, int_formula_prop_less_lemma, int_formula_prop_wf, istype-le, istype-false, exp-positive, istype-less_than, exp_wf2, itermAdd_wf, int_term_value_add_lemma, decidable__lt, zero-div-rem, exp_wf3, nat_plus_inc_int_nzero
Rules used in proof : sqequalSubstitution, sqequalTransitivity, computationStep, sqequalReflexivity, lambdaFormation_alt, cut, introduction, extract_by_obid, sqequalHypSubstitution, isectElimination, thin, hypothesisEquality, because_Cache, closedConclusion, natural_numberEquality, hypothesis, independent_isectElimination, productElimination, inhabitedIsType, universeIsType, sqequalRule, dependent_set_memberEquality_alt, setElimination, rename, dependent_functionElimination, unionElimination, approximateComputation, independent_functionElimination, dependent_pairFormation_alt, lambdaEquality_alt, int_eqEquality, Error :memTop, independent_pairFormation, voidElimination, productIsType, functionExtensionality, addEquality, applyEquality

Latex:
\mforall{}p,n:\mBbbN{}\msupplus{}. (p-shift(p;0(p);n) = 0(p)) Date html generated: 2020_05_19-PM-10_08_23 Last ObjectModification: 2020_01_08-PM-06_08_20 Theory : rings_1 Home Index