metamath/valid/mathd-algebra-140.mm

$(
  @{
    mathd-algebra-140.0 @e |- ( ph -> A e. RR+ ) $@
    mathd-algebra-140.1 @e |- ( ph -> B e. RR+ ) $@
    mathd-algebra-140.2 @e |- ( ph -> C e. RR+ ) $@
    mathd-algebra-140.3 @e |- ( ph -> X e. RR ) $@
    mathd-algebra-140.4 @e |- ( ph -> ( ( ( ; 2 4 x. ( X ^ 2 ) ) - ( ; 1 9 x. X ) ) - ; 3 5 ) = ( ( ( A x. X ) - 5 ) x. ( ( 2 x. ( B x. X ) ) + C ) ) ) $@
    @( (Contributed by Kunhao Zheng, 4-May-2021.) @)
    mathd-algebra-140 @p |- ( ph -> ( ( A x. B ) - ( 3 x. C ) ) = -u 9 ) @=
      ? @.
  @}
$)