metamath/valid/algebra-sqineq-4bap1lt4bsqpap1sq.mm

${
  algebra-sqineq-4bap1lt4bsqpap1sq.0 $e |- ( ph -> A e. RR ) $.
  algebra-sqineq-4bap1lt4bsqpap1sq.1 $e |- ( ph -> B e. RR ) $.
  $( (Contributed by Stanislas Polu, 26-Nov-2020.) $)
  algebra-sqineq-4bap1lt4bsqpap1sq $p |- ( ph -> ( ( 4 x. B ) x. ( A + 1 ) ) <_ 
( ( 4 x. ( B ^ 2 ) ) + ( ( A + 1 ) ^ 2 ) ) ) $=
( c4 cmul co c1 caddc cexp cle cc0 cmin mulcld breqtrd eqcomd eqtrd oveq2d c2 
wbr cr wcel 2re a1i remulcld 1red resubcld sqge0d wceq 2cnd recnd subcld cc 
binom2sub syl2anc mulassd mul32d oveq1d subadd23d subdid subsub2d sqmuld sqcld 
sq2 mulid1d 2t2e4 oveq12d 4re resqcld addsubd addsubassd addcld mul4d mulcomd 
eqtr2d subsub4d addcomd add12d binom2 adddid readdcld bicomd mpbird 1cnd 
subge0d ) AFCGHZBIJHZGHZFCTKHZGHZWHTKHZJHZLUAZMWMWINHZLUAZAMWKBTKHZTBI 
GHZGHZJHZITKHZJHZJHZWGBGHZWGIGHZJHZNHZWOLAMWKXAJHZWTJHZXDWGJHZNHZXGLAMXIWGX 
DJHZNHZXKLAMXIWGNHZXDNHZXMLAMXHWGNHZWQTBGHZIGHZJHZJHZXQTCGHZGHZNHZXOLAMXPXS 
YBNHZJHZYCLAMYAINHZTKHZWQXRYBNHJHZJHZYELAMYGWQYBXRNHZNHZJHZYILAMYGWQXQYFGHZ 
NHZJHZYLLAMYGYMNHZWQJHZYOLAMYGTYFBGHGHZNHZWQJHZYQLAMYFBNHZTKHZYTLAUUAAYFBAY 
AIATCTUBUCAUDUEEUFAUGZUHDUHUIAYFUNUCBUNUCZUUBYTUJAYAIATCAUKZACEULZOZAWEZUMZ 
ABDULZYFBUOUPPAYSYPWQJAYRYMYGNAYRTYFGHBGHZYMAUUKYRATYFBUUEUUIUUJUQQATYFBUUE 
UUIUUJURRSUSPAYGYMWQAYFUUIVDAXQYFATBUUEUUJOZUUIOABUUJVDZUTPAYNYKYGJAYMYJWQN 
AXQYAIUULUUGUUHVASSPAYKYHYGJAWQYBXRUUMAXQYAUULUUGOZAXQIUULUUHOZVBSPAYGXPYHY 
DJAYGWKWGNHZXAJHZXPAYGYATKHZTYAIGHZGHZNHZXAJHZUUQAYAUNUCIUNUCZYGUVBUJUUGUUH 
YAIUOUPAUVAUUPXAJAUURWKUUTWGNAUURTTKHZWJGHWKATCUUEUUFVCAUVDFWJGUVDFUJAVEUEU 
SRAUUTTYAGHZWGAUUSYATGAYAUUGVFSAWGUVEAWGTTGHZCGHUVEAFUVFCGAUVFFUVFFUJAVGUEZ 
QUSATTCUUEUUEUUFUQRQRVHUSRAXPUUQAWKXAWGAWKAFWJFUBUCAVIUEZACEVJUFZULZAIUUHVD 
ZAFCAFUVHULZUUFOZVKQRAYDYHAWQXRYBUUMUUOUUNVLQVHPAYCYEAXPXSYBAXHWGAWKXAUVJUV 
KVMZUVMUMAWQXRUUMUUOVMUUNVLQPAXTXNYBXDNAXNXTAXNXPWTJHXTAXHWTWGUVNAWQWSUUMAT 
WRUUEABIUUJUUHOOVMZUVMVKAWTXSXPJAWSXRWQJAXRWSATBIUUEUUJUUHUQQSSRQAYBFBCGHZG 
HZXDAYBUVFUVPGHUVQATBTCUUEUUJUUEUUFVNAUVFFUVPGUVGUSRAXDFCBGHZGHUVQAFCBUVLUU 
FUUJUQAUVRUVPFGACBUUFUUJVOSVPRVHPAXIWGXDAXHWTUVNUVOVMUVMAWGBUVMUUJOZVQPAXLX 
JXINAWGXDUVMUVSVRSPAXIXCXJXFNAXIWTXHJHXCAXHWTUVNUVOVRAWTWKXAUVOUVJUVKVSRAWG 
XEXDJAXEWGAWGUVMVFQSVHPAXCWMXFWINAXBWLWKJAWLXBAUUDUVCWLXBUJUUJUUHBIVTUPQSAW 
IXFAWGBIUVMUUJUUHWAQVHPAWPWNAWMWIAWKWLUVIAWHABIDUUCWBZVJWBAWGWHAFCUVHEUFUVT 
UFWFWCWD $. 
$}