metamath/valid/amc12-2000-p5.mm

${
  amc12-2000-p5.0 $e |- ( ph -> X e. RR ) $.
  amc12-2000-p5.1 $e |- ( ph -> P e. RR ) $.
  amc12-2000-p5.2 $e |- ( ph -> ( abs ` ( X - 2 ) ) = P ) $.
  amc12-2000-p5.3 $e |- ( ph -> X < 2 ) $.
  $( (Contributed by Stanislas Polu, 26-Oct-2020.) $)
  amc12-2000-p5 $p |- ( ph -> ( X - P ) = ( 2 - ( 2 x. P ) ) ) $=
( c2 cmin co wceq cmul wcel eqtrd caddc adantr eqcomd cc0 c1 ax-1cn abssubd 
cabs cfv recnd 2cnd cr 2re a1i ltled abssubge0d eqtr2d mulcld subcld addcld wa 
addsub12d oveq2d subsub4d subidd oveq1d cneg mulid2d 1cnd subdird eqtr4d cc 2cn 
neg1cn 2m1e1 negsubib subaddrii oveq1i mulm1d syl5eq subnegd addid2d 0cnd simpr 
subcand wb subaddd bicomd mpbid mpdan ) AHCIJZBKZCBIJHHBLJZIJZKZ 
AWECHIJUBUCZBAWJWEUBUCWEACHACDUDZAUEZUAACHDHUFMAUGUHZACHDWMGUIUJUKFNAWFUOZB 
WHOJZCKZWIWNHWOCWNUEAWOVFMWFABWHABEUDZAHWGWLAHBWLWQULZUMZUNPACVFMWFWKPWNHWO 
IJZBWEAWTBKWFAWTHHBWGIJZOJZIJZBAWOXBHIABHWGWQWLWRUPUQAXCHHIJZXAIJZBAXEXCAHH 
XAWLWLABWGWQWRUMURQAXERXAIJZBAXDRXAIAHWLUSUTAXFRBVAZIJZBAXAXGRIAXASHIJZBLJZ 
XGAXASBLJZWGIJXJABXKWGIAXKBABWQVBQUTASHBAVCWLWQVDVEAXJSVAZBLJXGXIXLBLSHXLTV 
GVHHSSVGTTVIVJVKVLABWQVMVNNUQAXHRBOJBARBAVQWQVOABWQVPNNNNNPWNWEBAWFVRQNVSAW 
PWIVTWFAWIWPACBWHWKWQWSWAWBPWCWD $.
$}