metamath/valid/mathd-algebra-251.mm

${
  mathd-algebra-251.0 $e |- ( ph -> X e. RR ) $.
  mathd-algebra-251.1 $e |- ( ph -> X =/= 0 ) $.
  mathd-algebra-251.2 $e |- ( ph -> ( 3 + ( 1 / X ) ) = ( 7 / X ) ) $.
  $( (Contributed by Kunhao Zheng, 1-Jun-2021.) $)
  mathd-algebra-251 $p |- ( ph -> X = 2 ) $=
( c3 cmul co c1 caddc c7 wceq c2 cdiv cc wcel a1i c6 eqtr4d wb recnd reccld 3cn 
adddird recid2d oveq2d eqtr2d oveq1d 7cn divcan1d 3eqtrd wa simpr 6p1e7 mulcld 
6cn 1cnd addcan2d adantr mpbid 3t2e6 2cnd cc0 wne 3ne0 mulcand mpdan ) 
AFBGHZIJHZKLZBMLZAVIFIBNHZJHZBGHZKBNHZBGHKAVNVHVLBGHZJHVIAFVLBFOPAUCQZABA 
BCUAZDUBVRUDAVPIVHJABVRDUEUFUGAVMVOBGEUHAKBKOPAUIQVRDUJUKAVJULZVHFMGHZLZVKV 
SVHRVTVSVIRIJHZLZVHRLZVSVIKWBAVJUMWBKLVSUNQSAWCWDTVJAVHRIAFBVQVRUOROPAUPQAU 
QURUSUTVTRLVSVAQSAWAVKTVJABMFVRAVBVQFVCVDAVEQVFUSUTVG $.
$}