let R be preordered domRing; 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; 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; 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; ( 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 ( - p <= P,a & a <= P,p implies abs (P,a) <= P,p )
assume A1:
abs (
P,
a)
<= P,
p
;
( - 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
;
( - 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;
verum end; suppose
a in - P
;
( - 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;
verum end; end;
end;
assume A1:
( - p <= P,a & a <= P,p )
; abs (P,a) <= P,p