:: The Field of Complex Numbers
:: by Anna Justyna Milewska
::
:: Received January 18, 2000
:: Copyright (c) 2000-2021 Association of Mizar Users


definition
func F_Complex -> strict doubleLoopStr means :Def1: :: COMPLFLD:def 1
( the carrier of it = COMPLEX & the addF of it = addcomplex & the multF of it = multcomplex & 1. it = 1r & 0. it = 0c );
existence
ex b1 being strict doubleLoopStr st
( the carrier of b1 = COMPLEX & the addF of b1 = addcomplex & the multF of b1 = multcomplex & 1. b1 = 1r & 0. b1 = 0c )
proof end;
uniqueness
for b1, b2 being strict doubleLoopStr st the carrier of b1 = COMPLEX & the addF of b1 = addcomplex & the multF of b1 = multcomplex & 1. b1 = 1r & 0. b1 = 0c & the carrier of b2 = COMPLEX & the addF of b2 = addcomplex & the multF of b2 = multcomplex & 1. b2 = 1r & 0. b2 = 0c holds
b1 = b2 ;
end;

:: deftheorem Def1 defines F_Complex COMPLFLD:def 1 :
for b1 being strict doubleLoopStr holds
( b1 = F_Complex iff ( the carrier of b1 = COMPLEX & the addF of b1 = addcomplex & the multF of b1 = multcomplex & 1. b1 = 1r & 0. b1 = 0c ) );

registration
cluster F_Complex -> non empty strict ;
coherence
not F_Complex is empty by Def1;
end;

registration
cluster the carrier of F_Complex -> complex-membered ;
coherence
the carrier of F_Complex is complex-membered by Def1;
end;

registration
let a, b be Complex;
let x, y be Element of F_Complex;
identify x + y with a + b when x = a, y = b;
compatibility
( x = a & y = b implies x + y = a + b )
proof end;
identify x * y with a * b when x = a, y = b;
compatibility
( x = a & y = b implies x * y = a * b )
proof end;
end;

registration
cluster F_Complex -> strict well-unital ;
coherence
F_Complex is well-unital
proof end;
end;

Lm1: 1_ F_Complex = 1r
by Def1;

Lm2: 1. F_Complex = 1r
by Def1;

registration
cluster F_Complex -> non degenerated right_complementable almost_left_invertible strict right_unital distributive left_unital Abelian add-associative right_zeroed associative commutative ;
coherence
( F_Complex is add-associative & F_Complex is right_zeroed & F_Complex is right_complementable & F_Complex is Abelian & F_Complex is commutative & F_Complex is associative & F_Complex is left_unital & F_Complex is right_unital & F_Complex is distributive & F_Complex is almost_left_invertible & not F_Complex is degenerated )
proof end;
end;

theorem :: COMPLFLD:1
for x1, y1 being Element of F_Complex
for x2, y2 being Complex st x1 = x2 & y1 = y2 holds
x1 + y1 = x2 + y2 ;

theorem Th2: :: COMPLFLD:2
for x1 being Element of F_Complex
for x2 being Complex st x1 = x2 holds
- x1 = - x2
proof end;

theorem Th3: :: COMPLFLD:3
for x1, y1 being Element of F_Complex
for x2, y2 being Complex st x1 = x2 & y1 = y2 holds
x1 - y1 = x2 - y2
proof end;

theorem :: COMPLFLD:4
for x1, y1 being Element of F_Complex
for x2, y2 being Complex st x1 = x2 & y1 = y2 holds
x1 * y1 = x2 * y2 ;

theorem Th5: :: COMPLFLD:5
for x1 being Element of F_Complex
for x2 being Complex st x1 = x2 & x1 <> 0. F_Complex holds
x1 " = x2 "
proof end;

theorem Th6: :: COMPLFLD:6
for x1, y1 being Element of F_Complex
for x2, y2 being Complex st x1 = x2 & y1 = y2 & y1 <> 0. F_Complex holds
x1 / y1 = x2 / y2
proof end;

theorem Th7: :: COMPLFLD:7
0. F_Complex = 0c by Def1;

theorem :: COMPLFLD:8
1_ F_Complex = 1r by Def1;

theorem :: COMPLFLD:9
(1_ F_Complex) + (1_ F_Complex) <> 0. F_Complex by Def1, Lm1;

definition
let z be Element of F_Complex;
:: original: *'
redefine func z *' -> Element of F_Complex;
coherence
z *' is Element of F_Complex
proof end;
end;

theorem :: COMPLFLD:10
for z being Element of F_Complex holds - z = (- (1_ F_Complex)) * z
proof end;

theorem :: COMPLFLD:11
for z1, z2 being Element of F_Complex holds z1 - (- z2) = z1 + z2
proof end;

theorem :: COMPLFLD:12
for z, z1 being Element of F_Complex holds z1 = (z1 + z) - z
proof end;

theorem :: COMPLFLD:13
for z, z1 being Element of F_Complex holds z1 = (z1 - z) + z
proof end;

theorem :: COMPLFLD:14
for z1, z2 being Element of F_Complex st z1 <> 0. F_Complex & z2 <> 0. F_Complex & z1 " = z2 " holds
z1 = z2
proof end;

theorem :: COMPLFLD:15
for z1, z2 being Element of F_Complex st z2 <> 0. F_Complex & ( z1 * z2 = 1. F_Complex or z2 * z1 = 1. F_Complex ) holds
z1 = z2 "
proof end;

theorem :: COMPLFLD:16
for z1, z2, z3 being Element of F_Complex st z2 <> 0. F_Complex & ( z1 * z2 = z3 or z2 * z1 = z3 ) holds
( z1 = z3 * (z2 ") & z1 = (z2 ") * z3 )
proof end;

theorem :: COMPLFLD:17
(1. F_Complex) " = 1. F_Complex
proof end;

theorem :: COMPLFLD:18
for z1, z2 being Element of F_Complex st z1 <> 0. F_Complex & z2 <> 0. F_Complex holds
(z1 * z2) " = (z1 ") * (z2 ")
proof end;

theorem :: COMPLFLD:19
for z being Element of F_Complex st z <> 0. F_Complex holds
(- z) " = - (z ")
proof end;

theorem :: COMPLFLD:20
for z1, z2 being Element of F_Complex st z1 <> 0. F_Complex & z2 <> 0. F_Complex holds
(z1 ") + (z2 ") = (z1 + z2) * ((z1 * z2) ")
proof end;

theorem :: COMPLFLD:21
for z1, z2 being Element of F_Complex st z1 <> 0. F_Complex & z2 <> 0. F_Complex holds
(z1 ") - (z2 ") = (z2 - z1) * ((z1 * z2) ")
proof end;

theorem :: COMPLFLD:22
for z being Element of F_Complex st z <> 0. F_Complex holds
z " = (1. F_Complex) / z ;

theorem :: COMPLFLD:23
for z being Element of F_Complex holds z / (1. F_Complex) = z
proof end;

theorem :: COMPLFLD:24
for z being Element of F_Complex st z <> 0. F_Complex holds
z / z = 1. F_Complex
proof end;

theorem :: COMPLFLD:25
for z being Element of F_Complex st z <> 0. F_Complex holds
(0. F_Complex) / z = 0. F_Complex ;

theorem Th26: :: COMPLFLD:26
for z1, z2 being Element of F_Complex st z2 <> 0. F_Complex & z1 / z2 = 0. F_Complex holds
z1 = 0. F_Complex
proof end;

theorem :: COMPLFLD:27
for z1, z2, z3, z4 being Element of F_Complex st z2 <> 0. F_Complex & z4 <> 0. F_Complex holds
(z1 / z2) * (z3 / z4) = (z1 * z3) / (z2 * z4)
proof end;

theorem :: COMPLFLD:28
for z, z1, z2 being Element of F_Complex st z2 <> 0. F_Complex holds
z * (z1 / z2) = (z * z1) / z2 ;

theorem :: COMPLFLD:29
for z1, z2 being Element of F_Complex st z2 <> 0. F_Complex & z1 / z2 = 1. F_Complex holds
z1 = z2
proof end;

theorem :: COMPLFLD:30
for z, z1 being Element of F_Complex st z <> 0. F_Complex holds
z1 = (z1 * z) / z
proof end;

theorem :: COMPLFLD:31
for z1, z2 being Element of F_Complex st z1 <> 0. F_Complex & z2 <> 0. F_Complex holds
(z1 / z2) " = z2 / z1
proof end;

theorem :: COMPLFLD:32
for z1, z2 being Element of F_Complex st z1 <> 0. F_Complex & z2 <> 0. F_Complex holds
(z1 ") / (z2 ") = z2 / z1
proof end;

theorem :: COMPLFLD:33
for z1, z2 being Element of F_Complex st z2 <> 0. F_Complex holds
z1 / (z2 ") = z1 * z2
proof end;

theorem :: COMPLFLD:34
for z1, z2 being Element of F_Complex st z1 <> 0. F_Complex & z2 <> 0. F_Complex holds
(z1 ") / z2 = (z1 * z2) "
proof end;

theorem :: COMPLFLD:35
for z, z1, z2 being Element of F_Complex st z1 <> 0. F_Complex & z2 <> 0. F_Complex holds
(z1 ") * (z / z2) = z / (z1 * z2)
proof end;

theorem :: COMPLFLD:36
for z, z1, z2 being Element of F_Complex st z <> 0. F_Complex & z2 <> 0. F_Complex holds
( z1 / z2 = (z1 * z) / (z2 * z) & z1 / z2 = (z * z1) / (z * z2) )
proof end;

theorem :: COMPLFLD:37
for z1, z2, z3 being Element of F_Complex st z2 <> 0. F_Complex & z3 <> 0. F_Complex holds
z1 / (z2 * z3) = (z1 / z2) / z3
proof end;

theorem :: COMPLFLD:38
for z1, z2, z3 being Element of F_Complex st z2 <> 0. F_Complex & z3 <> 0. F_Complex holds
(z1 * z3) / z2 = z1 / (z2 / z3)
proof end;

theorem :: COMPLFLD:39
for z1, z2, z3, z4 being Element of F_Complex st z2 <> 0. F_Complex & z3 <> 0. F_Complex & z4 <> 0. F_Complex holds
(z1 / z2) / (z3 / z4) = (z1 * z4) / (z2 * z3)
proof end;

theorem :: COMPLFLD:40
for z1, z2, z3, z4 being Element of F_Complex st z2 <> 0. F_Complex & z4 <> 0. F_Complex holds
(z1 / z2) + (z3 / z4) = ((z1 * z4) + (z3 * z2)) / (z2 * z4)
proof end;

theorem :: COMPLFLD:41
for z, z1, z2 being Element of F_Complex st z <> 0. F_Complex holds
(z1 / z) + (z2 / z) = (z1 + z2) / z ;

theorem :: COMPLFLD:42
for z1, z2 being Element of F_Complex st z2 <> 0. F_Complex holds
( - (z1 / z2) = (- z1) / z2 & - (z1 / z2) = z1 / (- z2) )
proof end;

theorem :: COMPLFLD:43
for z1, z2 being Element of F_Complex st z2 <> 0. F_Complex holds
z1 / z2 = (- z1) / (- z2)
proof end;

theorem :: COMPLFLD:44
for z1, z2, z3, z4 being Element of F_Complex st z2 <> 0. F_Complex & z4 <> 0. F_Complex holds
(z1 / z2) - (z3 / z4) = ((z1 * z4) - (z3 * z2)) / (z2 * z4)
proof end;

theorem :: COMPLFLD:45
for z, z1, z2 being Element of F_Complex st z <> 0. F_Complex holds
(z1 / z) - (z2 / z) = (z1 - z2) / z
proof end;

theorem :: COMPLFLD:46
for z1, z2, z3 being Element of F_Complex st z2 <> 0. F_Complex & ( z1 * z2 = z3 or z2 * z1 = z3 ) holds
z1 = z3 / z2
proof end;

theorem :: COMPLFLD:47
(0. F_Complex) *' = 0. F_Complex
proof end;

theorem Th48: :: COMPLFLD:48
for z being Element of F_Complex st z *' = 0. F_Complex holds
z = 0. F_Complex
proof end;

theorem :: COMPLFLD:49
(1. F_Complex) *' = 1. F_Complex
proof end;

theorem :: COMPLFLD:50
for z being Element of F_Complex holds (z *') *' = z ;

theorem :: COMPLFLD:51
for z1, z2 being Element of F_Complex holds (z1 + z2) *' = (z1 *') + (z2 *') by COMPLEX1:32;

theorem :: COMPLFLD:52
for z being Element of F_Complex holds (- z) *' = - (z *')
proof end;

theorem :: COMPLFLD:53
for z1, z2 being Element of F_Complex holds (z1 - z2) *' = (z1 *') - (z2 *')
proof end;

theorem :: COMPLFLD:54
for z1, z2 being Element of F_Complex holds (z1 * z2) *' = (z1 *') * (z2 *') by COMPLEX1:35;

theorem :: COMPLFLD:55
for z being Element of F_Complex st z <> 0. F_Complex holds
(z ") *' = (z *') "
proof end;

theorem :: COMPLFLD:56
for z1, z2 being Element of F_Complex st z2 <> 0. F_Complex holds
(z1 / z2) *' = (z1 *') / (z2 *')
proof end;

theorem :: COMPLFLD:57
|.(0. F_Complex).| = 0 by Def1, COMPLEX1:44;

theorem :: COMPLFLD:58
for z being Element of F_Complex st |.z.| = 0 holds
z = 0. F_Complex by Th7;

theorem :: COMPLFLD:59
for z being Element of F_Complex holds
( z <> 0. F_Complex iff 0 < |.z.| ) by Th7, COMPLEX1:47;

theorem :: COMPLFLD:60
|.(1. F_Complex).| = 1 by Def1, COMPLEX1:48;

theorem :: COMPLFLD:61
for z being Element of F_Complex holds |.(- z).| = |.z.|
proof end;

theorem :: COMPLFLD:62
for z1, z2 being Element of F_Complex holds |.(z1 + z2).| <= |.z1.| + |.z2.| by COMPLEX1:56;

theorem :: COMPLFLD:63
for z1, z2 being Element of F_Complex holds |.(z1 - z2).| <= |.z1.| + |.z2.|
proof end;

theorem :: COMPLFLD:64
for z1, z2 being Element of F_Complex holds |.z1.| - |.z2.| <= |.(z1 + z2).| by COMPLEX1:58;

theorem :: COMPLFLD:65
for z1, z2 being Element of F_Complex holds |.z1.| - |.z2.| <= |.(z1 - z2).|
proof end;

theorem :: COMPLFLD:66
for z1, z2 being Element of F_Complex holds |.(z1 - z2).| = |.(z2 - z1).|
proof end;

theorem :: COMPLFLD:67
for z1, z2 being Element of F_Complex holds
( |.(z1 - z2).| = 0 iff z1 = z2 )
proof end;

theorem :: COMPLFLD:68
for z1, z2 being Element of F_Complex holds
( z1 <> z2 iff 0 < |.(z1 - z2).| )
proof end;

theorem :: COMPLFLD:69
for z, z1, z2 being Element of F_Complex holds |.(z1 - z2).| <= |.(z1 - z).| + |.(z - z2).|
proof end;

theorem :: COMPLFLD:70
for z1, z2 being Element of F_Complex holds |.(|.z1.| - |.z2.|).| <= |.(z1 - z2).|
proof end;

theorem :: COMPLFLD:71
for z1, z2 being Element of F_Complex holds |.(z1 * z2).| = |.z1.| * |.z2.| by COMPLEX1:65;

theorem :: COMPLFLD:72
for z being Element of F_Complex st z <> 0. F_Complex holds
|.(z ").| = |.z.| "
proof end;

theorem :: COMPLFLD:73
for z1, z2 being Element of F_Complex st z2 <> 0. F_Complex holds
|.z1.| / |.z2.| = |.(z1 / z2).|
proof end;

:: from COMPTRIG, 2006.08.12, A.T.
scheme :: COMPLFLD:sch 1
Regrwithout0{ P1[ Nat] } :
P1[1]
provided
A1: ex k being non zero Element of NAT st P1[k] and
A2: for k being non zero Element of NAT st k <> 1 & P1[k] holds
ex n being non zero Element of NAT st
( n < k & P1[n] )
proof end;

theorem Th74: :: COMPLFLD:74
for e being Element of F_Complex
for n being Nat holds (power F_Complex) . (e,n) = e |^ n
proof end;

definition
let x be Element of F_Complex;
let n be non zero Element of NAT ;
:: original: CRoot
redefine mode CRoot of n,x -> Element of F_Complex means :Def2: :: COMPLFLD:def 2
(power F_Complex) . (it,n) = x;
coherence
for b1 being CRoot of n,x holds b1 is Element of F_Complex
proof end;
compatibility
for b1 being Element of F_Complex holds
( b1 is CRoot of n,x iff (power F_Complex) . (b1,n) = x )
proof end;
end;

:: deftheorem Def2 defines CRoot COMPLFLD:def 2 :
for x being Element of F_Complex
for n being non zero Element of NAT
for b3 being Element of F_Complex holds
( b3 is CRoot of n,x iff (power F_Complex) . (b3,n) = x );

theorem :: COMPLFLD:75
for x being Element of F_Complex
for v being CRoot of 1,x holds v = x
proof end;

theorem :: COMPLFLD:76
for n being non zero Element of NAT
for v being CRoot of n, 0. F_Complex holds v = 0. F_Complex
proof end;

theorem :: COMPLFLD:77
for n being non zero Element of NAT
for x being Element of F_Complex
for v being CRoot of n,x st v = 0. F_Complex holds
x = 0. F_Complex
proof end;