`∀[p:{2...}]. (padic-ring(p) ∈ CRng)`

Proof

Definitions occuring in Statement :  padic-ring: `padic-ring(p)` crng: `CRng` int_upper: `{i...}` uall: `∀[x:A]. B[x]` member: `t ∈ T` natural_number: `\$n`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` crng: `CRng` rng: `Rng` p-adic-ring: `ℤ(p)` ring_p: `IsRing(T;plus;zero;neg;times;one)` rng_car: `|r|` pi1: `fst(t)` rng_plus: `+r` pi2: `snd(t)` rng_zero: `0` rng_minus: `-r` rng_times: `*` rng_one: `1` monoid_p: `IsMonoid(T;op;id)` group_p: `IsGroup(T;op;id;inv)` bilinear: `BiLinear(T;pl;tm)` ident: `Ident(T;op;id)` assoc: `Assoc(T;op)` inverse: `Inverse(T;op;id;inv)` infix_ap: `x f y` comm: `Comm(T;op)` and: `P ∧ Q` padic-ring: `padic-ring(p)` prop: `ℙ` rng_sig: `RngSig` int_upper: `{i...}` subtype_rel: `A ⊆r B` all: `∀x:A. B[x]` pa-mul: `pa-mul(p;x;y)` nat_plus: `ℕ+` decidable: `Dec(P)` or: `P ∨ Q` uimplies: `b supposing a` not: `¬A` implies: `P `` Q` satisfiable_int_formula: `satisfiable_int_formula(fmla)` exists: `∃x:A. B[x]` false: `False` pa-add: `pa-add(p;x;y)` cand: `A c∧ B` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` squash: `↓T` true: `True` guard: `{T}` basic-padic: `basic-padic(p)` bpa-add: `bpa-add(p;x;y)` bpa-equiv: `bpa-equiv(p;x;y)` nat: `ℕ` ge: `i ≥ j ` has-value: `(a)↓` top: `Top` int_seg: `{i..j-}` p-adics: `p-adics(p)` less_than': `less_than'(a;b)` le: `A ≤ B` assert: `↑b` bnot: `¬bb` bfalse: `ff` sq_type: `SQType(T)` ifthenelse: `if b then t else f fi ` uiff: `uiff(P;Q)` btrue: `tt` it: `⋅` unit: `Unit` bool: `𝔹` so_apply: `x[s]` so_lambda: `λ2x.t[x]` pa-int: `k(p)` subtract: `n - m` pa-minus: `pa-minus(p;x)` bpa-minus: `bpa-minus(p;x)` bpa-mul: `bpa-mul(p;x;y)` lelt: `i ≤ j < k` padic: `padic(p)` istype: `istype(T)` p-units: `p-units(p)`
Rules used in proof :  cut introduction extract_by_obid sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt hypothesis sqequalHypSubstitution isectElimination thin hypothesisEquality equalityTransitivity equalitySymmetry applyLambdaEquality setElimination rename sqequalRule dependent_set_memberEquality_alt productElimination universeIsType because_Cache natural_numberEquality dependent_pairEquality lambdaEquality applyEquality inrEquality functionEquality unionEquality productEquality lambdaFormation_alt dependent_functionElimination unionElimination independent_isectElimination approximateComputation independent_functionElimination dependent_pairFormation_alt lambdaEquality_alt int_eqEquality Error :memTop,  independent_pairFormation voidElimination inhabitedIsType independent_pairEquality axiomEquality isect_memberEquality_alt isectIsTypeImplies hyp_replacement imageElimination instantiate universeEquality imageMemberEquality baseClosed inlFormation_alt inrFormation_alt callbyvalueReduce intEquality productIsType equalityIstype addEquality multiplyEquality functionIsType promote_hyp cumulativity equalityElimination sqequalIntensionalEquality isect_memberFormation dependent_set_memberEquality lambdaFormation isect_memberEquality voidEquality dependent_pairFormation minusEquality

Latex: