metamath/valid/mathd-numbertheory-37.mm

$(
  @{
    @( (Contributed by Kunhao Zheng, 4-May-2021.) @)
    mathd-numbertheory-37 @p |- ( ph -> ( ; ; ; 9 9 9 9 lcm ; ; ; ; ; 1 0 0 0 0 1 ) = ; ; ; ; ; ; ; 9 0 9 0 0 9 0 9 ) @=
      ? @.
  @}
$)