metamath/valid/mathd-numbertheory-35.mm

$(
  @{
    @( (Contributed by Kunhao Zheng, 4-May-2021.) @)
    mathd-numbertheory-35 @p |- ( ph -> sum_ k e. { n e. NN | n || ( sqrt ` ; ; 1 9 6 ) } k = ; 2 4 ) @=
      ? @.
  @}
$)