${
  amc12-2000-p11.0 $e |- ( ph -> A e. RR ) $.
  amc12-2000-p11.1 $e |- ( ph -> B e. RR ) $.
  amc12-2000-p11.2 $e |- ( ph -> A =/= 0 ) $.
  amc12-2000-p11.3 $e |- ( ph -> B =/= 0 ) $.
  amc12-2000-p11.4 $e |- ( ph -> ( A x. B ) = ( A - B ) ) $.
  $( (Contributed by Stanislas Polu, 26-Oct-2020.) $)
  amc12-2000-p11 $p |- ( ph -> ( ( ( A / B ) + ( B / A ) ) - ( A x. B ) ) = 2 ) 
$=
( cdiv co caddc cmul cmin c2 cexp eqcomd oveq2d eqtrd oveq1d cc0 divmuldivd 
divcld divcan4d divassd mulcomd sqvald eqtr4d oveq12d mulcld mulne0d div23d 
recnd cc wcel wne divcan1 syl3anc sqcld divdird addcld divsubdird binom2sub 
wceq syl2anc 2cnd subcld sub32d subsub4d addsubassd addid1d subsubd addid2d 
subidd ) ABCIJZCBIJZKJZBCLJZMJBNOJZVQIJZCNOJZVQIJZKJZVQNOJZVQIJZMJZNAVPWBVQ 
WDMAVNVSVOWAKAVNVNBLJBIJZVSAWFVNAVNBABCABDULZACEULZGUBZWGFUCPAWFVNBBIJLJZVS 
AVNBBWIWGWGFUDAWJBBLJZVQIJZVSAWJWKCBLJZIJWLABCBBWGWHWGWGGFUAAWMVQWKIACBWHWG 
UEQRAVRWKVQIABWGUFSUGRRAVOVOCLJCIJZWAAWNVOAVOCACBWHWGFUBZWHGUCPAWNVOCCIJLJZ 
WAAVOCCWOWHWHGUDAWPCCLJZVQIJWAACBCCWHWGWHWHFGUAAWQVTVQIAVTWQACWHUFPSRRRUHAW 
DVQAWDVQVQLJZVQIJZVQAWCWRVQIAVQABCWGWHUIZUFSAWSVQVQIJVQLJZVQAVQVQVQWTWTWTAB 
CWGWHFGUJZUKAVQUMUNZXCVQTUOXAVQVCWTWTXBVQVQUPUQRRPUHAWEVRVTKJZVQIJZWDMJZNAW 
BXEWDMAXEWBAVRVTVQABWGURZACWHURZWTXBUSPSAXFXDWCMJZVQIJZNAXJXFAXDWCVQAVRVTXG 
XHUTZAVQWTURWTXBVAPAXJXDBCMJZNOJZMJZVQIJZNAXIXNVQIAWCXMXDMAVQXLNOHSQSAXOXDV 
RNVQLJZMJZVTKJZMJZVQIJZNAXNXSVQIAXMXRXDMABUMUNCUMUNXMXRVCWGWHBCVBVDQSAXTXDV 
TMJZXQMJZVQIJZNAXSYBVQIAYBXSAYBXDXQMJVTMJXSAXDVTXQXKXHAVRXPXGANVQAVEZWTUIZV 
FZVGAXDXQVTXKYFXHVHRPSAYCVRVTVTMJZKJZXQMJZVQIJZNAYBYIVQIAYAYHXQMAVRVTVTXGXH 
XHVISSAYJVRXQMJZVQIJZNAYIYKVQIAYHVRXQMAYHVRTKJVRAYGTVRKAVTXHVMQAVRXGVJRSSAY 
LVRVRMJZXPKJZVQIJZNAYKYNVQIAVRVRXPXGXGYEVKSAYOXPVQIJNAYNXPVQIAYNTXPKJXPAYMT 
XPKAVRXGVMSAXPYEVLRSANVQYDWTXBUCRRRRRRRRRR $.
$}