metamath/valid/algebra-binomnegdiscrineq-10alt28asqp1.mm

${
  algebra-binomnegdiscrineq-10alt28asqp1.0 $e |- ( ph -> A e. RR ) $.
  $( (Contributed by Stanislas Polu, 8-Oct-2020.) $)
  algebra-binomnegdiscrineq-10alt28asqp1 $p |- ( ph -> ( ; 1 0 x. A ) <_ ( ( ; 
2 8 x. ( A ^ 2 ) ) + 1 ) ) $=
( cc0 c2 c8 cdc co cmul c1 caddc cle wbr wcel 2nn0 a1i 1nn0 0nn0 c4 c3 cexp 
cmin cneg cr 8nn0 deccl nn0rei renegcld 1red clt decnncl nngt0i wceq nn0cni 
negcli 1p1e2 0p1e1 exp0i mulid2i expp1i ax-frege54c mul02i addid1i decm1mma 8nn 
dec0h mul2negib 2nn nnrei 10pos 1nn 0lt1 declt decltc ltleii 4nn0 4t2e8 3nn0 
oveq1i 8p3e11 eqtri 8cn 8t4e32 mulcomli decmul2c mulid1d eqcomd oveq2d 4cn 
recnd eqtr3d breqtrd eqbrtrd quadineqpos resqcl remulcld cc mulcld 1cnd addassd 
addsubd negsubd mulneg1d eqtrd oveq1d eqtr2d readdcld subge0d mpbid syl ) 
ADEFGZBEUAHZIHZJKHZJDGZBIHZUBHZLMXPXNLMADXMXOUCZBIHZJKHKHZXQLAXKXRJBX 
KUDNAXKEFOUEUFUGPZAXOXOUDNAXOJDQRUFZUGPZUHAUIZCDXKUJMAXKEFOVEUKULPAXREUAHZX 
ODGZSXKJIHZIHZLYEYFUMAXRYFXRJEXOXOYBUNZUOZQUPXRXRJDJYJRUQXRYJURXRYJUSUTXOXO 
YFYIYIYFXODYBRUFZUNXOXOXODJDXODDYBRQRRXOVADRVFXOYIUSXOYIVBXOYIVCVDVGUTPAYFJ 
JGZEGZYHLYFYMLMAYFYMYFYKUGYMYLEJJQQUFZVHUKVIXOYLDEYBYNROVJJDJQRVKVLVMVNVOPA 
SXKIHZYMYHYOYMUMAEFYLESTXKVPOUEXKVAOVRSEIHZTKHFTKHYLYPFTKVQVSVTWAFSTEGWBWIW 
CWDWEPAXKYGSIAYGXKAXKAXKYAWJWFWGWHWKWLWMWNAXTXMXSKHZJKHZXQAYRXTAXMXSJAXMAXK 
XLYAABUDNXLUDNCBWOXJWPZWJZAXRBXRWQNAYJPABCWJZWRAWSZWTWGAXQXMXPUBHZJKHYRAXMJ 
XPYTUUBAXPAXOBYCCWPZWJZXAAUUCYQJKAUUCXMXPUCZKHZYQAUUGUUCAXMXPYTUUEXBWGAUUFX 
SXMKAXSUUFAXOBXOWQNAYIPUUAXCWGWHXDXEXFXDWLAXNXPAXMJYSYDXGUUDXHXI $. 
$}