:: Subsets of Complex Numbers
:: by Andrzej Trybulec
::
:: Received November 7, 2003
:: Copyright (c) 2003 Association of Mizar Users
Lm1:
omega c= ({ [c,d] where c, d is Element of omega : ( c,d are_relative_prime & d <> {} ) } \ { [k,1] where k is Element of omega : verum } ) \/ omega
by XBOOLE_1:7;
Lm2:
1 = succ 0
;
:: deftheorem defines REAL NUMBERS:def 1 :
Lm3:
REAL+ c= REAL
definition
func COMPLEX -> set equals :: NUMBERS:def 2
((Funcs {0 ,1},REAL ) \ { x where x is Element of Funcs {0 ,1},REAL : x . 1 = 0 } ) \/ REAL ;
coherence
((Funcs {0 ,1},REAL ) \ { x where x is Element of Funcs {0 ,1},REAL : x . 1 = 0 } ) \/ REAL is set
;
func RAT -> set equals :: NUMBERS:def 3
(RAT+ \/ [:{0 },RAT+ :]) \ {[0 ,0 ]};
coherence
(RAT+ \/ [:{0 },RAT+ :]) \ {[0 ,0 ]} is set
;
func INT -> set equals :: NUMBERS:def 4
(NAT \/ [:{0 },NAT :]) \ {[0 ,0 ]};
coherence
(NAT \/ [:{0 },NAT :]) \ {[0 ,0 ]} is set
;
:: original: NATredefine func NAT -> Subset of
REAL ;
coherence
NAT is Subset of REAL
by Lm3, ARYTM_2:2, XBOOLE_1:1;
end;
:: deftheorem defines COMPLEX NUMBERS:def 2 :
:: deftheorem defines RAT NUMBERS:def 3 :
:: deftheorem defines INT NUMBERS:def 4 :
Lm4:
RAT+ c= RAT
Lm5:
NAT c= INT
Lm6:
for x, y, z being set st [x,y] = {z} holds
( z = {x} & x = y )
Lm7:
for a, b being Element of REAL holds not 0 ,one --> a,b in REAL
theorem Th1: :: NUMBERS:1
Lm8:
RAT c= REAL
Lm9:
for i, j being ordinal Element of RAT+ st i in j holds
i < j
Lm10:
for i, j being ordinal Element of RAT+ st i c= j holds
i <=' j
Lm11: 2 =
succ 1
.=
(succ 0 ) \/ {1}
by ORDINAL1:def 1
.=
(0 \/ {0 }) \/ {1}
by ORDINAL1:def 1
.=
{0 ,1}
by ENUMSET1:41
;
Lm12:
for i, k being natural Ordinal st i *^ i = 2 *^ k holds
ex k being natural Ordinal st i = 2 *^ k
1 in omega
;
then reconsider 1' = 1 as Element of RAT+ by Lm1;
2 in omega
;
then reconsider two = 2 as ordinal Element of RAT+ by Lm1;
Lm13:
one + one = two
Lm14:
for i being Element of RAT+ holds i + i = two *' i
theorem Th2: :: NUMBERS:2
theorem Th3: :: NUMBERS:3
Lm15:
INT c= RAT
theorem Th4: :: NUMBERS:4
theorem Th5: :: NUMBERS:5
theorem Th6: :: NUMBERS:6
theorem Th7: :: NUMBERS:7
theorem Th8: :: NUMBERS:8
theorem Th9: :: NUMBERS:9
theorem Th10: :: NUMBERS:10
theorem :: NUMBERS:11
theorem :: NUMBERS:12
theorem :: NUMBERS:13
theorem :: NUMBERS:14
theorem :: NUMBERS:15
theorem :: NUMBERS:16
theorem :: NUMBERS:17
theorem Th18: :: NUMBERS:18
theorem Th19: :: NUMBERS:19
theorem Th20: :: NUMBERS:20
theorem :: NUMBERS:21
theorem :: NUMBERS:22
theorem :: NUMBERS:23
theorem :: NUMBERS:24
theorem :: NUMBERS:25
theorem :: NUMBERS:26
theorem :: NUMBERS:27
theorem :: NUMBERS:28
theorem :: NUMBERS:29
theorem :: NUMBERS:30
:: deftheorem defines ExtREAL NUMBERS:def 5 :
theorem Th31: :: NUMBERS:31
theorem Th32: :: NUMBERS:32
theorem :: NUMBERS:33