metamath/valid/algebra-amgm-sumasqdivbsqgeqsumbdiva.mm

$(
  @{
    algebra-amgm-sumasqdivbsqgeqsumbdiva.0 @e |- ( ph -> A e. RR+ ) $@
    algebra-amgm-sumasqdivbsqgeqsumbdiva.1 @e |- ( ph -> B e. RR+ ) $@
    algebra-amgm-sumasqdivbsqgeqsumbdiva.2 @e |- ( ph -> C e. RR+ ) $@
    @( (Contributed by Kunhao Zheng, 4-May-2021.) @)
    algebra-amgm-sumasqdivbsqgeqsumbdiva @p |- ( ph -> ( ( ( ( A ^ 2 ) / ( B ^ 2 ) ) + ( ( B ^ 2 ) / ( C ^ 2 ) ) ) + ( ( C ^ 2 ) / ( A ^ 2 ) ) ) >_ ( ( ( B / A ) + ( C / B ) ) + ( A / C ) ) ) @=
      ? @.
  @}
$)