metamath/valid/mathd-numbertheory-200.mm (
7
lines of code) (
raw
):
$( @{ @( (Contributed by Kunhao Zheng, 4-May-2021.) @) mathd-numbertheory-200 @p |- ( ph -> ( ; ; 1 3 9 mod ; 1 1 ) = 7 ) @= ? @. @} $)