:: by Andrzej Trybulec

::

:: Received November 7, 2003

:: Copyright (c) 2003-2012 Association of Mizar Users

begin

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

;

Lm3: REAL+ c= REAL

proof end;

definition

((Funcs ({0,1},REAL)) \ { x where x is Element of Funcs ({0,1},REAL) : x . 1 = 0 } ) \/ REAL is set ;

coherence

(RAT+ \/ [:{0},RAT+:]) \ {[0,0]} is set ;

coherence

(NAT \/ [:{0},NAT:]) \ {[0,0]} is set ;

:: original: NAT

redefine func NAT -> Subset of REAL;

coherence

NAT is Subset of REAL by Lm3, ARYTM_2:2, XBOOLE_1:1;

end;

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;

((Funcs ({0,1},REAL)) \ { x where x is Element of Funcs ({0,1},REAL) : x . 1 = 0 } ) \/ REAL is set ;

coherence

(RAT+ \/ [:{0},RAT+:]) \ {[0,0]} is set ;

coherence

(NAT \/ [:{0},NAT:]) \ {[0,0]} is set ;

:: original: NAT

redefine func NAT -> Subset of REAL;

coherence

NAT is Subset of REAL by Lm3, ARYTM_2:2, XBOOLE_1:1;

:: deftheorem defines COMPLEX NUMBERS:def 2 :

COMPLEX = ((Funcs ({0,1},REAL)) \ { x where x is Element of Funcs ({0,1},REAL) : x . 1 = 0 } ) \/ REAL;

COMPLEX = ((Funcs ({0,1},REAL)) \ { x where x is Element of Funcs ({0,1},REAL) : x . 1 = 0 } ) \/ REAL;

Lm4: RAT+ c= RAT

proof end;

Lm5: NAT c= INT

proof end;

registration

coherence

not COMPLEX is empty ;

coherence

not RAT is empty by Lm4, XBOOLE_1:3;

coherence

not INT is empty by Lm5, XBOOLE_1:3;

end;
not COMPLEX is empty ;

coherence

not RAT is empty by Lm4, XBOOLE_1:3;

coherence

not INT is empty by Lm5, XBOOLE_1:3;

Lm6: for x, y, z being set st [x,y] = {z} holds

( z = {x} & x = y )

proof end;

Lm7: for a, b being Element of REAL holds not (0,one) --> (a,b) in REAL

proof end;

definition
end;

Lm8: RAT c= REAL

proof end;

Lm9: for i, j being ordinal Element of RAT+ st i in j holds

i < j

proof end;

Lm10: for i, j being ordinal Element of RAT+ st i c= j holds

i <=' j

proof end;

Lm11: 2 = succ 1

.= (succ 0) \/ {1} by ORDINAL1:def 1

.= (0 \/ {0}) \/ {1} by ORDINAL1:def 1

.= {0,1} by ENUMSET1:1 ;

Lm12: for i, k being natural Ordinal st i *^ i = 2 *^ k holds

ex k being natural Ordinal st i = 2 *^ k

proof end;

1 in omega

;

then reconsider a9 = 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

proof end;

Lm14: for i being Element of RAT+ holds i + i = two *' i

proof end;

Lm15: INT c= RAT

proof end;

begin

registration

coherence

not INT is finite by Lm5, FINSET_1:1;

coherence

not RAT is finite by Th18, FINSET_1:1;

coherence

not REAL is finite by Th19, FINSET_1:1;

coherence

not COMPLEX is finite by Th20, FINSET_1:1;

end;
not INT is finite by Lm5, FINSET_1:1;

coherence

not RAT is finite by Th18, FINSET_1:1;

coherence

not REAL is finite by Th19, FINSET_1:1;

coherence

not COMPLEX is finite by Th20, FINSET_1:1;