metamath/valid/imo-1984-p2.mm

$(
  @{
    imo-1984-p2.0 @e |- ( ph -> A e. NN ) $@
    imo-1984-p2.1 @e |- ( ph -> B e. NN ) $@
    imo-1984-p2.2 @e |- ( ph -> -. 7 || A ) $@
    imo-1984-p2.3 @e |- ( ph -> -. 7 || B ) $@
    imo-1984-p2.4 @e |- ( ph -> -. 7 || ( A + B ) ) $@
    imo-1984-p2.5 @e |- ( ph -> ( 7 ^ 7 ) || ( ( ( ( A + B ) ^ 7 ) - ( A ^ 7 ) ) - ( B ^ 7 ) ) ) $@
    @( (Contributed by Kunhao Zheng, 9-Aug-2021.) @)
    imo-1984-p2 @p |- ( ph -> ; 1 9 <_ ( A + B ) ) @=
      ? @.
  @}
$)