:: Multiplication-related Classes of Complex Numbers
:: by Rafal Ziobro
::
:: Received May 31, 2020
:: Copyright (c) 2020-2021 Association of Mizar Users


registration
let a be Complex;
reduce (a ") " to a;
reducibility
(a ") " = a
;
end;

definition
let a be Complex;
attr a is heavy means :Def1: :: COMPLEX3:def 1
|.a.| > 1;
attr a is light means :Def2: :: COMPLEX3:def 2
|.a.| < 1;
:: zero is included in weightless so as to adhere to trivial for Nats
attr a is weightless means :Def3: :: COMPLEX3:def 3
( |.a.| = 0 or |.a.| = 1 );
end;

:: deftheorem Def1 defines heavy COMPLEX3:def 1 :
for a being Complex holds
( a is heavy iff |.a.| > 1 );

:: deftheorem Def2 defines light COMPLEX3:def 2 :
for a being Complex holds
( a is light iff |.a.| < 1 );

:: deftheorem Def3 defines weightless COMPLEX3:def 3 :
for a being Complex holds
( a is weightless iff ( |.a.| = 0 or |.a.| = 1 ) );

::added theorems
theorem TA1: :: COMPLEX3:1
for a being Real holds
( ( a is heavy & a is negative implies a < - 1 ) & ( a < - 1 implies ( a is heavy & a is negative ) ) & ( a is light & a is negative implies ( - 1 < a & a < 0 ) ) & ( - 1 < a & a < 0 implies ( a is light & a is negative ) ) & ( a is light & a is positive implies ( 0 < a & a < 1 ) ) & ( 0 < a & a < 1 implies ( a is light & a is positive ) ) & ( a is heavy & a is positive implies a > 1 ) & ( a > 1 implies ( a is heavy & a is positive ) ) & ( a is weightless & a is positive implies a = 1 ) & ( a = 1 implies ( a is weightless & a is positive ) ) & ( a is weightless & a is negative implies a = - 1 ) & ( a = - 1 implies ( a is weightless & a is negative ) ) )
proof end;

theorem :: COMPLEX3:2
for a being Real holds
( ( not a is light & a is negative implies a <= - 1 ) & ( a <= - 1 implies ( not a is light & a is negative ) ) & ( not a is heavy & a is negative implies ( - 1 <= a & a < 0 ) ) & ( - 1 <= a & a < 0 implies ( not a is heavy & a is negative ) ) & ( not a is heavy & a is positive implies ( 0 < a & a <= 1 ) ) & ( 0 < a & a <= 1 implies ( not a is heavy & a is positive ) ) & ( not a is light & a is positive implies 1 <= a ) & ( 1 <= a implies ( not a is light & a is positive ) ) )
proof end;

:: could be another definition, in fact it was a starting point
theorem Th0: :: COMPLEX3:3
for a being Real holds
( a is weightless iff a = sgn a )
proof end;

registration
cluster zero complex -> weightless for object ;
coherence
for b1 being Complex st b1 is zero holds
b1 is weightless
;
cluster complex heavy -> non light for object ;
coherence
for b1 being Complex st b1 is heavy holds
not b1 is light
;
cluster complex non light -> non zero for object ;
coherence
for b1 being Complex st not b1 is light holds
not b1 is zero
;
cluster complex heavy -> non weightless for object ;
coherence
for b1 being Complex st b1 is heavy holds
not b1 is weightless
;
cluster non zero complex light -> non zero non weightless for object ;
coherence
for b1 being non zero Complex st b1 is light holds
not b1 is weightless
;
cluster integer light -> zero for object ;
coherence
for b1 being Integer st b1 is light holds
b1 is zero
by NAT_1:14;
cluster trivial natural -> weightless for set ;
coherence
for b1 being Nat st b1 is trivial holds
b1 is weightless
;
cluster natural non heavy -> trivial for set ;
coherence
for b1 being Nat st not b1 is heavy holds
b1 is trivial
;
cluster natural non zero -> non light for set ;
coherence
for b1 being Nat st not b1 is zero holds
not b1 is light
;
cluster non trivial natural -> heavy for set ;
coherence
for b1 being Nat st not b1 is trivial holds
b1 is heavy
;
cluster complex weightless -> non heavy for object ;
coherence
for b1 being Complex st b1 is weightless holds
not b1 is heavy
;
cluster complex light -> non heavy for object ;
coherence
for b1 being Complex st b1 is light holds
not b1 is heavy
;
cluster non negative real non light -> positive non negative for object ;
coherence
for b1 being non negative Real st not b1 is light holds
b1 is positive
;
end;

registration
cluster non zero complex ext-real positive non negative real heavy for object ;
existence
ex b1 being positive Real st b1 is heavy
proof end;
cluster non zero complex ext-real non positive negative real heavy for object ;
existence
ex b1 being negative Real st b1 is heavy
proof end;
cluster non zero complex ext-real positive non negative real light for object ;
existence
ex b1 being positive Real st b1 is light
proof end;
cluster non zero complex ext-real non positive negative real light for object ;
existence
ex b1 being negative Real st b1 is light
proof end;
cluster complex ext-real positive real integer non heavy weightless for object ;
existence
ex b1 being weightless Integer st b1 is positive
proof end;
cluster complex ext-real negative real integer non heavy weightless for object ;
existence
ex b1 being weightless Integer st b1 is negative
proof end;
end;

:: more on Complex numbers
theorem COMPLEX154a: :: COMPLEX3:4
for a being Complex holds Re a >= - |.a.|
proof end;

theorem COMPLEX155a: :: COMPLEX3:5
for a being Complex holds Im a >= - |.a.|
proof end;

theorem RI: :: COMPLEX3:6
for a being Complex holds |.(Re a).| + |.(Im a).| >= |.a.|
proof end;

:: registrations
:: using single variable
registration
let a be Complex;
cluster a * (a ") -> trivial ;
coherence
a * (a ") is trivial
proof end;
cluster a * (a *') -> real ;
coherence
a * (a *') is real
proof end;
cluster (a * (a *')) |^ 2 -> non negative ;
coherence
not (a * (a *')) |^ 2 is negative
proof end;
cluster a / |.a.| -> weightless ;
coherence
a / |.a.| is weightless
proof end;
end;

:: a/|.a.| shows a direction of a, so it may be useful to use it in a way similar to sgn
definition
let a be Complex;
func director a -> weightless Complex equals :: COMPLEX3:def 4
a / |.a.|;
coherence
a / |.a.| is weightless Complex
;
end;

:: deftheorem defines director COMPLEX3:def 4 :
for a being Complex holds director a = a / |.a.|;

theorem :: COMPLEX3:7
for a being Complex holds a = |.a.| * (director a)
proof end;

theorem DIR: :: COMPLEX3:8
for a being Complex holds director (- a) = - (director a)
proof end;

registration
let a be Real;
identify director a with sgn a;
correctness
compatibility
director a = sgn a
;
proof end;
end;

registration
let a be Real;
cluster director a -> integer weightless ;
coherence
director a is integer
;
end;

registration
let a be negative Real;
cluster director a -> negative weightless ;
coherence
director a is negative
;
end;

registration
let a be positive Real;
cluster director a -> positive weightless ;
coherence
director a is positive
;
end;

registration
reduce director 0 to 0 ;
reducibility
director 0 = 0
;
end;

registration
let a be non weightless Complex;
cluster |.a.| -> positive ;
coherence
|.a.| is positive
proof end;
cluster - a -> non weightless ;
coherence
not - a is weightless
proof end;
cluster a *' -> non weightless ;
coherence
not a *' is weightless
proof end;
cluster a " -> non weightless ;
coherence
not a " is weightless
proof end;
end;

registration
let a be weightless Complex;
cluster - a -> weightless ;
coherence
- a is weightless
proof end;
cluster a *' -> weightless ;
coherence
a *' is weightless
proof end;
cluster a " -> weightless ;
coherence
a " is weightless
proof end;
cluster a * (a *') -> weightless ;
coherence
a * (a *') is weightless
proof end;
cluster |.(Re a).| -> non heavy ;
coherence
not |.(Re a).| is heavy
proof end;
cluster |.(Im a).| -> non heavy ;
coherence
not |.(Im a).| is heavy
proof end;
cluster |.a.| - 1 -> weightless ;
coherence
|.a.| - 1 is weightless
proof end;
cluster 1 - |.a.| -> weightless ;
coherence
1 - |.a.| is weightless
proof end;
end;

registration
let a be weightless Real;
reduce sgn a to a;
reducibility
sgn a = a
by Th0;
end;

registration
let a be heavy Complex;
cluster - a -> heavy ;
coherence
- a is heavy
proof end;
cluster a *' -> heavy ;
coherence
a *' is heavy
proof end;
cluster a " -> light ;
coherence
a " is light
proof end;
cluster a * (a *') -> heavy ;
coherence
a * (a *') is heavy
proof end;
cluster |.(Re a).| + |.(Im a).| -> heavy ;
coherence
|.(Re a).| + |.(Im a).| is heavy
proof end;
cluster |.a.| - 1 -> positive ;
coherence
|.a.| - 1 is positive
proof end;
cluster 1 - |.a.| -> negative ;
coherence
1 - |.a.| is negative
proof end;
end;

registration
let a be non light Complex;
cluster - a -> non light ;
coherence
not - a is light
proof end;
cluster a *' -> non light ;
coherence
not a *' is light
proof end;
cluster a " -> non heavy ;
coherence
not a " is heavy
proof end;
cluster a * (a *') -> non light ;
coherence
not a * (a *') is light
proof end;
cluster |.(Re a).| + |.(Im a).| -> non light ;
coherence
not |.(Re a).| + |.(Im a).| is light
proof end;
cluster |.a.| - 1 -> non negative ;
coherence
not |.a.| - 1 is negative
proof end;
cluster 1 - |.a.| -> non positive ;
coherence
not 1 - |.a.| is positive
proof end;
end;

registration
let a be light Complex;
cluster - a -> light ;
coherence
- a is light
proof end;
cluster a *' -> light ;
coherence
a *' is light
proof end;
cluster a * (a *') -> light ;
coherence
a * (a *') is light
proof end;
cluster |.a.| - 1 -> negative ;
coherence
|.a.| - 1 is negative
proof end;
cluster 1 - |.a.| -> positive ;
coherence
1 - |.a.| is positive
proof end;
cluster Re a -> light ;
coherence
Re a is light
proof end;
cluster Im a -> light ;
coherence
Im a is light
proof end;
cluster (Re a) - 1 -> negative ;
coherence
(Re a) - 1 is negative
proof end;
cluster (Re a) - 2 -> heavy ;
coherence
(Re a) - 2 is heavy
proof end;
cluster (Im a) - 1 -> negative ;
coherence
(Im a) - 1 is negative
proof end;
cluster (Im a) - 2 -> heavy ;
coherence
(Im a) - 2 is heavy
proof end;
end;

registration
let a be non zero light Complex;
cluster a " -> heavy ;
coherence
a " is heavy
proof end;
end;

registration
let a be non heavy Complex;
cluster - a -> non heavy ;
coherence
not - a is heavy
proof end;
cluster a *' -> non heavy ;
coherence
not a *' is heavy
proof end;
cluster a * (a *') -> non heavy ;
coherence
not a * (a *') is heavy
proof end;
cluster |.a.| - 1 -> non positive ;
coherence
not |.a.| - 1 is positive
proof end;
cluster 1 - |.a.| -> non negative ;
coherence
not 1 - |.a.| is negative
proof end;
cluster Re a -> non heavy ;
coherence
not Re a is heavy
proof end;
cluster Im a -> non heavy ;
coherence
not Im a is heavy
proof end;
cluster (Re a) - 1 -> non positive ;
coherence
not (Re a) - 1 is positive
proof end;
cluster (Im a) - 1 -> non positive ;
coherence
not (Im a) - 1 is positive
proof end;
end;

registration
let a be non zero non heavy Complex;
cluster a " -> non light ;
coherence
not a " is light
proof end;
end;

:: we could now extend the definition of sgn for Complex
:: rsgn a = Re (a/|.a.|)
definition
let a be Complex;
func rsgn a -> non heavy Complex equals :: COMPLEX3:def 5
Re (director a);
coherence
Re (director a) is non heavy Complex
;
end;

:: deftheorem defines rsgn COMPLEX3:def 5 :
for a being Complex holds rsgn a = Re (director a);

:: and construct isgn a = Im (a/|.a.|)
definition
let a be Complex;
func isgn a -> non heavy Complex equals :: COMPLEX3:def 6
Im (director a);
coherence
Im (director a) is non heavy Complex
;
end;

:: deftheorem defines isgn COMPLEX3:def 6 :
for a being Complex holds isgn a = Im (director a);

registration
let a be Real;
identify rsgn a with sgn a;
correctness
compatibility
rsgn a = sgn a
;
proof end;
identify sgn a with rsgn a;
correctness
compatibility
sgn a = rsgn a
;
;
cluster isgn a -> zero non heavy ;
coherence
isgn a is zero
;
end;

registration
let a be Real;
cluster frac a -> light ;
coherence
frac a is light
proof end;
cluster |.a.| + a -> non negative ;
coherence
not |.a.| + a is negative
by ABSVALUE:26;
cluster |.a.| - a -> non negative ;
coherence
not |.a.| - a is negative
by ABSVALUE:27;
end;

:: added
registration
let a be positive heavy Real;
cluster a - 1 -> positive ;
coherence
a - 1 is positive
proof end;
cluster 1 - a -> negative ;
coherence
1 - a is negative
proof end;
end;

registration
let a be positive light Real;
cluster a - 1 -> negative ;
coherence
a - 1 is negative
proof end;
cluster 1 - a -> positive ;
coherence
1 - a is positive
proof end;
end;

::/added
theorem Th1: :: COMPLEX3:9
for a being non heavy Complex holds
( a is light or a is weightless )
proof end;

theorem :: COMPLEX3:10
for a being non light Complex holds
( a is heavy or a is weightless )
proof end;

theorem :: COMPLEX3:11
for a being positive heavy Real
for b being non heavy Real holds
( a > b & b > - a )
proof end;

theorem :: COMPLEX3:12
for a being positive non light Real
for b being light Real holds
( a > b & b > - a )
proof end;

:: multiplication
registration
let a be heavy Complex;
let b be non light Complex;
cluster a * b -> heavy ;
coherence
a * b is heavy
proof end;
end;

registration
let a, b be non light Complex;
cluster a * b -> non light ;
coherence
not a * b is light
proof end;
end;

registration
let a be light Complex;
let b be non heavy Complex;
cluster a * b -> light ;
coherence
a * b is light
proof end;
end;

registration
let a, b be non heavy Complex;
cluster a * b -> non heavy ;
coherence
not a * b is heavy
proof end;
end;

registration
let a, b be weightless Complex;
cluster a * b -> weightless ;
coherence
a * b is weightless
proof end;
end;

:: as above, we can extend frac to Complex using cfrac a = (a/|.a.|)*frac|.a.|
:: also we could use rsgn(a) instead and obtain Real;
:: neither way is exact, however, as it is limited to positive Reals only
:: (it could be done in more complicated way, but it looks ugly and doesn't make much sense)
definition
let a be Complex;
func cfrac a -> light Complex equals :: COMPLEX3:def 7
(director a) * (frac |.a.|);
coherence
(director a) * (frac |.a.|) is light Complex
;
end;

:: deftheorem defines cfrac COMPLEX3:def 7 :
for a being Complex holds cfrac a = (director a) * (frac |.a.|);

theorem :: COMPLEX3:13
for a being Complex holds cfrac (- a) = - (cfrac a)
proof end;

registration
let a be non negative Real;
identify frac a with cfrac a;
correctness
compatibility
frac a = cfrac a
;
proof end;
identify cfrac a with frac a;
correctness
compatibility
cfrac a = frac a
;
;
end;

:: power, root
theorem TAYLOR21: :: COMPLEX3:14
for a being Complex
for n being Nat holds |.a.| |^ n = |.(a |^ n).|
proof end;

registration
let a be weightless Complex;
let n be Nat;
cluster a |^ n -> weightless ;
coherence
a |^ n is weightless
proof end;
end;

registration
let a be weightless Real;
let n be Nat;
cluster (a |^ (2 * n)) - 1 -> weightless ;
coherence
(a |^ (2 * n)) - 1 is weightless
proof end;
end;

registration
let a be non light Complex;
let n be Nat;
cluster a |^ n -> non light ;
coherence
not a |^ n is light
proof end;
end;

registration
let a be non light Real;
let n be Nat;
cluster (a |^ (2 * n)) - 1 -> non negative ;
coherence
not (a |^ (2 * n)) - 1 is negative
proof end;
end;

registration
let a be light Complex;
let n be non zero Nat;
cluster a |^ n -> light ;
coherence
a |^ n is light
proof end;
cluster n -root a -> light ;
coherence
n -root a is light
proof end;
end;

registration
let a be light Real;
let n be non zero Nat;
cluster (a |^ (2 * n)) - 1 -> negative ;
coherence
(a |^ (2 * n)) - 1 is negative
proof end;
end;

registration
let a be non heavy Complex;
let n be Nat;
cluster a |^ n -> non heavy ;
coherence
not a |^ n is heavy
proof end;
end;

registration
let a be non heavy Real;
let n be Nat;
cluster (a |^ (2 * n)) - 1 -> non positive ;
coherence
not (a |^ (2 * n)) - 1 is positive
proof end;
end;

registration
let a be heavy Complex;
let n be non zero Nat;
cluster a |^ n -> heavy ;
coherence
a |^ n is heavy
proof end;
cluster n -root a -> heavy ;
coherence
n -root a is heavy
proof end;
end;

registration
let a be non weightless Complex;
let n be non zero Nat;
cluster a |^ n -> non weightless ;
coherence
not a |^ n is weightless
proof end;
end;

registration
let a be weightless Complex;
let n be non zero Nat;
cluster n -root a -> weightless ;
coherence
n -root a is weightless
proof end;
end;

registration
let a be non weightless Complex;
let n be non zero Nat;
cluster n -root a -> non weightless ;
coherence
not n -root a is weightless
proof end;
end;

registration
let a be non light Complex;
let n be non zero Nat;
cluster n -root a -> non light ;
coherence
not n -root a is light
proof end;
end;

registration
let a be non heavy Complex;
let n be non zero Nat;
cluster n -root a -> non heavy ;
coherence
not n -root a is heavy
proof end;
end;

:: division
registration
let a, b be weightless Complex;
cluster a / b -> weightless ;
coherence
a / b is weightless
;
end;

registration
let a be non heavy Complex;
let b be heavy Complex;
cluster a / b -> light ;
coherence
a / b is light
;
end;

registration
let a be light Complex;
let b be non light Complex;
cluster a / b -> light ;
coherence
a / b is light
;
end;

registration
let a be non light Complex;
let b be non zero light Complex;
cluster a / b -> heavy ;
coherence
a / b is heavy
;
end;

registration
let a be heavy Complex;
let b be non zero non heavy Complex;
cluster a / b -> heavy ;
coherence
a / b is heavy
;
end;

:: sum
registration
let a be positive heavy Real;
let b be non negative Real;
cluster a + b -> heavy ;
coherence
a + b is heavy
proof end;
end;

registration
let a be negative heavy Real;
let b be non positive Real;
cluster a + b -> heavy ;
coherence
a + b is heavy
proof end;
end;

registration
let a be positive non light Real;
let b be positive Real;
cluster a + b -> heavy ;
coherence
a + b is heavy
proof end;
end;

registration
let a be negative non light Real;
let b be negative Real;
cluster a + b -> heavy ;
coherence
a + b is heavy
proof end;
end;

registration
let a be non heavy Real;
let b be positive heavy Real;
cluster a + b -> positive ;
coherence
a + b is positive
proof end;
end;

registration
let a be light Real;
let b be positive non light Real;
cluster a + b -> positive ;
coherence
a + b is positive
proof end;
end;

registration
let a be non heavy Real;
let b be positive non light Real;
cluster a + b -> non negative ;
coherence
not a + b is negative
proof end;
end;

registration
let a be non heavy Real;
let b be negative heavy Real;
cluster a + b -> negative ;
coherence
a + b is negative
proof end;
end;

registration
let a be light Real;
let b be negative non light Real;
cluster a + b -> negative ;
coherence
a + b is negative
proof end;
end;

registration
let a be non heavy Real;
let b be negative non light Real;
cluster a + b -> non positive ;
coherence
not a + b is positive
proof end;
end;

registration
let a be positive light Real;
let c be negative light Real;
cluster a + c -> light ;
coherence
a + c is light
proof end;
end;

registration
let a be positive non heavy Real;
let c be negative non heavy Real;
cluster a + c -> non heavy ;
coherence
not a + c is heavy
proof end;
end;

:: min, max
registration
let a, b be Real;
cluster a - (min (a,b)) -> non negative ;
coherence
not a - (min (a,b)) is negative
proof end;
end;

:: choosing one element of two of the same type
registration
let a, b be weightless Real;
cluster min (a,b) -> weightless ;
coherence
min (a,b) is weightless
by XXREAL_0:def 9;
cluster max (a,b) -> weightless ;
coherence
max (a,b) is weightless
by XXREAL_0:def 10;
end;

registration
let a, b be light Real;
cluster min (a,b) -> light ;
coherence
min (a,b) is light
by XXREAL_0:def 9;
cluster max (a,b) -> light ;
coherence
max (a,b) is light
by XXREAL_0:def 10;
end;

registration
let a, b be heavy Real;
cluster min (a,b) -> heavy ;
coherence
min (a,b) is heavy
by XXREAL_0:def 9;
cluster max (a,b) -> heavy ;
coherence
max (a,b) is heavy
by XXREAL_0:def 10;
end;

registration
let a, b be positive Real;
cluster (min (a,b)) / (max (a,b)) -> non heavy ;
coherence
not (min (a,b)) / (max (a,b)) is heavy
proof end;
cluster (max (a,b)) / (min (a,b)) -> non light ;
coherence
not (max (a,b)) / (min (a,b)) is light
proof end;
cluster (a + b) / a -> heavy ;
coherence
(a + b) / a is heavy
proof end;
cluster a / (a + b) -> light ;
coherence
a / (a + b) is light
proof end;
end;

:: some theorems
theorem MP: :: COMPLEX3:15
for a, b being Real st a * b is positive holds
|.(a - b).| < |.(a + b).|
proof end;

theorem :: COMPLEX3:16
for a, b being Real st a * b is negative holds
|.(a - b).| > |.(a + b).|
proof end;

theorem :: COMPLEX3:17
for a, b being non zero Real holds |.((a |^ 2) - (b |^ 2)).| < |.((a |^ 2) + (b |^ 2)).|
proof end;

:: reformulation of theorems
theorem :: COMPLEX3:18
for a, b, c being positive Real st a < b holds
(b + c) / (a + c) is heavy by SERIES_5:3;

:: some examples of justification using theorems in XREAL_1
:: theorem ::XREAL_1:159
:: for a,b be non light positive Real holds a*b is non light positive;
:: theorem ::XREAL_1:160
:: for a be non heavy non negative Real, b be Real st ((not b is positive) or (not b is heavy)) holds ((a*b is non heavy) or (a*b is non positive));
:: theorem ::XREAL_1:161
:: for a be heavy positive Real, b be non light positive Real holds a*b is heavy positive;
:: theorem ::XREAL_1:162
:: for a be light positive Real, b be Real st ((not b is positive) or (not b is heavy)) holds ((a*b is non heavy) or (a*b is non positive));
:: theorem ::XREAL_1:163
:: for a,b be heavy non positive Real holds a*b is heavy positive;
::some examples of registrations, based on SERIES
theorem PP1: :: COMPLEX3:19
for a, b being positive Real holds ((a / b) + (b / a)) / 2 >= 1
proof end;

theorem NN1: :: COMPLEX3:20
for a, b being negative Real holds ((a / b) + (b / a)) / 2 >= 1
proof end;

theorem NP1: :: COMPLEX3:21
for a being negative Real
for b being positive Real holds ((a / b) + (b / a)) / 2 <= - 1
proof end;

registration
let a, b be non zero Real;
cluster ((a / b) + (b / a)) / 2 -> non light ;
coherence
not ((a / b) + (b / a)) / 2 is light
proof end;
cluster (a / b) + (b / a) -> heavy ;
coherence
(a / b) + (b / a) is heavy
proof end;
end;

:: We could use these registrations for some shortcuts
:: theorem for a,b be non zero Real, n be non zero Nat holds (a/b + b/a)|^(2*n) > 1 by TA1;
:: in fact, however:
theorem :: COMPLEX3:22
for a, b being non zero Real holds ((a / b) + (b / a)) |^ 2 >= 4
proof end;

registration
let a, b be positive Real;
cluster ((a + (2 * b)) * a) / ((a + b) |^ 2) -> non heavy ;
coherence
not ((a + (2 * b)) * a) / ((a + b) |^ 2) is heavy
proof end;
cluster ((b / a) + (a / b)) - 1 -> non light ;
coherence
not ((b / a) + (a / b)) - 1 is light
proof end;
cluster ((a + b) * ((a ") + (b "))) / 4 -> non light ;
coherence
not ((a + b) * ((a ") + (b "))) / 4 is light
proof end;
end;

::SERIESx5x13:
registration
let a, b be light Real;
cluster (a + b) / (1 + (a * b)) -> non heavy ;
coherence
not (a + b) / (1 + (a * b)) is heavy
proof end;
end;

registration
let a, b, c, d be positive Real;
cluster (((a / ((a + b) + d)) + (b / ((a + b) + c))) + (c / ((b + c) + d))) + (d / ((a + c) + d)) -> heavy ;
coherence
(((a / ((a + b) + d)) + (b / ((a + b) + c))) + (c / ((b + c) + d))) + (d / ((a + c) + d)) is heavy
by SERIES_5:15;
end;

:: ADDED 2020
registration
let a be non negative Real;
reduce |.(- a).| to a;
reducibility
|.(- a).| = a
proof end;
end;

registration
cluster trivial epsilon-transitive epsilon-connected ordinal natural non zero complex ext-real non negative real integer dim-like for set ;
existence
ex b1 being Nat st
( b1 is trivial & not b1 is zero )
proof end;
cluster trivial epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real integer dim-like for set ;
existence
ex b1 being Nat st b1 is trivial
proof end;
end;

registration
let a, b be non zero Real;
cluster min (a,b) -> non zero ;
coherence
not min (a,b) is zero
by XXREAL_0:def 9;
cluster max (a,b) -> non zero ;
coherence
not max (a,b) is zero
by XXREAL_0:def 10;
end;

registration
let a be non negative Real;
let b be Real;
cluster max (a,b) -> non negative ;
coherence
not max (a,b) is negative
by XXREAL_0:25;
end;

registration
let a be non positive Real;
let b be Real;
cluster min (a,b) -> non positive ;
coherence
not min (a,b) is positive
by XXREAL_0:17;
end;

registration
let a be positive Real;
let b be Real;
cluster max (a,b) -> positive ;
coherence
max (a,b) is positive
by XXREAL_0:25;
end;

registration
let a be negative Real;
let b be Real;
cluster min (a,b) -> negative ;
coherence
min (a,b) is negative
by XXREAL_0:17;
end;

registration
let a, b be non negative Real;
cluster min (a,b) -> non negative ;
coherence
not min (a,b) is negative
by XXREAL_0:def 9;
end;

registration
let a, b be non positive Real;
cluster max (a,b) -> non positive ;
coherence
not max (a,b) is positive
by XXREAL_0:def 10;
end;

registration
let a be positive Real;
let b be non negative Real;
cluster a / (a + b) -> non heavy ;
coherence
not a / (a + b) is heavy
proof end;
cluster (a + b) / a -> non light ;
coherence
not (a + b) / a is light
proof end;
end;

registration
let a, b be positive Real;
cluster a / (max (a,b)) -> non heavy ;
coherence
not a / (max (a,b)) is heavy
proof end;
cluster a / (min (a,b)) -> non light ;
coherence
not a / (min (a,b)) is light
proof end;
end;

theorem :: COMPLEX3:23
for a, b being Real st sgn a > sgn b holds
a > b
proof end;

theorem SGNZ: :: COMPLEX3:24
for a, b being non zero Real st sgn a > sgn b holds
( a is positive & b is negative )
proof end;

registration
let a, b be Real;
cluster (max (a,b)) - (min (a,b)) -> non negative ;
coherence
not (max (a,b)) - (min (a,b)) is negative
proof end;
reduce (sgn (a - b)) * ((max (a,b)) - (min (a,b))) to a - b;
reducibility
(sgn (a - b)) * ((max (a,b)) - (min (a,b))) = a - b
proof end;
end;

registration
let a be Real;
reduce a to_power 1 to a;
reducibility
a to_power 1 = a
;
reduce 1 to_power a to 1;
reducibility
1 to_power a = 1
by POWER:26;
cluster a to_power 0 -> natural ;
coherence
a to_power 0 is natural
by POWER:24;
cluster a to_power 0 -> weightless ;
coherence
a to_power 0 is weightless
by POWER:24;
end;

registration
let a be positive Real;
let b be Real;
cluster a to_power b -> positive ;
coherence
a to_power b is positive
by POWER:34;
end;

registration
let a be positive weightless Real;
let b be positive Real;
reduce b to_power a to b;
reducibility
b to_power a = b
proof end;
end;

registration
let a be positive heavy Real;
let b be positive Real;
cluster a to_power b -> heavy ;
coherence
a to_power b is heavy
by TA1, POWER:35;
end;

registration
let a be positive heavy Real;
let b be negative Real;
cluster a to_power b -> light ;
coherence
a to_power b is light
proof end;
end;

registration
let a be positive light Real;
let b be positive Real;
cluster a to_power b -> light ;
coherence
a to_power b is light
proof end;
end;

registration
let a be positive light Real;
let b be negative Real;
cluster a to_power b -> heavy ;
coherence
a to_power b is heavy
proof end;
end;

registration
let a be positive non weightless Real;
let b be Real;
reduce log (a,(a to_power b)) to b;
reducibility
log (a,(a to_power b)) = b
proof end;
end;

registration
let a be positive non weightless Real;
let b be positive Real;
reduce a to_power (log (a,b)) to b;
reducibility
a to_power (log (a,b)) = b
proof end;
end;

theorem ABD: :: COMPLEX3:25
for a, b being positive Real holds
( a > b iff 1 / a < 1 / b ) by XREAL_1:118, XREAL_1:76;

theorem ABN: :: COMPLEX3:26
for a, b being negative Real holds
( a > b iff 1 / a < 1 / b ) by XREAL_1:119, XREAL_1:99;

theorem :: COMPLEX3:27
for a, b being positive Real holds
( 1 / a > 1 / b iff - a > - b ) by ABD, XREAL_1:24;

theorem :: COMPLEX3:28
for a, b being negative Real holds
( 1 / a > 1 / b iff - a > - b ) by ABN, XREAL_1:24;

theorem OPR: :: COMPLEX3:29
for a, b being positive Real holds sgn ((1 / a) - (1 / b)) = sgn (b - a)
proof end;

theorem NPR: :: COMPLEX3:30
for a, b being negative Real holds sgn ((1 / a) - (1 / b)) = sgn (b - a)
proof end;

theorem :: COMPLEX3:31
for a, b being non zero Real holds
( sgn ((1 / a) - (1 / b)) = sgn (b - a) iff sgn b = sgn a )
proof end;

:: Sums and products
theorem SIO: :: COMPLEX3:32
for a, b being non zero Real holds
( a + b = a * b iff (1 / a) + (1 / b) = 1 )
proof end;

theorem SIL: :: COMPLEX3:33
for a, b being positive Real holds
( a + b > a * b iff (1 / a) + (1 / b) > 1 )
proof end;

theorem :: COMPLEX3:34
for a, b being positive Real holds
( a + b < a * b iff (1 / a) + (1 / b) < 1 )
proof end;

theorem :: COMPLEX3:35
for a being positive non heavy Real
for b being positive Real holds a + b > a * b
proof end;

theorem DIO: :: COMPLEX3:36
for a, b being non zero Real holds
( a - b = a * b iff (1 / b) - (1 / a) = 1 )
proof end;

theorem :: COMPLEX3:37
for a, b being positive Real st a - b = a * b holds
b is light
proof end;

:: Some relations for equal sums
theorem SAD: :: COMPLEX3:38
for a, b, c, d being positive Real st a + b = c + d holds
(max (a,b)) - (max (c,d)) = (min (c,d)) - (min (a,b))
proof end;

theorem :: COMPLEX3:39
for a, b, c, d being positive Real st a + b = c + d holds
( max (a,b) = max (c,d) iff min (a,b) = min (c,d) )
proof end;

theorem :: COMPLEX3:40
for a, b, c, d being positive Real st a + b = c + d holds
( max (a,b) > max (c,d) iff min (a,b) < min (c,d) )
proof end;

theorem ISM: :: COMPLEX3:41
for a, b, c, d being positive Real st a + b = c + d & a * b = c * d holds
max (a,b) = max (c,d)
proof end;

theorem ABCD: :: COMPLEX3:42
for a, b, c, d being positive Real
for n being Real st a + b = c + d & a * b = c * d holds
(a to_power n) + (b to_power n) = (c to_power n) + (d to_power n)
proof end;

theorem :: COMPLEX3:43
for a, b, c, d being positive Real
for n being Real st a + b = c + d & (a to_power n) + (b to_power n) <> (c to_power n) + (d to_power n) holds
a * b <> c * d by ABCD;

theorem :: COMPLEX3:44
for a, b, c, d being positive Real st a + b = c + d holds
( (1 / a) + (1 / b) = (1 / c) + (1 / d) iff a * b = c * d )
proof end;

theorem :: COMPLEX3:45
for a, b, c, d being positive Real st a + b = c + d holds
( (1 / a) + (1 / b) > (1 / c) + (1 / d) iff a * b < c * d )
proof end;

theorem SRL: :: COMPLEX3:46
for a, b, c, d being positive Real st a + b >= c + d & a * b < c * d holds
(1 / a) + (1 / b) > (1 / c) + (1 / d)
proof end;

theorem :: COMPLEX3:47
for a, b, c, d being positive Real st a * b < c * d & (1 / a) + (1 / b) <= (1 / c) + (1 / d) holds
a + b < c + d by SRL;

theorem SRI: :: COMPLEX3:48
for a, b, c, d being positive Real st a + b <= c + d & (1 / a) + (1 / b) > (1 / c) + (1 / d) holds
a * b < c * d
proof end;

theorem :: COMPLEX3:49
for a, b, c, d being positive Real holds
( not a * b >= c * d or a + b > c + d or (1 / a) + (1 / b) <= (1 / c) + (1 / d) ) by SRI;

theorem N158: :: COMPLEX3:50
for a, b being positive Real
for n, m being Real holds
( (a to_power (m + n)) + (b to_power (m + n)) = ((((a to_power m) + (b to_power m)) * ((a to_power n) + (b to_power n))) + (((a to_power n) - (b to_power n)) * ((a to_power m) - (b to_power m)))) / 2 & (a to_power (m + n)) - (b to_power (m + n)) = ((((a to_power m) + (b to_power m)) * ((a to_power n) - (b to_power n))) + (((a to_power n) + (b to_power n)) * ((a to_power m) - (b to_power m)))) / 2 )
proof end;

theorem :: COMPLEX3:51
for a, b being positive Real
for n being Real holds (a to_power (n + 1)) + (b to_power (n + 1)) = ((((a to_power n) + (b to_power n)) * (a + b)) + ((a - b) * ((a to_power n) - (b to_power n)))) / 2
proof end;

theorem :: COMPLEX3:52
for a, b, n, m being positive Real holds (a to_power (n + m)) + (b to_power (n + m)) >= (((a to_power n) + (b to_power n)) * ((a to_power m) + (b to_power m))) / 2
proof end;

theorem :: COMPLEX3:53
for a, b, n, m being positive Real holds
( (a to_power (n + m)) + (b to_power (n + m)) = (((a to_power n) + (b to_power n)) * ((a to_power m) + (b to_power m))) / 2 iff a = b )
proof end;

theorem SMI: :: COMPLEX3:54
for a, b, c, d being positive Real st a + b <= c + d & max (a,b) > max (c,d) holds
a * b < c * d
proof end;

theorem :: COMPLEX3:55
for a, b, c, d being positive Real st a + b <= c + d & a * b > c * d holds
( max (a,b) < max (c,d) & min (a,b) > min (c,d) )
proof end;

theorem :: COMPLEX3:56
for a, b, c, d being positive Real holds
( max (a,b) = max (c,d) & min (a,b) = min (c,d) iff ( a * b = c * d & a + b = c + d ) )
proof end;

theorem POWER37: :: COMPLEX3:57
for a, b being non negative Real
for c being positive Real holds
( a >= b iff a to_power c >= b to_power c )
proof end;

theorem :: COMPLEX3:58
for a, b, n being non negative Real holds
( max ((a to_power n),(b to_power n)) = (max (a,b)) to_power n & min ((a to_power n),(b to_power n)) = (min (a,b)) to_power n )
proof end;

theorem :: COMPLEX3:59
for a, b, c, d being positive Real st ( ( a * b > c * d & a / b >= c / d ) or ( a * b >= c * d & a / b > c / d ) ) holds
a > c
proof end;

theorem :: COMPLEX3:60
for a being positive Real holds 1 - a < 1 / (1 + a)
proof end;

theorem :: COMPLEX3:61
for a being positive light Real holds 1 + a < 1 / (1 - a)
proof end;

theorem Pow: :: COMPLEX3:62
for a, b being positive Real
for m being non negative Real
for n being positive Real st (a to_power m) + (b to_power m) <= 1 holds
(a to_power (m + n)) + (b to_power (m + n)) < 1
proof end;

theorem :: COMPLEX3:63
for a, b being positive Real
for m being non positive Real
for n being negative Real st (a to_power m) + (b to_power m) <= 1 holds
(a to_power (m + n)) + (b to_power (m + n)) < 1
proof end;

theorem NEW: :: COMPLEX3:64
for a, b, c, n being positive Real
for m being non negative Real st (a to_power m) + (b to_power m) <= c to_power m holds
(a to_power (m + n)) + (b to_power (m + n)) < c to_power (m + n)
proof end;

theorem APB: :: COMPLEX3:65
for a, b being positive Real
for n being positive heavy Real holds (a to_power n) + (b to_power n) < (a + b) to_power n
proof end;

registration
let k be positive Real;
let n be positive heavy Real;
cluster ((k + 1) to_power n) - (k to_power n) -> positive heavy ;
coherence
( ((k + 1) to_power n) - (k to_power n) is heavy & ((k + 1) to_power n) - (k to_power n) is positive )
proof end;
end;

registration
let k be positive heavy Real;
let n be non negative Real;
cluster (k to_power (n + 1)) - (k to_power n) -> positive ;
coherence
(k to_power (n + 1)) - (k to_power n) is positive
proof end;
end;

theorem :: COMPLEX3:66
for k being positive Real
for n being positive heavy Real holds (k + 1) to_power n > (k to_power n) + 1
proof end;

theorem BPA: :: COMPLEX3:67
for a, b being positive Real
for n being positive light Real holds (a to_power n) + (b to_power n) > (a + b) to_power n
proof end;

theorem :: COMPLEX3:68
for k being positive Real
for n being positive light Real holds (k + 1) to_power n < (k to_power n) + 1
proof end;

theorem LMN: :: COMPLEX3:69
for k being positive Real
for n being non positive Real holds (k + 1) to_power n < (k to_power n) + 1
proof end;

theorem BPC: :: COMPLEX3:70
for a, b being positive Real
for n being non positive Real holds (a to_power n) + (b to_power n) > (a + b) to_power n
proof end;

theorem LME: :: COMPLEX3:71
for a, b being positive Real
for n being Real holds
( (a + b) to_power n > (a to_power n) + (b to_power n) iff ( n is heavy & n is positive ) )
proof end;

theorem NE1: :: COMPLEX3:72
for a, b being positive Real
for n being Real holds
( (a + b) to_power n = (a to_power n) + (b to_power n) iff n = 1 )
proof end;

theorem :: COMPLEX3:73
for a, b being positive Real
for n being Real holds
( (a + b) to_power n < (a to_power n) + (b to_power n) iff n < 1 )
proof end;

theorem FPC: :: COMPLEX3:74
for a, b, c being positive Real holds (a + b) * (a + c) > a * ((a + b) + c)
proof end;

theorem FRAC: :: COMPLEX3:75
for a, b, c being positive Real holds ((a + b) + c) / (a + b) < (a + c) / a
proof end;

theorem :: COMPLEX3:76
for a, b, c, n being positive Real holds (((a + b) + c) to_power n) / ((a + b) to_power n) < ((a + c) to_power n) / (a to_power n)
proof end;

theorem ADB: :: COMPLEX3:77
for a, b being positive heavy Real holds
( (a + b) - 1 > a / b & a / b > 1 / ((a + b) - 1) )
proof end;

theorem :: COMPLEX3:78
for a, b, c being positive Real holds
( ((a + b) + c) / a > (a + b) / (a + c) & (a + b) / (a + c) > a / ((a + b) + c) )
proof end;

theorem IL1: :: COMPLEX3:79
for a being positive light Real
for n being positive heavy Real holds ((1 + a) to_power n) * ((1 - a) to_power n) < (1 + (a to_power n)) * (1 - (a to_power n))
proof end;

theorem :: COMPLEX3:80
for a being positive light Real
for n being positive heavy Real holds ((1 + a) to_power n) / (1 + (a to_power n)) < (1 - (a to_power n)) / ((1 - a) to_power n)
proof end;

theorem :: COMPLEX3:81
for a being positive light Real holds
( max (a,(1 - a)) >= 1 / 2 & min (a,(1 - a)) <= 1 / 2 )
proof end;

theorem :: COMPLEX3:82
for a being positive light Real holds (1 / (1 + a)) + (1 / (1 - a)) > 2
proof end;

theorem :: COMPLEX3:83
for a being positive heavy Real holds (1 / (a + 1)) + (1 / (a - 1)) > 2 / a
proof end;

theorem :: COMPLEX3:84
for a, b being positive Real
for n being positive heavy Real holds (((2 * a) + b) to_power n) + (b to_power n) < (2 * (a + b)) to_power n
proof end;

theorem :: COMPLEX3:85
for a, n being positive heavy Real holds ((a + 1) to_power n) - ((a - 1) to_power n) > 2 to_power n
proof end;

theorem :: COMPLEX3:86
for a being positive light Real
for n being positive heavy Real holds
( 2 to_power n > ((1 + a) to_power n) - ((1 - a) to_power n) & ((1 + a) to_power n) - ((1 - a) to_power n) > (2 * a) to_power n )
proof end;

theorem :: COMPLEX3:87
for a, n being positive heavy Real
for b being positive light Real holds
( ((a + 1) to_power n) - ((a - 1) to_power n) > ((a + b) to_power n) - ((a - b) to_power n) & ((a + b) to_power n) - ((a - b) to_power n) > (2 * b) to_power n )
proof end;

theorem :: COMPLEX3:88
for a, b, n being positive Real holds
( 2 * ((a + b) to_power n) > ((a + b) to_power n) + (a to_power n) & ((a + b) to_power n) + (a to_power n) > 2 * (a to_power n) )
proof end;

theorem ATB: :: COMPLEX3:89
for a, b being positive Real st a <> b holds
ex n, m being Real st
( a = (a / b) to_power n & b = (a / b) to_power m )
proof end;

theorem :: COMPLEX3:90
for a, b being positive Real st a <> b holds
ex n, m being Real st a - b = ((a / b) to_power n) * (((a / b) to_power m) - 1)
proof end;

theorem :: COMPLEX3:91
for a, m, n being positive Real holds (a to_power n) + (a to_power m) = (a to_power (min (n,m))) * (1 + (a to_power |.(m - n).|))
proof end;

:: Logarithms
theorem ABA: :: COMPLEX3:92
for a, b being positive non weightless Real holds log (a,b) = 1 / (log (b,a))
proof end;

registration
let a be positive heavy Real;
let b be positive Real;
cluster log (a,(a + b)) -> heavy ;
coherence
log (a,(a + b)) is heavy
proof end;
cluster log ((a + b),a) -> light ;
coherence
log ((a + b),a) is light
proof end;
end;

theorem :: COMPLEX3:93
for a being positive non weightless Real
for b being positive Real holds
( log (a,b) = 0 iff b = 1 )
proof end;

theorem AZ1: :: COMPLEX3:94
for a being positive non weightless Real
for b being positive Real holds
( log (a,b) = 1 iff a = b )
proof end;

theorem :: COMPLEX3:95
for a, b being positive Real
for n being non zero Real holds
( a to_power n = b to_power n iff a = b )
proof end;

theorem ABO: :: COMPLEX3:96
for a being positive non weightless Real
for b being positive Real holds
( log (a,b) = - (log ((1 / a),b)) & log ((1 / a),b) = log (a,(1 / b)) & log (a,b) = - (log (a,(1 / b))) & log (a,b) = log ((1 / a),(1 / b)) )
proof end;

theorem AG1: :: COMPLEX3:97
for a being positive heavy Real
for b being positive Real holds
( a > b iff log (a,b) < 1 )
proof end;

theorem AM1: :: COMPLEX3:98
for a being positive light Real
for b being positive Real holds
( a < b iff log (a,b) < 1 )
proof end;

theorem AG2: :: COMPLEX3:99
for a being positive heavy Real
for b being positive Real holds
( a < b iff log (a,b) > 1 )
proof end;

theorem AM2: :: COMPLEX3:100
for a being positive light Real
for b being positive Real holds
( a > b iff log (a,b) > 1 )
proof end;

theorem :: COMPLEX3:101
for a, b being positive non weightless Real st log (a,b) >= 1 holds
( 0 < log (b,a) & log (b,a) <= 1 )
proof end;

theorem :: COMPLEX3:102
for a, b being positive non weightless Real st log (a,b) <= - 1 holds
( 0 > log (b,a) & log (b,a) >= - 1 )
proof end;

theorem :: COMPLEX3:103
for a, b being positive heavy Real st log (a,b) > log (b,a) & log (b,a) >= 1 holds
a > b
proof end;

theorem :: COMPLEX3:104
for a, b being positive heavy Real st log (b,a) < 1 holds
a < b
proof end;

theorem ACG: :: COMPLEX3:105
for a, c being positive heavy Real
for b, d being positive Real st log (a,b) <= log (c,d) & a < b holds
c < d
proof end;

theorem ACL: :: COMPLEX3:106
for a, c being positive heavy Real
for b, d being positive Real st log (a,b) >= log (c,d) & a > b holds
c > d
proof end;

theorem :: COMPLEX3:107
for a being positive heavy Real
for c being positive light Real
for b, d being positive Real st log (a,b) <= log (c,d) & a < b holds
c > d
proof end;

theorem :: COMPLEX3:108
for a being positive heavy Real
for c being positive light Real
for b, d being positive Real st log (a,b) >= log (c,d) & a > b holds
c < d
proof end;

theorem :: COMPLEX3:109
for a, c being positive light Real
for b, d being positive Real st log (a,b) <= log (c,d) & a > b holds
c > d
proof end;

theorem :: COMPLEX3:110
for a, c being positive light Real
for b, d being positive Real st log (a,b) >= log (c,d) & a < b holds
c < d
proof end;

theorem :: COMPLEX3:111
for a being positive light Real
for c being positive heavy Real
for b, d being positive Real st log (a,b) <= log (c,d) & a > b holds
c < d
proof end;

theorem :: COMPLEX3:112
for a being positive light Real
for c being positive heavy Real
for b, d being positive Real st log (a,b) >= log (c,d) & a < b holds
c > d
proof end;

theorem :: COMPLEX3:113
for a, c being positive heavy Real
for b, d being positive Real st log (a,b) < log (c,d) & a <= b holds
c < d
proof end;

theorem :: COMPLEX3:114
for a, c being positive heavy Real
for b, d being positive Real st log (a,b) <= log (c,d) & a <= b holds
c <= d
proof end;

theorem :: COMPLEX3:115
for a, b being positive Real st a > b holds
log ((a / b),a) > log ((a / b),b)
proof end;