:: Basic Properties of Extended Real Numbers
:: by Noboru Endou , Katsumi Wasaki and Yasunari Shidama
::
:: Received September 7, 2000
:: Copyright (c) 2000 Association of Mizar Users

begin

definition

let x, y be R_eal;
:: original: *
redefine func x * y -> R_eal;
coherence
x * y is R_eal by XXREAL_0:def 1;

end;

theorem :: EXTREAL1:1

canceled;

theorem :: EXTREAL1:2

canceled;

theorem :: EXTREAL1:3

canceled;

theorem :: EXTREAL1:4

canceled;

theorem :: EXTREAL1:5

canceled;

theorem :: EXTREAL1:6

canceled;

theorem :: EXTREAL1:7

canceled;

theorem :: EXTREAL1:8

canceled;

theorem :: EXTREAL1:9

canceled;

theorem :: EXTREAL1:10

canceled;

theorem :: EXTREAL1:11

canceled;

theorem :: EXTREAL1:12

canceled;

theorem Th13: :: EXTREAL1:13

for x, y being R_eal
for a, b being Real st x = a & y = b holds
x * y = a * b

proof end;

definition

let x, y be R_eal;
:: original: /
redefine func x / y -> R_eal;
coherence
x / y is R_eal by XXREAL_0:def 1;

end;

theorem :: EXTREAL1:14

canceled;

theorem :: EXTREAL1:15

canceled;

theorem :: EXTREAL1:16

canceled;

theorem :: EXTREAL1:17

canceled;

theorem :: EXTREAL1:18

canceled;

theorem :: EXTREAL1:19

canceled;

theorem :: EXTREAL1:20

canceled;

theorem :: EXTREAL1:21

canceled;

theorem :: EXTREAL1:22

canceled;

theorem :: EXTREAL1:23

canceled;

theorem :: EXTREAL1:24

canceled;

theorem :: EXTREAL1:25

canceled;

theorem :: EXTREAL1:26

canceled;

theorem :: EXTREAL1:27

canceled;

theorem :: EXTREAL1:28

canceled;

theorem :: EXTREAL1:29

canceled;

theorem :: EXTREAL1:30

canceled;

theorem :: EXTREAL1:31

canceled;

theorem Th32: :: EXTREAL1:32

for x, y being R_eal
for a, b being Real st x = a & y = b holds
x / y = a / b

proof end;

definition

canceled;
canceled;
let x be R_eal;
func |.x.| -> R_eal equals :Def3: :: EXTREAL1:def 3
x if 0 <= x
otherwise - x;
coherence
( ( 0 <= x implies x is R_eal ) & ( not 0 <= x implies - x is R_eal ) ) ;
consistency
for b₁ being R_eal holds verum ;

end;

:: deftheorem EXTREAL1:def 1 :

canceled;

:: deftheorem EXTREAL1:def 2 :

canceled;

:: deftheorem Def3 defines |. EXTREAL1:def 3 :

for x being R_eal holds
( ( 0 <= x implies |.x.| = x ) & ( not 0 <= x implies |.x.| = - x ) );

theorem :: EXTREAL1:33

canceled;

theorem :: EXTREAL1:34

canceled;

theorem :: EXTREAL1:35

canceled;

theorem :: EXTREAL1:36

for x being R_eal st 0 < x holds
|.x.| = x by Def3;

theorem :: EXTREAL1:37

for x being R_eal st x < 0 holds
|.x.| = - x by Def3;

theorem :: EXTREAL1:38

for a, b being Real holds a * b = (R_EAL a) * (R_EAL b)

proof end;

theorem :: EXTREAL1:39

for a, b being Real holds a / b = (R_EAL a) / (R_EAL b)

proof end;