:: XXREAL_3 semantic presentation begin definition let x, y be ext-real number ; redefine pred x <= y means :Def1: :: XXREAL_3:def 1 ex p, q being Element of REAL st ( p = x & q = y & p <= q ) if ( x in REAL & y in REAL ) otherwise ( x = -infty or y = +infty ); consistency verum ; compatibility ( ( x in REAL & y in REAL implies ( x <= y iff ex p, q being Element of REAL st ( p = x & q = y & p <= q ) ) ) & ( ( not x in REAL or not y in REAL ) implies ( x <= y iff ( x = -infty or y = +infty ) ) ) ) proof thus ( x in REAL & y in REAL implies ( x <= y iff ex p, q being Element of REAL st ( p = x & q = y & p <= q ) ) ) ; ::_thesis: ( ( not x in REAL or not y in REAL ) implies ( x <= y iff ( x = -infty or y = +infty ) ) ) thus ( ( not x in REAL or not y in REAL ) implies ( x <= y iff ( x = -infty or y = +infty ) ) ) ::_thesis: verum proof assume A1: ( not x in REAL or not y in REAL ) ; ::_thesis: ( x <= y iff ( x = -infty or y = +infty ) ) percases ( not x in REAL or not y in REAL ) by A1; supposeA2: not x in REAL ; ::_thesis: ( x <= y iff ( x = -infty or y = +infty ) ) thus ( not x <= y or x = -infty or y = +infty ) ::_thesis: ( ( x = -infty or y = +infty ) implies x <= y ) proof assume A3: x <= y ; ::_thesis: ( x = -infty or y = +infty ) assume x <> -infty ; ::_thesis: y = +infty then x = +infty by A2, XXREAL_0:14; hence y = +infty by A3, XXREAL_0:4; ::_thesis: verum end; thus ( ( x = -infty or y = +infty ) implies x <= y ) by XXREAL_0:3, XXREAL_0:5; ::_thesis: verum end; supposeA4: not y in REAL ; ::_thesis: ( x <= y iff ( x = -infty or y = +infty ) ) thus ( not x <= y or x = -infty or y = +infty ) ::_thesis: ( ( x = -infty or y = +infty ) implies x <= y ) proof assume A5: x <= y ; ::_thesis: ( x = -infty or y = +infty ) assume A6: x <> -infty ; ::_thesis: y = +infty assume y <> +infty ; ::_thesis: contradiction then y = -infty by A4, XXREAL_0:14; hence contradiction by A5, A6, XXREAL_0:6; ::_thesis: verum end; thus ( ( x = -infty or y = +infty ) implies x <= y ) by XXREAL_0:3, XXREAL_0:5; ::_thesis: verum end; end; end; end; end; :: deftheorem Def1 defines <= XXREAL_3:def_1_:_ for x, y being ext-real number holds ( ( x in REAL & y in REAL implies ( x <= y iff ex p, q being Element of REAL st ( p = x & q = y & p <= q ) ) ) & ( ( not x in REAL or not y in REAL ) implies ( x <= y iff ( x = -infty or y = +infty ) ) ) ); registration cluster ext-real positive non real for set ; existence ex b1 being ext-real number st ( not b1 is real & b1 is positive ) proof take +infty ; ::_thesis: ( not +infty is real & +infty is positive ) thus ( not +infty is real & +infty is positive ) ; ::_thesis: verum end; cluster ext-real negative non real for set ; existence ex b1 being ext-real number st ( not b1 is real & b1 is negative ) proof take -infty ; ::_thesis: ( not -infty is real & -infty is negative ) thus ( not -infty is real & -infty is negative ) ; ::_thesis: verum end; end; theorem Th1: :: XXREAL_3:1 for x being ext-real positive non real number holds x = +infty proof let x be ext-real positive non real number ; ::_thesis: x = +infty not x in REAL ; hence x = +infty by XXREAL_0:14; ::_thesis: verum end; theorem Th2: :: XXREAL_3:2 for x being ext-real negative non real number holds x = -infty proof let x be ext-real negative non real number ; ::_thesis: x = -infty not x in REAL ; hence x = -infty by XXREAL_0:14; ::_thesis: verum end; registration cluster ext-real non negative non real -> ext-real positive for set ; coherence for b1 being ext-real number st not b1 is real & not b1 is negative holds b1 is positive ; cluster ext-real non positive non real -> ext-real negative for set ; coherence for b1 being ext-real number st not b1 is real & not b1 is positive holds b1 is negative ; end; theorem Th3: :: XXREAL_3:3 for x, z being ext-real number st x < z holds ex y being real number st ( x < y & y < z ) proof let x, z be ext-real number ; ::_thesis: ( x < z implies ex y being real number st ( x < y & y < z ) ) assume A1: x < z ; ::_thesis: ex y being real number st ( x < y & y < z ) percases ( ( x in REAL & z in REAL ) or x = +infty or z = -infty or z = +infty or x = -infty ) by XXREAL_0:14; suppose ( x in REAL & z in REAL ) ; ::_thesis: ex y being real number st ( x < y & y < z ) hence ex y being real number st ( x < y & y < z ) by A1, XREAL_1:5; ::_thesis: verum end; suppose ( x = +infty or z = -infty ) ; ::_thesis: ex y being real number st ( x < y & y < z ) hence ex y being real number st ( x < y & y < z ) by A1, XXREAL_0:4, XXREAL_0:6; ::_thesis: verum end; supposeA2: z = +infty ; ::_thesis: ex y being real number st ( x < y & y < z ) percases ( x = -infty or x in REAL ) by A1, A2, XXREAL_0:14; suppose x = -infty ; ::_thesis: ex y being real number st ( x < y & y < z ) hence ex y being real number st ( x < y & y < z ) by A2; ::_thesis: verum end; suppose x in REAL ; ::_thesis: ex y being real number st ( x < y & y < z ) then reconsider x1 = x as real number ; take x1 + 1 ; ::_thesis: ( x < x1 + 1 & x1 + 1 < z ) A3: x1 + 1 in REAL by XREAL_0:def_1; x1 + 0 < x1 + 1 by XREAL_1:8; hence ( x < x1 + 1 & x1 + 1 < z ) by A2, A3, XXREAL_0:9; ::_thesis: verum end; end; end; supposeA4: x = -infty ; ::_thesis: ex y being real number st ( x < y & y < z ) percases ( z = +infty or z in REAL ) by A1, A4, XXREAL_0:14; suppose z = +infty ; ::_thesis: ex y being real number st ( x < y & y < z ) hence ex y being real number st ( x < y & y < z ) by A4; ::_thesis: verum end; suppose z in REAL ; ::_thesis: ex y being real number st ( x < y & y < z ) then reconsider z1 = z as real number ; take z1 - 1 ; ::_thesis: ( x < z1 - 1 & z1 - 1 < z ) A5: z1 - 1 in REAL by XREAL_0:def_1; z1 - 1 < z1 - 0 by XREAL_1:10; hence ( x < z1 - 1 & z1 - 1 < z ) by A4, A5, XXREAL_0:12; ::_thesis: verum end; end; end; end; end; begin definition let x, y be ext-real number ; funcx + y -> ext-real number means :Def2: :: XXREAL_3:def 2 ex a, b being complex number st ( x = a & y = b & it = a + b ) if ( x is real & y is real ) it = +infty if ( ( x = +infty & y <> -infty ) or ( y = +infty & x <> -infty ) ) it = -infty if ( ( x = -infty & y <> +infty ) or ( y = -infty & x <> +infty ) ) otherwise it = 0 ; existence ( ( x is real & y is real implies ex b1 being ext-real number ex a, b being complex number st ( x = a & y = b & b1 = a + b ) ) & ( ( ( x = +infty & y <> -infty ) or ( y = +infty & x <> -infty ) ) implies ex b1 being ext-real number st b1 = +infty ) & ( ( ( x = -infty & y <> +infty ) or ( y = -infty & x <> +infty ) ) implies ex b1 being ext-real number st b1 = -infty ) & ( ( x is real & y is real ) or ( x = +infty & y <> -infty ) or ( y = +infty & x <> -infty ) or ( x = -infty & y <> +infty ) or ( y = -infty & x <> +infty ) or ex b1 being ext-real number st b1 = 0 ) ) proof thus ( x is real & y is real implies ex c being ext-real number ex a, b being complex number st ( x = a & y = b & c = a + b ) ) ::_thesis: ( ( ( ( x = +infty & y <> -infty ) or ( y = +infty & x <> -infty ) ) implies ex b1 being ext-real number st b1 = +infty ) & ( ( ( x = -infty & y <> +infty ) or ( y = -infty & x <> +infty ) ) implies ex b1 being ext-real number st b1 = -infty ) & ( ( x is real & y is real ) or ( x = +infty & y <> -infty ) or ( y = +infty & x <> -infty ) or ( x = -infty & y <> +infty ) or ( y = -infty & x <> +infty ) or ex b1 being ext-real number st b1 = 0 ) ) proof assume ( x is real & y is real ) ; ::_thesis: ex c being ext-real number ex a, b being complex number st ( x = a & y = b & c = a + b ) then reconsider a = x, b = y as real number ; take a + b ; ::_thesis: ex a, b being complex number st ( x = a & y = b & a + b = a + b ) take a ; ::_thesis: ex b being complex number st ( x = a & y = b & a + b = a + b ) take b ; ::_thesis: ( x = a & y = b & a + b = a + b ) thus ( x = a & y = b & a + b = a + b ) ; ::_thesis: verum end; thus ( ( ( ( x = +infty & y <> -infty ) or ( y = +infty & x <> -infty ) ) implies ex b1 being ext-real number st b1 = +infty ) & ( ( ( x = -infty & y <> +infty ) or ( y = -infty & x <> +infty ) ) implies ex b1 being ext-real number st b1 = -infty ) & ( ( x is real & y is real ) or ( x = +infty & y <> -infty ) or ( y = +infty & x <> -infty ) or ( x = -infty & y <> +infty ) or ( y = -infty & x <> +infty ) or ex b1 being ext-real number st b1 = 0 ) ) ; ::_thesis: verum end; uniqueness for b1, b2 being ext-real number holds ( ( x is real & y is real & ex a, b being complex number st ( x = a & y = b & b1 = a + b ) & ex a, b being complex number st ( x = a & y = b & b2 = a + b ) implies b1 = b2 ) & ( ( ( x = +infty & y <> -infty ) or ( y = +infty & x <> -infty ) ) & b1 = +infty & b2 = +infty implies b1 = b2 ) & ( ( ( x = -infty & y <> +infty ) or ( y = -infty & x <> +infty ) ) & b1 = -infty & b2 = -infty implies b1 = b2 ) & ( ( x is real & y is real ) or ( x = +infty & y <> -infty ) or ( y = +infty & x <> -infty ) or ( x = -infty & y <> +infty ) or ( y = -infty & x <> +infty ) or not b1 = 0 or not b2 = 0 or b1 = b2 ) ) ; consistency for b1 being ext-real number holds ( ( x is real & y is real & ( ( x = +infty & y <> -infty ) or ( y = +infty & x <> -infty ) ) implies ( ex a, b being complex number st ( x = a & y = b & b1 = a + b ) iff b1 = +infty ) ) & ( x is real & y is real & ( ( x = -infty & y <> +infty ) or ( y = -infty & x <> +infty ) ) implies ( ex a, b being complex number st ( x = a & y = b & b1 = a + b ) iff b1 = -infty ) ) & ( ( ( x = +infty & y <> -infty ) or ( y = +infty & x <> -infty ) ) & ( ( x = -infty & y <> +infty ) or ( y = -infty & x <> +infty ) ) implies ( b1 = +infty iff b1 = -infty ) ) ) ; commutativity for b1, x, y being ext-real number st ( x is real & y is real implies ex a, b being complex number st ( x = a & y = b & b1 = a + b ) ) & ( ( ( x = +infty & y <> -infty ) or ( y = +infty & x <> -infty ) ) implies b1 = +infty ) & ( ( ( x = -infty & y <> +infty ) or ( y = -infty & x <> +infty ) ) implies b1 = -infty ) & ( ( x is real & y is real ) or ( x = +infty & y <> -infty ) or ( y = +infty & x <> -infty ) or ( x = -infty & y <> +infty ) or ( y = -infty & x <> +infty ) or b1 = 0 ) holds ( ( y is real & x is real implies ex a, b being complex number st ( y = a & x = b & b1 = a + b ) ) & ( ( ( y = +infty & x <> -infty ) or ( x = +infty & y <> -infty ) ) implies b1 = +infty ) & ( ( ( y = -infty & x <> +infty ) or ( x = -infty & y <> +infty ) ) implies b1 = -infty ) & ( ( y is real & x is real ) or ( y = +infty & x <> -infty ) or ( x = +infty & y <> -infty ) or ( y = -infty & x <> +infty ) or ( x = -infty & y <> +infty ) or b1 = 0 ) ) ; end; :: deftheorem Def2 defines + XXREAL_3:def_2_:_ for x, y, b3 being ext-real number holds ( ( x is real & y is real implies ( b3 = x + y iff ex a, b being complex number st ( x = a & y = b & b3 = a + b ) ) ) & ( ( ( x = +infty & y <> -infty ) or ( y = +infty & x <> -infty ) ) implies ( b3 = x + y iff b3 = +infty ) ) & ( ( ( x = -infty & y <> +infty ) or ( y = -infty & x <> +infty ) ) implies ( b3 = x + y iff b3 = -infty ) ) & ( ( x is real & y is real ) or ( x = +infty & y <> -infty ) or ( y = +infty & x <> -infty ) or ( x = -infty & y <> +infty ) or ( y = -infty & x <> +infty ) or ( b3 = x + y iff b3 = 0 ) ) ); definition let x be ext-real number ; func - x -> ext-real number means :Def3: :: XXREAL_3:def 3 ex a being complex number st ( x = a & it = - a ) if x is real it = -infty if x = +infty otherwise it = +infty ; existence ( ( x is real implies ex b1 being ext-real number ex a being complex number st ( x = a & b1 = - a ) ) & ( x = +infty implies ex b1 being ext-real number st b1 = -infty ) & ( not x is real & not x = +infty implies ex b1 being ext-real number st b1 = +infty ) ) proof thus ( x is real implies ex c being ext-real number ex a being complex number st ( x = a & c = - a ) ) ::_thesis: ( ( x = +infty implies ex b1 being ext-real number st b1 = -infty ) & ( not x is real & not x = +infty implies ex b1 being ext-real number st b1 = +infty ) ) proof assume x is real ; ::_thesis: ex c being ext-real number ex a being complex number st ( x = a & c = - a ) then reconsider a = x as real number ; take - a ; ::_thesis: ex a being complex number st ( x = a & - a = - a ) take a ; ::_thesis: ( x = a & - a = - a ) thus ( x = a & - a = - a ) ; ::_thesis: verum end; thus ( ( x = +infty implies ex b1 being ext-real number st b1 = -infty ) & ( not x is real & not x = +infty implies ex b1 being ext-real number st b1 = +infty ) ) ; ::_thesis: verum end; uniqueness for b1, b2 being ext-real number holds ( ( x is real & ex a being complex number st ( x = a & b1 = - a ) & ex a being complex number st ( x = a & b2 = - a ) implies b1 = b2 ) & ( x = +infty & b1 = -infty & b2 = -infty implies b1 = b2 ) & ( not x is real & not x = +infty & b1 = +infty & b2 = +infty implies b1 = b2 ) ) ; consistency for b1 being ext-real number st x is real & x = +infty holds ( ex a being complex number st ( x = a & b1 = - a ) iff b1 = -infty ) ; involutiveness for b1, b2 being ext-real number st ( b2 is real implies ex a being complex number st ( b2 = a & b1 = - a ) ) & ( b2 = +infty implies b1 = -infty ) & ( not b2 is real & not b2 = +infty implies b1 = +infty ) holds ( ( b1 is real implies ex a being complex number st ( b1 = a & b2 = - a ) ) & ( b1 = +infty implies b2 = -infty ) & ( not b1 is real & not b1 = +infty implies b2 = +infty ) ) proof let y, x be ext-real number ; ::_thesis: ( ( x is real implies ex a being complex number st ( x = a & y = - a ) ) & ( x = +infty implies y = -infty ) & ( not x is real & not x = +infty implies y = +infty ) implies ( ( y is real implies ex a being complex number st ( y = a & x = - a ) ) & ( y = +infty implies x = -infty ) & ( not y is real & not y = +infty implies x = +infty ) ) ) assume that A1: ( x is real implies ex a being complex number st ( x = a & y = - a ) ) and A2: ( x = +infty implies y = -infty ) and A3: ( not x is real & x <> +infty implies y = +infty ) ; ::_thesis: ( ( y is real implies ex a being complex number st ( y = a & x = - a ) ) & ( y = +infty implies x = -infty ) & ( not y is real & not y = +infty implies x = +infty ) ) thus ( y is real implies ex a being complex number st ( y = a & x = - a ) ) ::_thesis: ( ( y = +infty implies x = -infty ) & ( not y is real & not y = +infty implies x = +infty ) ) proof assume y is real ; ::_thesis: ex a being complex number st ( y = a & x = - a ) then consider a being complex number such that A4: ( x = a & y = - a ) by A1, A2, A3; take - a ; ::_thesis: ( y = - a & x = - (- a) ) thus ( y = - a & x = - (- a) ) by A4; ::_thesis: verum end; ( x in REAL implies x is real ) ; hence ( y = +infty implies x = -infty ) by A1, A2, XXREAL_0:14; ::_thesis: ( not y is real & not y = +infty implies x = +infty ) thus ( not y is real & not y = +infty implies x = +infty ) by A1, A3; ::_thesis: verum end; end; :: deftheorem Def3 defines - XXREAL_3:def_3_:_ for x, b2 being ext-real number holds ( ( x is real implies ( b2 = - x iff ex a being complex number st ( x = a & b2 = - a ) ) ) & ( x = +infty implies ( b2 = - x iff b2 = -infty ) ) & ( not x is real & not x = +infty implies ( b2 = - x iff b2 = +infty ) ) ); definition let x, y be ext-real number ; funcx - y -> ext-real number equals :: XXREAL_3:def 4 x + (- y); coherence x + (- y) is ext-real number ; end; :: deftheorem defines - XXREAL_3:def_4_:_ for x, y being ext-real number holds x - y = x + (- y); registration let x, y be real number ; let a, b be complex number ; identifyx + y with a + b when x = a, y = b; compatibility ( x = a & y = b implies x + y = a + b ) by Def2; end; registration let x be real number ; let a be complex number ; identify - x with - a when x = a; compatibility ( x = a implies - x = - a ) by Def3; end; registration let r be real number ; cluster - r -> ext-real real ; coherence - r is real ; end; registration let r, s be real number ; clusterr + s -> ext-real real ; coherence r + s is real ; clusterr - s -> ext-real real ; coherence r - s is real ; end; registration let x be real number ; let y be ext-real non real number ; clusterx + y -> non real for number ; coherence for b1 being number st b1 = x + y holds not b1 is real proof not y in REAL ; then A1: ( y = -infty or y = +infty ) by XXREAL_0:14; let z be number ; ::_thesis: ( z = x + y implies not z is real ) assume z = x + y ; ::_thesis: not z is real hence not z is real by A1, Def2; ::_thesis: verum end; end; registration let x, y be ext-real positive non real number ; clusterx + y -> ext-real non real ; coherence not x + y is real proof x = +infty by Th1; hence not x + y is real by Def2; ::_thesis: verum end; end; registration let x, y be ext-real negative non real number ; clusterx + y -> ext-real non real ; coherence not x + y is real proof x = -infty by Th2; hence not x + y is real by Def2; ::_thesis: verum end; end; registration let x be ext-real negative non real number ; let y be ext-real positive non real number ; clusterx + y -> zero ext-real ; coherence x + y is zero proof ( x = -infty & y = +infty ) by Th1, Th2; hence x + y is zero by Def2; ::_thesis: verum end; end; registration let x, y be real number ; let a, b be complex number ; identifyx - y with a - b when x = a, y = b; compatibility ( x = a & y = b implies x - y = a - b ) ; end; theorem Th4: :: XXREAL_3:4 for x being ext-real number holds x + 0 = x proof let x be ext-real number ; ::_thesis: x + 0 = x percases ( x in REAL or x = -infty or x = +infty ) by XXREAL_0:14; suppose x in REAL ; ::_thesis: x + 0 = x then reconsider r = x as real number ; r + 0 = r ; hence x + 0 = x ; ::_thesis: verum end; suppose ( x = -infty or x = +infty ) ; ::_thesis: x + 0 = x hence x + 0 = x by Def2; ::_thesis: verum end; end; end; theorem Th5: :: XXREAL_3:5 - -infty = +infty by Def3; theorem Th6: :: XXREAL_3:6 - +infty = -infty by Def3; Lm1: +infty + +infty = +infty by Def2; Lm2: -infty + -infty = -infty by Def2; theorem Th7: :: XXREAL_3:7 for x being ext-real number holds x + (- x) = 0 proof let x be ext-real number ; ::_thesis: x + (- x) = 0 percases ( x = -infty or x in REAL or x = +infty ) by XXREAL_0:14; suppose x = -infty ; ::_thesis: x + (- x) = 0 hence x + (- x) = 0 by Th5; ::_thesis: verum end; suppose x in REAL ; ::_thesis: x + (- x) = 0 then reconsider x = x as real number ; reconsider y = - x as real number ; x + y = 0 ; hence x + (- x) = 0 ; ::_thesis: verum end; suppose x = +infty ; ::_thesis: x + (- x) = 0 hence x + (- x) = 0 by Th6; ::_thesis: verum end; end; end; theorem :: XXREAL_3:8 for x, y being ext-real number st x + y = 0 holds x = - y proof let x, y be ext-real number ; ::_thesis: ( x + y = 0 implies x = - y ) assume A1: x + y = 0 ; ::_thesis: x = - y percases ( x in REAL or x = -infty or x = +infty ) by XXREAL_0:14; suppose x in REAL ; ::_thesis: x = - y then reconsider x = x as real number ; x + y is real by A1; then reconsider y = y as real number ; x + y = 0 by A1; then x = - y ; hence x = - y ; ::_thesis: verum end; supposeA2: x = -infty ; ::_thesis: x = - y then y = +infty by A1, Def2; hence x = - y by A2, Def3; ::_thesis: verum end; supposeA3: x = +infty ; ::_thesis: x = - y then y = -infty by A1, Def2; hence x = - y by A3, Def3; ::_thesis: verum end; end; end; Lm3: for x being ext-real number holds ( - x in REAL iff x in REAL ) proof let x be ext-real number ; ::_thesis: ( - x in REAL iff x in REAL ) hereby ::_thesis: ( x in REAL implies - x in REAL ) assume - x in REAL ; ::_thesis: x in REAL then reconsider a = - x as real number ; - a in REAL by XREAL_0:def_1; hence x in REAL ; ::_thesis: verum end; assume x in REAL ; ::_thesis: - x in REAL then reconsider a = x as real number ; - a is real ; hence - x in REAL by XREAL_0:def_1; ::_thesis: verum end; Lm4: - (+infty + -infty) = +infty - +infty by Def3 .= (- -infty) - +infty by Def3 ; Lm5: - +infty = -infty by Def3; Lm6: for x being ext-real number st x in REAL holds - (x + +infty) = (- +infty) + (- x) proof let x be ext-real number ; ::_thesis: ( x in REAL implies - (x + +infty) = (- +infty) + (- x) ) assume A1: x in REAL ; ::_thesis: - (x + +infty) = (- +infty) + (- x) then x + +infty = +infty by Def2; hence - (x + +infty) = (- +infty) + (- x) by A1, Def2, Th6; ::_thesis: verum end; Lm7: for x being ext-real number st x in REAL holds - (x + -infty) = (- -infty) + (- x) proof let x be ext-real number ; ::_thesis: ( x in REAL implies - (x + -infty) = (- -infty) + (- x) ) assume A1: x in REAL ; ::_thesis: - (x + -infty) = (- -infty) + (- x) then x + -infty = -infty by Def2; hence - (x + -infty) = (- -infty) + (- x) by A1, Def2, Th5; ::_thesis: verum end; theorem Th9: :: XXREAL_3:9 for x, y being ext-real number holds - (x + y) = (- x) + (- y) proof let x, y be ext-real number ; ::_thesis: - (x + y) = (- x) + (- y) percases ( ( x = +infty & y = +infty ) or ( x = +infty & y = -infty ) or ( x = +infty & y in REAL ) or ( x = -infty & y = +infty ) or ( x = -infty & y = -infty ) or ( x = -infty & y in REAL ) or ( x in REAL & y = +infty ) or ( x in REAL & y = -infty ) or ( x in REAL & y in REAL ) ) by XXREAL_0:14; supposeA1: ( x = +infty & y = +infty ) ; ::_thesis: - (x + y) = (- x) + (- y) hence - (x + y) = - +infty by Def2 .= (- x) + (- y) by A1, Def2, Lm5 ; ::_thesis: verum end; suppose ( x = +infty & y = -infty ) ; ::_thesis: - (x + y) = (- x) + (- y) hence - (x + y) = (- x) + (- y) by Lm4; ::_thesis: verum end; suppose ( x = +infty & y in REAL ) ; ::_thesis: - (x + y) = (- x) + (- y) hence - (x + y) = (- x) + (- y) by Lm6; ::_thesis: verum end; suppose ( x = -infty & y = +infty ) ; ::_thesis: - (x + y) = (- x) + (- y) hence - (x + y) = (- x) + (- y) by Lm4; ::_thesis: verum end; supposeA2: ( x = -infty & y = -infty ) ; ::_thesis: - (x + y) = (- x) + (- y) hence - (x + y) = - -infty by Def2 .= (- x) + (- y) by A2, Def2, Th5 ; ::_thesis: verum end; suppose ( x = -infty & y in REAL ) ; ::_thesis: - (x + y) = (- x) + (- y) hence - (x + y) = (- x) + (- y) by Lm7; ::_thesis: verum end; suppose ( x in REAL & y = +infty ) ; ::_thesis: - (x + y) = (- x) + (- y) hence - (x + y) = (- x) + (- y) by Lm6; ::_thesis: verum end; suppose ( x in REAL & y = -infty ) ; ::_thesis: - (x + y) = (- x) + (- y) hence - (x + y) = (- x) + (- y) by Lm7; ::_thesis: verum end; suppose ( x in REAL & y in REAL ) ; ::_thesis: - (x + y) = (- x) + (- y) then reconsider a = x, b = y as real number ; - (x + y) = - (a + b) .= (- a) + (- b) ; hence - (x + y) = (- x) + (- y) ; ::_thesis: verum end; end; end; theorem Th10: :: XXREAL_3:10 for f, g being ext-real number st - f = - g holds f = g proof let f, g be ext-real number ; ::_thesis: ( - f = - g implies f = g ) assume A1: - f = - g ; ::_thesis: f = g percases ( f in REAL or f = +infty or f = -infty ) by XXREAL_0:14; supposeA2: f in REAL ; ::_thesis: f = g now__::_thesis:_g_in_REAL assume not g in REAL ; ::_thesis: contradiction then ( g = +infty or g = -infty ) by XXREAL_0:14; hence contradiction by A1, A2, Def3; ::_thesis: verum end; then A3: ex a being complex number st ( g = a & - g = - a ) by Def3; ex a being complex number st ( f = a & - f = - a ) by A2, Def3; hence f = g by A1, A3; ::_thesis: verum end; suppose f = +infty ; ::_thesis: f = g hence f = g by A1, Th5; ::_thesis: verum end; suppose f = -infty ; ::_thesis: f = g then - (- g) = -infty by A1; hence f = g by A1; ::_thesis: verum end; end; end; Lm8: for x, y being ext-real number holds ( not x + y = +infty or x = +infty or y = +infty ) proof let x, y be ext-real number ; ::_thesis: ( not x + y = +infty or x = +infty or y = +infty ) assume A1: x + y = +infty ; ::_thesis: ( x = +infty or y = +infty ) assume ( not x = +infty & not y = +infty ) ; ::_thesis: contradiction then ( ( x in REAL & y in REAL ) or ( x in REAL & y = -infty ) or ( x = -infty & y in REAL ) or ( x = -infty & y = -infty ) ) by XXREAL_0:14; hence contradiction by A1, Def2; ::_thesis: verum end; Lm9: for x, y being ext-real number holds ( not x + y = -infty or x = -infty or y = -infty ) proof let x, y be ext-real number ; ::_thesis: ( not x + y = -infty or x = -infty or y = -infty ) assume A1: x + y = -infty ; ::_thesis: ( x = -infty or y = -infty ) assume ( not x = -infty & not y = -infty ) ; ::_thesis: contradiction then ( ( x in REAL & y in REAL ) or ( x in REAL & y = +infty ) or ( x = +infty & y in REAL ) or ( x = +infty & y = +infty ) ) by XXREAL_0:14; hence contradiction by A1, Def2; ::_thesis: verum end; theorem Th11: :: XXREAL_3:11 for r being real number for f, g being ext-real number st r + f = r + g holds f = g proof let r be real number ; ::_thesis: for f, g being ext-real number st r + f = r + g holds f = g let f, g be ext-real number ; ::_thesis: ( r + f = r + g implies f = g ) assume A1: r + f = r + g ; ::_thesis: f = g percases ( f in REAL or f = +infty or f = -infty ) by XXREAL_0:14; supposeA2: f in REAL ; ::_thesis: f = g now__::_thesis:_g_in_REAL assume not g in REAL ; ::_thesis: contradiction then ( g = +infty or g = -infty ) by XXREAL_0:14; hence contradiction by A1, A2; ::_thesis: verum end; then A3: ex c, d being complex number st ( r = c & g = d & r + g = c + d ) by Def2; ex a, b being complex number st ( r = a & f = b & r + f = a + b ) by A2, Def2; hence f = g by A1, A3; ::_thesis: verum end; supposeA4: f = +infty ; ::_thesis: f = g then r + f = +infty by Def2; hence f = g by A1, A4, Lm8; ::_thesis: verum end; supposeA5: f = -infty ; ::_thesis: f = g then r + f = -infty by Def2; hence f = g by A1, A5, Lm9; ::_thesis: verum end; end; end; theorem :: XXREAL_3:12 for r being real number for f, g being ext-real number st r - f = r - g holds f = g proof let r be real number ; ::_thesis: for f, g being ext-real number st r - f = r - g holds f = g let f, g be ext-real number ; ::_thesis: ( r - f = r - g implies f = g ) assume r - f = r - g ; ::_thesis: f = g then - f = - g by Th11; hence f = g by Th10; ::_thesis: verum end; theorem Th13: :: XXREAL_3:13 for x being ext-real number st x <> +infty holds ( +infty - x = +infty & x - +infty = -infty ) proof let x be ext-real number ; ::_thesis: ( x <> +infty implies ( +infty - x = +infty & x - +infty = -infty ) ) assume A1: x <> +infty ; ::_thesis: ( +infty - x = +infty & x - +infty = -infty ) then - x <> -infty by Th5; hence +infty - x = +infty by Def2; ::_thesis: x - +infty = -infty - +infty = -infty by Def3; hence x - +infty = -infty by A1, Def2; ::_thesis: verum end; theorem Th14: :: XXREAL_3:14 for x being ext-real number st x <> -infty holds ( -infty - x = -infty & x - -infty = +infty ) proof let x be ext-real number ; ::_thesis: ( x <> -infty implies ( -infty - x = -infty & x - -infty = +infty ) ) assume A1: x <> -infty ; ::_thesis: ( -infty - x = -infty & x - -infty = +infty ) now__::_thesis:_not_-_x_=_+infty assume - x = +infty ; ::_thesis: contradiction then - (- x) = -infty by Def3; hence contradiction by A1; ::_thesis: verum end; hence -infty - x = -infty by Def2; ::_thesis: x - -infty = +infty thus x - -infty = +infty by A1, Def2, Th5; ::_thesis: verum end; theorem Th15: :: XXREAL_3:15 for x being ext-real number holds x - 0 = x proof let x be ext-real number ; ::_thesis: x - 0 = x percases ( x in REAL or x = -infty or x = +infty ) by XXREAL_0:14; suppose x in REAL ; ::_thesis: x - 0 = x then reconsider a = x as real number ; x - 0 = a - 0 .= x ; hence x - 0 = x ; ::_thesis: verum end; suppose x = -infty ; ::_thesis: x - 0 = x hence x - 0 = x by Th14; ::_thesis: verum end; suppose x = +infty ; ::_thesis: x - 0 = x hence x - 0 = x by Th13; ::_thesis: verum end; end; end; theorem :: XXREAL_3:16 for x, y being ext-real number holds ( not x + y = +infty or x = +infty or y = +infty ) by Lm8; theorem :: XXREAL_3:17 for x, y being ext-real number holds ( not x + y = -infty or x = -infty or y = -infty ) by Lm9; theorem Th18: :: XXREAL_3:18 for x, y being ext-real number holds ( not x - y = +infty or x = +infty or y = -infty ) proof let x, y be ext-real number ; ::_thesis: ( not x - y = +infty or x = +infty or y = -infty ) assume A1: x - y = +infty ; ::_thesis: ( x = +infty or y = -infty ) assume ( not x = +infty & not y = -infty ) ; ::_thesis: contradiction then ( ( x in REAL & y in REAL ) or ( x in REAL & y = +infty ) or ( x = -infty & y in REAL ) or ( x = -infty & y = +infty ) ) by XXREAL_0:14; hence contradiction by A1, Th13, Th14; ::_thesis: verum end; theorem Th19: :: XXREAL_3:19 for x, y being ext-real number holds ( not x - y = -infty or x = -infty or y = +infty ) proof let x, y be ext-real number ; ::_thesis: ( not x - y = -infty or x = -infty or y = +infty ) assume A1: x - y = -infty ; ::_thesis: ( x = -infty or y = +infty ) assume ( not x = -infty & not y = +infty ) ; ::_thesis: contradiction then ( ( x in REAL & y in REAL ) or ( x in REAL & y = -infty ) or ( x = +infty & y in REAL ) or ( x = +infty & y = -infty ) ) by XXREAL_0:14; hence contradiction by A1, Th13, Th14; ::_thesis: verum end; theorem Th20: :: XXREAL_3:20 for x, y being ext-real number holds ( ( x = +infty & y = -infty ) or ( x = -infty & y = +infty ) or not x + y in REAL or ( x in REAL & y in REAL ) ) proof let x, y be ext-real number ; ::_thesis: ( ( x = +infty & y = -infty ) or ( x = -infty & y = +infty ) or not x + y in REAL or ( x in REAL & y in REAL ) ) assume A1: ( not ( x = +infty & y = -infty ) & not ( x = -infty & y = +infty ) & x + y in REAL ) ; ::_thesis: ( x in REAL & y in REAL ) A2: ( x in REAL or x = -infty or x = +infty ) by XXREAL_0:14; A3: ( y in REAL or y = -infty or y = +infty ) by XXREAL_0:14; assume ( not x in REAL or not y in REAL ) ; ::_thesis: contradiction hence contradiction by A1, A2, A3; ::_thesis: verum end; theorem Th21: :: XXREAL_3:21 for x, y being ext-real number holds ( ( x = +infty & y = +infty ) or ( x = -infty & y = -infty ) or not x - y in REAL or ( x in REAL & y in REAL ) ) proof let x, y be ext-real number ; ::_thesis: ( ( x = +infty & y = +infty ) or ( x = -infty & y = -infty ) or not x - y in REAL or ( x in REAL & y in REAL ) ) assume A1: ( not ( x = +infty & y = +infty ) & not ( x = -infty & y = -infty ) & x - y in REAL ) ; ::_thesis: ( x in REAL & y in REAL ) A2: ( x in REAL or x = -infty or x = +infty ) by XXREAL_0:14; A3: ( y in REAL or y = -infty or y = +infty ) by XXREAL_0:14; assume ( not x in REAL or not y in REAL ) ; ::_thesis: contradiction hence contradiction by A1, A2, A3, Th13, Th14; ::_thesis: verum end; theorem Th22: :: XXREAL_3:22 for x, y being ext-real number st x is real holds ( (y - x) + x = y & (y + x) - x = y ) proof let x, y be ext-real number ; ::_thesis: ( x is real implies ( (y - x) + x = y & (y + x) - x = y ) ) assume A1: x is real ; ::_thesis: ( (y - x) + x = y & (y + x) - x = y ) percases ( ( x in REAL & y in REAL ) or ( x in REAL & y = -infty ) or ( x in REAL & y = +infty ) ) by A1, XXREAL_0:14; suppose ( x in REAL & y in REAL ) ; ::_thesis: ( (y - x) + x = y & (y + x) - x = y ) then reconsider a = x, b = y as real number ; A2: (y + x) - x = (b + a) - a .= y ; (y - x) + x = (b - a) + a .= y ; hence ( (y - x) + x = y & (y + x) - x = y ) by A2; ::_thesis: verum end; supposeA3: ( x in REAL & y = -infty ) ; ::_thesis: ( (y - x) + x = y & (y + x) - x = y ) then y - x = -infty by Def2; hence ( (y - x) + x = y & (y + x) - x = y ) by A3, Def2; ::_thesis: verum end; supposeA4: ( x in REAL & y = +infty ) ; ::_thesis: ( (y - x) + x = y & (y + x) - x = y ) then y - x = +infty by Def2; hence ( (y - x) + x = y & (y + x) - x = y ) by A4, Def2; ::_thesis: verum end; end; end; theorem Th23: :: XXREAL_3:23 for x being ext-real number holds ( ( x = +infty implies - x = -infty ) & ( - x = -infty implies x = +infty ) & ( x = -infty implies - x = +infty ) & ( - x = +infty implies x = -infty ) ) proof let x be ext-real number ; ::_thesis: ( ( x = +infty implies - x = -infty ) & ( - x = -infty implies x = +infty ) & ( x = -infty implies - x = +infty ) & ( - x = +infty implies x = -infty ) ) ( - x = +infty implies x = -infty ) proof assume - x = +infty ; ::_thesis: x = -infty then - (- x) = -infty by Def3; hence x = -infty ; ::_thesis: verum end; hence ( ( x = +infty implies - x = -infty ) & ( - x = -infty implies x = +infty ) & ( x = -infty implies - x = +infty ) & ( - x = +infty implies x = -infty ) ) by Th5; ::_thesis: verum end; theorem :: XXREAL_3:24 for z, x being ext-real number st z is real holds x = (x + z) - z proof let z, x be ext-real number ; ::_thesis: ( z is real implies x = (x + z) - z ) assume A1: z is real ; ::_thesis: x = (x + z) - z percases ( x = +infty or x = -infty or x is Element of REAL ) by XXREAL_0:14; supposeA2: x = +infty ; ::_thesis: x = (x + z) - z then x + z = +infty by A1, Def2; hence x = (x + z) - z by A1, A2, Th13; ::_thesis: verum end; supposeA3: x = -infty ; ::_thesis: x = (x + z) - z then x + z = -infty by A1, Def2; hence x = (x + z) - z by A1, A3, Th14; ::_thesis: verum end; suppose x is Element of REAL ; ::_thesis: x = (x + z) - z then reconsider a = x, c = z as real number by A1; (x + z) - z = (a + c) - c ; hence x = (x + z) - z ; ::_thesis: verum end; end; end; Lm10: - +infty = -infty by Def3; Lm11: for x being ext-real number st x in REAL holds - (x + -infty) = (- -infty) + (- x) proof let x be ext-real number ; ::_thesis: ( x in REAL implies - (x + -infty) = (- -infty) + (- x) ) A1: - -infty = +infty by Th23; assume A2: x in REAL ; ::_thesis: - (x + -infty) = (- -infty) + (- x) then x + -infty = -infty by Def2; hence - (x + -infty) = (- -infty) + (- x) by A2, A1, Def2; ::_thesis: verum end; theorem Th25: :: XXREAL_3:25 for x, y being ext-real number holds - (x + y) = (- y) - x proof let x, y be ext-real number ; ::_thesis: - (x + y) = (- y) - x percases ( ( x = +infty & y = +infty ) or ( x = +infty & y = -infty ) or ( x = +infty & y in REAL ) or ( x = -infty & y = +infty ) or ( x = -infty & y = -infty ) or ( x = -infty & y in REAL ) or ( x in REAL & y = +infty ) or ( x in REAL & y = -infty ) or ( x in REAL & y in REAL ) ) by XXREAL_0:14; supposeA1: ( x = +infty & y = +infty ) ; ::_thesis: - (x + y) = (- y) - x hence - (x + y) = - +infty by Def2 .= (- y) - x by A1, Def2, Lm10 ; ::_thesis: verum end; suppose ( x = +infty & y = -infty ) ; ::_thesis: - (x + y) = (- y) - x hence - (x + y) = (- y) - x by Lm4; ::_thesis: verum end; suppose ( x = +infty & y in REAL ) ; ::_thesis: - (x + y) = (- y) - x hence - (x + y) = (- y) - x by Lm6; ::_thesis: verum end; suppose ( x = -infty & y = +infty ) ; ::_thesis: - (x + y) = (- y) - x hence - (x + y) = (- y) - x by Lm4; ::_thesis: verum end; supposeA2: ( x = -infty & y = -infty ) ; ::_thesis: - (x + y) = (- y) - x hence - (x + y) = - -infty by Def2 .= (- y) - x by A2, Def2, Th5 ; ::_thesis: verum end; suppose ( x = -infty & y in REAL ) ; ::_thesis: - (x + y) = (- y) - x hence - (x + y) = (- y) - x by Lm11; ::_thesis: verum end; suppose ( x in REAL & y = +infty ) ; ::_thesis: - (x + y) = (- y) - x hence - (x + y) = (- y) - x by Lm6; ::_thesis: verum end; suppose ( x in REAL & y = -infty ) ; ::_thesis: - (x + y) = (- y) - x hence - (x + y) = (- y) - x by Lm11; ::_thesis: verum end; suppose ( x in REAL & y in REAL ) ; ::_thesis: - (x + y) = (- y) - x then reconsider a = x, b = y as real number ; - (x + y) = - (a + b) .= (- a) + (- b) ; hence - (x + y) = (- y) - x ; ::_thesis: verum end; end; end; theorem :: XXREAL_3:26 for x, y being ext-real number holds ( - (x - y) = (- x) + y & - (x - y) = y - x ) proof let x, y be ext-real number ; ::_thesis: ( - (x - y) = (- x) + y & - (x - y) = y - x ) - (x - y) = (- (- y)) - x by Th25; hence ( - (x - y) = (- x) + y & - (x - y) = y - x ) ; ::_thesis: verum end; theorem Th27: :: XXREAL_3:27 for x, y being ext-real number holds ( - ((- x) + y) = x - y & - ((- x) + y) = x + (- y) ) proof let x, y be ext-real number ; ::_thesis: ( - ((- x) + y) = x - y & - ((- x) + y) = x + (- y) ) - ((- x) + y) = (- (- x)) - y by Th25 .= x - y ; hence ( - ((- x) + y) = x - y & - ((- x) + y) = x + (- y) ) ; ::_thesis: verum end; theorem :: XXREAL_3:28 for y, z being ext-real number st 0 <= y & y < +infty holds z = (z + y) - y proof let y, z be ext-real number ; ::_thesis: ( 0 <= y & y < +infty implies z = (z + y) - y ) assume ( 0 <= y & y < +infty ) ; ::_thesis: z = (z + y) - y then y in REAL by XXREAL_0:14; hence z = (z + y) - y by Th22; ::_thesis: verum end; theorem Th29: :: XXREAL_3:29 for x, y, z being ext-real number st ( not x = +infty or not y = -infty ) & ( not x = -infty or not y = +infty ) & not ( y = +infty & z = -infty ) & not ( y = -infty & z = +infty ) & not ( x = +infty & z = -infty ) & not ( x = -infty & z = +infty ) holds (x + y) + z = x + (y + z) proof let x, y, z be ext-real number ; ::_thesis: ( ( not x = +infty or not y = -infty ) & ( not x = -infty or not y = +infty ) & not ( y = +infty & z = -infty ) & not ( y = -infty & z = +infty ) & not ( x = +infty & z = -infty ) & not ( x = -infty & z = +infty ) implies (x + y) + z = x + (y + z) ) assume A1: ( not ( x = +infty & y = -infty ) & not ( x = -infty & y = +infty ) & not ( y = +infty & z = -infty ) & not ( y = -infty & z = +infty ) & not ( x = +infty & z = -infty ) & not ( x = -infty & z = +infty ) ) ; ::_thesis: (x + y) + z = x + (y + z) percases ( ( x in REAL & y in REAL & z in REAL ) or ( x in REAL & y = +infty & z in REAL ) or ( x in REAL & y = -infty & z in REAL ) or ( x = -infty & y in REAL & z in REAL ) or ( x = +infty & y in REAL & z in REAL ) or ( x in REAL & y in REAL & z = +infty ) or ( x in REAL & y in REAL & z = -infty ) or ( x = +infty & y = +infty & z in REAL ) or ( x in REAL & y = -infty & z = -infty ) or ( x = -infty & y = -infty & z in REAL ) or ( x = -infty & y in REAL & z = -infty ) or ( x = -infty & y = -infty & z = -infty ) or ( x = +infty & y in REAL & z = +infty ) or ( x = +infty & y = +infty & z = +infty ) or ( x in REAL & y = +infty & z = +infty ) ) by A1, XXREAL_0:14; suppose ( x in REAL & y in REAL & z in REAL ) ; ::_thesis: (x + y) + z = x + (y + z) then reconsider A = x, B = y, C = z as real number ; ( (A + B) + C = (x + y) + z & A + (B + C) = x + (y + z) ) ; hence (x + y) + z = x + (y + z) ; ::_thesis: verum end; supposeA2: ( x in REAL & y = +infty & z in REAL ) ; ::_thesis: (x + y) + z = x + (y + z) then ( x + y = +infty & y + z = +infty ) by Def2; hence (x + y) + z = x + (y + z) by A2; ::_thesis: verum end; supposeA3: ( x in REAL & y = -infty & z in REAL ) ; ::_thesis: (x + y) + z = x + (y + z) then ( x + y = -infty & y + z = -infty ) by Def2; hence (x + y) + z = x + (y + z) by A3; ::_thesis: verum end; supposeA4: ( x = -infty & y in REAL & z in REAL ) ; ::_thesis: (x + y) + z = x + (y + z) then x + y = -infty by Def2; then (x + y) + z = -infty by A4, Def2; hence (x + y) + z = x + (y + z) by A4, Def2; ::_thesis: verum end; supposeA5: ( x = +infty & y in REAL & z in REAL ) ; ::_thesis: (x + y) + z = x + (y + z) then x + y = +infty by Def2; then (x + y) + z = +infty by A5, Def2; hence (x + y) + z = x + (y + z) by A5, Def2; ::_thesis: verum end; supposeA6: ( x in REAL & y in REAL & z = +infty ) ; ::_thesis: (x + y) + z = x + (y + z) then y + z = +infty by Def2; then x + (y + z) = +infty by A6, Def2; hence (x + y) + z = x + (y + z) by A6, Def2; ::_thesis: verum end; supposeA7: ( x in REAL & y in REAL & z = -infty ) ; ::_thesis: (x + y) + z = x + (y + z) then y + z = -infty by Def2; then x + (y + z) = -infty by A7, Def2; hence (x + y) + z = x + (y + z) by A7, Def2; ::_thesis: verum end; supposeA8: ( x = +infty & y = +infty & z in REAL ) ; ::_thesis: (x + y) + z = x + (y + z) then x + y = +infty by Def2; then A9: (x + y) + z = +infty by A8, Def2; y + z <> -infty by A8, Def2; hence (x + y) + z = x + (y + z) by A8, A9, Def2; ::_thesis: verum end; supposeA10: ( x in REAL & y = -infty & z = -infty ) ; ::_thesis: (x + y) + z = x + (y + z) then A11: x + y = -infty by Def2; then (x + y) + z = -infty by A10, Def2; hence (x + y) + z = x + (y + z) by A10, A11; ::_thesis: verum end; supposeA12: ( x = -infty & y = -infty & z in REAL ) ; ::_thesis: (x + y) + z = x + (y + z) then A13: x + y = -infty by Def2; then (x + y) + z = -infty by A12, Def2; hence (x + y) + z = x + (y + z) by A12, A13; ::_thesis: verum end; suppose ( ( x = -infty & y in REAL & z = -infty ) or ( x = -infty & y = -infty & z = -infty ) or ( x = +infty & y in REAL & z = +infty ) or ( x = +infty & y = +infty & z = +infty ) ) ; ::_thesis: (x + y) + z = x + (y + z) hence (x + y) + z = x + (y + z) ; ::_thesis: verum end; supposeA14: ( x in REAL & y = +infty & z = +infty ) ; ::_thesis: (x + y) + z = x + (y + z) then ( x + y = +infty & y + z = +infty ) by Def2; hence (x + y) + z = x + (y + z) by A14; ::_thesis: verum end; end; end; theorem Th30: :: XXREAL_3:30 for x, y, z being ext-real number st ( not x = +infty or not y = -infty ) & ( not x = -infty or not y = +infty ) & ( not y = +infty or not z = +infty ) & ( not y = -infty or not z = -infty ) & ( not x = +infty or not z = +infty ) & ( not x = -infty or not z = -infty ) holds (x + y) - z = x + (y - z) proof let x, y, z be ext-real number ; ::_thesis: ( ( not x = +infty or not y = -infty ) & ( not x = -infty or not y = +infty ) & ( not y = +infty or not z = +infty ) & ( not y = -infty or not z = -infty ) & ( not x = +infty or not z = +infty ) & ( not x = -infty or not z = -infty ) implies (x + y) - z = x + (y - z) ) assume that A1: ( ( not x = +infty or not y = -infty ) & ( not x = -infty or not y = +infty ) ) and A2: ( ( not y = +infty or not z = +infty ) & ( not y = -infty or not z = -infty ) ) and A3: ( ( not x = +infty or not z = +infty ) & ( not x = -infty or not z = -infty ) ) ; ::_thesis: (x + y) - z = x + (y - z) A4: ( ( not x = +infty or not - z = -infty ) & ( not x = -infty or not - z = +infty ) ) by A3, Th23; ( ( not y = +infty or not - z = -infty ) & ( not y = -infty or not - z = +infty ) ) by A2, Th23; hence (x + y) - z = x + (y - z) by A1, A4, Th29; ::_thesis: verum end; theorem :: XXREAL_3:31 for x, y, z being ext-real number st ( not x = +infty or not y = +infty ) & ( not x = -infty or not y = -infty ) & ( not y = +infty or not z = -infty ) & ( not y = -infty or not z = +infty ) & ( not x = +infty or not z = +infty ) & ( not x = -infty or not z = -infty ) holds (x - y) - z = x - (y + z) proof let x, y, z be ext-real number ; ::_thesis: ( ( not x = +infty or not y = +infty ) & ( not x = -infty or not y = -infty ) & ( not y = +infty or not z = -infty ) & ( not y = -infty or not z = +infty ) & ( not x = +infty or not z = +infty ) & ( not x = -infty or not z = -infty ) implies (x - y) - z = x - (y + z) ) assume that A1: ( not x = +infty or not y = +infty ) and A2: ( not x = -infty or not y = -infty ) and A3: ( not y = +infty or not z = -infty ) and A4: ( not y = -infty or not z = +infty ) and A5: ( not x = +infty or not z = +infty ) and A6: ( not x = -infty or not z = -infty ) ; ::_thesis: (x - y) - z = x - (y + z) percases ( x = +infty or x = -infty or ( x <> +infty & x <> -infty ) ) ; supposeA7: x = +infty ; ::_thesis: (x - y) - z = x - (y + z) then x - y = +infty by A1, Th13; then A8: (x - y) - z = +infty by A5, A7, Th13; y + z <> +infty by A1, A5, A7, Lm8; hence (x - y) - z = x - (y + z) by A7, A8, Th13; ::_thesis: verum end; supposeA9: x = -infty ; ::_thesis: (x - y) - z = x - (y + z) then x - y = -infty by A2, Th14; then A10: (x - y) - z = -infty by A6, A9, Th14; y + z <> -infty by A2, A6, A9, Lm9; hence (x - y) - z = x - (y + z) by A9, A10, Th14; ::_thesis: verum end; supposeA11: ( x <> +infty & x <> -infty ) ; ::_thesis: (x - y) - z = x - (y + z) then x in REAL by XXREAL_0:14; then reconsider a = x as real number ; percases ( y = +infty or y = -infty or ( y <> +infty & y <> -infty ) ) ; supposeA12: y = +infty ; ::_thesis: (x - y) - z = x - (y + z) then ( x - y = -infty & y + z = +infty ) by A3, A11, Def2, Th13; hence (x - y) - z = x - (y + z) by A3, A12, Th14; ::_thesis: verum end; supposeA13: y = -infty ; ::_thesis: (x - y) - z = x - (y + z) then ( x - y = +infty & y + z = -infty ) by A4, A11, Def2, Th14; hence (x - y) - z = x - (y + z) by A4, A13, Th13; ::_thesis: verum end; suppose ( y <> +infty & y <> -infty ) ; ::_thesis: (x - y) - z = x - (y + z) then y in REAL by XXREAL_0:14; then reconsider b = y as real number ; A14: x - y = a - b ; percases ( z = +infty or z = -infty or ( z <> +infty & z <> -infty ) ) ; suppose z = +infty ; ::_thesis: (x - y) - z = x - (y + z) then ( (x - y) - z = -infty & y + z = +infty ) by A14, Def2, Th13; hence (x - y) - z = x - (y + z) by A11, Th13; ::_thesis: verum end; suppose z = -infty ; ::_thesis: (x - y) - z = x - (y + z) then ( (x - y) - z = +infty & y + z = -infty ) by A14, Def2, Th14; hence (x - y) - z = x - (y + z) by A11, Th14; ::_thesis: verum end; suppose ( z <> +infty & z <> -infty ) ; ::_thesis: (x - y) - z = x - (y + z) then z in REAL by XXREAL_0:14; then reconsider c = z as real number ; ( (x - y) - z = (a - b) - c & x - (y + z) = a - (b + c) ) ; hence (x - y) - z = x - (y + z) ; ::_thesis: verum end; end; end; end; end; end; end; theorem Th32: :: XXREAL_3:32 for x, y, z being ext-real number st ( not x = +infty or not y = +infty ) & ( not x = -infty or not y = -infty ) & ( not y = +infty or not z = +infty ) & ( not y = -infty or not z = -infty ) & ( not x = +infty or not z = -infty ) & ( not x = -infty or not z = +infty ) holds (x - y) + z = x - (y - z) proof let x, y, z be ext-real number ; ::_thesis: ( ( not x = +infty or not y = +infty ) & ( not x = -infty or not y = -infty ) & ( not y = +infty or not z = +infty ) & ( not y = -infty or not z = -infty ) & ( not x = +infty or not z = -infty ) & ( not x = -infty or not z = +infty ) implies (x - y) + z = x - (y - z) ) assume that A1: ( not x = +infty or not y = +infty ) and A2: ( not x = -infty or not y = -infty ) and A3: ( not y = +infty or not z = +infty ) and A4: ( not y = -infty or not z = -infty ) and A5: ( not x = +infty or not z = -infty ) and A6: ( not x = -infty or not z = +infty ) ; ::_thesis: (x - y) + z = x - (y - z) percases ( x = +infty or x = -infty or ( x <> +infty & x <> -infty ) ) ; supposeA7: x = +infty ; ::_thesis: (x - y) + z = x - (y - z) then x - y = +infty by A1, Th13; then A8: (x - y) + z = +infty by A5, A7, Def2; y - z <> +infty by A1, A5, A7, Th18; hence (x - y) + z = x - (y - z) by A7, A8, Th13; ::_thesis: verum end; supposeA9: x = -infty ; ::_thesis: (x - y) + z = x - (y - z) then x - y = -infty by A2, Th14; then A10: (x - y) + z = -infty by A6, A9, Def2; y - z <> -infty by A2, A6, A9, Th19; hence (x - y) + z = x - (y - z) by A9, A10, Th14; ::_thesis: verum end; supposeA11: ( x <> +infty & x <> -infty ) ; ::_thesis: (x - y) + z = x - (y - z) then x in REAL by XXREAL_0:14; then reconsider a = x as real number ; percases ( y = +infty or y = -infty or ( y <> +infty & y <> -infty ) ) ; supposeA12: y = +infty ; ::_thesis: (x - y) + z = x - (y - z) then ( x - y = -infty & y - z = +infty ) by A3, A11, Th13; hence (x - y) + z = x - (y - z) by A3, A12, Def2; ::_thesis: verum end; supposeA13: y = -infty ; ::_thesis: (x - y) + z = x - (y - z) then ( x - y = +infty & y - z = -infty ) by A4, A11, Th14; hence (x - y) + z = x - (y - z) by A4, A13, Def2; ::_thesis: verum end; suppose ( y <> +infty & y <> -infty ) ; ::_thesis: (x - y) + z = x - (y - z) then y in REAL by XXREAL_0:14; then reconsider b = y as real number ; A14: x - y = a - b ; percases ( z = +infty or z = -infty or ( z <> +infty & z <> -infty ) ) ; suppose z = +infty ; ::_thesis: (x - y) + z = x - (y - z) then ( (x - y) + z = +infty & y - z = -infty ) by A14, Def2, Th13; hence (x - y) + z = x - (y - z) by A11, Th14; ::_thesis: verum end; suppose z = -infty ; ::_thesis: (x - y) + z = x - (y - z) then ( (x - y) + z = -infty & y - z = +infty ) by A14, Def2, Th14; hence (x - y) + z = x - (y - z) by A11, Th13; ::_thesis: verum end; suppose ( z <> +infty & z <> -infty ) ; ::_thesis: (x - y) + z = x - (y - z) then z in REAL by XXREAL_0:14; then reconsider c = z as real number ; ( (x - y) + z = (a - b) + c & x - (y - z) = a - (b - c) ) ; hence (x - y) + z = x - (y - z) ; ::_thesis: verum end; end; end; end; end; end; end; theorem Th33: :: XXREAL_3:33 for z, x, y being ext-real number st z is real holds (z + x) - (z + y) = x - y proof let z, x, y be ext-real number ; ::_thesis: ( z is real implies (z + x) - (z + y) = x - y ) assume A1: z is real ; ::_thesis: (z + x) - (z + y) = x - y percases ( x = -infty or y = +infty or ( x in REAL & y in REAL & z in REAL ) or ( x = +infty & y in REAL & z in REAL ) or ( x in REAL & y = -infty & z in REAL ) or ( x = +infty & y = -infty & z in REAL ) ) by A1, XXREAL_0:14; supposeA2: x = -infty ; ::_thesis: (z + x) - (z + y) = x - y percases ( y = -infty or y = +infty or y in REAL ) by XXREAL_0:14; supposeA3: y = -infty ; ::_thesis: (z + x) - (z + y) = x - y (z + -infty) - (z + -infty) = -infty - (z + -infty) by A1, Def2 .= -infty - -infty by A1, Def2 ; hence (z + x) - (z + y) = x - y by A2, A3; ::_thesis: verum end; supposeA4: y = +infty ; ::_thesis: (z + x) - (z + y) = x - y (z + -infty) - (z + +infty) = -infty - (z + +infty) by A1, Def2 .= -infty - +infty by A1, Def2 ; hence (z + x) - (z + y) = x - y by A2, A4; ::_thesis: verum end; supposeA5: y in REAL ; ::_thesis: (z + x) - (z + y) = x - y then consider a, b being complex number such that A6: ( z = a & y = b ) and z + y = a + b by A1, Def2; reconsider a = a, b = b as real number by A1, A5, A6; A7: a + b in REAL by XREAL_0:def_1; (z + -infty) - (z + y) = -infty - (z + y) by A1, Def2 .= -infty by A6, A7, Def2 .= -infty - y by A5, Def2 ; hence (z + x) - (z + y) = x - y by A2; ::_thesis: verum end; end; end; supposeA8: y = +infty ; ::_thesis: (z + x) - (z + y) = x - y percases ( x = -infty or x = +infty or x in REAL ) by XXREAL_0:14; supposeA9: x = -infty ; ::_thesis: (z + x) - (z + y) = x - y (z + -infty) - (z + +infty) = (z + -infty) - +infty by A1, Def2 .= -infty - +infty by A1, Def2 ; hence (z + x) - (z + y) = x - y by A8, A9; ::_thesis: verum end; supposeA10: x = +infty ; ::_thesis: (z + x) - (z + y) = x - y (z + +infty) - (z + +infty) = (z + +infty) - +infty by A1, Def2 .= +infty - +infty by A1, Def2 ; hence (z + x) - (z + y) = x - y by A8, A10; ::_thesis: verum end; supposeA11: x in REAL ; ::_thesis: (z + x) - (z + y) = x - y then consider a, b being complex number such that A12: ( z = a & x = b ) and z + x = a + b by A1, Def2; reconsider a = a, b = b as real number by A1, A11, A12; A13: a + b in REAL by XREAL_0:def_1; A14: - +infty = -infty by Def3; (z + x) - (z + +infty) = (z + x) - +infty by A1, Def2 .= (z + x) + -infty by Def3 .= -infty by A12, A13, Def2 .= x + (- +infty) by A11, A14, Def2 ; hence (z + x) - (z + y) = x - y by A8; ::_thesis: verum end; end; end; suppose ( x in REAL & y in REAL & z in REAL ) ; ::_thesis: (z + x) - (z + y) = x - y then reconsider a = x, b = y, c = z as real number ; (z + x) - (z + y) = (a + c) - (c + b) .= a - b .= x - y ; hence (z + x) - (z + y) = x - y ; ::_thesis: verum end; supposeA15: ( x = +infty & y in REAL & z in REAL ) ; ::_thesis: (z + x) - (z + y) = x - y then reconsider c = z, b = y as real number ; A16: z + y = c + b ; ( z + x = +infty & x - y = +infty ) by A15, Def2; hence (z + x) - (z + y) = x - y by A16, Th13; ::_thesis: verum end; supposeA17: ( x in REAL & y = -infty & z in REAL ) ; ::_thesis: (z + x) - (z + y) = x - y then reconsider c = z, a = x as real number ; ( z + x = c + a & z + y = -infty ) by A17, Def2; then (z + x) - (z + y) = +infty by Th14 .= x - y by A17, Th14 ; hence (z + x) - (z + y) = x - y ; ::_thesis: verum end; supposeA18: ( x = +infty & y = -infty & z in REAL ) ; ::_thesis: (z + x) - (z + y) = x - y then ( z + y = -infty & not z + x = -infty ) by Def2; then (z + x) - (z + y) = +infty by Th14 .= x - y by A18, Th14 ; hence (z + x) - (z + y) = x - y ; ::_thesis: verum end; end; end; theorem :: XXREAL_3:34 for y, z, x being ext-real number st y is real holds (z - y) + (y - x) = z - x proof let y, z, x be ext-real number ; ::_thesis: ( y is real implies (z - y) + (y - x) = z - x ) assume A1: y is real ; ::_thesis: (z - y) + (y - x) = z - x thus (z - y) + (y - x) = (z - y) - (x - y) by Th27 .= z - x by A1, Th33 ; ::_thesis: verum end; begin Lm12: for x, y, z being ext-real number st x <= y holds x + z <= y + z proof let x, y, z be ext-real number ; ::_thesis: ( x <= y implies x + z <= y + z ) assume A1: x <= y ; ::_thesis: x + z <= y + z percases ( ( x in REAL & y in REAL ) or ( x in REAL & y = +infty ) or ( x = -infty & y in REAL ) or ( x = -infty & y = +infty ) or x = +infty or y = -infty ) by XXREAL_0:14; supposeA2: ( x in REAL & y in REAL ) ; ::_thesis: x + z <= y + z percases ( z = -infty or z in REAL or z = +infty ) by XXREAL_0:14; supposeA3: z = -infty ; ::_thesis: x + z <= y + z -infty <= y + z by XXREAL_0:5; hence x + z <= y + z by A2, A3, Def2; ::_thesis: verum end; suppose z in REAL ; ::_thesis: x + z <= y + z then reconsider x = x, y = y, z = z as real number by A2; x + z <= y + z by A1, XREAL_1:6; hence x + z <= y + z ; ::_thesis: verum end; supposeA4: z = +infty ; ::_thesis: x + z <= y + z x + z <= +infty by XXREAL_0:3; hence x + z <= y + z by A2, A4, Def2; ::_thesis: verum end; end; end; supposeA5: ( x in REAL & y = +infty ) ; ::_thesis: x + z <= y + z percases ( z = -infty or z in REAL or z = +infty ) by XXREAL_0:14; supposeA6: z = -infty ; ::_thesis: x + z <= y + z -infty <= y + z by XXREAL_0:5; hence x + z <= y + z by A5, A6, Def2; ::_thesis: verum end; supposeA7: z in REAL ; ::_thesis: x + z <= y + z x + z <= +infty by XXREAL_0:3; hence x + z <= y + z by A5, A7, Def2; ::_thesis: verum end; suppose z = +infty ; ::_thesis: x + z <= y + z hence x + z <= y + z by A5, Lm1, XXREAL_0:3; ::_thesis: verum end; end; end; supposeA8: ( x = -infty & y in REAL ) ; ::_thesis: x + z <= y + z percases ( z = -infty or z in REAL or z = +infty ) by XXREAL_0:14; suppose z = -infty ; ::_thesis: x + z <= y + z hence x + z <= y + z by A8, Lm2, XXREAL_0:5; ::_thesis: verum end; supposeA9: z in REAL ; ::_thesis: x + z <= y + z -infty <= y + z by XXREAL_0:5; hence x + z <= y + z by A8, A9, Def2; ::_thesis: verum end; supposeA10: z = +infty ; ::_thesis: x + z <= y + z x + z <= +infty by XXREAL_0:3; hence x + z <= y + z by A8, A10, Def2; ::_thesis: verum end; end; end; supposeA11: ( x = -infty & y = +infty ) ; ::_thesis: x + z <= y + z percases ( z = -infty or z in REAL or z = +infty ) by XXREAL_0:14; suppose z = -infty ; ::_thesis: x + z <= y + z hence x + z <= y + z by A11, Lm2; ::_thesis: verum end; supposeA12: z in REAL ; ::_thesis: x + z <= y + z -infty <= y + z by XXREAL_0:5; hence x + z <= y + z by A11, A12, Def2; ::_thesis: verum end; suppose z = +infty ; ::_thesis: x + z <= y + z hence x + z <= y + z by A11, Lm1; ::_thesis: verum end; end; end; suppose x = +infty ; ::_thesis: x + z <= y + z hence x + z <= y + z by A1, XXREAL_0:4; ::_thesis: verum end; suppose y = -infty ; ::_thesis: x + z <= y + z hence x + z <= y + z by A1, XXREAL_0:6; ::_thesis: verum end; end; end; Lm13: for x, y being ext-real number st x >= 0 & y > 0 holds x + y > 0 proof let x, y be ext-real number ; ::_thesis: ( x >= 0 & y > 0 implies x + y > 0 ) assume x >= 0 ; ::_thesis: ( not y > 0 or x + y > 0 ) then x + y >= 0 + y by Lm12; hence ( not y > 0 or x + y > 0 ) by Th4; ::_thesis: verum end; Lm14: for x, y being ext-real number st x <= 0 & y < 0 holds x + y < 0 proof let x, y be ext-real number ; ::_thesis: ( x <= 0 & y < 0 implies x + y < 0 ) assume x <= 0 ; ::_thesis: ( not y < 0 or x + y < 0 ) then x + y <= 0 + y by Lm12; hence ( not y < 0 or x + y < 0 ) by Th4; ::_thesis: verum end; registration let x, y be ext-real non negative number ; clusterx + y -> ext-real non negative ; coherence not x + y is negative proof percases ( x = 0 or x > 0 ) ; suppose x = 0 ; ::_thesis: not x + y is negative hence x + y >= 0 by Th4; :: according to XXREAL_0:def_7 ::_thesis: verum end; suppose x > 0 ; ::_thesis: not x + y is negative hence x + y >= 0 by Lm13; :: according to XXREAL_0:def_7 ::_thesis: verum end; end; end; end; registration let x, y be ext-real non positive number ; clusterx + y -> ext-real non positive ; coherence not x + y is positive proof percases ( x = 0 or x < 0 ) ; suppose x = 0 ; ::_thesis: not x + y is positive hence x + y <= 0 by Th4; :: according to XXREAL_0:def_6 ::_thesis: verum end; suppose x < 0 ; ::_thesis: not x + y is positive hence x + y <= 0 by Lm14; :: according to XXREAL_0:def_6 ::_thesis: verum end; end; end; end; registration let x be ext-real positive number ; let y be ext-real non negative number ; clusterx + y -> ext-real positive ; coherence x + y is positive by Lm13; clustery + x -> ext-real positive ; coherence y + x is positive ; end; registration let x be ext-real negative number ; let y be ext-real non positive number ; clusterx + y -> ext-real negative ; coherence x + y is negative by Lm14; clustery + x -> ext-real negative ; coherence y + x is negative ; end; registration let x be ext-real non positive number ; cluster - x -> ext-real non negative ; coherence not - x is negative proof assume - x < 0 ; :: according to XXREAL_0:def_7 ::_thesis: contradiction then (- x) - (- x) < 0 ; hence contradiction by Th7; ::_thesis: verum end; end; registration let x be ext-real non negative number ; cluster - x -> ext-real non positive ; coherence not - x is positive proof assume - x > 0 ; :: according to XXREAL_0:def_6 ::_thesis: contradiction then (- x) - (- x) > 0 ; hence contradiction by Th7; ::_thesis: verum end; end; registration let x be ext-real positive number ; cluster - x -> ext-real negative ; coherence - x is negative proof assume - x >= 0 ; :: according to XXREAL_0:def_7 ::_thesis: contradiction then (- x) - (- x) > 0 ; hence contradiction by Th7; ::_thesis: verum end; end; registration let x be ext-real negative number ; cluster - x -> ext-real positive ; coherence - x is positive proof assume - x <= 0 ; :: according to XXREAL_0:def_6 ::_thesis: contradiction then (- x) - (- x) < 0 ; hence contradiction by Th7; ::_thesis: verum end; end; registration let x be ext-real non negative number ; let y be ext-real non positive number ; clusterx - y -> ext-real non negative ; coherence not x - y is negative ; clustery - x -> ext-real non positive ; coherence not y - x is positive ; end; registration let x be ext-real positive number ; let y be ext-real non positive number ; clusterx - y -> ext-real positive ; coherence x - y is positive ; clustery - x -> ext-real negative ; coherence y - x is negative ; end; registration let x be ext-real negative number ; let y be ext-real non negative number ; clusterx - y -> ext-real negative ; coherence x - y is negative ; clustery - x -> ext-real positive ; coherence y - x is positive ; end; Lm15: for x, y being ext-real number st x <= y holds - y <= - x proof let x, y be ext-real number ; ::_thesis: ( x <= y implies - y <= - x ) assume A1: x <= y ; ::_thesis: - y <= - x percases ( ( - y in REAL & - x in REAL ) or not - y in REAL or not - x in REAL ) ; :: according to XXREAL_3:def_1 casethat A2: - y in REAL and A3: - x in REAL ; ::_thesis: ex p, q being Element of REAL st ( p = - y & q = - x & p <= q ) x in REAL by A3, Lm3; then consider a being complex number such that A4: x = a and A5: - x = - a by Def3; y in REAL by A2, Lm3; then consider b being complex number such that A6: y = b and A7: - y = - b by Def3; ( x in REAL & y in REAL ) by A2, A3, Lm3; then reconsider a = a, b = b as real number by A6, A4; reconsider mb = - b, ma = - a as Element of REAL by XREAL_0:def_1; take mb ; ::_thesis: ex q being Element of REAL st ( mb = - y & q = - x & mb <= q ) take ma ; ::_thesis: ( mb = - y & ma = - x & mb <= ma ) thus ( mb = - y & ma = - x ) by A7, A5; ::_thesis: mb <= ma thus mb <= ma by A1, A6, A4, XREAL_1:24; ::_thesis: verum end; case ( not - y in REAL or not - x in REAL ) ; ::_thesis: ( - y = -infty or - x = +infty ) then ( not y in REAL or not x in REAL ) by Lm3; then ( x = -infty or y = +infty ) by A1, Def1; hence ( - y = -infty or - x = +infty ) by Def3; ::_thesis: verum end; end; end; theorem :: XXREAL_3:35 for x, y, z being ext-real number st x <= y holds x + z <= y + z by Lm12; theorem Th36: :: XXREAL_3:36 for x, y, z, w being ext-real number st x <= y & z <= w holds x + z <= y + w proof let x, y, z, w be ext-real number ; ::_thesis: ( x <= y & z <= w implies x + z <= y + w ) assume that A1: x <= y and A2: z <= w ; ::_thesis: x + z <= y + w percases ( ( x = +infty & z = -infty ) or ( x = -infty & z = +infty ) or ( y = +infty & w = -infty ) or ( y = -infty & w = +infty ) or ( not ( x = +infty & z = -infty ) & not ( x = -infty & z = +infty ) & not ( y = +infty & w = -infty ) & not ( y = -infty & w = +infty ) ) ) ; supposeA3: ( x = +infty & z = -infty ) ; ::_thesis: x + z <= y + w A4: ( w <> -infty implies +infty + w = +infty ) by Def2; y = +infty by A1, A3, XXREAL_0:4; hence x + z <= y + w by A3, A4; ::_thesis: verum end; supposeA5: ( x = -infty & z = +infty ) ; ::_thesis: x + z <= y + w A6: ( y <> -infty implies +infty + y = +infty ) by Def2; w = +infty by A2, A5, XXREAL_0:4; hence x + z <= y + w by A5, A6; ::_thesis: verum end; supposeA7: ( y = +infty & w = -infty ) ; ::_thesis: x + z <= y + w A8: ( x <> +infty implies -infty + x = -infty ) by Def2; z = -infty by A2, A7, XXREAL_0:6; hence x + z <= y + w by A7, A8; ::_thesis: verum end; supposeA9: ( y = -infty & w = +infty ) ; ::_thesis: x + z <= y + w A10: ( z <> +infty implies -infty + z = -infty ) by Def2; x = -infty by A1, A9, XXREAL_0:6; hence x + z <= y + w by A9, A10; ::_thesis: verum end; supposeA11: ( not ( x = +infty & z = -infty ) & not ( x = -infty & z = +infty ) & not ( y = +infty & w = -infty ) & not ( y = -infty & w = +infty ) ) ; ::_thesis: x + z <= y + w reconsider a = x + z, b = y + w as Element of ExtREAL by XXREAL_0:def_1; A12: ( not a = +infty or not b = -infty ) proof assume that A13: a = +infty and A14: b = -infty ; ::_thesis: contradiction ( x = +infty or z = +infty ) by A13, Lm8; hence contradiction by A1, A2, A11, A14, Lm9, XXREAL_0:4; ::_thesis: verum end; A15: ( a in REAL & b in REAL implies a <= b ) proof assume A16: ( a in REAL & b in REAL ) ; ::_thesis: a <= b then A17: ( z in REAL & w in REAL ) by A11, Th20; ( x in REAL & y in REAL ) by A11, A16, Th20; then consider Ox, Oy, Os, Ot being real number such that A18: ( Ox = x & Oy = y & Os = z & Ot = w ) and A19: ( Ox <= Oy & Os <= Ot ) by A1, A2, A17; ( Ox + Os <= Os + Oy & Os + Oy <= Ot + Oy ) by A19, XREAL_1:6; hence a <= b by A18, XXREAL_0:2; ::_thesis: verum end; A20: ( a = +infty & b in REAL implies a <= b ) proof assume that A21: a = +infty and b in REAL ; ::_thesis: a <= b ( x = +infty or z = +infty ) by A21, Lm8; then ( y = +infty or w = +infty ) by A1, A2, XXREAL_0:4; then b = +infty by A11, Def2; hence a <= b by XXREAL_0:4; ::_thesis: verum end; A22: ( a in REAL & b = -infty implies a <= b ) proof assume that a in REAL and A23: b = -infty ; ::_thesis: a <= b ( y = -infty or w = -infty ) by A23, Lm9; then ( x = -infty or z = -infty ) by A1, A2, XXREAL_0:6; then a = -infty by A11, Def2; hence a <= b by XXREAL_0:5; ::_thesis: verum end; ( ( a in REAL & b in REAL ) or ( a in REAL & b = +infty ) or ( a in REAL & b = -infty ) or ( a = +infty & b in REAL ) or ( a = +infty & b = +infty ) or ( a = +infty & b = -infty ) or ( a = -infty & b in REAL ) or ( a = -infty & b = +infty ) or ( a = -infty & b = -infty ) ) by XXREAL_0:14; hence x + z <= y + w by A15, A22, A20, A12, XXREAL_0:4, XXREAL_0:5; ::_thesis: verum end; end; end; theorem Th37: :: XXREAL_3:37 for x, y, z, w being ext-real number st x <= y & z <= w holds x - w <= y - z proof let x, y, z, w be ext-real number ; ::_thesis: ( x <= y & z <= w implies x - w <= y - z ) assume that A1: x <= y and A2: z <= w ; ::_thesis: x - w <= y - z - w <= - z by A2, Lm15; hence x - w <= y - z by A1, Th36; ::_thesis: verum end; theorem Th38: :: XXREAL_3:38 for x, y being ext-real number holds ( x <= y iff - y <= - x ) proof let x, y be ext-real number ; ::_thesis: ( x <= y iff - y <= - x ) thus ( x <= y implies - y <= - x ) by Lm15; ::_thesis: ( - y <= - x implies x <= y ) ( - y <= - x implies - (- x) <= - (- y) ) by Lm15; hence ( - y <= - x implies x <= y ) ; ::_thesis: verum end; theorem Th39: :: XXREAL_3:39 for z, x being ext-real number st 0 <= z holds x <= x + z proof let z, x be ext-real number ; ::_thesis: ( 0 <= z implies x <= x + z ) assume 0 <= z ; ::_thesis: x <= x + z then x + 0 <= x + z by Th36; hence x <= x + z by Th4; ::_thesis: verum end; theorem :: XXREAL_3:40 for x, y being ext-real number st x <= y holds y - x >= 0 proof let x, y be ext-real number ; ::_thesis: ( x <= y implies y - x >= 0 ) assume x <= y ; ::_thesis: y - x >= 0 then - y <= - x by Lm15; then (- y) + y <= y + (- x) by Th36; hence y - x >= 0 by Th7; ::_thesis: verum end; theorem :: XXREAL_3:41 for z, y, x being ext-real number st ( z = -infty & y = +infty implies x <= 0 ) & ( z = +infty & y = -infty implies x <= 0 ) & x - y <= z holds x <= z + y proof let z, y, x be ext-real number ; ::_thesis: ( ( z = -infty & y = +infty implies x <= 0 ) & ( z = +infty & y = -infty implies x <= 0 ) & x - y <= z implies x <= z + y ) assume that A1: ( z = -infty & y = +infty implies x <= 0 ) and A2: ( z = +infty & y = -infty implies x <= 0 ) and A3: x - y <= z ; ::_thesis: x <= z + y percases ( z = -infty or z = +infty or z in REAL ) by XXREAL_0:14; supposeA4: z = -infty ; ::_thesis: x <= z + y percases ( x = -infty or y = +infty ) by A3, A4, Th19, XXREAL_0:6; suppose x = -infty ; ::_thesis: x <= z + y hence x <= z + y by XXREAL_0:5; ::_thesis: verum end; suppose y = +infty ; ::_thesis: x <= z + y hence x <= z + y by A1, A4; ::_thesis: verum end; end; end; supposeA5: z = +infty ; ::_thesis: x <= z + y percases ( y = -infty or y <> -infty ) ; suppose y = -infty ; ::_thesis: x <= z + y hence x <= z + y by A2, A5; ::_thesis: verum end; suppose y <> -infty ; ::_thesis: x <= z + y then z + y = +infty by A5, Def2; hence x <= z + y by XXREAL_0:3; ::_thesis: verum end; end; end; supposeA6: z in REAL ; ::_thesis: x <= z + y percases ( x - y in REAL or x - y = -infty ) by A3, A6, XXREAL_0:13; supposeA7: x - y in REAL ; ::_thesis: x <= z + y percases ( y = +infty or x = -infty or ( x in REAL & y in REAL ) ) by A7, Th21; suppose y = +infty ; ::_thesis: x <= z + y then z + y = +infty by A6, Def2; hence x <= z + y by XXREAL_0:3; ::_thesis: verum end; suppose x = -infty ; ::_thesis: x <= z + y hence x <= z + y by XXREAL_0:5; ::_thesis: verum end; suppose ( x in REAL & y in REAL ) ; ::_thesis: x <= z + y then reconsider a = x, b = y, c = z as Element of REAL by A6; a - b <= c by A3; then a <= b + c by XREAL_1:20; hence x <= z + y ; ::_thesis: verum end; end; end; supposeA8: x - y = -infty ; ::_thesis: x <= z + y percases ( x = -infty or y = +infty ) by A8, Th19; suppose x = -infty ; ::_thesis: x <= z + y hence x <= z + y by XXREAL_0:5; ::_thesis: verum end; suppose y = +infty ; ::_thesis: x <= z + y then z + y = +infty by A6, Def2; hence x <= z + y by XXREAL_0:3; ::_thesis: verum end; end; end; end; end; end; end; theorem :: XXREAL_3:42 for x, y, z being ext-real number st ( x = +infty & y = +infty implies 0 <= z ) & ( x = -infty & y = -infty implies 0 <= z ) & x <= z + y holds x - y <= z proof let x, y, z be ext-real number ; ::_thesis: ( ( x = +infty & y = +infty implies 0 <= z ) & ( x = -infty & y = -infty implies 0 <= z ) & x <= z + y implies x - y <= z ) assume that A1: ( x = +infty & y = +infty implies 0 <= z ) and A2: ( x = -infty & y = -infty implies 0 <= z ) and A3: x <= z + y ; ::_thesis: x - y <= z percases ( x = +infty or x = -infty or x in REAL ) by XXREAL_0:14; supposeA4: x = +infty ; ::_thesis: x - y <= z percases ( z = +infty or y = +infty ) by A3, A4, Lm8, XXREAL_0:4; suppose z = +infty ; ::_thesis: x - y <= z hence x - y <= z by XXREAL_0:3; ::_thesis: verum end; suppose y = +infty ; ::_thesis: x - y <= z hence x - y <= z by A1, A4, Th7; ::_thesis: verum end; end; end; supposeA5: x = -infty ; ::_thesis: x - y <= z percases ( y = -infty or - (- y) <> -infty ) ; suppose y = -infty ; ::_thesis: x - y <= z hence x - y <= z by A2, A5, Th7; ::_thesis: verum end; suppose - (- y) <> -infty ; ::_thesis: x - y <= z then - y <> +infty by Def3; then x - y = -infty by A5, Def2; hence x - y <= z by XXREAL_0:5; ::_thesis: verum end; end; end; supposeA6: x in REAL ; ::_thesis: x - y <= z percases ( z + y in REAL or z + y = +infty ) by A3, A6, XXREAL_0:10; supposeA7: z + y in REAL ; ::_thesis: x - y <= z percases ( y = +infty or z = +infty or ( z in REAL & y in REAL ) ) by A7, Th20; suppose y = +infty ; ::_thesis: x - y <= z then x - y = -infty by A6, Def2, Th5; hence x - y <= z by XXREAL_0:5; ::_thesis: verum end; suppose z = +infty ; ::_thesis: x - y <= z hence x - y <= z by XXREAL_0:3; ::_thesis: verum end; suppose ( z in REAL & y in REAL ) ; ::_thesis: x - y <= z then reconsider a = x, b = y, c = z as Element of REAL by A6; a <= b + c by A3; then a - b <= c by XREAL_1:20; hence x - y <= z ; ::_thesis: verum end; end; end; supposeA8: z + y = +infty ; ::_thesis: x - y <= z percases ( z = +infty or y = +infty ) by A8, Lm8; suppose z = +infty ; ::_thesis: x - y <= z hence x - y <= z by XXREAL_0:3; ::_thesis: verum end; suppose y = +infty ; ::_thesis: x - y <= z then x - y = -infty by A6, Def2, Th5; hence x - y <= z by XXREAL_0:5; ::_thesis: verum end; end; end; end; end; end; end; theorem Th43: :: XXREAL_3:43 for z, x, y being ext-real number st z in REAL & x < y holds ( x + z < y + z & x - z < y - z ) proof let z, x, y be ext-real number ; ::_thesis: ( z in REAL & x < y implies ( x + z < y + z & x - z < y - z ) ) assume that A1: z in REAL and A2: x < y ; ::_thesis: ( x + z < y + z & x - z < y - z ) A3: x + z <> y + z proof assume x + z = y + z ; ::_thesis: contradiction then x = (y + z) - z by A1, Th22 .= y by A1, Th22 ; hence contradiction by A2; ::_thesis: verum end; A4: x - z <> y - z proof assume x - z = y - z ; ::_thesis: contradiction then x = (y - z) + z by A1, Th22 .= y by A1, Th22 ; hence contradiction by A2; ::_thesis: verum end; ( x + z <= y + z & x - z <= y - z ) by A2, Th36; hence ( x + z < y + z & x - z < y - z ) by A3, A4, XXREAL_0:1; ::_thesis: verum end; theorem :: XXREAL_3:44 for x, y, z being ext-real number st 0 <= x & 0 <= y & 0 <= z holds (x + y) + z = x + (y + z) proof let x, y, z be ext-real number ; ::_thesis: ( 0 <= x & 0 <= y & 0 <= z implies (x + y) + z = x + (y + z) ) assume that A1: 0 <= x and A2: 0 <= y and A3: 0 <= z ; ::_thesis: (x + y) + z = x + (y + z) percases ( ( x in REAL & y in REAL & z in REAL ) or x = +infty or y = +infty or z = +infty ) by A1, A2, A3, XXREAL_0:14; suppose ( x in REAL & y in REAL & z in REAL ) ; ::_thesis: (x + y) + z = x + (y + z) then consider a, b, c, d, e being real number such that A4: ( x = a & y = b & z = c ) and x + y = d and y + z = e ; (x + y) + z = (a + b) + c by A4 .= a + (b + c) .= x + (y + z) by A4 ; hence (x + y) + z = x + (y + z) ; ::_thesis: verum end; supposeA5: x = +infty ; ::_thesis: (x + y) + z = x + (y + z) then (x + y) + z = +infty + z by A2, Def2 .= +infty by A3, Def2 .= +infty + (y + z) by A2, A3, Def2 ; hence (x + y) + z = x + (y + z) by A5; ::_thesis: verum end; supposeA6: y = +infty ; ::_thesis: (x + y) + z = x + (y + z) then (x + y) + z = +infty + z by A1, Def2 .= +infty by A3, Def2 .= x + +infty by A1, Def2 .= x + (+infty + z) by A3, Def2 ; hence (x + y) + z = x + (y + z) by A6; ::_thesis: verum end; supposeA7: z = +infty ; ::_thesis: (x + y) + z = x + (y + z) then (x + y) + z = +infty by A1, A2, Def2 .= x + +infty by A1, Def2 .= x + (y + +infty) by A2, Def2 ; hence (x + y) + z = x + (y + z) by A7; ::_thesis: verum end; end; end; theorem Th45: :: XXREAL_3:45 for x, y, z being ext-real number st x is real holds ( y + x <= z iff y <= z - x ) proof let x, y, z be ext-real number ; ::_thesis: ( x is real implies ( y + x <= z iff y <= z - x ) ) assume A1: x is real ; ::_thesis: ( y + x <= z iff y <= z - x ) A2: (z - x) + x = z proof percases ( z in REAL or z = -infty or z = +infty ) by XXREAL_0:14; suppose z in REAL ; ::_thesis: (z - x) + x = z then reconsider a = x, b = z as real number by A1; thus (z - x) + x = (b - a) + a .= z ; ::_thesis: verum end; supposeA3: z = -infty ; ::_thesis: (z - x) + x = z hence (z - x) + x = -infty + x by A1, Th14 .= z by A1, A3, Def2 ; ::_thesis: verum end; supposeA4: z = +infty ; ::_thesis: (z - x) + x = z hence (z - x) + x = +infty + x by A1, Th13 .= z by A1, A4, Def2 ; ::_thesis: verum end; end; end; hereby ::_thesis: ( y <= z - x implies y + x <= z ) A5: (y + x) - x = y proof percases ( y in REAL or y = -infty or y = +infty ) by XXREAL_0:14; suppose y in REAL ; ::_thesis: (y + x) - x = y then reconsider a = x, b = y as Element of REAL by A1, XXREAL_0:14; (y + x) - x = (b + a) - a .= y ; hence (y + x) - x = y ; ::_thesis: verum end; supposeA6: ( y = -infty or y = +infty ) ; ::_thesis: (y + x) - x = y percases ( y = -infty or y = +infty ) by A6; supposeA7: y = -infty ; ::_thesis: (y + x) - x = y hence (y + x) - x = -infty - x by A1, Def2 .= y by A1, A7, Th14 ; ::_thesis: verum end; supposeA8: y = +infty ; ::_thesis: (y + x) - x = y hence (y + x) - x = +infty - x by A1, Def2 .= y by A1, A8, Th13 ; ::_thesis: verum end; end; end; end; end; assume y + x <= z ; ::_thesis: y <= z - x hence y <= z - x by A5, Th37; ::_thesis: verum end; assume y <= z - x ; ::_thesis: y + x <= z hence y + x <= z by A2, Th36; ::_thesis: verum end; theorem Th46: :: XXREAL_3:46 for x, y being ext-real number st 0 < x & x < y holds 0 < y - x proof let x, y be ext-real number ; ::_thesis: ( 0 < x & x < y implies 0 < y - x ) assume that A1: 0 < x and A2: x < y ; ::_thesis: 0 < y - x A3: x in REAL by A1, A2, XXREAL_0:48; A4: 0 <> y - x proof assume 0 = y - x ; ::_thesis: contradiction then x = (y - x) + x by Th4 .= y by A3, Th22 ; hence contradiction by A2; ::_thesis: verum end; 0 + x < y by A2, Th4; hence 0 < y - x by A3, A4, Th45; ::_thesis: verum end; theorem :: XXREAL_3:47 for x, z, y being ext-real number st 0 <= x & 0 <= z & z + x < y holds z < y - x proof let x, z, y be ext-real number ; ::_thesis: ( 0 <= x & 0 <= z & z + x < y implies z < y - x ) assume that A1: 0 <= x and A2: 0 <= z and A3: z + x < y ; ::_thesis: z < y - x x in REAL proof A4: x <> +infty proof assume x = +infty ; ::_thesis: contradiction then +infty < y by A2, A3, Def2; hence contradiction by XXREAL_0:4; ::_thesis: verum end; assume not x in REAL ; ::_thesis: contradiction hence contradiction by A1, A4, XXREAL_0:10; ::_thesis: verum end; then ( z <= y - x & z <> y - x ) by A3, Th22, Th45; hence z < y - x by XXREAL_0:1; ::_thesis: verum end; theorem :: XXREAL_3:48 for x, z, y being ext-real number st 0 <= x & 0 <= z & z + x < y holds z <= y proof let x, z, y be ext-real number ; ::_thesis: ( 0 <= x & 0 <= z & z + x < y implies z <= y ) assume that A1: 0 <= x and A2: 0 <= z and A3: z + x < y ; ::_thesis: z <= y x in REAL proof A4: x <> +infty proof assume x = +infty ; ::_thesis: contradiction then +infty < y by A2, A3, Def2; hence contradiction by XXREAL_0:4; ::_thesis: verum end; assume not x in REAL ; ::_thesis: contradiction hence contradiction by A1, A4, XXREAL_0:10; ::_thesis: verum end; then A5: (z + x) - x = z by Th22; y - 0 = y by Th15; hence z <= y by A1, A3, A5, Th37; ::_thesis: verum end; theorem Th49: :: XXREAL_3:49 for x, z being ext-real number st 0 <= x & x < z holds ex y being real number st ( 0 < y & x + y < z ) proof let x, z be ext-real number ; ::_thesis: ( 0 <= x & x < z implies ex y being real number st ( 0 < y & x + y < z ) ) assume that A1: 0 <= x and A2: x < z ; ::_thesis: ex y being real number st ( 0 < y & x + y < z ) percases ( 0 < x or 0 = x ) by A1; supposeA3: 0 < x ; ::_thesis: ex y being real number st ( 0 < y & x + y < z ) then 0 < z - x by A2, Th46; then consider y being real number such that A4: 0 < y and A5: y < z - x by Th3; take y ; ::_thesis: ( 0 < y & x + y < z ) A6: x + y <= x + (z - x) by A5, Th36; A7: x in REAL by A2, A3, XXREAL_0:48; then A8: x + (z - x) = z by Th22; x + y <> z by A7, A5, Th22; hence ( 0 < y & x + y < z ) by A4, A6, A8, XXREAL_0:1; ::_thesis: verum end; supposeA9: 0 = x ; ::_thesis: ex y being real number st ( 0 < y & x + y < z ) consider y being real number such that A10: ( 0 < y & y < z ) by A1, A2, Th3; take y ; ::_thesis: ( 0 < y & x + y < z ) thus ( 0 < y & x + y < z ) by A9, A10, Th4; ::_thesis: verum end; end; end; theorem :: XXREAL_3:50 for x being ext-real number st 0 < x holds ex y being real number st ( 0 < y & y + y < x ) proof let x be ext-real number ; ::_thesis: ( 0 < x implies ex y being real number st ( 0 < y & y + y < x ) ) assume 0 < x ; ::_thesis: ex y being real number st ( 0 < y & y + y < x ) then consider x1 being real number such that A1: 0 < x1 and A2: x1 < x by Th3; consider x2 being real number such that A3: 0 < x2 and A4: x1 + x2 < x by A1, A2, Th49; take y = min (x1,x2); ::_thesis: ( 0 < y & y + y < x ) percases ( x1 <= x2 or x2 <= x1 ) ; supposeA5: x1 <= x2 ; ::_thesis: ( 0 < y & y + y < x ) hence 0 < y by A1, XXREAL_0:def_9; ::_thesis: y + y < x y = x1 by A5, XXREAL_0:def_9; then y + y <= x1 + x2 by A5, Th36; hence y + y < x by A4, XXREAL_0:2; ::_thesis: verum end; supposeA6: x2 <= x1 ; ::_thesis: ( 0 < y & y + y < x ) hence 0 < y by A3, XXREAL_0:def_9; ::_thesis: y + y < x y = x2 by A6, XXREAL_0:def_9; then y + y <= x1 + x2 by A6, Th36; hence y + y < x by A4, XXREAL_0:2; ::_thesis: verum end; end; end; theorem Th51: :: XXREAL_3:51 for x, y being ext-real number st x < y & x < +infty & -infty < y holds 0 < y - x proof let x, y be ext-real number ; ::_thesis: ( x < y & x < +infty & -infty < y implies 0 < y - x ) assume that A1: x < y and A2: x < +infty and A3: -infty < y ; ::_thesis: 0 < y - x percases ( y = +infty or y <> +infty ) ; suppose y = +infty ; ::_thesis: 0 < y - x hence 0 < y - x by A2, Th13; ::_thesis: verum end; supposeA4: y <> +infty ; ::_thesis: 0 < y - x percases ( x = -infty or x <> -infty ) ; suppose x = -infty ; ::_thesis: 0 < y - x hence 0 < y - x by A3, Th14; ::_thesis: verum end; supposeA5: x <> -infty ; ::_thesis: 0 < y - x A6: y in REAL by A3, A4, XXREAL_0:14; x in REAL by A2, A5, XXREAL_0:14; then reconsider a = x, b = y as real number by A6; b - a > 0 by A1, XREAL_1:50; hence 0 < y - x ; ::_thesis: verum end; end; end; end; end; theorem :: XXREAL_3:52 for x, y, z being ext-real number holds ( ( x = +infty & y = -infty ) or ( x = -infty & y = +infty ) or not x + y < z or ( x <> +infty & y <> +infty & z <> -infty & x < z - y ) ) proof let x, y, z be ext-real number ; ::_thesis: ( ( x = +infty & y = -infty ) or ( x = -infty & y = +infty ) or not x + y < z or ( x <> +infty & y <> +infty & z <> -infty & x < z - y ) ) assume that A1: ( not ( x = +infty & y = -infty ) & not ( x = -infty & y = +infty ) ) and A2: x + y < z ; ::_thesis: ( x <> +infty & y <> +infty & z <> -infty & x < z - y ) percases ( z = +infty or z <> +infty ) ; supposeA3: z = +infty ; ::_thesis: ( x <> +infty & y <> +infty & z <> -infty & x < z - y ) then x <> +infty by A1, A2, Def2; then A4: x < +infty by XXREAL_0:4; y <> +infty by A1, A2, A3, Def2; hence ( x <> +infty & y <> +infty & z <> -infty & x < z - y ) by A3, A4, Th13; ::_thesis: verum end; supposeA5: z <> +infty ; ::_thesis: ( x <> +infty & y <> +infty & z <> -infty & x < z - y ) A6: -infty <= x + y by XXREAL_0:5; then z in REAL by A2, A5, XXREAL_0:14; then reconsider c = z as real number ; A7: x + y < +infty by A2, XXREAL_0:2, XXREAL_0:4; then A8: x <> +infty by A1, Def2; A9: y <> +infty by A1, A7, Def2; percases ( y = -infty or y <> -infty ) ; supposeA10: y = -infty ; ::_thesis: ( x <> +infty & y <> +infty & z <> -infty & x < z - y ) then x < +infty by A1, XXREAL_0:4; hence ( x <> +infty & y <> +infty & z <> -infty & x < z - y ) by A2, A6, A10, Th14; ::_thesis: verum end; suppose y <> -infty ; ::_thesis: ( x <> +infty & y <> +infty & z <> -infty & x < z - y ) then y in REAL by A9, XXREAL_0:14; then reconsider b = y as real number ; percases ( x = -infty or x <> -infty ) ; supposeA11: x = -infty ; ::_thesis: ( x <> +infty & y <> +infty & z <> -infty & x < z - y ) hence x <> +infty ; ::_thesis: ( y <> +infty & z <> -infty & x < z - y ) A12: z - y = c - b ; hence y <> +infty ; ::_thesis: ( z <> -infty & x < z - y ) thus z <> -infty by A12; ::_thesis: x < z - y c - b in REAL by XREAL_0:def_1; hence x < z - y by A11, XXREAL_0:12; ::_thesis: verum end; suppose x <> -infty ; ::_thesis: ( x <> +infty & y <> +infty & z <> -infty & x < z - y ) then x in REAL by A8, XXREAL_0:14; then reconsider a = x as real number ; x + y = a + b ; then a < c - b by A2, XREAL_1:20; hence ( x <> +infty & y <> +infty & z <> -infty & x < z - y ) ; ::_thesis: verum end; end; end; end; end; end; end; theorem :: XXREAL_3:53 for z, y, x being ext-real number holds ( ( z = +infty & y = +infty ) or ( z = -infty & y = -infty ) or not x < z - y or ( x <> +infty & y <> +infty & z <> -infty & x + y < z ) ) proof let z, y, x be ext-real number ; ::_thesis: ( ( z = +infty & y = +infty ) or ( z = -infty & y = -infty ) or not x < z - y or ( x <> +infty & y <> +infty & z <> -infty & x + y < z ) ) assume that A1: ( not ( z = +infty & y = +infty ) & not ( z = -infty & y = -infty ) ) and A2: x < z - y ; ::_thesis: ( x <> +infty & y <> +infty & z <> -infty & x + y < z ) percases ( x = -infty or x <> -infty ) ; supposeA3: x = -infty ; ::_thesis: ( x <> +infty & y <> +infty & z <> -infty & x + y < z ) A4: -infty <= z by XXREAL_0:5; z <> -infty by A1, A2, A3, Th14; then A5: -infty < z by A4, XXREAL_0:1; y <> +infty by A1, A2, A3, Th13; hence ( x <> +infty & y <> +infty & z <> -infty & x + y < z ) by A3, A5, Def2; ::_thesis: verum end; supposeA6: x <> -infty ; ::_thesis: ( x <> +infty & y <> +infty & z <> -infty & x + y < z ) A7: z - y <= +infty by XXREAL_0:4; then x in REAL by A2, A6, XXREAL_0:14; then reconsider a = x as real number ; A8: -infty <= x by XXREAL_0:5; then A9: z <> -infty by A1, A2, Th14; A10: y <> +infty by A1, A2, A8, Th13; percases ( y = -infty or y <> -infty ) ; supposeA11: y = -infty ; ::_thesis: ( x <> +infty & y <> +infty & z <> -infty & x + y < z ) -infty <= z by XXREAL_0:5; then -infty < z by A1, A11, XXREAL_0:1; hence ( x <> +infty & y <> +infty & z <> -infty & x + y < z ) by A2, A7, A11, Def2; ::_thesis: verum end; suppose y <> -infty ; ::_thesis: ( x <> +infty & y <> +infty & z <> -infty & x + y < z ) then y in REAL by A10, XXREAL_0:14; then reconsider b = y as real number ; percases ( z = +infty or z <> +infty ) ; supposeA12: z = +infty ; ::_thesis: ( x <> +infty & y <> +infty & z <> -infty & x + y < z ) a + b in REAL by XREAL_0:def_1; hence ( x <> +infty & y <> +infty & z <> -infty & x + y < z ) by A12, XXREAL_0:9; ::_thesis: verum end; suppose z <> +infty ; ::_thesis: ( x <> +infty & y <> +infty & z <> -infty & x + y < z ) then z in REAL by A9, XXREAL_0:14; then reconsider c = z as real number ; z - y = c - b ; then a + b < c by A2, XREAL_1:20; hence ( x <> +infty & y <> +infty & z <> -infty & x + y < z ) ; ::_thesis: verum end; end; end; end; end; end; end; theorem :: XXREAL_3:54 for x, y, z being ext-real number holds ( ( x = +infty & y = +infty ) or ( x = -infty & y = -infty ) or not x - y < z or ( x <> +infty & y <> -infty & z <> -infty & x < z + y ) ) proof let x, y, z be ext-real number ; ::_thesis: ( ( x = +infty & y = +infty ) or ( x = -infty & y = -infty ) or not x - y < z or ( x <> +infty & y <> -infty & z <> -infty & x < z + y ) ) assume that A1: ( not ( x = +infty & y = +infty ) & not ( x = -infty & y = -infty ) ) and A2: x - y < z ; ::_thesis: ( x <> +infty & y <> -infty & z <> -infty & x < z + y ) percases ( z = +infty or z <> +infty ) ; supposeA3: z = +infty ; ::_thesis: ( x <> +infty & y <> -infty & z <> -infty & x < z + y ) then x <> +infty by A1, A2, Th13; then A4: x < +infty by XXREAL_0:4; y <> -infty by A1, A2, A3, Th14; hence ( x <> +infty & y <> -infty & z <> -infty & x < z + y ) by A3, A4, Def2; ::_thesis: verum end; supposeA5: z <> +infty ; ::_thesis: ( x <> +infty & y <> -infty & z <> -infty & x < z + y ) A6: -infty <= x - y by XXREAL_0:5; then z in REAL by A2, A5, XXREAL_0:14; then reconsider c = z as real number ; A7: x - y < +infty by A2, XXREAL_0:2, XXREAL_0:4; then A8: x <> +infty by A1, Th13; A9: y <> -infty by A1, A7, Th14; percases ( y = +infty or y <> +infty ) ; supposeA10: y = +infty ; ::_thesis: ( x <> +infty & y <> -infty & z <> -infty & x < z + y ) then x < +infty by A1, XXREAL_0:4; hence ( x <> +infty & y <> -infty & z <> -infty & x < z + y ) by A2, A6, A10, Def2; ::_thesis: verum end; suppose y <> +infty ; ::_thesis: ( x <> +infty & y <> -infty & z <> -infty & x < z + y ) then y in REAL by A9, XXREAL_0:14; then reconsider b = y as real number ; percases ( x = -infty or x <> -infty ) ; supposeA11: x = -infty ; ::_thesis: ( x <> +infty & y <> -infty & z <> -infty & x < z + y ) c + b in REAL by XREAL_0:def_1; hence ( x <> +infty & y <> -infty & z <> -infty & x < z + y ) by A11, XXREAL_0:12; ::_thesis: verum end; suppose x <> -infty ; ::_thesis: ( x <> +infty & y <> -infty & z <> -infty & x < z + y ) then x in REAL by A8, XXREAL_0:14; then reconsider a = x as real number ; x - y = a - b ; then a < c + b by A2, XREAL_1:19; hence ( x <> +infty & y <> -infty & z <> -infty & x < z + y ) ; ::_thesis: verum end; end; end; end; end; end; end; theorem :: XXREAL_3:55 for z, y, x being ext-real number holds ( ( z = +infty & y = -infty ) or ( z = -infty & y = +infty ) or not x < z + y or ( x <> +infty & y <> -infty & z <> -infty & x - y < z ) ) proof let z, y, x be ext-real number ; ::_thesis: ( ( z = +infty & y = -infty ) or ( z = -infty & y = +infty ) or not x < z + y or ( x <> +infty & y <> -infty & z <> -infty & x - y < z ) ) assume that A1: ( not ( z = +infty & y = -infty ) & not ( z = -infty & y = +infty ) ) and A2: x < z + y ; ::_thesis: ( x <> +infty & y <> -infty & z <> -infty & x - y < z ) percases ( x = -infty or x <> -infty ) ; supposeA3: x = -infty ; ::_thesis: ( x <> +infty & y <> -infty & z <> -infty & x - y < z ) A4: -infty <= z by XXREAL_0:5; z <> -infty by A1, A2, A3, Def2; then A5: -infty < z by A4, XXREAL_0:1; y <> -infty by A1, A2, A3, Def2; hence ( x <> +infty & y <> -infty & z <> -infty & x - y < z ) by A3, A5, Th14; ::_thesis: verum end; supposeA6: x <> -infty ; ::_thesis: ( x <> +infty & y <> -infty & z <> -infty & x - y < z ) A7: z + y <= +infty by XXREAL_0:4; then x in REAL by A2, A6, XXREAL_0:14; then reconsider a = x as real number ; A8: -infty <= x by XXREAL_0:5; then A9: z <> -infty by A1, A2, Def2; A10: y <> -infty by A1, A2, A8, Def2; percases ( y = +infty or y <> +infty ) ; supposeA11: y = +infty ; ::_thesis: ( x <> +infty & y <> -infty & z <> -infty & x - y < z ) -infty <= z by XXREAL_0:5; then -infty < z by A1, A11, XXREAL_0:1; hence ( x <> +infty & y <> -infty & z <> -infty & x - y < z ) by A2, A7, A11, Th13; ::_thesis: verum end; suppose y <> +infty ; ::_thesis: ( x <> +infty & y <> -infty & z <> -infty & x - y < z ) then y in REAL by A10, XXREAL_0:14; then reconsider b = y as real number ; percases ( z = +infty or z <> +infty ) ; supposeA12: z = +infty ; ::_thesis: ( x <> +infty & y <> -infty & z <> -infty & x - y < z ) a - b in REAL by XREAL_0:def_1; hence ( x <> +infty & y <> -infty & z <> -infty & x - y < z ) by A12, XXREAL_0:9; ::_thesis: verum end; suppose z <> +infty ; ::_thesis: ( x <> +infty & y <> -infty & z <> -infty & x - y < z ) then z in REAL by A9, XXREAL_0:14; then reconsider c = z as real number ; z + y = c + b ; then a - b < c by A2, XREAL_1:19; hence ( x <> +infty & y <> -infty & z <> -infty & x - y < z ) ; ::_thesis: verum end; end; end; end; end; end; end; theorem :: XXREAL_3:56 for x, y, z being ext-real number holds ( ( x = +infty & y = -infty ) or ( x = -infty & y = +infty ) or ( y = +infty & z = +infty ) or ( y = -infty & z = -infty ) or not x + y <= z or ( y <> +infty & x <= z - y ) ) proof let x, y, z be ext-real number ; ::_thesis: ( ( x = +infty & y = -infty ) or ( x = -infty & y = +infty ) or ( y = +infty & z = +infty ) or ( y = -infty & z = -infty ) or not x + y <= z or ( y <> +infty & x <= z - y ) ) assume that A1: ( not ( x = +infty & y = -infty ) & not ( x = -infty & y = +infty ) & not ( y = +infty & z = +infty ) & not ( y = -infty & z = -infty ) ) and A2: x + y <= z ; ::_thesis: ( y <> +infty & x <= z - y ) thus y <> +infty ::_thesis: x <= z - y proof assume A3: y = +infty ; ::_thesis: contradiction then x + y = +infty by A1, Def2; hence contradiction by A1, A2, A3, XXREAL_0:4; ::_thesis: verum end; percases ( z = +infty or z <> +infty ) ; suppose z = +infty ; ::_thesis: x <= z - y then z - y = +infty by A1, Th13; hence x <= z - y by XXREAL_0:4; ::_thesis: verum end; supposeA4: z <> +infty ; ::_thesis: x <= z - y then A5: x + y < +infty by A2, XXREAL_0:2, XXREAL_0:4; then A6: x <> +infty by A1, Def2; A7: y <> +infty by A1, A5, Def2; percases ( x = -infty or x <> -infty ) ; suppose x = -infty ; ::_thesis: x <= z - y hence x <= z - y by XXREAL_0:5; ::_thesis: verum end; suppose x <> -infty ; ::_thesis: x <= z - y then x in REAL by A6, XXREAL_0:14; then reconsider a = x as real number ; percases ( y = -infty or y <> -infty ) ; suppose y = -infty ; ::_thesis: x <= z - y then z - y = +infty by A1, Th14; hence x <= z - y by XXREAL_0:4; ::_thesis: verum end; suppose y <> -infty ; ::_thesis: x <= z - y then y in REAL by A7, XXREAL_0:14; then reconsider b = y as real number ; a + b in REAL by XREAL_0:def_1; then z <> -infty by A2, XXREAL_0:12; then z in REAL by A4, XXREAL_0:14; then reconsider c = z as real number ; x + y = a + b ; then a <= c - b by A2, XREAL_1:19; hence x <= z - y ; ::_thesis: verum end; end; end; end; end; end; end; theorem :: XXREAL_3:57 for x, y, z being ext-real number st ( not x = +infty or not y = -infty ) & ( not x = -infty or not y = +infty ) & ( not y = +infty or not z = +infty ) & x <= z - y holds ( y <> +infty & x + y <= z ) proof let x, y, z be ext-real number ; ::_thesis: ( ( not x = +infty or not y = -infty ) & ( not x = -infty or not y = +infty ) & ( not y = +infty or not z = +infty ) & x <= z - y implies ( y <> +infty & x + y <= z ) ) assume that A1: ( not x = +infty or not y = -infty ) and A2: ( not x = -infty or not y = +infty ) and A3: ( not y = +infty or not z = +infty ) and A4: x <= z - y ; ::_thesis: ( y <> +infty & x + y <= z ) thus A5: y <> +infty ::_thesis: x + y <= z proof assume A6: y = +infty ; ::_thesis: contradiction then z - y = -infty by A3, Th13; hence contradiction by A2, A4, A6, XXREAL_0:6; ::_thesis: verum end; percases ( y = -infty or ( y <> +infty & y <> -infty ) ) by A5; suppose y = -infty ; ::_thesis: x + y <= z then x + y = -infty by A1, Def2; hence x + y <= z by XXREAL_0:5; ::_thesis: verum end; supposeA7: ( y <> +infty & y <> -infty ) ; ::_thesis: x + y <= z - -infty = +infty by Def3; then A8: - y <> -infty by A7; - +infty = -infty by Def3; then - y <> +infty by A7; then (z - y) + y = z + ((- y) + y) by A7, A8, Th29 .= z + 0 by Th7 .= z by Th4 ; hence x + y <= z by A4, Th36; ::_thesis: verum end; end; end; theorem :: XXREAL_3:58 for x, y, z being ext-real number holds ( ( x = +infty & y = +infty ) or ( x = -infty & y = -infty ) or ( y = +infty & z = -infty ) or ( y = -infty & z = +infty ) or not x - y <= z or y <> -infty ) proof let x, y, z be ext-real number ; ::_thesis: ( ( x = +infty & y = +infty ) or ( x = -infty & y = -infty ) or ( y = +infty & z = -infty ) or ( y = -infty & z = +infty ) or not x - y <= z or y <> -infty ) assume that A1: ( not ( x = +infty & y = +infty ) & not ( x = -infty & y = -infty ) & not ( y = +infty & z = -infty ) & not ( y = -infty & z = +infty ) ) and A2: x - y <= z ; ::_thesis: y <> -infty assume A3: y = -infty ; ::_thesis: contradiction then x - y = +infty by A1, Th14; hence contradiction by A1, A2, A3, XXREAL_0:4; ::_thesis: verum end; theorem :: XXREAL_3:59 for x, y, z being ext-real number st ( not x = -infty or not y = -infty ) & ( not y = -infty or not z = +infty ) & x <= z + y holds y <> -infty proof let x, y, z be ext-real number ; ::_thesis: ( ( not x = -infty or not y = -infty ) & ( not y = -infty or not z = +infty ) & x <= z + y implies y <> -infty ) assume that A1: ( not x = -infty or not y = -infty ) and A2: ( not y = -infty or not z = +infty ) and A3: x <= z + y ; ::_thesis: y <> -infty assume A4: y = -infty ; ::_thesis: contradiction then z + y = -infty by A2, Def2; hence contradiction by A1, A3, A4, XXREAL_0:6; ::_thesis: verum end; theorem :: XXREAL_3:60 for x, y being ext-real number holds ( ( x <= - y implies y <= - x ) & ( - x <= y implies - y <= x ) ) proof let x, y be ext-real number ; ::_thesis: ( ( x <= - y implies y <= - x ) & ( - x <= y implies - y <= x ) ) ( x <= - y implies - (- y) <= - x ) by Th38; hence ( x <= - y implies y <= - x ) ; ::_thesis: ( - x <= y implies - y <= x ) ( - x <= y implies - y <= - (- x) ) by Th38; hence ( - x <= y implies - y <= x ) ; ::_thesis: verum end; theorem :: XXREAL_3:61 for x, y being ext-real number st ( for e being real number st 0 < e holds x < y + e ) holds x <= y proof let x, y be ext-real number ; ::_thesis: ( ( for e being real number st 0 < e holds x < y + e ) implies x <= y ) assume A1: for e being real number st 0 < e holds x < y + e ; ::_thesis: x <= y percases ( y = +infty or y = -infty or ( y <> +infty & y <> -infty ) ) ; supposeA2: ( y = +infty or y = -infty ) ; ::_thesis: x <= y percases ( y = +infty or y = -infty ) by A2; suppose y = +infty ; ::_thesis: x <= y hence x <= y by XXREAL_0:4; ::_thesis: verum end; supposeA3: y = -infty ; ::_thesis: x <= y x < y + 1 by A1; hence x <= y by A3, Def2; ::_thesis: verum end; end; end; supposeA4: ( y <> +infty & y <> -infty ) ; ::_thesis: x <= y percases ( x = +infty or x <> +infty ) ; supposeA5: x = +infty ; ::_thesis: x <= y x < y + 1 by A1; hence x <= y by A5, XXREAL_0:4; ::_thesis: verum end; supposeA6: x <> +infty ; ::_thesis: x <= y now__::_thesis:_(_x_<>_-infty_implies_x_<=_y_) assume A7: x <> -infty ; ::_thesis: x <= y then x in REAL by A6, XXREAL_0:14; then reconsider x1 = x as real number ; -infty <= x by XXREAL_0:5; then A8: -infty < x by A7, XXREAL_0:1; y in REAL by A4, XXREAL_0:14; then reconsider y1 = y as real number ; assume A9: not x <= y ; ::_thesis: contradiction y < +infty by A4, XXREAL_0:4; then 0 < x - y by A9, A8, Th51; then x < y + (x1 - y1) by A1; then x < (y + x) - y by Th30; then x < x + (y - y) by A4, Th30; then x < x + 0 by Th7; hence contradiction by Th4; ::_thesis: verum end; hence x <= y by XXREAL_0:5; ::_thesis: verum end; end; end; end; end; theorem :: XXREAL_3:62 for x, y, t being ext-real number st t <> -infty & t <> +infty & x < y holds x + t < y + t proof let x, y, t be ext-real number ; ::_thesis: ( t <> -infty & t <> +infty & x < y implies x + t < y + t ) assume that A1: ( t <> -infty & t <> +infty ) and A2: x < y ; ::_thesis: x + t < y + t A3: t - t = 0 by Th7; A4: now__::_thesis:_not_x_+_t_=_y_+_t assume x + t = y + t ; ::_thesis: contradiction then x + (t - t) = (y + t) - t by A1, Th30; then x + 0 = y + (t - t) by A1, A3, Th30; then x = y + 0 by A3, Th4; hence contradiction by A2, Th4; ::_thesis: verum end; x + t <= y + t by A2, Th36; hence x + t < y + t by A4, XXREAL_0:1; ::_thesis: verum end; theorem :: XXREAL_3:63 for x, y, t being ext-real number st t <> -infty & t <> +infty & x < y holds x - t < y - t proof let x, y, t be ext-real number ; ::_thesis: ( t <> -infty & t <> +infty & x < y implies x - t < y - t ) assume that A1: ( t <> -infty & t <> +infty ) and A2: x < y ; ::_thesis: x - t < y - t A3: t - t = 0 by Th7; A4: now__::_thesis:_not_x_-_t_=_y_-_t assume x - t = y - t ; ::_thesis: contradiction then x - (t - t) = (y - t) + t by A1, Th32; then x - 0 = y - (t - t) by A1, A3, Th32; then x = y + 0 by A3, Th4; hence contradiction by A2, Th4; ::_thesis: verum end; x - t <= y - t by A2, Th37; hence x - t < y - t by A4, XXREAL_0:1; ::_thesis: verum end; theorem :: XXREAL_3:64 for x, y, w, z being ext-real number st x < y & w < z holds x + w < y + z proof let x, y, w, z be ext-real number ; ::_thesis: ( x < y & w < z implies x + w < y + z ) assume that A2: x < y and A3: w < z ; ::_thesis: x + w < y + z -infty <= w by XXREAL_0:5; percasesthen ( w = -infty or -infty < w ) by XXREAL_0:1; supposeB2: w = -infty ; ::_thesis: x + w < y + z B3: ( y <> -infty & z <> -infty ) by A2, A3, XXREAL_0:5; x <> +infty by A2, XXREAL_0:3; then x + w = -infty by B2, Def2; hence x + w < y + z by B3, Lm9, XXREAL_0:6; ::_thesis: verum end; supposeA1: -infty < w ; ::_thesis: x + w < y + z percases ( y = +infty or y <> +infty ) ; supposeA4: y = +infty ; ::_thesis: x + w < y + z A5: z <= +infty by XXREAL_0:4; y + z = +infty by A1, A3, A4, Def2; hence x + w < y + z by A2, A3, A4, A5, Lm8, XXREAL_0:4; ::_thesis: verum end; supposeA6: y <> +infty ; ::_thesis: x + w < y + z -infty <= x by XXREAL_0:5; then y in REAL by A2, A6, XXREAL_0:14; then A7: y + w < y + z by A3, Th43; z <= +infty by XXREAL_0:4; then w in REAL by A1, A3, XXREAL_0:14; then x + w < y + w by A2, Th43; hence x + w < y + z by A7, XXREAL_0:2; ::_thesis: verum end; end; end; end; end; theorem :: XXREAL_3:65 for x, z, y being ext-real number st 0 <= x & z + x <= y holds z <= y proof let x, z, y be ext-real number ; ::_thesis: ( 0 <= x & z + x <= y implies z <= y ) assume 0 <= x ; ::_thesis: ( not z + x <= y or z <= y ) then z <= z + x by Th39; hence ( not z + x <= y or z <= y ) by XXREAL_0:2; ::_thesis: verum end; begin definition let x, y be ext-real number ; funcx * y -> ext-real number means :Def5: :: XXREAL_3:def 5 ex a, b being complex number st ( x = a & y = b & it = a * b ) if ( x is real & y is real ) it = +infty if ( ( not x is real or not y is real ) & ( ( x is positive & y is positive ) or ( x is negative & y is negative ) ) ) it = -infty if ( ( not x is real or not y is real ) & ( ( x is positive & y is negative ) or ( x is negative & y is positive ) ) ) otherwise it = 0 ; existence ( ( x is real & y is real implies ex b1 being ext-real number ex a, b being complex number st ( x = a & y = b & b1 = a * b ) ) & ( ( not x is real or not y is real ) & ( ( x is positive & y is positive ) or ( x is negative & y is negative ) ) implies ex b1 being ext-real number st b1 = +infty ) & ( ( not x is real or not y is real ) & ( ( x is positive & y is negative ) or ( x is negative & y is positive ) ) implies ex b1 being ext-real number st b1 = -infty ) & ( ( not x is real or not y is real ) & ( ( x is real & y is real ) or ( not ( x is positive & y is positive ) & not ( x is negative & y is negative ) ) ) & ( ( x is real & y is real ) or ( not ( x is positive & y is negative ) & not ( x is negative & y is positive ) ) ) implies ex b1 being ext-real number st b1 = 0 ) ) proof thus ( x is real & y is real implies ex c being ext-real number ex a, b being complex number st ( x = a & y = b & c = a * b ) ) ::_thesis: ( ( ( not x is real or not y is real ) & ( ( x is positive & y is positive ) or ( x is negative & y is negative ) ) implies ex b1 being ext-real number st b1 = +infty ) & ( ( not x is real or not y is real ) & ( ( x is positive & y is negative ) or ( x is negative & y is positive ) ) implies ex b1 being ext-real number st b1 = -infty ) & ( ( not x is real or not y is real ) & ( ( x is real & y is real ) or ( not ( x is positive & y is positive ) & not ( x is negative & y is negative ) ) ) & ( ( x is real & y is real ) or ( not ( x is positive & y is negative ) & not ( x is negative & y is positive ) ) ) implies ex b1 being ext-real number st b1 = 0 ) ) proof assume ( x is real & y is real ) ; ::_thesis: ex c being ext-real number ex a, b being complex number st ( x = a & y = b & c = a * b ) then reconsider a = x, b = y as real number ; take a * b ; ::_thesis: ex a, b being complex number st ( x = a & y = b & a * b = a * b ) take a ; ::_thesis: ex b being complex number st ( x = a & y = b & a * b = a * b ) take b ; ::_thesis: ( x = a & y = b & a * b = a * b ) thus ( x = a & y = b & a * b = a * b ) ; ::_thesis: verum end; thus ( ( ( not x is real or not y is real ) & ( ( x is positive & y is positive ) or ( x is negative & y is negative ) ) implies ex b1 being ext-real number st b1 = +infty ) & ( ( not x is real or not y is real ) & ( ( x is positive & y is negative ) or ( x is negative & y is positive ) ) implies ex b1 being ext-real number st b1 = -infty ) & ( ( not x is real or not y is real ) & ( ( x is real & y is real ) or ( not ( x is positive & y is positive ) & not ( x is negative & y is negative ) ) ) & ( ( x is real & y is real ) or ( not ( x is positive & y is negative ) & not ( x is negative & y is positive ) ) ) implies ex b1 being ext-real number st b1 = 0 ) ) ; ::_thesis: verum end; uniqueness for b1, b2 being ext-real number holds ( ( x is real & y is real & ex a, b being complex number st ( x = a & y = b & b1 = a * b ) & ex a, b being complex number st ( x = a & y = b & b2 = a * b ) implies b1 = b2 ) & ( ( not x is real or not y is real ) & ( ( x is positive & y is positive ) or ( x is negative & y is negative ) ) & b1 = +infty & b2 = +infty implies b1 = b2 ) & ( ( not x is real or not y is real ) & ( ( x is positive & y is negative ) or ( x is negative & y is positive ) ) & b1 = -infty & b2 = -infty implies b1 = b2 ) & ( ( not x is real or not y is real ) & ( ( x is real & y is real ) or ( not ( x is positive & y is positive ) & not ( x is negative & y is negative ) ) ) & ( ( x is real & y is real ) or ( not ( x is positive & y is negative ) & not ( x is negative & y is positive ) ) ) & b1 = 0 & b2 = 0 implies b1 = b2 ) ) ; consistency for b1 being ext-real number holds ( ( x is real & y is real & ( not x is real or not y is real ) & ( ( x is positive & y is positive ) or ( x is negative & y is negative ) ) implies ( ex a, b being complex number st ( x = a & y = b & b1 = a * b ) iff b1 = +infty ) ) & ( x is real & y is real & ( not x is real or not y is real ) & ( ( x is positive & y is negative ) or ( x is negative & y is positive ) ) implies ( ex a, b being complex number st ( x = a & y = b & b1 = a * b ) iff b1 = -infty ) ) & ( ( not x is real or not y is real ) & ( ( x is positive & y is positive ) or ( x is negative & y is negative ) ) & ( not x is real or not y is real ) & ( ( x is positive & y is negative ) or ( x is negative & y is positive ) ) implies ( b1 = +infty iff b1 = -infty ) ) ) ; commutativity for b1, x, y being ext-real number st ( x is real & y is real implies ex a, b being complex number st ( x = a & y = b & b1 = a * b ) ) & ( ( not x is real or not y is real ) & ( ( x is positive & y is positive ) or ( x is negative & y is negative ) ) implies b1 = +infty ) & ( ( not x is real or not y is real ) & ( ( x is positive & y is negative ) or ( x is negative & y is positive ) ) implies b1 = -infty ) & ( ( not x is real or not y is real ) & ( ( x is real & y is real ) or ( not ( x is positive & y is positive ) & not ( x is negative & y is negative ) ) ) & ( ( x is real & y is real ) or ( not ( x is positive & y is negative ) & not ( x is negative & y is positive ) ) ) implies b1 = 0 ) holds ( ( y is real & x is real implies ex a, b being complex number st ( y = a & x = b & b1 = a * b ) ) & ( ( not y is real or not x is real ) & ( ( y is positive & x is positive ) or ( y is negative & x is negative ) ) implies b1 = +infty ) & ( ( not y is real or not x is real ) & ( ( y is positive & x is negative ) or ( y is negative & x is positive ) ) implies b1 = -infty ) & ( ( not y is real or not x is real ) & ( ( y is real & x is real ) or ( not ( y is positive & x is positive ) & not ( y is negative & x is negative ) ) ) & ( ( y is real & x is real ) or ( not ( y is positive & x is negative ) & not ( y is negative & x is positive ) ) ) implies b1 = 0 ) ) ; end; :: deftheorem Def5 defines * XXREAL_3:def_5_:_ for x, y, b3 being ext-real number holds ( ( x is real & y is real implies ( b3 = x * y iff ex a, b being complex number st ( x = a & y = b & b3 = a * b ) ) ) & ( ( not x is real or not y is real ) & ( ( x is positive & y is positive ) or ( x is negative & y is negative ) ) implies ( b3 = x * y iff b3 = +infty ) ) & ( ( not x is real or not y is real ) & ( ( x is positive & y is negative ) or ( x is negative & y is positive ) ) implies ( b3 = x * y iff b3 = -infty ) ) & ( ( not x is real or not y is real ) & ( ( x is real & y is real ) or ( not ( x is positive & y is positive ) & not ( x is negative & y is negative ) ) ) & ( ( x is real & y is real ) or ( not ( x is positive & y is negative ) & not ( x is negative & y is positive ) ) ) implies ( b3 = x * y iff b3 = 0 ) ) ); registration let x, y be real number ; let a, b be complex number ; identifyx * y with a * b when x = a, y = b; compatibility ( x = a & y = b implies x * y = a * b ) by Def5; end; definition let x be ext-real number ; funcx " -> ext-real number means :Def6: :: XXREAL_3:def 6 ex a being complex number st ( x = a & it = a " ) if x is real otherwise it = 0 ; existence ( ( x is real implies ex b1 being ext-real number ex a being complex number st ( x = a & b1 = a " ) ) & ( not x is real implies ex b1 being ext-real number st b1 = 0 ) ) proof thus ( x is real implies ex c being ext-real number ex a being complex number st ( x = a & c = a " ) ) ::_thesis: ( not x is real implies ex b1 being ext-real number st b1 = 0 ) proof assume x is real ; ::_thesis: ex c being ext-real number ex a being complex number st ( x = a & c = a " ) then reconsider a = x as real number ; take a " ; ::_thesis: ex a being complex number st ( x = a & a " = a " ) take a ; ::_thesis: ( x = a & a " = a " ) thus ( x = a & a " = a " ) ; ::_thesis: verum end; thus ( not x is real implies ex b1 being ext-real number st b1 = 0 ) ; ::_thesis: verum end; uniqueness for b1, b2 being ext-real number holds ( ( x is real & ex a being complex number st ( x = a & b1 = a " ) & ex a being complex number st ( x = a & b2 = a " ) implies b1 = b2 ) & ( not x is real & b1 = 0 & b2 = 0 implies b1 = b2 ) ) ; consistency for b1 being ext-real number holds verum ; end; :: deftheorem Def6 defines " XXREAL_3:def_6_:_ for x, b2 being ext-real number holds ( ( x is real implies ( b2 = x " iff ex a being complex number st ( x = a & b2 = a " ) ) ) & ( not x is real implies ( b2 = x " iff b2 = 0 ) ) ); registration let x be real number ; let a be complex number ; identifyx " with a " when x = a; compatibility ( x = a implies x " = a " ) by Def6; end; definition let x, y be ext-real number ; funcx / y -> ext-real number equals :: XXREAL_3:def 7 x * (y "); coherence x * (y ") is ext-real number ; end; :: deftheorem defines / XXREAL_3:def_7_:_ for x, y being ext-real number holds x / y = x * (y "); registration let x, y be real number ; let a, b be complex number ; identifyx / y with a / b when x = a, y = b; compatibility ( x = a & y = b implies x / y = a / b ) proof reconsider y1 = y " as real number ; assume ( x = a & y = b ) ; ::_thesis: x / y = a / b hence a / b = x * y1 .= x / y ; ::_thesis: verum end; end; Lm16: for x being ext-real number holds x * 0 = 0 proof let x be ext-real number ; ::_thesis: x * 0 = 0 percases ( x in REAL or x = +infty or x = -infty ) by XXREAL_0:14; suppose x in REAL ; ::_thesis: x * 0 = 0 then ex a, b being complex number st ( x = a & 0 = b & x * 0 = a * b ) by Def5; hence x * 0 = 0 ; ::_thesis: verum end; suppose x = +infty ; ::_thesis: x * 0 = 0 hence x * 0 = 0 by Def5; ::_thesis: verum end; suppose x = -infty ; ::_thesis: x * 0 = 0 hence x * 0 = 0 by Def5; ::_thesis: verum end; end; end; registration let x be ext-real positive number ; let y be ext-real negative number ; clusterx * y -> ext-real negative ; coherence x * y is negative proof percases ( ( x in REAL & y in REAL ) or not x in REAL or not y in REAL ) ; suppose ( x in REAL & y in REAL ) ; ::_thesis: x * y is negative then reconsider x = x, y = y as real number ; x * y < 0 ; hence x * y is negative ; ::_thesis: verum end; suppose ( not x in REAL or not y in REAL ) ; ::_thesis: x * y is negative then ( not x is real or not y is real ) by XREAL_0:def_1; hence x * y is negative by Def5; ::_thesis: verum end; end; end; end; registration let x, y be ext-real negative number ; clusterx * y -> ext-real positive ; coherence x * y is positive proof percases ( ( x in REAL & y in REAL ) or not x in REAL or not y in REAL ) ; suppose ( x in REAL & y in REAL ) ; ::_thesis: x * y is positive then reconsider x = x, y = y as real number ; x * y > 0 ; hence x * y is positive ; ::_thesis: verum end; suppose ( not x in REAL or not y in REAL ) ; ::_thesis: x * y is positive then ( not x is real or not y is real ) by XREAL_0:def_1; hence x * y is positive by Def5; ::_thesis: verum end; end; end; end; registration let x, y be ext-real positive number ; clusterx * y -> ext-real positive ; coherence x * y is positive proof percases ( ( x in REAL & y in REAL ) or not x in REAL or not y in REAL ) ; suppose ( x in REAL & y in REAL ) ; ::_thesis: x * y is positive then reconsider x = x, y = y as real number ; x * y > 0 ; hence x * y is positive ; ::_thesis: verum end; suppose ( not x in REAL or not y in REAL ) ; ::_thesis: x * y is positive then ( not x is real or not y is real ) by XREAL_0:def_1; hence x * y is positive by Def5; ::_thesis: verum end; end; end; end; registration let x be ext-real non positive number ; let y be ext-real non negative number ; clusterx * y -> ext-real non positive ; coherence not x * y is positive proof percases ( x = 0 or y = 0 or ( x < 0 & y > 0 ) ) ; suppose ( x = 0 or y = 0 ) ; ::_thesis: not x * y is positive hence x * y <= 0 by Lm16; :: according to XXREAL_0:def_6 ::_thesis: verum end; suppose ( x < 0 & y > 0 ) ; ::_thesis: not x * y is positive hence x * y <= 0 ; :: according to XXREAL_0:def_6 ::_thesis: verum end; end; end; end; registration let x, y be ext-real non positive number ; clusterx * y -> ext-real non negative ; coherence not x * y is negative proof percases ( x = 0 or y = 0 or ( x < 0 & y < 0 ) ) ; suppose ( x = 0 or y = 0 ) ; ::_thesis: not x * y is negative hence x * y >= 0 by Lm16; :: according to XXREAL_0:def_7 ::_thesis: verum end; suppose ( x < 0 & y < 0 ) ; ::_thesis: not x * y is negative hence x * y >= 0 ; :: according to XXREAL_0:def_7 ::_thesis: verum end; end; end; end; registration let x, y be ext-real non negative number ; clusterx * y -> ext-real non negative ; coherence not x * y is negative proof percases ( x = 0 or y = 0 or ( x > 0 & y > 0 ) ) ; suppose ( x = 0 or y = 0 ) ; ::_thesis: not x * y is negative hence x * y >= 0 by Lm16; :: according to XXREAL_0:def_7 ::_thesis: verum end; suppose ( x > 0 & y > 0 ) ; ::_thesis: not x * y is negative hence x * y >= 0 ; :: according to XXREAL_0:def_7 ::_thesis: verum end; end; end; end; registration let x be ext-real non positive number ; clusterx " -> ext-real non positive ; coherence not x " is positive proof percases ( x is real or not x is real ) ; suppose x is real ; ::_thesis: not x " is positive then reconsider x = x as real number ; not x " is positive ; hence not x " is positive ; ::_thesis: verum end; suppose not x is real ; ::_thesis: not x " is positive hence not x " is positive by Def6; ::_thesis: verum end; end; end; end; registration let x be ext-real non negative number ; clusterx " -> ext-real non negative ; coherence not x " is negative proof percases ( x is real or not x is real ) ; suppose x is real ; ::_thesis: not x " is negative then reconsider x = x as real number ; not x " is negative ; hence not x " is negative ; ::_thesis: verum end; suppose not x is real ; ::_thesis: not x " is negative hence not x " is negative by Def6; ::_thesis: verum end; end; end; end; registration let x be ext-real non negative number ; let y be ext-real non positive number ; clusterx / y -> ext-real non positive ; coherence not x / y is positive ; clustery / x -> ext-real non positive ; coherence not y / x is positive ; end; registration let x, y be ext-real non negative number ; clusterx / y -> ext-real non negative ; coherence not x / y is negative ; end; registration let x, y be ext-real non positive number ; clusterx / y -> ext-real non negative ; coherence not x / y is negative ; end; Lm17: for x, y being ext-real number st not x is real & x * y = 0 holds y = 0 proof let x, y be ext-real number ; ::_thesis: ( not x is real & x * y = 0 implies y = 0 ) assume that A1: not x is real and A2: x * y = 0 ; ::_thesis: y = 0 ( not ( x is positive & y is positive ) & not ( x is negative & y is negative ) ) by A2; hence y = 0 by A1, A2; ::_thesis: verum end; registration let x, y be non zero ext-real number ; clusterx * y -> non zero ext-real ; coherence not x * y is zero proof percases ( ( x is real & y is real ) or not x is real or not y is real ) ; suppose ( x is real & y is real ) ; ::_thesis: not x * y is zero then reconsider r = x, s = y as real number ; assume x * y is zero ; ::_thesis: contradiction then r * s = 0 ; hence contradiction ; ::_thesis: verum end; suppose ( not x is real or not y is real ) ; ::_thesis: not x * y is zero hence not x * y is zero by Lm17; ::_thesis: verum end; end; end; end; registration let x be zero ext-real number ; let y be ext-real number ; clusterx * y -> zero ext-real for ext-real number ; coherence for b1 being ext-real number st b1 = x * y holds b1 is zero by Lm16; end; Lm18: for x, y, z being ext-real number st x = 0 holds x * (y * z) = (x * y) * z proof let x, y, z be ext-real number ; ::_thesis: ( x = 0 implies x * (y * z) = (x * y) * z ) assume A1: x = 0 ; ::_thesis: x * (y * z) = (x * y) * z hence x * (y * z) = 0 .= (x * y) * z by A1 ; ::_thesis: verum end; Lm19: for y, x, z being ext-real number st y = 0 holds x * (y * z) = (x * y) * z proof let y, x, z be ext-real number ; ::_thesis: ( y = 0 implies x * (y * z) = (x * y) * z ) assume A1: y = 0 ; ::_thesis: x * (y * z) = (x * y) * z hence x * (y * z) = 0 .= (x * y) * z by A1 ; ::_thesis: verum end; Lm20: for y, x, z being ext-real number st not y is real holds x * (y * z) = (x * y) * z proof let y, x, z be ext-real number ; ::_thesis: ( not y is real implies x * (y * z) = (x * y) * z ) assume not y is real ; ::_thesis: x * (y * z) = (x * y) * z then A1: not y in REAL ; assume A2: not x * (y * z) = (x * y) * z ; ::_thesis: contradiction then A3: ( x <> 0 & z <> 0 ) by Lm18; percases ( y = -infty or y = +infty ) by A1, XXREAL_0:14; supposeA4: y = -infty ; ::_thesis: contradiction percases ( ( x is positive & z is positive ) or ( x is positive & z is negative ) or ( x is negative & z is positive ) or ( x is negative & z is negative ) ) by A3; supposeA5: ( x is positive & z is positive ) ; ::_thesis: contradiction then x * (-infty * z) = x * -infty by Def5 .= -infty by A5, Def5 .= -infty * z by A5, Def5 .= (x * -infty) * z by A5, Def5 ; hence contradiction by A2, A4; ::_thesis: verum end; supposeA6: ( x is positive & z is negative ) ; ::_thesis: contradiction then x * (-infty * z) = x * +infty by Def5 .= +infty by A6, Def5 .= -infty * z by A6, Def5 .= (x * -infty) * z by A6, Def5 ; hence contradiction by A2, A4; ::_thesis: verum end; supposeA7: ( x is negative & z is positive ) ; ::_thesis: contradiction then x * (-infty * z) = x * -infty by Def5 .= +infty by A7, Def5 .= +infty * z by A7, Def5 .= (x * -infty) * z by A7, Def5 ; hence contradiction by A2, A4; ::_thesis: verum end; supposeA8: ( x is negative & z is negative ) ; ::_thesis: contradiction then x * (-infty * z) = x * +infty by Def5 .= -infty by A8, Def5 .= +infty * z by A8, Def5 .= (x * -infty) * z by A8, Def5 ; hence contradiction by A2, A4; ::_thesis: verum end; end; end; supposeA9: y = +infty ; ::_thesis: contradiction percases ( ( x is positive & z is positive ) or ( x is positive & z is negative ) or ( x is negative & z is positive ) or ( x is negative & z is negative ) ) by A3; supposeA10: ( x is positive & z is positive ) ; ::_thesis: contradiction then x * (+infty * z) = x * +infty by Def5 .= +infty by A10, Def5 .= +infty * z by A10, Def5 .= (x * +infty) * z by A10, Def5 ; hence contradiction by A2, A9; ::_thesis: verum end; supposeA11: ( x is positive & z is negative ) ; ::_thesis: contradiction then x * (+infty * z) = x * -infty by Def5 .= -infty by A11, Def5 .= +infty * z by A11, Def5 .= (x * +infty) * z by A11, Def5 ; hence contradiction by A2, A9; ::_thesis: verum end; supposeA12: ( x is negative & z is positive ) ; ::_thesis: contradiction then x * (+infty * z) = x * +infty by Def5 .= -infty by A12, Def5 .= -infty * z by A12, Def5 .= (x * +infty) * z by A12, Def5 ; hence contradiction by A2, A9; ::_thesis: verum end; supposeA13: ( x is negative & z is negative ) ; ::_thesis: contradiction then x * (+infty * z) = x * -infty by Def5 .= +infty by A13, Def5 .= -infty * z by A13, Def5 .= (x * +infty) * z by A13, Def5 ; hence contradiction by A2, A9; ::_thesis: verum end; end; end; end; end; Lm21: for x, y, z being ext-real number st not x is real holds x * (y * z) = (x * y) * z proof let x, y, z be ext-real number ; ::_thesis: ( not x is real implies x * (y * z) = (x * y) * z ) assume not x is real ; ::_thesis: x * (y * z) = (x * y) * z then A1: not x in REAL ; assume A2: not x * (y * z) = (x * y) * z ; ::_thesis: contradiction then A3: ( y <> 0 & z <> 0 ) by Lm18, Lm19; percases ( x = -infty or x = +infty ) by A1, XXREAL_0:14; supposeA4: x = -infty ; ::_thesis: contradiction percases ( ( y is positive & z is positive ) or ( y is positive & z is negative ) or ( y is negative & z is positive ) or ( y is negative & z is negative ) ) by A3; supposeA5: ( y is positive & z is positive ) ; ::_thesis: contradiction then -infty * (y * z) = -infty by Def5 .= -infty * z by A5, Def5 .= (-infty * y) * z by A5, Def5 ; hence contradiction by A2, A4; ::_thesis: verum end; supposeA6: ( y is positive & z is negative ) ; ::_thesis: contradiction then -infty * (y * z) = +infty by Def5 .= -infty * z by A6, Def5 .= (-infty * y) * z by A6, Def5 ; hence contradiction by A2, A4; ::_thesis: verum end; supposeA7: ( y is negative & z is positive ) ; ::_thesis: contradiction then -infty * (y * z) = +infty by Def5 .= +infty * z by A7, Def5 .= (-infty * y) * z by A7, Def5 ; hence contradiction by A2, A4; ::_thesis: verum end; supposeA8: ( y is negative & z is negative ) ; ::_thesis: contradiction then -infty * (y * z) = -infty by Def5 .= +infty * z by A8, Def5 .= (-infty * y) * z by A8, Def5 ; hence contradiction by A2, A4; ::_thesis: verum end; end; end; supposeA9: x = +infty ; ::_thesis: contradiction percases ( ( y is positive & z is positive ) or ( y is positive & z is negative ) or ( y is negative & z is positive ) or ( y is negative & z is negative ) ) by A3; supposeA10: ( y is positive & z is positive ) ; ::_thesis: contradiction then +infty * (y * z) = +infty by Def5 .= +infty * z by A10, Def5 .= (+infty * y) * z by A10, Def5 ; hence contradiction by A2, A9; ::_thesis: verum end; supposeA11: ( y is positive & z is negative ) ; ::_thesis: contradiction then +infty * (y * z) = -infty by Def5 .= +infty * z by A11, Def5 .= (+infty * y) * z by A11, Def5 ; hence contradiction by A2, A9; ::_thesis: verum end; supposeA12: ( y is negative & z is positive ) ; ::_thesis: contradiction then +infty * (y * z) = -infty by Def5 .= -infty * z by A12, Def5 .= (+infty * y) * z by A12, Def5 ; hence contradiction by A2, A9; ::_thesis: verum end; supposeA13: ( y is negative & z is negative ) ; ::_thesis: contradiction then +infty * (y * z) = +infty by Def5 .= -infty * z by A13, Def5 .= (+infty * y) * z by A13, Def5 ; hence contradiction by A2, A9; ::_thesis: verum end; end; end; end; end; theorem Th66: :: XXREAL_3:66 for x, y, z being ext-real number holds x * (y * z) = (x * y) * z proof let x, y, z be ext-real number ; ::_thesis: x * (y * z) = (x * y) * z percases ( ( x is real & y is real & z is real ) or not x is real or not z is real or not y is real ) ; suppose ( x is real & y is real & z is real ) ; ::_thesis: x * (y * z) = (x * y) * z then reconsider r = x, s = y, t = z as real number ; reconsider rs = r * s, sx = s * t as real number ; thus x * (y * z) = r * sx .= rs * t .= (x * y) * z ; ::_thesis: verum end; suppose ( not x is real or not z is real ) ; ::_thesis: x * (y * z) = (x * y) * z hence x * (y * z) = (x * y) * z by Lm21; ::_thesis: verum end; suppose not y is real ; ::_thesis: x * (y * z) = (x * y) * z hence x * (y * z) = (x * y) * z by Lm20; ::_thesis: verum end; end; end; registration let r be real number ; clusterr " -> ext-real real ; coherence r " is real ; end; registration let r, s be real number ; clusterr * s -> ext-real real ; coherence r * s is real ; clusterr / s -> ext-real real ; coherence r / s is real ; end; registration cluster-infty " -> zero ext-real ; coherence -infty " is zero by Def6; cluster+infty " -> zero ext-real ; coherence +infty " is zero by Def6; end; theorem :: XXREAL_3:67 for f, g being ext-real number holds (f * g) " = (f ") * (g ") proof let f, g be ext-real number ; ::_thesis: (f * g) " = (f ") * (g ") percases ( ( f in REAL & g in REAL ) or f = +infty or f = -infty or g = +infty or g = -infty ) by XXREAL_0:14; suppose ( f in REAL & g in REAL ) ; ::_thesis: (f * g) " = (f ") * (g ") then reconsider f1 = f, g1 = g as real number ; A1: ( ex a being complex number st ( f1 = a & f " = a " ) & ex b being complex number st ( g1 = b & g " = b " ) ) by Def6; then ex a, b being complex number st ( f " = a & g " = b & (f ") * (g ") = a * b ) by Def5; then (f ") * (g ") = (f1 * g1) " by A1, XCMPLX_1:204; hence (f * g) " = (f ") * (g ") ; ::_thesis: verum end; supposeA2: f = +infty ; ::_thesis: (f * g) " = (f ") * (g ") ( g is positive or g is negative or g = 0 ) ; then ( (f * g) " = +infty " or (f * g) " = -infty " or (f * g) " = 0 " ) by A2, Def5; hence (f * g) " = (f ") * (g ") by A2; ::_thesis: verum end; supposeA3: f = -infty ; ::_thesis: (f * g) " = (f ") * (g ") ( g is positive or g is negative or g = 0 ) ; then ( (f * g) " = +infty " or (f * g) " = -infty " or (f * g) " = 0 " ) by A3, Def5; hence (f * g) " = (f ") * (g ") by A3; ::_thesis: verum end; supposeA4: g = +infty ; ::_thesis: (f * g) " = (f ") * (g ") ( f is positive or f is negative or f = 0 ) ; then ( (f * g) " = +infty " or (f * g) " = -infty " or (f * g) " = 0 " ) by A4, Def5; hence (f * g) " = (f ") * (g ") by A4; ::_thesis: verum end; supposeA5: g = -infty ; ::_thesis: (f * g) " = (f ") * (g ") ( f is positive or f is negative or f = 0 ) ; then ( (f * g) " = +infty " or (f * g) " = -infty " or (f * g) " = 0 " ) by A5, Def5; hence (f * g) " = (f ") * (g ") by A5; ::_thesis: verum end; end; end; theorem :: XXREAL_3:68 for r being real number for f, g being ext-real number st r <> 0 & r * f = r * g holds f = g proof let r be real number ; ::_thesis: for f, g being ext-real number st r <> 0 & r * f = r * g holds f = g let f, g be ext-real number ; ::_thesis: ( r <> 0 & r * f = r * g implies f = g ) assume that A1: r <> 0 and A2: r * f = r * g ; ::_thesis: f = g A3: ( r is positive or r is negative ) by A1; percases ( f in REAL or f = +infty or f = -infty ) by XXREAL_0:14; supposeA4: f in REAL ; ::_thesis: f = g now__::_thesis:_g_in_REAL assume not g in REAL ; ::_thesis: contradiction then ( g = +infty or g = -infty ) by XXREAL_0:14; hence contradiction by A2, A3, A4, Def5; ::_thesis: verum end; then A5: ex c, d being complex number st ( r = c & g = d & r * g = c * d ) by Def5; ex a, b being complex number st ( r = a & f = b & r * f = a * b ) by A4, Def5; hence f = g by A1, A2, A5, XCMPLX_1:5; ::_thesis: verum end; supposeA6: f = +infty ; ::_thesis: f = g assume f <> g ; ::_thesis: contradiction then ( g in REAL or g = -infty ) by A6, XXREAL_0:14; hence contradiction by A2, A3, A6, Def5; ::_thesis: verum end; supposeA7: f = -infty ; ::_thesis: f = g assume f <> g ; ::_thesis: contradiction then ( g in REAL or g = +infty ) by A7, XXREAL_0:14; hence contradiction by A2, A3, A7, Def5; ::_thesis: verum end; end; end; theorem Th69: :: XXREAL_3:69 for x, y being ext-real number st x <> +infty & x <> -infty & x * y = +infty & not y = +infty holds y = -infty proof let x, y be ext-real number ; ::_thesis: ( x <> +infty & x <> -infty & x * y = +infty & not y = +infty implies y = -infty ) assume that A1: ( x <> +infty & x <> -infty ) and A2: x * y = +infty ; ::_thesis: ( y = +infty or y = -infty ) assume ( y <> +infty & y <> -infty ) ; ::_thesis: contradiction then A3: y in REAL by XXREAL_0:14; x in REAL by A1, XXREAL_0:14; then reconsider a = x, b = y as real number by A3; x * y = a * b ; hence contradiction by A2; ::_thesis: verum end; theorem Th70: :: XXREAL_3:70 for x, y being ext-real number st x <> +infty & x <> -infty & x * y = -infty & not y = +infty holds y = -infty proof let x, y be ext-real number ; ::_thesis: ( x <> +infty & x <> -infty & x * y = -infty & not y = +infty implies y = -infty ) assume that A1: ( x <> +infty & x <> -infty ) and A2: x * y = -infty ; ::_thesis: ( y = +infty or y = -infty ) assume ( y <> +infty & y <> -infty ) ; ::_thesis: contradiction then A3: y in REAL by XXREAL_0:14; x in REAL by A1, XXREAL_0:14; then reconsider a = x, b = y as real number by A3; x * y = a * b ; hence contradiction by A2; ::_thesis: verum end; Lm22: for x, y being ext-real number holds ( not x * y in REAL or ( x in REAL & y in REAL ) or x * y = 0 ) proof let x, y be ext-real number ; ::_thesis: ( not x * y in REAL or ( x in REAL & y in REAL ) or x * y = 0 ) assume A1: x * y in REAL ; ::_thesis: ( ( x in REAL & y in REAL ) or x * y = 0 ) assume ( not x in REAL or not y in REAL ) ; ::_thesis: x * y = 0 then A2: ( not x is real or not y is real ) by XREAL_0:def_1; assume A3: x * y <> 0 ; ::_thesis: contradiction percases ( ( x is positive & y is positive ) or ( x is negative & y is negative ) or ( x is positive & y is negative ) or ( x is negative & y is positive ) ) by A3; suppose ( ( x is positive & y is positive ) or ( x is negative & y is negative ) ) ; ::_thesis: contradiction hence contradiction by A1, A2, Def5; ::_thesis: verum end; suppose ( ( x is positive & y is negative ) or ( x is negative & y is positive ) ) ; ::_thesis: contradiction hence contradiction by A1, A2, Def5; ::_thesis: verum end; end; end; theorem Th71: :: XXREAL_3:71 for x, y, z being ext-real number st x <= y & 0 <= z holds x * z <= y * z proof let x, y, z be ext-real number ; ::_thesis: ( x <= y & 0 <= z implies x * z <= y * z ) assume that A1: x <= y and A2: 0 <= z ; ::_thesis: x * z <= y * z percases ( z = 0 or z > 0 ) by A2; suppose z = 0 ; ::_thesis: x * z <= y * z hence x * z <= y * z ; ::_thesis: verum end; supposeA3: z > 0 ; ::_thesis: x * z <= y * z percases ( x = 0 or x <> 0 ) ; supposeA4: x = 0 ; ::_thesis: x * z <= y * z then z * y >= 0 by A1, A2; hence x * z <= y * z by A4; ::_thesis: verum end; supposeA5: x <> 0 ; ::_thesis: x * z <= y * z percases ( ( x * z in REAL & y * z in REAL ) or not x * z in REAL or not y * z in REAL ) ; :: according to XXREAL_3:def_1 caseA6: ( x * z in REAL & y * z in REAL ) ; ::_thesis: ex p, q being Element of REAL st ( p = x * z & q = y * z & p <= q ) ( y * z = 0 implies y = 0 ) by A3; then reconsider x = x, y = y, z = z as Element of REAL by A3, A5, A6, Lm22; reconsider p = x * z, q = y * z as Element of REAL by XREAL_0:def_1; take p ; ::_thesis: ex q being Element of REAL st ( p = x * z & q = y * z & p <= q ) take q ; ::_thesis: ( p = x * z & q = y * z & p <= q ) thus ( p = x * z & q = y * z & p <= q ) by A1, A2, XREAL_1:64; ::_thesis: verum end; caseA7: ( not x * z in REAL or not y * z in REAL ) ; ::_thesis: ( x * z = -infty or y * z = +infty ) percases ( not x * z in REAL or not y * z in REAL ) by A7; supposeA8: not x * z in REAL ; ::_thesis: ( x * z = -infty or y * z = +infty ) percases ( x * z = -infty or x * z = +infty ) by A8, XXREAL_0:14; suppose x * z = -infty ; ::_thesis: ( x * z = -infty or y * z = +infty ) hence ( x * z = -infty or y * z = +infty ) ; ::_thesis: verum end; suppose x * z = +infty ; ::_thesis: ( x * z = -infty or y * z = +infty ) then A9: x <> -infty by A3; A10: ( not x in REAL or not y in REAL or not z in REAL ) by A8, XREAL_0:def_1; percases ( y = +infty or x = +infty or y = -infty or ( not z in REAL & x in REAL & y in REAL ) ) by A9, A10, XXREAL_0:14; suppose y = +infty ; ::_thesis: ( x * z = -infty or y * z = +infty ) hence ( x * z = -infty or y * z = +infty ) by A3, Def5; ::_thesis: verum end; suppose x = +infty ; ::_thesis: ( x * z = -infty or y * z = +infty ) then y = +infty by A1, XXREAL_0:4; hence ( x * z = -infty or y * z = +infty ) by A3, Def5; ::_thesis: verum end; suppose y = -infty ; ::_thesis: ( x * z = -infty or y * z = +infty ) then x = -infty by A1, XXREAL_0:6; hence ( x * z = -infty or y * z = +infty ) by A3, Def5; ::_thesis: verum end; supposethat A11: not z in REAL and ( x in REAL & y in REAL ) ; ::_thesis: ( x * z = -infty or y * z = +infty ) A12: z = +infty by A3, A11, XXREAL_0:14; percases ( x < 0 or 0 < x ) by A5; suppose x < 0 ; ::_thesis: ( x * z = -infty or y * z = +infty ) hence ( x * z = -infty or y * z = +infty ) by A12, Def5; ::_thesis: verum end; suppose 0 < x ; ::_thesis: ( x * z = -infty or y * z = +infty ) hence ( x * z = -infty or y * z = +infty ) by A1, A12, Def5; ::_thesis: verum end; end; end; end; end; end; end; suppose not y * z in REAL ; ::_thesis: ( x * z = -infty or y * z = +infty ) then A13: ( not x in REAL or not y in REAL or not z in REAL ) by XREAL_0:def_1; percases ( x = -infty or y = +infty or x = +infty or y = -infty or ( not z in REAL & x in REAL & y in REAL ) ) by A13, XXREAL_0:14; suppose x = -infty ; ::_thesis: ( x * z = -infty or y * z = +infty ) hence ( x * z = -infty or y * z = +infty ) by A3, Def5; ::_thesis: verum end; suppose y = +infty ; ::_thesis: ( x * z = -infty or y * z = +infty ) hence ( x * z = -infty or y * z = +infty ) by A3, Def5; ::_thesis: verum end; suppose x = +infty ; ::_thesis: ( x * z = -infty or y * z = +infty ) then y = +infty by A1, XXREAL_0:4; hence ( x * z = -infty or y * z = +infty ) by A3, Def5; ::_thesis: verum end; suppose y = -infty ; ::_thesis: ( x * z = -infty or y * z = +infty ) then x = -infty by A1, XXREAL_0:6; hence ( x * z = -infty or y * z = +infty ) by A3, Def5; ::_thesis: verum end; supposethat A14: not z in REAL and ( x in REAL & y in REAL ) ; ::_thesis: ( x * z = -infty or y * z = +infty ) A15: z = +infty by A3, A14, XXREAL_0:14; percases ( x < 0 or 0 < x ) by A5; suppose x < 0 ; ::_thesis: ( x * z = -infty or y * z = +infty ) hence ( x * z = -infty or y * z = +infty ) by A15, Def5; ::_thesis: verum end; suppose 0 < x ; ::_thesis: ( x * z = -infty or y * z = +infty ) hence ( x * z = -infty or y * z = +infty ) by A1, A15, Def5; ::_thesis: verum end; end; end; end; end; end; end; end; end; end; end; end; end; theorem Th72: :: XXREAL_3:72 for x, y, z being ext-real number st x < y & 0 < z & z <> +infty holds x * z < y * z proof let x, y, z be ext-real number ; ::_thesis: ( x < y & 0 < z & z <> +infty implies x * z < y * z ) assume that A1: x < y and A2: 0 < z and A3: z <> +infty ; ::_thesis: x * z < y * z A4: now__::_thesis:_not_x_*_z_=_y_*_z A5: ( x <> +infty & y <> -infty ) by A1, XXREAL_0:3, XXREAL_0:5; assume A6: x * z = y * z ; ::_thesis: contradiction percases ( ( x in REAL & y in REAL ) or y = +infty or x = -infty ) by A5, XXREAL_0:14; supposeA7: ( x in REAL & y in REAL ) ; ::_thesis: contradiction z in REAL by A2, A3, XXREAL_0:14; then reconsider x = x, y = y, z = z as real number by A7; x * z < y * z by A1, A2, XREAL_1:68; hence contradiction by A6; ::_thesis: verum end; supposeA8: y = +infty ; ::_thesis: contradiction then y * z = +infty by A2, Def5; then ( x = +infty or x = -infty ) by A2, A3, A6, Th69; hence contradiction by A1, A2, A6, A8; ::_thesis: verum end; supposeA9: x = -infty ; ::_thesis: contradiction then x * z = -infty by A2, Def5; then ( y = +infty or y = -infty ) by A2, A3, A6, Th70; hence contradiction by A1, A2, A6, A9; ::_thesis: verum end; end; end; x * z <= y * z by A1, A2, Th71; hence x * z < y * z by A4, XXREAL_0:1; ::_thesis: verum end; theorem :: XXREAL_3:73 for x, y being ext-real number holds ( not x * y in REAL or ( x in REAL & y in REAL ) or x * y = 0 ) by Lm22; theorem :: XXREAL_3:74 +infty " = 0 ; theorem :: XXREAL_3:75 -infty " = 0 ; theorem :: XXREAL_3:76 for x being ext-real number holds x / +infty = 0 ; theorem :: XXREAL_3:77 for x being ext-real number holds x / -infty = 0 ; theorem Th78: :: XXREAL_3:78 for x being ext-real number st x <> -infty & x <> +infty & x <> 0 holds x / x = 1 proof let x be ext-real number ; ::_thesis: ( x <> -infty & x <> +infty & x <> 0 implies x / x = 1 ) assume ( x <> -infty & x <> +infty ) ; ::_thesis: ( not x <> 0 or x / x = 1 ) then x in REAL by XXREAL_0:14; then reconsider a = x as real number ; assume x <> 0 ; ::_thesis: x / x = 1 then a / a = 1 by XCMPLX_1:60; hence x / x = 1 ; ::_thesis: verum end; theorem :: XXREAL_3:79 for x, y, z being ext-real number st x <= y & 0 < z holds x / z <= y / z by Th71; theorem :: XXREAL_3:80 for x, y, z being ext-real number st x < y & 0 < z & z <> +infty holds x / z < y / z proof let x, y, z be ext-real number ; ::_thesis: ( x < y & 0 < z & z <> +infty implies x / z < y / z ) assume that A1: x < y and A2: 0 < z and A3: z <> +infty ; ::_thesis: x / z < y / z percases ( z = -infty or z in REAL ) by A3, XXREAL_0:14; suppose z = -infty ; ::_thesis: x / z < y / z hence x / z < y / z by A2; ::_thesis: verum end; suppose z in REAL ; ::_thesis: x / z < y / z then reconsider z = z as real number ; z " > 0 by A2; hence x / z < y / z by A1, Th72; ::_thesis: verum end; end; end; theorem Th81: :: XXREAL_3:81 for x being ext-real number holds 1 * x = x proof let x be ext-real number ; ::_thesis: 1 * x = x percases ( x in REAL or x = -infty or x = +infty ) by XXREAL_0:14; suppose x in REAL ; ::_thesis: 1 * x = x then reconsider x = x, y = 1 as real number ; y * x = x ; hence 1 * x = x ; ::_thesis: verum end; suppose ( x = -infty or x = +infty ) ; ::_thesis: 1 * x = x hence 1 * x = x by Def5; ::_thesis: verum end; end; end; theorem Th82: :: XXREAL_3:82 for y being ext-real number holds ( not y " = 0 or y = +infty or y = -infty or y = 0 ) proof let y be ext-real number ; ::_thesis: ( not y " = 0 or y = +infty or y = -infty or y = 0 ) assume A1: y " = 0 ; ::_thesis: ( y = +infty or y = -infty or y = 0 ) assume ( y <> +infty & y <> -infty ) ; ::_thesis: y = 0 then y in REAL by XXREAL_0:14; then reconsider y = y as real number ; (y ") " = 0 by A1; hence y = 0 ; ::_thesis: verum end; theorem Th83: :: XXREAL_3:83 for y being ext-real number st 0 < y & y <> +infty holds +infty / y = +infty proof let y be ext-real number ; ::_thesis: ( 0 < y & y <> +infty implies +infty / y = +infty ) assume that A1: 0 < y and A2: y <> +infty ; ::_thesis: +infty / y = +infty y " <> 0 by A1, A2, Th82; hence +infty / y = +infty by A1, Def5; ::_thesis: verum end; theorem Th84: :: XXREAL_3:84 for y being ext-real number st y < 0 & -infty <> y holds -infty / y = +infty proof let y be ext-real number ; ::_thesis: ( y < 0 & -infty <> y implies -infty / y = +infty ) assume that A1: y < 0 and A2: -infty <> y ; ::_thesis: -infty / y = +infty y " <> 0 by A1, A2, Th82; hence -infty / y = +infty by A1, Def5; ::_thesis: verum end; theorem Th85: :: XXREAL_3:85 for y being ext-real number st y < 0 & -infty <> y holds +infty / y = -infty proof let y be ext-real number ; ::_thesis: ( y < 0 & -infty <> y implies +infty / y = -infty ) assume that A1: y < 0 and A2: -infty <> y ; ::_thesis: +infty / y = -infty y " <> 0 by A1, A2, Th82; hence +infty / y = -infty by A1, Def5; ::_thesis: verum end; theorem Th86: :: XXREAL_3:86 for y being ext-real number st 0 < y & y <> +infty holds -infty / y = -infty proof let y be ext-real number ; ::_thesis: ( 0 < y & y <> +infty implies -infty / y = -infty ) assume that A1: 0 < y and A2: y <> +infty ; ::_thesis: -infty / y = -infty y " <> 0 by A1, A2, Th82; hence -infty / y = -infty by A1, Def5; ::_thesis: verum end; theorem :: XXREAL_3:87 for x being ext-real number st x <> +infty & x <> -infty & x <> 0 holds ( x * (1 / x) = 1 & (1 / x) * x = 1 ) proof let x be ext-real number ; ::_thesis: ( x <> +infty & x <> -infty & x <> 0 implies ( x * (1 / x) = 1 & (1 / x) * x = 1 ) ) assume that A1: ( x <> +infty & x <> -infty ) and A2: x <> 0 ; ::_thesis: ( x * (1 / x) = 1 & (1 / x) * x = 1 ) x in REAL by A1, XXREAL_0:14; then reconsider a = x as real number ; x * (1 / x) = a * (1 / a) .= 1 by A2, XCMPLX_1:106 ; hence ( x * (1 / x) = 1 & (1 / x) * x = 1 ) ; ::_thesis: verum end; theorem :: XXREAL_3:88 for y, x being ext-real number st -infty <> y & y <> +infty & y <> 0 holds ( (x * y) / y = x & x * (y / y) = x ) proof let y, x be ext-real number ; ::_thesis: ( -infty <> y & y <> +infty & y <> 0 implies ( (x * y) / y = x & x * (y / y) = x ) ) assume that A1: -infty <> y and A2: y <> +infty and A3: y <> 0 ; ::_thesis: ( (x * y) / y = x & x * (y / y) = x ) reconsider b = y as Element of REAL by A1, A2, XXREAL_0:14; A4: (x * y) / y = x proof percases ( x = +infty or x = -infty or ( x <> +infty & x <> -infty ) ) ; supposeA5: x = +infty ; ::_thesis: (x * y) / y = x percases ( 0 < y or y < 0 ) by A3; supposeA6: 0 < y ; ::_thesis: (x * y) / y = x then x * y = +infty by A5, Def5; hence (x * y) / y = x by A2, A5, A6, Th83; ::_thesis: verum end; supposeA7: y < 0 ; ::_thesis: (x * y) / y = x then x * y = -infty by A5, Def5; hence (x * y) / y = x by A1, A5, A7, Th84; ::_thesis: verum end; end; end; supposeA8: x = -infty ; ::_thesis: (x * y) / y = x percases ( 0 < y or y < 0 ) by A3; supposeA9: 0 < y ; ::_thesis: (x * y) / y = x then x * y = -infty by A8, Def5; hence (x * y) / y = x by A2, A8, A9, Th86; ::_thesis: verum end; supposeA10: y < 0 ; ::_thesis: (x * y) / y = x then x * y = +infty by A8, Def5; hence (x * y) / y = x by A1, A8, A10, Th85; ::_thesis: verum end; end; end; suppose ( x <> +infty & x <> -infty ) ; ::_thesis: (x * y) / y = x then x in REAL by XXREAL_0:14; then reconsider a = x as real number ; (x * y) / y = (a * b) / b .= a by A3, XCMPLX_1:89 ; hence (x * y) / y = x ; ::_thesis: verum end; end; end; y / y = 1 by A1, A2, A3, Th78; hence ( (x * y) / y = x & x * (y / y) = x ) by A4, Th81; ::_thesis: verum end; theorem :: XXREAL_3:89 for y being ext-real number holds ( +infty * y <> 1 & -infty * y <> 1 ) proof let y be ext-real number ; ::_thesis: ( +infty * y <> 1 & -infty * y <> 1 ) ( y = 0 or 0 < y or y < 0 ) ; hence ( +infty * y <> 1 & -infty * y <> 1 ) by Def5; ::_thesis: verum end; theorem :: XXREAL_3:90 for x, y being ext-real number st x * y <> +infty & x * y <> -infty & not x in REAL holds y in REAL proof let x, y be ext-real number ; ::_thesis: ( x * y <> +infty & x * y <> -infty & not x in REAL implies y in REAL ) assume that A1: x * y <> +infty and A2: x * y <> -infty ; ::_thesis: ( x in REAL or y in REAL ) assume A3: ( not x in REAL & not y in REAL ) ; ::_thesis: contradiction percases ( ( x = +infty & y = +infty ) or ( x = +infty & y = -infty ) or ( x = -infty & y = +infty ) or ( x = -infty & y = -infty ) ) by A3, XXREAL_0:14; suppose ( x = +infty & y = +infty ) ; ::_thesis: contradiction hence contradiction by A1, Def5; ::_thesis: verum end; suppose ( x = +infty & y = -infty ) ; ::_thesis: contradiction hence contradiction by A2, Def5; ::_thesis: verum end; suppose ( x = -infty & y = +infty ) ; ::_thesis: contradiction hence contradiction by A2, Def5; ::_thesis: verum end; suppose ( x = -infty & y = -infty ) ; ::_thesis: contradiction hence contradiction by A1, Def5; ::_thesis: verum end; end; end; begin theorem Th91: :: XXREAL_3:91 for x being ext-real number holds (- 1) * x = - x proof let x be ext-real number ; ::_thesis: (- 1) * x = - x percases ( x in REAL or x = -infty or x = +infty ) by XXREAL_0:14; suppose x in REAL ; ::_thesis: (- 1) * x = - x then reconsider x = x, y = - 1 as real number ; y * x = - x ; hence (- 1) * x = - x ; ::_thesis: verum end; supposeA1: x = -infty ; ::_thesis: (- 1) * x = - x hence (- 1) * x = +infty by Def5 .= - x by A1, Def3 ; ::_thesis: verum end; supposeA2: x = +infty ; ::_thesis: (- 1) * x = - x hence (- 1) * x = -infty by Def5 .= - x by A2, Def3 ; ::_thesis: verum end; end; end; theorem Th92: :: XXREAL_3:92 for x, y being ext-real number holds - (x * y) = (- x) * y proof let x, y be ext-real number ; ::_thesis: - (x * y) = (- x) * y thus - (x * y) = (- 1) * (x * y) by Th91 .= ((- 1) * x) * y by Th66 .= (- x) * y by Th91 ; ::_thesis: verum end; theorem Th93: :: XXREAL_3:93 for y, z, x being ext-real number st y = - z holds x * (y + z) = (x * y) + (x * z) proof let y, z, x be ext-real number ; ::_thesis: ( y = - z implies x * (y + z) = (x * y) + (x * z) ) assume A1: y = - z ; ::_thesis: x * (y + z) = (x * y) + (x * z) hence x * (y + z) = x * 0 by Th7 .= (x * y) - (x * y) by Th7 .= (x * y) + (x * (- y)) by Th92 .= (x * y) + (x * z) by A1 ; ::_thesis: verum end; theorem Th94: :: XXREAL_3:94 for x being ext-real number holds 2 * x = x + x proof let x be ext-real number ; ::_thesis: 2 * x = x + x percases ( x in REAL or x = -infty or x = +infty ) by XXREAL_0:14; suppose x in REAL ; ::_thesis: 2 * x = x + x then reconsider x = x as real number ; 2 * x = x + x ; hence 2 * x = x + x ; ::_thesis: verum end; supposeA1: x = -infty ; ::_thesis: 2 * x = x + x hence 2 * x = -infty by Def5 .= x + x by A1, Def2 ; ::_thesis: verum end; supposeA2: x = +infty ; ::_thesis: 2 * x = x + x hence 2 * x = +infty by Def5 .= x + x by A2, Def2 ; ::_thesis: verum end; end; end; Lm23: for x, y being ext-real number holds x * (y + y) = (x * y) + (x * y) proof let x, y be ext-real number ; ::_thesis: x * (y + y) = (x * y) + (x * y) thus x * (y + y) = x * (2 * y) by Th94 .= 2 * (x * y) by Th66 .= (x * y) + (x * y) by Th94 ; ::_thesis: verum end; Lm24: for x, z being ext-real number holds x * (0 + z) = (x * 0) + (x * z) proof let x, z be ext-real number ; ::_thesis: x * (0 + z) = (x * 0) + (x * z) thus x * (0 + z) = x * z by Th4 .= (x * 0) + (x * z) by Th4 ; ::_thesis: verum end; Lm25: for y, z being ext-real number holds 0 * (y + z) = (0 * y) + (0 * z) ; Lm26: for x, y, z being ext-real number st x is real & y is real holds x * (y + z) = (x * y) + (x * z) proof let x, y, z be ext-real number ; ::_thesis: ( x is real & y is real implies x * (y + z) = (x * y) + (x * z) ) assume that A1: x is real and A2: y is real ; ::_thesis: x * (y + z) = (x * y) + (x * z) reconsider r = x, s = y as real number by A1, A2; A3: x * y = r * s ; percases ( z in REAL or z = -infty or z = +infty ) by XXREAL_0:14; suppose z in REAL ; ::_thesis: x * (y + z) = (x * y) + (x * z) then reconsider t = z as real number ; reconsider u = s + t, v = r * s, w = r * t as real number ; r * u = v + w ; hence x * (y + z) = (x * y) + (x * z) ; ::_thesis: verum end; supposeA4: z = -infty ; ::_thesis: x * (y + z) = (x * y) + (x * z) then A5: y + z = -infty by A2, Def2; percases ( x is zero or x is positive or x is negative ) ; suppose x is zero ; ::_thesis: x * (y + z) = (x * y) + (x * z) hence x * (y + z) = (x * y) + (x * z) by Lm25; ::_thesis: verum end; supposeA6: x is positive ; ::_thesis: x * (y + z) = (x * y) + (x * z) hence x * (y + z) = -infty by A5, Def5 .= (x * y) + -infty by A3, Def2 .= (x * y) + (x * z) by A4, A6, Def5 ; ::_thesis: verum end; supposeA7: x is negative ; ::_thesis: x * (y + z) = (x * y) + (x * z) hence x * (y + z) = +infty by A5, Def5 .= (x * y) + +infty by A3, Def2 .= (x * y) + (x * z) by A4, A7, Def5 ; ::_thesis: verum end; end; end; supposeA8: z = +infty ; ::_thesis: x * (y + z) = (x * y) + (x * z) then A9: y + z = +infty by A2, Def2; percases ( x is zero or x is positive or x is negative ) ; suppose x is zero ; ::_thesis: x * (y + z) = (x * y) + (x * z) hence x * (y + z) = (x * y) + (x * z) by Lm25; ::_thesis: verum end; supposeA10: x is positive ; ::_thesis: x * (y + z) = (x * y) + (x * z) hence x * (y + z) = +infty by A9, Def5 .= (x * y) + +infty by A3, Def2 .= (x * y) + (x * z) by A8, A10, Def5 ; ::_thesis: verum end; supposeA11: x is negative ; ::_thesis: x * (y + z) = (x * y) + (x * z) hence x * (y + z) = -infty by A9, Def5 .= (x * y) + -infty by A3, Def2 .= (x * y) + (x * z) by A8, A11, Def5 ; ::_thesis: verum end; end; end; end; end; Lm27: for x, y, z being ext-real number st x is real & not y is real holds x * (y + z) = (x * y) + (x * z) proof let x, y, z be ext-real number ; ::_thesis: ( x is real & not y is real implies x * (y + z) = (x * y) + (x * z) ) assume that A1: x is real and A2: not y is real ; ::_thesis: x * (y + z) = (x * y) + (x * z) percases ( z is real or not z is real ) ; suppose z is real ; ::_thesis: x * (y + z) = (x * y) + (x * z) hence x * (y + z) = (x * y) + (x * z) by A1, Lm26; ::_thesis: verum end; suppose not z is real ; ::_thesis: x * (y + z) = (x * y) + (x * z) then A3: not z in REAL ; A4: not y in REAL by A2; percases ( ( y = -infty & z = -infty ) or ( y = -infty & z = +infty ) or ( y = +infty & z = -infty ) or ( y = +infty & z = +infty ) ) by A4, A3, XXREAL_0:14; suppose ( y = -infty & z = -infty ) ; ::_thesis: x * (y + z) = (x * y) + (x * z) hence x * (y + z) = (x * y) + (x * z) by Lm23; ::_thesis: verum end; suppose ( y = -infty & z = +infty ) ; ::_thesis: x * (y + z) = (x * y) + (x * z) hence x * (y + z) = (x * y) + (x * z) by Th5, Th93; ::_thesis: verum end; suppose ( y = +infty & z = -infty ) ; ::_thesis: x * (y + z) = (x * y) + (x * z) hence x * (y + z) = (x * y) + (x * z) by Th6, Th93; ::_thesis: verum end; suppose ( y = +infty & z = +infty ) ; ::_thesis: x * (y + z) = (x * y) + (x * z) hence x * (y + z) = (x * y) + (x * z) by Lm23; ::_thesis: verum end; end; end; end; end; theorem Th95: :: XXREAL_3:95 for x, y, z being ext-real number st x is real holds x * (y + z) = (x * y) + (x * z) proof let x, y, z be ext-real number ; ::_thesis: ( x is real implies x * (y + z) = (x * y) + (x * z) ) assume A1: x is real ; ::_thesis: x * (y + z) = (x * y) + (x * z) percases ( ( y is real & z is real ) or not y is real or not z is real ) ; suppose ( y is real & z is real ) ; ::_thesis: x * (y + z) = (x * y) + (x * z) hence x * (y + z) = (x * y) + (x * z) by A1, Lm26; ::_thesis: verum end; suppose ( not y is real or not z is real ) ; ::_thesis: x * (y + z) = (x * y) + (x * z) hence x * (y + z) = (x * y) + (x * z) by A1, Lm27; ::_thesis: verum end; end; end; theorem Th96: :: XXREAL_3:96 for y, z, x being ext-real number st y >= 0 & z >= 0 holds x * (y + z) = (x * y) + (x * z) proof let y, z, x be ext-real number ; ::_thesis: ( y >= 0 & z >= 0 implies x * (y + z) = (x * y) + (x * z) ) assume A1: ( y >= 0 & z >= 0 ) ; ::_thesis: x * (y + z) = (x * y) + (x * z) percases ( y = 0 or z = 0 or ( y > 0 & z > 0 ) ) by A1; suppose ( y = 0 or z = 0 ) ; ::_thesis: x * (y + z) = (x * y) + (x * z) hence x * (y + z) = (x * y) + (x * z) by Lm24; ::_thesis: verum end; supposeA2: ( y > 0 & z > 0 ) ; ::_thesis: x * (y + z) = (x * y) + (x * z) percases ( x is real or not x is real ) ; suppose x is real ; ::_thesis: x * (y + z) = (x * y) + (x * z) hence x * (y + z) = (x * y) + (x * z) by Th95; ::_thesis: verum end; suppose not x is real ; ::_thesis: x * (y + z) = (x * y) + (x * z) then A3: not x in REAL ; percases ( x = -infty or x = +infty ) by A3, XXREAL_0:14; supposeA4: x = -infty ; ::_thesis: x * (y + z) = (x * y) + (x * z) hence x * (y + z) = -infty by A2, Def5 .= -infty + (x * z) by A2, A4, Def2 .= (x * y) + (x * z) by A2, A4, Def5 ; ::_thesis: verum end; supposeA5: x = +infty ; ::_thesis: x * (y + z) = (x * y) + (x * z) hence x * (y + z) = +infty by A2, Def5 .= +infty + (x * z) by A2, A5, Def2 .= (x * y) + (x * z) by A2, A5, Def5 ; ::_thesis: verum end; end; end; end; end; end; end; theorem :: XXREAL_3:97 for y, z, x being ext-real number st y <= 0 & z <= 0 holds x * (y + z) = (x * y) + (x * z) proof let y, z, x be ext-real number ; ::_thesis: ( y <= 0 & z <= 0 implies x * (y + z) = (x * y) + (x * z) ) assume A1: ( y <= 0 & z <= 0 ) ; ::_thesis: x * (y + z) = (x * y) + (x * z) thus x * (y + z) = - (- (x * (y + z))) .= - (x * (- (y + z))) by Th92 .= - (x * ((- y) + (- z))) by Th9 .= - ((x * (- y)) + (x * (- z))) by A1, Th96 .= - ((- (x * y)) + (x * (- z))) by Th92 .= - ((- (x * y)) + (- (x * z))) by Th92 .= - (- ((x * y) + (x * z))) by Th9 .= (x * y) + (x * z) ; ::_thesis: verum end; theorem :: XXREAL_3:98 for x, z being ext-real number holds x * (0 + z) = (x * 0) + (x * z) by Lm24; theorem :: XXREAL_3:99 for f being ext-real number holds (- f) " = - (f ") proof let f be ext-real number ; ::_thesis: (- f) " = - (f ") percases ( f in REAL or f = +infty or f = -infty ) by XXREAL_0:14; supposeA1: f in REAL ; ::_thesis: (- f) " = - (f ") then reconsider g = f as real number ; A2: - f = - g ; consider a being complex number such that A3: f = a and A4: f " = a " by A1, Def6; A5: (- a) " = - (a ") by XCMPLX_1:222; ex m being complex number st ( - f = m & - (f ") = m " ) proof take - a ; ::_thesis: ( - f = - a & - (f ") = (- a) " ) thus - f = - a by A3, A2; ::_thesis: - (f ") = (- a) " thus - (f ") = (- a) " by A4, A5, A2, Def3; ::_thesis: verum end; hence (- f) " = - (f ") by A2, Def6; ::_thesis: verum end; supposeA6: f = +infty ; ::_thesis: (- f) " = - (f ") hence (- f) " = -infty " by Def3 .= - (f ") by A6 ; ::_thesis: verum end; supposeA7: f = -infty ; ::_thesis: (- f) " = - (f ") hence (- f) " = +infty " by Def3 .= - (f ") by A7 ; ::_thesis: verum end; end; end; theorem :: XXREAL_3:100 for x, y, z being ext-real number st x is real holds x * (y - z) = (x * y) - (x * z) proof let x, y, z be ext-real number ; ::_thesis: ( x is real implies x * (y - z) = (x * y) - (x * z) ) assume x is real ; ::_thesis: x * (y - z) = (x * y) - (x * z) then x * (y - z) = (x * y) + (x * (- z)) by Th95 .= (x * y) + (- (x * z)) by Th92 ; hence x * (y - z) = (x * y) - (x * z) ; ::_thesis: verum end; theorem Th101: :: XXREAL_3:101 for x, y, z being ext-real number st x <= y & z <= 0 holds y * z <= x * z proof let x, y, z be ext-real number ; ::_thesis: ( x <= y & z <= 0 implies y * z <= x * z ) assume ( x <= y & z <= 0 ) ; ::_thesis: y * z <= x * z then A1: x * (- z) <= y * (- z) by Th71; ( - (x * z) = x * (- z) & - (y * z) = y * (- z) ) by Th92; hence y * z <= x * z by A1, Th38; ::_thesis: verum end; theorem Th102: :: XXREAL_3:102 for x, y, z being ext-real number st x < y & z < 0 & z <> -infty holds y * z < x * z proof let x, y, z be ext-real number ; ::_thesis: ( x < y & z < 0 & z <> -infty implies y * z < x * z ) assume ( x < y & z < 0 & z <> -infty ) ; ::_thesis: y * z < x * z then A1: x * (- z) < y * (- z) by Th5, Th10, Th72; ( - (x * z) = x * (- z) & - (y * z) = y * (- z) ) by Th92; hence y * z < x * z by A1, Th38; ::_thesis: verum end; theorem :: XXREAL_3:103 for x, y, z being ext-real number st x <= y & z < 0 holds y / z <= x / z by Th101; theorem :: XXREAL_3:104 for x, y, z being ext-real number st x < y & z < 0 & z <> -infty holds y / z < x / z proof let x, y, z be ext-real number ; ::_thesis: ( x < y & z < 0 & z <> -infty implies y / z < x / z ) assume that A1: x < y and A2: 0 > z and A3: z <> -infty ; ::_thesis: y / z < x / z percases ( z = +infty or z in REAL ) by A3, XXREAL_0:14; suppose z = +infty ; ::_thesis: y / z < x / z hence y / z < x / z by A2; ::_thesis: verum end; suppose z in REAL ; ::_thesis: y / z < x / z then reconsider z = z as real number ; z " < 0 by A2; hence y / z < x / z by A1, Th102; ::_thesis: verum end; end; end; theorem :: XXREAL_3:105 for x being ext-real number holds (x / 2) + (x / 2) = x proof let x be ext-real number ; ::_thesis: (x / 2) + (x / 2) = x (x / 2) + (x / 2) = (x + x) / 2 by Th95 .= (2 * x) / 2 by Th94 .= x * (2 / 2) by Th66 .= x by Th81 ; hence (x / 2) + (x / 2) = x ; ::_thesis: verum end;