metamath/valid/amc12a-2013-p8.mm

$(
  @{
    amc12a-2013-p8.0 @e |- ( ph -> X e. RR ) $@
    amc12a-2013-p8.1 @e |- ( ph -> Y e. RR ) $@
    amc12a-2013-p8.2 @e |- ( ph -> X =/= 0 ) $@
    amc12a-2013-p8.3 @e |- ( ph -> Y =/= 0 ) $@
    amc12a-2013-p8.4 @e |- ( ph -> X =/= Y ) $@
    amc12a-2013-p8.5 @e |- ( ph -> ( X + ( 2 / X ) ) = ( Y + ( 2 / Y ) ) ) $@
    @( (Contributed by Kunhao Zheng, 9-Aug-2021.) @)
    amc12a-2013-p8 @p |- ( ph -> ( X x. Y ) = 2 ) @=
      ? @.
  @}
$)