Step
*
of Lemma
quadratic2_functionality
No Annotations
∀[a,b,c,a',b',c':ℝ].
(quadratic2(a;b;c) = quadratic2(a';b';c')) supposing
((c = c') and
(b = b') and
(a = a') and
(r0 ≤ ((b * b) - r(4) * a * c)) and
a ≠ r0)
BY
{ (Intros
THEN Unfold `quadratic2` 0
THEN BLemma `rdiv_functionality`
THEN Try (BLemma `rsub_functionality`)
THEN Try (Complete ((Auto THEN MemTypeCD THEN Auto THEN RWO "-1< -2< -3<" 0 THEN Auto)))
THEN RWO "-1 -2 -3" 0
THEN Auto
THEN MemTypeCD
THEN Auto
THEN RWO "-1< -2< -3<" 0
THEN Auto) }
Latex:
Latex:
No Annotations
\mforall{}[a,b,c,a',b',c':\mBbbR{}].
(quadratic2(a;b;c) = quadratic2(a';b';c')) supposing
((c = c') and
(b = b') and
(a = a') and
(r0 \mleq{} ((b * b) - r(4) * a * c)) and
a \mneq{} r0)
By
Latex:
(Intros
THEN Unfold `quadratic2` 0
THEN BLemma `rdiv\_functionality`
THEN Try (BLemma `rsub\_functionality`)
THEN Try (Complete ((Auto THEN MemTypeCD THEN Auto THEN RWO "-1< -2< -3<" 0 THEN Auto)))
THEN RWO "-1 -2 -3" 0
THEN Auto
THEN MemTypeCD
THEN Auto
THEN RWO "-1< -2< -3<" 0
THEN Auto)
Home
Index