:: ABSVALUE semantic presentation begin definition let x be real number ; redefine func |.x.| equals :Def1: :: ABSVALUE:def 1 x if 0 <= x otherwise - x; correctness compatibility for b1 being set holds ( ( 0 <= x implies ( b1 = |.x.| iff b1 = x ) ) & ( not 0 <= x implies ( b1 = |.x.| iff b1 = - x ) ) ); consistency for b1 being set holds verum; by COMPLEX1:43, COMPLEX1:70; end; :: deftheorem Def1 defines |. ABSVALUE:def_1_:_ for x being real number holds ( ( 0 <= x implies |.x.| = x ) & ( not 0 <= x implies |.x.| = - x ) ); theorem :: ABSVALUE:1 for x being real number holds ( abs x = x or abs x = - x ) by Def1; theorem Th2: :: ABSVALUE:2 for x being real number holds ( x = 0 iff abs x = 0 ) by Def1, COMPLEX1:47; theorem :: ABSVALUE:3 for x being real number st abs x = - x & x <> 0 holds x < 0 by Def1; theorem :: ABSVALUE:4 for x being real number holds ( - (abs x) <= x & x <= abs x ) proof let x be real number ; ::_thesis: ( - (abs x) <= x & x <= abs x ) percases ( x < 0 or 0 <= x ) ; supposeA1: x < 0 ; ::_thesis: ( - (abs x) <= x & x <= abs x ) then abs x = - x by Def1; hence ( - (abs x) <= x & x <= abs x ) by A1; ::_thesis: verum end; supposeA2: 0 <= x ; ::_thesis: ( - (abs x) <= x & x <= abs x ) then - x <= - 0 ; hence ( - (abs x) <= x & x <= abs x ) by A2, Def1; ::_thesis: verum end; end; end; theorem :: ABSVALUE:5 for y, x being real number holds ( ( - y <= x & x <= y ) iff abs x <= y ) proof let y, x be real number ; ::_thesis: ( ( - y <= x & x <= y ) iff abs x <= y ) hereby ::_thesis: ( abs x <= y implies ( - y <= x & x <= y ) ) assume that A1: - y <= x and A2: x <= y ; ::_thesis: abs x <= y - x <= - (- y) by A1, XREAL_1:24; hence abs x <= y by A2, Def1; ::_thesis: verum end; assume A3: abs x <= y ; ::_thesis: ( - y <= x & x <= y ) then A4: 0 <= y by COMPLEX1:46; percases ( 0 < x or x < 0 or x = - 0 ) ; suppose 0 < x ; ::_thesis: ( - y <= x & x <= y ) hence ( - y <= x & x <= y ) by A3, A4, Def1; ::_thesis: verum end; supposeA5: x < 0 ; ::_thesis: ( - y <= x & x <= y ) then - x <= y by A3, Def1; then - y <= - (- x) by XREAL_1:24; hence ( - y <= x & x <= y ) by A5; ::_thesis: verum end; suppose x = - 0 ; ::_thesis: ( - y <= x & x <= y ) hence ( - y <= x & x <= y ) by A4; ::_thesis: verum end; end; end; theorem :: ABSVALUE:6 for x being real number st x <> 0 holds (abs x) * (abs (1 / x)) = 1 proof let x be real number ; ::_thesis: ( x <> 0 implies (abs x) * (abs (1 / x)) = 1 ) assume x <> 0 ; ::_thesis: (abs x) * (abs (1 / x)) = 1 then ( (abs x) * (abs (1 / x)) = abs (x * (1 / x)) & abs (x * (1 / x)) = abs 1 ) by COMPLEX1:65, XCMPLX_1:106; hence (abs x) * (abs (1 / x)) = 1 by Def1; ::_thesis: verum end; theorem :: ABSVALUE:7 for x being real number holds abs (1 / x) = 1 / (abs x) by COMPLEX1:80; theorem :: ABSVALUE:8 for x, y being real number st 0 <= x * y holds sqrt (x * y) = (sqrt (abs x)) * (sqrt (abs y)) proof let x, y be real number ; ::_thesis: ( 0 <= x * y implies sqrt (x * y) = (sqrt (abs x)) * (sqrt (abs y)) ) assume 0 <= x * y ; ::_thesis: sqrt (x * y) = (sqrt (abs x)) * (sqrt (abs y)) then abs (x * y) = x * y by Def1; then A1: (abs x) * (abs y) = x * y by COMPLEX1:65; ( 0 <= abs x & 0 <= abs y ) by COMPLEX1:46; hence sqrt (x * y) = (sqrt (abs x)) * (sqrt (abs y)) by A1, SQUARE_1:29; ::_thesis: verum end; theorem :: ABSVALUE:9 for x, z, y, t being real number st abs x <= z & abs y <= t holds abs (x + y) <= z + t proof let x, z, y, t be real number ; ::_thesis: ( abs x <= z & abs y <= t implies abs (x + y) <= z + t ) assume ( abs x <= z & abs y <= t ) ; ::_thesis: abs (x + y) <= z + t then ( abs (x + y) <= (abs x) + (abs y) & (abs x) + (abs y) <= z + t ) by COMPLEX1:56, XREAL_1:7; hence abs (x + y) <= z + t by XXREAL_0:2; ::_thesis: verum end; theorem :: ABSVALUE:10 for x, y being real number st 0 < x / y holds sqrt (x / y) = (sqrt (abs x)) / (sqrt (abs y)) proof let x, y be real number ; ::_thesis: ( 0 < x / y implies sqrt (x / y) = (sqrt (abs x)) / (sqrt (abs y)) ) assume 0 < x / y ; ::_thesis: sqrt (x / y) = (sqrt (abs x)) / (sqrt (abs y)) then x / y = abs (x / y) by Def1; then A1: x / y = (abs x) / (abs y) by COMPLEX1:67; ( 0 <= abs x & 0 <= abs y ) by COMPLEX1:46; hence sqrt (x / y) = (sqrt (abs x)) / (sqrt (abs y)) by A1, SQUARE_1:30; ::_thesis: verum end; theorem :: ABSVALUE:11 for x, y being real number st 0 <= x * y holds abs (x + y) = (abs x) + (abs y) proof let x, y be real number ; ::_thesis: ( 0 <= x * y implies abs (x + y) = (abs x) + (abs y) ) assume A1: 0 <= x * y ; ::_thesis: abs (x + y) = (abs x) + (abs y) percases ( x * y = 0 or 0 < x * y ) by A1; supposeA2: x * y = 0 ; ::_thesis: abs (x + y) = (abs x) + (abs y) percases ( x = 0 or y = 0 ) by A2, XCMPLX_1:6; supposeA3: x = 0 ; ::_thesis: abs (x + y) = (abs x) + (abs y) then (abs x) + (abs y) = 0 + (abs y) by Def1 .= abs y ; hence abs (x + y) = (abs x) + (abs y) by A3; ::_thesis: verum end; supposeA4: y = 0 ; ::_thesis: abs (x + y) = (abs x) + (abs y) then (abs x) + (abs y) = (abs x) + 0 by Def1 .= abs x ; hence abs (x + y) = (abs x) + (abs y) by A4; ::_thesis: verum end; end; end; supposeA5: 0 < x * y ; ::_thesis: abs (x + y) = (abs x) + (abs y) then A6: ( x <> 0 & y <> 0 ) ; percases ( ( 0 < x & 0 < y ) or ( x < 0 & y < 0 ) ) by A5, A6; supposeA7: ( 0 < x & 0 < y ) ; ::_thesis: abs (x + y) = (abs x) + (abs y) ( abs x = x & abs y = y ) by A7, Def1; hence abs (x + y) = (abs x) + (abs y) by A7, Def1; ::_thesis: verum end; supposethat A8: x < 0 and A9: y < 0 ; ::_thesis: abs (x + y) = (abs x) + (abs y) abs x = - x by A8, Def1; then (abs x) + (abs y) = ((- 1) * x) + (- (1 * y)) by A9, Def1 .= - (x + y) ; hence abs (x + y) = (abs x) + (abs y) by A8, A9, Def1; ::_thesis: verum end; end; end; end; end; theorem :: ABSVALUE:12 for x, y being real number st abs (x + y) = (abs x) + (abs y) holds 0 <= x * y proof let x, y be real number ; ::_thesis: ( abs (x + y) = (abs x) + (abs y) implies 0 <= x * y ) A1: ( not x * y < 0 or ( x < 0 & 0 < y ) or ( 0 < x & y < 0 ) ) proof assume A2: x * y < 0 ; ::_thesis: ( ( x < 0 & 0 < y ) or ( 0 < x & y < 0 ) ) then ( x <> 0 & y <> 0 ) ; hence ( ( x < 0 & 0 < y ) or ( 0 < x & y < 0 ) ) by A2; ::_thesis: verum end; A3: ( x < 0 & 0 < y & x + y < 0 implies abs (x + y) <> (abs x) + (abs y) ) proof assume that A4: x < 0 and A5: 0 < y and A6: x + y < 0 ; ::_thesis: abs (x + y) <> (abs x) + (abs y) (- (1 * x)) + (- y) < (- x) + y by A5, XREAL_1:6; then A7: - (1 * (x + y)) < (- x) + y ; ( abs x = - x & abs y = y ) by A4, A5, Def1; hence abs (x + y) <> (abs x) + (abs y) by A6, A7, Def1; ::_thesis: verum end; A8: ( 0 < x & y < 0 & x + y < 0 implies abs (x + y) <> (abs x) + (abs y) ) proof assume that A9: 0 < x and A10: y < 0 and A11: x + y < 0 ; ::_thesis: abs (x + y) <> (abs x) + (abs y) (- (1 * x)) + (- y) < x + (- y) by A9, XREAL_1:6; then A12: - (1 * (x + y)) < x + (- y) ; ( abs x = x & abs y = - y ) by A9, A10, Def1; hence abs (x + y) <> (abs x) + (abs y) by A11, A12, Def1; ::_thesis: verum end; A13: ( 0 < x & y < 0 & 0 <= x + y implies abs (x + y) <> (abs x) + (abs y) ) proof assume that A14: 0 < x and A15: y < 0 and A16: 0 <= x + y ; ::_thesis: abs (x + y) <> (abs x) + (abs y) A17: abs y = - y by A15, Def1; ( x + y < x + (- y) & abs x = x ) by A14, A15, Def1, XREAL_1:6; hence abs (x + y) <> (abs x) + (abs y) by A16, A17, Def1; ::_thesis: verum end; A18: ( x < 0 & 0 < y & 0 <= x + y implies abs (x + y) <> (abs x) + (abs y) ) proof assume that A19: x < 0 and A20: 0 < y and A21: 0 <= x + y ; ::_thesis: abs (x + y) <> (abs x) + (abs y) A22: abs y = y by A20, Def1; ( x + y < (- x) + y & abs x = - x ) by A19, Def1, XREAL_1:6; hence abs (x + y) <> (abs x) + (abs y) by A21, A22, Def1; ::_thesis: verum end; assume ( abs (x + y) = (abs x) + (abs y) & 0 > x * y ) ; ::_thesis: contradiction hence contradiction by A1, A3, A18, A8, A13; ::_thesis: verum end; theorem :: ABSVALUE:13 for x, y being real number holds (abs (x + y)) / (1 + (abs (x + y))) <= ((abs x) / (1 + (abs x))) + ((abs y) / (1 + (abs y))) proof let x, y be real number ; ::_thesis: (abs (x + y)) / (1 + (abs (x + y))) <= ((abs x) / (1 + (abs x))) + ((abs y) / (1 + (abs y))) A1: for s, t being real number st s <= t & 0 < 1 + s & 0 < 1 + t holds s / (1 + s) <= t / (1 + t) proof let s, t be real number ; ::_thesis: ( s <= t & 0 < 1 + s & 0 < 1 + t implies s / (1 + s) <= t / (1 + t) ) assume that A2: s <= t and A3: 0 < 1 + s and A4: 0 < 1 + t ; ::_thesis: s / (1 + s) <= t / (1 + t) (s * 1) + (s * t) <= t + (s * t) by A2, XREAL_1:6; then (s * (1 + t)) * ((1 + s) ") <= (t * (1 + s)) * ((1 + s) ") by A3, XREAL_1:64; then (s * (1 + t)) * ((1 + s) ") <= t * ((1 + s) * ((1 + s) ")) ; then (s * (1 + t)) * ((1 + s) ") <= t * 1 by A3, XCMPLX_0:def_7; then ((s * ((1 + s) ")) * (1 + t)) * ((1 + t) ") <= t * ((1 + t) ") by A4, XREAL_1:64; then (s * ((1 + s) ")) * ((1 + t) * ((1 + t) ")) <= t * ((1 + t) ") ; then (s * ((1 + s) ")) * 1 <= t * ((1 + t) ") by A4, XCMPLX_0:def_7; then s / (1 + s) <= t * ((1 + t) ") by XCMPLX_0:def_9; hence s / (1 + s) <= t / (1 + t) by XCMPLX_0:def_9; ::_thesis: verum end; set a = abs x; set b = abs y; set c = abs (x + y); A5: 0 <= abs x by COMPLEX1:46; A6: 0 <= abs y by COMPLEX1:46; A7: 0 + 0 < 1 + (abs x) by COMPLEX1:46, XREAL_1:8; A8: ( 0 < 1 + (abs x) & 0 < (1 + (abs x)) + (abs y) implies (abs x) / ((1 + (abs x)) + (abs y)) <= (abs x) / (1 + (abs x)) ) proof assume that A9: 0 < 1 + (abs x) and A10: 0 < (1 + (abs x)) + (abs y) ; ::_thesis: (abs x) / ((1 + (abs x)) + (abs y)) <= (abs x) / (1 + (abs x)) 0 + (abs x) <= ((abs x) * (abs y)) + (abs x) by A5, A6, XREAL_1:6; then ((abs x) * 1) + ((abs x) * (abs x)) <= ((abs x) * (1 + (abs y))) + ((abs x) * (abs x)) by XREAL_1:6; then ((abs x) * (1 + (abs x))) * ((1 + (abs x)) ") <= ((abs x) * ((1 + (abs x)) + (abs y))) * ((1 + (abs x)) ") by A9, XREAL_1:64; then (abs x) * ((1 + (abs x)) * ((1 + (abs x)) ")) <= ((abs x) * ((1 + (abs x)) + (abs y))) * ((1 + (abs x)) ") ; then (abs x) * 1 <= ((abs x) * ((1 + (abs x)) + (abs y))) * ((1 + (abs x)) ") by A7, XCMPLX_0:def_7; then (abs x) * (((1 + (abs x)) + (abs y)) ") <= (((abs x) * ((1 + (abs x)) ")) * ((1 + (abs x)) + (abs y))) * (((1 + (abs x)) + (abs y)) ") by A10, XREAL_1:64; then (abs x) * (((1 + (abs x)) + (abs y)) ") <= ((abs x) * ((1 + (abs x)) ")) * (((1 + (abs x)) + (abs y)) * (((1 + (abs x)) + (abs y)) ")) ; then (abs x) * (((1 + (abs x)) + (abs y)) ") <= ((abs x) * ((1 + (abs x)) ")) * 1 by A5, A6, XCMPLX_0:def_7; then (abs x) / ((1 + (abs x)) + (abs y)) <= (abs x) * ((1 + (abs x)) ") by XCMPLX_0:def_9; hence (abs x) / ((1 + (abs x)) + (abs y)) <= (abs x) / (1 + (abs x)) by XCMPLX_0:def_9; ::_thesis: verum end; A11: 0 + 0 < 1 + (abs y) by COMPLEX1:46, XREAL_1:8; A12: ( 0 < 1 + (abs y) & 0 < (1 + (abs x)) + (abs y) implies (abs y) / ((1 + (abs x)) + (abs y)) <= (abs y) / (1 + (abs y)) ) proof assume that A13: 0 < 1 + (abs y) and A14: 0 < (1 + (abs x)) + (abs y) ; ::_thesis: (abs y) / ((1 + (abs x)) + (abs y)) <= (abs y) / (1 + (abs y)) 0 + (abs y) <= ((abs x) * (abs y)) + (abs y) by A5, A6, XREAL_1:6; then ((abs y) * 1) + ((abs y) * (abs y)) <= ((1 + (abs x)) * (abs y)) + ((abs y) * (abs y)) by XREAL_1:6; then ((abs y) * (1 + (abs y))) * ((1 + (abs y)) ") <= ((abs y) * ((1 + (abs x)) + (abs y))) * ((1 + (abs y)) ") by A13, XREAL_1:64; then (abs y) * ((1 + (abs y)) * ((1 + (abs y)) ")) <= ((abs y) * ((1 + (abs x)) + (abs y))) * ((1 + (abs y)) ") ; then (abs y) * 1 <= ((abs y) * ((1 + (abs x)) + (abs y))) * ((1 + (abs y)) ") by A11, XCMPLX_0:def_7; then (abs y) * (((1 + (abs x)) + (abs y)) ") <= (((abs y) * ((1 + (abs y)) ")) * ((1 + (abs x)) + (abs y))) * (((1 + (abs x)) + (abs y)) ") by A14, XREAL_1:64; then (abs y) * (((1 + (abs x)) + (abs y)) ") <= ((abs y) * ((1 + (abs y)) ")) * (((1 + (abs x)) + (abs y)) * (((1 + (abs x)) + (abs y)) ")) ; then (abs y) * (((1 + (abs x)) + (abs y)) ") <= ((abs y) * ((1 + (abs y)) ")) * 1 by A5, A6, XCMPLX_0:def_7; then (abs y) / ((1 + (abs x)) + (abs y)) <= (abs y) * ((1 + (abs y)) ") by XCMPLX_0:def_9; hence (abs y) / ((1 + (abs x)) + (abs y)) <= (abs y) / (1 + (abs y)) by XCMPLX_0:def_9; ::_thesis: verum end; 0 + 0 < 1 + (abs (x + y)) by COMPLEX1:46, XREAL_1:8; then A15: (abs (x + y)) / (1 + (abs (x + y))) <= ((abs x) + (abs y)) / (1 + ((abs x) + (abs y))) by A5, A6, A1, COMPLEX1:56; ((abs x) + (abs y)) / ((1 + (abs x)) + (abs y)) = ((abs x) / ((1 + (abs x)) + (abs y))) + ((abs y) / ((1 + (abs x)) + (abs y))) by XCMPLX_1:62; then ((abs x) + (abs y)) / ((1 + (abs x)) + (abs y)) <= ((abs x) / (1 + (abs x))) + ((abs y) / (1 + (abs y))) by A6, A7, A8, A12, XREAL_1:7; hence (abs (x + y)) / (1 + (abs (x + y))) <= ((abs x) / (1 + (abs x))) + ((abs y) / (1 + (abs y))) by A15, XXREAL_0:2; ::_thesis: verum end; definition let x be real number ; func sgn x -> real number equals :Def2: :: ABSVALUE:def 2 1 if 0 < x - 1 if x < 0 otherwise 0 ; coherence ( ( 0 < x implies 1 is real number ) & ( x < 0 implies - 1 is real number ) & ( not 0 < x & not x < 0 implies 0 is real number ) ) ; consistency for b1 being real number st 0 < x & x < 0 holds ( b1 = 1 iff b1 = - 1 ) ; projectivity for b1, b2 being real number st ( 0 < b2 implies b1 = 1 ) & ( b2 < 0 implies b1 = - 1 ) & ( not 0 < b2 & not b2 < 0 implies b1 = 0 ) holds ( ( 0 < b1 implies b1 = 1 ) & ( b1 < 0 implies b1 = - 1 ) & ( not 0 < b1 & not b1 < 0 implies b1 = 0 ) ) ; end; :: deftheorem Def2 defines sgn ABSVALUE:def_2_:_ for x being real number holds ( ( 0 < x implies sgn x = 1 ) & ( x < 0 implies sgn x = - 1 ) & ( not 0 < x & not x < 0 implies sgn x = 0 ) ); registration let x be real number ; cluster sgn x -> real integer ; coherence sgn x is integer proof ( x = 0 or x > 0 or x < 0 ) ; hence sgn x is integer by Def2; ::_thesis: verum end; end; definition let x be Real; :: original: sgn redefine func sgn x -> Real; coherence sgn x is Real by XREAL_0:def_1; end; theorem :: ABSVALUE:14 for x being real number st sgn x = 1 holds 0 < x proof let x be real number ; ::_thesis: ( sgn x = 1 implies 0 < x ) assume that A1: sgn x = 1 and A2: 0 >= x ; ::_thesis: contradiction ( x < 0 or x = 0 ) by A2; hence contradiction by A1, Def2; ::_thesis: verum end; theorem :: ABSVALUE:15 for x being real number st sgn x = - 1 holds x < 0 proof let x be real number ; ::_thesis: ( sgn x = - 1 implies x < 0 ) assume that A1: sgn x = - 1 and A2: x >= 0 ; ::_thesis: contradiction ( 0 < x or x = 0 ) by A2; hence contradiction by A1, Def2; ::_thesis: verum end; theorem Th16: :: ABSVALUE:16 for x being real number st sgn x = 0 holds x = 0 proof let x be real number ; ::_thesis: ( sgn x = 0 implies x = 0 ) assume that A1: sgn x = 0 and A2: x <> 0 ; ::_thesis: contradiction ( 0 < x or x < 0 ) by A2; hence contradiction by A1, Def2; ::_thesis: verum end; theorem :: ABSVALUE:17 for x being real number holds x = (abs x) * (sgn x) proof let x be real number ; ::_thesis: x = (abs x) * (sgn x) A1: ( 0 < x implies x = (abs x) * (sgn x) ) proof assume A2: 0 < x ; ::_thesis: x = (abs x) * (sgn x) then abs x = x by Def1; then (abs x) * (sgn x) = x * 1 by A2, Def2; hence x = (abs x) * (sgn x) ; ::_thesis: verum end; A3: ( x < 0 implies x = (abs x) * (sgn x) ) proof assume A4: x < 0 ; ::_thesis: x = (abs x) * (sgn x) then abs x = - x by Def1; then (abs x) * (sgn x) = (- x) * (- 1) by A4, Def2 .= x ; hence x = (abs x) * (sgn x) ; ::_thesis: verum end; ( x = 0 implies x = (abs x) * (sgn x) ) proof assume A5: x = 0 ; ::_thesis: x = (abs x) * (sgn x) then sgn x = 0 by Def2; hence x = (abs x) * (sgn x) by A5; ::_thesis: verum end; hence x = (abs x) * (sgn x) by A1, A3; ::_thesis: verum end; theorem Th18: :: ABSVALUE:18 for x, y being real number holds sgn (x * y) = (sgn x) * (sgn y) proof let x, y be real number ; ::_thesis: sgn (x * y) = (sgn x) * (sgn y) A1: ( 0 < x & 0 < y implies sgn (x * y) = (sgn x) * (sgn y) ) proof assume that A2: 0 < x and A3: 0 < y ; ::_thesis: sgn (x * y) = (sgn x) * (sgn y) A4: sgn y = 1 by A3, Def2; ( 0 * y < x * y & sgn x = 1 ) by A2, A3, Def2, XREAL_1:68; hence sgn (x * y) = (sgn x) * (sgn y) by A4, Def2; ::_thesis: verum end; A5: ( 0 < x & y < 0 implies sgn (x * y) = (sgn x) * (sgn y) ) proof assume that A6: 0 < x and A7: y < 0 ; ::_thesis: sgn (x * y) = (sgn x) * (sgn y) sgn y = - 1 by A7, Def2; then A8: (sgn x) * (sgn y) = 1 * (- 1) by A6, Def2 .= - 1 ; x * y < 0 * y by A6, A7, XREAL_1:69; hence sgn (x * y) = (sgn x) * (sgn y) by A8, Def2; ::_thesis: verum end; A9: ( x < 0 & y < 0 implies sgn (x * y) = (sgn x) * (sgn y) ) proof assume that A10: x < 0 and A11: y < 0 ; ::_thesis: sgn (x * y) = (sgn x) * (sgn y) sgn y = - 1 by A11, Def2; then A12: (sgn x) * (sgn y) = (- 1) * (- 1) by A10, Def2 .= 1 ; x * 0 < x * y by A10, A11, XREAL_1:69; hence sgn (x * y) = (sgn x) * (sgn y) by A12, Def2; ::_thesis: verum end; A13: ( x < 0 & 0 < y implies sgn (x * y) = (sgn x) * (sgn y) ) proof assume that A14: x < 0 and A15: 0 < y ; ::_thesis: sgn (x * y) = (sgn x) * (sgn y) sgn y = 1 by A15, Def2; then A16: (sgn x) * (sgn y) = - 1 by A14, Def2; x * y < 0 * y by A14, A15, XREAL_1:68; hence sgn (x * y) = (sgn x) * (sgn y) by A16, Def2; ::_thesis: verum end; ( ( x = 0 or y = 0 ) implies sgn (x * y) = (sgn x) * (sgn y) ) proof assume A17: ( x = 0 or y = 0 ) ; ::_thesis: sgn (x * y) = (sgn x) * (sgn y) then ( sgn x = 0 or sgn y = 0 ) by Def2; hence sgn (x * y) = (sgn x) * (sgn y) by A17; ::_thesis: verum end; hence sgn (x * y) = (sgn x) * (sgn y) by A1, A5, A13, A9; ::_thesis: verum end; theorem :: ABSVALUE:19 canceled; theorem :: ABSVALUE:20 for x, y being real number holds sgn (x + y) <= ((sgn x) + (sgn y)) + 1 proof let x, y be real number ; ::_thesis: sgn (x + y) <= ((sgn x) + (sgn y)) + 1 A1: ( y = 0 implies sgn (x + y) <= ((sgn x) + (sgn y)) + 1 ) proof assume A2: y = 0 ; ::_thesis: sgn (x + y) <= ((sgn x) + (sgn y)) + 1 then ((sgn x) + (sgn y)) + 1 = ((sgn x) + 0) + 1 by Def2 .= (sgn x) + 1 ; hence sgn (x + y) <= ((sgn x) + (sgn y)) + 1 by A2, XREAL_1:29; ::_thesis: verum end; A3: ( 0 < x & 0 < y implies sgn (x + y) <= ((sgn x) + (sgn y)) + 1 ) proof sgn x < (sgn x) + 1 by XREAL_1:29; then A4: (sgn x) + 0 < ((sgn x) + 1) + 1 by XREAL_1:8; assume A5: ( 0 < x & 0 < y ) ; ::_thesis: sgn (x + y) <= ((sgn x) + (sgn y)) + 1 then ( sgn x = 1 & sgn y = 1 ) by Def2; hence sgn (x + y) <= ((sgn x) + (sgn y)) + 1 by A5, A4, Def2; ::_thesis: verum end; A6: ( x < 0 & 0 < y implies sgn (x + y) <= ((sgn x) + (sgn y)) + 1 ) proof assume that A7: x < 0 and A8: 0 < y ; ::_thesis: sgn (x + y) <= ((sgn x) + (sgn y)) + 1 sgn x = - 1 by A7, Def2; then A9: ((sgn x) + (sgn y)) + 1 = 1 by A8, Def2; ( x + y < 0 or x + y = 0 or 0 < x + y ) ; hence sgn (x + y) <= ((sgn x) + (sgn y)) + 1 by A9, Def2; ::_thesis: verum end; A10: ( 0 < x & y < 0 implies sgn (x + y) <= ((sgn x) + (sgn y)) + 1 ) proof assume that A11: 0 < x and A12: y < 0 ; ::_thesis: sgn (x + y) <= ((sgn x) + (sgn y)) + 1 sgn x = 1 by A11, Def2; then A13: ((sgn x) + (sgn y)) + 1 = (1 + (- 1)) + 1 by A12, Def2 .= 1 ; ( x + y < 0 or x + y = 0 or 0 < x + y ) ; hence sgn (x + y) <= ((sgn x) + (sgn y)) + 1 by A13, Def2; ::_thesis: verum end; A14: ( x < 0 & y < 0 implies sgn (x + y) <= ((sgn x) + (sgn y)) + 1 ) proof assume that A15: x < 0 and A16: y < 0 ; ::_thesis: sgn (x + y) <= ((sgn x) + (sgn y)) + 1 sgn y = - 1 by A16, Def2; then ((sgn x) + (sgn y)) + 1 = - 1 by A15, Def2; hence sgn (x + y) <= ((sgn x) + (sgn y)) + 1 by A15, A16, Def2; ::_thesis: verum end; ( x = 0 implies sgn (x + y) <= ((sgn x) + (sgn y)) + 1 ) proof assume A17: x = 0 ; ::_thesis: sgn (x + y) <= ((sgn x) + (sgn y)) + 1 then ((sgn x) + (sgn y)) + 1 = (0 + (sgn y)) + 1 by Def2 .= (sgn y) + 1 ; hence sgn (x + y) <= ((sgn x) + (sgn y)) + 1 by A17, XREAL_1:29; ::_thesis: verum end; hence sgn (x + y) <= ((sgn x) + (sgn y)) + 1 by A3, A10, A6, A14, A1; ::_thesis: verum end; theorem Th21: :: ABSVALUE:21 for x being real number st x <> 0 holds (sgn x) * (sgn (1 / x)) = 1 proof let x be real number ; ::_thesis: ( x <> 0 implies (sgn x) * (sgn (1 / x)) = 1 ) assume x <> 0 ; ::_thesis: (sgn x) * (sgn (1 / x)) = 1 then sgn (x * (1 / x)) = sgn 1 by XCMPLX_1:106; then sgn (x * (1 / x)) = 1 by Def2; hence (sgn x) * (sgn (1 / x)) = 1 by Th18; ::_thesis: verum end; theorem Th22: :: ABSVALUE:22 for x being real number holds 1 / (sgn x) = sgn (1 / x) proof let x be real number ; ::_thesis: 1 / (sgn x) = sgn (1 / x) percases ( x = 0 or x <> 0 ) ; supposeA1: x = 0 ; ::_thesis: 1 / (sgn x) = sgn (1 / x) hence 1 / (sgn x) = 1 / 0 by Def2 .= sgn (1 / x) by A1, Def2 ; ::_thesis: verum end; supposeA2: x <> 0 ; ::_thesis: 1 / (sgn x) = sgn (1 / x) then ((sgn x) * (sgn (1 / x))) * (1 / (sgn x)) = 1 * (1 / (sgn x)) by Th21; then (sgn (1 / x)) * ((sgn x) * (1 / (sgn x))) = 1 / (sgn x) ; then (sgn (1 / x)) * 1 = 1 / (sgn x) by A2, Th16, XCMPLX_1:106; hence 1 / (sgn x) = sgn (1 / x) ; ::_thesis: verum end; end; end; theorem :: ABSVALUE:23 for x, y being real number holds ((sgn x) + (sgn y)) - 1 <= sgn (x + y) proof let x, y be real number ; ::_thesis: ((sgn x) + (sgn y)) - 1 <= sgn (x + y) A1: ( ( x = 0 or y = 0 ) implies ((sgn x) + (sgn y)) - 1 <= sgn (x + y) ) proof A2: ( y = 0 implies ((sgn x) + (sgn y)) - 1 <= sgn (x + y) ) proof A3: (sgn x) - 1 < ((sgn x) + (- 1)) + 1 by XREAL_1:29; assume A4: y = 0 ; ::_thesis: ((sgn x) + (sgn y)) - 1 <= sgn (x + y) then ((sgn x) + (sgn y)) - 1 = ((sgn x) + 0) - 1 by Def2 .= (sgn x) - 1 ; hence ((sgn x) + (sgn y)) - 1 <= sgn (x + y) by A4, A3; ::_thesis: verum end; A5: ( x = 0 implies ((sgn x) + (sgn y)) - 1 <= sgn (x + y) ) proof A6: (sgn y) - 1 < ((sgn y) + (- 1)) + 1 by XREAL_1:29; assume A7: x = 0 ; ::_thesis: ((sgn x) + (sgn y)) - 1 <= sgn (x + y) then ((sgn x) + (sgn y)) - 1 = (0 + (sgn y)) - 1 by Def2 .= (sgn y) - 1 ; hence ((sgn x) + (sgn y)) - 1 <= sgn (x + y) by A7, A6; ::_thesis: verum end; assume ( x = 0 or y = 0 ) ; ::_thesis: ((sgn x) + (sgn y)) - 1 <= sgn (x + y) hence ((sgn x) + (sgn y)) - 1 <= sgn (x + y) by A5, A2; ::_thesis: verum end; A8: ( x < 0 & y < 0 implies ((sgn x) + (sgn y)) - 1 <= sgn (x + y) ) proof assume that A9: x < 0 and A10: y < 0 ; ::_thesis: ((sgn x) + (sgn y)) - 1 <= sgn (x + y) sgn x = - 1 by A9, Def2; then A11: sgn x = sgn (x + y) by A9, A10, Def2; A12: ( ((sgn (x + y)) + (- 1)) - 1 < (((sgn (x + y)) + (- 1)) - 1) + 1 & (sgn (x + y)) + (- 1) < ((sgn (x + y)) + (- 1)) + 1 ) by XREAL_1:29; sgn y = - 1 by A10, Def2; hence ((sgn x) + (sgn y)) - 1 <= sgn (x + y) by A11, A12, XXREAL_0:2; ::_thesis: verum end; A13: ( 0 < x & y < 0 implies ((sgn x) + (sgn y)) - 1 <= sgn (x + y) ) proof assume that A14: 0 < x and A15: y < 0 ; ::_thesis: ((sgn x) + (sgn y)) - 1 <= sgn (x + y) sgn x = 1 by A14, Def2; then A16: (sgn x) + (sgn y) = 1 + (- 1) by A15, Def2 .= 0 ; ( x + y < 0 or x + y = 0 or 0 < x + y ) ; hence ((sgn x) + (sgn y)) - 1 <= sgn (x + y) by A16, Def2; ::_thesis: verum end; A17: ( x < 0 & 0 < y implies ((sgn x) + (sgn y)) - 1 <= sgn (x + y) ) proof assume that A18: x < 0 and A19: 0 < y ; ::_thesis: ((sgn x) + (sgn y)) - 1 <= sgn (x + y) sgn x = - 1 by A18, Def2; then A20: (sgn x) + (sgn y) = (- 1) + 1 by A19, Def2 .= 0 ; ( x + y < 0 or x + y = 0 or 0 < x + y ) ; hence ((sgn x) + (sgn y)) - 1 <= sgn (x + y) by A20, Def2; ::_thesis: verum end; ( 0 < x & 0 < y implies ((sgn x) + (sgn y)) - 1 <= sgn (x + y) ) proof assume that A21: 0 < x and A22: 0 < y ; ::_thesis: ((sgn x) + (sgn y)) - 1 <= sgn (x + y) sgn y = 1 by A22, Def2; then ((sgn x) + (sgn y)) - 1 = 1 by A21, Def2; hence ((sgn x) + (sgn y)) - 1 <= sgn (x + y) by A21, A22, Def2; ::_thesis: verum end; hence ((sgn x) + (sgn y)) - 1 <= sgn (x + y) by A8, A17, A13, A1; ::_thesis: verum end; theorem :: ABSVALUE:24 for x being real number holds sgn x = sgn (1 / x) proof let x be real number ; ::_thesis: sgn x = sgn (1 / x) A1: ( 0 < x implies sgn x = sgn (1 / x) ) proof assume A2: 0 < x ; ::_thesis: sgn x = sgn (1 / x) sgn (1 / x) = 1 / (sgn x) by Th22; then sgn (1 / x) = 1 / 1 by A2, Def2 .= 1 ; hence sgn x = sgn (1 / x) by A2, Def2; ::_thesis: verum end; ( x < 0 implies sgn x = sgn (1 / x) ) proof assume A3: x < 0 ; ::_thesis: sgn x = sgn (1 / x) then sgn x = - 1 by Def2; then sgn (1 / x) = 1 / (- 1) by Th22; hence sgn x = sgn (1 / x) by A3, Def2; ::_thesis: verum end; hence sgn x = sgn (1 / x) by A1; ::_thesis: verum end; theorem :: ABSVALUE:25 for x, y being real number holds sgn (x / y) = (sgn x) / (sgn y) proof let x, y be real number ; ::_thesis: sgn (x / y) = (sgn x) / (sgn y) percases ( y = 0 or y <> 0 ) ; supposeA1: y = 0 ; ::_thesis: sgn (x / y) = (sgn x) / (sgn y) hence sgn (x / y) = sgn (x * (0 ")) by XCMPLX_0:def_9 .= (sgn x) * (0 ") by Def2 .= (sgn x) / 0 by XCMPLX_0:def_9 .= (sgn x) / (sgn y) by A1, Def2 ; ::_thesis: verum end; supposeA2: y <> 0 ; ::_thesis: sgn (x / y) = (sgn x) / (sgn y) x / y = (x / y) * 1 .= (x / y) * (y * (1 / y)) by A2, XCMPLX_1:106 .= ((x / y) * y) * (1 / y) .= x * (1 / y) by A2, XCMPLX_1:87 ; then sgn (x / y) = (sgn x) * (sgn (1 / y)) by Th18 .= ((sgn x) / 1) * (1 / (sgn y)) by Th22 .= ((sgn x) * 1) / (1 * (sgn y)) by XCMPLX_1:76 .= (sgn x) / (1 * (sgn y)) ; hence sgn (x / y) = (sgn x) / (sgn y) ; ::_thesis: verum end; end; end; theorem :: ABSVALUE:26 for r being real number holds 0 <= r + (abs r) proof let r be real number ; ::_thesis: 0 <= r + (abs r) A1: 0 <= abs r by COMPLEX1:46; ( (abs r) + (abs r) = r + (abs r) or (abs r) + r = (- r) + r ) by Def1; hence 0 <= r + (abs r) by A1; ::_thesis: verum end; theorem :: ABSVALUE:27 for r being real number holds 0 <= (- r) + (abs r) proof let r be real number ; ::_thesis: 0 <= (- r) + (abs r) r <= abs r by COMPLEX1:76; then - r >= - (abs r) by XREAL_1:24; then (- r) + (abs r) >= (- (abs r)) + (abs r) by XREAL_1:7; hence 0 <= (- r) + (abs r) ; ::_thesis: verum end; theorem :: ABSVALUE:28 for r, s being real number holds ( not abs r = abs s or r = s or r = - s ) proof let r, s be real number ; ::_thesis: ( not abs r = abs s or r = s or r = - s ) assume A1: abs r = abs s ; ::_thesis: ( r = s or r = - s ) assume A2: r <> s ; ::_thesis: r = - s percases ( ( abs r = r & abs s = s ) or ( abs r = r & abs s = - s ) or ( abs r = - r & abs s = s ) or ( abs r = - r & abs s = - s ) ) by Def1; suppose ( abs r = r & abs s = s ) ; ::_thesis: r = - s hence r = - s by A1, A2; ::_thesis: verum end; suppose ( abs r = r & abs s = - s ) ; ::_thesis: r = - s hence r = - s by A1; ::_thesis: verum end; suppose ( abs r = - r & abs s = s ) ; ::_thesis: r = - s hence r = - s by A1; ::_thesis: verum end; suppose ( abs r = - r & abs s = - s ) ; ::_thesis: r = - s hence r = - s by A1, A2; ::_thesis: verum end; end; end; theorem :: ABSVALUE:29 for m being Nat holds m = abs m proof let m be Nat; ::_thesis: m = abs m m >= 0 by NAT_1:2; hence abs m = m by Def1; ::_thesis: verum end; theorem :: ABSVALUE:30 for r being real number st r <= 0 holds abs r = - r proof let r be real number ; ::_thesis: ( r <= 0 implies abs r = - r ) assume A1: r <= 0 ; ::_thesis: abs r = - r percases ( r < 0 or r = 0 ) by A1; suppose r < 0 ; ::_thesis: abs r = - r hence abs r = - r by Def1; ::_thesis: verum end; suppose r = 0 ; ::_thesis: abs r = - r hence abs r = - r by Th2; ::_thesis: verum end; end; end;