metamath/valid/amc12b-2003-p17.mm

${
  amc12b-2003-p17.0 $e |- ( ph -> X e. RR+ ) $.
  amc12b-2003-p17.1 $e |- ( ph -> Y e. RR+ ) $.
  amc12b-2003-p17.2 $e |- ( ph -> ( log ` ( X x. ( Y ^ 3 ) ) ) = 1 ) $.
  amc12b-2003-p17.3 $e |- ( ph -> ( log ` ( ( X ^ 2 ) x. Y ) ) = 1 ) $.
  $( (Contributed by Stanislas Polu, 26-Nov-2020.) $)
  amc12b-2003-p17 $p |- ( ph -> ( log ` ( X x. Y ) ) = ( 3 / 5 ) ) $=
( cmul co clog cfv caddc c3 c5 wcel a1i oveq12d c1 c2 eqtrd relogmuld recnd 
cdiv relogcld addcld cc 5cn cc0 wne 5pos gt0ne0ii adddird mulcomd eqtr4d c4 5re 
wceq 2t2e4 oveq2i 4cn ax-1cn 4p1e5 addcomli syl6req 2t1e2 3p2e5 syl5req oveq1d 
1cnd 2cnd mulcld 3cn mulid2d mulassd oveq2d add4d adddid eqcomd cexp crp cz 3z 
relogexp sylancl rpexpcl rpexpcld df-3 addcomd syl6eqr mvlrmuld 2z ) 
ABCHIJKBJKZCJKZLIZMNUCIABCDEUAAWNNMAWLWMAWLABDUDUBZAWMACEUDUBZUENUFOAU 
GPZNUHUIANUPUJUKPAWNNHIZNWLHIZNWMHIZLIZMAWRWLNHIZWMNHIZLIXAAWLWMNWOWPWQULAW 
SXBWTXCLANWLWQWOUMANWMWQWPUMQUNAXARSSHIZLIZWLHIZMSRHIZLIZWMHIZLIZMAWSXFWTXI 
LANXEWLHAXERUOLIZNXEXKUQAXDUORLURUSPUORNUTVAVBVCVDVHANXHWMHAXHMSLIZNXGSMLVE 
USXLNUQAVFPVGVHQAXJRWLHIZXDWLHIZLIZMWMHIZXGWMHIZLIZLIZMAXFXOXIXRLARXDWLAVIZ 
ASSAVJZYAVKWOULAMXGWMMUFOAVLPZASRYAXTVKWPULQAXSWLSSWLHIZHIZLIZXPSWMHIZLIZLI 
ZMAXOYEXRYGLAXMWLXNYDLAWLWOVMASSWLYAYAWOVNQAXQYFXPLAXGSWMHXGSUQAVEPVHVOQAYH 
WLXPLIZYDYFLIZLIZMAWLYDXPYFWOASYCYAASWLYAWOVKZVKAMWMYBWPVKASWMYAWPVKVPAYKYI 
SYCWMLIZHIZLIZMAYJYNYILAYNYJASYCWMYAYLWPVQVRVOAYOWLCMVSIZJKZLIZSBSVSIZJKZWM 
LIZHIZLIZMAYIYRYNUUBLAXPYQWLLAYQXPACVTOZMWAOZYQXPUQEWBCMWCWDVRVOAYMUUASHAYC 
YTWMLAYTYCABVTOSWAOZYTYCUQDWKBSWCWDVRVHVOQAUUCBYPHIJKZSYSCHIJKZHIZLIZMAYRUU 
GUUBUUILAUUGYRABYPDAUUDUUEYPVTOEWBCMWEWDUAVRAUUAUUHSHAUUHUUAAYSCABSDUUFAWKP 
WFEUAVRVOQAUUJRXGLIZMAUUGRUUIXGLFAUUHRSHGVOQAMSRLIZUUKWGAUULRSLIUUKASRYAXTW 
HXGSRLVEUSWIVGTTTTTTTTTWJT $.
$}