Nuprl Lemma : quadratic2_wf

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


Proof




Definitions occuring in Statement :  quadratic2: quadratic2(a;b;c) rneq: x ≠ y rleq: x ≤ y rsub: y rmul: b int-to-real: r(n) real: uimplies: supposing a uall: [x:A]. B[x] member: t ∈ T natural_number: $n
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a quadratic2: quadratic2(a;b;c) subtype_rel: A ⊆B all: x:A. B[x] so_lambda: λ2x.t[x] rneq: x ≠ y guard: {T} or: P ∨ Q iff: ⇐⇒ Q and: P ∧ Q rev_implies:  Q implies:  Q less_than: a < b squash: T less_than': less_than'(a;b) true: True prop: so_apply: x[s] false: False not: ¬A rat_term_to_real: rat_term_to_real(f;t) rtermVar: rtermVar(var) rat_term_ind: rat_term_ind pi1: fst(t) rtermDivide: num "/" denom rtermMultiply: left "*" right rtermConstant: "const" pi2: snd(t) stable: Stable{P} uiff: uiff(P;Q) rev_uimplies: rev_uimplies(P;Q) int_nzero: -o nequal: a ≠ b ∈  sq_type: SQType(T) decidable: Dec(P) satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x]

Latex:
\mforall{}[a,b,c:\mBbbR{}].    (quadratic2(a;b;c)  \mmember{}  \mBbbR{})  supposing  ((r0  \mleq{}  ((b  *  b)  -  r(4)  *  a  *  c))  and  a  \mneq{}  r0)



Date html generated: 2020_05_20-PM-00_34_10
Last ObjectModification: 2020_01_06-PM-00_08_44

Theory : reals


Home Index