:: 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 b₁ being Complex st b₁ is zero holds
b₁ is weightless ;

cluster complex heavy -> non light for object ;

coherence
for b₁ being Complex st b₁ is heavy holds
not b₁ is light ;

cluster complex non light -> non zero for object ;

coherence
for b₁ being Complex st not b₁ is light holds
not b₁ is zero ;

cluster complex heavy -> non weightless for object ;

coherence
for b₁ being Complex st b₁ is heavy holds
not b₁ is weightless ;

cluster non zero complex light -> non zero non weightless for object ;

coherence
for b₁ being non zero Complex st b₁ is light holds
not b₁ is weightless ;

cluster integer light -> zero for object ;

coherence
for b₁ being Integer st b₁ is light holds
b₁ is zero by NAT_1:14;

cluster trivial natural -> weightless for set ;

coherence
for b₁ being Nat st b₁ is trivial holds
b₁ is weightless ;

cluster natural non heavy -> trivial for set ;

coherence
for b₁ being Nat st not b₁ is heavy holds
b₁ is trivial ;

cluster natural non zero -> non light for set ;

coherence
for b₁ being Nat st not b₁ is zero holds
not b₁ is light ;

cluster non trivial natural -> heavy for set ;

coherence
for b₁ being Nat st not b₁ is trivial holds
b₁ is heavy ;

cluster complex weightless -> non heavy for object ;

coherence
for b₁ being Complex st b₁ is weightless holds
not b₁ is heavy ;

cluster complex light -> non heavy for object ;

coherence
for b₁ being Complex st b₁ is light holds
not b₁ is heavy ;

cluster non negative real non light -> positive non negative for object ;

coherence
for b₁ being non negative Real st not b₁ is light holds
b₁ is positive ;

end;

registration

cluster non zero complex ext-real positive non negative real heavy for object ;

existence
ex b₁ being positive Real st b₁ is heavy

proof end;

cluster non zero complex ext-real non positive negative real heavy for object ;

existence
ex b₁ being negative Real st b₁ is heavy

proof end;

cluster non zero complex ext-real positive non negative real light for object ;

existence
ex b₁ being positive Real st b₁ is light

proof end;

cluster non zero complex ext-real non positive negative real light for object ;

existence
ex b₁ being negative Real st b₁ is light

proof end;

cluster complex ext-real positive real integer non heavy weightless for object ;

existence
ex b₁ being weightless Integer st b₁ is positive

proof end;

cluster complex ext-real negative real integer non heavy weightless for object ;

existence
ex b₁ being weightless Integer st b₁ 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 b₁ being Nat st
( b₁ is trivial & not b₁ 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 b₁ being Nat st b₁ 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;