`∀p:ℕ+. ∀x,y:p-adics(p).  uiff(x = y ∈ p-adics(p);∀n:ℕ+. ((x n) ≡ (y n) mod p^n))`

Proof

Definitions occuring in Statement :  p-adics: `p-adics(p)` eqmod: `a ≡ b mod m` exp: `i^n` nat_plus: `ℕ+` uiff: `uiff(P;Q)` all: `∀x:A. B[x]` apply: `f a` equal: `s = t ∈ T`
Definitions unfolded in proof :  all: `∀x:A. B[x]` uiff: `uiff(P;Q)` and: `P ∧ Q` uimplies: `b supposing a` member: `t ∈ T` uall: `∀[x:A]. B[x]` subtype_rel: `A ⊆r B` nat_plus: `ℕ+` p-adics: `p-adics(p)` int_seg: `{i..j-}` prop: `ℙ` so_lambda: `λ2x.t[x]` so_apply: `x[s]` decidable: `Dec(P)` or: `P ∨ Q` iff: `P `⇐⇒` Q` not: `¬A` rev_implies: `P `` Q` implies: `P `` Q` false: `False` subtract: `n - m` le: `A ≤ B` less_than': `less_than'(a;b)` true: `True` lelt: `i ≤ j < k` guard: `{T}` nat: `ℕ` satisfiable_int_formula: `satisfiable_int_formula(fmla)` exists: `∃x:A. B[x]` top: `Top` int_nzero: `ℤ-o` nequal: `a ≠ b ∈ T `
Lemmas referenced :  equal-p-adics eqmod_weakening exp_wf2 nat_plus_subtype_nat int_seg_wf and_wf equal_wf nat_plus_wf p-adics_wf all_wf eqmod_wf decidable__lt false_wf not-lt-2 less-iff-le condition-implies-le minus-add minus-one-mul zero-add minus-one-mul-top add-commutes add_functionality_wrt_le add-associates add-zero le-add-cancel less_than_wf less_than_transitivity2 decidable__le full-omega-unsat intformand_wf intformnot_wf intformle_wf itermConstant_wf itermVar_wf intformless_wf 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 le_wf modulus_base modulus-equal-iff-eqmod int_seg_properties nat_plus_properties decidable__equal_int intformeq_wf int_formula_prop_eq_lemma mod_bounds_1 exp_wf3 subtype_rel_sets nequal_wf equal-wf-base int_subtype_base mod_bounds lelt_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation independent_pairFormation isect_memberFormation cut introduction axiomEquality hypothesis thin rename extract_by_obid sqequalHypSubstitution isectElimination hypothesisEquality productElimination independent_isectElimination dependent_functionElimination applyEquality sqequalRule setElimination because_Cache lambdaEquality natural_numberEquality equalitySymmetry dependent_set_memberEquality equalityTransitivity functionEquality intEquality applyLambdaEquality functionExtensionality addEquality unionElimination voidElimination independent_functionElimination minusEquality approximateComputation dependent_pairFormation int_eqEquality isect_memberEquality voidEquality setEquality baseClosed

Latex:
\mforall{}p:\mBbbN{}\msupplus{}.  \mforall{}x,y:p-adics(p).    uiff(x  =  y;\mforall{}n:\mBbbN{}\msupplus{}.  ((x  n)  \mequiv{}  (y  n)  mod  p\^{}n))

Date html generated: 2018_05_21-PM-03_18_42
Last ObjectModification: 2018_05_19-AM-08_10_23

Theory : rings_1

Home Index