metamath/valid/amc12b-2002-p6.mm

$(
  @{
    amc12b-2002-p6.0 @e |- ( ph -> A e. RR ) $@
    amc12b-2002-p6.1 @e |- ( ph -> A =/= 0 ) $@
    amc12b-2002-p6.2 @e |- ( ph -> B e. RR ) $@
    amc12b-2002-p6.3 @e |- ( ph -> B =/= 0 ) $@
    amc12b-2002-p6.4 @e |- ( ph -> A. x e. RR ( ( ( x ^ 2 ) + ( A x. x ) ) + B ) = ( ( x - A ) x. ( x - B ) ) ) $@
    @( (Contributed by Kunhao Zheng, 4-May-2021.) @)
    amc12b-2002-p6 @p |- ( ph -> ( A = 1 /\ B = -u 2 ) ) @=
      ? @.
  @}
$)