metamath/valid/mathd-algebra-28.mm

$(
  @{
    mathd-algebra-28.0 @e |- ( ph -> C e. RR ) $@
    mathd-algebra-28.1 @e |- F = ( x e. RR |-> ( ( ( 2 x. ( x ^ 2 ) ) + ( 5 x. x ) ) + C ) ) $@
    mathd-algebra-28.2 @e |- ( ph -> E. x e. RR ( F ` x ) <_ 0 ) $@
    @( (Contributed by Kunhao Zheng, 4-May-2021.) @)
    mathd-algebra-28 @p |- ( ph -> C <_ ( ; 2 5 / 8 ) ) @=
      ? @.
  @}
$)