metamath/valid/amc12a-2003-p25.mm

$(
  @{
    amc12a-2003-p25.0 @e |- ( ph -> A e. RR ) $@
    amc12a-2003-p25.1 @e |- ( ph -> B e. RR ) $@
    amc12a-2003-p25.2 @e |- ( ph -> 0 < B ) $@
    amc12a-2003-p25.3 @e |- ( ph -> A. x e. RR ( F ` x ) = ( sqrt ` ( ( A x. ( x ^ 2 ) ) + ( B x. x ) ) ) ) $@
    amc12a-2003-p25.4 @e |- D = { x e. RR | 0 <_ ( F ` x ) } $@
    @( (Contributed by Kunhao Zheng, 4-May-2021.) @)
    amc12a-2003-p25 @p |- ( ph -> ( D = ( F " D ) -> ( A = 0 \/ A = -u 4 ) ) ) @=
      ? @.
  @}
$)