### Nuprl Lemma : int-to-ring-minus-one

`∀[r:Rng]. (int-to-ring(r;-1) = (-r 1) ∈ |r|)`

Proof

Definitions occuring in Statement :  int-to-ring: `int-to-ring(r;n)` rng: `Rng` rng_one: `1` rng_minus: `-r` rng_car: `|r|` uall: `∀[x:A]. B[x]` apply: `f a` minus: `-n` natural_number: `\$n` equal: `s = t ∈ T`
Definitions unfolded in proof :  int-to-ring: `int-to-ring(r;n)` lt_int: `i <z j` ifthenelse: `if b then t else f fi ` btrue: `tt` rng_nat_op: `n ⋅r e` mon_nat_op: `n ⋅ e` add_grp_of_rng: `r↓+gp` grp_op: `*` pi2: `snd(t)` pi1: `fst(t)` grp_id: `e` nat_op: `n x(op;id) e` itop: `Π(op,id) lb ≤ i < ub. E[i]` ycomb: `Y` subtract: `n - m` uall: `∀[x:A]. B[x]` bfalse: `ff` member: `t ∈ T` squash: `↓T` rng: `Rng` true: `True` subtype_rel: `A ⊆r B` uimplies: `b supposing a` guard: `{T}` iff: `P `⇐⇒` Q` and: `P ∧ Q` rev_implies: `P `` Q` implies: `P `` Q` infix_ap: `x f y`
Lemmas referenced :  equal_wf rng_car_wf rng_minus_over_plus rng_zero_wf rng_one_wf rng_minus_wf iff_weakening_equal rng_plus_wf rng_minus_zero rng_plus_zero rng_wf
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep isect_memberFormation_alt cut applyEquality thin lambdaEquality_alt sqequalHypSubstitution imageElimination introduction extract_by_obid isectElimination because_Cache hypothesis setElimination rename hypothesisEquality natural_numberEquality imageMemberEquality baseClosed equalityTransitivity equalitySymmetry independent_isectElimination productElimination independent_functionElimination universeIsType

Latex:
\mforall{}[r:Rng].  (int-to-ring(r;-1)  =  (-r  1))

Date html generated: 2020_05_19-PM-10_07_58
Last ObjectModification: 2020_01_08-PM-06_00_23

Theory : rings_1

Home Index