metamath/valid/aime-1984-p15.mm

$(
  @{
    aime-1984-p15.0 @e |- ( ph -> X e. RR ) $@
    aime-1984-p15.1 @e |- ( ph -> Y e. RR ) $@
    aime-1984-p15.2 @e |- ( ph -> Z e. RR ) $@
    aime-1984-p15.3 @e |- ( ph -> W e. RR ) $@
    aime-1984-p15.4 @e |- ( ph -> ( ( ( ( X ^ 2 ) / ( ( 2 ^ 2 ) - 1 ) ) + ( ( Y ^ 2 ) / ( ( 2 ^ 2 ) - ( 3 ^ 2 ) ) ) ) + ( ( ( Z ^ 2 ) / ( ( 2 ^ 2 ) - ( 5 ^ 2 ) ) ) + ( ( W ^ 2 ) / ( ( 2 ^ 2 ) - ( 7 ^ 2 ) ) ) ) ) = 1 ) $@
    aime-1984-p15.5 @e |- ( ph -> ( ( ( ( X ^ 2 ) / ( ( 4 ^ 2 ) - 1 ) ) + ( ( Y ^ 2 ) / ( ( 4 ^ 2 ) - ( 3 ^ 2 ) ) ) ) + ( ( ( Z ^ 2 ) / ( ( 4 ^ 2 ) - ( 5 ^ 2 ) ) ) + ( ( W ^ 2 ) / ( ( 4 ^ 2 ) - ( 7 ^ 2 ) ) ) ) ) = 1 ) $@
    aime-1984-p15.6 @e |- ( ph -> ( ( ( ( X ^ 2 ) / ( ( 6 ^ 2 ) - 1 ) ) + ( ( Y ^ 2 ) / ( ( 6 ^ 2 ) - ( 3 ^ 2 ) ) ) ) + ( ( ( Z ^ 2 ) / ( ( 6 ^ 2 ) - ( 5 ^ 2 ) ) ) + ( ( W ^ 2 ) / ( ( 6 ^ 2 ) - ( 7 ^ 2 ) ) ) ) ) = 1 ) $@
    aime-1984-p15.7 @e |- ( ph -> ( ( ( ( X ^ 2 ) / ( ( 8 ^ 2 ) - 1 ) ) + ( ( Y ^ 2 ) / ( ( 8 ^ 2 ) - ( 3 ^ 2 ) ) ) ) + ( ( ( Z ^ 2 ) / ( ( 8 ^ 2 ) - ( 5 ^ 2 ) ) ) + ( ( W ^ 2 ) / ( ( 8 ^ 2 ) - ( 7 ^ 2 ) ) ) ) ) = 1 ) $@
    @( (Contributed by Kunhao Zheng, 4-May-2021.) @)
    aime-1984-p15 @p |- ( ph -> ( ( ( X ^ 2 ) + ( Y ^ 2 ) ) + ( ( Z ^ 2 ) + ( W ^ 2 ) ) ) = ; 3 6 ) @=
      ? @.
  @}
$)