metamath/valid/mathd-algebra-89.mm

$(
  @{
    mathd-algebra-89.0 @e |- ( ph -> B e. RR* ) $@
    @( (Contributed by Kunhao Zheng, 4-May-2021.) @)
    mathd-algebra-89 @p |- ( ph -> ( ( ( 7 x. ( B ^ 3 ) ) ^ 2 ) x. ( ( 4 x. ( B ^ 2 ) ) ^ -u 3 ) ) = ( ; 4 9 / ; 6 4 ) ) @=
      ? @.
  @}
$)