metamath/valid/algebra-2complexrootspoly-xsqp49eqxp7itxpn7i.mm

${
  algebra-2complexrootspoly-xsqp49eqxp7itxpn7i.0 $e |- ( ph -> X e. CC ) $.
  $( (Contributed by Stanislas Polu, 8-Oct-2020.) $)
  algebra-2complexrootspoly-xsqp49eqxp7itxpn7i $p |- ( ph -> ( ( X ^ 2 ) + ; 4 
9 ) = ( ( X + ( 7 x. _i ) ) x. ( X + ( -u 7 x. _i ) ) ) ) $=
( co c4 caddc c7 cneg ci cmul cc0 eqcomd 7cn a1i ax-icn mulcld oveq2d eqtrd 
oveq12d eqtri c2 cexp c9 cdc sqcld addid1d sqvald cc mulneg1d negidd eqtr2d 
wcel negcld addcomd addassd eqtr4d oveq1d wceq negcli mul4i mulneg2i 7t7e49 
mulcomd negeqi oveq1i c1 ixi oveq2i 4nn0 9nn0 deccl nn0cni ax-1cn mul2negib 
mulid1i eqcomi addcld adddid adddird ) ABUAUBDZEUCUDZFDZBBGHZIJDZFDZJDZGIJD 
ZWEJDZFDZBWGFDWEJDZAWBBBJDZBWDJDZFDZWGBJDZWGWDJDZFDZFDZWIAWBWMWNFDZWOFDWQAV 
TWRWAWOFAVTWKWGHZBJDZFDZWNFDZWRAVTVTKFDZXBAXCVTAVTABCUEUFLAXCWKWTWNFDZFDZXB 
AVTWKKXDFABCUGAKWNWTFDZXDAXFWNWNHZFDKAWTXGWNFAWGBAGIGUHULAMNZIUHULAONZPZCUI 
QAWNAWGBXJCPZUJUKAWNWTXKAWSBAWGXJUMZCPZUNRSAXBXEAWKWTWNABBCCPZXMXKUOLRRAXAW 
MWNFAWTWLWKFAWTBWSJDWLAWSBXLCVCAWDWSBJAGIXHXIUIQUPQUQRWAWOURAWOWAWOGWCJDZII 
JDZJDZWAGIWCIMOGMUSOUTXQWAHZXPJDZWAXOXRXPJXOGGJDZHXRGGMMVAXTWAVBVDTVEXSXRVF 
HZJDWAXPYAXRJVGVHWAVFWAWAEUCVIVJVKVLZVMYBWAYBVOVNTTTVPNSAWMWNWOAWKWLXNABWDC 
AWCIAGXHUMXIPZPVQXKAWGWDXJYCPUORAWMWFWPWHFAWFWMABBWDCCYCVRLAWHWPAWGBWDXJCYC 
VRLSRAWJWIABWGWECXJABWDCYCVQVSLR $. 
$}