metamath/valid/mathd-numbertheory-24.mm

$(
  @{
    @( (Contributed by Kunhao Zheng, 4-May-2021.) @)
    mathd-numbertheory-24 @p |- ( ph -> ( sum_ k e. ( 1 ... 9 ) ( ; 1 1 ^ k ) mod ; ; 1 0 0 ) = ; 5 9 ) @=
      ? @.
  @}
$)