metamath/valid/algebra-manipexpr-2erprsqpesqeqnrpnesq.mm

${
  algebra-manipexpr-2erprsqpesqeqnrpnesq.0 $e |- ( ph -> E e. CC ) $.
  algebra-manipexpr-2erprsqpesqeqnrpnesq.1 $e |- ( ph -> R e. CC ) $.
  $( (Contributed by Stanislas Polu, 8-Oct-2020.) $)
  algebra-manipexpr-2erprsqpesqeqnrpnesq $p |- ( ph -> ( ( 2 x. ( E x. R ) ) + 
( ( E ^ 2 ) + ( R ^ 2 ) ) ) = ( ( -u R + -u E ) ^ 2 ) ) $=
( c2 cmul co cexp caddc cneg cc wcel wceq sqneg oveq2d oveq12d sqcld mulcld syl 
mul2negd 2cnd add32d addcomd mulcomd addcld eqtr4d eqtr2d negcld binom2 eqtrd 
syl2anc eqcomd ) AFCBGHZGHZCFIHZBFIHZJHZJHZBKZFIHZFUTCKZGHZGHZJHZVBFI 
HZJHZUTVBJHFIHZAVGUQFBCGHZGHZJHZUPJHZUSAVEVKVFUPJAVAUQVDVJJABLMVAUQNEBOTAVC 
VIFGABCEDUAPQACLMVFUPNDCOTQAVLUQUPJHZVJJHZUSAUQVJUPABERZAFVIAUBZABCEDSSACDR 
ZUCAVNURUOJHUSAVMURVJUOJAUQUPVOVQUDAVIUNFGABCEDUEPQAUOURAFUNVPACBDESSAUPUQV 
QVOUFUDUGUKUHAVHVGAUTLMVBLMVHVGNABEUIACDUIUTVBUJULUMUK $. 
$}