metamath/valid/mathd-numbertheory-84.mm

$(
  @{
    @( (Contributed by Kunhao Zheng, 4-May-2021.) @)
    mathd-numbertheory-84 @p |- ( ph -> ( |_ ` ( ( 9 / ; ; 1 6 0 ) x. ; ; 1 0 0 ) ) = 5 ) @=
      ? @.
  @}
$)