metamath/valid/algebra-3rootspoly-amdtamctambeqnasqmbpctapcbtdpasqmbpctapcbta.mm

${
  algebra-3rootspoly-amdtamctambeqnasqmbpctapcbtdpasqmbpctapcbta.0 $e |- ( ph 
-> B e. CC ) $.
  algebra-3rootspoly-amdtamctambeqnasqmbpctapcbtdpasqmbpctapcbta.1 $e |- ( ph 
-> C e. CC ) $.
  algebra-3rootspoly-amdtamctambeqnasqmbpctapcbtdpasqmbpctapcbta.2 $e |- ( ph 
-> D e. CC ) $.
  algebra-3rootspoly-amdtamctambeqnasqmbpctapcbtdpasqmbpctapcbta.3 $e |- ( ph 
-> A e. CC ) $.
  $( (Contributed by Stanislas Polu, 8-Oct-2020.) $)
  algebra-3rootspoly-amdtamctambeqnasqmbpctapcbtdpasqmbpctapcbta $p |- ( ph -> 
( ( ( A - D ) x. ( A - C ) ) x. ( A - B ) ) = ( -u ( ( ( ( A ^ 2 ) - ( ( B + C 
) x. A ) ) + ( C x. B ) ) x. D ) + ( ( ( ( A ^ 2 ) - ( ( B + C ) x. A ) ) + ( C 
x. B ) ) x. A ) ) ) $=
( cmin co cmul caddc subcld mulcld mulcomd eqtrd subdird subdid oveq12d c2 cexp 
cneg mulassd subsub4d sqvald eqcomd addcld adddid eqtr2d oveq1d eqtr4d subsubd 
sqcld negsubd negcld addcomd ) ABEJKZBDJKZLKBCJKZLKZBUAUBKZCDMKZBLK 
ZJKZDCLKZMKZBLKZVGELKZJKZVIUCZVHMKZAVAVGURLKZVJAVAUSUTLKZURLKZVMAVAURVNLKVO 
AURUSUTABEIHNZABDIGNZABCIFNZUDAURVNVPAUSUTVQVROPQAVGVNURLAVNBUTLKZDUTLKZJKZ 
VGABDUTIGVRRAWABBLKZBCLKZJKZBDLKZCDLKZJKZJKZVGAVSWDVTWGJABBCIIFSAVTUTDLKWGA 
DUTGVRPABCDIFGRQTAWHWDWEJKZWFMKVGAWDWEWFAWBWCABBIIOZABCIFOZNABDIGOZACDFGOUM 
AWIVEWFVFMAWIWBWCWEMKZJKVEAWBWCWEWJWKWLUEAWBVBWMVDJAVBWBABIUFUGAVDBVCLKWMAV 
CBACDFGUHZIPABCDIFGUIUJTQACDFGPTQQUJUKULAVGBEAVEVFAVBVDABIUNAVCBWNIONADCGFO 
UHZIHSQAVJVHVKMKZVLAWPVJAVHVIAVGBWOIOZAVGEWOHOZUOUGAVHVKWQAVIWRUPUQQQ $. 
$}