:: Multiplication-related Classes of Complex Numbers
::  by Rafal Ziobro
:: 
:: Received May 31, 2020
:: Copyright (c) 2020-2021 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NUMBERS, ARYTM_3, ZFMISC_1, CARD_1, XXREAL_0, ARYTM_1, RELAT_1,
      REAL_1, XCMPLX_0, COMPLEX3, COMPLEX1, ABSVALUE, NAT_1, NEWTON, POWER,
      INT_1, SQUARE_1, XREAL_0, PROB_2, ORDINAL1;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, FUNCT_4, ARYTM_2,
      ARYTM_1, ARYTM_0, XCMPLX_0, XREAL_0, NUMBERS, XXREAL_0, COMPLEX1,
      ABSVALUE, NEWTON, INT_1, SQUARE_1, COMPLEX2, PROB_2, POWER, POLYEQ_5,
      RAT_1, REAL_1, NAT_1, COMSEQ_2, SEQ_4, XXREAL_2, INT_2, PYTHTRIP,
      IRRAT_1, NAT_3, CARD_1, NAT_D, RELAT_1, FUNCT_1;
 constructors FUNCT_4, ARYTM_1, ARYTM_0, XCMPLX_0, XXREAL_0, XREAL_0, COMPLEX1,
      ABSVALUE, NEWTON, ORDINAL1, NAT_1, INT_1, REAL_1, SQUARE_1, POWER, ABIAN,
      COMPLEX2, PROB_2, POLYEQ_5, SEQ_2, SEQM_3, SEQ_4, XXREAL_2, RELSET_1,
      BINOP_2, COMSEQ_2, PREPOWER, NAT_D, PEPIN, PYTHTRIP, RAT_1, NAT_3,
      NUMBERS, WSIERP_1, MOEBIUS1, EULER_1;
 registrations XCMPLX_0, XXREAL_0, XREAL_0, ORDINAL1, NEWTON03, NAT_1, NEWTON,
      NAT_6, INT_1, COMPLEX1, SQUARE_1, ABIAN, ABSVALUE, POWER, REAL_3,
      PARTFUN3, FOMODEL0;
 requirements SUBSET, NUMERALS, ARITHM, REAL;


begin

registration
  let a be Complex;
  reduce a"" to a;
end;

definition
  let a be Complex;
  attr a is heavy means
:: COMPLEX3:def 1

  |.a.| > 1;
  attr a is light means
:: COMPLEX3:def 2

  |.a.| < 1;
:: zero is included in weightless so as to adhere to trivial for Nats
  attr a is weightless means
:: COMPLEX3:def 3

  |.a.| = 0 or |.a.| = 1;
end;

::added theorems
theorem :: COMPLEX3:1
  for a be Real holds
  (a is heavy negative iff a < -1) &
  (a is light negative iff -1 < a < 0) &
  (a is light positive iff 0 < a < 1) &
  (a is heavy positive iff a > 1) &
  (a is weightless positive iff a = 1) &
  (a is weightless negative iff a = -1);

theorem :: COMPLEX3:2
  for a be Real holds (a is non light negative iff a <= -1) &
  (a is non heavy negative iff -1 <= a < 0) &
  (a is non heavy positive  iff 0 < a <= 1) &
  (a is non light positive iff 1 <= a);

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

registration
  cluster zero -> weightless for Complex;
  cluster heavy -> non light for Complex;
  cluster non light -> non zero for Complex;
  cluster heavy -> non weightless for Complex;
  cluster light -> non weightless for non zero Complex;
  cluster light -> zero for Integer;
  cluster trivial -> weightless for Nat;
  cluster non heavy -> trivial for Nat;
  cluster non zero -> non light for Nat;
  cluster non trivial -> heavy for Nat;
  cluster weightless -> non heavy for Complex;
  cluster light -> non heavy for Complex;
  cluster non light -> positive for non negative Real;
end;

registration
  cluster heavy for positive Real;
  cluster heavy for negative Real;
  cluster light for positive Real;
  cluster light for negative Real;
  cluster positive for weightless Integer;
  cluster negative for weightless Integer;
end;

:: more on Complex numbers

theorem :: COMPLEX3:4
  for a be Complex holds Re a >= -|.a.|;

theorem :: COMPLEX3:5
  for a be Complex holds Im a >= -|.a.|;

theorem :: COMPLEX3:6
  for a be Complex holds |.Re a.| + |.Im a.| >= |.a.|;

:: registrations
:: using single variable

registration
  let a be Complex;
  cluster a*a" -> trivial;
  cluster a*a*' -> real;
  cluster (a*a*')|^2 -> non negative;
  cluster a/|.a.| -> weightless;
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.|;
end;

theorem :: COMPLEX3:7
  for a be Complex holds a = |.a.|*director a;

theorem :: COMPLEX3:8
  for a be Complex holds director (-a) = -director a;

registration
  let a be Real;
  identify director a with sgn a;
end;

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

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

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

registration
  reduce director 0 to 0;
end;

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

registration
  let a be weightless Complex;
  cluster -a -> weightless;
  cluster a*' -> weightless;
  cluster a" -> weightless;
  cluster a*a*' -> weightless;
  cluster |.Re a.| -> non heavy;
  cluster |.Im a.| -> non heavy;
  cluster |.a.| - 1 -> weightless;
  cluster 1 - |.a.| -> weightless;
end;

registration
  let a be weightless Real;
  reduce sgn a to a;
end;

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

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

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

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

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

registration
  let a be non zero non heavy Complex;
  cluster a" -> non light;
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);
end;

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

registration
  let a be Real;
  identify rsgn a with sgn a;
  identify sgn a with rsgn a;
  cluster isgn a -> zero;
end;

registration
  let a be Real;
  cluster frac a -> light;
  cluster |.a.| + a -> non negative;
  cluster |.a.| - a -> non negative;
end;

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

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

::/added

theorem :: COMPLEX3:9
  for a be non heavy Complex holds
  a is light or a is weightless;

theorem :: COMPLEX3:10
  for a be non light Complex holds
  a is heavy or a is weightless;

theorem :: COMPLEX3:11
  for a be heavy positive Real, b be non heavy Real holds a > b > -a;

theorem :: COMPLEX3:12
  for a be non light positive Real, b be light Real holds a > b > -a;

:: multiplication

registration
  let a be heavy Complex, b be non light Complex;
  cluster a*b -> heavy;
end;

registration
  let a,b be non light Complex;
  cluster a*b -> non light;
end;

registration
  let a be light Complex, b be non heavy Complex;
  cluster a*b -> light;
end;

registration
  let a,b be non heavy Complex;
  cluster a*b -> non heavy;
end;

registration
  let a,b be weightless Complex;
  cluster a*b -> weightless;
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.|;
end;

theorem :: COMPLEX3:13
  for a be Complex holds cfrac (-a) = -cfrac a;

registration
  let a be non negative Real;
  identify frac a with cfrac a;
  identify cfrac a with frac a;
end;

:: power, root

theorem :: COMPLEX3:14
  for a be Complex, n be Nat holds |.a.||^n = |.a|^n.|;

registration
  let a be weightless Complex, n be Nat;
  cluster a|^n -> weightless;
end;

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

registration
  let a be non light Complex, n be Nat;
  cluster a|^n -> non light;
end;

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

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

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

registration
  let a be non heavy Complex, n be Nat;
  cluster a|^n -> non heavy;
end;

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

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

registration
  let a be non weightless Complex, n be non zero Nat;
  cluster a|^n -> non weightless;
end;

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

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

registration
  let a be non light Complex, n be non zero Nat;
  cluster n -root a -> non light;
end;

registration
  let a be non heavy Complex, n be non zero Nat;
  cluster n -root a -> non heavy;
end;

:: division

registration
  let a,b be weightless Complex;
  cluster a/b -> weightless;
end;

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

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

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

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

:: sum

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

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

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

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

registration
  let a be non heavy Real, b be heavy positive Real;
  cluster a+b -> positive;
end;

registration
  let a be light Real, b be non light positive Real;
  cluster a+b -> positive;
end;

registration
  let a be non heavy Real, b be non light positive Real;
  cluster a+b -> non negative;
end;

registration
  let a be non heavy Real, b be heavy negative Real;
  cluster a+b -> negative;
end;

registration
  let a be light Real, b be non light negative Real;
  cluster a+b -> negative;
end;

registration
  let a be non heavy Real, b be non light negative Real;
  cluster a+b -> non positive;
end;

registration
  let a be light positive Real, c be light negative Real;
  cluster a+c -> light;
end;

registration
  let a be non heavy positive Real, c be non heavy negative Real;
  cluster a+c -> non heavy;
end;

:: min, max

registration
  let a,b be Real;
  cluster a - min(a,b) -> non negative;
end;

:: choosing one element of two of the same type

registration
  let a,b be weightless Real;
  cluster min(a,b) -> weightless;
  cluster max(a,b) -> weightless;
end;

registration
  let a,b be light Real;
  cluster min(a,b) -> light;
  cluster max(a,b) -> light;
end;

registration
  let a,b be heavy Real;
  cluster min(a,b) -> heavy;
  cluster max(a,b) -> heavy;
end;

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

:: some theorems

theorem :: COMPLEX3:15
  for a,b be Real st a*b is positive holds |.a - b.| < |.a + b.|;

theorem :: COMPLEX3:16
  for a,b be Real st a*b is negative holds |.a - b.| > |.a + b.|;

theorem :: COMPLEX3:17
  for a,b be non zero Real holds |.a|^2 - b|^2.| < |.a|^2 + b|^2.|;

:: reformulation of theorems

theorem :: COMPLEX3:18 ::SERIES_5:3:
  for a,b,c be positive Real st a < b holds (b+c)/(a+c) is heavy;

:: 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 :: COMPLEX3:19
  for a,b be positive Real holds (a/b + b/a)/2 >= 1;

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

theorem :: COMPLEX3:21
  for a be negative Real, b be positive Real holds (a/b + b/a)/2 <= -1;

registration
  let a,b be non zero Real;
  cluster (a/b + b/a)/2 -> non light;
  cluster a/b + b/a -> heavy;
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 be non zero Real holds (a/b + b/a)|^2 >= 4;

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

::SERIESx5x13:
registration
  let a,b be light Real;
  cluster (a+b)/(1+a*b) -> non heavy;
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;
end;

:: ADDED 2020

registration
  let a be non negative Real;
  reduce |.-a.| to a;
end;

registration
  cluster trivial non zero for Nat;
  cluster trivial for Nat;
end;

registration
  let a,b be non zero Real;
  cluster min (a,b) -> non zero;
  cluster max (a,b) -> non zero;
end;

registration let a be non negative Real, b be Real;
  cluster max (a,b) -> non negative;
end;

registration let a be non positive Real, b be Real;
  cluster min (a,b) -> non positive;
end;

registration let a be positive Real, b be Real;
  cluster max (a,b) -> positive;
end;

registration let a be negative Real, b be Real;
  cluster min (a,b) -> negative;
end;

registration
  let a,b be non negative Real;
  cluster min (a,b) -> non negative;
end;

registration
  let a,b be non positive Real;
  cluster max (a,b) -> non positive;
end;

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

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

theorem :: COMPLEX3:23
  for a,b be Real st sgn a > sgn b holds a > b;

theorem :: COMPLEX3:24
  for a,b be non zero Real st sgn a > sgn b holds a is positive & b is negative
;

registration let a,b be Real;
  cluster max (a,b) - min (a,b) -> non negative;
  reduce sgn (a-b) * (max (a,b) - min (a,b)) to a - b;
end;

registration
  let a be Real;
  reduce a to_power 1 to a;
  reduce 1 to_power a to 1;
  cluster a to_power 0 -> natural;
  cluster a to_power 0 -> weightless;
end;

registration
  let a be positive Real, b be Real;
  cluster a to_power b -> positive;
end;

registration
  let a be weightless positive Real, b be positive Real;
  reduce b to_power a to b;
end;

registration
  let a be heavy positive Real, b be positive Real;
  cluster a to_power b -> heavy;
end;

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

registration
  let a be light positive Real, b be positive Real;
  cluster a to_power b -> light;
end;

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

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

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

theorem :: COMPLEX3:25
  for a,b be positive Real holds
  a > b iff 1/a < 1/b;

theorem :: COMPLEX3:26
  for a,b be negative Real holds
  a > b iff 1/a < 1/b;

theorem :: COMPLEX3:27
  for a,b be positive Real holds
  1/a > 1/b iff -a > -b;

theorem :: COMPLEX3:28
  for a,b be negative Real holds
  1/a > 1/b iff -a > -b;

theorem :: COMPLEX3:29
  for a,b be positive Real holds sgn (1/a - 1/b) = sgn (b - a);

theorem :: COMPLEX3:30
  for a,b be negative Real holds sgn (1/a - 1/b) = sgn (b - a);

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

:: Sums and products

theorem :: COMPLEX3:32
  for a,b be non zero Real holds
  a + b = a * b iff 1/a + 1/b = 1;

theorem :: COMPLEX3:33
  for a,b be positive Real holds
  a + b > a * b iff 1/a + 1/b > 1;

theorem :: COMPLEX3:34
  for a,b be positive Real holds a + b < a * b iff 1/a + 1/b < 1;

theorem :: COMPLEX3:35
  for a be non heavy positive Real, b be positive Real holds a + b > a * b;

theorem :: COMPLEX3:36
  for a,b be non zero Real holds a - b = a*b iff 1/b - 1/a = 1;

theorem :: COMPLEX3:37
  for a,b be positive Real holds a - b = a*b implies b is light;

:: Some relations for equal sums

theorem :: COMPLEX3:38
  for a,b,c,d be positive Real st a + b = c + d holds
  max (a,b) - max (c,d) = min (c,d) - min (a,b);

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

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

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

theorem :: COMPLEX3:42
  for a,b,c,d be positive Real, n be 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;

theorem :: COMPLEX3:43
  for a,b,c,d be positive Real, n be 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;

theorem :: COMPLEX3:44
  for a,b,c,d be positive Real st a + b = c + d holds
  1/a + 1/b = 1/c + 1/d  iff a*b = c*d;

theorem :: COMPLEX3:45
  for a,b,c,d be positive Real st a + b = c + d holds
    1/a + 1/b > 1/c + 1/d iff a*b < c*d;

theorem :: COMPLEX3:46
  for a,b,c,d be positive Real st a + b >= c + d & a*b < c*d holds
    1/a + 1/b > 1/c + 1/d;

theorem :: COMPLEX3:47
  for a,b,c,d be positive Real st a*b < c*d & 1/a + 1/b <= 1/c + 1/d holds
  a + b < c + d;

theorem :: COMPLEX3:48
  for a,b,c,d be positive Real st a + b <= c + d & 1/a + 1/b > 1/c + 1/d holds
  a*b < c*d;

theorem :: COMPLEX3:49
  for a,b,c,d be positive Real st a*b >= c*d holds
  a + b > c + d or 1/a + 1/b <= 1/c + 1/d;

theorem :: COMPLEX3:50  ::see NEWTON01:5,NEWTON01:8
  for a,b be positive Real, n,m be 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;

theorem :: COMPLEX3:51
for a,b be positive Real, n be 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;

theorem :: COMPLEX3:52
  for a,b be positive Real, n,m be 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;

theorem :: COMPLEX3:53
  for a,b be positive Real, n,m be 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;

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

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

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

theorem :: COMPLEX3:57
  for a,b be non negative Real, c be positive Real holds
  a >= b iff a to_power c >= b to_power c;

theorem :: COMPLEX3:58 ::see NEWTON03:42;
  for a,b,n be 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;

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

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

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

theorem :: COMPLEX3:62
  for a,b be positive Real, m be non negative Real, n be positive Real holds
  a to_power m + b to_power m <= 1 implies
  a to_power (m+n) + b to_power (m+n) < 1;

theorem :: COMPLEX3:63
  for a,b be positive Real, m be non positive Real, n be negative Real holds
  a to_power m + b to_power m <= 1 implies
  a to_power (m+n) + b to_power (m+n) < 1;

theorem :: COMPLEX3:64
  for a,b,c,n be positive Real, m be non negative Real holds
  a to_power m + b to_power m <= c to_power m implies
  a to_power (m+n) + b to_power (m+n) < c to_power (m+n);

theorem :: COMPLEX3:65
  for a,b be positive Real, n be heavy positive Real holds
  a to_power n + b to_power n < (a + b) to_power n;

registration
  let k be positive Real, n be heavy positive Real;
  cluster (k+1) to_power n - k to_power n -> heavy positive;
end;

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

theorem :: COMPLEX3:66
  for k be positive Real, n be heavy positive Real holds
  (k+1) to_power n > (k to_power n) + 1;

theorem :: COMPLEX3:67
  for a,b be positive Real, n be light positive Real holds
  a to_power n + b to_power n > (a + b) to_power n;

theorem :: COMPLEX3:68
  for k be positive Real, n be light positive Real holds
  (k+1) to_power n < (k to_power n) + 1;

theorem :: COMPLEX3:69
  for k be positive Real, n be non positive Real holds
  (k+1) to_power n < (k to_power n) + 1;

theorem :: COMPLEX3:70
  for a,b be positive Real, n be non positive Real holds
  a to_power n + b to_power n > (a + b) to_power n;

theorem :: COMPLEX3:71
  for a,b be positive Real, n be Real holds
  (a + b) to_power n > a to_power n + b to_power n iff n is heavy positive;

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

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

theorem :: COMPLEX3:74
  for a,b,c be positive Real holds (a+b)*(a+c) > a*(a+b+c);

theorem :: COMPLEX3:75
  for a,b,c be positive Real holds (a+b+c)/(a+b) < (a+c)/a;

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

theorem :: COMPLEX3:77
  for a,b be heavy positive Real holds a+b-1 > a/b > 1/(a+b-1);

theorem :: COMPLEX3:78
  for a,b,c be positive Real holds (a+b+c)/a > (a+b)/(a+c) > a/(a+b+c);

theorem :: COMPLEX3:79
  for a be light positive Real, n be heavy positive Real holds
  ((1+a) to_power n)*((1-a) to_power n) < (1 + a to_power n)*(1 - a to_power n)
;

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

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

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

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

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

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

theorem :: COMPLEX3:86
  for a be light positive Real, n be heavy positive Real holds
  2 to_power n > (1+a) to_power n - (1-a) to_power n > (2*a) to_power n;

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

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

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

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

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

:: Logarithms

theorem :: COMPLEX3:92
  for a,b be non weightless positive Real holds
  log (a,b) = 1/log (b,a);

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

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

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

theorem :: COMPLEX3:95
  for a,b be positive Real, n be non zero Real holds
  a to_power n = b to_power n iff a = b;

theorem :: COMPLEX3:96
  for a be non weightless positive Real, b be 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);

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

theorem :: COMPLEX3:98
  for a be light positive Real, b be positive Real holds
  a < b iff log (a,b) < 1;

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

theorem :: COMPLEX3:100
  for a be light positive Real, b be positive Real holds
  a > b iff log (a,b) > 1;

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

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

theorem :: COMPLEX3:103
  for a,b be heavy positive Real holds
  log (a,b) > log (b,a) >= 1 implies a > b;

theorem :: COMPLEX3:104
  for a,b be heavy positive Real holds
  log (b,a) < 1 implies a < b;

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

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

theorem :: COMPLEX3:107
  for a be heavy positive Real,c be light positive Real, b,d be positive Real
  holds
  log (a,b) <= log (c,d) & a < b implies c > d;

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

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

theorem :: COMPLEX3:110
  for a,c be light positive Real, b,d be positive Real holds
  log (a,b) >= log (c,d) & a < b implies c < d;

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

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

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

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

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