metamath/valid/imo-1990-p3.mm

$(
  @{
    imo-1990-p3.0 @e |- ( ph -> N e. ( ZZ>= ` 2 ) ) $@
    imo-1990-p3.1 @e |- ( ph -> ( ( ( 2 ^ N ) + 1 ) / ( N ^ 2 ) ) e. ZZ ) $@
    @( (Contributed by Kunhao Zheng, 4-May-2021.) @)
    imo-1990-p3 @p |- ( ph -> N = 3 ) @=
      ? @.
  @}
$)