metamath/valid/algebra-amgm-prod1toneq1-sum1tongeqn.mm

$(
  @{
    algebra-amgm-prod1toneq1-sum1tongeqn.0 @e |- ( ph -> A : NN --> RR+ ) $@
    algebra-amgm-prod1toneq1-sum1tongeqn.1 @e |- ( ph -> N e. NN ) $@
    algebra-amgm-prod1toneq1-sum1tongeqn.2 @e |- ( ph -> prod_ k e. ( 1 ... N ) ( A ` k ) = 1 ) $@
    @( (Contributed by Kunhao Zheng, 4-May-2021.) @)
    algebra-amgm-prod1toneq1-sum1tongeqn @p |- ( ph -> sum_ k e. ( 1 ... N ) ( A ` k ) >_ N ) @=
      ? @.
  @}
$)