Nuprl Lemma : int-to-ring_wf

[r:Rng]. ∀[n:ℤ].  (int-to-ring(r;n) ∈ |r|)


Proof




Definitions occuring in Statement :  int-to-ring: int-to-ring(r;n) rng: Rng rng_car: |r| uall: [x:A]. B[x] member: t ∈ T int:
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T int-to-ring: int-to-ring(r;n) all: x:A. B[x] implies:  Q bool: 𝔹 unit: Unit it: btrue: tt subtype_rel: A ⊆B uiff: uiff(P;Q) and: P ∧ Q uimplies: supposing a ifthenelse: if then else fi  rng: Rng nat: decidable: Dec(P) or: P ∨ Q satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] false: False not: ¬A top: Top prop: bfalse: ff guard: {T}
Lemmas referenced :  lt_int_wf bool_wf uiff_transitivity equal-wf-base int_subtype_base assert_wf less_than_wf eqtt_to_assert assert_of_lt_int rng_minus_wf rng_nat_op_wf decidable__le satisfiable-full-omega-tt intformand_wf intformnot_wf intformle_wf itermConstant_wf itermMinus_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_minus_lemma int_term_value_var_lemma int_formula_prop_less_lemma int_formula_prop_wf le_wf rng_one_wf le_int_wf bnot_wf eqff_to_assert assert_functionality_wrt_uiff bnot_of_lt_int assert_of_le_int equal_wf rng_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality natural_numberEquality hypothesis lambdaFormation unionElimination equalityElimination baseApply closedConclusion baseClosed applyEquality independent_functionElimination because_Cache productElimination independent_isectElimination setElimination rename dependent_set_memberEquality dependent_functionElimination minusEquality dependent_pairFormation lambdaEquality int_eqEquality intEquality isect_memberEquality voidElimination voidEquality independent_pairFormation computeAll equalityTransitivity equalitySymmetry axiomEquality

Latex:
\mforall{}[r:Rng].  \mforall{}[n:\mBbbZ{}].    (int-to-ring(r;n)  \mmember{}  |r|)



Date html generated: 2017_10_01-AM-08_18_55
Last ObjectModification: 2017_02_28-PM-02_03_43

Theory : rings_1


Home Index