metamath/valid/mathd-algebra-421.mm

$(
  @{
    mathd-algebra-421.0 @e |- ( ph -> A e. RR ) $@
    mathd-algebra-421.1 @e |- ( ph -> B e. RR ) $@
    mathd-algebra-421.2 @e |- ( ph -> C e. RR ) $@
    mathd-algebra-421.3 @e |- ( ph -> D e. RR ) $@
    mathd-algebra-421.4 @e |- ( ph -> B = ( ( ( A ^ 2 ) + ( 4 x. A ) ) + 6 ) ) $@
    mathd-algebra-421.5 @e |- ( ph -> B = ( ( ( ( 1 / 2 ) x. ( A ^ 2 ) ) + A ) + 6 ) ) $@
    mathd-algebra-421.6 @e |- ( ph -> D = ( ( ( C ^ 2 ) + ( 4 x. C ) ) + 6 ) ) $@
    mathd-algebra-421.7 @e |- ( ph -> D = ( ( ( ( 1 / 2 ) x. ( C ^ 2 ) ) + C ) + 6 ) ) $@
    mathd-algebra-421.8 @e |- ( ph -> A <_ C ) $@
    @( (Contributed by Kunhao Zheng, 31-May-2021.) @)
    mathd-algebra-421 @p |- ( ph -> ( C - A ) = 6 ) @=
      ? @.
  @}
$)