:: COMPLEX1 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

Lm1: one = succ 0 by ORDINAL2:def 4
.= 1 ;

Lm2: 2 = succ 1
.= (succ 0) \/ {1} by ORDINAL1:def 1
.= ({} \/ {0}) \/ {1} by ORDINAL1:def 1
.= {0,one } by Lm1, ENUMSET1:41 ;

theorem :: COMPLEX1:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th2: :: COMPLEX1:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b being real number holds
( (a ^2 ) + (b ^2 ) = 0 iff ( a = 0 & b = 0 ) )
proof end;

Lm3: for a, b being Element of REAL holds 0 <= (a ^2 ) + (b ^2 )
proof end;

registration
cluster -> complex Element of COMPLEX ;
coherence
for b1 being Element of COMPLEX holds b1 is complex ;
end;

definition
let z be complex number ;
canceled;
func Re z -> set means :Def2: :: COMPLEX1:def 2
it = z if z in REAL
otherwise ex f being Function of 2, REAL st
( z = f & it = f . 0 );
existence
( ( z in REAL implies ex b1 being set st b1 = z ) & ( not z in REAL implies ex b1 being set ex f being Function of 2, REAL st
( z = f & b1 = f . 0 ) ) )
proof end;
uniqueness
for b1, b2 being set holds
( ( z in REAL & b1 = z & b2 = z implies b1 = b2 ) & ( not z in REAL & ex f being Function of 2, REAL st
( z = f & b1 = f . 0 ) & ex f being Function of 2, REAL st
( z = f & b2 = f . 0 ) implies b1 = b2 ) ) ;
consistency
for b1 being set holds verum ;
func Im z -> set means :Def3: :: COMPLEX1:def 3
it = 0 if z in REAL
otherwise ex f being Function of 2, REAL st
( z = f & it = f . 1 );
existence
( ( z in REAL implies ex b1 being set st b1 = 0 ) & ( not z in REAL implies ex b1 being set ex f being Function of 2, REAL st
( z = f & b1 = f . 1 ) ) )
proof end;
uniqueness
for b1, b2 being set holds
( ( z in REAL & b1 = 0 & b2 = 0 implies b1 = b2 ) & ( not z in REAL & ex f being Function of 2, REAL st
( z = f & b1 = f . 1 ) & ex f being Function of 2, REAL st
( z = f & b2 = f . 1 ) implies b1 = b2 ) ) ;
consistency
for b1 being set holds verum ;
end;

:: deftheorem COMPLEX1:def 1 :
canceled;

:: deftheorem Def2 defines Re COMPLEX1:def 2 :
for z being complex number
for b2 being set holds
( ( z in REAL implies ( b2 = Re z iff b2 = z ) ) & ( not z in REAL implies ( b2 = Re z iff ex f being Function of 2, REAL st
( z = f & b2 = f . 0 ) ) ) );

:: deftheorem Def3 defines Im COMPLEX1:def 3 :
for z being complex number
for b2 being set holds
( ( z in REAL implies ( b2 = Im z iff b2 = 0 ) ) & ( not z in REAL implies ( b2 = Im z iff ex f being Function of 2, REAL st
( z = f & b2 = f . 1 ) ) ) );

registration
let z be complex number ;
cluster Re z -> real ;
coherence
Re z is real
proof end;
cluster Im z -> real ;
coherence
Im z is real
proof end;
end;

definition
let z be complex number ;
:: original: Re
redefine func Re z -> Real;
coherence
Re z is Real by XREAL_0:def 1;
:: original: Im
redefine func Im z -> Real;
coherence
Im z is Real by XREAL_0:def 1;
end;

theorem :: COMPLEX1:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: COMPLEX1:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th5: :: COMPLEX1:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being Function of 2, REAL ex a, b being Element of REAL st f = 0,1 --> a,b
proof end;

Lm4: for a, b being Element of REAL holds
( Re [*a,b*] = a & Im [*a,b*] = b )
proof end;

Lm5: for z being complex number holds [*(Re z),(Im z)*] = z
proof end;

theorem :: COMPLEX1:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: COMPLEX1:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: COMPLEX1:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th9: :: COMPLEX1:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for z1, z2 being complex number st Re z1 = Re z2 & Im z1 = Im z2 holds
z1 = z2
proof end;

definition
let z1, z2 be complex number ;
canceled;
redefine pred z1 = z2 means :: COMPLEX1:def 5
( Re z1 = Re z2 & Im z1 = Im z2 );
compatibility
( z1 = z2 iff ( Re z1 = Re z2 & Im z1 = Im z2 ) ) by Th9;
end;

:: deftheorem COMPLEX1:def 4 :
canceled;

:: deftheorem defines = COMPLEX1:def 5 :
for z1, z2 being complex number holds
( z1 = z2 iff ( Re z1 = Re z2 & Im z1 = Im z2 ) );

definition
func 0c -> Element of COMPLEX equals :: COMPLEX1:def 6
0;
correctness
coherence
0 is Element of COMPLEX ;
by XCMPLX_0:def 2;
func 1r -> Element of COMPLEX equals :: COMPLEX1:def 7
1;
correctness
coherence
1 is Element of COMPLEX ;
by XCMPLX_0:def 2;
:: original: <i>
redefine func <i> -> Element of COMPLEX equals :: COMPLEX1:def 8
[*0,1*];
coherence
<i> is Element of COMPLEX by XCMPLX_0:def 2;
compatibility
for b1 being Element of COMPLEX holds
( b1 = <i> iff b1 = [*0,1*] ) by Lm1, ARYTM_0:def 7, XCMPLX_0:def 1;
end;

:: deftheorem defines 0c COMPLEX1:def 6 :
0c = 0;

:: deftheorem defines 1r COMPLEX1:def 7 :
1r = 1;

:: deftheorem defines <i> COMPLEX1:def 8 :
<i> = [*0,1*];

Lm6: 0 = [*0,0*]
by ARYTM_0:def 7;

Lm7: 1r = [*1,0*]
by ARYTM_0:def 7;

registration
cluster 0c -> zero complex ;
coherence
0c is empty ;
end;

theorem :: COMPLEX1:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: COMPLEX1:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th12: :: COMPLEX1:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
( Re 0 = 0 & Im 0 = 0 ) by Lm6, Lm4;

theorem Th13: :: COMPLEX1:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for z being complex number holds
( z = 0 iff ((Re z) ^2 ) + ((Im z) ^2 ) = 0 )
proof end;

theorem :: COMPLEX1:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th15: :: COMPLEX1:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
( Re 1r = 1 & Im 1r = 0 ) by Lm7, Lm4;

theorem :: COMPLEX1:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th17: :: COMPLEX1:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
( Re <i> = 0 & Im <i> = 1 ) by Lm4;

Lm8: for x being real number
for x1, x2 being Element of REAL st x = [*x1,x2*] holds
( x2 = 0 & x = x1 )
proof end;

Lm9: for x', y' being Element of REAL
for x, y being real number st x' = x & y' = y holds
+ x',y' = x + y
proof end;

Lm10: for x being Element of REAL holds opp x = - x
proof end;

Lm11: for x', y' being Element of REAL
for x, y being real number st x' = x & y' = y holds
* x',y' = x * y
proof end;

Lm12: for x, y, z being Element of COMPLEX st z = x + y holds
Re z = (Re x) + (Re y)
proof end;

Lm13: for x, y, z being Element of COMPLEX st z = x + y holds
Im z = (Im x) + (Im y)
proof end;

Lm14: for x, y, z being Element of COMPLEX st z = x * y holds
Re z = ((Re x) * (Re y)) - ((Im x) * (Im y))
proof end;

Lm15: for x, y, z being Element of COMPLEX st z = x * y holds
Im z = ((Re x) * (Im y)) + ((Im x) * (Re y))
proof end;

Lm16: for z1, z2 being Element of COMPLEX holds z1 + z2 = [*((Re z1) + (Re z2)),((Im z1) + (Im z2))*]
proof end;

Lm17: for z1, z2 being Element of COMPLEX holds z1 * z2 = [*(((Re z1) * (Re z2)) - ((Im z1) * (Im z2))),(((Re z1) * (Im z2)) + ((Re z2) * (Im z1)))*]
proof end;

Lm18: for z1, z2 being complex number holds
( Re (z1 * z2) = ((Re z1) * (Re z2)) - ((Im z1) * (Im z2)) & Im (z1 * z2) = ((Re z1) * (Im z2)) + ((Re z2) * (Im z1)) )
proof end;

Lm19: for z1, z2 being complex number holds
( Re (z1 + z2) = (Re z1) + (Re z2) & Im (z1 + z2) = (Im z1) + (Im z2) )
proof end;

Lm20: for x being Real holds Re (x * <i> ) = 0
proof end;

Lm21: for x being Real holds Im (x * <i> ) = x
proof end;

Lm22: for x, y being Real holds [*x,y*] = x + (y * <i> )
proof end;

definition
let z1, z2 be Element of COMPLEX ;
:: original: +
redefine func z1 + z2 -> Element of COMPLEX equals :: COMPLEX1:def 9
((Re z1) + (Re z2)) + (((Im z1) + (Im z2)) * <i> );
coherence
z1 + z2 is Element of COMPLEX by XCMPLX_0:def 2;
compatibility
for b1 being Element of COMPLEX holds
( b1 = z1 + z2 iff b1 = ((Re z1) + (Re z2)) + (((Im z1) + (Im z2)) * <i> ) )
proof end;
end;

:: deftheorem defines + COMPLEX1:def 9 :
for z1, z2 being Element of COMPLEX holds z1 + z2 = ((Re z1) + (Re z2)) + (((Im z1) + (Im z2)) * <i> );

theorem :: COMPLEX1:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th19: :: COMPLEX1:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for z1, z2 being complex number holds
( Re (z1 + z2) = (Re z1) + (Re z2) & Im (z1 + z2) = (Im z1) + (Im z2) )
proof end;

definition
let z1, z2 be Element of COMPLEX ;
:: original: *
redefine func z1 * z2 -> Element of COMPLEX equals :: COMPLEX1:def 10
(((Re z1) * (Re z2)) - ((Im z1) * (Im z2))) + ((((Re z1) * (Im z2)) + ((Re z2) * (Im z1))) * <i> );
coherence
z1 * z2 is Element of COMPLEX by XCMPLX_0:def 2;
compatibility
for b1 being Element of COMPLEX holds
( b1 = z1 * z2 iff b1 = (((Re z1) * (Re z2)) - ((Im z1) * (Im z2))) + ((((Re z1) * (Im z2)) + ((Re z2) * (Im z1))) * <i> ) )
proof end;
end;

:: deftheorem defines * COMPLEX1:def 10 :
for z1, z2 being Element of COMPLEX holds z1 * z2 = (((Re z1) * (Re z2)) - ((Im z1) * (Im z2))) + ((((Re z1) * (Im z2)) + ((Re z2) * (Im z1))) * <i> );

theorem :: COMPLEX1:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: COMPLEX1:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: COMPLEX1:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: COMPLEX1:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th24: :: COMPLEX1:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for z1, z2 being complex number holds
( Re (z1 * z2) = ((Re z1) * (Re z2)) - ((Im z1) * (Im z2)) & Im (z1 * z2) = ((Re z1) * (Im z2)) + ((Re z2) * (Im z1)) )
proof end;

theorem Th25: :: COMPLEX1:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being Real holds Re (x * <i> ) = 0
proof end;

theorem Th26: :: COMPLEX1:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being Real holds Im (x * <i> ) = x
proof end;

theorem :: COMPLEX1:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y being Real holds [*x,y*] = x + (y * <i> )
proof end;

theorem Th28: :: COMPLEX1:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b being Element of REAL holds
( Re (a + (b * <i> )) = a & Im (a + (b * <i> )) = b )
proof end;

theorem Th29: :: COMPLEX1:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for z being complex number holds (Re z) + ((Im z) * <i> ) = z
proof end;

theorem Th30: :: COMPLEX1:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for z1, z2 being complex number st Im z1 = 0 & Im z2 = 0 holds
( Re (z1 * z2) = (Re z1) * (Re z2) & Im (z1 * z2) = 0 )
proof end;

theorem Th31: :: COMPLEX1:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for z1, z2 being complex number st Re z1 = 0 & Re z2 = 0 holds
( Re (z1 * z2) = - ((Im z1) * (Im z2)) & Im (z1 * z2) = 0 )
proof end;

theorem :: COMPLEX1:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for z being Element of COMPLEX holds
( Re (z * z) = ((Re z) ^2 ) - ((Im z) ^2 ) & Im (z * z) = 2 * ((Re z) * (Im z)) ) by Th24;

definition
let z be Element of COMPLEX ;
:: original: -
redefine func - z -> Element of COMPLEX equals :Def11: :: COMPLEX1:def 11
(- (Re z)) + ((- (Im z)) * <i> );
coherence
- z is Element of COMPLEX by XCMPLX_0:def 2;
compatibility
for b1 being Element of COMPLEX holds
( b1 = - z iff b1 = (- (Re z)) + ((- (Im z)) * <i> ) )
proof end;
end;

:: deftheorem Def11 defines - COMPLEX1:def 11 :
for z being Element of COMPLEX holds - z = (- (Re z)) + ((- (Im z)) * <i> );

theorem :: COMPLEX1:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th34: :: COMPLEX1:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for z being complex number holds
( Re (- z) = - (Re z) & Im (- z) = - (Im z) )
proof end;

- <i> = 0 + ((- 1) * <i> )
;

then Lm23: ( Re (- <i> ) = 0 & Im (- <i> ) = - 1 )
by Th28;

theorem :: COMPLEX1:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: COMPLEX1:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: COMPLEX1:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
<i> * <i> = - 1r ;

definition
let z1, z2 be Element of COMPLEX ;
:: original: -
redefine func z1 - z2 -> Element of COMPLEX equals :: COMPLEX1:def 12
((Re z1) - (Re z2)) + (((Im z1) - (Im z2)) * <i> );
coherence
z1 - z2 is Element of COMPLEX by XCMPLX_0:def 2;
compatibility
for b1 being Element of COMPLEX holds
( b1 = z1 - z2 iff b1 = ((Re z1) - (Re z2)) + (((Im z1) - (Im z2)) * <i> ) )
proof end;
end;

:: deftheorem defines - COMPLEX1:def 12 :
for z1, z2 being Element of COMPLEX holds z1 - z2 = ((Re z1) - (Re z2)) + (((Im z1) - (Im z2)) * <i> );

theorem :: COMPLEX1:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: COMPLEX1:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: COMPLEX1:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: COMPLEX1:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: COMPLEX1:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: COMPLEX1:43  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: COMPLEX1:44  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: COMPLEX1:45  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: COMPLEX1:46  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: COMPLEX1:47  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th48: :: COMPLEX1:48  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for z1, z2 being Element of COMPLEX holds
( Re (z1 - z2) = (Re z1) - (Re z2) & Im (z1 - z2) = (Im z1) - (Im z2) ) by Th28;

definition
let z be Element of COMPLEX ;
:: original: "
redefine func z " -> Element of COMPLEX equals :Def13: :: COMPLEX1:def 13
((Re z) / (((Re z) ^2 ) + ((Im z) ^2 ))) + (((- (Im z)) / (((Re z) ^2 ) + ((Im z) ^2 ))) * <i> );
coherence
z " is Element of COMPLEX by XCMPLX_0:def 2;
compatibility
for b1 being Element of COMPLEX holds
( b1 = z " iff b1 = ((Re z) / (((Re z) ^2 ) + ((Im z) ^2 ))) + (((- (Im z)) / (((Re z) ^2 ) + ((Im z) ^2 ))) * <i> ) )
proof end;
end;

:: deftheorem Def13 defines " COMPLEX1:def 13 :
for z being Element of COMPLEX holds z " = ((Re z) / (((Re z) ^2 ) + ((Im z) ^2 ))) + (((- (Im z)) / (((Re z) ^2 ) + ((Im z) ^2 ))) * <i> );

theorem :: COMPLEX1:49  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: COMPLEX1:50  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: COMPLEX1:51  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: COMPLEX1:52  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: COMPLEX1:53  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: COMPLEX1:54  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: COMPLEX1:55  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: COMPLEX1:56  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: COMPLEX1:57  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: COMPLEX1:58  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: COMPLEX1:59  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: COMPLEX1:60  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: COMPLEX1:61  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: COMPLEX1:62  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: COMPLEX1:63  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th64: :: COMPLEX1:64  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for z being complex number holds
( Re (z " ) = (Re z) / (((Re z) ^2 ) + ((Im z) ^2 )) & Im (z " ) = (- (Im z)) / (((Re z) ^2 ) + ((Im z) ^2 )) )
proof end;

theorem :: COMPLEX1:65  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: COMPLEX1:66  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: COMPLEX1:67  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: COMPLEX1:68  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: COMPLEX1:69  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: COMPLEX1:70  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: COMPLEX1:71  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: COMPLEX1:72  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
<i> " = - <i> ;

theorem :: COMPLEX1:73  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: COMPLEX1:74  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: COMPLEX1:75  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: COMPLEX1:76  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: COMPLEX1:77  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: COMPLEX1:78  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th79: :: COMPLEX1:79  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for z being Element of COMPLEX st Re z <> 0 & Im z = 0 holds
( Re (z " ) = (Re z) " & Im (z " ) = 0 )
proof end;

theorem Th80: :: COMPLEX1:80  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for z being Element of COMPLEX st Re z = 0 & Im z <> 0 holds
( Re (z " ) = 0 & Im (z " ) = - ((Im z) " ) )
proof end;

definition
let z1, z2 be Element of COMPLEX ;
:: original: /
redefine func z1 / z2 -> Element of COMPLEX equals :: COMPLEX1:def 14
((((Re z1) * (Re z2)) + ((Im z1) * (Im z2))) / (((Re z2) ^2 ) + ((Im z2) ^2 ))) + (((((Re z2) * (Im z1)) - ((Re z1) * (Im z2))) / (((Re z2) ^2 ) + ((Im z2) ^2 ))) * <i> );
coherence
z1 / z2 is Element of COMPLEX by XCMPLX_0:def 2;
compatibility
for b1 being Element of COMPLEX holds
( b1 = z1 / z2 iff b1 = ((((Re z1) * (Re z2)) + ((Im z1) * (Im z2))) / (((Re z2) ^2 ) + ((Im z2) ^2 ))) + (((((Re z2) * (Im z1)) - ((Re z1) * (Im z2))) / (((Re z2) ^2 ) + ((Im z2) ^2 ))) * <i> ) )
proof end;
end;

:: deftheorem defines / COMPLEX1:def 14 :
for z1, z2 being Element of COMPLEX holds z1 / z2 = ((((Re z1) * (Re z2)) + ((Im z1) * (Im z2))) / (((Re z2) ^2 ) + ((Im z2) ^2 ))) + (((((Re z2) * (Im z1)) - ((Re z1) * (Im z2))) / (((Re z2) ^2 ) + ((Im z2) ^2 ))) * <i> );

theorem :: COMPLEX1:81  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: COMPLEX1:82  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for z1, z2 being Element of COMPLEX holds
( Re (z1 / z2) = (((Re z1) * (Re z2)) + ((Im z1) * (Im z2))) / (((Re z2) ^2 ) + ((Im z2) ^2 )) & Im (z1 / z2) = (((Re z2) * (Im z1)) - ((Re z1) * (Im z2))) / (((Re z2) ^2 ) + ((Im z2) ^2 )) ) by Th28;

theorem :: COMPLEX1:83  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: COMPLEX1:84  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: COMPLEX1:85  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: COMPLEX1:86  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: COMPLEX1:87  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: COMPLEX1:88  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: COMPLEX1:89  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: COMPLEX1:90  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: COMPLEX1:91  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: COMPLEX1:92  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: COMPLEX1:93  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: COMPLEX1:94  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: COMPLEX1:95  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: COMPLEX1:96  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: COMPLEX1:97  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: COMPLEX1:98  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: COMPLEX1:99  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: COMPLEX1:100  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: COMPLEX1:101  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: COMPLEX1:102  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: COMPLEX1:103  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: COMPLEX1:104  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: COMPLEX1:105  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: COMPLEX1:106  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: COMPLEX1:107  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: COMPLEX1:108  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: COMPLEX1:109  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for z1, z2 being Element of COMPLEX st Im z1 = 0 & Im z2 = 0 & Re z2 <> 0 holds
( Re (z1 / z2) = (Re z1) / (Re z2) & Im (z1 / z2) = 0 )
proof end;

theorem :: COMPLEX1:110  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for z1, z2 being Element of COMPLEX st Re z1 = 0 & Re z2 = 0 & Im z2 <> 0 holds
( Re (z1 / z2) = (Im z1) / (Im z2) & Im (z1 / z2) = 0 )
proof end;

definition
let z be complex number ;
func z *' -> complex number equals :: COMPLEX1:def 15
(Re z) - ((Im z) * <i> );
correctness
coherence
(Re z) - ((Im z) * <i> ) is complex number ;
;
involutiveness
for b1, b2 being complex number st b1 = (Re b2) - ((Im b2) * <i> ) holds
b2 = (Re b1) - ((Im b1) * <i> )
proof end;
end;

:: deftheorem defines *' COMPLEX1:def 15 :
for z being complex number holds z *' = (Re z) - ((Im z) * <i> );

definition
let z be complex number ;
:: original: *'
redefine func z *' -> Element of COMPLEX ;
coherence
z *' is Element of COMPLEX by XCMPLX_0:def 2;
end;

theorem :: COMPLEX1:111  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th112: :: COMPLEX1:112  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for z being complex number holds
( Re (z *' ) = Re z & Im (z *' ) = - (Im z) )
proof end;

theorem :: COMPLEX1:113  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
0 *' = 0 by Th12;

theorem :: COMPLEX1:114  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for z being complex number st z *' = 0 holds
z = 0
proof end;

theorem :: COMPLEX1:115  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
1r *' = 1r by Th15;

Lm24: ( Re (<i> *' ) = 0 & Im (<i> *' ) = - 1 )
by Th17, Th112;

theorem :: COMPLEX1:116  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
<i> *' = - <i> by Lm23, Lm24, Th9;

theorem :: COMPLEX1:117  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th118: :: COMPLEX1:118  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for z1, z2 being complex number holds (z1 + z2) *' = (z1 *' ) + (z2 *' )
proof end;

theorem Th119: :: COMPLEX1:119  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for z being Element of COMPLEX holds (- z) *' = - (z *' )
proof end;

theorem :: COMPLEX1:120  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for z1, z2 being Element of COMPLEX holds (z1 - z2) *' = (z1 *' ) - (z2 *' )
proof end;

theorem Th121: :: COMPLEX1:121  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for z1, z2 being Element of COMPLEX holds (z1 * z2) *' = (z1 *' ) * (z2 *' )
proof end;

theorem Th122: :: COMPLEX1:122  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for z being Element of COMPLEX holds (z " ) *' = (z *' ) "
proof end;

theorem :: COMPLEX1:123  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for z1, z2 being Element of COMPLEX holds (z1 / z2) *' = (z1 *' ) / (z2 *' )
proof end;

theorem :: COMPLEX1:124  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for z being Element of COMPLEX st Im z = 0 holds
z *' = z
proof end;

theorem :: COMPLEX1:125  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for z being Element of COMPLEX st Re z = 0 holds
z *' = - z ;

theorem :: COMPLEX1:126  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for z being Element of COMPLEX holds
( Re (z * (z *' )) = ((Re z) ^2 ) + ((Im z) ^2 ) & Im (z * (z *' )) = 0 )
proof end;

theorem :: COMPLEX1:127  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for z being Element of COMPLEX holds
( Re (z + (z *' )) = 2 * (Re z) & Im (z + (z *' )) = 0 )
proof end;

theorem :: COMPLEX1:128  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for z being Element of COMPLEX holds
( Re (z - (z *' )) = 0 & Im (z - (z *' )) = 2 * (Im z) )
proof end;

definition
let z be complex number ;
func |.z.| -> complex number equals :: COMPLEX1:def 16
 sqrt (((Re z) ^2 ) + ((Im z) ^2 ));
coherence
sqrt (((Re z) ^2 ) + ((Im z) ^2 )) is complex number ;
projectivity
for b1, b2 being complex number st b1 = sqrt (((Re b2) ^2 ) + ((Im b2) ^2 )) holds
b1 = sqrt (((Re b1) ^2 ) + ((Im b1) ^2 ))
proof end;
end;

:: deftheorem defines |. COMPLEX1:def 16 :
for z being complex number holds |.z.| = sqrt (((Re z) ^2 ) + ((Im z) ^2 ));

registration
let z be complex number ;
cluster |.z.| -> complex real ;
coherence
|.z.| is real ;
end;

definition
let z be complex number ;
:: original: |.
redefine func |.z.| -> Real;
coherence
|.z.| is Real ;
end;

Lm25: sqrt ((0 ^2 ) + (0 ^2 )) = 0
by SQUARE_1:82;

theorem Th129: :: COMPLEX1:129  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being real number st x >= 0 holds
|.x.| = x
proof end;

theorem Th130: :: COMPLEX1:130  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
|.0.| = 0 by Lm25, Th12;

theorem Th131: :: COMPLEX1:131  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for z being complex number st |.z.| = 0 holds
z = 0
proof end;

theorem Th132: :: COMPLEX1:132  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for z being complex number holds 0 <= |.z.|
proof end;

theorem :: COMPLEX1:133  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for z being complex number holds
( z <> 0 iff 0 < |.z.| )
proof end;

Lm26: sqrt ((1 ^2 ) + (0 ^2 )) = 1
by SQUARE_1:83;

theorem :: COMPLEX1:134  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
|.1r .| = 1 by Lm26, Th15;

Lm27: sqrt ((0 ^2 ) + (1 ^2 )) = 1
by SQUARE_1:83;

theorem :: COMPLEX1:135  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
|.<i> .| = 1 by Lm27, Th17;

Lm28: for z being complex number holds |.(- z).| = |.z.|
proof end;

Lm29: for a being real number st a <= 0 holds
|.a.| = - a
proof end;

Lm30: for a being real number holds sqrt (a ^2 ) = |.a.|
proof end;

theorem :: COMPLEX1:136  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for z being complex number st Im z = 0 holds
|.z.| = |.(Re z).| by Lm30;

theorem :: COMPLEX1:137  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for z being complex number st Re z = 0 holds
|.z.| = |.(Im z).| by Lm30;

theorem :: COMPLEX1:138  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for z being complex number holds |.(- z).| = |.z.| by Lm28;

theorem Th139: :: COMPLEX1:139  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for z being complex number holds |.(z *' ).| = |.z.|
proof end;

Lm31: for x being real number holds
( - |.x.| <= x & x <= |.x.| )
proof end;

theorem :: COMPLEX1:140  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for z being complex number holds Re z <= |.z.|
proof end;

theorem :: COMPLEX1:141  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for z being complex number holds Im z <= |.z.|
proof end;

theorem Th142: :: COMPLEX1:142  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for z1, z2 being complex number holds |.(z1 + z2).| <= |.z1.| + |.z2.|
proof end;

theorem Th143: :: COMPLEX1:143  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for z1, z2 being complex number holds |.(z1 - z2).| <= |.z1.| + |.z2.|
proof end;

theorem :: COMPLEX1:144  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for z1, z2 being complex number holds |.z1.| - |.z2.| <= |.(z1 + z2).|
proof end;

theorem Th145: :: COMPLEX1:145  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for z1, z2 being complex number holds |.z1.| - |.z2.| <= |.(z1 - z2).|
proof end;

theorem Th146: :: COMPLEX1:146  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for z1, z2 being complex number holds |.(z1 - z2).| = |.(z2 - z1).|
proof end;

theorem Th147: :: COMPLEX1:147  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for z1, z2 being complex number holds
( |.(z1 - z2).| = 0 iff z1 = z2 )
proof end;

theorem :: COMPLEX1:148  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for z1, z2 being complex number holds
( z1 <> z2 iff 0 < |.(z1 - z2).| )
proof end;

theorem :: COMPLEX1:149  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for z, z1, z2 being complex number holds |.(z1 - z2).| <= |.(z1 - z).| + |.(z - z2).|
proof end;

Lm32: for x, y being real number holds
( ( - y <= x & x <= y ) iff |.x.| <= y )
proof end;

theorem :: COMPLEX1:150  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for z1, z2 being complex number holds |.(|.z1.| - |.z2.|).| <= |.(z1 - z2).|
proof end;

theorem Th151: :: COMPLEX1:151  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for z1, z2 being complex number holds |.(z1 * z2).| = |.z1.| * |.z2.|
proof end;

theorem Th152: :: COMPLEX1:152  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for z being complex number holds |.(z " ).| = |.z.| "
proof end;

theorem :: COMPLEX1:153  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for z1, z2 being complex number holds |.z1.| / |.z2.| = |.(z1 / z2).|
proof end;

theorem :: COMPLEX1:154  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for z being complex number holds |.(z * z).| = ((Re z) ^2 ) + ((Im z) ^2 )
proof end;

theorem :: COMPLEX1:155  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for z being complex number holds |.(z * z).| = |.(z * (z *' )).|
proof end;

theorem :: COMPLEX1:156  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being real number st a <= 0 holds
|.a.| = - a by Lm29;

theorem Th157: :: COMPLEX1:157  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being real number holds
( |.a.| = a or |.a.| = - a )
proof end;

theorem :: COMPLEX1:158  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being real number holds sqrt (a ^2 ) = |.a.| by Lm30;

theorem :: COMPLEX1:159  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y being real number holds min x,y = ((x + y) - |.(x - y).|) / 2
proof end;

theorem :: COMPLEX1:160  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y being real number holds max x,y = ((x + y) + |.(x - y).|) / 2
proof end;

theorem :: COMPLEX1:161  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being real number holds |.x.| ^2 = x ^2
proof end;

theorem :: COMPLEX1:162  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being real number holds
( - |.x.| <= x & x <= |.x.| ) by Lm31;

notation
let x be complex number ;
synonym absx.| for |.x.|;
end;

definition
let x be complex number ;
:: original: |.
redefine func abs x -> Real;
coherence
|.x.| is Real ;
end;

theorem :: COMPLEX1:163  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, c, d being Element of REAL st a + (b * <i> ) = c + (d * <i> ) holds
( a = c & b = d )
proof end;