metamath/valid/mathd-numbertheory-109.mm

$(
  @{
    mathd-numbertheory-109.0 @e |- V = ( n e. NN |-> ( ( 2 x. n ) - 1 ) ) $@
    @( (Contributed by Kunhao Zheng, 4-May-2021.) @)
    mathd-numbertheory-109 @p |- ( ph -> ( sum_ k e. ( 1 ... ; ; 1 0 0 ) ( V ` k ) mod 7 ) = 4 ) @=
      ? @.
  @}
$)