metamath/valid/algebra-sqineq-36azm9asqle36zsq.mm

${
  algebra-sqineq-36azm9asqle36zsq.0 $e |- ( ph -> Z e. RR ) $.
  algebra-sqineq-36azm9asqle36zsq.1 $e |- ( ph -> A e. RR ) $.
  $( (Contributed by Stanislas Polu, 8-Oct-2020.) $)
  algebra-sqineq-36azm9asqle36zsq $p |- ( ph -> ( ( ; 3 6 x. ( A x. Z ) ) - ( 9 
x. ( A ^ 2 ) ) ) <_ ( ; 3 6 x. ( Z ^ 2 ) ) ) $=
( c3 c6 cmul co c9 c2 cexp cmin cle cc0 wcel a1i remulcld cc mulcld cdc wbr 
caddc cr 6re 3re resubcld sqge0d wceq 6cn recnd 3cn binom2sub syl2anc sqcld 
breqtrd 2cnd subsubd eqcomd mulcomd oveq2d eqidd oveq12d c1 1nn0 1p1e2 6nn0 
sqmuld numexp1 6t6e36 expp1i oveq1d eqtrd mulassd mul4d 2cn 6t2e12 mulcomli 2nn 
decnncl nncni 3nn0 2nn0 0nn0 ax-frege54c dec0h mulid2i addid1i decm1mma 3t2e6 
oveq1i syl6eq sq3 6nn nnrei resqcld 9re subge0d bicomd mpbird ) AFGUA 
ZBCHIZHIZJBKLIZHIZMIZXACKLIZHIZNUBZOXHXFMIZNUBZAOGCHIZKLIZKFBHIZXLHIZHIZXNK 
LIZMIZMIZXJNAOXMKXLXNHIZHIZXQMIZMIZXSNAOXMYAMIXQUCIZYCNAOXLXNMIZKLIZYDNAYEA 
XLXNAGCGUDPAUEQDRAFBFUDPAUFQERUGUHAXLSPXNSPYFYDUIAGCGSPAUJQZACDUKZTZAFBFSPA 
ULQZABEUKZTZXLXNUMUNUPAYCYDAXMYAXQAXLYIUOAKXTAUQZAXLXNYIYLTTAXNYLUOURUSUPAY 
BXRXMMAYAXPXQXQMAXTXOKHAXLXNYIYLUTVAAXQVBVCVAUPAXMXHXRXFMAXMGKLIZXGHIXHAGCY 
GYHVHAYNXAXGHYNXAUIAGXAGVDKUJVEVFGVGVIVJVKQVLVMAXPXCXQXEMAXPKXNHIXLHIZXCAYO 
XPAKXNXLYMYLYIVNUSAYOKGHIZXNCHIZHIZXCAKXNGCYMYLYGYHVOAYRVDKUAZFXBHIZHIZXCAY 
PYSYQYTHYPYSUIAGKYSUJVPVQVRQAFBCYJYKYHVNVCAUUAYSFHIZXBHIZXCAUUCUUAAYSFXBYSS 
PAYSVDKVEVSVTWAQYJABCYKYHTVNUSUUBXAXBHYSFFGVDKFOGWBVGVEWCWDYSWEGVGWFFULWGFK 
GULVPWJVRFULWHWIWKWLVMVMVMAXQFKLIZXDHIXEAFBYJYKVHAUUDJXDHUUDJUIAWMQVLVMVCVC 
UPAXKXIAXHXFAXAXGXAUDPAXAFGWBWNVTWOQZACDWPRAXCXEAXAXBUUEABCEDRRAJXDJUDPAWQQ 
ABEWPRUGWRWSWT $. 
$}