:: Basic Operations on Extended Real Numbers
:: by Andrzej Trybulec
::
:: Received September 23, 2008
:: Copyright (c) 2008 Association of Mizar Users
:: deftheorem Def1 defines <= XXREAL_3:def 1 :
theorem Th1: :: XXREAL_3:1
theorem Th2: :: XXREAL_3:2
theorem Th3: :: XXREAL_3:3
definition
let x,
y be
ext-real number ;
func x + 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 ) )
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 :
:: deftheorem Def3 defines - XXREAL_3:def 3 :
:: deftheorem defines - XXREAL_3:def 4 :
theorem Th4: :: XXREAL_3:4
theorem Th5: :: XXREAL_3:5
theorem Th6: :: XXREAL_3:6
Lm1:
+infty + +infty = +infty
by Def2;
Lm2:
-infty + -infty = -infty
by Def2;
theorem Th7: :: XXREAL_3:7
theorem :: XXREAL_3:8
Lm3:
for x being ext-real number holds
( - x in REAL iff x in REAL )
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)
Lm7:
for x being ext-real number st x in REAL holds
- (x + -infty ) = (- -infty ) + (- x)
theorem Th9: :: XXREAL_3:9
theorem Th10: :: XXREAL_3:10
Lm8:
for x, y being ext-real number holds
( not x + y = +infty or x = +infty or y = +infty )
Lm9:
for x, y being ext-real number holds
( not x + y = -infty or x = -infty or y = -infty )
theorem Th11: :: XXREAL_3:11
theorem :: XXREAL_3:12
theorem Th13: :: XXREAL_3:13
theorem Th14: :: XXREAL_3:14
theorem Th15: :: XXREAL_3:15
theorem :: XXREAL_3:16
theorem :: XXREAL_3:17
theorem Th18: :: XXREAL_3:18
theorem Th19: :: XXREAL_3:19
theorem Th20: :: XXREAL_3:20
theorem Th21: :: XXREAL_3:21
theorem Th22: :: XXREAL_3:22
theorem Th23: :: XXREAL_3:23
theorem :: XXREAL_3:24
Lm10:
- +infty = -infty
by Def3;
Lm11:
for x being ext-real number st x in REAL holds
- (x + -infty ) = (- -infty ) + (- x)
theorem :: XXREAL_3:25
canceled;
theorem Th26: :: XXREAL_3:26
theorem :: XXREAL_3:27
theorem Th28: :: XXREAL_3:28
theorem :: XXREAL_3:29
theorem Th30: :: XXREAL_3:30
theorem Th31: :: XXREAL_3:31
theorem :: XXREAL_3:32
theorem Th33: :: XXREAL_3:33
theorem Th34: :: XXREAL_3:34
theorem :: XXREAL_3:35
Lm12:
for x, y, z being ext-real number st x <= y holds
x + z <= y + z
Lm13:
for x, y being ext-real number st x >= 0 & y > 0 holds
x + y > 0
Lm14:
for x, y being ext-real number st x <= 0 & y < 0 holds
x + y < 0
Lm15:
for x, y being ext-real number st x <= y holds
- y <= - x
theorem :: XXREAL_3:36
theorem :: XXREAL_3:37
canceled;
theorem Th38: :: XXREAL_3:38
theorem Th39: :: XXREAL_3:39
theorem Th40: :: XXREAL_3:40
theorem :: XXREAL_3:41
canceled;
theorem Th42: :: XXREAL_3:42
theorem :: XXREAL_3:43
theorem :: XXREAL_3:44
theorem :: XXREAL_3:45
theorem :: XXREAL_3:46
canceled;
theorem Th47: :: XXREAL_3:47
theorem :: XXREAL_3:48
theorem Th49: :: XXREAL_3:49
theorem Th50: :: XXREAL_3:50
theorem :: XXREAL_3:51
theorem :: XXREAL_3:52
canceled;
theorem :: XXREAL_3:53
theorem :: XXREAL_3:54
canceled;
theorem Th55: :: XXREAL_3:55
theorem :: XXREAL_3:56
theorem Th57: :: XXREAL_3:57
theorem :: XXREAL_3:58
canceled;
theorem :: XXREAL_3:59
canceled;
theorem :: XXREAL_3:60
canceled;
theorem :: XXREAL_3:61
canceled;
theorem :: XXREAL_3:62
canceled;
theorem :: XXREAL_3:63
theorem :: XXREAL_3:64
theorem :: XXREAL_3:65
theorem :: XXREAL_3:66
theorem :: XXREAL_3:67
theorem :: XXREAL_3:68
theorem :: XXREAL_3:69
theorem :: XXREAL_3:70
theorem :: XXREAL_3:71
theorem :: XXREAL_3:72
theorem :: XXREAL_3:73
theorem :: XXREAL_3:74
theorem :: XXREAL_3:75
theorem :: XXREAL_3:76
definition
let x,
y be
ext-real number ;
func x * 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 ) )
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 :
:: deftheorem Def6 defines " XXREAL_3:def 6 :
:: deftheorem defines / XXREAL_3:def 7 :
Lm16:
for x being ext-real number holds x * 0 = 0
Lm17:
for x, y being ext-real number st not x is real & x * y = 0 holds
y = 0
Lm18:
for x, y, z being ext-real number st x = 0 holds
x * (y * z) = (x * y) * z
Lm19:
for y, x, z being ext-real number st y = 0 holds
x * (y * z) = (x * y) * z
Lm20:
for y, x, z being ext-real number st not y is real holds
x * (y * z) = (x * y) * z
Lm21:
for x, y, z being ext-real number st not x is real holds
x * (y * z) = (x * y) * z
theorem Th77: :: XXREAL_3:77
theorem :: XXREAL_3:78
theorem :: XXREAL_3:79
theorem Th80: :: XXREAL_3:80
theorem Th81: :: XXREAL_3:81
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 )
theorem Th82: :: XXREAL_3:82
theorem Th83: :: XXREAL_3:83
theorem :: XXREAL_3:84
theorem :: XXREAL_3:85
theorem :: XXREAL_3:86
theorem :: XXREAL_3:87
theorem :: XXREAL_3:88
theorem Th89: :: XXREAL_3:89
theorem :: XXREAL_3:90
theorem :: XXREAL_3:91
theorem Th92: :: XXREAL_3:92
theorem Th93: :: XXREAL_3:93
theorem Th94: :: XXREAL_3:94
theorem Th95: :: XXREAL_3:95
theorem Th96: :: XXREAL_3:96
theorem Th97: :: XXREAL_3:97
theorem :: XXREAL_3:98
theorem :: XXREAL_3:99
theorem :: XXREAL_3:100
theorem :: XXREAL_3:101
theorem Th102: :: XXREAL_3:102
theorem Th103: :: XXREAL_3:103
theorem Th104: :: XXREAL_3:104
theorem Th105: :: XXREAL_3:105
Lm23:
for x, y being ext-real number holds x * (y + y) = (x * y) + (x * y)
Lm24:
for x, z being ext-real number holds x * (0 + z) = (x * 0 ) + (x * z)
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)
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)
theorem Th106: :: XXREAL_3:106
theorem Th107: :: XXREAL_3:107
theorem :: XXREAL_3:108
canceled;
theorem :: XXREAL_3:109
theorem :: XXREAL_3:110
theorem :: XXREAL_3:111
theorem :: XXREAL_3:112
theorem Th113: :: XXREAL_3:113
theorem Th114: :: XXREAL_3:114
theorem :: XXREAL_3:115
theorem :: XXREAL_3:116
theorem :: XXREAL_3:117