Nuprl Lemma : quadratic1-one
∀[a,b,c:ℝ]. (quadratic1(a;b;c) = r1) supposing ((c ≤ a) and (b = -(a + c)) and (r0 < a))
Proof
Definitions occuring in Statement :
quadratic1: quadratic1(a;b;c),
rleq: x ≤ y,
rless: x < y,
req: x = y,
rminus: -(x),
radd: a + b,
int-to-real: r(n),
real: ℝ,
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
natural_number: $n
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
uimplies: b supposing a,
member: t ∈ T,
sq_stable: SqStable(P),
implies: P ⇒ Q,
squash: ↓T,
rneq: x ≠ y,
or: P ∨ Q,
prop: ℙ,
all: ∀x:A. B[x],
iff: P ⇐⇒ Q,
and: P ∧ Q,
rev_implies: P ⇐ Q,
less_than: a < b,
less_than': less_than'(a;b),
true: True,
quadratic1: quadratic1(a;b;c),
subtype_rel: A ⊆r B,
uiff: uiff(P;Q),
rev_uimplies: rev_uimplies(P;Q),
req_int_terms: t1 ≡ t2,
false: False,
not: ¬A,
top: Top,
guard: {T},
rdiv: (x/y)
Latex:
\mforall{}[a,b,c:\mBbbR{}]. (quadratic1(a;b;c) = r1) supposing ((c \mleq{} a) and (b = -(a + c)) and (r0 < a))
Date html generated:
2020_05_20-PM-00_33_46
Last ObjectModification:
2019_11_11-PM-00_18_28
Theory : reals
Home
Index