metamath/valid/algebra-2varlineareq-xpeeq7-2xpeeq3-eeq11-xeqn4.mm

${
  algebra-2varlineareq-xpeeq7-2xpeeq3-eeq11-xeqn4.0 $e |- ( ph -> X e. CC ) $.
  algebra-2varlineareq-xpeeq7-2xpeeq3-eeq11-xeqn4.1 $e |- ( ph -> E e. CC ) $.
  algebra-2varlineareq-xpeeq7-2xpeeq3-eeq11-xeqn4.2 $e |- ( ph -> ( X + E ) = 7 
) $.
  algebra-2varlineareq-xpeeq7-2xpeeq3-eeq11-xeqn4.3 $e |- ( ph -> ( ( 2 x. X ) 
+ E ) = 3 ) $.
  $( (Contributed by Stanislas Polu, 5-Oct-2020.) $)
  algebra-2varlineareq-xpeeq7-2xpeeq3-eeq11-xeqn4 $p |- ( ph -> ( E = ; 1 1 /\ 
X = -u 4 ) ) $=
( c1 c4 a1i cmin co cmul c2 mulcld caddc c3 eqtrd c8 c7 wceq cneg wcel 1nn0 cdc 
cc deccl nn0cni subcld 1cnd 2cnd wne 1t1e1 1ne2 eqnetri mulid2d subne0d 
neeqtrrd cc0 subdid mulcomd oveq12d 4cn negcld addcomd mulid2i 2cn mulneg2i 
oveq2d 4t2e8 mulcomli negeqi eqtri oveq1i negcli negsubi addcomli subaddrii 8cn 
3cn 8p3e11 lineqlem0d facmullelimd addcomgi 7cn facmulrelimd subeq0addd 7p4e11 
muleq0d subeq0d jca ) ABHHUEZUACIUBZUAABWLEWLUFUCAWLHHUDUDUGUHZJZABW 
LKLZHHMLZHNMLZKLZABWLEWOUIZAWQWRAHHAUJZXAOZAHNXAAUKZOZUIZAWQWRXBXDAWQNWRWQN 
ULAWQHNUMUNUOJANXCUPURUQZAWPWSMLWPWQMLZWPWRMLZKLZUSAWPWQWRWTXBXDUTAXIWQWPML 
ZWRWPMLZKLUSAXGXJXHXKKAWPWQWTXBVAAWPWRWTXDVAVBAXJXKWRCWMKLZMLZAWQWPXBWTOZAW 
RWPXDWTOAWRXLXDACWMDAIIUFUCAVCJVDZUIZOZAHNHWPXLXAAHWPMLZNXLMLZPLXSXRPLUSAXR 
XSAHWPXAWTOZANXLXCXPOVEANWMWLHQCBXCANCMLZHBMLZPLYABPLQAYBBYAPABEUPZVIGRANWM 
MLZHWLMLZPLYDWLPLZQAYEWLYDPYEWLUAAWLWNVFJZVIYFQUAAYFSUBZWLPLZQYDYHWLPYDNIML 
ZUBYHNIVGVCVHYJSINSVCVGVJVKVLVMVNYIWLSKLZQWLYHYKWNSVSVOWLSWNVSVPVQWLSQWNVSV 
TWAVRVMVMJRXOWOXADEQUFUCAVTJWBZRXAXCWTXPWCAHHNWPXLXAAXRHXLMLZPLYMXRPLUSAXRY 
MXTAHXLXAXPOVEAHWMWLHTCBXAAHCMLZYBPLCBPLTAYNCYBBPACDUPYCVBFRAHWMMLZYEPLWMWL 
PLZTAYOWMYEWLPAWMXOUPYGVBYPTUAAYPWLWMPLZTWMWLWDYQWLIKLTWLIWNVCVPWLITWNVCWET 
IWLWEVCWHVQVRVMVMJRXOWOXADETUFUCAWEJWBZRXCXAWTXPWFWGRRWIWJACWMDXOAXLWSXPXEX 
FAXLWSMLXLWQMLZXLWRMLZKLZUSAXLWQWRXPXBXDUTAUUAWQXLMLZXMKLUSAYSUUBYTXMKAXLWQ 
XPXBVAAXLWRXPXDVAVBAUUBXMXJAWQXLXBXPOXQXNAHHHXLWPXAYRXAXAXPWTWFANHHXLWPXCYL 
XAXAXPWTWCWGRRWIWJWK $. 
$}