metamath/valid/mathd-algebra-116.mm

$(
  @{
    mathd-algebra-116.0 @e |- ( ph -> K e. RR ) $@
    mathd-algebra-116.1 @e |- ( ph -> X = ( ( ; 1 3 - ( sqrt ` ; ; 1 3 1 ) ) / 4 ) ) $@
    mathd-algebra-116.2 @e |- ( ph -> ( ( ( 2 x. ( X ^ 2 ) ) - ( ; 1 3 x. X ) ) + K ) = 0 ) $@
    @( (Contributed by Kunhao Zheng, 4-May-2021.) @)
    mathd-algebra-116 @p |- ( ph -> K = ( ; 1 9 / 4 ) ) @=
      ? @.
  @}
$)