:: 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
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
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
:: deftheorem EXTREAL1:def 1 :
canceled;
:: deftheorem EXTREAL1:def 2 :
canceled;
:: deftheorem Def3 defines |. EXTREAL1:def 3 :
theorem :: EXTREAL1:33
canceled;
theorem :: EXTREAL1:34
canceled;
theorem :: EXTREAL1:35
canceled;
theorem :: EXTREAL1:36
theorem :: EXTREAL1:37
theorem :: EXTREAL1:38
theorem :: EXTREAL1:39