metamath/valid/mathd-algebra-55.mm

$(
  @{
    mathd-algebra-55.0 @e |- ( ph -> Q = ( ( ( ( ( ( 2 - 4 ) + 6 ) - 8 ) + ; 1 0 ) - ; 1 2 ) + ; 1 4 ) ) $@
    mathd-algebra-55.1 @e |- ( ph -> P = ( ( ( ( ( ( 3 - 6 ) + 9 ) - ; 1 2 ) + ; 1 5 ) - ; 1 8 ) + ; 2 1 ) ) $@
    @( (Contributed by Kunhao Zheng, 4-May-2021.) @)
    mathd-algebra-55 @p |- ( ph -> ( Q / P ) = ( 2 / 3 ) ) @=
      ? @.
  @}
$)