metamath/valid/mathd-algebra-10.mm

$(
  @{
    @( (Contributed by Kunhao Zheng, 4-May-2021.) @)
    mathd-algebra-10 @p |- ( ph -> ( abs ` ( ( ( ; ; 1 2 0 / ; ; 1 0 0 ) x. ; 3 0 ) - ( ( ; ; 1 3 0 / ; ; 1 0 0 ) x. ; 2 0 ) ) ) = ; 1 0 ) @=
      ? @.
  @}
$)