metamath/valid/imo-1974-p5.mm

$(
  @{
    imo-1974-p5.0 @e |- ( ph -> A e. RR ) $@
    imo-1974-p5.1 @e |- ( ph -> B e. RR ) $@
    imo-1974-p5.2 @e |- ( ph -> C e. RR ) $@
    imo-1974-p5.3 @e |- ( ph -> D e. RR ) $@
    imo-1974-p5.4 @e |- ( ph -> S e. RR ) $@
    imo-1974-p5.5 @e |- ( ph -> S = ( ( ( ( A / ( ( A + B ) + D ) ) + ( B / ( ( A + B ) + C ) ) ) + ( C / ( ( B + C ) + D ) ) ) + ( D / ( ( A + C ) + D ) ) ) ) $@
    @( (Contributed by Kunhao Zheng, 9-Aug-2021.) @)
    imo-1974-p5 @p |- ( ph -> ( 1 < S /\ S < 2 ) ) @=
      ? @.
  @}
$)