$(
  @{
    imo-1977-p5.0 @e |- ( ph -> A e. NN0 ) $@
    imo-1977-p5.1 @e |- ( ph -> B e. NN0 ) $@
    imo-1977-p5.2 @e |- ( ph -> Q e. NN0 ) $@
    imo-1977-p5.3 @e |- ( ph -> R e. NN0 ) $@
    imo-1977-p5.4 @e |- ( ph -> R < ( A + B ) ) $@
    imo-1977-p5.5 @e |- ( ph -> ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( ( ( A + B ) x. Q ) + R ) ) $@
    imo-1977-p5.6 @e |- ( ph -> ( ( Q ^ 2 ) + R ) = ; ; ; 1 9 7 7 ) $@
    @( (Contributed by Kunhao Zheng, 9-Aug-2021.) @)
    imo-1977-p5 @p |- ( ph -> ( ( ( abs ` ( A - ; 2 2 ) ) = ; 1 5 /\ ( abs ` ( B - ; 2 2 ) ) = ; 2 8 ) \/ ( ( abs ` ( A - ; 2 2 ) ) = ; 2 8 /\ ( abs ` ( B - ; 2 2 ) ) = ; 1 5 ) ) ) @=
      ? @.
  @}
$)