metamath/valid/mathd-algebra-13.mm

$(
  @{
    mathd-algebra-13.0 @e |- ( ph -> A e. RR ) $@
    mathd-algebra-13.1 @e |- ( ph -> B e. RR ) $@
    mathd-algebra-13.2 @e |- ( ph -> A. x e. RR ( ( 4 x. x ) / ( ( ( x ^ 2 ) - ( 8 x. x ) ) + ; 1 5 ) ) = ( ( A / ( x - 3 ) ) + ( B / ( x - 5 ) ) ) ) $@
    @( (Contributed by Kunhao Zheng, 4-May-2021.) @)
    mathd-algebra-13 @p |- ( ph -> ( A = -u 6 /\ B = ; 1 0 ) ) @=
      ? @.
  @}
$)