let R be preordered domRing; :: thesis: for P being Preordering of R
for a being b1 -ordered Element of R
for p being b1 -ordered non b1 -negative Element of R holds
( abs (P,a) <= P,p iff ( - p <= P,a & a <= P,p ) )
let P be Preordering of R; :: thesis: for a being P -ordered Element of R
for p being P -ordered non P -negative Element of R holds
( abs (P,a) <= P,p iff ( - p <= P,a & a <= P,p ) )
let a be P -ordered Element of R; :: thesis: for p being P -ordered non P -negative Element of R holds
( abs (P,a) <= P,p iff ( - p <= P,a & a <= P,p ) )
let p be P -ordered non P -negative Element of R; :: thesis: ( abs (P,a) <= P,p iff ( - p <= P,a & a <= P,p ) )
H: ( not p in (- P) \ {(0. R)} & p in P \/ (- P) ) by defn, defppp;
then ( not p in - P or p in {(0. R)} ) by XBOOLE_0:def 5;
then As: ( not p in - P or p = 0. R ) by TARSKI:def 1;
then AS: ( a in P \/ (- P) & 0. R <= P,p ) by defppp, H, XBOOLE_0:def 3, REALALG1:25;
hereby :: thesis: ( - p <= P,a & a <= P,p implies abs (P,a) <= P,p )
assume A1: abs (P,a) <= P,p ; :: thesis: ( - p <= P,a & a <= P,p )
per cases ( a in P or a in - P ) by AS, XBOOLE_0:def 3;
suppose a in P ; :: thesis: ( - p <= P,a & a <= P,p )
then A2: 0. R <= P,a ;
A3: a <= P, abs (P,a) by ineq2;
- p <= P, 0. R by As, H, XBOOLE_0:def 3, REALALG1:25;
hence ( - p <= P,a & a <= P,p ) by A3, A2, A1, c3; :: thesis: verum
end;
suppose a in - P ; :: thesis: ( - p <= P,a & a <= P,p )
then - a in - (- P) ;
then A3: - (- a) <= P, 0. R ;
- (abs (P,a)) <= P,a by ineq2;
then - a <= P, - (- (abs (P,a))) by c10a;
then - a <= P,p by A1, c3;
hence ( - p <= P,a & a <= P,p ) by A3, AS, c3, c10a; :: thesis: verum
end;
end;
end;
assume A1: ( - p <= P,a & a <= P,p ) ; :: thesis: abs (P,a) <= P,p
per cases ( a in P or a in - P ) by AS, XBOOLE_0:def 3;
suppose a in P ; :: thesis: abs (P,a) <= P,p
then 0. R <= P,a ;
hence abs (P,a) <= P,p by A1, av2; :: thesis: verum
end;
suppose a in - P ; :: thesis: abs (P,a) <= P,p
then - a in - (- P) ;
then - (- a) <= P, 0. R ;
then abs (P,a) = - a by av3;
hence abs (P,a) <= P,p by A1, c10a; :: thesis: verum
end;
end;