metamath/valid/algebra-sqineq-2at2pclta2c2p41pc.mm

${
  algebra-sqineq-2at2pclta2c2p41pc.0 $e |- ( ph -> A e. RR ) $.
  algebra-sqineq-2at2pclta2c2p41pc.1 $e |- ( ph -> C e. RR ) $.
  $( (Contributed by Stanislas Polu, 5-Oct-2020.) $)
  algebra-sqineq-2at2pclta2c2p41pc $p |- ( ph -> ( ( 2 x. A ) x. ( 2 + C ) ) <_ 
( ( ( A ^ 2 ) + ( C ^ 2 ) ) + ( 4 x. ( 1 + C ) ) ) ) $=
( cc0 c2 co caddc c4 cmul cmin cle recnd mulcld eqtrd oveq2d breqtrd eqcomd 
wcel cexp c1 wbr resubcld cr 2re readdcld sqge0d cc wceq subcld 2cnd binom2 a1i 
syl2anc sqcld addassd binom2sub mulcomd eqidd oveq12d resqcld subadd23d oveq1d 
addcomd eqtr4d remulcld addsubd mulassd eqtr2d sq2 4cn mulid1i 2t2e4 syl6eqr 
eqtr3d subdid 1cnd addsubassd adddid 4re ax-addrcl sylancr subsub4d 1re subge0d 
mpbid ) AFBGUAHZCGUAHZIHZJUBCIHZKHZIHZGBKHZGCIHZKHZLHZMUCWPWMMU 
CAFWMWNCKHZWNGKHZIHZLHZWQMAFWMWRLHZWSLHZXAMAFWJWRLHZWLIHZWSLHZXCMAFXDWLWSLH 
ZIHZXFMAFWHGBCKHZKHZLHZWIIHZGCBLHZGKHZKHZGGUAHZIHZIHZXHMAFWIXJLHZWHIHZXQIHZ 
XRMAFXMGIHZGUAHZYAMAYBAXMGACBEDUDGUETAUFUNZUGUHAYCXMGUAHZXQIHZYAAYCYEXOIHXP 
IHZYFAXMUITGUITYCYGUJACBACENZABDNZUKZAULZXMGUMUOAYEXOXPAXMYJUPAGXNYKAXMGYJY 
KOOZAGYKUPZUQPAYEXTXQXQIAYEWIGCBKHZKHZLHZWHIHZXTACUITBUITYEYQUJYHYICBURUOAY 
PXSWHIAYOXJWILAYNXIGKACBYHYIUSQQVDPAXQUTZVAPRAXTXLXQXQIAXTWIXKIHXLAWIXJWHAC 
YHUPZAGXIYKABCYIYHOOZAWHABDVBZNZVCAXKWIAWHXJUUBYTUKYSVEVFYRVARAXLXDXQXGIAXD 
WHWRLHZWIIHXLAWHWIWRUUBYSAWNCAWNAGBYDDVGZNZYHOZVHAUUCXKWIIAWRXJWHLAGBCYKYIY 
HVIQVDVJAXQJUBKHZJCKHZIHZWSLHZXGAXQXPXOIHZUUJAXOXPYLYMVEAUUKUUGUUHWSLHZIHZU 
UJAXPUUGXOUULIAXPJUUGXPJUJAVKUNJVLVMVOAXOGGXMKHZKHZUULAXNUUNGKAXMGYJYKUSQAU 
ULUUHGWNKHZLHZUUOAWSUUPUUHLAWNGUUEYKUSQAUUQUUHJBKHZLHZUUOAUUPUURUUHLAGGKHZB 
KHUUPUURAGGBYKYKYIVIAUUTJBKUUTJUJAVNUNZVDVPQAUUSUUTXMKHZUUOAUUSJXMKHZUVBAUV 
CUUSAJCBJUITAVLUNZYHYIVQSAUUTJXMKUVAVDVFAUVBUUOAGGXMYKYKYJVISVFPPVFVAAUUJUU 
MAUUGUUHWSAJUBUVDAVRZOAJCUVDYHOAWNGUUEYKOZVSSPPAUUIWLWSLAWLUUIAJUBCUVDUVEYH 
VTSVDPVARAXFXHAXDWLWSAWJWRAWJAWHWIUUAACEVBUGZNZUUFUKAWLAJWKJUETAWAUNAUBUETC 
UETWKUETWEEUBCWBWCVGZNZUVFVSSRAXEXBWSWSLAXBXEAWJWLWRUVHUVJUUFVHSAWSUTVARAWM 
WRWSAWMAWJWLUVGUVIUGZNUUFUVFWDRAWMWMWTWPLAWMUTAWTWNCGIHZKHZWPAUVMWTAWNCGUUE 
YHYKVTSAWOUVLWNKAGCYKYHVEQVFVARAWMWPUVKAWNWOUUDAGCYDEUGVGWFWG $. 
$}