### Nuprl Lemma : test-ring-eq

[r:CRng]
∀v,v1,v2,v3,v4,v5,v6,v7,v8,v9:|r|.
((((((v6 v3) +r ((v2 v5) +r (v4 v7))) +r (-r ((v7 v2) +r ((v3 v4) +r (v5 v6)))))

(((v6 v9) +r ((v8 v1) +r (v v7))) +r (-r ((v7 v8) +r ((v9 v) +r (v1 v6))))))
+r
(((((v v7) +r ((v6 v5) +r (v4 v1))) +r (-r ((v1 v6) +r ((v7 v4) +r (v5 v)))))

(((v6 v9) +r ((v8 v3) +r (v2 v7))) +r (-r ((v7 v8) +r ((v9 v2) +r (v3 v6))))))
+r
((((v v3) +r ((v2 v7) +r (v6 v1))) +r (-r ((v1 v2) +r ((v3 v6) +r (v7 v)))))

(((v6 v9) +r ((v8 v5) +r (v4 v7))) +r (-r ((v7 v8) +r ((v9 v4) +r (v5 v6))))))))
0
∈ |r|)

Proof

Definitions occuring in Statement :  crng: CRng rng_times: * rng_minus: -r rng_zero: 0 rng_plus: +r rng_car: |r| uall: [x:A]. B[x] infix_ap: y all: x:A. B[x] apply: a equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T all: x:A. B[x] crng: CRng rng: Rng infix_ap: y uiff: uiff(P;Q) and: P ∧ Q uimplies: supposing a ringeq_int_terms: t1 ≡ t2 false: False implies:  Q not: ¬A top: Top
Lemmas referenced :  rng_car_wf crng_wf rng_plus_wf rng_times_wf rng_minus_wf rng_zero_wf itermAdd_wf itermMultiply_wf itermVar_wf itermMinus_wf itermConstant_wf ringeq-iff-rsub-is-0 ring_polynomial_null int-to-ring_wf istype-int ring_term_value_add_lemma istype-void ring_term_value_mul_lemma ring_term_value_var_lemma ring_term_value_minus_lemma ring_term_value_const_lemma int-to-ring-zero
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt introduction cut lambdaFormation_alt hypothesis inhabitedIsType hypothesisEquality universeIsType extract_by_obid sqequalHypSubstitution isectElimination thin setElimination rename sqequalRule lambdaEquality_alt dependent_functionElimination axiomEquality functionIsTypeImplies applyEquality because_Cache natural_numberEquality productElimination independent_isectElimination approximateComputation int_eqEquality isect_memberEquality_alt voidElimination

Latex:
\mforall{}[r:CRng]
\mforall{}v,v1,v2,v3,v4,v5,v6,v7,v8,v9:|r|.
((((((v6  *  v3)  +r  ((v2  *  v5)  +r  (v4  *  v7)))  +r  (-r  ((v7  *  v2)  +r  ((v3  *  v4)  +r  (v5  *  v6)))))
*
(((v6  *  v9)  +r  ((v8  *  v1)  +r  (v  *  v7)))  +r  (-r  ((v7  *  v8)  +r  ((v9  *  v)  +r  (v1  *  v6))))))
+r
(((((v  *  v7)  +r  ((v6  *  v5)  +r  (v4  *  v1)))  +r  (-r  ((v1  *  v6)  +r  ((v7  *  v4)  +r  (v5  *  v)))))
*
(((v6  *  v9)  +r  ((v8  *  v3)  +r  (v2  *  v7)))  +r  (-r  ((v7  *  v8)  +r  ((v9  *  v2)  +r  (v3  *  v6))))))
+r
((((v  *  v3)  +r  ((v2  *  v7)  +r  (v6  *  v1)))  +r  (-r  ((v1  *  v2)  +r  ((v3  *  v6)  +r  (v7  *  v)))))
*
(((v6  *  v9)  +r  ((v8  *  v5)  +r  (v4  *  v7)))  +r  (-r  ((v7  *  v8)  +r  ((v9  *  v4)  +r  (v5  *  v6))))))))
=  0)

Date html generated: 2019_10_15-AM-10_34_14
Last ObjectModification: 2018_10_08-PM-06_00_25

Theory : rings_1

Home Index