let R be ordered domRing; :: thesis: for O being Ordering of R
for a, b being non b1 -negative Element of R holds
( a <= O,b iff a ^2 <= O,b ^2 )
let P be Ordering of R; :: thesis: for a, b being non P -negative Element of R holds
( a <= P,b iff a ^2 <= P,b ^2 )
let a, b be non P -negative Element of R; :: thesis: ( a <= P,b iff a ^2 <= P,b ^2 )
the carrier of R = P \/ (- P) by REALALG1:def 8;
then A: ( a is P -ordered & b is P -ordered ) ;
then AS: ( 0. R <= P,a & 0. R <= P,b ) by x1a;
per cases ( a = 0. R or a <> 0. R ) ;
suppose K: a = 0. R ; :: thesis: ( a <= P,b iff a ^2 <= P,b ^2 )
( SQ R c= P & b ^2 in SQ R ) by REALALG1:def 14;
hence ( a <= P,b iff a ^2 <= P,b ^2 ) by A, x1a, K; :: thesis: verum
end;
suppose K: a <> 0. R ; :: thesis: ( a <= P,b iff a ^2 <= P,b ^2 )
hereby :: thesis: ( a ^2 <= P,b ^2 implies a <= P,b )
assume a <= P,b ; :: thesis: a ^2 <= P,b ^2
then ( a * a <= P,b * a & a * b <= P,b * b ) by AS, c5;
hence a ^2 <= P,b ^2 by c3; :: thesis: verum
end;
C: ( P * (- P) c= - P & P + P c= P ) by v2, REALALG1:def 14;
B: a + b in P + P by AS;
D: the carrier of R = P \/ (- P) by REALALG1:def 8;
assume a ^2 <= P,b ^2 ; :: thesis: a <= P,b
then A: (b + a) * (b - a) in P by P4a;
per cases ( b - a in - P or b - a in P ) by D, XBOOLE_0:def 3;
suppose b - a in - P ; :: thesis: a <= P,b
then (b + a) * (b - a) in P * (- P) by B, C;
then (b + a) * (b - a) in P /\ (- P) by A, C;
then (b + a) * (b - a) in {(0. R)} by REALALG1:def 7;
then D: (b + a) * (b - a) = 0. R by TARSKI:def 1;
end;
suppose b - a in P ; :: thesis: a <= P,b
hence a <= P,b ; :: thesis: verum
end;
end;
end;
end;