metamath/valid/mathd-numbertheory-30.mm

$(
  @{
    @( (Contributed by Kunhao Zheng, 4-May-2021.) @)
    mathd-numbertheory-30 @p |- ( ph -> ( ( ( ( ( ( ; ; ; ; 3 3 8 1 8 ^ 2 ) + ( ; ; ; ; 3 3 8 1 9 ^ 2 ) ) + ( ; ; ; ; 3 3 8 2 0 ^ 2 ) ) + ( ; ; ; ; 3 3 8 2 1 ^ 2 ) ) + ( ; ; ; ; 3 3 8 2 2 ^ 2 ) ) mod ; 1 7 ) = 0 ) @=
      ? @.
  @}
$)