metamath/valid/numbertheory-sqmod3in01d.mm (8 lines of code) (raw):
$(
@{
numbertheory-sqmod3in01d.0 @e |- ( ph -> A e. ZZ ) $@
@( (Contributed by Kunhao Zheng, 4-May-2021.) @)
numbertheory-sqmod3in01d @p |- ( ph -> ( ( A ^ 2 ) mod 3 ) e. { 0 , 1 } ) @=
? @.
@}
$)