metamath/valid/mathd-numbertheory-211.mm

$(
  @{
    mathd-numbertheory-211.0 @e |- D = { n e. NN | ( n < ; 6 0 /\ 6 || ( ( 4 x. n ) - 2 ) ) } $@
    @( (Contributed by Kunhao Zheng, 4-May-2021.) @)
    mathd-numbertheory-211 @p |- ( ph -> ( # ` D ) = ; 2 0 ) @=
      ? @.
  @}
$)