Nuprl Lemma : quadratic2-zero

[a,b,c:ℝ].  (quadratic2(a;b;c) r0) supposing ((b ≤ r0) and (c r0) and a ≠ r0)


Proof




Definitions occuring in Statement :  quadratic2: quadratic2(a;b;c) rneq: x ≠ y rleq: x ≤ y req: y int-to-real: r(n) real: uimplies: supposing a uall: [x:A]. B[x] natural_number: $n
Definitions unfolded in proof :  uall: [x:A]. B[x] uimplies: supposing a member: t ∈ T sq_stable: SqStable(P) implies:  Q rneq: x ≠ y or: P ∨ Q all: x:A. B[x] iff: ⇐⇒ Q and: P ∧ Q rev_implies:  Q less_than: a < b squash: T less_than': less_than'(a;b) true: True prop: quadratic2: quadratic2(a;b;c) assert: b ifthenelse: if then else fi  nonneg-poly: nonneg-poly(p) bl-all: (∀x∈L.P[x])_b reduce: reduce(f;k;as) list_ind: list_ind int_term_to_ipoly: int_term_to_ipoly(t) int_term_ind: int_term_ind itermSubtract: left (-) right add_ipoly: add_ipoly(p;q) add-ipoly-prepend: add-ipoly-prepend(p;q;l) itermMultiply: left (*) right mul_ipoly: mul_ipoly(p;q) itermVar: vvar cons: [a b] cbv_list_accum: cbv_list_accum(x,a.f[x; a];y;L) nil: [] it: mul-mono-poly: mul-mono-poly(m;p) mul-monomials: mul-monomials(m1;m2) merge-int-accum: merge-int-accum(as;bs) eager-accum: eager-accum(x,a.f[x; a];y;l) callbyvalueall: callbyvalueall evalall: evalall(t) insert-int: insert-int(x;l) minus-poly: minus-poly(p) map: map(f;as) itermConstant: "const" rev-append: rev(as) bs list_accum: list_accum band: p ∧b q nonneg-monomial: nonneg-monomial(m) le_int: i ≤j bnot: ¬bb lt_int: i <j bfalse: ff btrue: tt even-int-list: even-int-list(L) bor: p ∨bq null: null(as) tl: tl(l) pi2: snd(t) eq_int: (i =z j) hd: hd(l) pi1: fst(t) false: False not: ¬A top: Top uiff: uiff(P;Q) subtype_rel: A ⊆B rev_uimplies: rev_uimplies(P;Q) req_int_terms: t1 ≡ t2 guard: {T} rdiv: (x/y)
Lemmas referenced :  sq_stable__req quadratic2_wf rmul_preserves_rless int-to-real_wf rless-int rless_wf rmul_wf rleq_wf req_wf rneq_wf real_wf rsub_wf real-term-nonneg itermSubtract_wf itermMultiply_wf itermVar_wf itermConstant_wf istype-int real_term_value_sub_lemma istype-void real_term_value_mul_lemma real_term_value_var_lemma real_term_value_const_lemma req-iff-rsub-is-0 rdiv_wf rminus_wf rsqrt_wf square-nonneg rabs_wf rleq_functionality req_weakening rsub_functionality rmul_functionality req_functionality real_polynomial_null rless_functionality rdiv_functionality rsqrt_functionality rsqrt_square rinv_wf2 itermMinus_wf rabs-of-nonpos req_transitivity rinv-of-rmul real_term_value_minus_lemma
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality independent_isectElimination hypothesis because_Cache independent_functionElimination unionElimination inlFormation_alt dependent_functionElimination natural_numberEquality productElimination sqequalRule independent_pairFormation imageMemberEquality baseClosed universeIsType inrFormation_alt imageElimination inhabitedIsType lambdaEquality_alt int_eqEquality isect_memberEquality_alt voidElimination dependent_set_memberEquality_alt applyEquality setElimination rename equalityTransitivity equalitySymmetry closedConclusion approximateComputation

Latex:
\mforall{}[a,b,c:\mBbbR{}].    (quadratic2(a;b;c)  =  r0)  supposing  ((b  \mleq{}  r0)  and  (c  =  r0)  and  a  \mneq{}  r0)



Date html generated: 2019_10_30-AM-07_59_47
Last ObjectModification: 2019_10_10-AM-10_51_23

Theory : reals


Home Index