:: Multiplication-related Classes of Complex Numbers
:: by Rafal Ziobro
::
:: Received May 31, 2020
:: Copyright (c) 2020-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, ARYTM_3, ZFMISC_1, CARD_1, XXREAL_0, ARYTM_1, RELAT_1,
REAL_1, XCMPLX_0, COMPLEX3, COMPLEX1, ABSVALUE, NAT_1, NEWTON, POWER,
INT_1, SQUARE_1, XREAL_0, PROB_2, ORDINAL1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, FUNCT_4, ARYTM_2,
ARYTM_1, ARYTM_0, XCMPLX_0, XREAL_0, NUMBERS, XXREAL_0, COMPLEX1,
ABSVALUE, NEWTON, INT_1, SQUARE_1, COMPLEX2, PROB_2, POWER, POLYEQ_5,
RAT_1, REAL_1, NAT_1, COMSEQ_2, SEQ_4, XXREAL_2, INT_2, PYTHTRIP,
IRRAT_1, NAT_3, CARD_1, NAT_D, RELAT_1, FUNCT_1;
constructors FUNCT_4, ARYTM_1, ARYTM_0, XCMPLX_0, XXREAL_0, XREAL_0, COMPLEX1,
ABSVALUE, NEWTON, ORDINAL1, NAT_1, INT_1, REAL_1, SQUARE_1, POWER, ABIAN,
COMPLEX2, PROB_2, POLYEQ_5, SEQ_2, SEQM_3, SEQ_4, XXREAL_2, RELSET_1,
BINOP_2, COMSEQ_2, PREPOWER, NAT_D, PEPIN, PYTHTRIP, RAT_1, NAT_3,
NUMBERS, WSIERP_1, MOEBIUS1, EULER_1;
registrations XCMPLX_0, XXREAL_0, XREAL_0, ORDINAL1, NEWTON03, NAT_1, NEWTON,
NAT_6, INT_1, COMPLEX1, SQUARE_1, ABIAN, ABSVALUE, POWER, REAL_3,
PARTFUN3, FOMODEL0;
requirements SUBSET, NUMERALS, ARITHM, REAL;
equalities XCMPLX_0;
expansions NEWTON03, NAT_2;
theorems XCMPLX_1, XXREAL_0, ABSVALUE, XREAL_1, COMPLEX1, NAT_1, NAT_2,
NEWTON, INT_1, NEWTON02, SERIES_5, COMPLEX2, POLYEQ_5, SERIES_3,
PREPOWER, POWER, NEWTON04, REAL_3, NAT_D;
schemes NAT_1;
begin
registration
let a be Complex;
reduce a"" to a;
reducibility;
end;
definition
let a be Complex;
attr a is heavy means
:Def1:
|.a.| > 1;
attr a is light means
:Def2:
|.a.| < 1;
:: zero is included in weightless so as to adhere to trivial for Nats
attr a is weightless means
:Def3:
|.a.| = 0 or |.a.| = 1;
end;
theorem 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 Th2:
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;
:: could be another definition, in fact it was a starting point
theorem Th0:
for a be Real holds a is weightless iff a = sgn a
proof
let a be Real;
thus 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;
assume
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;
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;
:: more on Complex numbers
theorem 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 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 RI:
for a be Complex holds |.Re a.| + |.Im a.| >= |.a.|
proof
let a be Complex;
|.(Im a)*<i>.| = |.Im a.|*|.<i>.| by COMPLEX1:65
.= |.Im a.| by COMPLEX1:49; then
|.Re a + (Im a)*<i>.| <= |.Re a.| + |.Im a.| by COMPLEX1:56;
hence thesis by COMPLEX1:13;
end;
:: registrations
:: using single variable
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;
:: a/|.a.| shows a direction of a, so it may be useful to use it in a way similar to sgn
definition
let a be Complex;
func director a -> weightless Complex equals
a / |.a.|;
coherence;
end;
theorem
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 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 director a with sgn 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;
hence thesis by ABSVALUE:def 1;
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;
hence thesis by ABSVALUE:def 1;
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;
:: we could now extend the definition of sgn for Complex
:: rsgn a = Re (a/|.a.|)
definition
let a be Complex;
func rsgn a -> non heavy Complex equals
Re (director a);
coherence;
end;
:: and construct isgn a = Im (a/|.a.|)
definition
let a be Complex;
func isgn a -> non heavy Complex equals
Im (director a);
coherence;
end;
registration
let a be Real;
identify rsgn a with sgn 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 sgn a with rsgn a;
correctness;
cluster isgn a -> zero;
coherence;
end;
registration
let a be Real;
cluster frac a -> light non negative;
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;
:: added
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;
::/added
theorem 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
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
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
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;
:: multiplication
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;
:: as above, we can extend frac to Complex using cfrac a = (a/|.a.|)*frac|.a.|
:: also we could use rsgn(a) instead and obtain Real;
:: neither way is exact, however, as it is limited to positive Reals only
:: (it could be done in more complicated way, but it looks ugly and doesn't make much sense)
definition
let a be Complex;
func cfrac a -> light Complex equals
(director a)*frac|.a.|;
coherence;
end;
theorem
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 frac a with cfrac a;
correctness
proof
per cases;
suppose a = 0;
hence thesis;
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 cfrac a with frac a;
correctness;
end;
:: power, root
theorem 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;
:: remark: the sentence (and similar):
:: for l be Nat holds |.a.||^l = |.a|^l.| from NAT_1:sch 2(A1,A2);
:: works with relprem, but not with the verifier (resulting in 23 error).
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;
:: division
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;
:: sum
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;
:: min, max
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;
:: choosing one element of two of the same type
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,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;
:: some theorems
theorem 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
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
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;
:: reformulation of theorems
theorem ::SERIES_5:3:
for a,b,c be positive Real st a < b holds (b+c)/(a+c) is heavy
by SERIES_5:3;
:: some examples of justification using theorems in XREAL_1
:: theorem ::XREAL_1:159
:: for a,b be non light positive Real holds a*b is non light positive;
:: theorem ::XREAL_1:160
:: for a be non heavy non negative Real, b be Real st ((not b is positive) or (not b is heavy)) holds ((a*b is non heavy) or (a*b is non positive));
:: theorem ::XREAL_1:161
:: for a be heavy positive Real, b be non light positive Real holds a*b is heavy positive;
:: theorem ::XREAL_1:162
:: for a be light positive Real, b be Real st ((not b is positive) or (not b is heavy)) holds ((a*b is non heavy) or (a*b is non positive));
:: theorem ::XREAL_1:163
:: for a,b be heavy non positive Real holds a*b is heavy positive;
::some examples of registrations, based on SERIES
theorem PP1:
for a,b be positive Real holds (a/b + b/a)/2 >= 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 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 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;
:: We could use these registrations for some shortcuts
:: theorem for a,b be non zero Real, n be non zero Nat holds (a/b + b/a)|^(2*n) > 1 by TA1;
:: in fact, however:
theorem
for a,b be non zero Real 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;
::SERIESx5x13:
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;
:: ADDED 2020
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
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 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,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,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, 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 ABD:
for a,b be positive Real holds
a > b iff 1/a < 1/b by XREAL_1:118,XREAL_1:76;
theorem ABN:
for a,b be negative Real holds
a > b iff 1/a < 1/b by XREAL_1:119,XREAL_1:99;
theorem
for a,b be positive Real holds
1/a > 1/b iff -a > -b by ABD,XREAL_1:24;
theorem
for a,b be negative Real holds
1/a > 1/b iff -a > -b by ABN,XREAL_1:24;
theorem 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 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
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; then
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;
:: Sums and products
theorem 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 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
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
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 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
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;
:: Some relations for equal sums
theorem 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,def 10;
hence thesis by A1;
end;
theorem
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,def 10;
hence thesis by A1;
end;
theorem
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 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,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; then
per cases;
suppose
x = z;
hence thesis;
end;
suppose
B1: x = t;
x >= a & a >= y & z >= c & c >= t by XXREAL_0:17,25; then
x >= y & z >= t by XXREAL_0:2;
hence thesis by B1,A4,XXREAL_0:1;
end;
end;
theorem 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,def 10;
hence thesis by A1,A2;
end;
theorem
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
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
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 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
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 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
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 N158: ::see NEWTON01:5,NEWTON01:8
for a,b be positive Real, n,m be Real holds
a to_power (m+n) + b to_power (m+n) =
((a to_power m + b to_power m)*(a to_power n + b to_power n) +
(a to_power n - b to_power n)*(a to_power m - b to_power m))/2 &
a to_power (m+n) - b to_power (m+n) =
((a to_power m + b to_power m)*(a to_power n - b to_power n) +
(a to_power n + b to_power n)*(a to_power m - b to_power m))/2
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 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
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
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; then
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 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
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; then
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
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 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 ::see NEWTON03:42;
for a,b,n be non negative Real holds
max (a to_power n, b to_power n) = max (a,b) to_power n &
min (a to_power n, b to_power n) = min (a,b) to_power n
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
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
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
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 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 < b < 1 & m + 0 < m + n by TA1,XREAL_1:6; then
a to_power m > 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
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 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 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
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 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
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 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 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 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; then
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 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
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 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 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
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 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
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 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
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
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
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
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
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
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
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
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 < b < 1 by TA1;
(a+b) = (a - b) + 2*b; then
A2: (a+b) to_power n - (a-b) to_power n > (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 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 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
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
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;
:: Logarithms
theorem 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
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 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
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; then
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 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;
A5: x to_power (-1) = a to_power (-(-1)) by POWER:32;
A3: 1/a <> 1/1; then
A6: log (x,b) = log (x,a) * log (a,b) by 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 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 AM1:
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 AG1;
hence thesis by XREAL_1:76,ABO,XREAL_1:118;
end;
theorem AG2:
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;
a <= b iff log (a,b) >= 1 by AG1;
hence thesis by AZ1,XXREAL_0:1;
end;
theorem 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
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
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
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
for a,b be heavy positive Real holds
log (b,a) < 1 implies a < b
proof
let a,b be heavy positive Real;
A1: 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 ACG:
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 AG2; then
log (c,d) > 1 by A2,XXREAL_0:2;
hence thesis by AG2;
end;
theorem 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
for a be heavy positive Real,c be light positive Real, b,d be positive Real
holds
log (a,b) <= log (c,d) & a < b implies c > d
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
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
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
for a,c be light positive Real, b,d be positive Real holds
log (a,b) >= log (c,d) & a < b implies 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,ACL;
hence thesis by XREAL_1:118;
end;
theorem
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
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 AM1; then
log (c,d) < 1 by A2,XXREAL_0:2;
hence thesis by AG1;
end;
theorem
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
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
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;
begin :: Added from NEWTON06, mostly trivial ones
registration
let a be weightless Complex;
cluster |.a.| -> weightless;
coherence by Def3;
end;
registration
let a be light Complex;
cluster |.a.| -> light;
coherence by Def2;
end;
registration
let a be heavy Complex;
cluster |.a.| -> heavy;
coherence by Def1;
end;
registration
let a be heavy positive Real, b be negative Real;
cluster a - b -> heavy;
coherence;
end;
registration
let a be heavy negative Real, b be positive Real;
cluster a - b -> heavy;
coherence;
end;
registration
let a be non light positive Real, b be negative Real;
cluster a - b -> heavy;
coherence;
end;
registration
let a be non light negative Real, b be positive Real;
cluster a - b -> heavy;
coherence;
end;
registration
let a be non heavy Real, b be heavy negative Real;
cluster a - b -> positive;
coherence;
end;
registration
let a be light Real, b be non light negative Real;
cluster a - b -> positive;
coherence;
end;
registration
let a be non heavy Real, b be non light negative Real;
cluster a - b -> non negative;
coherence;
end;
registration
let a be non heavy Real, b be heavy positive Real;
cluster a - b -> negative;
coherence;
end;
registration
let a be light Real, b be non light positive Real;
cluster a - b -> negative;
coherence;
end;
registration
let a be non heavy Real, b be non light positive Real;
cluster a - b -> non positive;
coherence;
end;
registration
let a be light positive Real, b be light positive Real;
cluster a - b -> light;
coherence;
end;
registration
let a be non heavy positive Real, b be non heavy positive Real;
cluster a - b -> non heavy;
coherence;
end;
registration
let a be non integer Complex;
let b be Integer;
cluster a + b -> non integer;
coherence
proof
assume not thesis; then
(a + b) - b is integer;
hence contradiction;
end;
cluster a - b -> non integer;
coherence;
cluster b - a -> non integer;
coherence;
end;
registration
let a be non integer Complex;
let b be non zero Integer;
cluster a/b -> non integer;
coherence
proof
assume not thesis; then
(a/b)*b is integer;
hence contradiction by XCMPLX_1:87;
end;
end;
registration
cluster heavy for Integer;
existence
proof
2 is heavy & 2 is Integer;
hence thesis;
end;
end;
registration
let a be non heavy Real;
cluster [\a/] -> weightless;
coherence
proof
-1 <= a <= 1 by Th2; then
per cases by XXREAL_0:1;
suppose -1 <= a < -1 + 1; then
[\a/] = - 1 by REAL_3:2;
hence thesis;
end;
suppose
0 <= a < 0 + 1;
hence thesis by REAL_3:2;
end;
suppose
a = 1;
hence thesis;
end;
end;
cluster [/a\] -> weightless;
coherence
proof
per cases by INT_1:41;
suppose [/a\] = [\a/];
hence thesis;
end;
suppose
B1: [/a\] = [\a/] + 1; then
B2: [/a\] <> [\a/];
B3: a <= 1 by Th2;
[\a/] < a by B2,INT_1:26,INT_1:34; then
[\a/] is weightless negative or [\a/] is zero by B3,TA1;
hence thesis by B1;
end;
end;
end;
registration
let a be heavy positive Real;
cluster [/a\] -> heavy;
coherence
proof
[/a\] >= a by INT_1:def 7;
hence thesis by TA1,XXREAL_0:2;
end;
end;
registration
let a be light non positive Real;
cluster [/a\] -> zero;
coherence
proof
per cases;
suppose a is zero;
hence thesis;
end;
suppose a is non zero; then
reconsider a as light negative Real;
not a is integer; then
[/a\] = [\a/] + 1 by INT_1:41,INT_1:34
.= -1 + 1 by TA1;
hence thesis;
end;
end;
end;
registration
let a be heavy negative Real;
cluster [\a/] -> heavy negative;
coherence
proof
[\a/] <= a by INT_1:def 6; then
[\a/] < -1 by TA1,XXREAL_0:2;
hence thesis by TA1;
end;
end;
registration
let a be positive Real;
let b be non zero Real;
cluster b/(b*a) -> positive;
coherence
proof
(b*1)/(b*a) = 1/a by XCMPLX_1:91;
hence thesis;
end;
end;
registration
let a be negative Real;
let b be non zero Real;
cluster b/(b*a) -> negative;
coherence
proof
(b*1)/(b*a) = 1/a by XCMPLX_1:91;
hence thesis;
end;
end;
registration
let a be light non negative Real;
cluster [\a/] -> zero;
coherence
proof
per cases;
suppose a is zero;
hence thesis;
end;
suppose
not a is zero; then
reconsider a as light positive Real;
0 <= a < [\0/] + 1 by TA1;
hence thesis by INT_1:67;
end;
end;
end;
registration
let a be non zero Integer, b be Integer;
cluster a/(a*b) -> non heavy;
coherence
proof
per cases;
suppose b = 0;
hence thesis;
end;
suppose b < 0; then
reconsider b as negative Integer;
per cases;
suppose a is positive; then
reconsider a as positive Integer;
b is non light; then
b <= -1 by TA1; then
a*b <= a*(-1) by XREAL_1:64; then
a/(a*b) >= a/(-a) by XREAL_1:119; then
a/(a*b) >= - 1 by XCMPLX_1:198;
hence thesis by TA1;
end;
suppose a is negative; then
reconsider a as negative Integer;
b is non light; then
b <= -1 by TA1; then
a*b >= a*(-1) by XREAL_1:65; then
a/(a*b) >= a/(-a) by XREAL_1:120; then
a/(a*b) >= -1 by XCMPLX_1:198;
hence thesis by TA1;
end;
end;
suppose b > 0; then
reconsider b as positive Integer;
per cases;
suppose a is positive; then
reconsider a as positive Integer;
b is non light; then
a*b >= a*1 by XREAL_1:64; then
a/(a*b) <= a/a by XREAL_1:118;
hence thesis by XCMPLX_1:60;
end;
suppose a is negative; then
reconsider a as negative Integer;
b is non light; then
a*b <= a*1 by XREAL_1:65; then
a/(a*b) <= a/a by XREAL_1:121;
hence thesis by XCMPLX_1:60;
end;
end;
end;
end;
registration
let a be non zero Integer, b be Integer;
cluster a div (a*b) -> weightless;
coherence
proof
per cases;
suppose b = 0;
hence thesis;
end;
suppose b <> 0; then
reconsider b as non zero Integer;
[\a/(a*b)/] is weightless;
hence thesis by INT_1:def 9;
end;
end;
end;
registration
let a be non zero Integer, b be heavy Integer;
cluster a*b -> heavy;
coherence
proof
|.a.|*|.b.| > 1 by TA1;
hence thesis by COMPLEX1:65;
end;
end;
registration
let a be Integer, b be heavy Integer;
cluster a/(a*b) -> light;
coherence
proof
per cases;
suppose a is zero;
hence thesis;
end;
suppose not a is zero; then
(a*1)/(a*b) = 1/b by XCMPLX_1:91
.= b";
hence thesis;
end;
end;
end;
registration let a be light Real, b be Nat;
cluster a/b -> light;
coherence
proof
assume not thesis; then
reconsider c = a/b as non light Real;
b = 0 implies c = 0; then
reconsider b as non zero Nat;
c*b = a;
hence contradiction;
end;
end;
registration
let a be Integer, b be heavy Integer;
cluster a div (a*b) -> weightless non positive;
coherence
proof
per cases;
suppose a is zero;
hence thesis;
end;
suppose a is non zero; then
reconsider a as non light Integer;
per cases;
suppose b is negative; then
reconsider b as heavy negative Real;
[\a/(a*b)/] is weightless non positive Real;
hence thesis by INT_1:def 9;
end;
suppose
b is positive; then
reconsider b as heavy positive Real;
[\a/(a*b)/] is weightless non positive Real;
hence thesis by INT_1:def 9;
end;
end;
end;
end;
registration
let a be non zero Integer;
cluster a div a -> weightless positive;
coherence
proof
a div a = 1 by INT_1:49;
hence thesis;
end;
end;
registration
let a be Nat, b be non zero Nat;
cluster (a mod b) div b -> zero;
coherence by NAT_D:1,NAT_D:27;
end;
registration
cluster non heavy non light -> weightless for Complex;
coherence by XXREAL_0:1;
end;
registration
let b be non zero Real;
cluster b*b" -> weightless positive;
coherence
proof
b*b" = b/b
.= 1 by XCMPLX_1:60;
hence thesis;
end;
end;