metamath/valid/aimeI-2000-p7.mm

$(
  @{
    aimeI-2000-p7.0 @e |- ( ph -> X e. RR+ ) $@
    aimeI-2000-p7.1 @e |- ( ph -> Y e. RR+ ) $@
    aimeI-2000-p7.2 @e |- ( ph -> Z e. RR+ ) $@
    aimeI-2000-p7.3 @e |- ( ph -> M e. QQ ) $@
    aimeI-2000-p7.4 @e |- ( ph -> ( ( X x. Y ) x. Z ) = 1 ) $@
    aimeI-2000-p7.5 @e |- ( ph -> ( X + ( 1 / Z ) ) = 5 ) $@
    aimeI-2000-p7.6 @e |- ( ph -> ( Y + ( 1 / X ) ) = ; 2 9 ) $@
    aimeI-2000-p7.7 @e |- ( ph -> ( Z + ( 1 / Y ) ) = M ) $@
    aimeI-2000-p7.8 @e |- ( ph -> 0 < M ) $@
    @( (Contributed by Kunhao Zheng, 9-Aug-2021.) @)
    aimeI-2000-p7 @p |- ( ph -> ( ( denom ` M ) + ( numer ` M ) ) = 5 ) @=
      ? @.
  @}
$)