:: ABSVALUE semantic presentation

definition
let c1 be real number ;
redefine func |.c1.| -> set equals :Def1: :: ABSVALUE:def 1
a1 if 0 <= a1
otherwise - a1;
correctness
compatibility
for b1 being set holds
( ( 0 <= c1 implies ( b1 = |.c1.| iff b1 = c1 ) ) & ( not 0 <= c1 implies ( b1 = |.c1.| iff b1 = - c1 ) ) );
consistency
for b1 being set holds verum;
by COMPLEX1:129, COMPLEX1:156;
end;

:: deftheorem Def1 defines |. ABSVALUE:def 1 :
for b1 being real number holds
( ( 0 <= b1 implies |.b1.| = b1 ) & ( not 0 <= b1 implies |.b1.| = - b1 ) );

theorem Th1: :: ABSVALUE:1
for b1 being real number holds
( abs b1 = b1 or abs b1 = - b1 )
proof end;

Lemma2: for b1 being real number holds 0 <= abs b1
by COMPLEX1:132;

Lemma3: for b1 being real number st b1 <> 0 holds
0 < abs b1
by COMPLEX1:133;

theorem Th2: :: ABSVALUE:2
canceled;

theorem Th3: :: ABSVALUE:3
canceled;

theorem Th4: :: ABSVALUE:4
canceled;

theorem Th5: :: ABSVALUE:5
canceled;

theorem Th6: :: ABSVALUE:6
canceled;

theorem Th7: :: ABSVALUE:7
for b1 being real number holds
( b1 = 0 iff abs b1 = 0 ) by Def1, COMPLEX1:133;

theorem Th8: :: ABSVALUE:8
canceled;

theorem Th9: :: ABSVALUE:9
for b1 being real number st abs b1 = - b1 & b1 <> 0 holds
b1 < 0
proof end;

Lemma4: for b1, b2 being real number holds abs (b1 * b2) = (abs b1) * (abs b2)
by COMPLEX1:151;

theorem Th10: :: ABSVALUE:10
canceled;

theorem Th11: :: ABSVALUE:11
for b1 being real number holds
( - (abs b1) <= b1 & b1 <= abs b1 )
proof end;

theorem Th12: :: ABSVALUE:12
for b1, b2 being real number holds
( ( - b1 <= b2 & b2 <= b1 ) iff abs b2 <= b1 )
proof end;

Lemma5: for b1, b2 being real number holds abs (b1 + b2) <= (abs b1) + (abs b2)
by COMPLEX1:142;

theorem Th13: :: ABSVALUE:13
canceled;

theorem Th14: :: ABSVALUE:14
for b1 being real number st b1 <> 0 holds
(abs b1) * (abs (1 / b1)) = 1
proof end;

theorem Th15: :: ABSVALUE:15
for b1 being real number holds abs (1 / b1) = 1 / (abs b1)
proof end;

Lemma7: for b1, b2 being real number holds abs (b1 / b2) = (abs b1) / (abs b2)
by COMPLEX1:153;

theorem Th16: :: ABSVALUE:16
canceled;

theorem Th17: :: ABSVALUE:17
canceled;

theorem Th18: :: ABSVALUE:18
canceled;

theorem Th19: :: ABSVALUE:19
canceled;

theorem Th20: :: ABSVALUE:20
for b1, b2 being real number st 0 <= b1 * b2 holds
sqrt (b1 * b2) = (sqrt (abs b1)) * (sqrt (abs b2))
proof end;

theorem Th21: :: ABSVALUE:21
for b1, b2, b3, b4 being real number st abs b1 <= b2 & abs b3 <= b4 holds
abs (b1 + b3) <= b2 + b4
proof end;

theorem Th22: :: ABSVALUE:22
canceled;

theorem Th23: :: ABSVALUE:23
for b1, b2 being real number st 0 < b1 / b2 holds
sqrt (b1 / b2) = (sqrt (abs b1)) / (sqrt (abs b2))
proof end;

theorem Th24: :: ABSVALUE:24
for b1, b2 being real number st 0 <= b1 * b2 holds
abs (b1 + b2) = (abs b1) + (abs b2)
proof end;

theorem Th25: :: ABSVALUE:25
for b1, b2 being real number st abs (b1 + b2) = (abs b1) + (abs b2) holds
0 <= b1 * b2
proof end;

theorem Th26: :: ABSVALUE:26
for b1, b2 being real number holds (abs (b1 + b2)) / (1 + (abs (b1 + b2))) <= ((abs b1) / (1 + (abs b1))) + ((abs b2) / (1 + (abs b2)))
proof end;

definition
let c1 be real number ;
func sgn c1 -> set equals :Def2: :: ABSVALUE:def 2
1 if 0 < a1
- 1 if a1 < 0
otherwise 0;
coherence
( ( 0 < c1 implies 1 is set ) & ( c1 < 0 implies - 1 is set ) & ( not 0 < c1 & not c1 < 0 implies 0 is set ) ) ;
consistency
for b1 being set st 0 < c1 & c1 < 0 holds
( b1 = 1 iff b1 = - 1 ) ;
end;

:: deftheorem Def2 defines sgn ABSVALUE:def 2 :
for b1 being real number holds
( ( 0 < b1 implies sgn b1 = 1 ) & ( b1 < 0 implies sgn b1 = - 1 ) & ( not 0 < b1 & not b1 < 0 implies sgn b1 = 0 ) );

registration
let c1 be real number ;
cluster sgn a1 -> real ;
coherence
sgn c1 is real
proof end;
end;

definition
let c1 be Real;
redefine func sgn as sgn c1 -> Real;
coherence
sgn c1 is Real by XREAL_0:def 1;
end;

theorem Th27: :: ABSVALUE:27
canceled;

theorem Th28: :: ABSVALUE:28
canceled;

theorem Th29: :: ABSVALUE:29
canceled;

theorem Th30: :: ABSVALUE:30
canceled;

theorem Th31: :: ABSVALUE:31
for b1 being real number st sgn b1 = 1 holds
0 < b1
proof end;

theorem Th32: :: ABSVALUE:32
for b1 being real number st sgn b1 = - 1 holds
b1 < 0
proof end;

theorem Th33: :: ABSVALUE:33
for b1 being real number st sgn b1 = 0 holds
b1 = 0
proof end;

theorem Th34: :: ABSVALUE:34
for b1 being real number holds b1 = (abs b1) * (sgn b1)
proof end;

theorem Th35: :: ABSVALUE:35
for b1, b2 being real number holds sgn (b1 * b2) = (sgn b1) * (sgn b2)
proof end;

theorem Th36: :: ABSVALUE:36
for b1 being real number holds sgn (sgn b1) = sgn b1
proof end;

theorem Th37: :: ABSVALUE:37
for b1, b2 being real number holds sgn (b1 + b2) <= ((sgn b1) + (sgn b2)) + 1
proof end;

theorem Th38: :: ABSVALUE:38
for b1 being real number st b1 <> 0 holds
(sgn b1) * (sgn (1 / b1)) = 1
proof end;

theorem Th39: :: ABSVALUE:39
for b1 being real number holds 1 / (sgn b1) = sgn (1 / b1)
proof end;

theorem Th40: :: ABSVALUE:40
for b1, b2 being real number holds ((sgn b1) + (sgn b2)) - 1 <= sgn (b1 + b2)
proof end;

theorem Th41: :: ABSVALUE:41
for b1 being real number holds sgn b1 = sgn (1 / b1)
proof end;

theorem Th42: :: ABSVALUE:42
for b1, b2 being real number holds sgn (b1 / b2) = (sgn b1) / (sgn b2)
proof end;