let R be ordered domRing; :: thesis: for O being Ordering of R
for a being square Element of R holds
not for b being Sqrt of a holds b is O -negative
let O be Ordering of R; :: thesis: for a being square Element of R holds
not for b being Sqrt of a holds b is O -negative
let a be square Element of R; :: thesis: not for b being Sqrt of a holds b is O -negative
consider b being Element of R such that
H: b ^2 = a by O_RING_1:def 2;
reconsider b = b as Sqrt of a by H, defsqrt;
A: O \/ (- O) = the carrier of R by REALALG1:def 8;
per cases ( b = 0. R or b <> 0. R ) ;
suppose C: b = 0. R ; :: thesis: not for b being Sqrt of a holds b is O -negative
take b ; :: thesis: not b is O -negative
thus not b is O -negative by C; :: thesis: verum
end;
suppose X: b <> 0. R ; :: thesis: not for b being Sqrt of a holds b is O -negative
per cases ( b in O or b in - O ) by A, XBOOLE_0:def 3;
suppose b in O ; :: thesis: not for b being Sqrt of a holds b is O -negative
then 0. R <= O,b ;
then B: 0. R < O,b by X;
take b ; :: thesis: not b is O -negative
thus not b is O -negative by B, x1; :: thesis: verum
end;
suppose b in - O ; :: thesis: not for b being Sqrt of a holds b is O -negative
then - b in - (- O) ;
then 0. R <= O, - b ;
then B: 0. R < O, - b by X;
set c = - b;
(- b) ^2 = b ^2 by VECTSP_1:10;
then reconsider c = - b as Sqrt of a by defsqrt;
take c ; :: thesis: not c is O -negative
thus not c is O -negative by B, x1; :: thesis: verum
end;
end;
end;
end;