Nuprl Lemma : quadratic-formula-simple
∀a,b,c:ℝ.
((r0 < a)
⇒ (c < r0)
⇒ (∀x:ℝ. (((x = quadratic1(a;b;c)) ∨ (x = quadratic2(a;b;c))) ⇒ (((a * x^2) + (b * x) + c) = r0))))
Proof
Definitions occuring in Statement :
quadratic2: quadratic2(a;b;c),
quadratic1: quadratic1(a;b;c),
rless: x < y,
rnexp: x^k1,
req: x = y,
rmul: a * b,
radd: a + b,
int-to-real: r(n),
real: ℝ,
all: ∀x:A. B[x],
implies: P ⇒ Q,
or: P ∨ Q,
natural_number: $n
Definitions unfolded in proof :
all: ∀x:A. B[x],
member: t ∈ T,
implies: P ⇒ Q,
rneq: x ≠ y,
or: P ∨ Q,
uall: ∀[x:A]. B[x],
prop: ℙ,
iff: P ⇐⇒ Q,
and: P ∧ Q,
rev_implies: P ⇐ Q,
less_than: a < b,
squash: ↓T,
less_than': less_than'(a;b),
true: True,
uimplies: b supposing a,
uiff: uiff(P;Q),
req_int_terms: t1 ≡ t2,
top: Top,
false: False,
not: ¬A,
rev_uimplies: rev_uimplies(P;Q),
rge: x ≥ y,
guard: {T}
Latex:
\mforall{}a,b,c:\mBbbR{}.
((r0 < a)
{}\mRightarrow{} (c < r0)
{}\mRightarrow{} (\mforall{}x:\mBbbR{}
(((x = quadratic1(a;b;c)) \mvee{} (x = quadratic2(a;b;c))) {}\mRightarrow{} (((a * x\^{}2) + (b * x) + c) = r0))))
Date html generated:
2020_05_20-PM-00_35_23
Last ObjectModification:
2019_11_11-AM-11_02_47
Theory : reals
Home
Index