metamath/valid/algebra-2rootsintpoly-am10tap11eqasqpam110.mm

${
  algebra-2rootsintpoly-am10tap11eqasqpam110.0 $e |- ( ph -> A e. CC ) $.
  $( (Contributed by Stanislas Polu, 8-Oct-2020.) $)
  algebra-2rootsintpoly-am10tap11eqasqpam110 $p |- ( ph -> ( ( A - ; 1 0 ) x. ( 
A + ; 1 1 ) ) = ( ( ( A ^ 2 ) + A ) - ; ; 1 1 0 ) ) $=
( c1 cc0 cdc cmin co caddc cmul cc wcel a1i 1nn0 oveq12d eqcomd wceq oveq2d 
0nn0 eqtrd c2 cexp 1nn decnncl2 nncni decnncl addcld subdird adddid mulcomd 
sqvald deccl ax-frege54c dec0h mulid2i mul02i addid1i decm1mma sqcld mulcld 
nn0cni subsub4d addsubassd mulid1 syl ax-1cn decsuc subaddrii eqcomi subdid 
0p1e1 eqtr4d oveq1d ) ABDEFZGHBDDFZIHZJHBVPJHZVNVPJHZGHZBUAUBHZBIHZVOEFZGHZ 
ABVNVPCVNKLAVNDUCUDUEZMZABVOCVOKLAVODDNUCUFUEZMZUGUHAVSBBJHZBVOJHZIHZVNBJHZ 
VNVOJHZIHZGHZWCAVQWJVRWMGABBVOCCWGUIAVNBVOWECWGUIOAWNVTVOBJHZIHZWKWBIHZGHZW 
CAWJWPWMWQGAWHVTWIWOIAVTWHABCUKPABVOCWGUJZOAWLWBWKIWLWBQAVNVOVOEDEVOEEDDNNU 
LZSNSSVNUMZESUNVOWFUOVOWFUPVOWFUQURMROAWRWPWKGHZWBGHZWCAXCWRAWPWKWBAVTWOABC 
USZAVOBWGCUTZUGAVNBWECUTZWBKLAWBVOEWTSULVAMVBPAXBWAWBGAXBVTWOWKGHZIHWAAVTWO 
WKXDXEXFVCABXGVTIABWIBVNJHZGHZXGABBVOVNGHZJHZXIABBDJHZXKAXLBABKLXLBQCBVDVEP 
ADXJBJDXJQAXJDVOVNDWFWDVFDEDVNNSVKXAVGVHVIMRTABVOVNCWGWEVJTAWIWOXHWKGWSABVN 
CWEUJOTRVLVMTTTT $. 
$}