metamath/valid/mathd-algebra-131.mm

$(
  @{
    mathd-algebra-131.0 @e |- ( ph -> A e. RR ) $@
    mathd-algebra-131.1 @e |- ( ph -> B e. RR ) $@
    mathd-algebra-131.2 @e |- F = ( x e. RR |-> ( ( ( 2 x. ( x ^ 2 ) ) - ( 7 x. x ) ) + 2 ) ) $@
    mathd-algebra-131.3 @e |- ( ph -> ( F ` A ) = 0 ) $@
    mathd-algebra-131.4 @e |- ( ph -> ( F ` B ) = 0 ) $@
    mathd-algebra-131.5 @e |- ( ph -> A =/= B ) $@
    @( (Contributed by Kunhao Zheng, 4-May-2021.) @)
    mathd-algebra-131 @p |- ( ph -> ( ( 1 / ( A - 1 ) ) + ( 1 / ( B - 1 ) ) ) = -u 1 ) @=
      ? @.
  @}
$)