:: by Rafal Ziobro

::

:: Received May 31, 2020

:: Copyright (c) 2020-2021 Association of Mizar Users

definition
end;

:: deftheorem Def1 defines heavy COMPLEX3:def 1 :

for a being Complex holds

( a is heavy iff |.a.| > 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 );

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 ) );

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 ) ) )

( ( 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 ) ) )

( ( 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

registration

coherence

for b_{1} being Complex st b_{1} is zero holds

b_{1} is weightless
;

coherence

for b_{1} being Complex st b_{1} is heavy holds

not b_{1} is light
;

coherence

for b_{1} being Complex st not b_{1} is light holds

not b_{1} is zero
;

coherence

for b_{1} being Complex st b_{1} is heavy holds

not b_{1} is weightless
;

coherence

for b_{1} being non zero Complex st b_{1} is light holds

not b_{1} is weightless
;

coherence

for b_{1} being Integer st b_{1} is light holds

b_{1} is zero
by NAT_1:14;

coherence

for b_{1} being Nat st b_{1} is trivial holds

b_{1} is weightless
;

coherence

for b_{1} being Nat st not b_{1} is heavy holds

b_{1} is trivial
;

coherence

for b_{1} being Nat st not b_{1} is zero holds

not b_{1} is light
;

coherence

for b_{1} being Nat st not b_{1} is trivial holds

b_{1} is heavy
;

coherence

for b_{1} being Complex st b_{1} is weightless holds

not b_{1} is heavy
;

coherence

for b_{1} being Complex st b_{1} is light holds

not b_{1} is heavy
;

coherence

for b_{1} being non negative Real st not b_{1} is light holds

b_{1} is positive
;

end;
for b

b

coherence

for b

not b

coherence

for b

not b

coherence

for b

not b

coherence

for b

not b

coherence

for b

b

coherence

for b

b

coherence

for b

b

coherence

for b

not b

coherence

for b

b

coherence

for b

not b

coherence

for b

not b

coherence

for b

b

registration

existence

ex b_{1} being positive Real st b_{1} is heavy

ex b_{1} being negative Real st b_{1} is heavy

ex b_{1} being positive Real st b_{1} is light

ex b_{1} being negative Real st b_{1} is light

ex b_{1} being weightless Integer st b_{1} is positive

ex b_{1} being weightless Integer st b_{1} is negative

end;
ex b

proof end;

existence ex b

proof end;

existence ex b

proof end;

existence ex b

proof end;

existence ex b

proof end;

existence ex b

proof end;

:: more on Complex numbers

:: registrations

:: using single variable

:: using single variable

registration

let a be Complex;

coherence

a * (a ") is trivial

a * (a *') is real

not (a * (a *')) |^ 2 is negative

a / |.a.| is weightless

end;
coherence

a * (a ") is trivial

proof end;

coherence a * (a *') is real

proof end;

coherence not (a * (a *')) |^ 2 is negative

proof end;

coherence a / |.a.| is weightless

proof end;

:: a/|.a.| shows a direction of a, so it may be useful to use it in a way similar to sgn

registration
end;

registration

let a be non weightless Complex;

coherence

|.a.| is positive

not - a is weightless

not a *' is weightless

not a " is weightless

end;
coherence

|.a.| is positive

proof end;

coherence not - a is weightless

proof end;

coherence not a *' is weightless

proof end;

coherence not a " is weightless

proof end;

registration

let a be weightless Complex;

coherence

- a is weightless

a *' is weightless

a " is weightless

a * (a *') is weightless

not |.(Re a).| is heavy

not |.(Im a).| is heavy

|.a.| - 1 is weightless

1 - |.a.| is weightless

end;
coherence

- a is weightless

proof end;

coherence a *' is weightless

proof end;

coherence a " is weightless

proof end;

coherence a * (a *') is weightless

proof end;

coherence not |.(Re a).| is heavy

proof end;

coherence not |.(Im a).| is heavy

proof end;

coherence |.a.| - 1 is weightless

proof end;

coherence 1 - |.a.| is weightless

proof end;

registration

let a be heavy Complex;

coherence

- a is heavy

a *' is heavy

a " is light

a * (a *') is heavy

|.(Re a).| + |.(Im a).| is heavy

|.a.| - 1 is positive

1 - |.a.| is negative

end;
coherence

- a is heavy

proof end;

coherence a *' is heavy

proof end;

coherence a " is light

proof end;

coherence a * (a *') is heavy

proof end;

coherence |.(Re a).| + |.(Im a).| is heavy

proof end;

coherence |.a.| - 1 is positive

proof end;

coherence 1 - |.a.| is negative

proof end;

registration

let a be non light Complex;

coherence

not - a is light

not a *' is light

not a " is heavy

not a * (a *') is light

not |.(Re a).| + |.(Im a).| is light

not |.a.| - 1 is negative

not 1 - |.a.| is positive

end;
coherence

not - a is light

proof end;

coherence not a *' is light

proof end;

coherence not a " is heavy

proof end;

coherence not a * (a *') is light

proof end;

coherence not |.(Re a).| + |.(Im a).| is light

proof end;

coherence not |.a.| - 1 is negative

proof end;

coherence not 1 - |.a.| is positive

proof end;

registration

let a be light Complex;

coherence

- a is light

a *' is light

a * (a *') is light

|.a.| - 1 is negative

1 - |.a.| is positive

Re a is light

Im a is light

(Re a) - 1 is negative

(Re a) - 2 is heavy

(Im a) - 1 is negative

(Im a) - 2 is heavy

end;
coherence

- a is light

proof end;

coherence a *' is light

proof end;

coherence a * (a *') is light

proof end;

coherence |.a.| - 1 is negative

proof end;

coherence 1 - |.a.| is positive

proof end;

coherence Re a is light

proof end;

coherence Im a is light

proof end;

coherence (Re a) - 1 is negative

proof end;

coherence (Re a) - 2 is heavy

proof end;

coherence (Im a) - 1 is negative

proof end;

coherence (Im a) - 2 is heavy

proof end;

registration
end;

registration

let a be non heavy Complex;

coherence

not - a is heavy

not a *' is heavy

not a * (a *') is heavy

not |.a.| - 1 is positive

not 1 - |.a.| is negative

not Re a is heavy

not Im a is heavy

not (Re a) - 1 is positive

not (Im a) - 1 is positive

end;
coherence

not - a is heavy

proof end;

coherence not a *' is heavy

proof end;

coherence not a * (a *') is heavy

proof end;

coherence not |.a.| - 1 is positive

proof end;

coherence not 1 - |.a.| is negative

proof end;

coherence not Re a is heavy

proof end;

coherence not Im a is heavy

proof end;

coherence not (Re a) - 1 is positive

proof end;

coherence not (Im a) - 1 is positive

proof end;

:: we could now extend the definition of sgn for Complex

:: rsgn a = Re (a/|.a.|)

:: rsgn a = Re (a/|.a.|)

:: and construct isgn a = Im (a/|.a.|)

registration

let a be Real;

correctness

compatibility

rsgn a = sgn a;

compatibility

sgn a = rsgn a;

;

coherence

isgn a is zero ;

end;
correctness

compatibility

rsgn a = sgn a;

proof end;

correctness compatibility

sgn a = rsgn a;

;

coherence

isgn a is zero ;

registration

let a be Real;

coherence

frac a is light

not |.a.| + a is negative by ABSVALUE:26;

coherence

not |.a.| - a is negative by ABSVALUE:27;

end;
coherence

frac a is light

proof end;

coherence not |.a.| + a is negative by ABSVALUE:26;

coherence

not |.a.| - a is negative by ABSVALUE:27;

:: added

registration

let a be positive heavy Real;

coherence

a - 1 is positive

1 - a is negative

end;
coherence

a - 1 is positive

proof end;

coherence 1 - a is negative

proof end;

registration

let a be positive light Real;

coherence

a - 1 is negative

1 - a is positive

end;
coherence

a - 1 is negative

proof end;

coherence 1 - a is positive

proof end;

::/added

:: multiplication

registration
end;

registration
end;

registration
end;

registration
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)

:: 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)

:: deftheorem defines cfrac COMPLEX3:def 7 :

for a being Complex holds cfrac a = (director a) * (frac |.a.|);

for a being Complex holds cfrac a = (director a) * (frac |.a.|);

registration

let a be non negative Real;

correctness

compatibility

frac a = cfrac a;

compatibility

cfrac a = frac a;

;

end;
correctness

compatibility

frac a = cfrac a;

proof end;

correctness compatibility

cfrac a = frac a;

;

:: power, root

registration
end;

registration
end;

registration
end;

registration

let a be light Complex;

let n be non zero Nat;

coherence

a |^ n is light

n -root a is light

end;
let n be non zero Nat;

coherence

a |^ n is light

proof end;

coherence n -root a is light

proof end;

registration
end;

registration
end;

registration

let a be heavy Complex;

let n be non zero Nat;

coherence

a |^ n is heavy

n -root a is heavy

end;
let n be non zero Nat;

coherence

a |^ n is heavy

proof end;

coherence n -root a is heavy

proof end;

registration

let a be non weightless Complex;

let n be non zero Nat;

coherence

not a |^ n is weightless

end;
let n be non zero Nat;

coherence

not a |^ n is weightless

proof end;

registration
end;

registration

let a be non weightless Complex;

let n be non zero Nat;

coherence

not n -root a is weightless

end;
let n be non zero Nat;

coherence

not n -root a is weightless

proof end;

registration
end;

registration
end;

:: division

registration
end;

registration
end;

registration
end;

:: sum

registration
end;

registration
end;

registration
end;

registration
end;

registration
end;

registration
end;

registration

let a be non heavy Real;

let b be positive non light Real;

coherence

not a + b is negative

end;
let b be positive non light Real;

coherence

not a + b is negative

proof end;

registration
end;

registration
end;

registration

let a be non heavy Real;

let b be negative non light Real;

coherence

not a + b is positive

end;
let b be negative non light Real;

coherence

not a + b is positive

proof end;

registration
end;

registration

let a be positive non heavy Real;

let c be negative non heavy Real;

coherence

not a + c is heavy

end;
let c be negative non heavy Real;

coherence

not a + c is heavy

proof end;

:: min, max

:: choosing one element of two of the same type

registration

let a, b be weightless Real;

coherence

min (a,b) is weightless by XXREAL_0:def 9;

coherence

max (a,b) is weightless by XXREAL_0:def 10;

end;
coherence

min (a,b) is weightless by XXREAL_0:def 9;

coherence

max (a,b) is weightless by XXREAL_0:def 10;

registration

let a, b be light Real;

coherence

min (a,b) is light by XXREAL_0:def 9;

coherence

max (a,b) is light by XXREAL_0:def 10;

end;
coherence

min (a,b) is light by XXREAL_0:def 9;

coherence

max (a,b) is light by XXREAL_0:def 10;

registration

let a, b be heavy Real;

coherence

min (a,b) is heavy by XXREAL_0:def 9;

coherence

max (a,b) is heavy by XXREAL_0:def 10;

end;
coherence

min (a,b) is heavy by XXREAL_0:def 9;

coherence

max (a,b) is heavy by XXREAL_0:def 10;

registration

let a, b be positive Real;

coherence

not (min (a,b)) / (max (a,b)) is heavy

not (max (a,b)) / (min (a,b)) is light

(a + b) / a is heavy

a / (a + b) is light

end;
coherence

not (min (a,b)) / (max (a,b)) is heavy

proof end;

coherence not (max (a,b)) / (min (a,b)) is light

proof end;

coherence (a + b) / a is heavy

proof end;

coherence a / (a + b) is light

proof end;

:: some theorems

:: reformulation of theorems

theorem :: COMPLEX3:18

:: 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 ::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

registration

let a, b be non zero Real;

coherence

not ((a / b) + (b / a)) / 2 is light

(a / b) + (b / a) is heavy

end;
coherence

not ((a / b) + (b / a)) / 2 is light

proof end;

coherence (a / b) + (b / a) is heavy

proof 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 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:

registration

let a, b be positive Real;

coherence

not ((a + (2 * b)) * a) / ((a + b) |^ 2) is heavy

not ((b / a) + (a / b)) - 1 is light

not ((a + b) * ((a ") + (b "))) / 4 is light

end;
coherence

not ((a + (2 * b)) * a) / ((a + b) |^ 2) is heavy

proof end;

coherence not ((b / a) + (a / b)) - 1 is light

proof end;

coherence not ((a + b) * ((a ") + (b "))) / 4 is light

proof end;

::SERIESx5x13:

registration

let a, b, c, d be positive Real;

(((a / ((a + b) + d)) + (b / ((a + b) + c))) + (c / ((b + c) + d))) + (d / ((a + c) + d)) is heavy by SERIES_5:15;

end;
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;

:: ADDED 2020

registration
end;

registration

ex b_{1} being Nat st

( b_{1} is trivial & not b_{1} is zero )

ex b_{1} being Nat st b_{1} is trivial
end;

cluster trivial epsilon-transitive epsilon-connected ordinal natural non zero complex ext-real non negative real integer dim-like for set ;

existence ex b

( b

proof end;

cluster trivial epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real integer dim-like for set ;

existence ex b

proof end;

registration

let a, b be non zero Real;

coherence

not min (a,b) is zero by XXREAL_0:def 9;

coherence

not max (a,b) is zero by XXREAL_0:def 10;

end;
coherence

not min (a,b) is zero by XXREAL_0:def 9;

coherence

not max (a,b) is zero by XXREAL_0:def 10;

registration
end;

registration
end;

registration
end;

registration
end;

registration
end;

registration
end;

registration

let a be positive Real;

let b be non negative Real;

coherence

not a / (a + b) is heavy

not (a + b) / a is light

end;
let b be non negative Real;

coherence

not a / (a + b) is heavy

proof end;

coherence not (a + b) / a is light

proof end;

registration

let a, b be positive Real;

coherence

not a / (max (a,b)) is heavy

not a / (min (a,b)) is light

end;
coherence

not a / (max (a,b)) is heavy

proof end;

coherence not a / (min (a,b)) is light

proof end;

registration

let a, b be Real;

coherence

not (max (a,b)) - (min (a,b)) is negative

(sgn (a - b)) * ((max (a,b)) - (min (a,b))) = a - b

end;
coherence

not (max (a,b)) - (min (a,b)) is negative

proof end;

reducibility (sgn (a - b)) * ((max (a,b)) - (min (a,b))) = a - b

proof end;

registration

let a be Real;

reducibility

a to_power 1 = a ;

reducibility

1 to_power a = 1 by POWER:26;

coherence

a to_power 0 is natural by POWER:24;

coherence

a to_power 0 is weightless by POWER:24;

end;
reducibility

a to_power 1 = a ;

reducibility

1 to_power a = 1 by POWER:26;

coherence

a to_power 0 is natural by POWER:24;

coherence

a to_power 0 is weightless by POWER:24;

registration
end;

registration
end;

registration

let a be positive heavy Real;

let b be positive Real;

coherence

a to_power b is heavy by TA1, POWER:35;

end;
let b be positive Real;

coherence

a to_power b is heavy by TA1, POWER:35;

registration
end;

registration
end;

registration
end;

registration

let a be positive non weightless Real;

let b be Real;

reducibility

log (a,(a to_power b)) = b

end;
let b be Real;

reducibility

log (a,(a to_power b)) = b

proof end;

registration

let a be positive non weightless Real;

let b be positive Real;

reducibility

a to_power (log (a,b)) = b

end;
let b be positive Real;

reducibility

a to_power (log (a,b)) = b

proof end;

theorem :: COMPLEX3:27

theorem :: COMPLEX3:28

:: Sums and products

:: 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))

(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) )

( 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) )

( max (a,b) > max (c,d) iff min (a,b) < min (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)

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

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 )

( (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 )

( (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)

(1 / a) + (1 / b) > (1 / c) + (1 / d)

proof end;

theorem :: COMPLEX3:47

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

a * b < c * d

proof end;

theorem :: COMPLEX3:49

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 )

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

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 )

( (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 :: 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) )

( 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 ) )

( 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 )

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 )

( 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

a > c

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

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

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)

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

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;

coherence

( ((k + 1) to_power n) - (k to_power n) is heavy & ((k + 1) to_power n) - (k to_power n) is positive )

end;
let n be positive heavy Real;

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;

registration

let k be positive heavy Real;

let n be non negative Real;

coherence

(k to_power (n + 1)) - (k to_power n) is positive

end;
let n be non negative Real;

coherence

(k to_power (n + 1)) - (k to_power n) is positive

proof 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

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

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

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

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

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 ) )

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 )

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 )

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: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 :: 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) )

( ((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))

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)

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: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

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: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 )

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 )

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) )

( 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 )

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)

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

registration

let a be positive heavy Real;

let b be positive Real;

coherence

log (a,(a + b)) is heavy

log ((a + b),a) is light

end;
let b be positive Real;

coherence

log (a,(a + b)) is heavy

proof end;

coherence log ((a + b),a) is light

proof end;

theorem :: COMPLEX3:93

for a being positive non weightless Real

for b being positive Real holds

( log (a,b) = 0 iff b = 1 )

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 )

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 )

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)) )

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 :: COMPLEX3:101

for a, b being positive non weightless Real st log (a,b) >= 1 holds

( 0 < log (b,a) & log (b,a) <= 1 )

( 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 )

( 0 > log (b,a) & log (b,a) >= - 1 )

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

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

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

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

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

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

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

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

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

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

for b, d being positive Real st log (a,b) <= log (c,d) & a <= b holds

c <= d

proof end;