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 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 by SEQ_1:57;
then
A2: lim s = 0 by SEQ_4:26;
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,SEQ_1:57;
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;
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=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: p0 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.|0;
then c/d>0 by A16;
then consider m1 such that
A20: for m st m>=m1 holds |.s3.m-1.| 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.|=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.|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.| 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.| 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.|= 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.| 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.| 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.|0 by A4;
A12: s1.m<>0 by A4;
A13: (s1.m) #Q p > 0 by A4,Th52;
|.s1.m.| 0 by A4,Th52;
assume m>=n;
then |.s2.m - 0.| 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.|=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.| 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;
theorem
m divides n iff m divides (n qua Integer);
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) by RAT_1:17
.= 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;