metamath/valid/amc12a-2003-p24.mm

${
  amc12a-2003-p24.0 $e |- ( ph -> A e. RR ) $.
  amc12a-2003-p24.1 $e |- ( ph -> B <_ A ) $.
  amc12a-2003-p24.2 $e |- ( ph -> B e. RR ) $.
  amc12a-2003-p24.3 $e |- ( ph -> 1 < B ) $.
  $( (Contributed by Stanislas Polu, 16-Nov-2020.) $)
  amc12a-2003-p24 $p |- ( ph -> ( ( A logb ( A / B ) ) + ( B logb ( B / A ) ) ) 
<_ 0 ) $=
( cdiv co clogb caddc cmin cc0 cle cc c1 wcel a1i c2 wne cpr cdif crp recnd 
wceq 0red 1red clt wbr 0lt1 ltled ltletrd gt0ne0d gtned nelprd eldifd elrpd 
rpgecld relogbdiv syl12anc rpne0d oveq12d alogbaeq1d oveq1d 1cnd cr syl3anc 
relogbcl addsub4d eqcomd df-2 eqtr4d logbswitchd oveq2d 2re clog cfv csn wa 
rpcnne0d eldifsn logbval syl2anc logccne0 divne0d eqnetrd rereccld readdcld 
sylibr logcld halfre cmul ax-1cn 2cn 2ne0 divcan1i ccxp halfcld 1cxpd eqidd 
recidd eqtrd rplogcld rpdivcld eqeltrd rpreccld amgm2d eqbrtrd 2cnd breqtrd 
divrec2d halfgt0 wwlemuld suble0d mpbird ) ABBCHIJIZCCBHIJIZKIBBJIZBCJIZLIZ 
CCJIZCBJIZLIZKIZMNAXPXTXQYCKABOMPUAZUBZQZBUCQZCUCQZXPXTUEABOYEABDUDZABMPABA 
MCBAUFZFDAMPCYKAUGZFMPUHUIAUJRAPCYLFGUKULZEULUMZAPBYLAPCBYLFDGEULZUNZUOUPZA 
BCDACFYMUQZEURZYRBBCUSUTACYFQYIYHXQYCUEACOYEACFUDZACMPACYRVAZAPCYLGUNZUOUPY 
RYSCCBUSUTVBAYDPXSLIZPYBLIZKIZMNAXTUUCYCUUDKAXRPXSLABYJYPYNVCVDAYAPYBLACYTU 
UBUUAVCVDVBAUUESXSYBKIZLIZMNAUUEPPKIZUUFLIZUUGAUUIUUEAPPXSYBAVEZUUJAXSAYHYI 
BPTZXSVFQYSYRYPBCVHVGZUDZAYBAYIYHCPTZYBVFQYRYSUUBCBVHVGUDVIVJASUUHUUFLSUUHU 
EAVKRVDVLAUUGSXSPXSHIZKIZLIZMNAUUFUUPSLAYBUUOXSKACBYTUUAUUBYJYNYPVMVNVNAUUQ 
MNUISUUPNUIASUUPPSHIZSVFQAVORZAXSUUOUULAXSUULAXSCVPVQZBVPVQZHIZMAYGCOMVRUBQ 
ZXSUVBUEYQACOQZCMTZVSUVCACYRVTCOMWAWIBCWBWCZAUUTUVAACYTUUAWJABYJYNWJAUVDUVE 
UUNUUTMTYTUUAUUBCWDVGABOQBMTUUKUVAMTYJYNYPBWDVGWEWFZWGWHZUURVFQAWKRAUURSWLI 
ZPUURUUPWLIZNUVIPUEAPSWMWNWOWPRAPUUPSHIZUVJNAPXSUUOWLIZUURWQIZUVKNAPPUURWQI 
ZUVMAUVNPAUURAPUUJWRWSVJAPUVLUURUURWQAUVLPAXSUUMUVGXAVJAUURWTVBXBAXSUUOAXSU 
VBUCUVFAUUTUVAACFGXCABDYOXCXDXEZAXSUVOXFXGXHAUUPSAUUPUVHUDAXISMTAWORXKXJXHM 
UURUHUIAXLRXMASUUPUUSUVHXNXOXHXHXHXH $.
$}