metamath/valid/algebra-amgm-faxinrrp2msqrt2geq2mxm1div2x.mm

$(
  @{
    @( (Contributed by Kunhao Zheng, 4-May-2021.) @)
    algebra-amgm-faxinrrp2msqrt2geq2mxm1div2x @p |- ( ph -> A. x e. RR+ ( 2 - ( sqrt ` 2 ) ) >_ ( ( 2 - x ) - ( 1 / ( 2 x. x ) ) ) ) @=
      ? @.
  @}
$)