:: EXTREAL2 semantic presentation begin begin theorem Th1: :: EXTREAL2:1 for x being R_eal for a being Real st x = a holds |.x.| = abs a proof let x be R_eal; ::_thesis: for a being Real st x = a holds |.x.| = abs a let a be Real; ::_thesis: ( x = a implies |.x.| = abs a ) assume A1: x = a ; ::_thesis: |.x.| = abs a percases ( 0 <= x or not 0 <= x ) ; suppose 0 <= x ; ::_thesis: |.x.| = abs a then |.x.| = a by A1, EXTREAL1:def_1; hence |.x.| = abs a by ABSVALUE:def_1; ::_thesis: verum end; supposeA2: not 0 <= x ; ::_thesis: |.x.| = abs a then |.x.| = - x by EXTREAL1:4 .= - a by A1, SUPINF_2:2 ; hence |.x.| = abs a by A1, A2, ABSVALUE:def_1; ::_thesis: verum end; end; end; theorem :: EXTREAL2:2 for x being R_eal holds ( |.x.| = x or |.x.| = - x ) by EXTREAL1:def_1; theorem :: EXTREAL2:3 for x being R_eal holds 0 <= |.x.| ; theorem Th4: :: EXTREAL2:4 for x being R_eal st x <> 0 holds 0 < |.x.| proof let x be R_eal; ::_thesis: ( x <> 0 implies 0 < |.x.| ) assume A1: x <> 0 ; ::_thesis: 0 < |.x.| percases ( 0 <= x or not 0 <= x ) ; suppose 0 <= x ; ::_thesis: 0 < |.x.| hence 0 < |.x.| by A1, EXTREAL1:def_1; ::_thesis: verum end; supposeA2: not 0 <= x ; ::_thesis: 0 < |.x.| then 0 < - x ; hence 0 < |.x.| by A2, EXTREAL1:def_1; ::_thesis: verum end; end; end; theorem :: EXTREAL2:5 for x being R_eal holds ( x = 0 iff |.x.| = 0 ) by Th4, EXTREAL1:def_1; theorem :: EXTREAL2:6 for x being R_eal st |.x.| = - x & x <> 0 holds x < 0 ; theorem Th7: :: EXTREAL2:7 for x being R_eal st x <= 0 holds |.x.| = - x proof let x be R_eal; ::_thesis: ( x <= 0 implies |.x.| = - x ) assume A1: x <= 0 ; ::_thesis: |.x.| = - x percases ( x < 0 or x = 0 ) by A1; suppose x < 0 ; ::_thesis: |.x.| = - x hence |.x.| = - x by EXTREAL1:def_1; ::_thesis: verum end; supposeA2: x = 0 ; ::_thesis: |.x.| = - x then - 0 = - x ; hence |.x.| = - x by A2, EXTREAL1:def_1; ::_thesis: verum end; end; end; theorem :: EXTREAL2:8 for x, y being R_eal holds |.(x * y).| = |.x.| * |.y.| proof let x, y be R_eal; ::_thesis: |.(x * y).| = |.x.| * |.y.| percases ( x = 0 or 0 < x or x < 0 ) ; suppose x = 0 ; ::_thesis: |.(x * y).| = |.x.| * |.y.| then ( |.x.| = 0 & |.(x * y).| = 0 ) by EXTREAL1:def_1; hence |.(x * y).| = |.x.| * |.y.| ; ::_thesis: verum end; supposeA1: 0 < x ; ::_thesis: |.(x * y).| = |.x.| * |.y.| percases ( y = 0 or 0 < y or y < 0 ) ; suppose y = 0 ; ::_thesis: |.(x * y).| = |.x.| * |.y.| then ( |.y.| = 0 & |.(x * y).| = 0 ) by EXTREAL1:def_1; hence |.(x * y).| = |.x.| * |.y.| ; ::_thesis: verum end; suppose 0 < y ; ::_thesis: |.(x * y).| = |.x.| * |.y.| then A2: |.y.| = y by EXTREAL1:def_1; |.x.| = x by A1, EXTREAL1:def_1; hence |.(x * y).| = |.x.| * |.y.| by A2, EXTREAL1:def_1; ::_thesis: verum end; supposeA3: y < 0 ; ::_thesis: |.(x * y).| = |.x.| * |.y.| then A4: |.y.| = - y by EXTREAL1:def_1; |.x.| = x by A1, EXTREAL1:def_1; then |.x.| * |.y.| = - (x * y) by A4, XXREAL_3:92; hence |.(x * y).| = |.x.| * |.y.| by A1, A3, EXTREAL1:def_1; ::_thesis: verum end; end; end; supposeA5: x < 0 ; ::_thesis: |.(x * y).| = |.x.| * |.y.| percases ( y = 0 or 0 < y or y < 0 ) ; suppose y = 0 ; ::_thesis: |.(x * y).| = |.x.| * |.y.| then ( |.y.| = 0 & |.(x * y).| = 0 ) by EXTREAL1:def_1; hence |.(x * y).| = |.x.| * |.y.| ; ::_thesis: verum end; supposeA6: 0 < y ; ::_thesis: |.(x * y).| = |.x.| * |.y.| then |.y.| = y by EXTREAL1:def_1; then A7: |.x.| * |.y.| = (- x) * y by A5, EXTREAL1:def_1; |.(x * y).| = - (x * y) by A5, A6, EXTREAL1:def_1; hence |.(x * y).| = |.x.| * |.y.| by A7, XXREAL_3:92; ::_thesis: verum end; suppose y < 0 ; ::_thesis: |.(x * y).| = |.x.| * |.y.| then |.y.| = - y by EXTREAL1:def_1; then |.x.| * |.y.| = (- x) * (- y) by A5, EXTREAL1:def_1; then |.x.| * |.y.| = - (x * (- y)) by XXREAL_3:92 .= - (- (x * y)) by XXREAL_3:92 ; hence |.(x * y).| = |.x.| * |.y.| by EXTREAL1:def_1; ::_thesis: verum end; end; end; end; end; theorem Th9: :: EXTREAL2:9 for x being R_eal holds ( - |.x.| <= x & x <= |.x.| ) proof let x be R_eal; ::_thesis: ( - |.x.| <= x & x <= |.x.| ) percases ( 0 <= x or not 0 <= x ) ; supposeA1: 0 <= x ; ::_thesis: ( - |.x.| <= x & x <= |.x.| ) thus ( - |.x.| <= x & x <= |.x.| ) by A1, EXTREAL1:def_1; ::_thesis: verum end; suppose not 0 <= x ; ::_thesis: ( - |.x.| <= x & x <= |.x.| ) then |.x.| = - x by EXTREAL1:def_1; hence ( - |.x.| <= x & x <= |.x.| ) ; ::_thesis: verum end; end; end; theorem Th10: :: EXTREAL2:10 for x, y being R_eal st |.x.| < y holds ( - y < x & x < y ) proof let x, y be R_eal; ::_thesis: ( |.x.| < y implies ( - y < x & x < y ) ) assume A1: |.x.| < y ; ::_thesis: ( - y < x & x < y ) percases ( 0 <= x or not 0 <= x ) ; suppose 0 <= x ; ::_thesis: ( - y < x & x < y ) hence ( - y < x & x < y ) by A1, EXTREAL1:def_1; ::_thesis: verum end; supposeA2: not 0 <= x ; ::_thesis: ( - y < x & x < y ) then |.x.| = - x by EXTREAL1:def_1; hence ( - y < x & x < y ) by A1, A2, XXREAL_3:60; ::_thesis: verum end; end; end; theorem Th11: :: EXTREAL2:11 for y, x being R_eal st - y < x & x < y holds ( 0 < y & |.x.| < y ) proof let y, x be R_eal; ::_thesis: ( - y < x & x < y implies ( 0 < y & |.x.| < y ) ) assume that A1: - y < x and A2: x < y ; ::_thesis: ( 0 < y & |.x.| < y ) percases ( 0 <= x or not 0 <= x ) ; suppose 0 <= x ; ::_thesis: ( 0 < y & |.x.| < y ) hence ( 0 < y & |.x.| < y ) by A2, EXTREAL1:def_1; ::_thesis: verum end; supposeA3: not 0 <= x ; ::_thesis: ( 0 < y & |.x.| < y ) - x < y by A1, XXREAL_3:60; hence ( 0 < y & |.x.| < y ) by A3, EXTREAL1:def_1; ::_thesis: verum end; end; end; theorem Th12: :: EXTREAL2:12 for y, x being R_eal holds ( ( - y <= x & x <= y ) iff |.x.| <= y ) proof let y, x be R_eal; ::_thesis: ( ( - y <= x & x <= y ) iff |.x.| <= y ) A1: ( - y <= x & x <= y implies |.x.| <= y ) proof assume that A2: - y <= x and A3: x <= y ; ::_thesis: |.x.| <= y percases ( 0 <= x or not 0 <= x ) ; suppose 0 <= x ; ::_thesis: |.x.| <= y hence |.x.| <= y by A3, EXTREAL1:def_1; ::_thesis: verum end; supposeA4: not 0 <= x ; ::_thesis: |.x.| <= y - x <= y by A2, XXREAL_3:60; hence |.x.| <= y by A4, EXTREAL1:def_1; ::_thesis: verum end; end; end; ( |.x.| <= y implies ( - y <= x & x <= y ) ) proof assume A5: |.x.| <= y ; ::_thesis: ( - y <= x & x <= y ) percases ( |.x.| = y or |.x.| < y ) by A5, XXREAL_0:1; suppose |.x.| = y ; ::_thesis: ( - y <= x & x <= y ) hence ( - y <= x & x <= y ) by Th9; ::_thesis: verum end; suppose |.x.| < y ; ::_thesis: ( - y <= x & x <= y ) hence ( - y <= x & x <= y ) by Th10; ::_thesis: verum end; end; end; hence ( ( - y <= x & x <= y ) iff |.x.| <= y ) by A1; ::_thesis: verum end; theorem Th13: :: EXTREAL2:13 for x, y being R_eal holds |.(x + y).| <= |.x.| + |.y.| proof let x, y be R_eal; ::_thesis: |.(x + y).| <= |.x.| + |.y.| A1: ( - |.x.| <= x & - |.y.| <= y ) by Th9; A2: ( x <= |.x.| & y <= |.y.| ) by Th9; A3: (- |.x.|) - |.y.| = - (|.x.| + |.y.|) by XXREAL_3:25; ( x + y <= |.x.| + |.y.| & (- |.x.|) + (- |.y.|) <= x + y ) by A1, A2, XXREAL_3:36; hence |.(x + y).| <= |.x.| + |.y.| by A3, Th12; ::_thesis: verum end; theorem Th14: :: EXTREAL2:14 for x being R_eal st -infty < x & x < +infty & x <> 0 holds |.x.| * |.(1. / x).| = 1. proof let x be R_eal; ::_thesis: ( -infty < x & x < +infty & x <> 0 implies |.x.| * |.(1. / x).| = 1. ) assume that A1: ( -infty < x & x < +infty ) and A2: x <> 0 ; ::_thesis: |.x.| * |.(1. / x).| = 1. reconsider a = x as Real by A1, XXREAL_0:14; A3: 1. / x = 1 / a by EXTREAL1:2, MESFUNC1:def_8; percases ( 0 <= x or not 0 <= x ) ; suppose 0 <= x ; ::_thesis: |.x.| * |.(1. / x).| = 1. then ( |.x.| = a & |.(1. / x).| = 1 / a ) by A3, EXTREAL1:def_1; then |.x.| * |.(1. / x).| = a * (1 / a) by EXTREAL1:1; hence |.x.| * |.(1. / x).| = 1. by A2, MESFUNC1:def_8, XCMPLX_1:106; ::_thesis: verum end; supposeA4: not 0 <= x ; ::_thesis: |.x.| * |.(1. / x).| = 1. then A5: |.x.| = - x by EXTREAL1:def_1 .= - a by SUPINF_2:2 ; |.(1. / x).| = - (1. / x) by A3, A4, EXTREAL1:4, XREAL_1:142 .= - (1 / a) by A3, SUPINF_2:2 ; then |.x.| * |.(1. / x).| = (- a) * (- (1 / a)) by A5, EXTREAL1:1 .= a * (1 / a) ; hence |.x.| * |.(1. / x).| = 1. by A4, MESFUNC1:def_8, XCMPLX_1:106; ::_thesis: verum end; end; end; theorem :: EXTREAL2:15 for x being R_eal st ( x = +infty or x = -infty ) holds |.x.| * |.(1. / x).| = 0 proof let x be R_eal; ::_thesis: ( ( x = +infty or x = -infty ) implies |.x.| * |.(1. / x).| = 0 ) assume ( x = +infty or x = -infty ) ; ::_thesis: |.x.| * |.(1. / x).| = 0 then |.(1. / x).| = 0 by EXTREAL1:def_1; hence |.x.| * |.(1. / x).| = 0 ; ::_thesis: verum end; theorem :: EXTREAL2:16 for x being R_eal st x <> 0 holds |.(1. / x).| = 1. / |.x.| proof let x be R_eal; ::_thesis: ( x <> 0 implies |.(1. / x).| = 1. / |.x.| ) assume A1: x <> 0 ; ::_thesis: |.(1. / x).| = 1. / |.x.| percases ( x = +infty or x = -infty or ( x <> +infty & x <> -infty ) ) ; supposeA2: x = +infty ; ::_thesis: |.(1. / x).| = 1. / |.x.| then |.(1. / x).| = 0 by EXTREAL1:def_1; hence |.(1. / x).| = 1. / |.x.| by A2, EXTREAL1:3; ::_thesis: verum end; suppose x = -infty ; ::_thesis: |.(1. / x).| = 1. / |.x.| then ( |.(1. / x).| = 0 & |.x.| = +infty ) by EXTREAL1:def_1, XXREAL_3:5; hence |.(1. / x).| = 1. / |.x.| ; ::_thesis: verum end; supposeA3: ( x <> +infty & x <> -infty ) ; ::_thesis: |.(1. / x).| = 1. / |.x.| A4: 0 < |.x.| by A1, Th4; A5: x < +infty by A3, XXREAL_0:4; -infty <= x by XXREAL_0:5; then A6: -infty < x by A3, XXREAL_0:1; then - +infty < x by XXREAL_3:def_3; then A7: |.x.| < +infty by A5, Th11; |.(1. / x).| * |.x.| = 1. by A1, A6, A5, Th14; hence |.(1. / x).| = 1. / |.x.| by A4, A7, XXREAL_3:88; ::_thesis: verum end; end; end; theorem :: EXTREAL2:17 for x, y being R_eal st ( ( not x = -infty & not x = +infty ) or ( not y = -infty & not y = +infty ) ) & y <> 0 holds |.(x / y).| = |.x.| / |.y.| proof let x, y be R_eal; ::_thesis: ( ( ( not x = -infty & not x = +infty ) or ( not y = -infty & not y = +infty ) ) & y <> 0 implies |.(x / y).| = |.x.| / |.y.| ) assume that A1: ( ( not x = -infty & not x = +infty ) or ( not y = -infty & not y = +infty ) ) and A2: y <> 0 ; ::_thesis: |.(x / y).| = |.x.| / |.y.| percases ( x = +infty or x = -infty or ( x <> +infty & x <> -infty ) ) ; supposeA3: x = +infty ; ::_thesis: |.(x / y).| = |.x.| / |.y.| A4: -infty < y by A1, A3, XXREAL_0:12, XXREAL_0:14; percases ( 0 < y or y < 0 ) by A2; supposeA5: 0 < y ; ::_thesis: |.(x / y).| = |.x.| / |.y.| then x / y = +infty by A3, A1, XXREAL_3:83; then A6: |.(x / y).| = +infty by EXTREAL1:3; |.y.| = y by A5, EXTREAL1:3; hence |.(x / y).| = |.x.| / |.y.| by A3, A1, A5, A6, XXREAL_3:83; ::_thesis: verum end; supposeA7: y < 0 ; ::_thesis: |.(x / y).| = |.x.| / |.y.| then |.y.| = - y by EXTREAL1:4; then A8: |.y.| < +infty by A4, XXREAL_3:5, XXREAL_3:38; x / y = -infty by A3, A1, A7, XXREAL_3:85; then |.(x / y).| = +infty by EXTREAL1:4, XXREAL_3:5; hence |.(x / y).| = |.x.| / |.y.| by A8, A2, A3, Th4, XXREAL_3:83; ::_thesis: verum end; end; end; supposeA9: x = -infty ; ::_thesis: |.(x / y).| = |.x.| / |.y.| A10: -infty < y by A1, A9, XXREAL_0:12, XXREAL_0:14; percases ( 0 < y or y < 0 ) by A2; supposeA11: 0 < y ; ::_thesis: |.(x / y).| = |.x.| / |.y.| then A12: x / y = -infty by A9, A1, XXREAL_3:86; A13: |.x.| = +infty by A9, EXTREAL1:4, XXREAL_3:5; |.y.| = y by A11, EXTREAL1:3; hence |.(x / y).| = |.x.| / |.y.| by A9, A1, A11, A12, A13, XXREAL_3:83; ::_thesis: verum end; supposeA14: y < 0 ; ::_thesis: |.(x / y).| = |.x.| / |.y.| then |.y.| = - y by EXTREAL1:4; then A15: |.y.| < +infty by A10, XXREAL_3:5, XXREAL_3:38; A16: x / y = +infty by A9, A1, A14, XXREAL_3:84; ( 0 < |.y.| & |.x.| = +infty ) by A2, A9, Th4, EXTREAL1:4, XXREAL_3:5; hence |.(x / y).| = |.x.| / |.y.| by A15, A16, XXREAL_3:83; ::_thesis: verum end; end; end; suppose ( x <> +infty & x <> -infty ) ; ::_thesis: |.(x / y).| = |.x.| / |.y.| then reconsider a = x as Real by XXREAL_0:14; percases ( y = +infty or y = -infty or ( y <> +infty & y <> -infty ) ) ; suppose y = +infty ; ::_thesis: |.(x / y).| = |.x.| / |.y.| then ( |.(x / y).| = 0 & |.y.| = +infty ) by EXTREAL1:def_1; hence |.(x / y).| = |.x.| / |.y.| ; ::_thesis: verum end; suppose y = -infty ; ::_thesis: |.(x / y).| = |.x.| / |.y.| then ( |.(x / y).| = 0 & |.y.| = +infty ) by EXTREAL1:def_1, XXREAL_3:5; hence |.(x / y).| = |.x.| / |.y.| ; ::_thesis: verum end; suppose ( y <> +infty & y <> -infty ) ; ::_thesis: |.(x / y).| = |.x.| / |.y.| then reconsider b = y as Real by XXREAL_0:14; ( |.x.| = abs a & |.y.| = abs b ) by Th1; then A17: |.x.| / |.y.| = (abs a) / (abs b) by EXTREAL1:2; x / y = a / b by EXTREAL1:2; then |.(x / y).| = abs (a / b) by Th1; hence |.(x / y).| = |.x.| / |.y.| by A17, COMPLEX1:67; ::_thesis: verum end; end; end; end; end; theorem Th18: :: EXTREAL2:18 for x being R_eal holds |.x.| = |.(- x).| proof let x be R_eal; ::_thesis: |.x.| = |.(- x).| percases ( 0 < x or x < 0 or x = 0 ) ; suppose 0 < x ; ::_thesis: |.x.| = |.(- x).| then |.(- x).| = - (- x) by EXTREAL1:4 .= x ; hence |.x.| = |.(- x).| ; ::_thesis: verum end; suppose x < 0 ; ::_thesis: |.x.| = |.(- x).| then |.x.| = - x by EXTREAL1:4; hence |.x.| = |.(- x).| ; ::_thesis: verum end; suppose x = 0 ; ::_thesis: |.x.| = |.(- x).| hence |.x.| = |.(- x).| ; ::_thesis: verum end; end; end; theorem Th19: :: EXTREAL2:19 ( |.+infty.| = +infty & |.-infty.| = +infty ) proof thus |.+infty.| = +infty by EXTREAL1:3; ::_thesis: |.-infty.| = +infty - -infty = +infty by XXREAL_3:23; hence |.-infty.| = +infty by EXTREAL1:4; ::_thesis: verum end; theorem Th20: :: EXTREAL2:20 for x, y being R_eal st ( x is Real or y is Real ) holds |.x.| - |.y.| <= |.(x - y).| proof let x, y be R_eal; ::_thesis: ( ( x is Real or y is Real ) implies |.x.| - |.y.| <= |.(x - y).| ) assume A1: ( x is Real or y is Real ) ; ::_thesis: |.x.| - |.y.| <= |.(x - y).| percases ( y is Real or x is Real ) by A1; supposeA2: y is Real ; ::_thesis: |.x.| - |.y.| <= |.(x - y).| then (x - y) + y = x by XXREAL_3:22; then A3: |.x.| <= |.(x - y).| + |.y.| by Th13; reconsider b = y as Real by A2; thus |.x.| - |.y.| <= |.(x - y).| by A3, XXREAL_3:42; ::_thesis: verum end; suppose x is Real ; ::_thesis: |.x.| - |.y.| <= |.(x - y).| then reconsider a = x as Real ; A4: |.x.| = abs a by Th1; percases ( y = +infty or y = -infty or ( y <> +infty & y <> -infty ) ) ; suppose ( y = +infty or y = -infty ) ; ::_thesis: |.x.| - |.y.| <= |.(x - y).| hence |.x.| - |.y.| <= |.(x - y).| by A4, Th19, XXREAL_3:13; ::_thesis: verum end; suppose ( y <> +infty & y <> -infty ) ; ::_thesis: |.x.| - |.y.| <= |.(x - y).| then reconsider b = y as Real by XXREAL_0:14; x - y = a - b by SUPINF_2:3; then A5: |.(x - y).| = abs (a - b) by Th1; |.y.| = abs b by Th1; then |.x.| - |.y.| = (abs a) - (abs b) by A4, SUPINF_2:3; hence |.x.| - |.y.| <= |.(x - y).| by A5, COMPLEX1:59; ::_thesis: verum end; end; end; end; end; theorem :: EXTREAL2:21 for x, y being R_eal holds |.(x - y).| <= |.x.| + |.y.| proof let x, y be R_eal; ::_thesis: |.(x - y).| <= |.x.| + |.y.| percases ( x = +infty or x = -infty or ( x <> +infty & x <> -infty ) ) ; suppose ( x = +infty or x = -infty ) ; ::_thesis: |.(x - y).| <= |.x.| + |.y.| then |.x.| + |.y.| = +infty by XXREAL_3:def_2, Th19; hence |.(x - y).| <= |.x.| + |.y.| by XXREAL_0:3; ::_thesis: verum end; supposeA1: ( x <> +infty & x <> -infty ) ; ::_thesis: |.(x - y).| <= |.x.| + |.y.| then reconsider a = x as Real by XXREAL_0:14; percases ( y = +infty or y = -infty or ( y <> +infty & y <> -infty ) ) ; supposeA2: y = +infty ; ::_thesis: |.(x - y).| <= |.x.| + |.y.| x - y = -infty by A1, A2, XXREAL_3:13; hence |.(x - y).| <= |.x.| + |.y.| by A2, Th19, XXREAL_3:def_2; ::_thesis: verum end; supposeA3: y = -infty ; ::_thesis: |.(x - y).| <= |.x.| + |.y.| x - y = +infty by A1, A3, XXREAL_3:14; hence |.(x - y).| <= |.x.| + |.y.| by A3, Th19, XXREAL_3:def_2; ::_thesis: verum end; suppose ( y <> +infty & y <> -infty ) ; ::_thesis: |.(x - y).| <= |.x.| + |.y.| then reconsider b = y as Real by XXREAL_0:14; ( |.x.| = abs a & |.y.| = abs b ) by Th1; then A4: |.x.| + |.y.| = (abs a) + (abs b) by SUPINF_2:1; x - y = a - b by SUPINF_2:3; then |.(x - y).| = abs (a - b) by Th1; hence |.(x - y).| <= |.x.| + |.y.| by A4, COMPLEX1:57; ::_thesis: verum end; end; end; end; end; theorem :: EXTREAL2:22 canceled; theorem :: EXTREAL2:23 for x, z, y, w being R_eal st |.x.| <= z & |.y.| <= w holds |.(x + y).| <= z + w proof let x, z, y, w be R_eal; ::_thesis: ( |.x.| <= z & |.y.| <= w implies |.(x + y).| <= z + w ) assume A1: ( |.x.| <= z & |.y.| <= w ) ; ::_thesis: |.(x + y).| <= z + w then ( - z <= x & - w <= y ) by Th12; then A2: (- z) + (- w) <= x + y by XXREAL_3:36; ( x <= z & y <= w ) by A1, Th12; then A3: x + y <= z + w by XXREAL_3:36; (- z) - w = - (z + w) by XXREAL_3:25; hence |.(x + y).| <= z + w by A3, A2, Th12; ::_thesis: verum end; theorem :: EXTREAL2:24 for x, y being R_eal st ( x is Real or y is Real ) holds |.(|.x.| - |.y.|).| <= |.(x - y).| proof let x, y be R_eal; ::_thesis: ( ( x is Real or y is Real ) implies |.(|.x.| - |.y.|).| <= |.(x - y).| ) A1: |.y.| - |.x.| = - (|.x.| - |.y.|) by XXREAL_3:26; assume A2: ( x is Real or y is Real ) ; ::_thesis: |.(|.x.| - |.y.|).| <= |.(x - y).| then A3: |.x.| - |.y.| <= |.(x - y).| by Th20; y - x = - (x - y) by XXREAL_3:26; then A4: |.(y - x).| = |.(x - y).| by Th18; |.y.| - |.x.| <= |.(y - x).| by A2, Th20; then - |.(x - y).| <= - (- (|.x.| - |.y.|)) by A4, A1, XXREAL_3:38; hence |.(|.x.| - |.y.|).| <= |.(x - y).| by A3, Th12; ::_thesis: verum end; theorem :: EXTREAL2:25 for x, y being R_eal st 0 <= x * y holds |.(x + y).| = |.x.| + |.y.| proof let x, y be R_eal; ::_thesis: ( 0 <= x * y implies |.(x + y).| = |.x.| + |.y.| ) assume A1: 0 <= x * y ; ::_thesis: |.(x + y).| = |.x.| + |.y.| percases ( ( ( 0 <= x or 0 < x ) & ( 0 <= y or 0 < y ) ) or ( ( x <= 0 or x < 0 ) & ( y <= 0 or y < 0 ) ) ) by A1; suppose ( ( 0 <= x or 0 < x ) & ( 0 <= y or 0 < y ) ) ; ::_thesis: |.(x + y).| = |.x.| + |.y.| then ( |.x.| = x & |.y.| = y ) by EXTREAL1:def_1; hence |.(x + y).| = |.x.| + |.y.| by EXTREAL1:def_1; ::_thesis: verum end; supposeA2: ( ( x <= 0 or x < 0 ) & ( y <= 0 or y < 0 ) ) ; ::_thesis: |.(x + y).| = |.x.| + |.y.| then A3: |.(x + y).| = - (x + y) by Th7 .= (- x) - y by XXREAL_3:25 ; |.x.| = - x by A2, Th7; hence |.(x + y).| = |.x.| + |.y.| by A2, A3, Th7; ::_thesis: verum end; end; end; begin theorem :: EXTREAL2:26 for x, y being R_eal st x <> +infty & y <> +infty & not ( x = +infty & y = +infty ) & not ( x = -infty & y = -infty ) holds min (x,y) = ((x + y) - |.(x - y).|) / (R_EAL 2) proof let x, y be R_eal; ::_thesis: ( x <> +infty & y <> +infty & not ( x = +infty & y = +infty ) & not ( x = -infty & y = -infty ) implies min (x,y) = ((x + y) - |.(x - y).|) / (R_EAL 2) ) assume that A1: x <> +infty and A2: y <> +infty and A3: ( not ( x = +infty & y = +infty ) & not ( x = -infty & y = -infty ) ) ; ::_thesis: min (x,y) = ((x + y) - |.(x - y).|) / (R_EAL 2) percases ( x = -infty or x <> -infty ) ; supposeA4: x = -infty ; ::_thesis: min (x,y) = ((x + y) - |.(x - y).|) / (R_EAL 2) then ( x + y = -infty & x - y = -infty ) by A2, A3, XXREAL_3:14, XXREAL_3:def_2; then A5: (x + y) - |.(x - y).| = -infty by XXREAL_3:14; A6: min (x,y) = -infty by A4, XXREAL_0:44; R_EAL 2 = 2 by MEASURE6:def_1; hence min (x,y) = ((x + y) - |.(x - y).|) / (R_EAL 2) by A6, A5, XXREAL_3:86; ::_thesis: verum end; suppose x <> -infty ; ::_thesis: min (x,y) = ((x + y) - |.(x - y).|) / (R_EAL 2) then reconsider a = x as Real by A1, XXREAL_0:14; percases ( y = -infty or y <> -infty ) ; supposeA7: y = -infty ; ::_thesis: min (x,y) = ((x + y) - |.(x - y).|) / (R_EAL 2) then ( x + y = -infty & x - y = +infty ) by A1, A3, XXREAL_3:14, XXREAL_3:def_2; then A8: (x + y) - |.(x - y).| = -infty by XXREAL_3:14; A9: min (x,y) = -infty by A7, XXREAL_0:44; R_EAL 2 = 2 by MEASURE6:def_1; hence min (x,y) = ((x + y) - |.(x - y).|) / (R_EAL 2) by A9, A8, XXREAL_3:86; ::_thesis: verum end; suppose y <> -infty ; ::_thesis: min (x,y) = ((x + y) - |.(x - y).|) / (R_EAL 2) then reconsider b = y as Real by A2, XXREAL_0:14; x - y = a - b by SUPINF_2:3; then ( x + y = a + b & |.(x - y).| = abs (a - b) ) by Th1, SUPINF_2:1; then A10: (x + y) - |.(x - y).| = (a + b) - (abs (a - b)) by SUPINF_2:3; R_EAL 2 = 2 by MEASURE6:def_1; then ((x + y) - |.(x - y).|) / (R_EAL 2) = ((a + b) - (abs (a - b))) / 2 by A10, EXTREAL1:2; hence min (x,y) = ((x + y) - |.(x - y).|) / (R_EAL 2) by COMPLEX1:73; ::_thesis: verum end; end; end; end; end; theorem :: EXTREAL2:27 for x, y being R_eal st x <> -infty & y <> -infty & not ( x = +infty & y = +infty ) & not ( x = -infty & y = -infty ) holds max (x,y) = ((x + y) + |.(x - y).|) / (R_EAL 2) proof let x, y be R_eal; ::_thesis: ( x <> -infty & y <> -infty & not ( x = +infty & y = +infty ) & not ( x = -infty & y = -infty ) implies max (x,y) = ((x + y) + |.(x - y).|) / (R_EAL 2) ) assume that A1: x <> -infty and A2: y <> -infty and A3: ( not ( x = +infty & y = +infty ) & not ( x = -infty & y = -infty ) ) ; ::_thesis: max (x,y) = ((x + y) + |.(x - y).|) / (R_EAL 2) percases ( x = +infty or x <> +infty ) ; supposeA4: x = +infty ; ::_thesis: max (x,y) = ((x + y) + |.(x - y).|) / (R_EAL 2) then ( x + y = +infty & x - y = +infty ) by A2, A3, XXREAL_3:13, XXREAL_3:def_2; then A5: (x + y) + |.(x - y).| = +infty by XXREAL_3:def_2; A6: max (x,y) = +infty by A4, XXREAL_0:41; R_EAL 2 = 2 by MEASURE6:def_1; hence max (x,y) = ((x + y) + |.(x - y).|) / (R_EAL 2) by A6, A5, XXREAL_3:83; ::_thesis: verum end; suppose x <> +infty ; ::_thesis: max (x,y) = ((x + y) + |.(x - y).|) / (R_EAL 2) then reconsider a = x as Real by A1, XXREAL_0:14; percases ( y = +infty or y <> +infty ) ; supposeA7: y = +infty ; ::_thesis: max (x,y) = ((x + y) + |.(x - y).|) / (R_EAL 2) then ( x + y = +infty & x - y = -infty ) by A1, A3, XXREAL_3:13, XXREAL_3:def_2; then A8: (x + y) + |.(x - y).| = +infty by XXREAL_3:def_2; A9: max (x,y) = +infty by A7, XXREAL_0:41; R_EAL 2 = 2 by MEASURE6:def_1; hence max (x,y) = ((x + y) + |.(x - y).|) / (R_EAL 2) by A9, A8, XXREAL_3:83; ::_thesis: verum end; suppose y <> +infty ; ::_thesis: max (x,y) = ((x + y) + |.(x - y).|) / (R_EAL 2) then reconsider b = y as Real by A2, XXREAL_0:14; x - y = a - b by SUPINF_2:3; then ( x + y = a + b & |.(x - y).| = abs (a - b) ) by Th1, SUPINF_2:1; then A10: (x + y) + |.(x - y).| = (a + b) + (abs (a - b)) by SUPINF_2:1; R_EAL 2 = 2 by MEASURE6:def_1; then ((x + y) + |.(x - y).|) / (R_EAL 2) = ((a + b) + (abs (a - b))) / 2 by A10, EXTREAL1:2; hence max (x,y) = ((x + y) + |.(x - y).|) / (R_EAL 2) by COMPLEX1:74; ::_thesis: verum end; end; end; end; end; definition let x, y be R_eal; :: original: max redefine func max (x,y) -> R_eal; coherence max (x,y) is R_eal by XXREAL_0:def_1; :: original: min redefine func min (x,y) -> R_eal; coherence min (x,y) is R_eal by XXREAL_0:def_1; end; theorem :: EXTREAL2:28 for x, y being R_eal holds (min (x,y)) + (max (x,y)) = x + y proof let x, y be R_eal; ::_thesis: (min (x,y)) + (max (x,y)) = x + y percases ( x <= y or not x <= y ) ; supposeA1: x <= y ; ::_thesis: (min (x,y)) + (max (x,y)) = x + y then min (x,y) = x by XXREAL_0:def_9; hence (min (x,y)) + (max (x,y)) = x + y by A1, XXREAL_0:def_10; ::_thesis: verum end; supposeA2: not x <= y ; ::_thesis: (min (x,y)) + (max (x,y)) = x + y then min (x,y) = y by XXREAL_0:def_9; hence (min (x,y)) + (max (x,y)) = x + y by A2, XXREAL_0:def_10; ::_thesis: verum end; end; end; begin theorem Th29: :: EXTREAL2:29 for x being R_eal holds ( not |.x.| = +infty or x = +infty or x = -infty ) proof let x be R_eal; ::_thesis: ( not |.x.| = +infty or x = +infty or x = -infty ) A1: ( |.x.| = x or - |.x.| = - (- x) ) by EXTREAL1:def_1; assume |.x.| = +infty ; ::_thesis: ( x = +infty or x = -infty ) hence ( x = +infty or x = -infty ) by A1, XXREAL_3:5; ::_thesis: verum end; theorem :: EXTREAL2:30 for x being R_eal holds ( |.x.| < +infty iff x in REAL ) proof let x be R_eal; ::_thesis: ( |.x.| < +infty iff x in REAL ) thus ( |.x.| < +infty implies x in REAL ) by Th19, XXREAL_0:14; ::_thesis: ( x in REAL implies |.x.| < +infty ) assume A1: x in REAL ; ::_thesis: |.x.| < +infty assume |.x.| >= +infty ; ::_thesis: contradiction hence contradiction by A1, Th29, XXREAL_0:4; ::_thesis: verum end;