complex3.miz

begin

 registration

 let a be Complex;

 reduce ((a " ) " ) to a;

 reducibility ;

 end

 definition

 let a be Complex;

 :: COMPLEX3:def1

 attr a is heavy means

 : Def1: |.a.| > 1;

 :: COMPLEX3:def2

 attr a is light means

 : Def2: |.a.| < 1;

 :: COMPLEX3:def3

 attr a is weightless means

 : Def3: |.a.| = 0 or |.a.| = 1;

 end

 theorem :: COMPLEX3:1



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

 proof

 let a be Real;



 A1: a is heavy negative implies a < ( - 1)

 proof

 assume a is heavy negative;

 then ( - a) > 1 by ABSVALUE:def 1;

 then ( - ( - a)) < ( - 1) by XREAL_1: 24;

 hence thesis;

 end;



 A1a: a < ( - 1) implies a is heavy negative

 proof

 assume

 B1: a < ( - 1);

 then ( - a) > ( - ( - 1)) by XREAL_1: 24;

 hence thesis by B1, ABSVALUE:def 1;

 end;



 A3: a is light negative implies ( - 1) < a < 0

 proof

 assume

 B1: a is light negative;

 then ( - a) < 1 by ABSVALUE:def 1;

 then ( - ( - a)) > ( - 1) by XREAL_1: 24;

 hence thesis by B1;

 end;



 A3a: ( - 1) < a < 0 implies a is light negative

 proof

 assume

 B1: ( - 1) < a < 0 ;

 then ( - a) < ( - ( - 1)) by XREAL_1: 24;

 hence thesis by B1, ABSVALUE:def 1;

 end;

 a is weightless implies a = 0 or 1 = a or 1 = ( - a) by ABSVALUE: 1;

 hence thesis by A1, A1a, ABSVALUE:def 1, A3, A3a;

 end;

 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)

 proof

 let a be Real;



 A1: a is non light negative implies a <= ( - 1)

 proof

 assume a is non light negative;

 then ( - a) >= 1 by ABSVALUE:def 1;

 then ( - ( - a)) <= ( - 1) by XREAL_1: 24;

 hence thesis;

 end;



 A1a: a <= ( - 1) implies a is non light negative

 proof

 assume

 B1: a <= ( - 1);

 then ( - a) >= ( - ( - 1)) by XREAL_1: 24;

 hence thesis by B1, ABSVALUE:def 1;

 end;



 A3: a is non heavy negative implies ( - 1) <= a < 0

 proof

 assume

 B1: a is non heavy negative;

 then ( - a) <= 1 by ABSVALUE:def 1;

 then ( - ( - a)) >= ( - 1) by XREAL_1: 24;

 hence thesis by B1;

 end;

 ( - 1) <= a < 0 implies a is non heavy negative

 proof

 assume

 B1: ( - 1) <= a < 0 ;

 then ( - a) <= ( - ( - 1)) by XREAL_1: 24;

 hence thesis by B1, ABSVALUE:def 1;

 end;

 hence thesis by A1, A1a, A3;

 end;

 theorem :: COMPLEX3:3



 Th0: for a be Real holds a is weightless iff a = ( sgn a)

 proof

 let a be Real;



 A1: a is weightless implies a = ( sgn a)

 proof

 assume a is weightless;

 then a = 0 or a = |.1.| or ( - a) = |.1.| by ABSVALUE: 1;

 hence thesis by ABSVALUE:def 2;

 end;

 a = ( sgn a) implies a is weightless

 proof

 assume that

 A1: a = ( sgn a);

 a > 0 or a = 0 or a < 0 ;

 then ( sgn a) = 0 or ( sgn a) = 1 or ( sgn a) = ( - 1) by ABSVALUE:def 2;

 hence thesis by A1;

 end;

 hence thesis by A1;

 end;

 registration

 cluster zero -> weightless for Complex;

 coherence ;

 cluster heavy -> non light for Complex;

 coherence ;

 cluster non light -> non zero for Complex;

 coherence ;

 cluster heavy -> non weightless for Complex;

 coherence ;

 cluster light -> non weightless for non zero Complex;

 coherence ;

 cluster light -> zero for Integer;

 coherence by NAT_1: 14;

 cluster trivial -> weightless for Nat;

 coherence ;

 cluster non heavy -> trivial for Nat;

 coherence ;

 cluster non zero -> non light for Nat;

 coherence ;

 cluster non trivial -> heavy for Nat;

 coherence ;

 cluster weightless -> non heavy for Complex;

 coherence ;

 cluster light -> non heavy for Complex;

 coherence ;

 cluster non light -> positive for non negative Real;

 coherence ;

 end

 registration

 cluster heavy for positive Real;

 existence

 proof

 2 is heavy;

 hence thesis;

 end;

 cluster heavy for negative Real;

 existence

 proof

 ( - 2) is heavy;

 hence thesis;

 end;

 cluster light for positive Real;

 existence

 proof

 (1 / 2) is light;

 hence thesis;

 end;

 cluster light for negative Real;

 existence

 proof

 |.( - (1 / 2)).| = ( - ( - (1 / 2))) by ABSVALUE:def 1;

 then ( - (1 / 2)) is light;

 hence thesis;

 end;

 cluster positive for weightless Integer;

 existence

 proof

 1 is weightless;

 hence thesis;

 end;

 cluster negative for weightless Integer;

 existence

 proof

 ( - 1) is weightless;

 hence thesis;

 end;

 end

 theorem :: COMPLEX3:4



 COMPLEX154a: for a be Complex holds ( Re a) >= ( - |.a.|)

 proof

 let a be Complex;

 reconsider b = ( - a) as Complex;

 ( Re b) <= |.b.| by COMPLEX1: 54;

 then ( - ( Re a)) <= ( - ( - |.b.|)) by COMPLEX1: 17;

 then ( Re a) >= ( - |.( - a).|) by XREAL_1: 24;

 hence thesis by COMPLEX1: 52;

 end;

 theorem :: COMPLEX3:5



 COMPLEX155a: for a be Complex holds ( Im a) >= ( - |.a.|)

 proof

 let a be Complex;

 reconsider b = ( - a) as Complex;

 ( Im b) <= |.b.| by COMPLEX1: 55;

 then ( - ( Im a)) <= ( - ( - |.b.|)) by COMPLEX1: 17;

 then ( Im a) >= ( - |.( - a).|) by XREAL_1: 24;

 hence thesis by COMPLEX1: 52;

 end;

 theorem :: COMPLEX3:6



 RI: for a be Complex holds ( |.( Re a).| + |.( Im a).|) >= |.a.|

 proof

 let a be Complex;

 |.(( Im a) * ).| = ( |.( Im a).| * |. .|) by COMPLEX1: 65

 .= |.( Im a).| by COMPLEX1: 49;

 then |.(( Re a) + (( Im a) * )).| <= ( |.( Re a).| + |.( Im a).|) by COMPLEX1: 56;

 hence thesis by COMPLEX1: 13;

 end;

 registration

 let a be Complex;

 cluster (a * (a " )) -> trivial;

 coherence

 proof

 per cases ;

 suppose a is zero;

 hence thesis;

 end;

 suppose a is non zero;

 then ((1 * a) * (a " )) = 1 by XCMPLX_1: 203;

 hence thesis by NAT_2:def 1;

 end;

 end;

 cluster (a * (a *' )) -> real;

 coherence

 proof

 (a * (a *' )) = (a .|. a) by COMPLEX2:def 1

 .= ((( Re a) ^2 ) + (( Im a) ^2 )) by COMPLEX2: 30;

 hence thesis;

 end;

 cluster ((a * (a *' )) |^ 2) -> non negative;

 coherence

 proof

 reconsider b = (a * (a *' )) as Real;

 (b |^ (2 * 1)) is non negative;

 hence thesis;

 end;

 cluster (a / |.a.|) -> weightless;

 coherence

 proof

 per cases ;

 suppose a is zero;

 hence thesis;

 end;

 suppose not a is zero;

 then

 reconsider b = |.a.| as non zero Real;

 1 = ((1 * b) / |.b.|) by XCMPLX_1: 89

 .= |.(a / |.a.|).| by COMPLEX1: 67;

 hence thesis;

 end;

 end;

 end

 definition

 let a be Complex;

 :: COMPLEX3:def4

 func director a -> weightless Complex equals (a / |.a.|);

 coherence ;

 end

 theorem :: COMPLEX3:7

 for a be Complex holds a = ( |.a.| * ( director a))

 proof

 let a be Complex;

 per cases ;

 suppose a is zero;

 hence thesis;

 end;

 suppose not a is zero;

 hence thesis by XCMPLX_1: 87;

 end;

 end;

 theorem :: COMPLEX3:8



 DIR: for a be Complex holds ( director ( - a)) = ( - ( director a))

 proof

 let a be Complex;

 ( director ( - a)) = (( - a) / |.a.|) by COMPLEX1: 52;

 hence thesis;

 end;

 registration

 let a be Real;

 identify sgn a with director a;

 correctness

 proof

 per cases ;

 suppose a = 0 ;

 hence thesis by ABSVALUE:def 2;

 end;

 suppose a > 0 ;

 then

 reconsider a as positive Real;



 W1: ( Re ( director a)) = ( Re ((1 * |.a.|) / |.a.|))

 .= ( Re 1) by XCMPLX_1: 89

 .= 1 by COMPLEX1:def 1

 .= ( sgn a) by ABSVALUE:def 2

 .= ( Re ( sgn a)) by COMPLEX1:def 1;

 ( Im ( director a)) = ( Im ( sgn a));

 hence thesis by W1, COMPLEX1:def 3;

 end;

 suppose a < 0 ;

 then

 reconsider a as negative Real;

 ( - a) = |.a.| by ABSVALUE:def 1;



 then

 W1: ( Re ( director a)) = ( Re ((( - 1) * |.a.|) / |.a.|))

 .= ( Re ( - 1)) by XCMPLX_1: 89

 .= ( - 1) by COMPLEX1:def 1

 .= ( sgn a) by ABSVALUE:def 2

 .= ( Re ( sgn a)) by COMPLEX1:def 1;

 ( Im ( director a)) = ( Im ( sgn a));

 hence thesis by COMPLEX1:def 3, W1;

 end;

 end;

 end

 registration

 let a be Real;

 cluster ( director a) -> integer;

 coherence ;

 end

 registration

 let a be negative Real;

 cluster ( director a) -> negative;

 coherence ;

 end

 registration

 let a be positive Real;

 cluster ( director a) -> positive;

 coherence ;

 end

 registration

 reduce ( director 0 ) to 0 ;

 reducibility ;

 end

 registration

 let a be non weightless Complex;

 cluster |.a.| -> positive;

 coherence

 proof

 |.a.| >= 0 & |.a.| <> 0 by Def3;

 hence thesis;

 end;

 cluster ( - a) -> non weightless;

 coherence

 proof

 |.a.| = |.( - a).| by COMPLEX1: 52;

 hence thesis by Def3;

 end;

 cluster (a *' ) -> non weightless;

 coherence

 proof

 |.(a *' ).| = |.a.| by COMPLEX1: 53;

 hence thesis by Def3;

 end;

 cluster (a " ) -> non weightless;

 coherence

 proof

 ( |.a.| " ) <> 0 & ( |.a.| " ) <> (1 " ) by Def3;

 hence thesis by COMPLEX1: 66;

 end;

 end

 registration

 let a be weightless Complex;

 cluster ( - a) -> weightless;

 coherence

 proof

 |.a.| = |.( - a).| by COMPLEX1: 52;

 hence thesis by Def3;

 end;

 cluster (a *' ) -> weightless;

 coherence

 proof

 |.(a *' ).| = |.a.| by COMPLEX1: 53;

 hence thesis by Def3;

 end;

 cluster (a " ) -> weightless;

 coherence

 proof

 per cases by Def3;

 suppose a = 0 ;

 hence thesis;

 end;

 suppose |.a.| = 1;

 then |.(a " ).| = (1 " ) by COMPLEX1: 66;

 hence thesis;

 end;

 end;

 cluster (a * (a *' )) -> weightless;

 coherence

 proof



 A1: ( |.a.| * |.(a *' ).|) = |.(a * (a *' )).| by COMPLEX1: 65;

 a is weightless implies (a *' ) is weightless;

 hence thesis by A1, Def3;

 end;

 cluster |.( Re a).| -> non heavy;

 coherence

 proof

 reconsider c = |.( Re a).| as non negative Real;

 ( - |.a.|) <= ( Re a) <= |.a.| by COMPLEX1: 54, COMPLEX154a;

 then c <= |.a.| by ABSVALUE: 5;

 hence thesis by Def3;

 end;

 cluster |.( Im a).| -> non heavy;

 coherence

 proof

 reconsider c = |.( Im a).| as non negative Real;

 ( - |.a.|) <= ( Im a) <= |.a.| by COMPLEX1: 55, COMPLEX155a;

 then c <= |.a.| by ABSVALUE: 5;

 hence thesis by Def3;

 end;

 cluster ( |.a.| - 1) -> weightless;

 coherence

 proof

 per cases by Def3;

 suppose |.a.| = 0 ;

 hence thesis;

 end;

 suppose |.a.| = 1;

 hence thesis;

 end;

 end;

 cluster (1 - |.a.|) -> weightless;

 coherence

 proof

 per cases by Def3;

 suppose |.a.| = 0 ;

 hence thesis;

 end;

 suppose |.a.| = 1;

 hence thesis;

 end;

 end;

 end

 registration

 let a be weightless Real;

 reduce ( sgn a) to a;

 reducibility by Th0;

 end

 registration

 let a be heavy Complex;

 cluster ( - a) -> heavy;

 coherence

 proof

 |.a.| = |.( - a).| by COMPLEX1: 52;

 hence thesis by Def1;

 end;

 cluster (a *' ) -> heavy;

 coherence

 proof

 |.(a *' ).| = |.a.| by COMPLEX1: 53;

 hence thesis by Def1;

 end;

 cluster (a " ) -> light;

 coherence

 proof

 |.(a " ).| = ( |.a.| " ) by COMPLEX1: 66;

 hence thesis by XREAL_1: 212, Def1;

 end;

 cluster (a * (a *' )) -> heavy;

 coherence

 proof

 a is heavy implies (a *' ) is heavy;

 then ( |.a.| * |.(a *' ).|) > (1 * 1) by Def1, XREAL_1: 97;

 hence thesis by COMPLEX1: 65;

 end;

 cluster ( |.( Re a).| + |.( Im a).|) -> heavy;

 coherence

 proof

 reconsider c = ( |.( Re a).| + |.( Im a).|) as non negative Real;

 c >= |.a.| > 1 by RI, Def1;

 hence thesis by XXREAL_0: 2;

 end;

 cluster ( |.a.| - 1) -> positive;

 coherence

 proof

 ( |.a.| - 1) > (1 - 1) by XREAL_1: 9, Def1;

 hence thesis;

 end;

 cluster (1 - |.a.|) -> negative;

 coherence

 proof

 (1 - |.a.|) < ( |.a.| - |.a.|) by XREAL_1: 9, Def1;

 hence thesis;

 end;

 end

 registration

 let a be non light Complex;

 cluster ( - a) -> non light;

 coherence

 proof

 |.a.| = |.( - a).| by COMPLEX1: 52;

 hence thesis by Def2;

 end;

 cluster (a *' ) -> non light;

 coherence

 proof

 |.(a *' ).| = |.a.| by COMPLEX1: 53;

 hence thesis by Def2;

 end;

 cluster (a " ) -> non heavy;

 coherence

 proof

 |.(a " ).| = ( |.a.| " ) by COMPLEX1: 66;

 hence thesis by XREAL_1: 211, Def2;

 end;

 cluster (a * (a *' )) -> non light;

 coherence

 proof

 |.a.| >= 1 & |.(a *' ).| >= 1 by Def2;

 then ( |.a.| * |.(a *' ).|) >= (1 * 1) by XREAL_1: 66;

 hence thesis by COMPLEX1: 65;

 end;

 cluster ( |.( Re a).| + |.( Im a).|) -> non light;

 coherence

 proof

 reconsider c = ( |.( Re a).| + |.( Im a).|) as non negative Real;

 c >= |.a.| >= 1 by RI, Def2;

 hence thesis by XXREAL_0: 2;

 end;

 cluster ( |.a.| - 1) -> non negative;

 coherence

 proof

 ( |.a.| - 1) >= (1 - 1) by XREAL_1: 9, Def2;

 hence thesis;

 end;

 cluster (1 - |.a.|) -> non positive;

 coherence

 proof

 (1 - |.a.|) <= ( |.a.| - |.a.|) by XREAL_1: 9, Def2;

 hence thesis;

 end;

 end

 registration

 let a be light Complex;

 cluster ( - a) -> light;

 coherence

 proof

 |.a.| = |.( - a).| by COMPLEX1: 52;

 hence thesis by Def2;

 end;

 cluster (a *' ) -> light;

 coherence

 proof

 |.(a *' ).| = |.a.| by COMPLEX1: 53;

 hence thesis by Def2;

 end;

 cluster (a * (a *' )) -> light;

 coherence

 proof

 |.a.| < 1 & |.(a *' ).| < 1 by Def2;

 then ( |.a.| * |.(a *' ).|) < (1 * 1) by XREAL_1: 96;

 hence thesis by COMPLEX1: 65;

 end;

 cluster ( |.a.| - 1) -> negative;

 coherence

 proof

 ( |.a.| - 1) < (1 - 1) by Def2, XREAL_1: 9;

 hence thesis;

 end;

 cluster (1 - |.a.|) -> positive;

 coherence

 proof

 (1 - |.a.|) > ( |.a.| - |.a.|) by Def2, XREAL_1: 9;

 hence thesis;

 end;

 cluster ( Re a) -> light;

 coherence

 proof

 per cases ;

 suppose ( Re a) is non negative;

 then

 reconsider b = ( Re a) as non negative Real;

 ( Re a) <= |.a.| & |.a.| < 1 by COMPLEX1: 54, Def2;

 then b < 1 by XXREAL_0: 2;

 hence thesis;

 end;

 suppose ( Re a) is negative;

 then |.( Re a).| = ( - ( Re a)) & ( - ( Re a)) <= ( - ( - |.a.|)) by COMPLEX154a, ABSVALUE:def 1, XREAL_1: 24;

 hence thesis by XXREAL_0: 2, Def2;

 end;

 end;

 cluster ( Im a) -> light;

 coherence

 proof

 per cases ;

 suppose ( Im a) is non negative;

 then

 reconsider b = ( Im a) as non negative Real;

 ( Im a) <= |.a.| & |.a.| < 1 by COMPLEX1: 55, Def2;

 then b < 1 by XXREAL_0: 2;

 hence thesis;

 end;

 suppose ( Im a) is negative;

 then |.( Im a).| = ( - ( Im a)) & ( - ( Im a)) <= ( - ( - |.a.|)) by COMPLEX155a, ABSVALUE:def 1, XREAL_1: 24;

 hence thesis by XXREAL_0: 2, Def2;

 end;

 end;

 cluster (( Re a) - 1) -> negative;

 coherence

 proof

 (( Re a) - 1) <= ( |.a.| - 1) by COMPLEX1: 54, XREAL_1: 9;

 hence thesis;

 end;

 cluster (( Re a) - 2) -> heavy;

 coherence

 proof

 reconsider k = (( Re a) - 1) as negative Real;

 (k - 1) < ( 0 - 1) by XREAL_1: 9;

 then ( - (k - 1)) > ( - ( - 1)) by XREAL_1: 24;

 then |.(k - 1).| > 1 by ABSVALUE:def 1;

 hence thesis;

 end;

 cluster (( Im a) - 1) -> negative;

 coherence

 proof

 (( Im a) - 1) <= ( |.a.| - 1) by COMPLEX1: 55, XREAL_1: 9;

 hence thesis;

 end;

 cluster (( Im a) - 2) -> heavy;

 coherence

 proof

 reconsider k = (( Im a) - 1) as negative Real;

 (k - 1) < ( 0 - 1) by XREAL_1: 9;

 then ( - (k - 1)) > ( - ( - 1)) by XREAL_1: 24;

 then |.(k - 1).| > 1 by ABSVALUE:def 1;

 hence thesis;

 end;

 end

 registration

 let a be non zero light Complex;

 cluster (a " ) -> heavy;

 coherence

 proof

 (1 " ) < ( |.a.| " ) by XREAL_1: 88, Def2;

 hence thesis by COMPLEX1: 66;

 end;

 end

 registration

 let a be non heavy Complex;

 cluster ( - a) -> non heavy;

 coherence

 proof

 |.a.| = |.( - a).| by COMPLEX1: 52;

 hence thesis by Def1;

 end;

 cluster (a *' ) -> non heavy;

 coherence

 proof

 |.(a *' ).| = |.a.| by COMPLEX1: 53;

 hence thesis by Def1;

 end;

 cluster (a * (a *' )) -> non heavy;

 coherence

 proof

 |.a.| <= 1 & |.(a *' ).| <= 1 by Def1;

 then ( |.a.| * |.(a *' ).|) <= (1 * 1) by XREAL_1: 66;

 hence thesis by COMPLEX1: 65;

 end;

 cluster ( |.a.| - 1) -> non positive;

 coherence

 proof

 ( |.a.| - 1) <= (1 - 1) by Def1, XREAL_1: 9;

 hence thesis;

 end;

 cluster (1 - |.a.|) -> non negative;

 coherence

 proof

 (1 - |.a.|) >= ( |.a.| - |.a.|) by Def1, XREAL_1: 9;

 hence thesis;

 end;

 cluster ( Re a) -> non heavy;

 coherence

 proof

 per cases ;

 suppose ( Re a) is non negative;

 then

 reconsider b = ( Re a) as non negative Real;

 ( Re a) <= |.a.| & |.a.| <= 1 by COMPLEX1: 54, Def1;

 then b <= 1 by XXREAL_0: 2;

 hence thesis;

 end;

 suppose ( Re a) is negative;

 then |.( Re a).| = ( - ( Re a)) & ( - ( Re a)) <= ( - ( - |.a.|)) by COMPLEX154a, ABSVALUE:def 1, XREAL_1: 24;

 then |.( Re a).| <= |.a.| & |.a.| <= 1 by Def1;

 hence thesis by XXREAL_0: 2;

 end;

 end;

 cluster ( Im a) -> non heavy;

 coherence

 proof

 per cases ;

 suppose ( Im a) is non negative;

 then

 reconsider b = ( Im a) as non negative Real;

 ( Im a) <= |.a.| & |.a.| <= 1 by COMPLEX1: 55, Def1;

 then b <= 1 by XXREAL_0: 2;

 hence thesis;

 end;

 suppose ( Im a) is negative;

 then |.( Im a).| = ( - ( Im a)) & ( - ( Im a)) <= ( - ( - |.a.|)) by COMPLEX155a, ABSVALUE:def 1, XREAL_1: 24;

 then |.( Im a).| <= |.a.| & |.a.| <= 1 by Def1;

 hence thesis by XXREAL_0: 2;

 end;

 end;

 cluster (( Re a) - 1) -> non positive;

 coherence

 proof

 (( Re a) - 1) <= ( |.a.| - 1) by COMPLEX1: 54, XREAL_1: 9;

 hence thesis;

 end;

 cluster (( Im a) - 1) -> non positive;

 coherence

 proof

 (( Im a) - 1) <= ( |.a.| - 1) by COMPLEX1: 55, XREAL_1: 9;

 hence thesis;

 end;

 end

 registration

 let a be non zero non heavy Complex;

 cluster (a " ) -> non light;

 coherence

 proof

 (1 " ) <= ( |.a.| " ) by XREAL_1: 85, Def1;

 hence thesis by COMPLEX1: 66;

 end;

 end

 definition

 let a be Complex;

 :: COMPLEX3:def5

 func rsgn a -> non heavy Complex equals ( Re ( director a));

 coherence ;

 end

 definition

 let a be Complex;

 :: COMPLEX3:def6

 func isgn a -> non heavy Complex equals ( Im ( director a));

 coherence ;

 end

 registration

 let a be Real;

 identify sgn a with rsgn a;

 correctness

 proof

 per cases ;

 suppose a = 0 ;

 thus thesis by COMPLEX1:def 1;

 end;

 suppose a > 0 ;

 then

 reconsider a as positive Real;

 ( Re ( director a)) = ( Re ((1 * |.a.|) / |.a.|))

 .= ( Re 1) by XCMPLX_1: 89

 .= 1 by COMPLEX1:def 1;

 hence thesis by ABSVALUE:def 2;

 end;

 suppose a < 0 ;

 then

 reconsider a as negative Real;

 ( - a) = |.a.| by ABSVALUE:def 1;



 then ( Re ( director a)) = ( Re ((( - 1) * |.a.|) / |.a.|))

 .= ( Re ( - 1)) by XCMPLX_1: 89

 .= ( - 1) by COMPLEX1:def 1

 .= ( sgn a) by ABSVALUE:def 2;

 hence thesis;

 end;

 end;

 identify rsgn a with sgn a;

 correctness ;

 cluster ( isgn a) -> zero;

 coherence ;

 end

 registration

 let a be Real;

 cluster ( frac a) -> light;

 coherence

 proof

 reconsider b = ( frac a) as non negative Real by INT_1: 43;

 b = |.b.|;

 hence thesis by INT_1: 43;

 end;

 cluster ( |.a.| + a) -> non negative;

 coherence by ABSVALUE: 26;

 cluster ( |.a.| - a) -> non negative;

 coherence by ABSVALUE: 27;

 end

 registration

 let a be heavy positive Real;

 cluster (a - 1) -> positive;

 coherence

 proof

 |.a.| > 1 by TA1;

 hence thesis;

 end;

 cluster (1 - a) -> negative;

 coherence

 proof

 |.a.| > 1 by TA1;

 hence thesis;

 end;

 end

 registration

 let a be light positive Real;

 cluster (a - 1) -> negative;

 coherence

 proof

 |.a.| < 1 by TA1;

 hence thesis;

 end;

 cluster (1 - a) -> positive;

 coherence

 proof

 |.a.| < 1 by TA1;

 hence thesis;

 end;

 end

 theorem :: COMPLEX3:9



 Th1: for a be non heavy Complex holds a is light or a is weightless

 proof

 let a be non heavy Complex;

 |.a.| <= 1 by Def1;

 hence thesis by XXREAL_0: 1;

 end;

 theorem :: COMPLEX3:10

 for a be non light Complex holds a is heavy or a is weightless

 proof

 let a be non light Complex;

 |.a.| >= 1 by Def2;

 hence thesis by XXREAL_0: 1;

 end;

 theorem :: COMPLEX3:11

 for a be heavy positive Real, b be non heavy Real holds a > b > ( - a)

 proof

 let a be heavy positive Real, b be non heavy Real;

 a > 1 & 1 >= b & b >= ( - 1) & ( - 1) > ( - a) by TA1;

 hence thesis by XXREAL_0: 2;

 end;

 theorem :: COMPLEX3:12

 for a be non light positive Real, b be light Real holds a > b > ( - a)

 proof

 let a be non light positive Real, b be light Real;

 a >= 1 & 1 > b & b > ( - 1) & ( - 1) >= ( - a) by TA1;

 hence thesis by XXREAL_0: 2;

 end;

 registration

 let a be heavy Complex, b be non light Complex;

 cluster (a * b) -> heavy;

 coherence

 proof

 |.a.| > 1 & |.b.| >= 1 by Def1, Def2;

 then ( |.a.| * |.b.|) > (1 * 1) by XREAL_1: 97;

 hence thesis by COMPLEX1: 65;

 end;

 end

 registration

 let a,b be non light Complex;

 cluster (a * b) -> non light;

 coherence

 proof

 |.a.| >= 1 & |.b.| >= 1 by Def2;

 then ( |.a.| * |.b.|) >= 1 by XREAL_1: 159;

 hence thesis by COMPLEX1: 65;

 end;

 end

 registration

 let a be light Complex, b be non heavy Complex;

 cluster (a * b) -> light;

 coherence

 proof

 0 <= |.a.| < 1 & 0 <= |.b.| <= 1 by Def1, Def2;

 then ( |.a.| * |.b.|) < 1 by XREAL_1: 162;

 hence thesis by COMPLEX1: 65;

 end;

 end

 registration

 let a,b be non heavy Complex;

 cluster (a * b) -> non heavy;

 coherence

 proof

 0 <= |.a.| <= 1 & 0 <= |.b.| <= 1 by Def1;

 then ( |.a.| * |.b.|) <= 1 by XREAL_1: 160;

 hence thesis by COMPLEX1: 65;

 end;

 end

 registration

 let a,b be weightless Complex;

 cluster (a * b) -> weightless;

 coherence

 proof

 per cases by Def3;

 suppose |.a.| = 1;



 then |.(a * b).| = ( |.1.| * |.b.|) by COMPLEX1: 65

 .= |.b.|;

 hence thesis by Def3;

 end;

 suppose |.a.| = 0 ;



 then |.(a * b).| = ( |. 0 .| * |.b.|) by COMPLEX1: 65

 .= 0 ;

 hence thesis;

 end;

 end;

 end

 definition

 let a be Complex;

 :: COMPLEX3:def7

 func cfrac a -> light Complex equals (( director a) * ( frac |.a.|));

 coherence ;

 end

 theorem :: COMPLEX3:13

 for a be Complex holds ( cfrac ( - a)) = ( - ( cfrac a))

 proof

 let a be Complex;

 ( cfrac ( - a)) = (( - ( director a)) * ( frac |.( - a).|)) by DIR

 .= (( - ( director a)) * ( frac |.a.|)) by COMPLEX1: 52;

 hence thesis;

 end;

 registration

 let a be non negative Real;

 identify cfrac a with frac a;

 correctness

 proof

 per cases ;

 suppose a = 0 ;

 hence thesis by INT_1: 45;

 end;

 suppose a > 0 ;

 then

 reconsider a as positive Real;

 reconsider b = ( director a) as positive weightless Real;

 b = 1 & ( frac a) = ( frac |.a.|) by TA1;

 hence thesis;

 end;

 end;

 identify frac a with cfrac a;

 correctness ;

 end

 theorem :: COMPLEX3:14



 TAYLOR21: for a be Complex, n be Nat holds ( |.a.| |^ n) = |.(a |^ n).|

 proof

 let a be Complex, n be Nat;

 defpred P[ Nat] means ( |.a.| |^ $1) = |.(a |^ $1).|;



 A1: P[ 0 ]

 proof

 ( |.a.| |^ 0 ) = |.1.| by NEWTON: 4

 .= |.(a |^ 0 ).| by NEWTON: 4;

 hence thesis;

 end;



 A2: for k be Nat st P[k] holds P[(k + 1)]

 proof

 let k be Nat such that

 B1: ( |.a.| |^ k) = |.(a |^ k).|;

 |.(a |^ (k + 1)).| = |.(a * (a |^ k)).| by NEWTON: 6

 .= ( |.a.| * ( |.a.| |^ k)) by B1, COMPLEX1: 65;

 hence thesis by NEWTON: 6;

 end;

 for l be Nat holds P[l] from NAT_1:sch 2( A1, A2);

 hence thesis;

 end;

 registration

 let a be weightless Complex, n be Nat;

 cluster (a |^ n) -> weightless;

 coherence

 proof

 per cases by Def3;

 suppose |.a.| = 0 ;

 then a = 0 ;

 then (a |^ n) = 0 or n = 0 by NAT_1: 14, NEWTON: 11;

 then |.(a |^ n).| = 0 or (a |^ n) = 1 by NEWTON: 4;

 hence thesis;

 end;

 suppose |.a.| = 1;



 then 1 = ( |.a.| |^ n)

 .= |.(a |^ n).| by TAYLOR21;

 hence thesis;

 end;

 end;

 end

 registration

 let a be weightless Real, n be Nat;

 cluster ((a |^ (2 * n)) - 1) -> weightless;

 coherence

 proof

 per cases by Def3;

 suppose |.a.| = 0 ;

 then a = 0 ;

 then (a |^ (2 * n)) = 0 or n = 0 by NAT_1: 14, NEWTON: 11;

 then (a |^ (2 * n)) = 0 or (a |^ (2 * n)) = 1 by NEWTON: 4;

 hence thesis;

 end;

 suppose |.a.| = 1;

 then a = 1 or ( - a) = 1 by ABSVALUE: 1;

 hence thesis;

 end;

 end;

 end

 registration

 let a be non light Complex, n be Nat;

 cluster (a |^ n) -> non light;

 coherence

 proof

 per cases ;

 suppose n is zero;

 hence thesis by NEWTON: 4;

 end;

 suppose not n is zero;

 then

 reconsider n as non zero Nat;

 defpred P[ Nat] means (a |^ ($1 + 1)) is non light;



 A1: P[ 0 ];



 A2: for k be Nat holds P[k] implies P[(k + 1)]

 proof

 let k be Nat;

 assume (a |^ (k + 1)) is non light;

 then (a * (a |^ (k + 1))) is non light;

 hence thesis by NEWTON: 6;

 end;



 A3: for l be Nat holds P[l] from NAT_1:sch 2( A1, A2);

 reconsider m = (n - 1) as Nat;

 (a |^ (m + 1)) is non light by A3;

 hence thesis;

 end;

 end;

 end

 registration

 let a be non light Real, n be Nat;

 cluster ((a |^ (2 * n)) - 1) -> non negative;

 coherence

 proof

 |.(a |^ (2 * n)).| >= 1 by TA1;

 hence thesis;

 end;

 end

 registration

 let a be light Complex, n be non zero Nat;

 cluster (a |^ n) -> light;

 coherence

 proof

 defpred P[ Nat] means (a |^ ($1 + 1)) is light;



 A1: P[ 0 ];



 A2: for k be Nat holds P[k] implies P[(k + 1)]

 proof

 let k be Nat;

 assume (a |^ (k + 1)) is light;

 then (a * (a |^ (k + 1))) is light;

 hence thesis by NEWTON: 6;

 end;



 A3: for l be Nat holds P[l] from NAT_1:sch 2( A1, A2);

 reconsider m = (n - 1) as Nat;

 (a |^ (m + 1)) is light by A3;

 hence thesis;

 end;

 cluster (n -root a) -> light;

 coherence

 proof

 assume not thesis;

 then not ((n -root a) |^ n) is light;

 hence contradiction by POLYEQ_5: 7;

 end;

 end

 registration

 let a be light Real, n be non zero Nat;

 cluster ((a |^ (2 * n)) - 1) -> negative;

 coherence

 proof

 |.(a |^ (2 * n)).| < 1 by TA1;

 hence thesis;

 end;

 end

 registration

 let a be non heavy Complex, n be Nat;

 cluster (a |^ n) -> non heavy;

 coherence

 proof

 per cases by Th1;

 suppose a is weightless;

 hence thesis;

 end;

 suppose a is light;

 then (a |^ n) is light or n = 0 ;

 then (a |^ n) is light or (a |^ n) = 1 by NEWTON: 4;

 hence thesis;

 end;

 end;

 end

 registration

 let a be non heavy Real, n be Nat;

 cluster ((a |^ (2 * n)) - 1) -> non positive;

 coherence

 proof

 |.(a |^ (2 * n)).| <= 1 by TA1;

 hence thesis;

 end;

 end

 registration

 let a be heavy Complex, n be non zero Nat;

 cluster (a |^ n) -> heavy;

 coherence

 proof

 defpred P[ Nat] means (a |^ ($1 + 1)) is heavy;



 A1: P[ 0 ];



 A2: for k be Nat holds P[k] implies P[(k + 1)]

 proof

 let k be Nat;

 (a * (a |^ (k + 1))) is heavy;

 hence thesis by NEWTON: 6;

 end;



 A3: for l be Nat holds P[l] from NAT_1:sch 2( A1, A2);

 reconsider m = (n - 1) as Nat;

 (a |^ (m + 1)) is heavy by A3;

 hence thesis;

 end;

 cluster (n -root a) -> heavy;

 coherence

 proof

 assume not thesis;

 then not ((n -root a) |^ n) is heavy;

 hence contradiction by POLYEQ_5: 7;

 end;

 end

 registration

 let a be non weightless Complex, n be non zero Nat;

 cluster (a |^ n) -> non weightless;

 coherence

 proof

 reconsider b = |.a.| as positive Real;

 |.a.| <> 1 implies |.a.| > 1 or |.a.| < 1 by XXREAL_0: 1;

 then ( |.a.| |^ n) <> (1 * ( 0 |^ n)) & ( |.a.| |^ n) <> (1 |^ n) by Def3, NEWTON02: 40;

 hence thesis by TAYLOR21;

 end;

 end

 registration

 let a be weightless Complex, n be non zero Nat;

 cluster (n -root a) -> weightless;

 coherence

 proof

 assume not thesis;

 then not ((n -root a) |^ n) is weightless;

 hence contradiction by POLYEQ_5: 7;

 end;

 end

 registration

 let a be non weightless Complex, n be non zero Nat;

 cluster (n -root a) -> non weightless;

 coherence

 proof

 assume not thesis;

 then ((n -root a) |^ n) is weightless;

 hence contradiction by POLYEQ_5: 7;

 end;

 end

 registration

 let a be non light Complex, n be non zero Nat;

 cluster (n -root a) -> non light;

 coherence

 proof

 assume not thesis;

 then ((n -root a) |^ n) is light;

 hence contradiction by POLYEQ_5: 7;

 end;

 end

 registration

 let a be non heavy Complex, n be non zero Nat;

 cluster (n -root a) -> non heavy;

 coherence

 proof

 assume not thesis;

 then not ((n -root a) |^ n) is non heavy;

 hence contradiction by POLYEQ_5: 7;

 end;

 end

 registration

 let a,b be weightless Complex;

 cluster (a / b) -> weightless;

 coherence ;

 end

 registration

 let a be non heavy Complex, b be heavy Complex;

 cluster (a / b) -> light;

 coherence ;

 end

 registration

 let a be light Complex, b be non light Complex;

 cluster (a / b) -> light;

 coherence ;

 end

 registration

 let a be non light Complex, b be non zero light Complex;

 cluster (a / b) -> heavy;

 coherence ;

 end

 registration

 let a be heavy Complex, b be non zero non heavy Complex;

 cluster (a / b) -> heavy;

 coherence ;

 end

 registration

 let a be heavy positive Real, b be non negative Real;

 cluster (a + b) -> heavy;

 coherence

 proof

 (a + b) > (1 + 0 ) by TA1, XREAL_1: 8;

 hence thesis;

 end;

 end

 registration

 let a be heavy negative Real, b be non positive Real;

 cluster (a + b) -> heavy;

 coherence

 proof

 (( - a) + ( - b)) is heavy;

 then ( - ( - (a + b))) is heavy;

 hence thesis;

 end;

 end

 registration

 let a be non light positive Real, b be positive Real;

 cluster (a + b) -> heavy;

 coherence

 proof

 a >= 1 by TA1;

 then (a + b) > (1 + 0 ) by XREAL_1: 8;

 hence thesis;

 end;

 end

 registration

 let a be non light negative Real, b be negative Real;

 cluster (a + b) -> heavy;

 coherence

 proof

 (( - a) + ( - b)) is heavy;

 then ( - ( - (a + b))) is heavy;

 hence thesis;

 end;

 end

 registration

 let a be non heavy Real, b be heavy positive Real;

 cluster (a + b) -> positive;

 coherence

 proof

 a >= ( - 1) & b > 1 by TA1;

 then (a + b) > (( - 1) + 1) by XREAL_1: 8;

 hence thesis;

 end;

 end

 registration

 let a be light Real, b be non light positive Real;

 cluster (a + b) -> positive;

 coherence

 proof

 a > ( - 1) & b >= 1 by TA1;

 then (a + b) > (( - 1) + 1) by XREAL_1: 8;

 hence thesis;

 end;

 end

 registration

 let a be non heavy Real, b be non light positive Real;

 cluster (a + b) -> non negative;

 coherence

 proof

 a >= ( - 1) & b >= 1 by TA1;

 then (a + b) >= (( - 1) + 1) by XREAL_1: 7;

 hence thesis;

 end;

 end

 registration

 let a be non heavy Real, b be heavy negative Real;

 cluster (a + b) -> negative;

 coherence

 proof

 a <= 1 & b < ( - 1) by TA1;

 then (a + b) < (1 + ( - 1)) by XREAL_1: 8;

 then (a + b) < 0 ;

 hence thesis;

 end;

 end

 registration

 let a be light Real, b be non light negative Real;

 cluster (a + b) -> negative;

 coherence

 proof

 a < 1 & b <= ( - 1) by TA1;

 then (a + b) < (1 + ( - 1)) by XREAL_1: 8;

 then (a + b) < 0 ;

 hence thesis;

 end;

 end

 registration

 let a be non heavy Real, b be non light negative Real;

 cluster (a + b) -> non positive;

 coherence

 proof

 a <= 1 & b <= ( - 1) by TA1;

 then (a + b) <= (1 + ( - 1)) by XREAL_1: 7;

 then (a + b) <= 0 ;

 hence thesis;

 end;

 end

 registration

 let a be light positive Real, c be light negative Real;

 cluster (a + c) -> light;

 coherence

 proof

 reconsider b = ( - c) as light positive Real;



 A2: |.b.| < 1 by Def2;

 |.a.| < 1 by Def2;

 then (a - b) < (1 - b) & (1 - b) <= (1 - 0 ) by XREAL_1: 9, XREAL_1: 10;

 then

 A3: (a - b) < 1 by XXREAL_0: 2;



 A4: (b - a) < (1 - a) & (1 - a) <= (1 - 0 ) by A2, XREAL_1: 9, XREAL_1: 10;

 per cases ;

 suppose (a - b) >= 0 ;

 hence thesis by A3, ABSVALUE:def 1;

 end;

 suppose (a - b) < 0 ;

 then |.(a - b).| = ( - (a - b)) by ABSVALUE:def 1;

 hence thesis by A4, XXREAL_0: 2;

 end;

 end;

 end

 registration

 let a be non heavy positive Real, c be non heavy negative Real;

 cluster (a + c) -> non heavy;

 coherence

 proof

 reconsider b = ( - c) as non heavy positive Real;



 A1: |.a.| <= 1 by Def1;



 A2: |.b.| <= 1 by Def1;

 (a - b) <= (1 - b) & (1 - b) <= (1 - 0 ) by A1, XREAL_1: 9, XREAL_1: 10;

 then

 A3: (a - b) <= 1 by XXREAL_0: 2;



 A4: (b - a) <= (1 - a) & (1 - a) <= (1 - 0 ) by A2, XREAL_1: 9, XREAL_1: 10;

 per cases ;

 suppose (a - b) >= 0 ;

 hence thesis by A3, ABSVALUE:def 1;

 end;

 suppose (a - b) < 0 ;

 then |.(a - b).| = ( - (a - b)) by ABSVALUE:def 1;

 hence thesis by A4, XXREAL_0: 2;

 end;

 end;

 end

 registration

 let a,b be Real;

 cluster (a - ( min (a,b))) -> non negative;

 coherence

 proof

 (a - ( min (a,b))) >= (( min (a,b)) - ( min (a,b))) by XREAL_1: 9, XXREAL_0: 17;

 hence thesis;

 end;

 end

 registration

 let a,b be weightless Real;

 cluster ( min (a,b)) -> weightless;

 coherence by XXREAL_0:def 9;

 cluster ( max (a,b)) -> weightless;

 coherence by XXREAL_0:def 10;

 end

 registration

 let a,b be light Real;

 cluster ( min (a,b)) -> light;

 coherence by XXREAL_0:def 9;

 cluster ( max (a,b)) -> light;

 coherence by XXREAL_0:def 10;

 end

 registration

 let a,b be heavy Real;

 cluster ( min (a,b)) -> heavy;

 coherence by XXREAL_0:def 9;

 cluster ( max (a,b)) -> heavy;

 coherence by XXREAL_0:def 10;

 end

 registration

 let a,b be positive Real;

 cluster (( min (a,b)) / ( max (a,b))) -> non heavy;

 coherence

 proof

 reconsider c = ( max (a,b)) as positive Real;

 ( max (a,b)) >= a & a >= ( min (a,b)) by XXREAL_0: 17, XXREAL_0: 25;

 then ( max (a,b)) >= ( min (a,b)) by XXREAL_0: 2;

 then (( min (a,b)) / c) <= ((1 * c) / c) by XREAL_1: 72;

 hence thesis by XCMPLX_1: 89;

 end;

 cluster (( max (a,b)) / ( min (a,b))) -> non light;

 coherence

 proof

 (( min (a,b)) / ( max (a,b))) is non heavy;

 then ((( max (a,b)) / ( min (a,b))) " ) is non heavy by XCMPLX_1: 213;

 hence thesis;

 end;

 cluster ((a + b) / a) -> heavy;

 coherence

 proof

 (a + b) > (a + 0 ) by XREAL_1: 6;

 then ((a + b) / a) > ((1 * a) / a) by XREAL_1: 74;

 hence thesis by XCMPLX_1: 89;

 end;

 cluster (a / (a + b)) -> light;

 coherence

 proof

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

 then ((a / (a + b)) " ) is heavy by XCMPLX_1: 213;

 hence thesis;

 end;

 end

 theorem :: COMPLEX3:15



 MP: for a,b be Real st (a * b) is positive holds |.(a - b).| < |.(a + b).|

 proof

 let a,b be Real such that

 A1: (a * b) is positive;



 A2: |.(a - b).| = (a - b) or |.(a - b).| = ( - (a - b)) by ABSVALUE:def 1;

 per cases ;

 suppose a = 0 ;

 hence thesis by A1;

 end;

 suppose

 B1: a > 0 ;

 then b > 0 by A1;

 then ((a - b) + (2 * b)) > ((a - b) + 0 ) & ((b - a) + (2 * a)) > ((b - a) + 0 ) by B1, XREAL_1: 6;

 hence thesis by A2, ABSVALUE:def 1;

 end;

 suppose

 B1: a < 0 ;

 then

 B2: b < 0 by A1;

 then ((a - b) + (2 * b)) < ((a - b) + 0 ) & ((b - a) + (2 * a)) < ((b - a) + 0 ) by B1, XREAL_1: 6;

 then ( - (a + b)) > ( - (a - b)) & ( - (a + b)) > ( - (b - a)) by XREAL_1: 24;

 hence thesis by B1, B2, A2, ABSVALUE:def 1;

 end;

 end;

 theorem :: COMPLEX3:16

 for a,b be Real st (a * b) is negative holds |.(a - b).| > |.(a + b).|

 proof

 let a,b be Real such that

 A1: (a * b) is negative;



 A2: |.(a - b).| = (a - b) or |.(a - b).| = ( - (a - b)) by ABSVALUE:def 1;

 per cases ;

 suppose a = 0 ;

 hence thesis by A1;

 end;

 suppose

 B1: a > 0 ;

 then

 B2: b < 0 by A1;

 then ((a - b) + (2 * b)) < ((a - b) + 0 ) & (( - (a - b)) + (2 * a)) > (( - (a - b)) + 0 ) by B1, XREAL_1: 6;

 then (a + b) < (a - b) & ( - (a + b)) < ( - ( - (a - b))) by XREAL_1: 24;

 hence thesis by B1, B2, A2, ABSVALUE:def 1;

 end;

 suppose

 B1: a < 0 ;

 then

 B2: b > 0 by A1;

 then ((a - b) + (2 * b)) > ((a - b) + 0 ) & ((b - a) + (2 * a)) < ((b - a) + 0 ) by B1, XREAL_1: 6;

 then ( - (a + b)) < ( - (a - b)) & (a + b) < (b - a) by XREAL_1: 24;

 hence thesis by B1, B2, A2, ABSVALUE:def 1;

 end;

 end;

 theorem :: COMPLEX3:17

 for a,b be non zero Real holds |.((a |^ 2) - (b |^ 2)).| < |.((a |^ 2) + (b |^ 2)).|

 proof

 let a,b be non zero Real;

 reconsider c = (a |^ (2 * 1)) as positive Real;

 reconsider d = (b |^ (2 * 1)) as positive Real;

 (c * d) > 0 ;

 hence thesis by MP;

 end;

 theorem :: COMPLEX3:18

 for a,b,c be positive Real st a = 1

 proof

 let a,b be positive Real;



 A1: ((a * a) / (a * b)) = (a / b) & ((b * b) / (a * b)) = (b / a) by XCMPLX_1: 91;

 ((a - b) * (a - b)) is non negative;

 then ((((a * a) - ((2 * a) * b)) + (b * b)) + ((2 * a) * b)) >= ( 0 + ((2 * a) * b)) by XREAL_1: 6;

 then (((a * a) + (b * b)) / ((2 * a) * b)) >= (((2 * a) * b) / ((2 * a) * b)) by XREAL_1: 72;

 then (((a * a) + (b * b)) / (2 * (a * b))) >= 1 by XCMPLX_1: 60;

 then ((((a * a) + (b * b)) / (a * b)) / 2) >= 1 by XCMPLX_1: 78;

 hence thesis by A1;

 end;

 theorem :: COMPLEX3:20



 NN1: for a,b be negative Real holds (((a / b) + (b / a)) / 2) >= 1

 proof

 let a,b be negative Real;



 A1: ((a * a) / (a * b)) = (a / b) & ((b * b) / (a * b)) = (b / a) by XCMPLX_1: 91;

 ((a - b) * (a - b)) is non negative;

 then ((((a * a) - ((2 * a) * b)) + (b * b)) + ((2 * a) * b)) >= ( 0 + ((2 * a) * b)) by XREAL_1: 6;

 then (((a * a) + (b * b)) / ((2 * a) * b)) >= (((2 * a) * b) / ((2 * a) * b)) by XREAL_1: 72;

 then (((a * a) + (b * b)) / (2 * (a * b))) >= 1 by XCMPLX_1: 60;

 then ((((a * a) + (b * b)) / (a * b)) / 2) >= 1 by XCMPLX_1: 78;

 hence thesis by A1;

 end;

 theorem :: COMPLEX3:21



 NP1: for a be negative Real, b be positive Real holds (((a / b) + (b / a)) / 2) <= ( - 1)

 proof

 let a be negative Real, b be positive Real;



 A1: ((a * a) / (a * b)) = (a / b) & ((b * b) / (a * b)) = (b / a) by XCMPLX_1: 91;

 ((a + b) * (a + b)) is non negative;

 then ((((a * a) + ((2 * a) * b)) + (b * b)) - ((2 * a) * b)) >= ( 0 - ((2 * a) * b)) by XREAL_1: 6;

 then (((a * a) + (b * b)) / ((2 * a) * b)) <= (( - ((2 * a) * b)) / ((2 * a) * b)) by XREAL_1: 73;

 then (((a * a) + (b * b)) / ((2 * a) * b)) <= ( - (((2 * a) * b) / ((2 * a) * b)));

 then (((a * a) + (b * b)) / (2 * (a * b))) <= ( - 1) by XCMPLX_1: 60;

 then ((((a * a) + (b * b)) / (a * b)) / 2) <= ( - 1) by XCMPLX_1: 78;

 hence thesis by A1;

 end;

 registration

 let a,b be non zero Real;

 cluster (((a / b) + (b / a)) / 2) -> non light;

 coherence

 proof

 per cases ;

 suppose a is positive & b is positive;

 hence thesis by PP1, TA1;

 end;

 suppose a is negative & b is negative;

 hence thesis by NN1, TA1;

 end;

 suppose a is positive & b is negative;

 hence thesis by NP1, TA1;

 end;

 suppose a is negative & b is positive;

 hence thesis by NP1, TA1;

 end;

 end;

 cluster ((a / b) + (b / a)) -> heavy;

 coherence

 proof

 2 is heavy & (((a / b) + (b / a)) / 2) is non light;

 hence thesis;

 end;

 end

 theorem :: COMPLEX3:22

 for a,b be non zero Real holds (((a / b) + (b / a)) |^ 2) >= 4

 proof

 let a,b be non zero Real;

 ((((a / b) + (b / a)) / 2) |^ (2 * 1)) >= 1 by TA1;

 then (((((a / b) + (b / a)) / 2) |^ 2) * 4) >= (1 * 4) by XREAL_1: 64;

 then (((((a / b) + (b / a)) |^ 2) / (2 |^ 2)) * (2 * 2)) >= 4 by PREPOWER: 8;

 then (((((a / b) + (b / a)) |^ 2) / (2 |^ 2)) * (2 |^ 2)) >= 4 by NEWTON: 81;

 hence thesis by XCMPLX_1: 87;

 end;

 registration

 let a,b be positive Real;

 cluster (((a + (2 * b)) * a) / ((a + b) |^ 2)) -> non heavy;

 coherence

 proof

 reconsider c = (a + b) as positive Real;

 reconsider d = (a + (2 * b)) as positive Real;

 (a + b) > (a + 0 ) by XREAL_1: 6;

 then (a / (a + b)) <= ((a + b) / ((a + b) + b)) by SERIES_3: 1;

 then ((d / c) * (a / c)) <= ((d / c) * (c / d)) by XREAL_1: 64;

 then ((d / c) * (a / c)) <= 1 by XCMPLX_1: 112;

 then ((d * a) / (c * c)) <= 1 by XCMPLX_1: 76;

 hence thesis by NEWTON: 81;

 end;

 cluster (((b / a) + (a / b)) - 1) -> non light;

 coherence

 proof

 (((b / a) + (a / b)) - 1) >= (2 - 1) by SERIES_3: 3, XREAL_1: 9;

 hence thesis;

 end;

 cluster (((a + b) * ((a " ) + (b " ))) / 4) -> non light;

 coherence

 proof

 (1 / a) = (a " ) & (1 / b) = (b " );

 then (((a + b) * ((a " ) + (b " ))) / 4) >= ((1 * 4) / 4) by XREAL_1: 72, SERIES_5: 1;

 hence thesis;

 end;

 end

 registration

 let a,b be light Real;

 cluster ((a + b) / (1 + (a * b))) -> non heavy;

 coherence

 proof

 |.a.| < 1 & |.b.| < 1 by Def2;

 hence thesis by SERIES_5: 13;

 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 by SERIES_5: 15;

 end

 registration

 let a be non negative Real;

 reduce |.( - a).| to a;

 reducibility

 proof

 |.( - a).| = ( - ( - a)) by ABSVALUE: 30;

 hence thesis;

 end;

 end

 registration

 cluster trivial non zero for Nat;

 existence

 proof

 1 is trivial & 1 <> 0 ;

 hence thesis;

 end;

 cluster trivial for Nat;

 existence

 proof

 1 is trivial;

 hence thesis;

 end;

 end

 registration

 let a,b be non zero Real;

 cluster ( min (a,b)) -> non zero;

 coherence by XXREAL_0:def 9;

 cluster ( max (a,b)) -> non zero;

 coherence by XXREAL_0:def 10;

 end

 registration

 let a be non negative Real, b be Real;

 cluster ( max (a,b)) -> non negative;

 coherence by XXREAL_0: 25;

 end

 registration

 let a be non positive Real, b be Real;

 cluster ( min (a,b)) -> non positive;

 coherence by XXREAL_0: 17;

 end

 registration

 let a be positive Real, b be Real;

 cluster ( max (a,b)) -> positive;

 coherence by XXREAL_0: 25;

 end

 registration

 let a be negative Real, b be Real;

 cluster ( min (a,b)) -> negative;

 coherence by XXREAL_0: 17;

 end

 registration

 let a,b be non negative Real;

 cluster ( min (a,b)) -> non negative;

 coherence by XXREAL_0:def 9;

 end

 registration

 let a,b be non positive Real;

 cluster ( max (a,b)) -> non positive;

 coherence by XXREAL_0:def 10;

 end

 registration

 let a be positive Real, b be non negative Real;

 cluster (a / (a + b)) -> non heavy;

 coherence

 proof

 (a + b) >= (a + 0 ) by XREAL_1: 6;

 hence thesis by XREAL_1: 185;

 end;

 cluster ((a + b) / a) -> non light;

 coherence

 proof

 ((a / (a + b)) " ) is non light;

 hence thesis by XCMPLX_1: 213;

 end;

 end

 registration

 let a,b be positive Real;

 cluster (a / ( max (a,b))) -> non heavy;

 coherence

 proof

 reconsider c = (( max (a,b)) - a) as non negative Real;

 (a / (a + c)) is non heavy;

 hence thesis;

 end;

 cluster (a / ( min (a,b))) -> non light;

 coherence

 proof

 reconsider c = (a - ( min (a,b))) as non negative Real;

 ((( min (a,b)) + c) / ( min (a,b))) is non light;

 hence thesis;

 end;

 end

 theorem :: COMPLEX3:23

 for a,b be Real st ( sgn a) > ( sgn b) holds a > b

 proof

 let a,b be Real;

 assume

 A1: ( sgn a) > ( sgn b);

 a > 0 or a = 0 or a < 0 ;

 then

 A2: ( sgn a) = 1 or ( sgn a) = 0 or ( sgn a) = ( - 1) by ABSVALUE:def 2;

 b > 0 or b = 0 or b < 0 ;

 hence thesis by A1, A2, ABSVALUE:def 2;

 end;

 theorem :: COMPLEX3:24



 SGNZ: for a,b be non zero Real st ( sgn a) > ( sgn b) holds a is positive & b is negative

 proof

 let a,b be non zero Real;

 assume

 A1: ( sgn a) > ( sgn b);

 (a > 0 or a < 0 ) & (b > 0 or b < 0 );

 then (( sgn a) = 1 or ( sgn a) = ( - 1)) & (( sgn b) = 1 or ( sgn b) = ( - 1)) by ABSVALUE:def 2;

 hence thesis by A1;

 end;

 registration

 let a,b be Real;

 cluster (( max (a,b)) - ( min (a,b))) -> non negative;

 coherence

 proof

 ( max (a,b)) >= a >= ( min (a,b)) by XXREAL_0: 17, XXREAL_0: 25;

 then ( max (a,b)) >= ( min (a,b)) by XXREAL_0: 2;

 then (( max (a,b)) - ( min (a,b))) >= (( min (a,b)) - ( min (a,b))) by XREAL_1: 9;

 hence thesis;

 end;

 reduce (( sgn (a - b)) * (( max (a,b)) - ( min (a,b)))) to (a - b);

 reducibility

 proof

 per cases by XXREAL_0: 1;

 suppose a = b;

 hence thesis;

 end;

 suppose

 B1: a > b;

 then

 B2: ( max (a,b)) = a & ( min (a,b)) = b by XXREAL_0:def 9, XXREAL_0:def 10;

 (a - b) > (b - b) by B1, XREAL_1: 9;

 then ( sgn (a - b)) = 1 by ABSVALUE:def 2;

 hence thesis by B2;

 end;

 suppose

 B1: a < b;

 then

 B2: ( max (a,b)) = b & ( min (a,b)) = a by XXREAL_0:def 9, XXREAL_0:def 10;

 (a - b) < (b - b) by B1, XREAL_1: 9;

 then ( sgn (a - b)) = ( - 1) by ABSVALUE:def 2;

 hence thesis by B2;

 end;

 end;

 end

 registration

 let a be Real;

 reduce (a to_power 1) to a;

 reducibility ;

 reduce (1 to_power a) to 1;

 reducibility by POWER: 26;

 cluster (a to_power 0 ) -> natural;

 coherence by POWER: 24;

 cluster (a to_power 0 ) -> weightless;

 coherence by POWER: 24;

 end

 registration

 let a be positive Real, b be Real;

 cluster (a to_power b) -> positive;

 coherence by POWER: 34;

 end

 registration

 let a be weightless positive Real, b be positive Real;

 reduce (b to_power a) to b;

 reducibility

 proof

 a = 1 by TA1;

 hence thesis;

 end;

 end

 registration

 let a be heavy positive Real, b be positive Real;

 cluster (a to_power b) -> heavy;

 coherence by TA1, POWER: 35;

 end

 registration

 let a be heavy positive Real, b be negative Real;

 cluster (a to_power b) -> light;

 coherence

 proof

 a > 1 & b < 0 by TA1;

 hence thesis by POWER: 36;

 end;

 end

 registration

 let a be light positive Real, b be positive Real;

 cluster (a to_power b) -> light;

 coherence

 proof

 ((1 / a) to_power ( - b)) is light positive;

 then (a to_power ( - ( - b))) is light by POWER: 32;

 hence thesis;

 end;

 end

 registration

 let a be light positive Real, b be negative Real;

 cluster (a to_power b) -> heavy;

 coherence

 proof

 ((1 / a) to_power ( - b)) is heavy positive;

 then (a to_power ( - ( - b))) is heavy by POWER: 32;

 hence thesis;

 end;

 end

 registration

 let a be non weightless positive Real, b be Real;

 reduce ( log (a,(a to_power b))) to b;

 reducibility

 proof

 |.a.| <> 1 & (a to_power b) > 0 by TA1;

 hence thesis by POWER:def 3;

 end;

 end

 registration

 let a be non weightless positive Real, b be positive Real;

 reduce (a to_power ( log (a,b))) to b;

 reducibility

 proof

 |.a.| <> 1 by TA1;

 hence thesis by POWER:def 3;

 end;

 end

 theorem :: COMPLEX3:25



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

 theorem :: COMPLEX3:26



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

 theorem :: COMPLEX3:27

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

 theorem :: COMPLEX3:28

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

 theorem :: COMPLEX3:29



 OPR: for a,b be positive Real holds ( sgn ((1 / a) - (1 / b))) = ( sgn (b - a))

 proof

 let a,b be positive Real;



 A1: ( sgn (a * b)) = 1 by ABSVALUE:def 2;

 (((1 / a) * a) * b) = ((1 / a) * (a * b)) & ((1 / b) * (a * b)) = (((1 / b) * b) * a) & ((1 / b) * b) = 1 & ((1 / a) * a) = 1 by XCMPLX_1: 87;

 then ((1 / a) * (a * b)) = b & ((1 / b) * (a * b)) = a;



 then ( sgn (b - a)) = ( sgn (((1 / a) - (1 / b)) * (a * b)))

 .= (( sgn ((1 / a) - (1 / b))) * ( sgn (a * b))) by ABSVALUE: 18;

 hence thesis by A1;

 end;

 theorem :: COMPLEX3:30



 NPR: for a,b be negative Real holds ( sgn ((1 / a) - (1 / b))) = ( sgn (b - a))

 proof

 let a,b be negative Real;



 A1: ( sgn (a * b)) = 1 by ABSVALUE:def 2;

 (((1 / a) * a) * b) = ((1 / a) * (a * b)) & ((1 / b) * (a * b)) = (((1 / b) * b) * a) & ((1 / b) * b) = 1 & ((1 / a) * a) = 1 by XCMPLX_1: 87;

 then ((1 / a) * (a * b)) = b & ((1 / b) * (a * b)) = a;



 then ( sgn (b - a)) = ( sgn (((1 / a) - (1 / b)) * (a * b)))

 .= (( sgn ((1 / a) - (1 / b))) * ( sgn (a * b))) by ABSVALUE: 18;

 hence thesis by A1;

 end;

 theorem :: COMPLEX3:31

 for a,b be non zero Real holds ( sgn ((1 / a) - (1 / b))) = ( sgn (b - a)) iff ( sgn b) = ( sgn a)

 proof

 let a,b be non zero Real;



 A1: ( sgn b) = ( sgn a) implies ( sgn ((1 / a) - (1 / b))) = ( sgn (b - a))

 proof

 assume ( sgn a) = ( sgn b);

 then (a is positive & b is positive) or (a is negative & b is negative);

 hence thesis by OPR, NPR;

 end;

 ( sgn b) <> ( sgn a) implies ( sgn ((1 / a) - (1 / b))) <> ( sgn (b - a))

 proof

 assume ( sgn b) <> ( sgn a);

 per cases by XXREAL_0: 1;

 suppose ( sgn b) > ( sgn a);

 then b is positive & a is negative by SGNZ;

 hence thesis;

 end;

 suppose ( sgn b) < ( sgn a);

 then b is negative & a is positive by SGNZ;

 hence thesis;

 end;

 end;

 hence thesis by A1;

 end;

 theorem :: COMPLEX3:32



 SIO: for a,b be non zero Real holds (a + b) = (a * b) iff ((1 / a) + (1 / b)) = 1

 proof

 let a,b be non zero Real;

 ((1 * a) / (a * b)) = (1 / b) & ((1 * b) / (a * b)) = (1 / a) by XCMPLX_1: 91;



 then (((1 / a) + (1 / b)) * (a * b)) = (((a + b) / (a * b)) * (a * b))

 .= (a + b) by XCMPLX_1: 87;

 hence thesis by XCMPLX_1: 7;

 end;

 theorem :: COMPLEX3:33



 SIL: for a,b be positive Real holds (a + b) > (a * b) iff ((1 / a) + (1 / b)) > 1

 proof

 let a,b be positive Real;



 A1: ((1 * a) / (a * b)) = (1 / b) & ((1 * b) / (a * b)) = (1 / a) by XCMPLX_1: 91;



 A2: (a + b) > (a * b) implies ((1 / a) + (1 / b)) > 1

 proof

 assume (a + b) > (a * b);

 then ((a + b) / (a * b)) > ((a * b) / (a * b)) by XREAL_1: 74;

 hence thesis by XCMPLX_1: 60, A1;

 end;

 ((1 / a) + (1 / b)) > 1 implies (a + b) > (a * b)

 proof

 assume ((1 / a) + (1 / b)) > 1;

 then ((a + b) / (a * b)) > ((a * b) / (a * b)) by A1, XCMPLX_1: 60;

 hence thesis by XREAL_1: 72;

 end;

 hence thesis by A2;

 end;

 theorem :: COMPLEX3:34

 for a,b be positive Real holds (a + b) < (a * b) iff ((1 / a) + (1 / b)) < 1

 proof

 let a,b be positive Real;

 thus (a + b) < (a * b) implies ((1 / a) + (1 / b)) < 1

 proof

 (a + b) < (a * b) implies ((1 / a) + (1 / b)) <= 1 & ((1 / a) + (1 / b)) <> 1 by SIO, SIL;

 hence thesis by XXREAL_0: 1;

 end;

 ((1 / a) + (1 / b)) < 1 implies (a + b) <= (a * b) & (a + b) <> (a * b) by SIO, SIL;

 hence thesis by XXREAL_0: 1;

 end;

 theorem :: COMPLEX3:35

 for a be non heavy positive Real, b be positive Real holds (a + b) > (a * b)

 proof

 let a be non heavy positive Real, b be positive Real;

 ((1 / a) + (1 / b)) is heavy positive;

 hence thesis by SIL;

 end;

 theorem :: COMPLEX3:36



 DIO: for a,b be non zero Real holds (a - b) = (a * b) iff ((1 / b) - (1 / a)) = 1

 proof

 let a,b be non zero Real;

 ((1 * a) / (a * b)) = (1 / b) & ((1 * b) / (a * b)) = (1 / a) by XCMPLX_1: 91;



 then (((1 / b) - (1 / a)) * (a * b)) = (((a - b) / (a * b)) * (a * b))

 .= (a - b) by XCMPLX_1: 87;

 hence thesis by XCMPLX_1: 7;

 end;

 theorem :: COMPLEX3:37

 for a,b be positive Real holds (a - b) = (a * b) implies b is light

 proof

 let a,b be positive Real;

 b is non light implies ((1 / b) - (1 / a)) < 1

 proof

 assume b is non light;

 then (1 / b) <= 1 by TA1;

 then

 A1: ((1 / b) - (1 / a)) <= (1 - (1 / a)) by XREAL_1: 9;

 (1 - (1 / a)) < (1 - 0 ) by XREAL_1: 15;

 hence thesis by A1, XXREAL_0: 2;

 end;

 hence thesis by DIO;

 end;

 theorem :: COMPLEX3:38



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

 proof

 let a,b,c,d be positive Real such that

 A1: (a + b) = (c + d);

 ((( max (a,b)) = a & ( min (a,b)) = b) or (( max (a,b)) = b & ( min (a,b)) = a)) & ((( max (c,d)) = c & ( min (c,d)) = d) or (( max (c,d)) = d & ( min (c,d)) = c)) by XXREAL_0:def 9, XXREAL_0:def 10;

 hence thesis by A1;

 end;

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

 proof

 let a,b,c,d be positive Real such that

 A1: (a + b) = (c + d);

 ((( max (a,b)) = a & ( min (a,b)) = b) or (( max (a,b)) = b & ( min (a,b)) = a)) & ((( max (c,d)) = c & ( min (c,d)) = d) or (( max (c,d)) = d & ( min (c,d)) = c)) by XXREAL_0:def 9, XXREAL_0:def 10;

 hence thesis by A1;

 end;

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

 proof

 let a,b,c,d be positive Real such that

 A1: (a + b) = (c + d);

 reconsider k = (( max (a,b)) - ( max (c,d))) as Real;



 A2: k = (( min (c,d)) - ( min (a,b))) by A1, SAD;



 A3: ( max (a,b)) > ( max (c,d)) implies ( min (a,b)) < ( min (c,d))

 proof

 assume ( max (a,b)) > ( max (c,d));

 then (( max (a,b)) - ( max (c,d))) > (( max (c,d)) - ( max (c,d))) by XREAL_1: 9;

 then (k + ( min (a,b))) > ( 0 + ( min (a,b))) by XREAL_1: 6;

 hence thesis by A2;

 end;

 ( max (a,b)) <= ( max (c,d)) implies ( min (a,b)) >= ( min (c,d))

 proof

 assume ( max (a,b)) <= ( max (c,d));

 then (( max (a,b)) - ( max (c,d))) <= (( max (c,d)) - ( max (c,d))) by XREAL_1: 9;

 then (k + ( min (a,b))) <= ( 0 + ( min (a,b))) by XREAL_1: 6;

 hence thesis by A2;

 end;

 hence thesis by A3;

 end;

 theorem :: COMPLEX3:41



 ISM: for a,b,c,d be positive Real st ((a + b) = (c + d) & (a * b) = (c * d)) holds ( max (a,b)) = ( max (c,d))

 proof

 let a,b,c,d be positive Real such that

 A1: (a + b) = (c + d) & (a * b) = (c * d);

 reconsider x = ( max (a,b)) as positive Real;

 reconsider y = ( min (a,b)) as positive Real;

 reconsider z = ( max (c,d)) as positive Real;

 reconsider t = ( min (c,d)) as positive Real;

 ((( max (a,b)) = a & ( min (a,b)) = b) or (( max (a,b)) = b & ( min (a,b)) = a)) & ((( max (c,d)) = c & ( min (c,d)) = d) or (( max (c,d)) = d & ( min (c,d)) = c)) by XXREAL_0:def 9, XXREAL_0:def 10;

 then (x * ((z + t) - x)) = (z * ((x + y) - z)) by A1;

 then

 A3: (x * (x - t)) = (z * (z - y));



 A4: (x - z) = (t - y) by A1, SAD;

 then (x - t) = 0 or x = z by A3, XCMPLX_1: 5;

 per cases ;

 suppose x = z;

 hence thesis;

 end;

 suppose

 B1: x = t;

 x >= a & a >= y & z >= c & c >= t by XXREAL_0: 17, XXREAL_0: 25;

 then x >= y & z >= t by XXREAL_0: 2;

 hence thesis by B1, A4, XXREAL_0: 1;

 end;

 end;

 theorem :: COMPLEX3:42



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

 proof

 let a,b,c,d be positive Real, n be Real such that

 A1: (a + b) = (c + d) & (a * b) = (c * d);



 A2: ( max (a,b)) = ( max (c,d)) by A1, ISM;

 ((( max (a,b)) = a & ( min (a,b)) = b) or (( max (a,b)) = b & ( min (a,b)) = a)) & ((( max (c,d)) = c & ( min (c,d)) = d) or (( max (c,d)) = d & ( min (c,d)) = c)) by XXREAL_0:def 9, XXREAL_0:def 10;

 hence thesis by A1, A2;

 end;

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

 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)

 proof

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

 assume

 A1: (a + b) = (c + d);

 (((1 / a) * a) * b) = (1 * b) & (((1 / b) * b) * a) = (1 * a) & (((1 / c) * c) * d) = (1 * d) & (((1 / d) * d) * c) = (1 * c) by XCMPLX_1: 87;

 then (a + b) = (((1 / a) + (1 / b)) * (a * b)) & (c + d) = (((1 / c) + (1 / d)) * (c * d));

 hence thesis by A1, XCMPLX_1: 5;

 end;

 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)

 proof

 let a,b,c,d be positive Real such that

 A1: (a + b) = (c + d);

 (((1 / a) * a) * b) = (1 * b) & (((1 / b) * b) * a) = (1 * a) & (((1 / c) * c) * d) = (1 * d) & (((1 / d) * d) * c) = (1 * c) by XCMPLX_1: 87;

 then (a + b) = (((1 / a) + (1 / b)) * (a * b)) & (c + d) = (((1 / c) + (1 / d)) * (c * d));

 hence thesis by A1, XREAL_1: 98;

 end;

 theorem :: COMPLEX3:46



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

 proof

 let a,b,c,d be positive Real such that

 A1: (a + b) >= (c + d);

 (((1 / a) * a) * b) = (1 * b) & (((1 / b) * b) * a) = (1 * a) & (((1 / c) * c) * d) = (1 * d) & (((1 / d) * d) * c) = (1 * c) by XCMPLX_1: 87;

 then (a + b) = (((1 / a) + (1 / b)) * (a * b)) & (c + d) = (((1 / c) + (1 / d)) * (c * d));

 hence thesis by A1, XREAL_1: 98;

 end;

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

 theorem :: COMPLEX3:48



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

 proof

 let a,b,c,d be positive Real such that

 A1: (a + b) <= (c + d);

 (((1 / a) * a) * b) = (1 * b) & (((1 / b) * b) * a) = (1 * a) & (((1 / c) * c) * d) = (1 * d) & (((1 / d) * d) * c) = (1 * c) by XCMPLX_1: 87;

 then (a + b) = (((1 / a) + (1 / b)) * (a * b)) & (c + d) = (((1 / c) + (1 / d)) * (c * d));

 hence thesis by A1, XREAL_1: 98;

 end;

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

 theorem :: COMPLEX3:50



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

 proof

 let a,b be positive Real, n,m be Real;

 ((a to_power m) * (a to_power n)) = (a to_power (m + n)) & ((b to_power m) * (b to_power n)) = (b to_power (m + n)) by POWER: 27;

 hence thesis;

 end;

 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)

 proof

 let a,b be positive Real, n be Real;

 (a to_power 1) = a & (b to_power 1) = b;

 hence thesis by N158;

 end;

 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)

 proof

 let a,b be positive Real, n,m be positive Real;

 (((a to_power n) - (b to_power n)) * ((a to_power m) - (b to_power m))) >= 0

 proof

 per cases by XXREAL_0: 1;

 suppose a = b;

 hence thesis;

 end;

 suppose a > b;

 then (a to_power n) > (b to_power n) & (a to_power m) > (b to_power m) by POWER: 37;

 then ((a to_power n) - (b to_power n)) > ((b to_power n) - (b to_power n)) & ((a to_power m) - (b to_power m)) > ((b to_power m) - (b to_power m)) by XREAL_1: 9;

 hence thesis;

 end;

 suppose a < b;

 then (a to_power n) < (b to_power n) & (a to_power m) < (b to_power m) by POWER: 37;

 then ((a to_power n) - (b to_power n)) < ((b to_power n) - (b to_power n)) & ((a to_power m) - (b to_power m)) < ((b to_power m) - (b to_power m)) by XREAL_1: 9;

 hence thesis;

 end;

 end;

 then ((((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)))) >= ((((a to_power m) + (b to_power m)) * ((a to_power n) + (b to_power n))) + 0 ) by XREAL_1: 6;

 then (((((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) + (b to_power m)) * ((a to_power n) + (b to_power n))) / 2) by XREAL_1: 72;

 hence thesis by N158;

 end;

 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

 proof

 let a,b be positive Real, n,m be positive Real;

 a = b implies (((a to_power n) - (b to_power n)) * ((a to_power m) - (b to_power m))) = 0 ;

 then

 A1: a = b implies ((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))) + 0 ) / 2) by N158;

 a <> b implies (((a to_power n) - (b to_power n)) * ((a to_power m) - (b to_power m))) > 0

 proof

 assume a <> b;

 per cases by XXREAL_0: 1;

 suppose a > b;

 then (a to_power n) > (b to_power n) & (a to_power m) > (b to_power m) by POWER: 37;

 then ((a to_power n) - (b to_power n)) > ((b to_power n) - (b to_power n)) & ((a to_power m) - (b to_power m)) > ((b to_power m) - (b to_power m)) by XREAL_1: 9;

 hence thesis;

 end;

 suppose a < b;

 then (a to_power n) < (b to_power n) & (a to_power m) < (b to_power m) by POWER: 37;

 then ((a to_power n) - (b to_power n)) < ((b to_power n) - (b to_power n)) & ((a to_power m) - (b to_power m)) < ((b to_power m) - (b to_power m)) by XREAL_1: 9;

 hence thesis;

 end;

 end;

 then a <> b implies ((((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)))) > ((((a to_power m) + (b to_power m)) * ((a to_power n) + (b to_power n))) + 0 ) by XREAL_1: 6;

 then a <> b implies (((((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) + (b to_power m)) * ((a to_power n) + (b to_power n))) / 2) by XREAL_1: 68;

 hence thesis by A1, N158;

 end;

 theorem :: COMPLEX3:54



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

 proof

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



 A1: (a + b) = (( max (a,b)) + ( min (a,b))) & (c + d) = (( max (c,d)) + ( min (c,d))) & (a * b) = (( max (a,b)) * ( min (a,b))) & (( max (c,d)) * ( min (c,d))) = (c * d) by NEWTON04: 18;

 assume

 A2: (a + b) <= (c + d) & ( max (a,b)) > ( max (c,d));

 then

 A4: ((( max (a,b)) + ( min (a,b))) * (( max (a,b)) + ( min (a,b)))) <= ((( max (c,d)) + ( min (c,d))) * (( max (c,d)) + ( min (c,d)))) by A1, XREAL_1: 66;

 ( min (a,b)) < ( min (c,d)) by A1, A2, XREAL_1: 8;

 then (( max (a,b)) * ( max (a,b))) > (( max (c,d)) * ( max (c,d))) & (( min (a,b)) * ( min (a,b))) < (( min (c,d)) * ( min (c,d))) by A2, XREAL_1: 96;

 then ((( max (a,b)) * ( max (a,b))) - (( min (a,b)) * ( min (a,b)))) > ((( max (c,d)) * ( max (c,d))) - (( min (c,d)) * ( min (c,d)))) by XREAL_1: 14;

 then ((( max (a,b)) - ( min (a,b))) * (( max (a,b)) + ( min (a,b)))) > ((( max (c,d)) - ( min (c,d))) * (( max (c,d)) + ( min (c,d))));

 then (( max (a,b)) - ( min (a,b))) > (( max (c,d)) - ( min (c,d))) by A1, A2, XREAL_1: 66;

 then ((( max (a,b)) - ( min (a,b))) * (( max (a,b)) - ( min (a,b)))) > ((( max (c,d)) - ( min (c,d))) * (( max (c,d)) - ( min (c,d)))) by XREAL_1: 96;

 then (((( max (a,b)) + ( min (a,b))) * (( max (a,b)) + ( min (a,b)))) - ((( max (a,b)) - ( min (a,b))) * (( max (a,b)) - ( min (a,b))))) < (((( max (c,d)) + ( min (c,d))) * (( max (c,d)) + ( min (c,d)))) - ((( max (c,d)) - ( min (c,d))) * (( max (c,d)) - ( min (c,d))))) by A4, XREAL_1: 15;

 then (4 * (( max (a,b)) * ( min (a,b)))) < (4 * (( max (c,d)) * ( min (c,d))));

 hence thesis by A1, XREAL_1: 64;

 end;

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

 proof

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



 A1: (a + b) = (( max (a,b)) + ( min (a,b))) & (c + d) = (( max (c,d)) + ( min (c,d))) & (a * b) = (( max (a,b)) * ( min (a,b))) & (c * d) = (( max (c,d)) * ( min (c,d))) by NEWTON04: 18;

 assume

 A2: ((a + b) <= (c + d) & (a * b) > (c * d));

 then ( max (a,b)) <= ( max (c,d)) by SMI;

 per cases by XXREAL_0: 1;

 suppose

 B1: ( max (a,b)) = ( max (c,d));

 then ( min (a,b)) <= ( min (c,d)) by A1, A2, XREAL_1: 6;

 hence thesis by A2, B1, A1, XREAL_1: 64;

 end;

 suppose ( max (a,b)) < ( max (c,d));

 hence thesis by A1, A2, XREAL_1: 66;

 end;

 end;

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

 proof

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



 A1: (a + b) = (( max (a,b)) + ( min (a,b))) & (c + d) = (( max (c,d)) + ( min (c,d))) & (a * b) = (( max (a,b)) * ( min (a,b))) & (( max (c,d)) * ( min (c,d))) = (c * d) by NEWTON04: 18;

 (a * b) = (c * d) & (a + b) = (c + d) implies ( max (a,b)) = ( max (c,d)) & ( min (a,b)) = ( min (c,d))

 proof

 assume

 B1: (a * b) = (c * d) & (a + b) = (c + d);

 then ( max (a,b)) = ( max (c,d)) by ISM;

 hence thesis by A1, B1;

 end;

 hence thesis by A1;

 end;

 theorem :: COMPLEX3:57



 POWER37: for a,b be non negative Real, c be positive Real holds a >= b iff (a to_power c) >= (b to_power c)

 proof

 let a,b be non negative Real, c be positive Real;

 b = 0 implies (b to_power c) = 0 by POWER:def 2;

 then

 A1: a > b implies (a to_power c) >= (b to_power c) by POWER: 37;

 a = 0 implies (a to_power c) = 0 by POWER:def 2;

 hence thesis by A1, XXREAL_0: 1, POWER: 37;

 end;

 theorem :: COMPLEX3:58

 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)

 proof

 let a,b,n be non negative Real;

 per cases ;

 suppose n is zero;

 then (( max (a,b)) to_power n) = 1 & (( min (a,b)) to_power n) = 1 & (a to_power n) = 1 & (b to_power n) = 1 by POWER: 24;

 hence thesis;

 end;

 suppose n is non zero;

 then

 reconsider n as positive Real;

 per cases ;

 suppose

 B1: a >= b;

 then

 B2: ( max (a,b)) = a & ( min (a,b)) = b by XXREAL_0:def 9, XXREAL_0:def 10;

 (a to_power n) >= (b to_power n) by B1, POWER37;

 hence thesis by B2, XXREAL_0:def 9, XXREAL_0:def 10;

 end;

 suppose

 B1: a < b;

 then

 B2: ( max (a,b)) = b & ( min (a,b)) = a by XXREAL_0:def 9, XXREAL_0:def 10;

 (a to_power n) < (b to_power n) by B1, POWER37;

 hence thesis by B2, XXREAL_0:def 9, XXREAL_0:def 10;

 end;

 end;

 end;

 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

 proof

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



 A1: ((a / b) * b) = a & ((c / d) * d) = c by XCMPLX_1: 87;

 assume ((a * b) > (c * d) & (a / b) >= (c / d)) or ((a * b) >= (c * d) & (a / b) > (c / d));

 then ((a * b) * (a / b)) > ((c * d) * (c / d)) by XREAL_1: 98;

 then (a * a) > (c * c) by A1;

 hence thesis by XREAL_1: 66;

 end;

 theorem :: COMPLEX3:60

 for a be positive Real holds (1 - a) < (1 / (1 + a))

 proof

 let a be positive Real;

 (1 - (a * a)) < (1 - 0 ) by XREAL_1: 10;

 then ((1 + a) * (1 - a)) < 1;

 hence thesis by XREAL_1: 81;

 end;

 theorem :: COMPLEX3:61

 for a be light positive Real holds (1 + a) < (1 / (1 - a))

 proof

 let a be light positive Real;

 (1 - (a * a)) < (1 - 0 ) by XREAL_1: 10;

 then ((1 + a) * (1 - a)) < 1 & (1 - a) > 0 ;

 hence thesis by XREAL_1: 81;

 end;

 theorem :: COMPLEX3:62



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

 proof

 let a,b be positive Real, m be non negative Real, n be positive Real;

 assume

 A1: ((a to_power m) + (b to_power m)) <= 1;

 (a to_power 0 ) = 1 & (b to_power 0 ) = 1 by POWER: 24;

 then not m = 0 by A1;

 then

 reconsider m as positive Real;



 A2: ((a to_power m) + 0 ) < ((a to_power m) + (b to_power m)) by XREAL_1: 6;

 (a > 1 implies (a to_power m) >= 1) & (a = 1 implies (a to_power m) = 1) by POWER: 35;

 then a >= 1 implies (a to_power m) >= 1 by XXREAL_0: 1;

 then

 reconsider a as light positive Real by A1, A2, TA1, XXREAL_0: 2;



 A3: ((b to_power m) + 0 ) < ((b to_power m) + (a to_power m)) by XREAL_1: 6;

 (b > 1 implies (b to_power m) >= 1) & (b = 1 implies (b to_power m) = 1) by POWER: 35;

 then b >= 1 implies (b to_power m) >= 1 by XXREAL_0: 1;

 then

 reconsider b as light positive Real by A1, A3, TA1, XXREAL_0: 2;

 0 < a < 1 & 0 (a to_power (m + n)) & (b to_power m) > (b to_power (m + n)) by POWER: 40;

 then ((a to_power (m + n)) + (b to_power (m + n))) < ((a to_power m) + (b to_power m)) by XREAL_1: 8;

 hence thesis by A1, XXREAL_0: 2;

 end;

 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

 proof

 let a,b be positive Real, m be non positive Real, n be negative Real;

 reconsider k = (a to_power ( - 1)) as positive Real;

 reconsider l = (b to_power ( - 1)) as positive Real;

 (k to_power ( - m)) = (a to_power (( - 1) * ( - m))) & (k to_power (( - m) - n)) = (a to_power (( - 1) * (( - m) - n))) & (l to_power ( - m)) = (b to_power (( - 1) * ( - m))) & (l to_power (( - m) - n)) = (b to_power (( - 1) * (( - m) - n))) by POWER: 33;

 hence thesis by Pow;

 end;

 theorem :: COMPLEX3:64



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

 proof

 let a,b,c,n be positive Real, m be non negative Real;

 assume

 A1: ((a to_power m) + (b to_power m)) <= (c to_power m);

 reconsider x = (a / c) as positive Real;

 reconsider y = (b / c) as positive Real;



 A2: (x * c) = a & (y * c) = b by XCMPLX_1: 87;



 A3: ((x * c) to_power m) = ((x to_power m) * (c to_power m)) & ((y * c) to_power m) = ((y to_power m) * (c to_power m)) & ((x * c) to_power (m + n)) = ((x to_power (m + n)) * (c to_power (m + n))) & ((y * c) to_power (m + n)) = ((y to_power (m + n)) * (c to_power (m + n))) by POWER: 30;

 then ((c to_power m) * ((x to_power m) + (y to_power m))) <= ((c to_power m) * 1) by A1, A2;

 then ((x to_power m) + (y to_power m)) <= 1 by XREAL_1: 68;

 then ((x to_power (m + n)) + (y to_power (m + n))) < 1 by Pow;

 then ((c to_power (m + n)) * ((x to_power (m + n)) + (y to_power (m + n)))) < ((c to_power (m + n)) * 1) by XREAL_1: 68;

 hence thesis by A2, A3;

 end;

 theorem :: COMPLEX3:65



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

 proof

 let a,b be positive Real, n be heavy positive Real;

 reconsider m = (n - 1) as positive Real;

 ((a to_power 1) + (b to_power 1)) = ((a + b) to_power 1);

 then ((a to_power (1 + m)) + (b to_power (1 + m))) < ((a + b) to_power (1 + m)) by NEW;

 hence thesis;

 end;

 registration

 let k be positive Real, n be heavy positive Real;

 cluster (((k + 1) to_power n) - (k to_power n)) -> heavy positive;

 coherence

 proof

 ((k + 1) to_power n) > ((k to_power n) + (1 to_power n)) by APB;

 then (((k + 1) to_power n) - (k to_power n)) > (((k to_power n) + 1) - (k to_power n)) by XREAL_1: 9;

 hence thesis by TA1;

 end;

 end

 registration

 let k be heavy positive Real, n be non negative Real;

 cluster ((k to_power (n + 1)) - (k to_power n)) -> positive;

 coherence

 proof

 (k to_power (n + 1)) = ((k to_power n) * (k to_power 1)) by POWER: 27

 .= (k * (k to_power n));

 then ((k to_power (n + 1)) - (k to_power n)) = ((k - 1) * (k to_power n));

 hence thesis;

 end;

 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)

 proof

 let k be positive Real, n be heavy positive Real;

 ((k + 1) to_power n) > ((k to_power n) + (1 to_power n)) by APB;

 hence thesis;

 end;

 theorem :: COMPLEX3:67



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

 proof

 let a,b be positive Real, n be light positive Real;

 reconsider m = (1 - n) as Real;

 ((a to_power (m + n)) + (b to_power (m + n))) = ((a + b) to_power (m + n));

 hence thesis by NEW;

 end;

 theorem :: COMPLEX3:68

 for k be positive Real, n be light positive Real holds ((k + 1) to_power n) < ((k to_power n) + 1)

 proof

 let k be positive Real, n be light positive Real;

 ((k + 1) to_power n) < ((k to_power n) + (1 to_power n)) by BPA;

 hence thesis;

 end;

 theorem :: COMPLEX3:69



 LMN: for k be positive Real, n be non positive Real holds ((k + 1) to_power n) < ((k to_power n) + 1)

 proof

 let k be positive Real, n be non positive Real;

 per cases ;

 suppose n = 0 ;

 then ((k + 1) to_power n) = 1 & (k to_power n) = 1 by POWER: 24;

 hence thesis;

 end;

 suppose n < 0 ;

 then

 reconsider n as negative Real;

 ((k + 1) to_power n) is light positive;

 then (((k + 1) to_power n) + 0 ) < (((k + 1) to_power n) + (k to_power n)) < (1 + (k to_power n)) by XREAL_1: 6;

 hence thesis by XXREAL_0: 2;

 end;

 end;

 theorem :: COMPLEX3:70



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

 proof

 let a,b be positive Real, n be non positive Real;

 reconsider k = (a / b) as positive Real;

 (k + 1) = ((a / b) + (b / b)) by XCMPLX_1: 60

 .= ((a + b) / b);

 then

 A1: ((k + 1) * b) = (a + b) & (k * b) = a by XCMPLX_1: 87;



 A2: (((k + 1) to_power n) * (b to_power n)) = (((k + 1) * b) to_power n) & ((k to_power n) * (b to_power n)) = ((k * b) to_power n) by POWER: 30;

 (((k + 1) to_power n) * (b to_power n)) < (((k to_power n) + 1) * (b to_power n)) by XREAL_1: 68, LMN;

 hence thesis by A1, A2;

 end;

 theorem :: COMPLEX3:71



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

 proof

 let a,b be positive Real, n be Real;

 not n is heavy positive implies ((a + b) to_power n) <= ((a to_power n) + (b to_power n))

 proof

 assume not n is heavy positive;

 then n <= 1 by TA1;

 per cases by XXREAL_0: 1;

 suppose n = 1;

 hence thesis;

 end;

 suppose

 B1: n < 1;

 per cases ;

 suppose n is positive;

 then n is light positive by B1, TA1;

 hence thesis by BPA;

 end;

 suppose n is non positive;

 hence thesis by BPC;

 end;

 end;

 end;

 hence thesis by APB;

 end;

 theorem :: COMPLEX3:72



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

 proof

 let a,b be positive Real, n be Real;

 ((a + b) to_power n) = ((a to_power n) + (b to_power n)) implies n = 1

 proof

 assume

 A1: ((a + b) to_power n) = ((a to_power n) + (b to_power n));

 then

 A2: not n is heavy positive by LME;

 reconsider n as positive Real by A1, BPC;

 n is light positive or n = 1 by A2, XXREAL_0: 1;

 hence thesis by A1, BPA;

 end;

 hence thesis;

 end;

 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

 proof

 let a,b be positive Real, n be Real;

 n is heavy positive iff n > 1 by TA1;

 then ((a + b) to_power n) <= ((a to_power n) + (b to_power n)) iff n <= 1 by LME;

 hence thesis by NE1, XXREAL_0: 1;

 end;

 theorem :: COMPLEX3:74



 FPC: for a,b,c be positive Real holds ((a + b) * (a + c)) > (a * ((a + b) + c))

 proof

 let a,b,c be positive Real;

 ((a * ((a + b) + c)) + (b * c)) > ((a * ((a + b) + c)) + 0 ) by XREAL_1: 6;

 hence thesis;

 end;

 theorem :: COMPLEX3:75



 FRAC: for a,b,c be positive Real holds (((a + b) + c) / (a + b)) < ((a + c) / a)

 proof

 let a,b,c be positive Real;

 ((a + b) * (a + c)) > (((a + b) + c) * a) by FPC;

 hence thesis by XREAL_1: 106;

 end;

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

 proof

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

 ((((a + b) + c) to_power n) / ((a + b) to_power n)) = ((((a + b) + c) / (a + b)) to_power n) & (((a + c) to_power n) / (a to_power n)) = (((a + c) / a) to_power n) by POWER: 31;

 hence thesis by FRAC, POWER: 37;

 end;

 theorem :: COMPLEX3:77



 ADB: for a,b be heavy positive Real holds ((a + b) - 1) > (a / b) > (1 / ((a + b) - 1))

 proof

 let a,b be heavy positive Real;

 a > 1 & b > 1 by TA1;

 then (a + b) > (1 + 1) by XREAL_1: 8;

 then ((a + b) - 1) > (2 - 1) by XREAL_1: 9;

 then

 reconsider c = ((a + b) - 1) as heavy positive Real by TA1;

 reconsider k = (a / b) as positive Real;

 ((k + 1) * b) > ((k + 1) * 1) by TA1, XREAL_1: 68;

 then (((k + 1) * b) - 1) > ((k + 1) - 1) by XREAL_1: 9;

 then

 A1: (((k * b) + b) - 1) > k;

 (((k " ) + 1) * a) > (((k " ) + 1) * 1) by TA1, XREAL_1: 68;

 then ((((k " ) + 1) * a) - 1) > (((k " ) + 1) - 1) by XREAL_1: 9;

 then ((((k " ) * a) + a) - 1) > (k " );

 then ((((b / a) * a) + a) - 1) > (k " ) by XCMPLX_1: 213;

 then ((((b + a) - 1) " ) " ) > (k " ) by XCMPLX_1: 87;

 hence thesis by A1, XCMPLX_1: 87, XREAL_1: 91;

 end;

 theorem :: COMPLEX3:78

 for a,b,c be positive Real holds (((a + b) + c) / a) > ((a + b) / (a + c)) > (a / ((a + b) + c))

 proof

 let a,b,c be positive Real;

 reconsider k = ((a + b) / a) as heavy positive Real;



 A1: (a + b) = (k * a) by XCMPLX_1: 87;

 reconsider l = ((a + c) / a) as heavy positive Real;



 A2: (a + c) = (l * a) by XCMPLX_1: 87;



 A3: (k / l) = ((a + b) / (a + c)) by XCMPLX_1: 55;



 A4: ((k + l) - 1) > (k / l) > (1 / ((k + l) - 1)) by ADB;

 ((a + b) + c) = (((k + l) - 1) * a) by A1, A2;

 then (((a + b) + c) / a) = ((k + l) - 1) by XCMPLX_1: 89;

 hence thesis by A3, A4, XCMPLX_1: 213;

 end;

 theorem :: COMPLEX3:79



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

 proof

 let a be light positive Real, n be heavy positive Real;



 A1: (((1 + a) to_power n) * ((1 - a) to_power n)) = (((1 - a) * (1 + a)) to_power n) by POWER: 30

 .= ((1 - (a * a)) to_power n);



 A2: ((1 + (a to_power n)) * (1 - (a to_power n))) = (1 - ((a to_power n) * (a to_power n)))

 .= (1 - ((a * a) to_power n)) by POWER: 30;

 (((1 - (a * a)) to_power n) + ((a * a) to_power n)) < (((1 - (a * a)) + (a * a)) to_power n) by APB;

 then ((((1 - (a * a)) to_power n) + ((a * a) to_power n)) - ((a * a) to_power n)) < ((1 to_power n) - ((a * a) to_power n)) by XREAL_1: 9;

 hence thesis by A1, A2;

 end;

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

 proof

 let a be light positive Real, n be heavy positive Real;

 (((1 + a) to_power n) * ((1 - a) to_power n)) < ((1 + (a to_power n)) * (1 - (a to_power n))) by IL1;

 hence thesis by XREAL_1: 106;

 end;

 theorem :: COMPLEX3:81

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

 proof

 let a be light positive Real;

 per cases ;

 suppose

 B1: a >= (1 - a);

 then (a + a) >= ((1 - a) + a) & (a + (1 - a)) >= ((1 - a) + (1 - a)) by XREAL_1: 6;

 then ((2 * a) / 2) >= (1 / 2) & ((2 * (1 - a)) / 2) <= (1 / 2) by XREAL_1: 72;

 hence thesis by B1, XXREAL_0:def 9, XXREAL_0:def 10;

 end;

 suppose

 B1: a < (1 - a);

 then (a + a) < ((1 - a) + a) & (a + (1 - a)) < ((1 - a) + (1 - a)) by XREAL_1: 6;

 then ((2 * a) / 2) < (1 / 2) & ((2 * (1 - a)) / 2) > (1 / 2) by XREAL_1: 74;

 hence thesis by B1, XXREAL_0:def 9, XXREAL_0:def 10;

 end;

 end;

 theorem :: COMPLEX3:82

 for a be light positive Real holds ((1 / (1 + a)) + (1 / (1 - a))) > 2

 proof

 let a be light positive Real;



 A1: (1 - (a * a)) < (1 - 0 ) by XREAL_1: 10;



 A2: ((1 * (1 - a)) / ((1 - a) * (1 + a))) = (1 / (1 + a)) & ((1 * (1 + a)) / ((1 + a) * (1 - a))) = (1 / (1 - a)) by XCMPLX_1: 91;

 (((1 - a) + (1 + a)) / ((1 - a) * (1 + a))) > (((1 - a) + (1 + a)) / 1) by A1, XREAL_1: 76;

 hence thesis by A2;

 end;

 theorem :: COMPLEX3:83

 for a be heavy positive Real holds ((1 / (a + 1)) + (1 / (a - 1))) > (2 / a)

 proof

 let a be heavy positive Real;



 A1: ((1 * (a + 1)) / ((a - 1) * (a + 1))) = (1 / (a - 1)) & ((1 * (a - 1)) / ((a - 1) * (a + 1))) = (1 / (a + 1)) & ((2 * a) / (a * a)) = (2 / a) by XCMPLX_1: 91;

 (1 - 1) < ((a * a) - 1) < ((a * a) - 0 ) by XREAL_1: 6;

 then (((a + 1) + (a - 1)) / ((a + 1) * (a - 1))) > (((a + 1) + (a - 1)) / (a * a)) by XREAL_1: 76;

 hence thesis by A1;

 end;

 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)

 proof

 let a,b be positive Real, n be heavy positive Real;

 ((((2 * a) + b) to_power n) + (b to_power n)) < ((((2 * a) + b) + b) to_power n) by APB;

 hence thesis;

 end;

 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)

 proof

 let a,n be heavy positive Real;

 (a + 1) = ((a - 1) + 2);

 then (((a + 1) to_power n) - ((a - 1) to_power n)) > ((((a - 1) to_power n) + (2 to_power n)) - ((a - 1) to_power n)) by APB, XREAL_1: 9;

 hence thesis;

 end;

 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)

 proof

 let a be light positive Real, n be heavy positive Real;



 A1: a < 1 & n > 1 by TA1;

 (1 + a) = ((1 - a) + (2 * a));

 then

 A2: (((1 + a) to_power n) - ((1 - a) to_power n)) > ((((1 - a) to_power n) + ((2 * a) to_power n)) - ((1 - a) to_power n)) by APB, XREAL_1: 9;

 (1 + 1) > (1 + a) by A1, XREAL_1: 6;

 then (2 to_power n) > ((1 + a) to_power n) by POWER: 37;

 then ((2 to_power n) - 0 ) > (((1 + a) to_power n) - ((1 - a) to_power n)) by XREAL_1: 14;

 hence thesis by A2;

 end;

 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)

 proof

 let a,n be heavy positive Real, b be light positive Real;



 A1: a > 1 & n > 1 & 0 ((((a - b) to_power n) + ((2 * b) to_power n)) - ((a - b) to_power n)) by APB, XREAL_1: 9;

 (1 + a) > (b + a) & ((a - 1) + (1 - b)) > ((a - 1) + 0 ) by A1, XREAL_1: 6;

 then ((a + 1) to_power n) > ((a + b) to_power n) & ((a - b) to_power n) > ((a - 1) to_power n) by POWER: 37;

 hence thesis by A2, XREAL_1: 14;

 end;

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

 proof

 let a,b be positive Real, n be positive Real;

 (a + b) > (a + 0 ) by XREAL_1: 6;

 then ((a + b) to_power n) > (a to_power n) by POWER: 37;

 then (((a + b) to_power n) + ((a + b) to_power n)) > (((a + b) to_power n) + (a to_power n)) > ((a to_power n) + (a to_power n)) by XREAL_1: 6;

 hence thesis;

 end;

 theorem :: COMPLEX3:89



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

 proof

 let a,b be positive Real such that

 A1: a <> b;

 reconsider x = (a / b) as positive Real;

 x <> 1 by A1, XCMPLX_1: 58;

 then (x to_power ( log (x,a))) = a & (x to_power ( log (x,b))) = b by POWER:def 3;

 hence thesis;

 end;

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

 proof

 let a,b be positive Real such that

 A1: a <> b;

 consider x,y be Real such that

 A2: a = ((a / b) to_power x) & b = ((a / b) to_power y) by A1, ATB;

 ((a / b) to_power x) = ((a / b) to_power (y + (x - y)))

 .= (((a / b) to_power y) * ((a / b) to_power (x - y))) by POWER: 27;

 then (((a / b) to_power y) * (((a / b) to_power (x - y)) - 1)) = (a - b) by A2;

 hence thesis;

 end;

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

 proof

 let a,m,n be positive Real;

 per cases ;

 suppose

 B1: n >= m;

 then (n - m) >= (m - m) by XREAL_1: 9;

 then

 reconsider k = (n - m) as non negative Real;

 (a to_power n) = (a to_power (m + k))

 .= ((a to_power m) * (a to_power k)) by POWER: 27;



 then ((a to_power n) + (a to_power m)) = ((a to_power m) * (1 + (a to_power |.( - (m - n)).|)))

 .= ((a to_power m) * (1 + (a to_power |.(m - n).|))) by COMPLEX1: 52;

 hence thesis by B1, XXREAL_0:def 9;

 end;

 suppose

 B1: n < m;

 then (n - n) < (m - n) by XREAL_1: 9;

 then

 reconsider k = (m - n) as positive Real;

 (a to_power m) = (a to_power (n + k))

 .= ((a to_power n) * (a to_power k)) by POWER: 27;

 then ((a to_power n) + (a to_power m)) = ((a to_power n) * (1 + (a to_power |.(m - n).|)));

 hence thesis by B1, XXREAL_0:def 9;

 end;

 end;

 theorem :: COMPLEX3:92



 ABA: for a,b be non weightless positive Real holds ( log (a,b)) = (1 / ( log (b,a)))

 proof

 let a,b be non weightless positive Real;



 A1: a > 0 & b > 0 & a <> 1 & b <> 1 by TA1;

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

 then a = (a to_power (( log (a,b)) * ( log (b,a)))) by POWER: 33;



 then (( log (a,b)) * ( log (b,a))) = ( log (a,a))

 .= 1 by A1, POWER: 52;

 hence thesis by XCMPLX_1: 73;

 end;

 registration

 let a be heavy positive Real, b be positive Real;

 cluster ( log (a,(a + b))) -> heavy;

 coherence

 proof



 A1: a > 1 & (a + b) > (a + 0 ) by TA1, XREAL_1: 6;

 then ( log (a,(a + b))) > ( log (a,a)) by POWER: 57;

 then ( log (a,(a + b))) > 1 by A1, POWER: 52;

 hence thesis by TA1;

 end;

 cluster ( log ((a + b),a)) -> light;

 coherence

 proof

 ( log ((a + b),a)) = (1 / ( log (a,(a + b)))) by ABA;

 hence thesis;

 end;

 end

 theorem :: COMPLEX3:93

 for a be positive non weightless Real, b be positive Real holds ( log (a,b)) = 0 iff b = 1

 proof

 let a be positive non weightless Real, b be positive Real;



 A1: |.a.| <> 1 by TA1;

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

 proof

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

 hence thesis by POWER: 24;

 end;

 hence thesis by POWER: 51, A1;

 end;

 theorem :: COMPLEX3:94



 AZ1: for a be non weightless positive Real, b be positive Real holds ( log (a,b)) = 1 iff a = b

 proof

 let a be non weightless positive Real, b be positive Real;



 A1: a <> 1 by TA1;

 ( log (a,b)) = 1 implies a = b

 proof

 assume ( log (a,b)) = 1;

 then b = (a to_power 1);

 hence thesis;

 end;

 hence thesis by A1, POWER: 52;

 end;

 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

 proof

 let a,b be positive Real, n be non zero Real;

 a <> b implies (a to_power n) <> (b to_power n)

 proof

 assume a <> b;

 per cases by XXREAL_0: 1;

 suppose

 B1: a > b;

 per cases ;

 suppose n > 0 ;

 hence thesis by B1, POWER: 37;

 end;

 suppose n < 0 ;

 hence thesis by B1, POWER: 38;

 end;

 end;

 suppose

 B1: a < b;

 per cases ;

 suppose n > 0 ;

 hence thesis by B1, POWER: 37;

 end;

 suppose n < 0 ;

 hence thesis by B1, POWER: 38;

 end;

 end;

 end;

 hence thesis;

 end;

 theorem :: COMPLEX3:96



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

 proof

 let a be non weightless positive Real, b be positive Real;



 A1: a <> 1 by TA1;

 reconsider x = (1 / a) as positive Real;



 A3: (1 / a) <> (1 / 1);



 A5: (x to_power ( - 1)) = (a to_power ( - ( - 1))) by POWER: 32;



 A6: ( log (x,b)) = (( log (x,a)) * ( log (a,b))) by A3, POWER: 56

 .= ((( - 1) * 1) * ( log (a,b))) by A5;



 A7: ((1 / b) to_power 1) = (b to_power ( - 1)) by POWER: 32;

 then

 A8: ( log (a,(1 / b))) = (( - 1) * ( log (a,b))) by A1, POWER: 55;

 ( log (x,(1 / b))) = (( - 1) * ( log (x,b))) by A3, A7, POWER: 55;

 hence thesis by A6, A8;

 end;

 theorem :: COMPLEX3:97



 AG1: for a be heavy positive Real, b be positive Real holds a > b iff ( log (a,b)) < 1

 proof

 let a be heavy positive Real, b be positive Real;



 A1: a > 1 by TA1;



 A2: ( log (a,b)) < 1 implies a > b

 proof

 assume ( log (a,b)) < 1;

 then (a to_power ( log (a,b))) < (a to_power 1) by A1, POWER: 39;

 hence thesis;

 end;

 a > b implies ( log (a,b)) < 1

 proof

 assume a > b;

 then (a to_power 1) > (a to_power ( log (a,b)));

 then 1 >= ( log (a,b)) & 1 <> ( log (a,b)) by A1, POWER: 39;

 hence thesis by XXREAL_0: 1;

 end;

 hence thesis by A2;

 end;

 theorem :: COMPLEX3:98



 AM1: for a be light positive Real, b be positive Real holds a (1 / b) iff ( log ((1 / a),(1 / b))) < 1 by AG1;

 hence thesis by XREAL_1: 76, ABO, XREAL_1: 118;

 end;

 theorem :: COMPLEX3:99



 AG2: for a be heavy positive Real, b be positive Real holds a 1

 proof

 let a be heavy positive Real, b be positive Real;

 a <= b iff ( log (a,b)) >= 1 by AG1;

 hence thesis by AZ1, XXREAL_0: 1;

 end;

 theorem :: COMPLEX3:100



 AM2: for a be light positive Real, b be positive Real holds a > b iff ( log (a,b)) > 1

 proof

 let a be light positive Real, b be positive Real;

 (1 / a) < (1 / b) iff ( log ((1 / a),(1 / b))) > 1 by AG2;

 hence thesis by XREAL_1: 76, ABO, XREAL_1: 118;

 end;

 theorem :: COMPLEX3:101

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

 proof

 let a,b be non weightless positive Real;

 assume

 A2: ( log (a,b)) >= 1;

 (( log (a,b)) / ( log (a,b))) >= (1 / ( log (a,b))) by A2, XREAL_1: 72;

 then 1 >= (1 / ( log (a,b))) by A2, XCMPLX_1: 60;

 hence thesis by A2, ABA;

 end;

 theorem :: COMPLEX3:102

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

 proof

 let a,b be non weightless positive Real;

 assume

 A2: ( log (a,b)) <= ( - 1);



 A4: ( log (b,a)) = (1 / ( log (a,b))) by ABA;

 (( log (a,b)) / ( log (a,b))) >= (( - 1) / ( log (a,b))) by A2, XREAL_1: 73;

 then 1 >= ( - (1 / ( log (a,b)))) by A2, XCMPLX_1: 60;

 hence thesis by A4, A2, XREAL_1: 26;

 end;

 theorem :: COMPLEX3:103

 for a,b be heavy positive Real holds ( log (a,b)) > ( log (b,a)) >= 1 implies a > b

 proof

 let a,b be heavy positive Real;



 A1: a > 1 & b > 1 by TA1;

 assume

 A2: ( log (a,b)) > ( log (b,a));

 assume ( log (b,a)) >= 1;

 then

 B2: ( log (b,a)) >= ( log (b,b)) by A1, POWER: 52;



 B4: a <> b by A2;

 a >= b by A1, B2, POWER: 57;

 hence thesis by B4, XXREAL_0: 1;

 end;

 theorem :: COMPLEX3:104

 for a,b be heavy positive Real holds ( log (b,a)) < 1 implies a 1 & b > 1 by TA1;

 assume

 B1: ( log (b,a)) < 1;

 then

 B2: ( log (b,a)) < ( log (b,b)) by A1, POWER: 52;

 a <= b by A1, B2, POWER: 57;

 hence thesis by B1, AZ1, XXREAL_0: 1;

 end;

 theorem :: COMPLEX3:105



 ACG: for a,c be heavy positive Real, b,d be positive Real st ( log (a,b)) <= ( log (c,d)) & a 1 by AG2;

 then ( log (c,d)) > 1 by A2, XXREAL_0: 2;

 hence thesis by AG2;

 end;

 theorem :: COMPLEX3:106



 ACL: for a,c be heavy positive Real, b,d be positive Real st ( log (a,b)) >= ( log (c,d)) & a > b holds c > d

 proof

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

 assume

 A2: ( log (a,b)) >= ( log (c,d)) & a > b;

 then ( log (a,b)) < 1 by AG1;

 then ( log (c,d)) < 1 by A2, XXREAL_0: 2;

 hence thesis by AG1;

 end;

 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 d

 proof

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

 assume

 A2: ( log (a,b)) <= ( log (c,d)) & a < b;

 then ( log (a,b)) > 1 by AG2;

 then ( log (c,d)) > 1 by A2, XXREAL_0: 2;

 hence thesis by AM2;

 end;

 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

 proof

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

 assume

 A2: ( log (a,b)) >= ( log (c,d)) & a > b;

 then ( log (a,b)) < 1 by AG1;

 then ( log (c,d)) < 1 by A2, XXREAL_0: 2;

 hence thesis by AM1;

 end;

 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

 proof

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

 assume

 A3: ( log (a,b)) <= ( log (c,d)) & a > b;



 A4: ( log (a,b)) = ( log ((1 / a),(1 / b))) & ( log (c,d)) = ( log ((1 / c),(1 / d))) by ABO;

 (1 / a) < (1 / b) by A3, XREAL_1: 76;

 then (1 / c) < (1 / d) by A3, A4, ACG;

 hence thesis by XREAL_1: 118;

 end;

 theorem :: COMPLEX3:110

 for a,c be light positive Real, b,d be positive Real holds ( log (a,b)) >= ( log (c,d)) & a = ( log (c,d)) & a < b;



 A4: ( log (a,b)) = ( log ((1 / a),(1 / b))) & ( log (c,d)) = ( log ((1 / c),(1 / d))) by ABO;

 (1 / a) > (1 / b) by A3, XREAL_1: 76;

 then (1 / c) > (1 / d) by A3, A4, ACL;

 hence thesis by XREAL_1: 118;

 end;

 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

 proof

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

 assume

 A2: ( log (a,b)) <= ( log (c,d)) & a > b;

 then ( log (a,b)) > 1 by AM2;

 then ( log (c,d)) > 1 by A2, XXREAL_0: 2;

 hence thesis by AG2;

 end;

 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 d

 proof

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

 assume

 A2: ( log (a,b)) >= ( log (c,d)) & a < b;

 then ( log (a,b)) < 1 by AM1;

 then ( log (c,d)) < 1 by A2, XXREAL_0: 2;

 hence thesis by AG1;

 end;

 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

 proof

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

 assume

 A2: ( log (a,b)) < ( log (c,d)) & a <= b;

 then ( log (a,b)) >= 1 by AG1;

 then ( log (c,d)) > 1 by A2, XXREAL_0: 2;

 hence thesis by AG2;

 end;

 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

 proof

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

 assume

 A2: ( log (a,b)) <= ( log (c,d)) & a <= b;

 then ( log (a,b)) >= 1 by AG1;

 then ( log (c,d)) >= 1 by A2, XXREAL_0: 2;

 hence thesis by AG1;

 end;

 theorem :: COMPLEX3:115

 for a,b be positive Real st a > b holds ( log ((a / b),a)) > ( log ((a / b),b))

 proof

 let a,b be positive Real;

 assume

 A1: a > b;

 then (a / b) > (b / b) by XREAL_1: 68;

 then (a / b) > 1 by XCMPLX_1: 60;

 hence thesis by A1, POWER: 57;

 end;