### 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: `P `` Q` bool: `𝔹` unit: `Unit` it: `⋅` btrue: `tt` ifthenelse: `if b then t else f fi ` uiff: `uiff(P;Q)` and: `P ∧ Q` uimplies: `b 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 ≥ j ` int_upper: `{i...}` p-adics: `p-adics(p)` nat_plus: `ℕ+` decidable: `Dec(P)` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` subtype_rel: `A ⊆r B` top: `Top` true: `True` int_seg: `{i..j-}` nequal: `a ≠ b ∈ T ` 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: