:: Integer and Rational Exponents
:: by Konrad Raczkowski
::
:: Received September 21, 1990
:: Copyright (c) 1990-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, INT_1, COMPLEX1, ORDINAL1, XREAL_0, SUBSET_1, RAT_1,
SEQ_1, SEQ_2, FUNCT_1, XXREAL_0, ORDINAL2, CARD_1, NEWTON, REAL_1,
ARYTM_3, RELAT_1, NAT_1, ARYTM_1, VALUED_1, XXREAL_2, SEQ_4, SQUARE_1,
VALUED_0, INT_2, PREPOWER, TARSKI, FUNCT_7, ASYMPT_1, XCMPLX_0;
notations TARSKI, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, XXREAL_2,
XREAL_0, COMPLEX1, REAL_1, INT_2, INT_1, NAT_1, NAT_D, NEWTON, RELAT_1,
FUNCT_1, FUNCOP_1, VALUED_0, VALUED_1, SEQ_1, COMSEQ_2, SEQ_2, SQUARE_1,
SEQ_4, RAT_1;
constructors FUNCOP_1, REAL_1, SQUARE_1, NAT_1, NAT_D, SEQ_2, SEQM_3,
PARTFUN1, VALUED_1, SEQ_4, NEWTON, XXREAL_2, RELSET_1, BINOP_2, COMSEQ_2,
SEQ_1, NUMBERS;
registrations ORDINAL1, RELSET_1, NUMBERS, XXREAL_0, XREAL_0, NAT_1, INT_1,
RAT_1, MEMBERED, NEWTON, XBOOLE_0, VALUED_0, VALUED_1, FUNCT_2, SEQ_1,
SEQ_2, XCMPLX_0;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions TARSKI, XXREAL_2;
equalities VALUED_1, XCMPLX_0, SEQ_1;
expansions TARSKI, XXREAL_2;
theorems ABSVALUE, NAT_1, SEQ_1, SEQ_2, INT_1, SQUARE_1, SEQ_4, RAT_1,
RFUNCT_2, TARSKI, FUNCT_2, NEWTON, XREAL_0, XCMPLX_0, XCMPLX_1, FUNCOP_1,
COMPLEX1, XREAL_1, XXREAL_0, INT_2, ORDINAL1, NAT_D, VALUED_1, VALUED_0,
RELAT_1, NUMBERS;
schemes NAT_1, SEQ_1, FUNCT_2;
begin
registration
let i be Integer;
cluster |.i.| -> natural;
coherence;
end;
reserve x for set;
reserve a, b, c for Real;
reserve m, n, m1, m2 for Nat;
reserve k, l for Integer;
reserve p, q for Rational;
reserve s1, s2 for Real_Sequence;
theorem Th1:
s1 is convergent & (for n holds s1.n>=a) implies lim s1 >= a
proof
assume that
A1: s1 is convergent and
A2: for n holds s1.n>=a;
set s = seq_const a;
A3: now
let n;
s1.n >= a by A2;
hence s1.n >= s.n by SEQ_1:57;
end;
lim s = s.0 by SEQ_4:26
.= a by SEQ_1:57;
hence thesis by A1,A3,SEQ_2:18;
end;
theorem Th2:
s1 is convergent & (for n holds s1.n<=a) implies lim s1 <= a
proof
assume that
A1: s1 is convergent and
A2: for n holds s1.n<=a;
set s = seq_const a;
A3: now
let n;
s1.n <= a by A2;
hence s1.n <= s.n by SEQ_1:57;
end;
lim s = s.0 by SEQ_4:26
.= a by SEQ_1:57;
hence thesis by A1,A3,SEQ_2:18;
end;
definition
let a be Real;
func a GeoSeq -> Real_Sequence means
:Def1:
for m holds it.m = a|^m;
existence
proof
reconsider a as Real;
deffunc F(Nat) = In(a|^$1,REAL);
consider f be Real_Sequence such that
A1: for m being Element of NAT holds f.m = F(m) from FUNCT_2:sch 4;
take f;
let m;
reconsider m as Element of NAT by ORDINAL1:def 12;
f.m = F(m) by A1;
hence thesis;
end;
uniqueness
proof
let s1,s2 such that
A2: for n holds s1.n= a|^n and
A3: for n holds s2.n= a|^n;
for n being Element of NAT holds s1.n = s2.n
proof
let n be Element of NAT;
thus s1.n = a|^n by A2
.= s2.n by A3;
end;
hence thesis by FUNCT_2:63;
end;
end;
theorem Th3:
s1 = a GeoSeq iff s1.0 = 1 & for m holds s1.(m+1) = s1.m * a
proof
defpred P[Nat] means s1.$1 = a GeoSeq.$1;
hereby
assume
A1: s1 = a GeoSeq;
hence s1.0 = a|^0 by Def1
.= 1 by NEWTON:4;
let m;
thus s1.(m+1) = a|^(m+1) by A1,Def1
.= a|^m * a by NEWTON:6
.= s1.m * a by A1,Def1;
end;
assume that
A2: s1.0 = 1 and
A3: for m holds s1.(m+1) = s1.m * a;
A4: for m st P[m] holds P[m+1]
proof
let m such that
A5: s1.m = a GeoSeq.m;
thus s1.(m+1) = s1.m * a by A3
.= a|^m * a by A5,Def1
.= a|^(m+1) by NEWTON:6
.= a GeoSeq.(m+1) by Def1;
end;
s1.0 = a|^0 by A2,NEWTON:4
.= a GeoSeq.0 by Def1;
then
A6: P[0];
for m holds P[m] from NAT_1:sch 2(A6,A4);
then for m being Element of NAT holds P[m];
hence thesis by FUNCT_2:63;
end;
theorem
for a st a <> 0 holds for m holds a GeoSeq.m <> 0
proof
let a such that
A1: a <> 0;
defpred P[Nat] means a GeoSeq.$1 <> 0;
A2: for n holds P[n] implies P[n+1]
proof
let n such that
A3: a GeoSeq.n <> 0;
a GeoSeq.(n+1) = a GeoSeq.n * a by Th3;
hence thesis by A1,A3;
end;
A4: P[0] by Th3;
thus for n holds P[n] from NAT_1:sch 2(A4,A2);
end;
theorem Th5:
for a being Complex
for n being natural Number holds 0 <> a implies 0 <> a |^ n
proof
let a be Complex;
let n be natural Number;
A1: n is Nat by TARSKI:1;
defpred P[Nat] means a |^ $1 <> 0;
assume
A2: 0<>a;
A3: for m be Nat st P[m] holds P[m+1]
proof
let m be Nat;
assume a |^ m <> 0;
then (a |^ m)*a <> 0 by A2;
hence thesis by NEWTON:6;
end;
A4: P[0] by NEWTON:4;
for m be Nat holds P[m] from NAT_1:sch 2(A4,A3);
hence thesis by A1;
end;
theorem Th6:
for n being natural Number holds 0 < a implies 0 < a |^ n
proof
let n be natural Number;
A1: n is Nat by TARSKI:1;
defpred P[Nat] means 0 < a |^ $1;
assume
A2: 0<a;
A3: for m be Nat st P[m] holds P[m+1]
proof
let m be Nat;
assume a |^ m > 0;
then (a |^ m)*a > 0*a by A2;
hence thesis by NEWTON:6;
end;
A4: P[0] by NEWTON:4;
for m be Nat holds P[m] from NAT_1:sch 2(A4,A3);
hence thesis by A1;
end;
theorem Th7:
for a being Complex, n being natural Number holds (1/a) |^ n = 1 / a |^ n
proof
let a be Complex;
let n be natural Number;
A1: n is Nat by TARSKI:1;
defpred P[Nat] means (1/a) |^ $1 = 1/ a |^ $1;
A2: for m be Nat st P[m] holds P[m+1]
proof
let m be Nat;
assume (1/a) |^ m = 1 / a |^ m;
hence (1/a) |^ (m+1) = 1 / a |^ m * (1/a) by NEWTON:6
.= 1*1 / (a |^ m * a) by XCMPLX_1:76
.= 1 / a |^ (m+1) by NEWTON:6;
end;
(1/a) |^ 0 = 1 by NEWTON:4
.= 1/1
.= 1/ a |^ 0 by NEWTON:4;
then
A3: P[0];
for m be Nat holds P[m] from NAT_1:sch 2(A3,A2);
hence thesis by A1;
end;
theorem
for a,b being Complex
for n being natural Number holds (b/a) |^ n = b |^ n / a |^ n
proof
let a,b be Complex;
let n be natural Number;
thus (b/a) |^ n = (b*a") |^ n .= b |^ n * (a") |^ n by NEWTON:7
.= b |^ n * (1/a) |^ n
.= b |^ n * (1/a |^ n) by Th7
.= b |^ n*1 / a |^ n
.= b |^ n / a |^ n;
end;
theorem Th9:
for n being natural Number st 0 < a & a <= b holds a |^ n <= b |^ n
proof
let n be natural Number;
A1: n is Nat by TARSKI:1;
assume that
A2: 0 < a and
A3: a <= b;
defpred P[Nat] means a |^ $1 <= b |^ $1;
A4: for m1 be Nat st P[m1] holds P[m1+1]
proof
let m1 be Nat such that
A5: a |^ m1 <= b |^ m1;
a |^ m1 > 0 by A2,Th6;
then a |^ m1 * a <= b |^ m1 * b by A2,A3,A5,XREAL_1:66;
then a |^ (m1+1) <= b |^ m1 * b by NEWTON:6;
hence thesis by NEWTON:6;
end;
A6: b |^ 0 = b GeoSeq.0 by Def1
.= 1 by Th3;
a |^ 0 = a GeoSeq.0 by Def1
.= 1 by Th3;
then
A7: P[0] by A6;
for m1 be Nat holds P[m1] from NAT_1:sch 2(A7,A4);
hence thesis by A1;
end;
Lm1: for n being natural Number holds 0 < a & a < b & 1 <= n
implies a |^ n < b |^ n
proof
let n be natural Number;
assume that
A1: 0 < a and
A2: a < b and
A3: 1 <= n;
consider m being Nat such that
A4: n = 1+m by A3,NAT_1:10;
defpred P[Nat] means a |^ (1+$1) < b |^ (1+$1);
A5: for m1 st P[m1] holds P[m1+1]
proof
let m1;
assume
A6: a |^ (1+m1) < b |^ (1+m1);
a |^ (1+m1) > 0 by A1,Th6;
then a |^ (1+m1) * a < b |^ (1+m1) * b by A1,A2,A6,XREAL_1:97;
then a |^ (1+m1+1) < b |^ (1+m1) * b by NEWTON:6;
hence thesis by NEWTON:6;
end;
A7: P[0] by A2;
A8: for m1 holds P[m1] from NAT_1:sch 2(A7,A5);
thus thesis by A4,A8;
end;
theorem Th10:
for n being natural Number st 0 <= a & a < b & 1 <= n holds a |^ n < b |^ n
proof
let n be natural Number;
assume that
A1: 0 <= a and
A2: a < b and
A3: 1 <= n;
per cases by A1;
suppose
a>0;
hence thesis by A2,A3,Lm1;
end;
suppose
A4: a=0;
reconsider k=n, k1=1 as Integer;
reconsider m=k-k1 as Element of NAT by A3,INT_1:5;
a |^ n = a |^ (m+1) .= a |^ m * a |^ 1 by NEWTON:8
.= a |^ m * a GeoSeq.(0+1) by Def1
.= a |^ m * (a GeoSeq.0 * 0) by A4,Th3
.= 0;
hence thesis by A1,A2,Th6;
end;
end;
theorem Th11:
for n being natural Number holds a>=1 implies a |^ n >= 1
proof
let n be natural Number;
assume a>=1;
then a |^ n >= 1 |^ n by Th9;
hence thesis by NEWTON:10;
end;
theorem Th12:
for n being natural Number st 1 <= a & 1 <= n holds a <= a |^ n
proof
let n be natural Number;
assume that
A1: 1 <= a and
A2: 1 <= n;
consider m being Nat such that
A3: n=m+1 by A2,NAT_1:6;
defpred P[Nat] means a <= a |^ ($1+1);
A4: for m1 st P[m1] holds P[m1+1]
proof
let m1;
assume a <= a |^ (m1+1);
then a*1 <= a |^ (m1+1) * a by A1,XREAL_1:66;
hence thesis by NEWTON:6;
end;
A5: P[0];
A6: for m1 holds P[m1] from NAT_1:sch 2(A5,A4);
thus thesis by A3,A6;
end;
theorem
for n being Nat st 1 < a & 2 <= n holds a < a |^ n
proof
let n be Nat;
assume that
A1: 1 < a and
A2: 2 <= n;
consider m being Nat such that
A3: n = 2+m by A2,NAT_1:10;
defpred P[Nat] means a < a |^ (2+$1);
A4: a*a > a*1 by A1,XREAL_1:68;
A5: for m1 st P[m1] holds P[m1+1]
proof
let m1;
assume a < a |^ (2+m1);
then a |^ (2+m1) * a > a*a by A1,XREAL_1:68;
then a |^ (2+m1+1) > a*a by NEWTON:6;
hence thesis by A4,XXREAL_0:2;
end;
a |^ (2+0) = a GeoSeq.(1+1) by Def1
.= a GeoSeq.(0+1) * a by Th3
.= a GeoSeq.0 * a * a by Th3
.= 1*a*a by Th3
.= a*a;
then
A6: P[0] by A4;
A7: for m1 holds P[m1] from NAT_1:sch 2(A6,A5);
thus thesis by A3,A7;
end;
theorem Th14:
for n being natural Number st 0 < a & a <= 1 & 1 <= n holds a |^ n <= a
proof
let n be natural Number;
assume that
A1: 0 < a and
A2: a <= 1 and
A3: 1 <= n;
consider m being Nat such that
A4: n = 1+m by A3,NAT_1:10;
defpred P[Nat] means a |^ (1+$1) <= a;
A5: a*a <= a*1 by A1,A2,XREAL_1:64;
A6: for m1 st P[m1] holds P[m1+1]
proof
let m1;
assume a |^ (1+m1) <= a;
then a |^ (1+m1) * a <= a*a by A1,XREAL_1:64;
then a |^ (1+(m1+1)) <= a*a by NEWTON:6;
hence thesis by A5,XXREAL_0:2;
end;
A7: P[0];
A8: for m1 holds P[m1] from NAT_1:sch 2(A7,A6);
thus thesis by A4,A8;
end;
theorem
for n being Nat st 0 < a & a < 1 & 2 <= n holds a |^ n < a
proof
let n be Nat;
assume that
A1: 0 < a and
A2: a < 1 and
A3: 2 <= n;
consider m being Nat such that
A4: n = 2+m by A3,NAT_1:10;
defpred P[Nat] means a |^ (2+$1) < a;
A5: a*a < a*1 by A1,A2,XREAL_1:68;
A6: for m1 st P[m1] holds P[m1+1]
proof
let m1;
assume a |^ (2+m1) < a;
then a |^ (2+m1) * a < a*a by A1,XREAL_1:68;
then a |^ (2+m1+1) < a*a by NEWTON:6;
hence thesis by A5,XXREAL_0:2;
end;
a |^ (2+0) = a GeoSeq.(1+1) by Def1
.= a GeoSeq.(0+1) * a by Th3
.= a GeoSeq.0 * a * a by Th3
.= 1*a*a by Th3
.= a*a;
then
A7: P[0] by A5;
A8: for m1 holds P[m1] from NAT_1:sch 2(A7,A6);
thus thesis by A4,A8;
end;
theorem Th16:
for n being natural Number holds -1 < a implies (1 + a) |^ n >= 1 + n * a
proof
let n be natural Number;
A1: n is Nat by TARSKI:1;
defpred P[Nat] means (1 + a) |^ $1 >= 1 + $1 * a;
assume
A2: -1 < a;
A3: for m be Nat st P[m] holds P[m+1]
proof
A4: -1+1<1+a by A2,XREAL_1:6;
let m be Nat;
assume (1+a) |^ m >= 1 + m * a;
then (1+a) |^ m * (1+a) >= (1 + m*a)*(1+a) by A4,XREAL_1:64;
then
A5: (1+a) |^ (m+1) >= 1 + 1*a + m*a + (m*a)*a by NEWTON:6;
0<=a*a by XREAL_1:63;
then 1 + (m+1)*a + 0 <= 1 + (m+1)*a + m*(a*a) by XREAL_1:7;
hence thesis by A5,XXREAL_0:2;
end;
(1 + a) |^ 0 = (1+a) GeoSeq.0 by Def1
.= 1 by Th3;
then
A6: P[0];
for m being Nat holds P[m] from NAT_1:sch 2(A6,A3);
hence thesis by A1;
end;
theorem Th17:
for n being natural Number st 0 < a & a < 1 holds
(1 + a) |^ n <= 1 + 3 |^ n * a
proof
let n be natural Number;
A1: n is Nat by TARSKI:1;
assume that
A2: 0 < a and
A3: a < 1;
A4: 1 + 0 < 1 + a by A2,XREAL_1:6;
defpred P[Nat] means (1 + a) |^ $1 <= 1 + 3 |^ $1 * a;
A5: for n be Nat holds P[n] implies P[n+1]
proof
let n be Nat;
assume (1 + a) |^ n <= 1 + 3 |^ n * a;
then
A6: (1 + a) |^ n * (1 + a) <= (1 + 3 |^ n * a) * (1+a) by A2,XREAL_1:64;
A7: 1 + 3 |^ n * a + (3 |^ n + 3 |^ n) * a = 1 + (3 |^ n * (1 + 2)) * a
.= 1 + 3 |^ (n+1) * a by NEWTON:6;
A8: 1 <= 3 |^ n
proof
per cases;
suppose
A9: 0 = n;
3 |^ n = 3 GeoSeq.n by Def1
.= 1 by A9,Th3;
hence thesis;
end;
suppose
0 <> n;
then 0 + 1 <= n by NAT_1:13;
then 1 |^ n < 3 |^ n by Lm1;
hence thesis;
end;
end;
then 1 * a <= 3 |^ n * a by A2,XREAL_1:64;
then
A10: 1 + a <= 1 + 3 |^ n * a by XREAL_1:7;
a * a < 1 * a by A2,A3,XREAL_1:68;
then 3 |^ n * (a * a) < 3 |^ n * a by A8,XREAL_1:68;
then
A11: 3 |^ n * a + 3 |^ n * (a*a) < 3 |^ n * a + 3 |^ n * a by XREAL_1:6;
(1 + 3 |^ n * a) * (1+a) = 1 + a + (3 |^ n * a + 3 |^ n * (a * a));
then (1 + 3 |^ n * a) * (1+a) < 1 + 3 |^ (n+1) * a by A10,A7,A11,XREAL_1:8;
then (1 + a) |^ n * (1 + a) <= 1 + 3 |^ (n + 1) * a by A6,XXREAL_0:2;
hence thesis by NEWTON:6;
end;
A12: 1 + 3 |^ 0 * a = 1 + 3 GeoSeq.0 * a by Def1
.= 1 + 1 * a by Th3
.= 1 + a;
(1 + a) |^ 0 = (1 + a) GeoSeq.0 by Def1
.= 1 by Th3;
then
A13: P[0] by A12,A4;
for n be Nat holds P[n] from NAT_1:sch 2(A13,A5);
hence thesis by A1;
end;
theorem Th18:
s1 is convergent & (for n holds s2.n = (s1.n) |^ m) implies s2
is convergent & lim s2 = (lim s1) |^ m
proof
assume that
A1: s1 is convergent and
A2: for n holds s2.n = (s1.n) |^ m;
defpred P[Nat] means
for s being Real_Sequence st (for n holds s.
n=(s1.n) |^ $1) holds s is convergent & lim s=(lim s1) |^ $1;
A3: P[0]
proof
let s be Real_Sequence;
assume
A4: for n holds s.n = (s1.n) |^ 0;
reconsider j = 1 as Element of REAL by NUMBERS:19;
A5: now
let n be Nat;
thus s.n = (s1.n) |^ 0 by A4
.= (s1.n) GeoSeq.0 by Def1
.= j by Th3;
end;
then
A6: s is constant by VALUED_0:def 18;
hence s is convergent;
thus lim s = s.0 by A6,SEQ_4:26
.= 1 by A5
.= (lim s1) GeoSeq.0 by Th3
.= (lim s1) |^ 0 by Def1;
end;
A7: for m1 holds P[m1] implies P[m1+1]
proof
let m1;
assume
A8: for s being Real_Sequence st (for n holds s.n = (s1.n) |^ m1)
holds s is convergent & lim s = (lim s1) |^ m1;
deffunc O(Nat) = (s1.$1) |^ m1;
let s be Real_Sequence;
consider s3 being Real_Sequence such that
A9: for n holds s3.n = O(n) from SEQ_1:sch 1;
assume
A10: for n holds s.n = (s1.n) |^ (m1+1);
now
let n;
thus s.n = (s1.n) |^ (m1+1) by A10
.= (s1.n) |^ m1 * (s1.n) by NEWTON:6
.= (s3.n) * (s1.n) by A9;
end;
then
A11: s = s3(#)s1 by SEQ_1:8;
A12: s3 is convergent by A8,A9;
hence s is convergent by A1,A11;
lim s3 = (lim s1) |^ m1 by A8,A9;
hence lim s = (lim s1) |^ m1 * (lim s1) by A1,A12,A11,SEQ_2:15
.= (lim s1) |^ (m1+1) by NEWTON:6;
end;
for m1 holds P[m1] from NAT_1:sch 2(A3,A7);
hence thesis by A2;
end;
definition
let n be natural Number;
let a be Real;
assume
A1: 1 <= n;
func n -Root a -> Real means
:Def2:
it |^ n = a & it > 0 if a>0, it = 0 if a=0;
consistency;
existence
proof
now
set X = {b where b is Real: 0 < b & b |^ n <= a};
for x being object holds x in X implies x in REAL
proof
let x be object;
assume x in X;
then ex b be Real st x = b & 0 < b & b |^ n <= a;
hence thesis by XREAL_0:def 1;
end;
then reconsider X as Subset of REAL by TARSKI:def 3;
reconsider a1 = a as Real;
reconsider j = 1 as Element of REAL by NUMBERS:19;
A2: j <= a implies ex c st c in X
proof
assume
A3: j <= a;
take j;
j |^ n <= a by A3,NEWTON:10;
hence thesis;
end;
A4: a < 1 implies ex c be Real st c is UpperBound of X
proof
consider c such that
A5: c = 1;
assume
A6: a < 1;
take c;
let b be ExtReal;
assume b in X;
then consider d being Real such that
A7: d = b & 0 < d & d |^ n <= a;
assume not b <= c;
then 1 |^ n < d |^ n by A1,A5,Lm1,A7;
then 1 < d |^ n by NEWTON:10;
hence contradiction by A6,A7,XXREAL_0:2;
end;
assume
A8: a>0;
1 <= a implies ex c be Real st c is UpperBound of X
proof
assume
A9: 1 <= a;
take a;
let b be ExtReal;
assume b in X;
then consider d being Real such that
A10: b = d & 0 < d & d |^ n <= a;
assume a < b;
then a |^ n < d |^ n by A1,A8,Lm1,A10;
then a |^ n < a by A10,XXREAL_0:2;
hence contradiction by A1,A9,Th12;
end;
then
A11: X is bounded_above by A4;
take d = upper_bound X;
A12: a < 1 implies ex c st c in X
proof
assume
A13: a < 1;
reconsider a as Real;
take a;
a |^ n <= a by A1,A8,A13,Th14;
hence thesis by A8;
end;
A14: 0 < d
proof
consider c such that
A15: c in X by A2,A12;
ex e be Real st e = c & 0 < e & e |^ n <= a by A15;
hence thesis by A11,A15,SEQ_4:def 1;
end;
A16: not a < d |^ n
proof
set b = d * (1 - a / d |^ n) / (n + 1);
assume
A17: a < d |^ n;
then
A18: 1/(n+1) * d |^ n > 1/(n+1) * a by XREAL_1:68;
a * (d |^ n)" > 0*a by A8,A17;
then -(- a / d |^ n) > 0;
then - a / d |^ n < 0;
then 1 + - a / d |^ n < 1+0 by XREAL_1:6;
then
A19: (1 - a / d |^ n) * (n+1)" < 1*(n+1)" by XREAL_1:68;
1 < n+1 by A1,NAT_1:13;
then (n+1)" < 1 by XREAL_1:212;
then (1 - a / d |^ n) / (n + 1) < 1 by A19,XXREAL_0:2;
then
A20: d * ((1 - a / d |^ n) / (n + 1)) < d*1 by A14,XREAL_1:68;
then b/d < d/d by A14,XREAL_1:74;
then b/d < 1 by A14,XCMPLX_1:60;
then - 1 < - b/d by XREAL_1:24;
then
A21: (1 + -b/d) |^ n >= 1 + n * (-b/d) by Th16;
a / d |^ n < d |^ n / d |^ n by A8,A17,XREAL_1:74;
then 0 + a / d |^ n < 1 by A8,A17,XCMPLX_1:60;
then 0 < 1 - a / d |^ n by XREAL_1:20;
then d * 0 < d * (1 - a / d |^ n) by A14;
then 0 / (n + 1) < d * (1 - a / d |^ n) / (n + 1);
then consider c be Real such that
A22: c in X and
A23: d - b < c by A2,A12,A11,SEQ_4:def 1;
0 < d - b by A20,XREAL_1:50;
then
A24: (d - b) |^ n < c |^ n by A1,A23,Lm1;
(1 + n * (-b/d)) * d |^ n = (1 - n * (d * (1 - a / d |^ n) / (n +
1)/d)) * d |^ n
.= (1 - n*(d * ((1 - a / d |^ n) / (n+1))/d)) * d |^ n
.= (1 - n * ((((1 - a / d |^ n) / (n + 1))/d) * d)) * d |^ n
.= (1 - n * ((1 - a / d |^ n) / (n + 1))) * d |^ n by A14,XCMPLX_1:87
.= (1 - (1 - a / d |^ n) * n / (n + 1)) * d |^ n
.= (1 - (1 - a / d |^ n) * (n / (n + 1))) * d |^ n
.= (1 - n/(n+1) + a/d |^ n * (n/(n+1))) * d |^ n
.= ((n+1)/(n+1)-n/(n+1) + a/d |^ n *(n/(n+1))) * d |^ n by
XCMPLX_1:60
.= ((n+1-n)/(n+1) + a/d |^ n *(n/(n+1))) * d |^ n
.= (1/(n+1) + (n/(n+1) * a)/d |^ n) * d |^ n
.= 1/(n+1) * d |^ n + (n/(n+1) * a)/d |^ n * d |^ n
.= 1/(n+1) * d |^ n + n/(n+1) * a by A8,A17,XCMPLX_1:87;
then
A25: (1 + n * (-b/d)) * d |^ n > 1/(n+1) * a + n/(n+1) * a by A18,XREAL_1:6;
(d - b) |^ n = ((d - b) * 1) |^ n
.= ((d - b) * (d" * d)) |^ n by A14,XCMPLX_0:def 7
.= ((d - b) * d" * d) |^ n
.= ((d - b) / d * d) |^ n
.= ((d/d - b/d) * d) |^ n
.= ((1 - b/d) * d) |^ n by A14,XCMPLX_1:60
.= (1 + -b/d) |^ n * d |^ n by NEWTON:7;
then (d - b) |^ n >= (1 + n * (-b/d)) * d |^ n by A8,A17,A21,XREAL_1:64
;
then (d - b) |^ n > ((n + 1)/(n+1)) * a by A25,XXREAL_0:2;
then
A26: (d - b) |^ n > 1 * a by XCMPLX_1:60;
ex e be Real st e = c & 0 < e & e |^ n <= a by A22;
hence contradiction by A24,A26,XXREAL_0:2;
end;
not d |^ n < a
proof
set b = min(1/2 , (a1 / d |^ n - 1)/3 |^ n );
set c = (1 + b) * d;
A27: c |^ n = (1 + b) |^ n * d |^ n by NEWTON:7;
A28: 0 < 3 |^ n by Th6;
3 |^ n * b <= (a / d |^ n - 1)/3 |^ n * 3 |^ n by XREAL_1:64
,XXREAL_0:17;
then 3 |^ n * b <= a / d |^ n - 1 by A28,XCMPLX_1:87;
then
A29: 1 + 3 |^ n * b <= a / d |^ n by XREAL_1:19;
A30: d |^ n > 0 by A14,Th6;
A31: d |^ n <> 0 by A14,Th6;
assume d |^ n < a;
then d |^ n / d |^ n < a / d |^ n by A30,XREAL_1:74;
then 1 < a / d |^ n by A31,XCMPLX_1:60;
then 1 - 1 < a / d |^ n - 1 by XREAL_1:9;
then (a / d |^ n - 1) / 3 |^ n > 0/3 |^ n by A28;
then
A32: b > 0 by XXREAL_0:15;
then 1 + b > 1 + 0 by XREAL_1:6;
then
A33: (1 + b) * d > 1 * d by A14,XREAL_1:68;
b <= 1/2 by XXREAL_0:17;
then b < 1 by XXREAL_0:2;
then (1 + b) |^ n <= 1 + 3 |^ n * b by A32,Th17;
then (1 + b) |^ n <= a / d |^ n by A29,XXREAL_0:2;
then c |^ n <= a / d |^ n * d |^ n by A30,A27,XREAL_1:64;
then
A34: c |^ n <= a by A31,XCMPLX_1:87;
(1 + b) * d > 0 * d by A14,A32;
then c in X by A34;
hence contradiction by A11,A33,SEQ_4:def 1;
end;
hence a = d |^ n & d>0 by A14,A16,XXREAL_0:1;
end;
hence thesis;
end;
uniqueness
proof
now
let b,c be Real;
assume that
A35: b |^ n = a and
A36: b>0 and
A37: c |^ n = a and
A38: c>0 and
A39: b <> c;
per cases by A39,XXREAL_0:1;
suppose
b > c;
hence contradiction by A1,A35,A37,A38,Lm1;
end;
suppose
c > b;
hence contradiction by A1,A35,A36,A37,Lm1;
end;
end;
hence thesis;
end;
end;
registration
let n;
let a be Real;
cluster n -Root a -> real;
coherence;
end;
Lm2: for n being Nat st a>0 & n>=1 holds (n -Root a) |^ n = a & n -Root (a |^
n) = a
proof
let n be Nat;
assume that
A1: a>0 and
A2: n>=1;
thus (n -Root a) |^ n = a by A1,A2,Def2;
assume
A3: n -Root (a |^ n) <> a;
per cases by A3,XXREAL_0:1;
suppose
A4: n -Root (a |^ n) > a;
a |^ n > 0 by A1,Th6;
hence contradiction by A1,A2,A4,Def2;
end;
suppose
A5: n -Root (a |^ n) < a;
a |^ n > 0 by A1,Th6;
hence contradiction by A1,A2,A5,Def2;
end;
end;
theorem Th19:
for n being Nat st a>=0 & n>=1 holds (n -Root a) |^ n = a & n
-Root (a |^ n) = a
proof
let n be Nat;
assume that
A1: a>=0 and
A2: n>=1;
per cases by A1;
suppose
a>0;
hence thesis by A2,Lm2;
end;
suppose
A3: a=0;
reconsider k=n, k1=1 as Integer;
reconsider m=k-k1 as Element of NAT by A2,INT_1:5;
A4: 0 |^ n = 0 |^ (m+1) .= 0 |^ m * 0 |^ 1 by NEWTON:8
.= 0 |^ m * 0 GeoSeq.(0+1) by Def1
.= 0 |^ m * (0 GeoSeq.0 * 0) by Th3
.= 0;
hence (n -Root a) |^ n = a by A2,A3,Def2;
thus thesis by A2,A3,A4,Def2;
end;
end;
theorem Th20:
n>=1 implies n -Root 1 = 1
proof
A1: 1 |^ n = 1;
assume n>=1;
hence thesis by A1,Def2;
end;
theorem Th21:
a>=0 implies 1 -Root a = a
proof
assume
A1: a>=0;
a |^ 1 = a GeoSeq.(0+1) by Def1
.= a GeoSeq.0 * a by Th3
.= 1*a by Th3
.= a;
hence thesis by A1,Th19;
end;
theorem Th22:
a>=0 & b>=0 & n>=1 implies n -Root (a*b) = n -Root a * n -Root b
proof
assume that
A1: a>=0 and
A2: b>=0 and
A3: n>=1 and
A4: n -Root (a*b) <> n -Root a * n -Root b;
A5: (n -Root a * n -Root b) |^ n = (n -Root a) |^ n * (n -Root b) |^ n by
NEWTON:7
.= a * (n -Root b) |^ n by A1,A3,Th19
.= a * b by A2,A3,Th19;
per cases by A1,A2;
suppose
A6: a>0 & b>0;
then
A7: n -Root b > 0 by A3,Def2;
A8: n -Root a > 0 by A3,A6,Def2;
a*b>0 by A6;
then
A9: n -Root (a*b) > 0 by A3,Def2;
per cases by A4,XXREAL_0:1;
suppose
n -Root (a*b) < n -Root a * n -Root b;
hence contradiction by A3,A5,A9,Th19;
end;
suppose
n -Root (a*b) > n -Root a * n -Root b;
hence contradiction by A3,A5,A8,A7,Th19;
end;
end;
suppose
A10: a=0 & b>0;
then n -Root (a*b) = 0 by A3,Def2;
hence contradiction by A4,A10;
end;
suppose
A11: a>0 & b=0;
then n -Root (a*b) = 0 by A3,Def2;
hence contradiction by A4,A11;
end;
suppose
A12: a=0 & b=0;
then n -Root (a*b) = 0 by A3,Def2;
hence contradiction by A4,A12;
end;
end;
theorem Th23:
a>0 & n>=1 implies n -Root (1/a) = 1/(n -Root a)
proof
assume that
A1: a>0 and
A2: n>=1 and
A3: n -Root (1/a) <> 1/(n -Root a);
A4: n -Root a > 0 by A1,A2,Def2;
A5: (1/(n -Root a)) |^ n = 1 / (n -Root a) |^ n by Th7
.= 1/a by A1,A2,Lm2;
A6: n -Root (1/a) > 0 by A1,A2,Def2;
per cases by A3,XXREAL_0:1;
suppose
n -Root (1/a) > 1/(n -Root a);
hence contradiction by A2,A4,A5,Lm2;
end;
suppose
n -Root (1/a) < 1/(n -Root a);
hence contradiction by A2,A5,A6,Lm2;
end;
end;
theorem
a>=0 & b>0 & n>=1 implies n -Root (a/b) = n -Root a / n -Root b
proof
assume that
A1: a>=0 and
A2: b>0 and
A3: n>=1;
thus n -Root (a/b) = n -Root (a*b")
.= n -Root a * n -Root (b") by A1,A2,A3,Th22
.= n -Root a * n -Root (1/b)
.= n -Root a * (1/n -Root b) by A2,A3,Th23
.= n -Root a * 1 / n -Root b
.= n -Root a / n -Root b;
end;
theorem Th25:
a>=0 & n>=1 & m>=1 implies n -Root (m -Root a) = (n*m) -Root a
proof
assume that
A1: a>=0 and
A2: n>=1 and
A3: m>=1 and
A4: n -Root (m -Root a) <> (n*m) -Root a;
per cases by A1;
suppose
A5: a>0;
then
A6: m -Root a > 0 by A3,Def2;
then
A7: n -Root (m -Root a) > 0 by A2,Def2;
A8: (n -Root (m -Root a)) |^ (n*m) = ((n -Root (m -Root a)) |^ n) |^ m by
NEWTON:9
.= (m -Root a) |^ m by A2,A6,Lm2
.= a by A1,A3,Th19;
A9: n*m>=1 by A2,A3,XREAL_1:159;
then
A10: (n*m) -Root a > 0 by A5,Def2;
per cases by A4,XXREAL_0:1;
suppose
n -Root (m -Root a) < (n*m) -Root a;
hence contradiction by A5,A8,A9,A7,Def2;
end;
suppose
(n*m) -Root a < n -Root (m -Root a);
hence contradiction by A5,A8,A9,A10,Def2;
end;
end;
suppose
A11: a=0;
n*m>=1 by A2,A3,XREAL_1:159;
then
A12: (n*m) -Root a = 0 by A11,Def2;
m -Root a = 0 by A3,A11,Def2;
hence contradiction by A2,A4,A12,Def2;
end;
end;
theorem Th26:
a>=0 & n>=1 & m>=1 implies n -Root a * m -Root a = (n*m) -Root ( a |^ (n+m))
proof
assume that
A1: a>=0 and
A2: n>=1 and
A3: m>=1 and
A4: n -Root a * m -Root a <> (n*m) -Root (a |^ (n+m));
A5: (n -Root a * m -Root a) |^ (n*m) = (n -Root a) |^ (n*m) * (m -Root a) |^
(n*m) by NEWTON:7
.= ((n -Root a) |^ n) |^ m * (m -Root a) |^ (n*m) by NEWTON:9
.= a |^ m * (m -Root a) |^ (m*n) by A1,A2,Th19
.= a |^ m * ((m -Root a) |^ m) |^ n by NEWTON:9
.= a |^ m * a |^ n by A1,A3,Th19
.= a |^ (n+m) by NEWTON:8;
A6: n*m>=1 by A2,A3,XREAL_1:159;
per cases by A1;
suppose
A7: a>0;
then
A8: m -Root a > 0 by A3,Def2;
n -Root a > 0 by A2,A7,Def2;
then
A9: n -Root a * m -Root a > 0 by A8;
A10: a |^ (n+m) > 0 by A7,Th6;
then
A11: (n*m) -Root (a |^ (n+m)) > 0 by A6,Def2;
per cases by A4,XXREAL_0:1;
suppose
n -Root a * m -Root a < (n*m) -Root (a |^ (n+m));
hence contradiction by A5,A6,A10,A9,Def2;
end;
suppose
n -Root a * m -Root a > (n*m) -Root (a |^ (n+m));
hence contradiction by A5,A6,A10,A11,Def2;
end;
end;
suppose
A12: a=0;
reconsider k=n, k1=1 as Integer;
reconsider m1=k-k1 as Element of NAT by A2,INT_1:5;
A13: a |^ (n+m) = a |^ (m1+m+1) .= a |^ (m1+m) * a by NEWTON:6
.= 0 by A12;
n -Root a = 0 by A2,A12,Def2;
hence contradiction by A4,A6,A13,Def2;
end;
end;
theorem Th27:
0<=a & a<=b & n>=1 implies n -Root a <= n -Root b
proof
assume that
A1: a>=0 and
A2: a<=b and
A3: n>=1 and
A4: n -Root a > n -Root b;
A5: now
per cases by A1,A2;
suppose
b > 0;
hence n -Root b >= 0 by A3,Def2;
end;
suppose
b=0;
hence n -Root b >= 0 by A3,Def2;
end;
end;
(n -Root a) |^ n = a by A1,A3,Th19;
then (n -Root a) |^ n <= (n -Root b) |^ n by A1,A2,A3,Th19;
hence contradiction by A3,A4,A5,Th10;
end;
theorem Th28:
a>=0 & a<b & n>=1 implies n -Root a < n -Root b
proof
assume that
A1: a>=0 and
A2: a<b and
A3: n>=1 and
A4: n -Root a >= n -Root b;
(n -Root a) |^ n = a by A1,A3,Th19;
then
A5: (n -Root a) |^ n < (n -Root b) |^ n by A1,A2,A3,Lm2;
n -Root b > 0 by A1,A2,A3,Def2;
hence contradiction by A4,A5,Th9;
end;
theorem Th29:
a>=1 & n>=1 implies n -Root a >= 1 & a >= n -Root a
proof
assume that
A1: a>=1 and
A2: n>=1;
n -Root a >= n -Root 1 by A1,A2,Th27;
hence n -Root a >= 1 by A2,Th20;
n -Root a <= n -Root (a |^ n) by A1,A2,Th12,Th27;
hence thesis by A1,A2,Lm2;
end;
theorem Th30:
0<=a & a<1 & n>=1 implies a <= n -Root a & n -Root a < 1
proof
assume that
A1: 0<=a and
A2: a<1 and
A3: n>=1;
A4: now
per cases by A1;
suppose
a>0;
hence a |^ n >= 0 by Th6;
end;
suppose
a=0;
hence a |^ n >=0;
end;
end;
now
per cases by A1;
suppose
a>0;
hence a |^ n <= a by A2,A3,Th14;
end;
suppose
a=0;
hence a |^ n <= a by A3,NEWTON:11;
end;
end;
then n -Root (a |^ n) <= n -Root a by A3,A4,Th27;
hence a <= n -Root a by A1,A3,Th19;
n -Root a < n -Root 1 by A1,A2,A3,Th28;
hence thesis by A3,Th20;
end;
theorem Th31:
a>0 & n>=1 implies n -Root a - 1 <= (a-1)/n
proof
assume that
A1: a>0 and
A2: n>=1;
n -Root a > 0 by A1,A2,Def2;
then n -Root a - 1 > 0 - 1 by XREAL_1:9;
then (1 + (n -Root a - 1)) |^ n >= 1 + n*(n -Root a - 1) by Th16;
then a >= 1 + n*(n -Root a - 1) by A1,A2,Lm2;
then a - 1 >= n*(n -Root a - 1) by XREAL_1:19;
then (a - 1)/n >= n*(n -Root a - 1)/n by XREAL_1:72;
hence thesis by A2,XCMPLX_1:89;
end;
theorem
a>=0 implies 2-Root a = sqrt a
proof
assume that
A1: a>=0 and
A2: 2-Root a <> sqrt a;
A3: sqrt a >= 0 by A1,SQUARE_1:def 2;
sqrt a |^ 2 = (sqrt a)^2 by NEWTON:81
.= a by A1,SQUARE_1:def 2;
hence contradiction by A2,A3,Th19;
end;
Lm3: for s being Real_Sequence, a st a >= 1 & (for n st n>=1 holds s.n = n
-Root a) holds s is convergent & lim s = 1
proof
set s2 = seq_const 1;
let s be Real_Sequence;
let a such that
A1: a>=1;
deffunc O(Nat) = (a-1)/($1+1);
consider s1 being Real_Sequence such that
A2: for n holds s1.n = O(n) from SEQ_1:sch 1;
set s3 = s2 + s1;
A3: s1 is convergent by A2,SEQ_4:31;
then
A4: s3 is convergent;
assume
A5: for n st n>=1 holds s.n = n -Root a;
A6: now
let n;
A7: n+1>=0+1 by XREAL_1:6;
set b = (s^\1).n - 1;
A8: (s^\1).n = s.(n+1) by NAT_1:def 3
.= (n+1) -Root a by A5,A7;
then
A9: (s^\1).n >= 1 by A1,A7,Th29;
then (s^\1).n-1>=0 by XREAL_1:48;
then
A10: -1 < b;
a = (1+b) |^ (n+1) by A1,A7,A8,Lm2;
then a >= 1 + (n+1)*b by A10,Th16;
then a - 1 >= 1 + (n+1)*b - 1 by XREAL_1:9;
then (a - 1)*(n+1)" >= (n+1)"*((n+1)*b) by XREAL_1:64;
then (a - 1)*(n+1)" >= (n+1)"*(n+1)*b;
then (a - 1)*(n+1)" >= 1*b by XCMPLX_0:def 7;
then (a-1)/(n+1) + 1 >= (s^\1).n - 1 + 1 by XREAL_1:6;
then s2.n + (a-1)/(n+1) >= (s^\1).n by SEQ_1:57;
then s2.n + s1.n >= (s^\1).n by A2;
hence s2.n<=(s^\1).n & (s^\1).n<=s3.n by A9,SEQ_1:57,SEQ_1:7;
end;
lim s1 = 0 by A2,SEQ_4:31;
then
A11: lim s3 = s2.0 + 0 by A3,SEQ_4:42
.= 1 by SEQ_1:57;
A12: lim s2 = s2.0 by SEQ_4:26
.= 1 by SEQ_1:57;
then
A13: s^\1 is convergent by A4,A11,A6,SEQ_2:19;
hence s is convergent by SEQ_4:21;
lim (s^\1) = 1 by A4,A11,A12,A6,SEQ_2:20;
hence thesis by A13,SEQ_4:22;
end;
theorem
for s being Real_Sequence st a > 0 & (for n st n>=1 holds s.n = n
-Root a) holds s is convergent & lim s = 1
proof
let s be Real_Sequence;
assume
A1: a>0;
assume
A2: for n st n>=1 holds s.n = n -Root a;
per cases;
suppose
a>=1;
hence thesis by A2,Lm3;
end;
suppose
A3: a<1;
then a/a<1/a by A1,XREAL_1:74;
then
A4: 1<=1/a by A1,XCMPLX_1:60;
deffunc O(Nat) = $1 -Root (1/a);
consider s1 being Real_Sequence such that
A5: for n holds s1.n = O(n) from SEQ_1:sch 1;
A6: for n holds n>=1 implies s1.n=n -Root (1/a) by A5;
then
A7: lim s1 = 1 by A4,Lm3;
A8: s1 is convergent by A4,A6,Lm3;
A9: now
let b be Real;
assume b>0;
then consider m1 such that
A10: for m st m1<=m holds |.s1.m-1.|<b by A8,A7,SEQ_2:def 7;
reconsider n=m1+1 as Nat;
take n;
let m;
assume
A11: n<=m;
A12: n>=0+1 by XREAL_1:6;
then
A13: 1<=m by A11,XXREAL_0:2;
then
A14: m -Root a<1 by A1,A3,Th30;
A15: (m -Root a) <> 0 by A1,A13,Def2;
then
A16: |.1/(m -Root a) - 1.| = |.1/(m -Root a) - (m -Root a)/(m -Root a
).| by XCMPLX_1:60
.= |.(1 - m -Root a)/(m -Root a).|
.= |.(1 - m -Root a)*(m -Root a)".|
.= |.1 - m -Root a.|*|.(m -Root a)".| by COMPLEX1:65;
0<m -Root a by A1,A3,A13,Th30;
then (m -Root a)*(m -Root a)"<1*(m -Root a)" by A14,XREAL_1:68;
then 1<(m -Root a)" by A15,XCMPLX_0:def 7;
then
A17: 1<|.(m -Root a)".| by ABSVALUE:def 1;
0<>1 - m -Root a by A1,A3,A13,Th30;
then |.1 - m -Root a.| > 0 by COMPLEX1:47;
then
A18: 1*|.1 - m -Root a.| < |.1 - m -Root a.|*|.(m -Root a)".| by A17,
XREAL_1:68;
m1<=n by XREAL_1:29;
then m1<=m by A11,XXREAL_0:2;
then |.s1.m-1.|<b by A10;
then |.m -Root (1/a) - 1.|<b by A5;
then |.1/(m -Root a) - 1.|<b by A1,A13,Th23;
then |.-(m -Root a - 1).| < b by A16,A18,XXREAL_0:2;
then |.m -Root a - 1.| < b by COMPLEX1:52;
hence |.s.m - 1.| < b by A2,A12,A11,XXREAL_0:2;
end;
hence s is convergent by SEQ_2:def 6;
hence thesis by A9,SEQ_2:def 7;
end;
end;
definition
let a be Real;
let k be Integer;
func a #Z k -> number equals
:Def3:
a |^ |.k.| if k >= 0, (a |^ |.k.|)" if k < 0;
consistency;
coherence by TARSKI:1;
end;
registration
let a be Real;
let k be Integer;
cluster a #Z k -> real;
coherence
proof
a #Z k = a |^ |.k.| or a #Z k = (a |^ |.k.|)" by Def3;
hence thesis;
end;
end;
theorem Th34:
a #Z 0 = 1
proof
thus a #Z 0 = a |^ |.0.| by Def3
.= a |^ 0 by ABSVALUE:2
.= a GeoSeq.0 by Def1
.= 1 by Th3;
end;
theorem Th35:
a #Z 1 = a
proof
thus a #Z 1 = a |^ |.1.| by Def3
.= a |^ (0+1) by ABSVALUE:def 1
.= a GeoSeq.(0+1) by Def1
.= a GeoSeq.0 * a by Th3
.= 1*a by Th3
.= a;
end;
theorem Th36:
for n being Nat holds a #Z n = a |^ n
proof
let n be Nat;
thus a #Z n = a |^ |.n.| by Def3
.= a |^ n by ABSVALUE:def 1;
end;
Lm4: 1" = 1;
theorem Th37:
1 #Z k = 1
proof
per cases;
suppose
k>=0;
hence 1 #Z k = 1 |^ |.k.| by Def3
.= 1;
end;
suppose
k<0;
1 #Z k = (1 |^ |.k.|)" by Def3;
hence thesis;
end;
end;
theorem
a<>0 implies a #Z k <> 0
proof
assume
A1: a<>0;
per cases;
suppose
k>=0;
then a #Z k = a |^ |.k.| by Def3;
hence thesis by A1,Th5;
end;
suppose
k<0;
then a #Z k = (a |^ |.k.|)" by Def3;
hence thesis by A1,Th5,XCMPLX_1:202;
end;
end;
theorem Th39:
a>0 implies a #Z k > 0
proof
assume
A1: a>0;
per cases;
suppose
k>=0;
then a #Z k = a |^ |.k.| by Def3;
hence thesis by A1,Th6;
end;
suppose
A2: k<0;
A3: a |^ |.k.| > 0 by A1,Th6;
a #Z k = (a |^ |.k.|)" by A2,Def3;
hence thesis by A3;
end;
end;
theorem Th40:
(a*b) #Z k = a #Z k * b #Z k
proof
per cases;
suppose
A1: k>=0;
hence (a*b) #Z k = (a*b) |^ |.k.| by Def3
.= a |^ |.k.| * b |^ |.k.| by NEWTON:7
.= a #Z k * b |^ |.k.| by A1,Def3
.= a #Z k * b #Z k by A1,Def3;
end;
suppose
A2: k<0;
hence (a*b) #Z k = ((a*b) |^ |.k.|)" by Def3
.= (a |^ |.k.| * b |^ |.k.|)" by NEWTON:7
.= (a |^ |.k.|)" * (b |^ |.k.|)" by XCMPLX_1:204
.= a #Z k * (b |^ |.k.|)" by A2,Def3
.= a #Z k * b #Z k by A2,Def3;
end;
end;
theorem Th41:
a #Z (-k) = 1/a #Z k
proof
per cases;
suppose
A1: k>0;
then -k<-0;
hence a #Z (-k) = (a |^ |.-k.|)" by Def3
.= (a |^ |.k.|)" by COMPLEX1:52
.= 1 / a |^ |.k.|
.= 1 / a #Z k by A1,Def3;
end;
suppose
A2: k=0;
hence a #Z (-k) = 1/1 by Th34
.= 1/a GeoSeq.0 by Th3
.= 1/a |^ 0 by Def1
.= 1/a #Z k by A2,Th36;
end;
suppose
A3: k<0;
then a #Z k = (a |^ |.k.|)" by Def3
.= 1 / a |^ |.k.|
.= 1 / a |^ |.-k.| by COMPLEX1:52
.= 1 / a #Z (-k) by A3,Def3;
hence thesis;
end;
end;
theorem Th42:
(1/a) #Z k = 1/a #Z k
proof
per cases;
suppose
A1: k>=0;
hence (1/a) #Z k = (1/a) |^ |.k.| by Def3
.= 1 / a |^ |.k.| by Th7
.= 1 / a #Z k by A1,Def3;
end;
suppose
A2: k<0;
hence (1/a) #Z k = ((1/a) |^ |.k.|)" by Def3
.= (1 / a |^ |.k.|)" by Th7
.= (a |^ |.k.|)""
.= (a #Z k)" by A2,Def3
.= 1/a #Z k;
end;
end;
theorem Th43:
for m,n being Nat holds a<>0 implies a #Z (m-n) = a |^ m / a |^ n
proof
let m,n be Nat;
assume
A1: a<>0;
per cases;
suppose
m-n>=0;
then reconsider m1 = m-n as Element of NAT by INT_1:3;
A2: a #Z (m-n) * a |^ n = a |^ m1 * a |^ n by Th36
.= a |^ (m1+n) by NEWTON:8
.= a |^ m;
a |^ n <> 0 by A1,Th5;
hence thesis by A2,XCMPLX_1:89;
end;
suppose
m-n<0;
then -(m-n)>0;
then reconsider m1 = n-m as Element of NAT by INT_1:3;
A3: a #Z (n-m) = a #Z (-(m-n)) .= 1/a #Z (m-n) by Th41;
a #Z (n-m) * a |^ m = a |^ m1 * a |^ m by Th36
.= a |^ (m1+m) by NEWTON:8
.= a |^ n;
then
A4: a |^ m / a #Z (m-n) = a |^ n by A3;
a |^ n <> 0 by A1,Th5;
hence thesis by A4,XCMPLX_1:54;
end;
end;
theorem Th44:
a<>0 implies a #Z (k+l) = a #Z k * a #Z l
proof
assume
A1: a<>0;
per cases;
suppose
A2: k>=0 & l>=0;
then
A3: k*l>=0;
thus a #Z (k+l) = a |^ |.k+l.| by A2,Def3
.= a |^ (|.k.|+|.l.|) by A3,ABSVALUE:11
.= a |^ |.k.| * a |^ |.l.| by NEWTON:8
.= a #Z k * a |^ |.l.| by A2,Def3
.= a #Z k * a #Z l by A2,Def3;
end;
suppose
A4: k>=0 & l<0;
then reconsider m = k as Element of NAT by INT_1:3;
reconsider n = -l as Element of NAT by A4,INT_1:3;
k+l = m - n;
hence a #Z (k+l) = a |^ m / a |^ n by A1,Th43
.= a |^ m * (a |^ n)"
.= a |^ |.k.| * (a |^ n)" by ABSVALUE:def 1
.= a |^ |.k.| * (a |^ |.-l.|)" by ABSVALUE:def 1
.= a |^ |.k.| * (a |^ |.l.|)" by COMPLEX1:52
.= a #Z k * (a |^ |.l.|)" by A4,Def3
.= a #Z k * a #Z l by A4,Def3;
end;
suppose
A5: k<0 & l>=0;
then reconsider m = l as Element of NAT by INT_1:3;
reconsider n = -k as Element of NAT by A5,INT_1:3;
k+l = m - n;
hence a #Z (k+l) = a |^ m / a |^ n by A1,Th43
.= a |^ m * (a |^ n)"
.= a |^ |.l.| * (a |^ n)" by ABSVALUE:def 1
.= a |^ |.l.| * (a |^ |.-k.|)" by ABSVALUE:def 1
.= a |^ |.l.| * (a |^ |.k.|)" by COMPLEX1:52
.= a #Z l * (a |^ |.k.|)" by A5,Def3
.= a #Z k * a #Z l by A5,Def3;
end;
suppose
A6: k<0 & l<0;
then
A7: k*l>=0;
thus a #Z (k+l) = (a |^ |.k+l.|)" by A6,Def3
.= (a |^ (|.k.|+|.l.|))" by A7,ABSVALUE:11
.= (a |^ |.k.| * a |^ |.l.|)" by NEWTON:8
.= (a |^ |.k.|)" * (a |^ |.l.|)" by XCMPLX_1:204
.= a #Z k * (a |^ |.l.|)" by A6,Def3
.= a #Z k * a #Z l by A6,Def3;
end;
end;
theorem Th45:
a #Z k #Z l = a #Z (k*l)
proof
per cases;
suppose
A1: k*l > 0;
per cases by A1,XREAL_1:134;
suppose
A2: k>0 & l>0;
hence a #Z k #Z l = a #Z k |^ |.l.| by Def3
.=a |^ |.k.| |^ |.l.| by A2,Def3
.=a |^ (|.k.|*|.l.|) by NEWTON:9
.=a |^ |.k*l.| by COMPLEX1:65
.=a #Z (k*l) by A1,Def3;
end;
suppose
A3: k<0 & l<0;
hence a #Z k #Z l = (a #Z k |^ |.l.|)" by Def3
.=(((a |^ |.k.|)") |^ |.l.|)" by A3,Def3
.=((1 / a |^ |.k.|) |^ |.l.|)"
.=(1 / a |^ |.k.| |^ |.l.|)" by Th7
.=(a |^ |.k.| |^ |.l.|)""
.=a |^ (|.k.|*|.l.|) by NEWTON:9
.=a |^ |.k*l.| by COMPLEX1:65
.=a #Z (k*l) by A1,Def3;
end;
end;
suppose
A4: k*l < 0;
per cases by A4,XREAL_1:133;
suppose
A5: k<0 & l>0;
hence a #Z k #Z l = a #Z k |^ |.l.| by Def3
.=((a |^ |.k.|)") |^ |.l.| by A5,Def3
.=(1 / a |^ |.k.|) |^ |.l.|
.=1 / a |^ |.k.| |^ |.l.| by Th7
.=1 / a |^ (|.k.|*|.l.|) by NEWTON:9
.=1 / a |^ |.k*l.| by COMPLEX1:65
.=(a |^ |.k*l.|)"
.=a #Z (k*l) by A4,Def3;
end;
suppose
A6: k>0 & l<0;
hence a #Z k #Z l = (a #Z k |^ |.l.|)" by Def3
.=(a |^ |.k.| |^ |.l.|)" by A6,Def3
.=(a |^ (|.k.|*|.l.|))" by NEWTON:9
.=(a |^ |.k*l.|)" by COMPLEX1:65
.=a #Z (k*l) by A4,Def3;
end;
end;
suppose
A7: k*l = 0;
per cases by A7;
suppose
k=0;
hence a #Z k #Z l = 1 #Z l by Th34
.= 1 by Th37
.= a #Z (k*l) by A7,Th34;
end;
suppose
l=0;
hence a #Z k #Z l = 1 by Th34
.= a #Z (k*l) by A7,Th34;
end;
end;
end;
theorem Th46:
a>0 & n>=1 implies (n -Root a) #Z k = n -Root (a #Z k)
proof
assume that
A1: a>0 and
A2: n>=1;
A3: n -Root a > 0 by A1,A2,Def2;
A4: m>=1 implies (n -Root a) |^ m = n -Root (a |^ m)
proof
assume that
A5: m>=1 and
A6: (n -Root a) |^ m <> n -Root (a |^ m);
A7: a |^ m > 0 by A1,Th6;
then
A8: n -Root (a |^ m) >= 0 by A2,Def2;
A9: m -Root (n -Root (a |^ m)) = (n*m) -Root (a |^ m) by A2,A5,A7,Th25
.= n -Root (m -Root (a |^ m)) by A2,A5,A7,Th25
.= n -Root a by A1,A5,Lm2;
A10: m -Root ((n -Root a) |^ m) = n -Root a by A3,A5,Lm2;
A11: (n -Root a) |^ m >= 0 by A3,Th6;
per cases by A6,XXREAL_0:1;
suppose
(n -Root a) |^ m < n -Root (a |^ m);
hence contradiction by A5,A9,A11,Lm2;
end;
suppose
(n -Root a) |^ m > n -Root (a |^ m);
hence contradiction by A5,A9,A10,A8,Th28;
end;
end;
per cases;
suppose
A12: k>0;
then |.k.|>0 by ABSVALUE:def 1;
then
A13: |.k.|>=0+1 by NAT_1:13;
thus (n -Root a) #Z k = (n -Root a) |^ |.k.| by A12,Def3
.= n -Root (a |^ |.k.|) by A4,A13
.= n -Root (a #Z k) by A12,Def3;
end;
suppose
A14: k<0;
then |.k.|>0 by COMPLEX1:47;
then
A15: |.k.|>=0+1 by NAT_1:13;
A16: a |^ |.k.| > 0 by A1,Th6;
thus (n -Root a) #Z k = ((n -Root a) |^ |.k.|)" by A14,Def3
.= (n -Root (a |^ |.k.|))" by A4,A15
.= 1/n -Root (a |^ |.k.|)
.= n -Root (1/a |^ |.k.|) by A2,A16,Th23
.= n -Root ((a |^ |.k.|)")
.= n -Root (a #Z k) by A14,Def3;
end;
suppose
A17: k=0;
then n -Root (a #Z k) = n -Root 1 by Th34
.= 1 by A2,Th20;
hence thesis by A17,Th34;
end;
end;
definition
let a be Real;
let p be Rational;
func a #Q p -> number equals
(denominator p) -Root (a #Z numerator p);
coherence by TARSKI:1;
end;
registration
let a be Real;
let p be Rational;
cluster a #Q p -> real;
coherence;
end;
theorem Th47:
p = 0 implies a #Q p = 1
proof
reconsider i = 0 as Integer;
assume that
A1: p=0;
numerator(p)=0 by A1;
thus a #Q p = 1 -Root (a #Z i) by A1,RAT_1:19
.= 1 -Root 1 by Th34
.= 1 by Th21;
end;
theorem Th48:
a > 0 & p = 1 implies a #Q p = a
proof
assume that
A1: a>0 and
A2: p=1;
A3: denominator(p)=1 by A2,RAT_1:17;
numerator(p)=p by A2;
thus a #Q p = 1 -Root a by A2,A3,Th35
.= a by A1,Th21;
end;
Lm5: a>=0 implies a #Z k >= 0
proof
assume
A1: a>=0;
per cases by A1;
suppose
A2: a = 0;
|.k.| = 0 or |.k.| >= 1 by NAT_1:14;
then (0 |^ |.k.|)" = 0" or (0 |^ |.k.|)" = 1" by NEWTON:4,11;
hence thesis by A2,Def3;
end;
suppose
a > 0;
hence thesis by Th39;
end;
end;
theorem Th49:
for n be Nat st 0 <= a holds a #Q n = a |^ n
proof
let n be Nat;
A1: denominator n=1 by RAT_1:17;
A2: numerator n=n;
assume 0 <= a;
hence a #Q n = a #Z n by A1,Lm5,Th21
.= a |^ n by Th36;
end;
theorem Th50:
for n be Nat holds n>=1 & p = n" implies a #Q p = n -Root a
proof
let n be Nat;
assume that
A1: n>=1 and
A2: p = n";
reconsider q=n as Rational;
A3: p=1/n by A2;
then denominator(p)=numerator(q) by A1,RAT_1:44;
then
A4: denominator(p) = n;
numerator(p)=denominator(q) by A1,A3,RAT_1:44;
then numerator(p) = 1 by RAT_1:17;
hence thesis by A4,Th35;
end;
theorem Th51:
1 #Q p = 1
proof
thus 1 #Q p = (denominator(p)) -Root 1 by Th37
.= 1 by Th20,RAT_1:11;
end;
theorem Th52:
a>0 implies a #Q p > 0
proof
assume a>0;
then
A1: a #Z numerator(p) > 0 by Th39;
denominator(p) >= 1 by RAT_1:11;
hence thesis by A1,Def2;
end;
theorem Th53:
a>0 implies a #Q p * a #Q q = a #Q (p+q)
proof
set dp = denominator(p);
set dq = denominator(q);
set np = numerator(p);
set nq = numerator(q);
A1: dp >= 1 by RAT_1:11;
reconsider ddq=dq as Integer;
reconsider ddp=dp as Integer;
A2: denominator(p+q) >= 1 by RAT_1:11;
A3: dq >= 1 by RAT_1:11;
then
A4: dp*dq >= 1 by A1,XREAL_1:159;
p+q = np/dp + q
.= np/dp + nq/dq
.= (np*dq+nq*dp)/(dp*dq) by XCMPLX_1:116;
then consider n such that
A5: np*dq+nq*dp = numerator(p+q)*n and
A6: dp*dq = denominator(p+q)*n by RAT_1:27;
reconsider k=n as Integer;
assume
A7: a>0;
then
A8: a #Z (nq-np) >= 0 by Th39;
n>0 by A6;
then
A9: n>=0+1 by NAT_1:13;
A10: a #Z np > 0 by A7,Th39;
then
A11: (a #Z np) |^ (dp+dq)>= 0 by Th6;
A12: a #Z (nq-np) > 0 by A7,Th39;
then
A13: (a #Z (nq-np)) |^ dp >= 0 by Th6;
A14: a #Q (p+q) > 0 by A7,Th52;
A15: a #Z numerator(p+q) > 0 by A7,Th39;
thus a #Q p * a #Q q = dp -Root (a #Z np) * dq -Root (a #Z (np+(nq-np)))
.= dp -Root (a #Z np) * dq -Root (a #Z np * a #Z (nq-np)) by A7,Th44
.= dp -Root (a #Z np)*(dq -Root (a #Z np)*dq -Root (a #Z (nq-np))) by A10
,A8,Th22,RAT_1:11
.= dp -Root (a #Z np) * dq -Root (a #Z np) * dq -Root (a #Z (nq-np))
.= (dp*dq) -Root ((a #Z np) |^ (dp+dq))*dq -Root (a #Z (nq-np)) by A10,A3
,A1,Th26
.= (dp*dq) -Root ((a #Z np) |^ (dp+dq)) * dq -Root (dp -Root ((a #Z (nq-
np)) |^ dp)) by A12,A1,Lm2
.= (dp*dq) -Root ((a #Z np) |^ (dp+dq)) * (dp*dq) -Root ((a #Z (nq-np))
|^ dp) by A3,A1,A13,Th25
.= (dp*dq) -Root (((a #Z np) |^ (dp+dq)) * ((a #Z (nq-np)) |^ dp)) by A3,A1
,A13,A11,Th22,XREAL_1:159
.= (dp*dq) -Root (((a #Z np) #Z (ddp+ddq)) * ((a #Z (nq-np)) |^ dp)) by
Th36
.= (dp*dq) -Root (((a #Z np) #Z (ddp+ddq)) * ((a #Z (nq-np)) #Z ddp)) by
Th36
.= (dp*dq) -Root ( a #Z (np*(ddp+ddq)) * ((a #Z (nq-np)) #Z ddp) ) by Th45
.= (dp*dq) -Root ( a #Z (np*(ddp+ddq)) * a #Z ((nq-np)*ddp) ) by Th45
.= (dp*dq) -Root (a #Z (np*ddp+np*ddq+(nq-np)*ddp) ) by A7,Th44
.= (denominator(p+q)*n) -Root (a #Z numerator(p+q) #Z k) by A5,A6,Th45
.= ((denominator(p+q)*n) -Root (a #Z numerator(p+q))) #Z k by A4,A6,A15
,Th46
.= ((n*denominator(p+q)) -Root (a #Z numerator(p+q))) |^ n by Th36
.= (n -Root (a #Q (p+q))) |^ n by A9,A2,A15,Th25
.= a #Q (p+q) by A9,A14,Lm2;
end;
theorem Th54:
a>0 implies 1 / a #Q p = a #Q (-p)
proof
assume a>0;
then
A1: a #Z numerator(p) > 0 by Th39;
thus a #Q (-p) = (denominator(-p)) -Root (a #Z (-numerator(p))) by RAT_1:43
.= (denominator(p)) -Root (a #Z (-numerator(p))) by RAT_1:43
.= (denominator(p)) -Root (1/a #Z numerator(p)) by Th41
.= 1 / a #Q p by A1,Th23,RAT_1:11;
end;
theorem Th55:
a>0 implies a #Q p / a #Q q = a #Q (p-q)
proof
assume
A1: a>0;
thus a #Q (p-q) = a #Q (p+-q) .= a #Q p * a #Q (-q) by A1,Th53
.= a #Q p * (1/a #Q q) by A1,Th54
.= a #Q p * 1 / a #Q q
.= a #Q p / a #Q q;
end;
theorem Th56:
a>0 & b>0 implies (a*b) #Q p = a #Q p * b #Q p
proof
assume that
A1: a>0 and
A2: b>0;
A3: a #Z numerator(p) >= 0 by A1,Th39;
A4: b #Z numerator(p) >= 0 by A2,Th39;
thus (a*b) #Q p = (denominator(p)) -Root (a #Z numerator(p) * b #Z numerator
(p)) by Th40
.= a #Q p * b #Q p by A3,A4,Th22,RAT_1:11;
end;
theorem Th57:
a>0 implies (1/a) #Q p = 1/a #Q p
proof
assume
A1: a>0;
thus (1/a) #Q p = (denominator(p)) -Root (1/a #Z numerator(p)) by Th42
.= (denominator(p)) -Root (a #Z (-numerator(p))) by Th41
.= (denominator(p)) -Root (a #Z numerator(-p)) by RAT_1:43
.= a #Q (-p) by RAT_1:43
.= 1/a #Q p by A1,Th54;
end;
theorem Th58:
a>0 & b>0 implies (a/b) #Q p = a #Q p / b #Q p
proof
assume that
A1: a>0 and
A2: b>0;
thus (a/b) #Q p = (a*(1/b)) #Q p .= a #Q p * (1/b) #Q p by A1,A2,Th56
.= a #Q p * (1/b #Q p) by A2,Th57
.= a #Q p / b #Q p;
end;
theorem Th59:
a > 0 implies a #Q p #Q q = a #Q (p*q)
proof
A1: denominator(p)>=1 by RAT_1:11;
p = numerator(p)/denominator(p);
p*q = (numerator(p)/denominator(p))*(numerator(q)/denominator(q))
.= (numerator(p)/denominator(p))*numerator(q)/denominator(q)
.= (numerator(p)*numerator(q))/(denominator(p)*denominator(q)) by
XCMPLX_1:83;
then consider n such that
A2: numerator(p)*numerator(q) = numerator(p*q)*n and
A3: denominator(p)*denominator(q) = denominator(p*q)*n by RAT_1:27
;
A4: denominator(p*q)*n >= 0+1 by A3,NAT_1:13;
n>0 by A3;
then
A5: n>=0+1 by NAT_1:13;
reconsider k=n as Integer;
A6: denominator(q)>=1 by RAT_1:11;
A7: denominator(p*q) >= 1 by RAT_1:11;
assume
A8: a>0;
then
A9: a #Z (numerator(p)*numerator(q)) >= 0 by Th39;
A10: a #Q (p*q) > 0 by A8,Th52;
A11: a #Z numerator(p*q) > 0 by A8,Th39;
a #Z numerator(p) > 0 by A8,Th39;
hence a #Q p #Q q = (denominator(q)) -Root ((denominator(p)) -Root (a #Z
numerator(p) #Z numerator(q))) by Th46,RAT_1:11
.= (denominator(q)) -Root ((denominator(p)) -Root (a #Z (numerator(p)*
numerator(q)))) by Th45
.= (denominator(p*q)*n) -Root (a #Z (numerator(p*q)*k)) by A1,A6,A9,A2,A3
,Th25
.= (denominator(p*q)*n) -Root (a #Z numerator(p*q) #Z k) by Th45
.= ((denominator(p*q)*n) -Root (a #Z numerator(p*q))) #Z k by A11,A4,Th46
.= ((n*denominator(p*q)) -Root (a #Z numerator(p*q))) |^ n by Th36
.= (n -Root (a #Q (p*q))) |^ n by A5,A7,A11,Th25
.= a #Q (p*q) by A5,A10,Lm2;
end;
theorem Th60:
a>=1 & p >= 0 implies a #Q p >= 1
proof
assume that
A1: a>=1 and
A2: p>=0;
numerator(p)>=0 by A2;
then reconsider n = numerator(p) as Element of NAT by INT_1:3;
A3: a #Z numerator(p) = a |^ n by Th36;
a |^ n >= 1 |^ n by A1,Th9;
then
A4: a #Z numerator(p) >= 1 by A3;
denominator(p) >= 1 by RAT_1:11;
hence thesis by A4,Th29;
end;
theorem Th61:
a>=1 & p<=0 implies a #Q p <= 1
proof
assume that
A1: a>=1 and
A2: p<=0;
a #Q (-p) >= 1 by A1,A2,Th60;
then 1 / a #Q p >= 1 by A1,Th54;
hence thesis by XREAL_1:191;
end;
theorem Th62:
a>1 & p>0 implies a #Q p > 1
proof
assume that
A1: a>1 and
A2: p>0;
A3: numerator(p)>0 by A2;
then reconsider n = numerator(p) as Element of NAT by INT_1:3;
n>=0+1 by A3,NAT_1:13;
then
A4: a |^ n > 1 |^ n by A1,Lm1;
a #Z numerator(p) = a |^ n by Th36;
then a #Z numerator(p) > 1 by A4;
then (denominator(p)) -Root (a #Z numerator(p))>(denominator(p)) -Root 1 by
Th28,RAT_1:11;
hence thesis by Th20,RAT_1:11;
end;
theorem Th63:
a>=1 & p>=q implies a #Q p >= a #Q q
proof
assume that
A1: a>=1 and
A2: p>=q;
per cases by A2,XXREAL_0:1;
suppose
p=q;
hence thesis;
end;
suppose
p>q;
then
A3: p-q>=0 by XREAL_1:50;
A4: a #Q q <> 0 by A1,Th52;
A5: a #Q p / a #Q q = a #Q (p-q) by A1,Th55;
a #Q q >= 0 by A1,Th52;
then a #Q p / a #Q q * a #Q q >= 1 * a #Q q by A1,A3,A5,Th60,XREAL_1:64;
hence thesis by A4,XCMPLX_1:87;
end;
end;
theorem Th64:
a>1 & p>q implies a #Q p > a #Q q
proof
assume that
A1: a>1 and
A2: p>q;
A3: p-q>0 by A2,XREAL_1:50;
A4: a #Q p / a #Q q = a #Q (p-q) by A1,Th55;
A5: a #Q q <> 0 by A1,Th52;
a #Q q > 0 by A1,Th52;
then a #Q p / a #Q q * a #Q q > 1 * a #Q q by A1,A3,A4,Th62,XREAL_1:68;
hence thesis by A5,XCMPLX_1:87;
end;
theorem Th65:
a>0 & a<1 & p>0 implies a #Q p < 1
proof
reconsider q=0 as Rational;
assume that
A1: a>0 and
A2: a<1 and
A3: p>0;
1/a>1 by A1,A2,Lm4,XREAL_1:88;
then (1/a) #Q p > (1/a) #Q q by A3,Th64;
then (1/a) #Q p > 1 by Th47;
then 1/a #Q p > 1 by A1,Th57;
hence thesis by XREAL_1:185;
end;
theorem
a>0 & a<=1 & p<=0 implies a #Q p >= 1
proof
assume that
A1: a>0 and
A2: a<=1 and
A3: p<=0;
1/a >= 1 by A1,A2,Lm4,XREAL_1:85;
then (1/a) #Q p <= 1 by A3,Th61;
then
A4: 1/a #Q p <= 1 by A1,Th57;
a #Q p > 0 by A1,Th52;
hence thesis by A4,XREAL_1:187;
end;
registration
cluster RAT-valued for Real_Sequence;
existence
proof
take seq_const 0;
thus thesis;
end;
end;
definition
::$CD
mode Rational_Sequence is RAT-valued Real_Sequence;
end;
theorem Th67:
for a be Real ex s being Rational_Sequence st
s is convergent & lim s = a & for n holds s.n<=a
proof
let a be Real;
deffunc O(Nat) = [\($1+1)*a/]/($1+1);
consider s being Real_Sequence such that
A1: for n holds s.n = O(n) from SEQ_1:sch 1;
rng s c= RAT
proof
let y be object;
assume y in rng s;
then consider n being Element of NAT such that
A2: s.n = y by FUNCT_2:113;
s.n = O(n) by A1;
hence thesis by A2,RAT_1:def 2;
end;
then reconsider s as Rational_Sequence by RELAT_1:def 19;
deffunc O(Nat) = 1/($1+1);
consider s2 being Real_Sequence such that
A3: for n holds s2.n = O(n) from SEQ_1:sch 1;
reconsider a1 = a as Element of REAL by XREAL_0:def 1;
set s1 = seq_const a;
take s;
set s3 = s1 - s2;
A4: s2 is convergent by A3,SEQ_4:31;
then
A5: s3 is convergent;
A6: now
let n;
(n+1)*a <= [\(n+1)*a/] + 1 by INT_1:29;
then (n+1)*a - 1 <= [\(n+1)*a/] + 1 - 1 by XREAL_1:9;
then ((n+1)*a - 1)*(n+1)" <= [\(n+1)*a/]/(n+1) by XREAL_1:64;
then (a/(n+1))*(n+1) - 1/(n+1) <= s.n by A1;
then a - 1/(n+1) <= s.n by XCMPLX_1:87;
then s1.n - 1/(n+1) <= s.n by SEQ_1:57;
then
A7: s1.n - s2.n <= s.n by A3;
[\(n+1)*a/] <= (n+1)*a by INT_1:def 6;
then [\(n+1)*a/]*(n+1)" <= a*(n+1)*(n+1)" by XREAL_1:64;
then [\(n+1)*a/]*(n+1)" <= a*((n+1)*(n+1)");
then [\(n+1)*a/]*(n+1)" <= a*1 by XCMPLX_0:def 7;
then [\(n+1)*a/]/(n+1) <= s1.n by SEQ_1:57;
hence s3.n <= s.n & s.n <= s1.n by A1,A7,RFUNCT_2:1;
end;
lim s2 = 0 by A3,SEQ_4:31;
then
A8: lim s3 = s1.0 - 0 by A4,SEQ_4:42
.= a by SEQ_1:57;
A9: lim s1 = s1.0 by SEQ_4:26
.= a by SEQ_1:57;
hence s is convergent by A5,A8,A6,SEQ_2:19;
thus lim s = a by A5,A8,A9,A6,SEQ_2:20;
let n;
s.n<=s1.n by A6;
hence thesis by SEQ_1:57;
end;
theorem Th68:
ex s being Rational_Sequence st s is convergent & lim s = a &
for n holds s.n>=a
proof
deffunc O(Nat) = [/($1+1)*a\]/($1+1);
consider s being Real_Sequence such that
A1: for n holds s.n = O(n) from SEQ_1:sch 1;
rng s c= RAT
proof
let y be object;
assume y in rng s;
then consider n being Element of NAT such that
A2: s.n = y by FUNCT_2:113;
s.n = O(n) by A1;
hence thesis by A2,RAT_1:def 2;
end;
then reconsider s as Rational_Sequence by RELAT_1:def 19;
deffunc O(Nat) = 1/($1+1);
consider s2 being Real_Sequence such that
A3: for n holds s2.n = O(n) from SEQ_1:sch 1;
take s;
set s1 = seq_const a;
set s3 = s1 + s2;
A4: s2 is convergent by A3,SEQ_4:31;
then
A5: s3 is convergent;
A6: now
let n;
(n+1)*a + 1 >= [/(n+1)*a\] by INT_1:def 7;
then ((n+1)*a + 1)*(n+1)" >= [/(n+1)*a\]/(n+1) by XREAL_1:64;
then (a/(n+1))*(n+1) + 1/(n+1) >= s.n by A1;
then a + 1/(n+1) >= s.n by XCMPLX_1:87;
then s1.n + 1/(n+1) >= s.n by SEQ_1:57;
then
A7: s1.n + s2.n >= s.n by A3;
[/(n+1)*a\] >= (n+1)*a by INT_1:def 7;
then [/(n+1)*a\]*(n+1)" >= a*(n+1)*(n+1)" by XREAL_1:64;
then [/(n+1)*a\]*(n+1)" >= a*((n+1)*(n+1)");
then [/(n+1)*a\]*(n+1)" >= a*1 by XCMPLX_0:def 7;
then [/(n+1)*a\]/(n+1) >= s1.n by SEQ_1:57;
hence s1.n <= s.n & s.n <= s3.n by A1,A7,SEQ_1:7;
end;
lim s2 = 0 by A3,SEQ_4:31;
then
A8: lim s3 = s1.0 + 0 by A4,SEQ_4:42
.= a by SEQ_1:57;
A9: lim s1 = s1.0 by SEQ_4:26
.= a by SEQ_1:57;
hence s is convergent by A5,A8,A6,SEQ_2:19;
thus lim s = a by A5,A8,A9,A6,SEQ_2:20;
let n;
s.n>=s1.n by A6;
hence thesis by SEQ_1:57;
end;
definition
let a be Real;
let s be Rational_Sequence;
func a #Q s -> Real_Sequence means
:Def5:
for n holds it.n = a #Q (s.n);
existence
proof
deffunc O(Nat) = a #Q (s.$1);
consider s1 being Real_Sequence such that
A1: for n holds s1.n = O(n) from SEQ_1:sch 1;
take s1;
thus thesis by A1;
end;
uniqueness
proof
let s1,s2 be Real_Sequence;
assume that
A2: for n holds s1.n = a #Q (s.n) and
A3: for n holds s2.n = a #Q (s.n);
now
let n be Element of NAT;
thus s1.n = a #Q (s.n) by A2
.= s2.n by A3;
end;
hence thesis by FUNCT_2:63;
end;
end;
Lm6: for s being Rational_Sequence, a st s is convergent & a>=1 holds a #Q s
is convergent
proof
let s be Rational_Sequence;
let a;
assume that
A1: s is convergent and
A2: a>=1;
s is bounded by A1;
then consider d be Real such that
0<d and
A3: for n holds |.s.n.|<d by SEQ_2:3;
consider m2 such that
A4: d<m2 by SEQ_4:3;
reconsider m2 as Rational;
now
A5: a #Q m2 >= 0 by A2,Th52;
let c be Real;
assume
A6: c>0;
consider m1 such that
A7: a #Q m2*(a-1)/c < m1 by SEQ_4:3;
m1+1>=m1 by XREAL_1:29;
then a #Q m2 * (a-1)/c < m1+1 by A7,XXREAL_0:2;
then a #Q m2 * (a-1)/c*c < c*(m1+1) by A6,XREAL_1:68;
then a #Q m2 * (a-1) < c*(m1+1) by A6,XCMPLX_1:87;
then a #Q m2 * (a-1)/(m1+1) < (m1+1)*c/(m1+1) by XREAL_1:74;
then a #Q m2 * (a-1)/(m1+1) < c/(m1+1)*(m1+1);
then
A8: a #Q m2 * (a-1)/(m1+1) < c by XCMPLX_1:87;
consider n such that
A9: for m st n<=m holds |.s.m -s.n.|<(m1+1)" by A1,SEQ_4:41;
take n;
let m;
assume m>=n;
then
A10: |.s.m-s.n.|<=(m1+1)" by A9;
A11: m1+1>=0+1 by NAT_1:13;
then (m1+1) -Root a - 1 <= (a-1)/(m1+1) by A2,Th31;
then
A12: (a #Q m2)*((m1+1) -Root a - 1) <= (a #Q m2)*((a-1)/(m1+1)) by A5,
XREAL_1:64;
A13: a #Q (s.n) <> 0 by A2,Th52;
A14: |.a #Q (s.m) - a #Q (s.n).| = |.(a #Q (s.m) - a #Q (s.n))*1.|
.=|.(a #Q (s.m) - a #Q (s.n))*(a #Q (s.n)/a #Q (s.n)).| by A13,
XCMPLX_1:60
.=|.a #Q (s.n)*(a #Q (s.m) - a #Q (s.n))/a #Q (s.n).|
.=|.a #Q (s.n)*((a #Q (s.m) - a #Q (s.n))/a #Q (s.n)).|
.=|.a #Q (s.n).|*|.(a #Q (s.m) - a #Q (s.n))/a #Q (s.n).| by
COMPLEX1:65
.=|.a #Q (s.n).|*|.a #Q (s.m)/a #Q (s.n) - a #Q (s.n)/a #Q (s.n).|
.=|.a #Q (s.n).|*|.a #Q (s.m)/a #Q (s.n) - 1.| by A13,XCMPLX_1:60
.=|.a #Q (s.n).|*|.a #Q (s.m-s.n) - 1.| by A2,Th55;
A15: s.n<=|.s.n.| by ABSVALUE:4;
reconsider m3 = (m1+1)" as Rational;
A16: |.a #Q (s.m-s.n) - 1.| >= 0 by COMPLEX1:46;
A17: a #Q (s.m-s.n) <> 0 by A2,Th52;
s.m -s.n<=|.s.m-s.n.| by ABSVALUE:4;
then s.m -s.n <= (m1+1)" by A10,XXREAL_0:2;
then a #Q (s.m-s.n) <= a #Q m3 by A2,Th63;
then a #Q (s.m-s.n) <= (m1+1) -Root a by A11,Th50;
then
A18: a #Q (s.m-s.n) - 1 <= (m1+1) -Root a - 1 by XREAL_1:9;
A19: a #Q (s.m-s.n) > 0 by A2,Th52;
A20: now
per cases;
suppose
s.m-s.n>=0;
then a #Q (s.m-s.n) >= 1 by A2,Th60;
then a #Q (s.m-s.n) - 1 >= 0 by XREAL_1:48;
hence |.a #Q (s.m-s.n) - 1.| <= (m1+1) -Root a - 1 by A18,
ABSVALUE:def 1;
end;
suppose
A21: s.m-s.n<0;
A22: -(s.m -s.n)<=|.-(s.m -s.n).| by ABSVALUE:4;
|.s.m-s.n.| = |.-(s.m -s.n).| by COMPLEX1:52;
then -(s.m -s.n) <= m3 by A10,A22,XXREAL_0:2;
then a #Q (-(s.m-s.n)) <= a #Q m3 by A2,Th63;
then a #Q (-(s.m-s.n)) <= (m1+1) -Root a by A11,Th50;
then
A23: a #Q (-(s.m-s.n)) - 1 <= (m1+1) -Root a - 1 by XREAL_1:9;
a #Q (-(s.m-s.n)) >= 1 by A2,A21,Th60;
then a #Q (-(s.m-s.n)) - 1 >= 0 by XREAL_1:48;
then
A24: |.a #Q (-(s.m-s.n)) - 1.| <= (m1+1) -Root a - 1 by A23,ABSVALUE:def 1;
a #Q (s.m-s.n) <= 1 by A2,A21,Th61;
then
A25: |.a #Q (s.m-s.n).| <= 1 by A19,ABSVALUE:def 1;
|.a #Q (-(s.m-s.n)) - 1.| >= 0 by COMPLEX1:46;
then
A26: |.a #Q (s.m-s.n).|*|.a #Q (-(s.m-s.n)) - 1.| <= 1*|.a #Q (-(s
.m-s.n)) - 1.| by A25,XREAL_1:64;
|.a #Q (s.m-s.n) - 1.| = |.(a #Q (s.m-s.n) - 1)*1.|
.= |.(a #Q (s.m-s.n) - 1)*(a #Q (s.m-s.n)/a #Q (s.m-s.n)).| by A17,
XCMPLX_1:60
.= |.a #Q (s.m-s.n)*(a #Q (s.m-s.n) - 1)/a #Q (s.m-s.n).|
.= |.a #Q (s.m-s.n)*((a #Q (s.m-s.n) - 1)/a #Q (s.m-s.n)).|
.= |.a #Q (s.m-s.n).|*|.(a #Q (s.m-s.n) - 1)/a #Q (s.m-s.n).| by
COMPLEX1:65
.= |.a #Q (s.m-s.n).|*|.a #Q (s.m-s.n)/a #Q (s.m-s.n) - 1/a #Q
(s.m-s.n).|
.= |.a #Q (s.m-s.n).|*|.1 - 1/a #Q (s.m-s.n).| by A17,XCMPLX_1:60
.= |.a #Q (s.m-s.n).|*|.1 - a #Q (-(s.m-s.n)).| by A2,Th54
.= |.a #Q (s.m-s.n).|*|.-(1 - a #Q (-(s.m-s.n))).| by COMPLEX1:52
.= |.a #Q (s.m-s.n).|*|.a #Q (-(s.m-s.n)) - 1.|;
hence |.a #Q (s.m-s.n) - 1.| <= (m1+1) -Root a - 1 by A24,A26,
XXREAL_0:2;
end;
end;
A27: a #Q (s.n) > 0 by A2,Th52;
|.s.n.|<=m2 by A3,A4,XXREAL_0:2;
then s.n<=m2 by A15,XXREAL_0:2;
then a #Q (s.n) <= a #Q m2 by A2,Th63;
then
A28: |.a #Q (s.n).| <= a #Q m2 by A27,ABSVALUE:def 1;
|.a #Q (s.n).| >= 0 by A27,ABSVALUE:def 1;
then |.a #Q (s.n).|*|.a #Q (s.m-s.n) - 1.| <= (a #Q m2)*((m1+1) -Root a
- 1) by A20,A16,A28,XREAL_1:66;
then |.a #Q (s.m) - a #Q (s.n).| <= (a #Q m2)*(a-1)/(m1+1) by A14,A12,
XXREAL_0:2;
then |.a #Q (s.m) - a #Q (s.n).| < c by A8,XXREAL_0:2;
then |.(a #Q s).m - a #Q (s.n).| < c by Def5;
hence |.(a #Q s).m - (a #Q s).n.| < c by Def5;
end;
hence thesis by SEQ_4:41;
end;
theorem Th69:
for s being Rational_Sequence st s is convergent & a>0 holds a
#Q s is convergent
proof
let s be Rational_Sequence;
assume that
A1: s is convergent and
A2: a>0;
per cases;
suppose
a>=1;
hence thesis by A1,Lm6;
end;
suppose
A3: a<1;
then a/a<1/a by A2,XREAL_1:74;
then 1<1/a by A2,XCMPLX_1:60;
then
A4: (1/a) #Q s is convergent by A1,Lm6;
s is bounded by A1;
then consider d be Real such that
0<d and
A5: for n holds |.s.n.|<d by SEQ_2:3;
reconsider d as Real;
consider m1 such that
A6: 2*d < m1 by SEQ_4:3;
reconsider m1 as Rational;
A7: a #Q m1 > 0 by A2,Th52;
now
let c be Real;
assume
A8: c>0;
then c* a #Q m1 > 0 by A7;
then consider n such that
A9: for m st n<=m holds |.((1/a) #Q s).m -((1/a) #Q s).n.|<c* a #Q
m1 by A4,SEQ_4:41;
take n;
let m;
assume m>=n;
then
A10: |.((1/a) #Q s).m -((1/a) #Q s).n.|<c* a #Q m1 by A9;
A11: a #Q (s.m) <> 0 by A2,Th52;
A12: a #Q (s.m+s.n) > 0 by A2,Th52;
|.s.m.|<d by A5;
then
A13: |.s.m.|+|.s.n.|<d+d by A5,XREAL_1:8;
|.s.m+s.n.|<=|.s.m.|+|.s.n.| by COMPLEX1:56;
then |.s.m+s.n.|<d+d by A13,XXREAL_0:2;
then |.s.m+s.n.|<m1 by A6,XXREAL_0:2;
then
A14: |.-(s.m+s.n).|<m1 by COMPLEX1:52;
-(s.m+s.n)<=|.-(s.m+s.n).| by ABSVALUE:4;
then -(s.m+s.n)<m1 by A14,XXREAL_0:2;
then
A15: m1-(-(s.m+s.n))>0 by XREAL_1:50;
A16: a #Q (s.n) <> 0 by A2,Th52;
|.((1/a) #Q s).m -((1/a) #Q s).n.| = |.(1/a) #Q (s.m) -((1/a) #Q
s) . n.| by Def5
.= |.(1/a) #Q (s.m) -(1/a) #Q (s.n).| by Def5
.= |.1/a #Q (s.m) -(1/a) #Q (s.n).| by A2,Th57
.= |.1/a #Q (s.m) -1/a #Q (s.n).| by A2,Th57
.= |.(a #Q (s.m))" -1/a #Q (s.n).|
.= |.(a #Q (s.m))" -(a #Q (s.n))".|
.= |.a #Q (s.m) - a #Q (s.n).|/(|.a #Q (s.m).|*|.a #Q (s.n).|) by
A11,A16,SEQ_2:2
.= |.a #Q (s.m) - a #Q (s.n).|/|.a #Q (s.m) * a #Q (s.n).| by
COMPLEX1:65
.= |.a #Q (s.m) - a #Q (s.n).|/|.a #Q (s.m+s.n).| by A2,Th53
.= |.a #Q (s.m) - a #Q (s.n).|/(a #Q (s.m+s.n)) by A12,ABSVALUE:def 1;
then
A17: (|.a #Q (s.m) - a #Q (s.n).|/a #Q (s.m+s.n))*a #Q (s.m+s.n) < c*a
#Q m1 * a #Q (s.m+s.n) by A10,A12,XREAL_1:68;
a #Q (s.m+s.n) <> 0 by A2,Th52;
then
A18: |.a #Q (s.m) - a #Q (s.n).|<c * a #Q m1 * a #Q (s.m+s.n) by A17,
XCMPLX_1:87;
a #Q m1 * a #Q (s.m+s.n) = a #Q (m1+(s.m+s.n)) by A2,Th53;
then c*(a #Q m1 * a #Q (s.m+s.n)) < 1*c by A2,A3,A8,A15,Th65,XREAL_1:68;
then |.a #Q (s.m) - a #Q (s.n).|<c by A18,XXREAL_0:2;
then |.(a #Q s).m - a #Q (s.n).| < c by Def5;
hence |.(a #Q s).m - (a #Q s).n.| < c by Def5;
end;
hence thesis by SEQ_4:41;
end;
end;
Lm7: for s1,s2 being Rational_Sequence, a st s1 is convergent & s2 is
convergent & lim s1 = lim s2 & a>=1 holds lim a #Q s1 = lim a #Q s2
proof
let s1,s2 be Rational_Sequence;
let a;
assume that
A1: s1 is convergent and
A2: s2 is convergent and
A3: lim s1 = lim s2 and
A4: a>=1;
A5: s1-s2 is convergent by A1,A2;
A6: a #Q s2 is convergent by A2,A4,Th69;
A7: now
let n be Element of NAT;
thus (((a #Q s1) - (a #Q s2)) + a #Q s2).n = ((a #Q s1) - (a #Q s2)).n + (
a #Q s2).n by SEQ_1:7
.= (a #Q s1).n - (a #Q s2).n + (a #Q s2).n by RFUNCT_2:1
.= (a #Q s1).n;
end;
s2 is bounded by A2;
then consider d be Real such that
0<d and
A8: for n holds |.s2.n.|<d by SEQ_2:3;
consider m2 such that
A9: d<m2 by SEQ_4:3;
reconsider m2 as Rational;
A10: lim(s1-s2) = lim s1 - lim s2 by A1,A2,SEQ_2:12
.= 0 by A3;
A11: now
A12: a #Q m2 >= 0 by A4,Th52;
let c be Real;
assume
A13: c>0;
consider m1 such that
A14: a #Q m2*(a-1)/c < m1 by SEQ_4:3;
m1+1>=m1 by XREAL_1:29;
then a #Q m2 * (a-1)/c < m1+1 by A14,XXREAL_0:2;
then a #Q m2 * (a-1)/c*c < c*(m1+1) by A13,XREAL_1:68;
then a #Q m2 * (a-1) < c*(m1+1) by A13,XCMPLX_1:87;
then a #Q m2 * (a-1)/(m1+1) < (m1+1)*c/(m1+1) by XREAL_1:74;
then a #Q m2 * (a-1)/(m1+1) < c/(m1+1)*(m1+1);
then
A15: a #Q m2 * (a-1)/(m1+1) < c by XCMPLX_1:87;
consider n such that
A16: for m st n<=m holds |.(s1-s2).m -0.|<(m1+1)" by A5,A10,SEQ_2:def 7;
take n;
let m;
assume m>=n;
then |.(s1-s2).m -0.|<(m1+1)" by A16;
then
A17: |.s1.m-s2.m.|<=(m1+1)" by RFUNCT_2:1;
A18: m1+1>=0+1 by NAT_1:13;
then (m1+1) -Root a - 1 <= (a-1)/(m1+1) by A4,Th31;
then
A19: (a #Q m2)*((m1+1) -Root a - 1) <= (a #Q m2)*((a-1)/(m1+1)) by A12,
XREAL_1:64;
A20: a #Q (s2.m) <> 0 by A4,Th52;
A21: |.a #Q (s1.m) - a #Q (s2.m).| = |.(a #Q (s1.m) - a #Q (s2.m))*1.|
.=|.(a #Q (s1.m) - a #Q (s2.m))*(a #Q (s2.m)/a #Q (s2.m)).| by A20,
XCMPLX_1:60
.=|.a #Q (s2.m)*(a #Q (s1.m) - a #Q (s2.m))/a #Q (s2.m).|
.=|.a #Q (s2.m)*((a #Q (s1.m) - a #Q (s2.m))/a #Q (s2.m)).|
.=|.a #Q (s2.m).|*|.(a #Q (s1.m) - a #Q (s2.m))/a #Q (s2.m).| by
COMPLEX1:65
.=|.a #Q (s2.m).|*|.a #Q (s1.m)/a #Q (s2.m) - a #Q (s2.m)/a #Q (s2.
m).|
.=|.a #Q (s2.m).|*|.a #Q (s1.m)/a #Q (s2.m) - 1.| by A20,XCMPLX_1:60
.=|.a #Q (s2.m).|*|.a #Q (s1.m-s2.m) - 1.| by A4,Th55;
A22: s2.m<=|.s2.m.| by ABSVALUE:4;
reconsider m3 = (m1+1)" as Rational;
A23: |.a #Q (s1.m-s2.m) - 1.| >= 0 by COMPLEX1:46;
A24: a #Q (s1.m-s2.m) <> 0 by A4,Th52;
s1.m -s2.m<=|.s1.m-s2.m.| by ABSVALUE:4;
then s1.m -s2.m <= (m1+1)" by A17,XXREAL_0:2;
then a #Q (s1.m-s2.m) <= a #Q m3 by A4,Th63;
then a #Q (s1.m-s2.m) <= (m1+1) -Root a by A18,Th50;
then
A25: a #Q (s1.m-s2.m) - 1 <= (m1+1) -Root a - 1 by XREAL_1:9;
A26: a #Q (s1.m-s2.m) > 0 by A4,Th52;
A27: now
per cases;
suppose
s1.m-s2.m>=0;
then a #Q (s1.m-s2.m) >= 1 by A4,Th60;
then a #Q (s1.m-s2.m) - 1 >= 0 by XREAL_1:48;
hence |.a #Q (s1.m-s2.m) - 1.| <= (m1+1) -Root a - 1 by A25,
ABSVALUE:def 1;
end;
suppose
A28: s1.m-s2.m<0;
A29: -(s1.m -s2.m)<=|.-(s1.m -s2.m).| by ABSVALUE:4;
|.s1.m-s2.m.| = |.-(s1.m -s2.m).| by COMPLEX1:52;
then -(s1.m -s2.m) <= m3 by A17,A29,XXREAL_0:2;
then a #Q (-(s1.m-s2.m)) <= a #Q m3 by A4,Th63;
then a #Q (-(s1.m-s2.m)) <= (m1+1) -Root a by A18,Th50;
then
A30: a #Q (-(s1.m-s2.m)) - 1 <= (m1+1) -Root a - 1 by XREAL_1:9;
a #Q (-(s1.m-s2.m)) >= 1 by A4,A28,Th60;
then a #Q (-(s1.m-s2.m)) - 1 >= 0 by XREAL_1:48;
then
A31: |.a #Q (-(s1.m-s2.m)) - 1.| <= (m1+1) -Root a - 1 by A30,
ABSVALUE:def 1;
a #Q (s1.m-s2.m) <= 1 by A4,A28,Th61;
then
A32: |.a #Q (s1.m-s2.m).| <= 1 by A26,ABSVALUE:def 1;
|.a #Q (-(s1.m-s2.m)) - 1.| >= 0 by COMPLEX1:46;
then
A33: |.a #Q (s1.m-s2.m).|*|.a #Q (-(s1.m-s2.m)) - 1.| <= 1*|.a #Q
(-(s1.m-s2.m)) - 1.| by A32,XREAL_1:64;
|.a #Q (s1.m-s2.m) - 1.| = |.(a #Q (s1.m-s2.m) - 1)*1.|
.= |.(a #Q (s1.m-s2.m) - 1)*(a #Q (s1.m-s2.m)/a #Q (s1.m-s2.m)).|
by A24,XCMPLX_1:60
.= |.a #Q (s1.m-s2.m)*(a #Q (s1.m-s2.m) - 1)/a #Q (s1.m-s2.m).|
.= |.a #Q (s1.m-s2.m)*((a #Q (s1.m-s2.m) - 1)/a #Q (s1.m-s2.m)).|
.= |.a #Q (s1.m-s2.m).|*|.(a #Q (s1.m-s2.m) - 1)/a #Q (s1.m-s2.
m).| by COMPLEX1:65
.= |.a #Q (s1.m-s2.m).|* |.a #Q (s1.m-s2.m)/a #Q (s1.m-s2.m) -
1/a #Q (s1.m-s2.m).|
.= |.a #Q (s1.m-s2.m).|*|.1 - 1/a #Q (s1.m-s2.m).| by A24,
XCMPLX_1:60
.= |.a #Q (s1.m-s2.m).|*|.1 - a #Q (-(s1.m-s2.m)).| by A4,Th54
.= |.a #Q (s1.m-s2.m).|*|.-(1 - a #Q (-(s1.m-s2.m))).| by
COMPLEX1:52
.= |.a #Q (s1.m-s2.m).|*|.a #Q (-(s1.m-s2.m)) - 1.|;
hence |.a #Q (s1.m-s2.m) - 1.| <= (m1+1) -Root a - 1 by A31,A33,
XXREAL_0:2;
end;
end;
A34: a #Q (s2.m) > 0 by A4,Th52;
|.s2.m.|<=m2 by A8,A9,XXREAL_0:2;
then s2.m<=m2 by A22,XXREAL_0:2;
then a #Q (s2.m) <= a #Q m2 by A4,Th63;
then
A35: |.a #Q (s2.m).| <= a #Q m2 by A34,ABSVALUE:def 1;
|.a #Q (s2.m).| >= 0 by A34,ABSVALUE:def 1;
then
|.a #Q (s2.m).|*|.a #Q (s1.m-s2.m) - 1.| <= (a #Q m2)*((m1+1) -Root
a - 1) by A27,A23,A35,XREAL_1:66;
then |.a #Q (s1.m) - a #Q (s2.m).|<= (a #Q m2)*(a-1)/(m1+1) by A21,A19,
XXREAL_0:2;
then |.a #Q (s1.m) - a #Q (s2.m).| < c by A15,XXREAL_0:2;
then |.(a #Q s1).m - a #Q (s2.m).| < c by Def5;
then |.(a #Q s1).m - (a #Q s2).m.| < c by Def5;
hence |.((a #Q s1) - (a #Q s2)).m - 0.| < c by RFUNCT_2:1;
end;
then
A36: ((a #Q s1) - (a #Q s2)) is convergent by SEQ_2:def 6;
then lim((a #Q s1) - (a #Q s2)) = 0 by A11,SEQ_2:def 7;
then lim(((a #Q s1) - (a #Q s2)) + a #Q s2) = 0 + lim a #Q s2 by A36,A6,
SEQ_2:6
.= lim a #Q s2;
hence thesis by A7,FUNCT_2:63;
end;
theorem Th70:
for s1,s2 being Rational_Sequence, a st s1 is convergent & s2 is
convergent & lim s1 = lim s2 & a>0 holds a #Q s1 is convergent & a #Q s2 is
convergent & lim a #Q s1 = lim a #Q s2
proof
let s1,s2 be Rational_Sequence;
let a;
assume that
A1: s1 is convergent and
A2: s2 is convergent and
A3: lim s1 = lim s2 and
A4: a>0;
thus
A5: a #Q s1 is convergent by A1,A4,Th69;
s2 is bounded by A2;
then consider e be Real such that
0<e and
A6: for n holds |.s2.n.|<e by SEQ_2:3;
s1 is bounded by A1;
then consider d be Real such that
0<d and
A7: for n holds |.s1.n.|<d by SEQ_2:3;
consider m1 such that
A8: d+e < m1 by SEQ_4:3;
thus
A9: a #Q s2 is convergent by A2,A4,Th69;
reconsider m1 as Rational;
A10: a #Q m1 > 0 by A4,Th52;
per cases;
suppose
a>=1;
hence thesis by A1,A2,A3,Lm7;
end;
suppose
A11: a<1;
then a/a<1/a by A4,XREAL_1:74;
then 1<1/a by A4,XCMPLX_1:60;
then
A12: lim (1/a) #Q s1 = lim (1/a) #Q s2 by A1,A2,A3,Lm7;
A13: (1/a) #Q s2 is convergent by A2,A4,Th69;
A14: (1/a) #Q s1 is convergent by A1,A4,Th69;
then
A15: (1/a) #Q s1 - (1/a) #Q s2 is convergent by A13;
A16: lim ((1/a) #Q s1 - (1/a) #Q s2) = lim (1/a) #Q s1 - lim (1/a) #Q s2
by A14,A13,SEQ_2:12
.= 0 by A12;
A17: now
let c be Real;
assume
A18: c>0;
then c* a #Q m1 > 0 by A10;
then consider n such that
A19: for m st n<=m holds |.((1/a) #Q s1 - (1/a) #Q s2).m-0.|<c*a #Q
m1 by A15,A16,SEQ_2:def 7;
take n;
let m;
assume m>=n;
then |.((1/a) #Q s1 - (1/a) #Q s2).m-0.|<c*a #Q m1 by A19;
then
A20: |.((1/a) #Q s1).m - ((1/a) #Q s2).m.|<c*a #Q m1 by RFUNCT_2:1;
A21: a #Q (s1.m) <> 0 by A4,Th52;
|.s1.m.|<d by A7;
then
A22: |.s1.m.|+|.s2.m.|<d+e by A6,XREAL_1:8;
|.s1.m+s2.m.|<=|.s1.m.|+|.s2.m.| by COMPLEX1:56;
then |.s1.m+s2.m.|<d+e by A22,XXREAL_0:2;
then |.s1.m+s2.m.|<m1 by A8,XXREAL_0:2;
then
A23: |.-(s1.m+s2.m).|<m1 by COMPLEX1:52;
-(s1.m+s2.m)<=|.-(s1.m+s2.m).| by ABSVALUE:4;
then -(s1.m+s2.m)<m1 by A23,XXREAL_0:2;
then
A24: m1-(-(s1.m+s2.m))>0 by XREAL_1:50;
A25: a #Q (s2.m) <> 0 by A4,Th52;
A26: a #Q (s1.m+s2.m) > 0 by A4,Th52;
|.((1/a) #Q s1).m -((1/a) #Q s2).m.| = |.(1/a) #Q (s1.m) -((1/a)
#Q s2).m.| by Def5
.= |.(1/a) #Q (s1.m) -(1/a) #Q (s2.m).| by Def5
.= |.1/a #Q (s1.m) -(1/a) #Q (s2.m).| by A4,Th57
.= |.1/a #Q (s1.m) -1/a #Q (s2.m).| by A4,Th57
.= |.(a #Q (s1.m))" -1/a #Q (s2.m).|
.= |.(a #Q (s1.m))" -(a #Q (s2.m))".|
.= |.a #Q (s1.m) - a #Q (s2.m).|/(|.a #Q (s1.m).|*|.a #Q (s2.m).|
) by A21,A25,SEQ_2:2
.= |.a #Q (s1.m) - a #Q (s2.m).|/(|.a #Q (s1.m) * a #Q (s2.m).|)
by COMPLEX1:65
.= |.a #Q (s1.m) - a #Q (s2.m).|/|.a #Q (s1.m+s2.m).| by A4,Th53
.= |.a #Q (s1.m) - a #Q (s2.m).|/(a #Q (s1.m+s2.m)) by A26,
ABSVALUE:def 1;
then
A27: (|.a #Q (s1.m) - a #Q (s2.m).|/a #Q (s1.m+s2.m))*a #Q (s1.m+s2.m)
< c*a #Q m1 * a #Q (s1.m+s2.m) by A20,A26,XREAL_1:68;
a #Q (s1.m+s2.m) <> 0 by A4,Th52;
then
A28: |.a #Q (s1.m) - a #Q (s2.m).|<c * a #Q m1 * a #Q (s1.m+s2.m) by A27,
XCMPLX_1:87;
a #Q m1 * a #Q (s1.m+s2.m) = a #Q (m1+(s1.m+s2.m)) by A4,Th53;
then c*(a #Q m1 * a #Q (s1.m+s2.m)) < 1*c by A4,A11,A18,A24,Th65,
XREAL_1:68;
then |.a #Q (s1.m) - a #Q (s2.m).|<c by A28,XXREAL_0:2;
then |.(a #Q s1).m - a #Q (s2.m).| < c by Def5;
then |.(a #Q s1).m - (a #Q s2).m.| < c by Def5;
hence |.((a #Q s1) - (a #Q s2)).m - 0.| < c by RFUNCT_2:1;
end;
then ((a #Q s1) - (a #Q s2)) is convergent by SEQ_2:def 6;
then lim((a #Q s1) - (a #Q s2)) = 0 by A17,SEQ_2:def 7;
then 0 = lim (a #Q s1)-lim (a #Q s2) by A5,A9,SEQ_2:12;
hence thesis;
end;
end;
definition
let a,b be Real;
assume
A1: a > 0;
func a #R b -> Real means
:Def6:
ex s being Rational_Sequence st s is convergent & lim s = b &
a #Q s is convergent & lim a #Q s = it;
existence
proof
consider s being Rational_Sequence such that
A2: s is convergent and
A3: lim s = b and
for n holds s.n<=b by Th67;
take IT=lim a #Q s;
thus thesis by A1,A2,A3,Th69;
end;
uniqueness by A1,Th70;
end;
theorem Th71:
a > 0 implies a #R 0 = 1
proof
set s = seq_const 0;
reconsider s as Rational_Sequence;
assume
A1: a > 0;
s.0 = 0;
then
A2: lim s = 0 by SEQ_4:26;
reconsider j = 1 as Element of REAL by NUMBERS:19;
A3: now
let n be Nat;
reconsider nn=n as Element of NAT by ORDINAL1:def 12;
thus a #Q s .n = a #Q (s.nn) by Def5
.= j by Th47;
end;
then
A4: a #Q s is constant by VALUED_0:def 18;
a #Q s .0 = 1 by A3;
then lim (a #Q s) = 1 by A4,SEQ_4:26;
hence thesis by A1,A2,A4,Def6;
end;
theorem
a > 0 implies a #R 1 = a
proof
set s = seq_const 1;
reconsider s as Rational_Sequence;
s.0 = 1 by SEQ_1:57;
then
A1: lim s = 1 by SEQ_4:26;
assume
A2: a > 0;
A3: now
let n be Nat;
reconsider nn=n as Element of NAT by ORDINAL1:def 12;
thus a #Q s .n = a #Q (s.nn) by Def5
.= a by A2,Th48,SEQ_1:57;
end;
a in REAL by XREAL_0:def 1;
then
A4: a #Q s is constant by A3,VALUED_0:def 18;
a #Q s .0 = a by A3;
then lim (a #Q s) = a by A4,SEQ_4:26;
hence thesis by A2,A1,A4,Def6;
end;
theorem Th73:
1 #R a = 1
proof
consider s being Rational_Sequence such that
A1: s is convergent and
A2: a = lim s and
for n holds s.n<=a by Th67;
reconsider j = 1 as Element of REAL by NUMBERS:19;
A3: now
let n be Nat;
reconsider nn=n as Element of NAT by ORDINAL1:def 12;
thus j #Q s .n = j #Q (s.nn) by Def5
.= j by Th51;
end;
then j #Q s is constant by VALUED_0:def 18;
then
A4: lim (1 #Q s) = 1 #Q s .0 by SEQ_4:26
.= 1 by A3;
1 #Q s is convergent by A1,Th69;
hence thesis by A1,A2,A4,Def6;
end;
theorem Th74:
a>0 implies a #R p = a #Q p
proof
assume
A1: a>0;
set s = seq_const p;
A2: lim s = s.0 by SEQ_4:26
.= p by FUNCOP_1:7;
reconsider s as Rational_Sequence;
A3: now
let n be Nat;
reconsider nn=n as Element of NAT by ORDINAL1:def 12;
thus (a #Q s).n = a #Q (s.nn) by Def5
.= a #Q p by FUNCOP_1:7;
end;
a #Q p in REAL by XREAL_0:def 1;
then
A4: a #Q s is constant by A3,VALUED_0:def 18;
then lim (a #Q s) = (a #Q s).0 by SEQ_4:26
.= a #Q p by A3;
hence thesis by A1,A2,A4,Def6;
end;
theorem Th75:
a > 0 implies a #R (b+c) = a #R b * a #R c
proof
consider sb being Rational_Sequence such that
A1: sb is convergent and
A2: b = lim sb and
for n holds sb.n<=b by Th67;
consider sc being Rational_Sequence such that
A3: sc is convergent and
A4: c = lim sc and
for n holds sc.n<=c by Th67;
assume
A5: a>0;
then
A6: a #Q sb is convergent by A1,Th69;
A7: a #Q sc is convergent by A5,A3,Th69;
reconsider s = sb + sc as Rational_Sequence;
A8: lim s = b + c by A1,A2,A3,A4,SEQ_2:6;
A9: now
let n;
thus a #Q s .n = a #Q (s.n) by Def5
.= a #Q (sb.n + sc.n) by SEQ_1:7
.= a #Q (sb.n) * a #Q (sc.n) by A5,Th53
.= a #Q (sb.n) * (a #Q sc .n) by Def5
.= (a #Q sb .n) * (a #Q sc .n) by Def5;
end;
A10: s is convergent by A1,A3;
then a #Q s is convergent by A5,Th69;
hence a #R (b+c) = lim (a #Q s) by A5,A10,A8,Def6
.= lim ((a #Q sb) (#) (a #Q sc)) by A9,SEQ_1:8
.= (lim (a #Q sb)) * (lim (a #Q sc)) by A6,A7,SEQ_2:15
.= a #R b * (lim (a #Q sc)) by A5,A1,A2,A6,Def6
.= a #R b * a #R c by A5,A3,A4,A7,Def6;
end;
Lm8: a > 0 implies a #R b >= 0
proof
consider s being Rational_Sequence such that
A1: s is convergent and
A2: b = lim s and
for n holds s.n<=b by Th67;
assume
A3: a > 0;
A4: now
let n;
a #Q s .n = a #Q (s.n) by Def5;
hence a #Q s .n >= 0 by A3,Th52;
end;
a #Q s is convergent by A3,A1,Th69;
then a #R b = lim (a #Q s) by A3,A1,A2,Def6;
hence thesis by A3,A1,A4,Th69,SEQ_2:17;
end;
Lm9: a > 0 implies a #R b <> 0
proof
assume
A1: a > 0;
assume a #R b = 0;
then 0 = a #R b * a #R (-b) .= a #R (b + -b) by A1,Th75
.= 1 by A1,Th71;
hence contradiction;
end;
theorem Th76:
a > 0 implies a #R (-c) = 1 / a #R c
proof
assume
A1: a>0;
then 1 = a #R (c+-c) by Th71
.= a #R (-c) * a #R c by A1,Th75;
then 1 / a #R c = a #R (-c) * (a #R c / a #R c) by XCMPLX_1:74
.= a #R (-c) * 1 by A1,Lm9,XCMPLX_1:60;
hence thesis;
end;
theorem Th77:
a > 0 implies a #R (b-c) = a #R b / a #R c
proof
assume
A1: a > 0;
thus a #R (b-c) = a #R (b + -c) .= a #R b * a #R (-c) by A1,Th75
.= a #R b * (1 / a #R c) by A1,Th76
.= a #R b * (1 * (a #R c)")
.= a #R b / a #R c;
end;
theorem Th78:
a > 0 & b > 0 implies (a * b) #R c = a #R c * b #R c
proof
assume that
A1: a>0 and
A2: b>0;
A3: a*b > 0 by A1,A2;
consider s1 being Rational_Sequence such that
A4: s1 is convergent and
A5: c = lim s1 and
for n holds s1.n>=c by Th68;
A6: a #Q s1 is convergent by A1,A4,Th69;
A7: b #Q s1 is convergent by A2,A4,Th69;
now
let n;
thus (a*b) #Q s1 .n = (a*b) #Q (s1.n) by Def5
.= a #Q (s1.n) * b #Q (s1.n) by A1,A2,Th56
.= (a #Q s1 .n) * b #Q (s1.n) by Def5
.= (a #Q s1 .n) * (b #Q s1 .n) by Def5;
end;
then
A8: (a*b) #Q s1 = a #Q s1 (#) b #Q s1 by SEQ_1:8;
then (a*b) #Q s1 is convergent by A6,A7;
hence (a*b) #R c = lim ((a *b) #Q s1) by A3,A4,A5,Def6
.= lim (a #Q s1) * lim (b #Q s1) by A6,A7,A8,SEQ_2:15
.= a #R c * lim (b #Q s1) by A1,A4,A5,A6,Def6
.= a #R c * b #R c by A2,A4,A5,A7,Def6;
end;
theorem Th79:
a>0 implies (1/a) #R c = 1 / a #R c
proof
assume
A1: a>0;
1 = 1 #R c by Th73
.= ((1/a)*a) #R c by A1,XCMPLX_1:106
.= (1/a) #R c * a #R c by A1,Th78;
then 1 / a #R c = (1/a) #R c * (a #R c / a #R c) by XCMPLX_1:74
.= (1/a) #R c * 1 by A1,Lm9,XCMPLX_1:60;
hence thesis;
end;
theorem
a > 0 & b > 0 implies (a/b) #R c = a #R c / b #R c
proof
assume that
A1: a>0 and
A2: b>0;
thus (a/b) #R c = (a*b") #R c .= a #R c * (b") #R c by A1,A2,Th78
.= a #R c * (1/b) #R c
.= a #R c * (1 / b #R c) by A2,Th79
.= a #R c * 1 / b #R c
.= a #R c / b #R c;
end;
theorem Th81:
a > 0 implies a #R b > 0
proof
assume
A1: a > 0;
then a #R b <> 0 by Lm9;
hence thesis by A1,Lm8;
end;
theorem Th82:
a>=1 & c>=b implies a #R c >= a #R b
proof
assume that
A1: a>=1 and
A2: c>=b;
consider s1 being Rational_Sequence such that
A3: s1 is convergent and
A4: c = lim s1 and
A5: for n holds s1.n>=c by Th68;
A6: a #Q s1 is convergent by A1,A3,Th69;
consider s2 being Rational_Sequence such that
A7: s2 is convergent and
A8: b = lim s2 and
A9: for n holds s2.n<=b by Th67;
A10: a #Q s2 is convergent by A1,A7,Th69;
now
let n;
s1.n>=c by A5;
then
A11: s1.n>=b by A2,XXREAL_0:2;
s2.n<=b by A9;
then s1.n >= s2.n by A11,XXREAL_0:2;
then a #Q (s1.n) >= a #Q (s2.n) by A1,Th63;
then a #Q (s1.n) >= a #Q s2 .n by Def5;
hence a #Q s1 .n >= a #Q s2 .n by Def5;
end;
then lim (a #Q s1) >= lim (a #Q s2) by A6,A10,SEQ_2:18;
then a #R c >= lim (a #Q s2) by A1,A3,A4,A6,Def6;
hence thesis by A1,A7,A8,A10,Def6;
end;
theorem Th83:
a>1 & c>b implies a #R c > a #R b
proof
assume that
A1: a>1 and
A2: c>b;
consider p such that
A3: b<p and
A4: p<c by A2,RAT_1:7;
consider q such that
A5: b<q and
A6: q<p by A3,RAT_1:7;
consider s2 being Rational_Sequence such that
A7: s2 is convergent and
A8: b = lim s2 and
A9: for n holds s2.n<=b by Th67;
A10: a #Q q < a #Q p by A1,A6,Th64;
now
let n;
s2.n<=b by A9;
then s2.n<=q by A5,XXREAL_0:2;
then a #Q (s2.n) <= a #Q q by A1,Th63;
hence a #Q s2 .n <= a #Q q by Def5;
end;
then
A11: lim (a #Q s2) <= a #Q q by A1,A7,Th2,Th69;
a #Q s2 is convergent by A1,A7,Th69;
then a #R b <= a #Q q by A1,A7,A8,A11,Def6;
then
A12: a #R b < a #Q p by A10,XXREAL_0:2;
consider s1 being Rational_Sequence such that
A13: s1 is convergent and
A14: c = lim s1 and
A15: for n holds s1.n>=c by Th68;
now
let n;
s1.n>=c by A15;
then s1.n>=p by A4,XXREAL_0:2;
then a #Q (s1.n) >= a #Q p by A1,Th63;
hence a #Q s1 .n >= a #Q p by Def5;
end;
then
A16: lim (a #Q s1) >= a #Q p by A1,A13,Th1,Th69;
a #Q s1 is convergent by A1,A13,Th69;
then a #R c >= a #Q p by A1,A13,A14,A16,Def6;
hence thesis by A12,XXREAL_0:2;
end;
theorem Th84:
a>0 & a<=1 & c>=b implies a #R c <= a #R b
proof
assume that
A1: a>0 and
A2: a<=1 and
A3: c>=b;
1/a>=1 by A1,A2,Lm4,XREAL_1:85;
then (1/a) #R c >= (1/a) #R b by A3,Th82;
then 1/a #R c >= (1/a) #R b by A1,Th79;
then
A4: 1/a #R c >= 1/a #R b by A1,Th79;
a #R b > 0 by A1,Th81;
hence thesis by A4,XREAL_1:89;
end;
theorem Th85:
a >= 1 & b >= 0 implies a #R b >= 1
proof
assume that
A1: a >= 1 and
A2: b >= 0;
consider s being Rational_Sequence such that
A3: s is convergent and
A4: b = lim s and
A5: for n holds s.n>=b by Th68;
A6: now
let n;
A7: a #Q s .n = a #Q (s.n) by Def5;
s.n>=b by A5;
hence a #Q s .n >= 1 by A1,A2,A7,Th60;
end;
a #Q s is convergent by A1,A3,Th69;
then a #R b = lim (a #Q s) by A1,A3,A4,Def6;
hence thesis by A1,A3,A6,Th1,Th69;
end;
theorem Th86:
a > 1 & b > 0 implies a #R b > 1
proof
assume that
A1: a>1 and
A2: b>0;
a #R b > a #R 0 by A1,A2,Th83;
hence thesis by A1,Th71;
end;
theorem Th87:
a >= 1 & b <= 0 implies a #R b <= 1
proof
assume that
A1: a>=1 and
A2: b<=0;
a #R (-b) >= 1 by A1,A2,Th85;
then 1 / a #R b >= 1 by A1,Th76;
then 1 / (1 / a #R b) <= 1 by XREAL_1:211;
hence thesis;
end;
theorem
a > 1 & b < 0 implies a #R b < 1
proof
assume that
A1: a>1 and
A2: b<0;
-b>0 by A2;
then a #R (-b) > 1 by A1,Th86;
then 1 / a #R b > 1 by A1,Th76;
then 1 / (1 / a #R b) < 1 by XREAL_1:212;
hence thesis;
end;
Lm10: s1 is convergent & s2 is convergent & lim s1 > 0 & p>=0 & (for n holds
s1.n>0 & s2.n = (s1.n) #Q p) implies lim s2 = (lim s1) #Q p
proof
assume that
A1: s1 is convergent and
A2: s2 is convergent and
A3: lim s1 > 0 and
A4: p>=0 and
A5: for n holds s1.n>0 & s2.n = (s1.n) #Q p;
reconsider ls = lim s1 as Element of REAL by XREAL_0:def 1;
set s = seq_const lim s1;
consider m0 being Nat such that
A6: p<m0 by SEQ_4:3;
A7: lim s = s.0 by SEQ_4:26
.= lim s1 by FUNCOP_1:7;
then
A8: s1/"s is convergent by A1,A3,SEQ_2:23;
deffunc O(Nat) = ((s/"s1).$1) |^ m0;
consider s3 being Real_Sequence such that
A9: for n holds s3.n = O(n) from SEQ_1:sch 1;
for n holds s1.n<>0 by A5;
then
A10: s1 is non-zero by SEQ_1:5;
then
A11: s/"s1 is convergent by A1,A3,SEQ_2:23;
then
A12: s3 is convergent by A9,Th18;
reconsider q=m0 as Rational;
deffunc O(Nat) = ((s1/"s).$1) |^ m0;
consider s4 being Real_Sequence such that
A13: for n holds s4.n = O(n) from SEQ_1:sch 1;
lim (s/"s1) = lim s/lim s1 by A1,A3,A10,SEQ_2:24
.= 1 by A3,A7,XCMPLX_1:60;
then lim s3 = 1 |^ m0 by A11,A9,Th18;
then
A14: lim s3 = 1;
lim (s1/"s) = lim s1/lim s by A1,A3,A7,SEQ_2:24
.= 1 by A3,A7,XCMPLX_1:60;
then lim s4 = 1 |^ m0 by A8,A13,Th18;
then
A15: lim s4 = 1;
s2 is bounded by A2;
then consider d be Real such that
A16: d>0 and
A17: for n holds |.s2.n.|<d by SEQ_2:3;
A18: s4 is convergent by A8,A13,Th18;
now
let c be Real;
assume
A19: c>0;
then c/d>0 by A16;
then consider m1 such that
A20: for m st m>=m1 holds |.s3.m-1.|<c/d by A12,A14,SEQ_2:def 7;
A21: (lim s1) #Q p > 0 by A3,Th52;
then
A22: |.(lim s1) #Q p.| > 0 by ABSVALUE:def 1;
then c/|.(lim s1) #Q p.|>0 by A19;
then consider m2 such that
A23: for m st m>=m2 holds |.s4.m-1.|<c/|.(lim s1) #Q p.| by A18,A15,
SEQ_2:def 7;
take n = m1 + m2;
let m such that
A24: m>=n;
m2<=n by NAT_1:11;
then
A25: m>=m2 by A24,XXREAL_0:2;
m1<=n by NAT_1:11;
then
A26: m>=m1 by A24,XXREAL_0:2;
now
per cases;
suppose
A27: s1.m >= lim s1;
m in NAT by ORDINAL1:def 12;
then
A28: s1.m/lim s1 = s1.m/s.m by FUNCOP_1:7
.= s1.m*(s.m)"
.= s1.m*s".m by VALUED_1:10
.= (s1/"s).m by SEQ_1:8;
s1.m*(lim s1)">=(lim s1)*(lim s1)" by A3,A27,XREAL_1:64;
then
A29: (s1/"s).m >= 1 by A3,A28,XCMPLX_0:def 7;
then ((s1/"s).m) #Q p <= ((s1/"s).m) #Q q by A6,Th63;
then ((s1/"s).m) #Q p <= ((s1/"s).m) |^ m0 by A29,Th49;
then
A30: ((s1/"s).m) #Q p - 1 <= ((s1/"s).m) |^ m0 - 1 by XREAL_1:9;
((s1/"s).m) #Q p >= 1 by A4,A29,Th60;
then ((s1/"s).m) #Q p - 1 >= 1-1 by XREAL_1:9;
then
A31: ((s1/"s).m) #Q p - 1 = |.((s1/"s).m) #Q p - 1.| by ABSVALUE:def 1;
A32: (lim s1) #Q p <> 0 by A3,Th52;
A33: |.s4.m-1.|<c/|.(lim s1) #Q p.| by A23,A25;
A34: s1.m>0 by A5;
((s1/"s).m) |^ m0 >= 1 by A29,Th11;
then ((s1/"s).m) |^ m0 - 1 >= 1-1 by XREAL_1:9;
then |.((s1/"s).m) #Q p - 1.| <= |.((s1/"s).m) |^ m0 - 1.| by A30,A31
,ABSVALUE:def 1;
then |.((s1/"s).m) #Q p - 1.| <= |.s4.m - 1.| by A13;
then
A35: |.((s1/"s).m) #Q p - 1.|<c/|.(lim s1) #Q p.| by A33,XXREAL_0:2;
A36: |.(lim s1) #Q p.| <> 0 by A21,ABSVALUE:def 1;
|.s2.m - (lim s1) #Q p.| = |.((s1.m) #Q p - (lim s1) #Q p)*1.| by A5
.= |.((s1.m) #Q p - (lim s1) #Q p)*((lim s1) #Q p/(lim s1) #Q p)
.| by A32,XCMPLX_1:60
.= |.(lim s1) #Q p * ((s1.m) #Q p - (lim s1) #Q p) / (lim s1) #Q
p.|
.= |.(lim s1) #Q p * (((s1.m) #Q p - (lim s1) #Q p) / (lim s1)
#Q p).|
.= |.(lim s1) #Q p.|*|.((s1.m) #Q p - (lim s1) #Q p) / (lim s1)
#Q p.| by COMPLEX1:65
.= |.(lim s1) #Q p.|*|.(s1.m) #Q p/(lim s1) #Q p - (lim s1) #Q
p / (lim s1) #Q p.|
.= |.(lim s1) #Q p.|*|.(s1.m) #Q p/(lim s1) #Q p - 1.| by A32,
XCMPLX_1:60
.= |.(lim s1) #Q p.|*|.(s1.m/lim s1) #Q p - 1.| by A3,A34,Th58;
then |.s2.m - (lim s1) #Q p.|< |.(lim s1) #Q p.|*(c/|.(lim s1) #Q
p.|) by A22,A28,A35,XREAL_1:68;
hence |.s2.m - (lim s1) #Q p.|<c by A36,XCMPLX_1:87;
end;
suppose
A37: s1.m <= lim s1;
A38: m in NAT by ORDINAL1:def 12;
A39: lim s1/s1.m = s.m/s1.m by FUNCOP_1:7,A38
.= s.m*(s1.m)"
.= s.m*s1".m by VALUED_1:10
.= (s/"s1).m by SEQ_1:8;
A40: s1.m <> 0 by A5;
A41: s1.m>0 by A5;
then s1.m*(s1.m)"<=(lim s1)*(s1.m)" by A37,XREAL_1:64;
then
A42: (s/"s1).m >= 1 by A40,A39,XCMPLX_0:def 7;
then ((s/"s1).m) #Q p <= ((s/"s1).m) #Q q by A6,Th63;
then ((s/"s1).m) #Q p <= ((s/"s1).m) |^ m0 by A42,Th49;
then
A43: ((s/"s1).m) #Q p - 1 <= ((s/"s1).m) |^ m0 - 1 by XREAL_1:9;
(s1.m) #Q p > 0 by A5,Th52;
then
A44: |.(s1.m) #Q p.| > 0 by ABSVALUE:def 1;
A45: |.s3.m-1.|<c/d by A20,A26;
((s/"s1).m) #Q p >= 1 by A4,A42,Th60;
then ((s/"s1).m) #Q p - 1 >= 1-1 by XREAL_1:9;
then
A46: ((s/"s1).m) #Q p - 1 = |.((s/"s1).m) #Q p - 1.| by ABSVALUE:def 1;
((s/"s1).m) |^ m0 >= 1 by A42,Th11;
then ((s/"s1).m) |^ m0 - 1 >= 1-1 by XREAL_1:9;
then |.((s/"s1).m) #Q p - 1.| <= |.((s/"s1).m) |^ m0 - 1.| by A43,A46
,ABSVALUE:def 1;
then |.((s/"s1).m) #Q p - 1.| <= |.s3.m - 1.| by A9;
then
A47: |.((s/"s1).m) #Q p - 1.|<c/d by A45,XXREAL_0:2;
|.s2.m.|<d by A17;
then |.(s1.m) #Q p.|<d by A5;
then |.(s1.m) #Q p.|/d<d/d by A16,XREAL_1:74;
then |.(s1.m) #Q p.|/d<1 by A16,XCMPLX_1:60;
then
A48: c*(|.(s1.m) #Q p.|/d)<c*1 by A19,XREAL_1:68;
A49: (s1.m) #Q p <> 0 by A5,Th52;
|.s2.m - (lim s1) #Q p.| = |.((s1.m) #Q p - (lim s1) #Q p)*1.| by A5
.= |.((s1.m) #Q p - (lim s1) #Q p)*((s1.m) #Q p/(s1.m) #Q p).| by
A49,XCMPLX_1:60
.= |.(s1.m) #Q p * ((s1.m) #Q p - (lim s1) #Q p) / (s1.m) #Q p.|
.= |.(s1.m) #Q p * (((s1.m) #Q p - (lim s1) #Q p) / (s1.m) #Q p)
.|
.= |.(s1.m) #Q p.|*|.((s1.m) #Q p - (lim s1) #Q p) / (s1.m) #Q
p.| by COMPLEX1:65
.= |.(s1.m) #Q p.|*|.(s1.m) #Q p/(s1.m) #Q p - (lim s1) #Q p /
(s1.m) #Q p.|
.= |.(s1.m) #Q p.|*|.1 - (lim s1) #Q p/(s1.m) #Q p.| by A49,
XCMPLX_1:60
.= |.(s1.m) #Q p.|*|.-(1 - (lim s1) #Q p/(s1.m) #Q p).| by
COMPLEX1:52
.= |.(s1.m) #Q p.|*|.(lim s1) #Q p/(s1.m) #Q p - 1.|
.= |.(s1.m) #Q p.|*|.(lim s1/s1.m) #Q p - 1.| by A3,A41,Th58;
then |.s2.m - (lim s1) #Q p.|<|.(s1.m) #Q p.|*(c/d) by A44,A39,A47,
XREAL_1:68;
hence |.s2.m - (lim s1 ) #Q p.| < c by A48,XXREAL_0:2;
end;
end;
hence |.s2.m - (lim s1) #Q p.| < c;
end;
hence thesis by A2,SEQ_2:def 7;
end;
theorem Th89:
s1 is convergent & s2 is convergent & lim s1 > 0 & (for n holds
s1.n>0 & s2.n = (s1.n) #Q p) implies lim s2 = (lim s1) #Q p
proof
assume that
A1: s1 is convergent and
A2: s2 is convergent and
A3: lim s1 > 0 and
A4: for n holds s1.n>0 & s2.n = (s1.n) #Q p;
per cases;
suppose
p>=0;
hence thesis by A1,A2,A3,A4,Lm10;
end;
suppose
A5: p<=0;
s1 is bounded by A1;
then consider d be Real such that
A6: d>0 and
A7: for n holds |.s1.n.|<d by SEQ_2:3;
reconsider d as Real;
A8: d #Q p > 0 by A6,Th52;
A9: now
assume lim s2 = 0;
then consider n such that
A10: for m st m>=n holds |.s2.m - 0.|<d #Q p by A2,A8,SEQ_2:def 7;
now
let m;
A11: s1.m>0 by A4;
A12: s1.m<>0 by A4;
A13: (s1.m) #Q p > 0 by A4,Th52;
|.s1.m.|<d by A7;
then s1.m<d by A11,ABSVALUE:def 1;
then s1.m/s1.m<d/s1.m by A11,XREAL_1:74;
then 1<=d/s1.m by A12,XCMPLX_1:60;
then (d/s1.m) #Q p <= 1 by A5,Th61;
then d #Q p/(s1.m) #Q p <= 1 by A6,A11,Th58;
then
A14: d #Q p/(s1.m) #Q p * (s1.m) #Q p<= 1*(s1.m) #Q p by A13,XREAL_1:64;
A15: (s1.m) #Q p <> 0 by A4,Th52;
assume m>=n;
then |.s2.m - 0.|<d #Q p by A10;
then |.(s1.m) #Q p.|<d #Q p by A4;
then (s1.m) #Q p<d #Q p by A13,ABSVALUE:def 1;
hence contradiction by A15,A14,XCMPLX_1:87;
end;
hence contradiction;
end;
now
let n;
(s1.n) #Q p <> 0 by A4,Th52;
hence s2.n <> 0 by A4;
end;
then
A16: s2 is non-zero by SEQ_1:5;
then
A17: lim s2" = (lim s2)" by A2,A9,SEQ_2:22;
deffunc O(Nat) = (s2.$1)";
consider s being Real_Sequence such that
A18: for n holds s.n = O(n) from SEQ_1:sch 1;
A19: now
let n;
s.n = (s2.n)" by A18
.= ((s1.n) #Q p)" by A4
.= 1 / (s1.n) #Q p
.= (s1.n) #Q (-p) by A4,Th54;
hence s1.n>0 & s.n = (s1.n) #Q (-p) by A4;
end;
A20: dom s2 = NAT by FUNCT_2:def 1;
A21: dom s = NAT by FUNCT_2:def 1;
for n being object st n in dom s holds s.n = (s2.n)" by A18;
then
A22: s = s2" by A21,A20,VALUED_1:def 7;
s2" is convergent by A2,A16,A9,SEQ_2:21;
then (lim s2)" = (lim s1) #Q (-p) by A1,A3,A5,A17,A22,A19,Lm10;
then 1/lim s2 = 1/(lim s1) #Q p by A3,Th54;
hence thesis by XCMPLX_1:59;
end;
end;
Lm11: a > 0 implies a #R b #Q p = a #R (b * p)
proof
consider s1 being Rational_Sequence such that
A1: s1 is convergent and
A2: b = lim s1 and
for n holds s1.n>=b by Th68;
reconsider s2 = p(#)s1 as Rational_Sequence;
assume
A3: a>0;
A4: now
let n;
A5: a #Q (s1.n) > 0 by A3,Th52;
(a #Q s1 .n) #Q p = (a #Q (s1.n)) #Q p by Def5
.= a #Q (p*s1.n) by A3,Th59
.= a #Q (s2.n) by SEQ_1:9
.= a #Q s2 .n by Def5;
hence a #Q s1 .n > 0 & (a #Q s1 .n) #Q p = a #Q s2 .n by A5,Def5;
end;
A6: s2 is convergent by A1;
then
A7: a #Q s2 is convergent by A3,Th69;
lim s2 = b*p by A1,A2,SEQ_2:8;
then
A8: a #R (b*p) = lim (a #Q s2) by A3,A6,A7,Def6;
A9: a #Q s1 is convergent by A3,A1,Th69;
then a #R b = lim (a #Q s1) by A3,A1,A2,Def6;
hence thesis by A3,A9,A7,A8,A4,Th81,Th89;
end;
Lm12: a>=1 & s1 is convergent & s2 is convergent & (for n holds s2.n = a #R (
s1.n)) implies lim s2 = a #R (lim s1)
proof
assume that
A1: a>=1 and
A2: s1 is convergent and
A3: s2 is convergent and
A4: for n holds s2.n = a #R (s1.n);
set d = |.lim s1.|+1;
A5: |.lim s1.|<|.lim s1.| + 1 by XREAL_1:29;
now
lim s1<=|.lim s1.| by ABSVALUE:4;
then lim s1<=d by A5,XXREAL_0:2;
then
A6: a #R (lim s1) <= a #R d by A1,Th82;
a #R (lim s1) > 0 by A1,Th81;
then
A7: |.a #R (lim s1).| <= a #R d by A6,ABSVALUE:def 1;
A8: a #R d >= 0 by A1,Th81;
let c be Real;
assume
A9: c>0;
consider m1 such that
A10: a #R d*(a-1)/c < m1 by SEQ_4:3;
m1+1>=m1 by XREAL_1:29;
then a #R d * (a-1)/c < m1+1 by A10,XXREAL_0:2;
then a #R d * (a-1)/c*c < c*(m1+1) by A9,XREAL_1:68;
then a #R d * (a-1) < c*(m1+1) by A9,XCMPLX_1:87;
then a #R d * (a-1)/(m1+1) < (m1+1)*c/(m1+1) by XREAL_1:74;
then a #R d * (a-1)/(m1+1) < c/(m1+1)*(m1+1);
then
A11: a #R d * (a-1)/(m1+1) < c by XCMPLX_1:87;
reconsider m3 = (m1+1)" as Rational;
A12: |.a #R (lim s1).| >= 0 by COMPLEX1:46;
consider n such that
A13: for m st n<=m holds |.s1.m -(lim s1).|<(m1+1) " by A2,SEQ_2:def 7;
take n;
let m;
assume m>=n;
then
A14: |.s1.m -(lim s1).|<=(m1+1)" by A13;
A15: m1+1>=0+1 by NAT_1:13;
then (m1+1) -Root a - 1 <= (a-1)/(m1+1) by A1,Th31;
then
A16: (a #R d)*((m1+1) -Root a - 1) <= (a #R d)*((a-1)/(m1+1)) by A8,XREAL_1:64;
s1.m -(lim s1)<=|.s1.m -(lim s1).| by ABSVALUE:4;
then s1.m -(lim s1) <= (m1+1)" by A14,XXREAL_0:2;
then a #R (s1.m-lim s1) <= a #R m3 by A1,Th82;
then a #R (s1.m-lim s1) <= a #Q m3 by A1,Th74;
then a #R (s1.m-lim s1) <= (m1+1) -Root a by A15,Th50;
then
A17: a #R (s1.m-lim s1) - 1 <= (m1+1) -Root a - 1 by XREAL_1:9;
A18: a #R (s1.m-lim s1) <> 0 by A1,Th81;
A19: a #R (s1.m-lim s1) > 0 by A1,Th81;
A20: now
per cases;
suppose
s1.m-lim s1>=0;
then a #R (s1.m-lim s1) >= 1 by A1,Th85;
then a #R (s1.m-lim s1) - 1 >= 0 by XREAL_1:48;
hence |.a #R (s1.m-lim s1) - 1.| <= (m1+1) -Root a - 1 by A17,
ABSVALUE:def 1;
end;
suppose
A21: s1.m-lim s1<0;
A22: -(s1.m -lim s1)<=|.-(s1.m -lim s1).| by ABSVALUE:4;
|.s1.m -lim s1.| = |.-(s1.m -lim s1).| by COMPLEX1:52;
then -(s1.m -lim s1) <= m3 by A14,A22,XXREAL_0:2;
then a #R (-(s1.m-lim s1)) <= a #R m3 by A1,Th82;
then a #R (-(s1.m-lim s1)) <= a #Q m3 by A1,Th74;
then a #R (-(s1.m-lim s1)) <= (m1+1) -Root a by A15,Th50;
then
A23: a #R (-(s1.m-lim s1)) - 1 <= (m1+1) -Root a - 1 by XREAL_1:9;
a #R (-(s1.m-lim s1)) >= 1 by A1,A21,Th85;
then a #R (-(s1.m-lim s1)) - 1 >= 0 by XREAL_1:48;
then
A24: |.a #R (-(s1.m-lim s1)) - 1.| <= (m1+1) -Root a - 1 by A23,
ABSVALUE:def 1;
a #R (s1.m-lim s1) <= 1 by A1,A21,Th87;
then
A25: |.a #R (s1.m-lim s1).| <= 1 by A19,ABSVALUE:def 1;
|.a #R (-(s1.m-lim s1)) - 1.| >= 0 by COMPLEX1:46;
then
A26: |.a #R (s1.m-lim s1).|*|.a #R (-(s1.m-lim s1)) - 1.| <= 1*|.a
#R (-(s1.m-lim s1)) - 1.| by A25,XREAL_1:64;
|.a #R (s1.m-lim s1) - 1.| = |.(a #R (s1.m-lim s1) - 1)*1.|
.= |.(a #R (s1.m-lim s1) - 1)*(a #R (s1.m-lim s1)/a #R (s1.m-lim
s1)).| by A18,XCMPLX_1:60
.= |.a #R (s1.m-lim s1)*(a #R (s1.m-lim s1) - 1)/a #R (s1.m-lim
s1).|
.= |.a #R (s1.m-lim s1)*((a #R (s1.m-lim s1) - 1)/a #R (s1.m-lim
s1)).|
.= |.a #R (s1.m-lim s1).|*|.(a #R (s1.m-lim s1) - 1)/a #R (s1.m
-lim s1).| by COMPLEX1:65
.= |.a #R (s1.m-lim s1).|* |.a #R (s1.m-lim s1)/a #R (s1.m-lim
s1) - 1/a #R (s1.m-lim s1).|
.= |.a #R (s1.m-lim s1).|*|.1 - 1/a #R (s1.m-lim s1).| by A18,
XCMPLX_1:60
.= |.a #R (s1.m-lim s1).|*|.1 - a #R (-(s1.m-lim s1)).| by A1,Th76
.= |.a #R (s1.m-lim s1).|*|.-(1 - a #R (-(s1.m-lim s1))).| by
COMPLEX1:52
.= |.a #R (s1.m-lim s1).|*|.a #R (-(s1.m-lim s1)) - 1.|;
hence |.a #R (s1.m-lim s1) - 1.| <= (m1+1) -Root a - 1 by A24,A26,
XXREAL_0:2;
end;
end;
|.a #R (s1.m-lim s1) - 1.| >= 0 by COMPLEX1:46;
then
A27: |.a #R (lim s1).|*|.a #R (s1.m-lim s1) - 1.| <= (a #R d)*((m1+1)
-Root a - 1) by A20,A12,A7,XREAL_1:66;
|.a #R (s1.m) - a #R (lim s1).| = |.(a #R (s1.m) - a #R (lim s1))* 1.|
.=|.(a #R (s1.m) - a #R (lim s1))*(a #R (lim s1)/a #R (lim s1)).| by A1
,Lm9,XCMPLX_1:60
.=|.a #R (lim s1)*(a #R (s1.m) - a #R (lim s1))/a #R (lim s1).|
.=|.a #R (lim s1)*((a #R (s1.m) - a #R (lim s1))/a #R (lim s1)).|
.=|.a #R (lim s1).|*|.(a #R (s1.m) - a #R (lim s1))/a #R (lim s1).|
by COMPLEX1:65
.=|.a #R(lim s1).|*|.a #R (s1.m)/a #R (lim s1)-a #R (lim s1)/a #R (
lim s1).|
.=|.a #R (lim s1).|*|.a #R (s1.m)/a #R (lim s1) - 1.| by A1,Lm9,
XCMPLX_1:60
.=|.a #R (lim s1).|*|.a #R (s1.m-lim s1) - 1.| by A1,Th77;
then |.a #R (s1.m) - a #R (lim s1).|<= (a #R d)*(a-1)/(m1+1) by A27,A16,
XXREAL_0:2;
then |.a #R (s1.m) - a #R (lim s1).| < c by A11,XXREAL_0:2;
hence |.s2.m - a #R (lim s1).| < c by A4;
end;
hence thesis by A3,SEQ_2:def 7;
end;
theorem Th90:
a>0 & s1 is convergent & s2 is convergent & (for n holds s2.n =
a #R (s1.n)) implies lim s2 = a #R (lim s1)
proof
assume that
A1: a>0 and
A2: s1 is convergent and
A3: s2 is convergent and
A4: for n holds s2.n = a #R (s1.n);
per cases;
suppose
a>=1;
hence thesis by A2,A3,A4,Lm12;
end;
suppose
A5: a<1;
A6: now
assume
A7: lim s2 = 0;
a #R ((lim s1) + 1) > 0 by A1,Th81;
then consider n such that
A8: for m st m>=n holds |.s2.m-0.|<a #R ((lim s1) +1) by A3,A7,SEQ_2:def 7;
consider n1 being Nat such that
A9: for m st m>=n1 holds |.s1.m-lim s1.|<1 by A2,SEQ_2:def 7;
now
let m such that
A10: m>=n+n1;
n+n1>=n1 by NAT_1:12;
then m>=n1 by A10,XXREAL_0:2;
then
A11: |.s1.m-lim s1.|<1 by A9;
s1.m-lim s1<=|.s1.m-lim s1.| by ABSVALUE:4;
then s1.m-lim s1< 1 by A11,XXREAL_0:2;
then
A12: s1.m-lim s1 + lim s1 < lim s1 + 1 by XREAL_1:6;
n+n1>=n by NAT_1:12;
then m>=n by A10,XXREAL_0:2;
then |.s2.m-0.|<a #R ((lim s1)+1) by A8;
then
A13: |.a #R (s1.m).|<a #R ((lim s1)+1) by A4;
a #R (s1.m) > 0 by A1,Th81;
then a #R (s1.m) < a #R ((lim s1)+1) by A13,ABSVALUE:def 1;
hence contradiction by A1,A5,A12,Th84;
end;
hence contradiction;
end;
A14: now
let n;
thus s2".n = (s2.n)" by VALUED_1:10
.= (a #R (s1.n))" by A4
.= 1/(a #R (s1.n))
.= (1/a) #R (s1.n) by A1,Th79;
end;
a*(1/a)<=1*(1/a) by A1,A5,XREAL_1:64;
then
A15: 1<=1/a by A1,XCMPLX_1:106;
A16: a #R (lim s1) <> 0 by A1,Th81;
now
let n;
s2.n = a #R (s1.n) by A4;
hence s2.n <> 0 by A1,Th81;
end;
then
A17: s2 is non-zero by SEQ_1:5;
then
A18: lim s2" = (lim s2)" by A3,A6,SEQ_2:22;
s2" is convergent by A3,A6,A17,SEQ_2:21;
then (lim s2)" = (1/a) #R (lim s1) by A2,A15,A18,A14,Lm12
.= 1/a #R (lim s1) by A1,Th79;
then 1 = 1/a #R (lim s1) * lim s2 by A6,XCMPLX_0:def 7;
then a #R (lim s1)= a #R (lim s1)*(1/a #R (lim s1) * lim s2)
.= a #R (lim s1)*(1/a #R (lim s1)) * lim s2
.= 1 * lim s2 by A16,XCMPLX_1:106;
hence thesis;
end;
end;
theorem
a > 0 implies a #R b #R c = a #R (b * c)
proof
consider s being Rational_Sequence such that
A1: s is convergent and
A2: c = lim s and
for n holds s.n<=c by Th67;
A3: lim (b(#)s) = b*c by A1,A2,SEQ_2:8;
A4: b(#)s is convergent by A1;
assume
A5: a>0;
then
A6: (a #R b) #Q s is convergent by A1,Th69,Th81;
A7: now
let n;
thus (a #R b) #Q s .n = (a #R b) #Q (s.n) by Def5
.= a #R (b*s.n) by A5,Lm11
.= a #R ((b(#)s).n) by SEQ_1:9;
end;
a #R b > 0 by A5,Th81;
then (a #R b) #R c = lim ((a #R b) #Q s) by A1,A2,A6,Def6;
hence thesis by A5,A6,A4,A3,A7,Th90;
end;
begin :: Addenda
:: from PCOMPS_2, 2006.02.10, A.T.
reserve r, u for Real,
k for Nat;
theorem
r>0 & u > 0 implies ex k be Nat st u/(2 |^ k) <= r
proof
defpred P[Nat] means $1 <= 2 |^ $1;
assume that
A1: r>0 and
A2: u>0;
set t = 1/r;
reconsider t as Real;
consider n such that
A3: (u * t) < n by SEQ_4:3;
A4: 0 < u * t by A1,A2;
then
A5: u/(u * t) > u/n by A2,A3,XREAL_1:76;
A6: for k be Nat st P[k] holds P[k + 1]
proof
let k be Nat;
assume k <= 2 |^ k;
then
A7: (2 |^ k) + 1 >= k + 1 by XREAL_1:7;
2 |^ k >= 1 by Th11;
then
A8: 2 |^ k + 2 |^ k >= 2 |^ k + 1 by XREAL_1:7;
2 |^ (k + 1) = (2 |^ k) * (2 |^ 1) by NEWTON:8
.= (2 |^ k) * 2
.= 2 |^ k + 2 |^ k;
hence thesis by A8,A7,XXREAL_0:2;
end;
take n;
A9: r = 1/t .= (u * 1) / (u * t) by A2,XCMPLX_1:91
.= u/(u * t);
A10: P[0];
for k be Nat holds P[k] from NAT_1:sch 2(A10,A6);
then u/n >= u/(2 |^ n) by A2,A3,A4,XREAL_1:118;
hence thesis by A9,A5,XXREAL_0:2;
end;
theorem
k>=n & r >= 1 implies r |^ k >= r |^ n
proof
assume that
A1: k>=n and
A2: r >= 1;
consider m be Nat such that
A3: k = n + m by A1,NAT_1:10;
A4: r |^ k = r |^ n * r |^ m by A3,NEWTON:8;
r |^ n >= 1 by A2,Th11;
hence thesis by A2,A4,Th11,XREAL_1:151;
end;
:: from SCPINVAR, 2006.03.14, A.T.
theorem Th94:
for n,m,l be Nat st n divides m & n divides l holds n divides m-l
proof
let n,m,l be Nat;
assume that
A1: n divides m and
A2: n divides l;
A3: -l =-n*(l div n) by A2,NAT_D:3
.=n*(-(l div n));
m = n * (m div n) by A1,NAT_D:3;
then m - l =n * ((m div n) + -(l div n)) by A3;
hence thesis by INT_1:def 3;
end;
::$CT
theorem Th96:
m gcd n = m gcd |.n-m.|
proof
set x=m gcd n, y=m gcd |. n - m .|;
A1: x divides m by NAT_D:def 5;
A2: x divides n by NAT_D:def 5;
A3: y divides m by NAT_D:def 5;
per cases;
suppose
n-m >= 0;
then reconsider nm=n-m as Element of NAT by INT_1:3;
A4: |. n - m .|=nm by ABSVALUE:def 1;
then y divides nm by NAT_D:def 5;
then y divides nm+m by A3,NAT_D:8;
then
A5: y divides x by A3,NAT_D:def 5;
x divides n-m by A1,A2,Th94;
then x divides y by A1,A4,NAT_D:def 5;
hence thesis by A5,NAT_D:5;
end;
suppose
A6: n-m < 0;
reconsider nn=n as Integer;
A7: |. n - m .|=-(n-m) by A6,ABSVALUE:def 1
.=m-n;
then reconsider mn=m-n as Element of NAT;
y divides mn by A7,NAT_D:def 5;
then y divides mn-m by A3,Th94;
then y divides nn by INT_2:10;
then
A8: y divides x by A3,NAT_D:def 5;
x divides m-n by A1,A2,Th94;
then x divides y by A1,A7,NAT_D:def 5;
hence thesis by A8,NAT_D:5;
end;
end;
theorem
for a,b be Integer st a>=0 & b>=0 holds a gcd b = a gcd (b-a)
proof
let a,b be Integer;
assume that
A1: a>=0 and
A2: b>=0;
thus a gcd b=|.a.| gcd |.b.| by INT_2:34
.=|.a.| gcd |.|.b.|-|.a.|.| by Th96
.=|.a.| gcd |.b-|.a.|.| by A2,ABSVALUE:def 1
.=|.a.| gcd |.b-a.| by A1,ABSVALUE:def 1
.=a gcd (b-a) by INT_2:34;
end;
:: missing, 2008.03.05, A.T.
theorem
a>=0 implies a #Z l >= 0 by Lm5;
theorem
a > 0 implies a #Q l = a #Z l
proof
assume a > 0;
then a #Z l > 0 by Th39;
then
A1: a #Z l = 1-Root (a #Z l) |^ 1 by Def2;
denominator l=1 by RAT_1:17;
hence a #Q l = 1-Root (a #Z l)
.= a #Z l by A1;
end;
:: missing, 2010.02.13, A.T.
theorem
l <> 0 implies 0 #Z l = 0 proof assume
A1: l <> 0;
per cases by A1;
suppose
A2: l > 0;
then reconsider l as Element of NAT by INT_1:3;
l >= 0+1 by A2,NAT_1:13;
then
A3: 0 |^ l = 0 by NEWTON:11;
|.l.| = l by ABSVALUE:def 1;
hence thesis by A3,Def3;
end;
suppose
A4: l < 0;
then reconsider k = -l as Element of NAT by INT_1:3;
k > -0 by A4;
then k >= 0+1 by NAT_1:13;
then
A5: 0 |^ k = 0 by NEWTON:11;
|.l.| = k by A4,ABSVALUE:def 1;
then (0 |^ |.l.|)" = 0 by A5;
hence thesis by A4,Def3;
end;
end;