Nuprl Lemma : bpa-norm_wf

p:ℕ+. ∀x:basic-padic(p).  (bpa-norm(p;x) ∈ basic-padic(p))


Proof




Definitions occuring in Statement :  bpa-norm: bpa-norm(p;x) basic-padic: basic-padic(p) nat_plus: + all: x:A. B[x] member: t ∈ T
Definitions unfolded in proof :  all: x:A. B[x] basic-padic: basic-padic(p) bpa-norm: bpa-norm(p;x) member: t ∈ T uall: [x:A]. B[x] nat: implies:  Q bool: 𝔹 unit: Unit it: btrue: tt ifthenelse: if then else fi  uiff: uiff(P;Q) and: P ∧ Q uimplies: supposing a le: A ≤ B less_than': less_than'(a;b) false: False not: ¬A prop: bfalse: ff exists: x:A. B[x] or: P ∨ Q sq_type: SQType(T) guard: {T} bnot: ¬bb assert: b ge: i ≥  int_upper: {i...} p-adics: p-adics(p) nat_plus: + decidable: Dec(P) iff: ⇐⇒ Q rev_implies:  Q subtype_rel: A ⊆B top: Top true: True int_seg: {i..j-} nequal: a ≠ b ∈  lelt: i ≤ j < k p-units: p-units(p) satisfiable_int_formula: satisfiable_int_formula(fmla)
Lemmas referenced :  eq_int_wf bool_wf eqtt_to_assert assert_of_eq_int false_wf le_wf eqff_to_assert equal_wf bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot neg_assert_of_eq_int upper_subtype_nat nat_properties nequal-le-implies zero-add decidable__lt not-lt-2 add_functionality_wrt_le add-commutes le-add-cancel less_than_wf int_seg_wf exp_wf2 p-shift_wf p-unitize_wf not-equal-2 p-units_wf p-adics_wf p-mul_wf p-int_wf subtract_wf int_seg_properties int_upper_properties nat_plus_properties decidable__le full-omega-unsat intformand_wf intformnot_wf intformle_wf itermConstant_wf itermSubtract_wf itermVar_wf intformless_wf itermAdd_wf 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_term_value_add_lemma int_formula_prop_wf basic-padic_wf nat_plus_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation sqequalHypSubstitution productElimination thin sqequalRule cut introduction extract_by_obid isectElimination setElimination rename because_Cache hypothesis natural_numberEquality unionElimination equalityElimination independent_isectElimination independent_pairEquality dependent_set_memberEquality equalityTransitivity equalitySymmetry independent_pairFormation hypothesisEquality dependent_pairFormation promote_hyp dependent_functionElimination instantiate cumulativity independent_functionElimination voidElimination hypothesis_subsumption applyEquality lambdaEquality isect_memberEquality voidEquality intEquality productEquality addEquality setEquality approximateComputation int_eqEquality

Latex:
\mforall{}p:\mBbbN{}\msupplus{}.  \mforall{}x:basic-padic(p).    (bpa-norm(p;x)  \mmember{}  basic-padic(p))



Date html generated: 2018_05_21-PM-03_25_13
Last ObjectModification: 2018_05_19-AM-08_22_41

Theory : rings_1


Home Index