0;
hence thesis by Lm5;
end;
suppose
A1: c < 0;
A2: rseq(0,1,c,d) = (-1)(#)rseq(0,1,-c,-d) by Th7;
rseq(0,1,-c,-d) is convergent by A1,Lm5;
hence thesis by A2;
end;
end;
Lm7:
0 < c implies lim rseq(0,1,c,d) = 0
proof
set f = rseq(0,1,c,d);
assume
A1: 0 < c;
then
A2: f is convergent by Lm5;
for p st 0 < p ex n st for m st n <= m holds |.f.m-0 .| < p by A1,Lm4;
hence thesis by A2,SEQ_2:def 7;
end;
Lm8:
c < 0 implies lim rseq(0,1,c,d) = 0
proof
set f = rseq(0,1,c,d);
assume
A1: c < 0;
set f1 = rseq(0,1,-c,-d);
A2: f = (-1)(#)f1 by Th7;
lim f1 = 0 by A1,Lm7;
hence 0 = (-1)*lim f1
.= lim f by A1,A2,Lm5,SEQ_2:8;
end;
registration
let b,c,d;
cluster rseq(0,b,c,d) -> convergent;
coherence
proof
set f1 = rseq(0,1,c,d);
A1: rseq(0,b,c,d) = b(#)f1
proof
let n be Element of NAT;
f1.n = (0*n+1)/(c*n+d)by Th5;
hence (b(#)f1).n = (0*n+b)/(c*n+d) by VALUED_1:6
.= rseq(0,b,c,d).n by Th5;
end;
f1 is convergent by Lm6;
hence thesis by A1;
end;
end;
theorem
lim(rseq(0,b,0,d)) = b/d
proof
thus lim(rseq(0,b,0,d)) = rseq(0,b,0,d).0 by SEQ_4:26
.= b/d by Th6;
end;
theorem Th10:
for c being non zero Real holds lim(rseq(0,b,c,d)) = 0
proof
let c be non zero Real;
set f1 = rseq(0,1,c,d);
A1: rseq(0,b,c,d) = b(#)f1
proof
let n be Element of NAT;
f1.n = (0*n+1)/(c*n+d) by Th5;
hence (b(#)f1).n = (0*n+b)/(c*n+d) by VALUED_1:6
.= rseq(0,b,c,d).n by Th5;
end;
c < 0 or 0 < c;
then lim f1 = 0 by Lm7,Lm8;
hence 0 = b*lim f1
.= lim(rseq(0,b,c,d)) by A1,SEQ_2:8;
end;
Lm9:
0 < c implies
for p st 0 < p ex n st for m st n <= m holds |.rseq(1,0,c,d).m-(1/c).| < p
proof
set f = rseq(1,0,c,d);
assume
A1: 0 < c;
let p such that
A2: 0 < p;
set f1 = rseq(0,-d,c*c,c*d);
lim f1 = 0 by A1,Th10;
then consider n such that
A3: for m st n <= m holds |.f1.m-0 .| < p by A2,SEQ_2:def 7;
consider m1 being Nat such that
A4: 0 < c*m1+d by A1,Th1;
reconsider mm = max(m1,n+1) as Nat by TARSKI:1;
take mm;
let m such that
A5: mm <= m;
m1 <= mm by XXREAL_0:25;
then m1 <= m by A5,XXREAL_0:2;
then c*m1 <= c*m by A1,XREAL_1:64;
then
A6: c*m1+d <= c*m+d by XREAL_1:6;
A7: n+0 <= n+1 by XREAL_1:6;
n+1 <= mm by XXREAL_0:25;
then
n <= mm by A7,XXREAL_0:2;
then
A8: n <= m by A5,XXREAL_0:2;
f.m-(1/c) = (1*m+0)/(c*m+d)-1/c by Th5
.= (m*c-1*(c*m+d))/((c*m+d)*c) by A1,A6,A4,XCMPLX_1:130
.= (0*m+-d)/(c*c*m+c*d)
.= f1.m-0 by Th5;
hence |.f.m-(1/c).| < p by A3,A8;
end;
Lm10:
0 < c implies rseq(1,0,c,d) is convergent
proof
assume
A1: 0 < c;
take 1/c;
thus thesis by A1,Lm9;
end;
Lm11:
0 < c implies lim rseq(1,0,c,d) = 1/c
proof
assume
A1: 0 < c;
then
A2: rseq(1,0,c,d) is convergent by Lm10;
for p st 0 < p ex n st for m st n <= m holds |.rseq(1,0,c,d).m-1/c.| < p
by A1,Lm9;
hence thesis by A2,SEQ_2:def 7;
end;
Lm12:
for c being non zero Real holds rseq(1,0,c,d) is convergent
proof
let c be non zero Real;
per cases;
suppose 0 < c;
hence thesis by Lm10;
end;
suppose
A1: c < 0;
A2: rseq(1,0,c,d) = (-1)(#)rseq(1,0,-c,-d) by Th8;
rseq(1,0,-c,-d) is convergent by A1,Lm10;
hence thesis by A2;
end;
end;
Lm13:
for c being non zero Real holds lim rseq(1,0,c,d) = 1/c
proof
let c be non zero Real;
per cases;
suppose 0 < c;
hence thesis by Lm11;
end;
suppose
A1: c < 0;
set f = rseq(1,0,c,d);
set f1 = rseq(1,0,-c,-d);
A2: f = (-1)(#)f1 by Th8;
lim f1 = 1/-c by A1,Lm11;
hence lim f = (-1)/-c by A2,A1,Lm10,SEQ_2:8
.= 1/c by XCMPLX_1:191;
end;
end;
registration
let c be non zero Real;
let a,b,d;
cluster rseq(a,b,c,d) -> convergent;
coherence
proof
set f2 = rseq(1,0,c,d);
set f3 = rseq(0,b,c,d);
A1: rseq(a,b,c,d) = a(#)f2+f3
proof
let n be Element of NAT;
A2: f2.n = (1*n+0)/(c*n+d) by Th5;
A3: f3.n = (0*n+b)/(c*n+d) by Th5;
(a(#)f2).n = a*f2.n by VALUED_1:6;
hence (a(#)f2+f3).n = a*f2.n+f3.n by VALUED_1:1
.= (a*n+b)/(c*n+d) by A2,A3
.= rseq(a,b,c,d).n by Th5;
end;
f2 is convergent by Lm12;
hence thesis by A1;
end;
end;
registration
let a,d be positive Real;
let b be Real;
cluster rseq(a,b,0,d) -> non bounded_above;
coherence
proof
let r;
A1: r*d/d = r by XCMPLX_1:89;
A2: (d*r-b)/a*a = d*r-b by XCMPLX_1:87;
consider n such that
A3: n > (d*r-b)/a by SEQ_4:3;
take n;
A4: rseq(a,b,0,d).n = (a*n+b)/(0*n+d) by Th5;
a*n >= a*(d*r-b)/a by A2,A3,XREAL_1:64;
then a*n+b >= d*r-b+b by A2,XREAL_1:6;
hence thesis by A1,A4,XREAL_1:72;
end;
end;
registration
let a,d be negative Real;
let b;
cluster rseq(a,b,0,d) -> non bounded_above;
coherence
proof
let r;
A1: r*d/d = r by XCMPLX_1:89;
A2: (d*r-b)/a*a = d*r-b by XCMPLX_1:87;
consider n such that
A3: n > (d*r-b)/a by SEQ_4:3;
take n;
A4: rseq(a,b,0,d).n = (a*n+b)/(0*n+d) by Th5;
a*n <= a*(d*r-b)/a by A2,A3,XREAL_1:65;
then a*n+b <= d*r-b+b by A2,XREAL_1:6;
hence thesis by A1,A4,XREAL_1:73;
end;
end;
registration
let a be positive Real;
let b;
let d be negative Real;
cluster rseq(a,b,0,d) -> non bounded_below;
coherence
proof
let r;
A1: r*d/d = r by XCMPLX_1:89;
A2: (d*r-b)/a*a = d*r-b by XCMPLX_1:87;
consider n such that
A3: n > (d*r-b)/a by SEQ_4:3;
take n;
A4: rseq(a,b,0,d).n = (a*n+b)/(0*n+d) by Th5;
a*n >= d*r-b by A2,A3,XREAL_1:64;
then a*n+b >= d*r-b+b by XREAL_1:6;
hence thesis by A1,A4,XREAL_1:73;
end;
end;
registration
let a be negative Real;
let b;
let d be positive Real;
cluster rseq(a,b,0,d) -> non bounded_below;
coherence
proof
let r;
A1: r*d/d = r by XCMPLX_1:89;
A2: (d*r-b)/a*a = d*r-b by XCMPLX_1:87;
consider n such that
A3: n > (d*r-b)/a by SEQ_4:3;
take n;
A4: rseq(a,b,0,d).n = (a*n+b)/(0*n+d) by Th5;
a*n <= a*(d*r-b)/a by A2,A3,XREAL_1:65;
then a*n+b <= d*r-b+b by A2,XREAL_1:6;
hence thesis by A1,A4,XREAL_1:72;
end;
end;
registration
let a,d be non zero Real;
let b;
cluster rseq(a,b,0,d) -> non bounded;
coherence
proof
(a is positive or a is negative) & (d is positive or d is negative);
hence thesis;
end;
end;
registration
let a,d be non zero Real;
let b;
cluster rseq(a,b,0,d) -> non convergent;
coherence;
end;
theorem Th11:
for c being non zero Real holds lim(rseq(a,b,c,d)) = a/c
proof
let c be non zero Real;
set f2 = rseq(1,0,c,d);
set f3 = rseq(0,b,c,d);
A1: rseq(a,b,c,d) = a(#)f2+f3
proof
let n be Element of NAT;
A2: f2.n = (1*n+0)/(c*n+d) by Th5;
A3: f3.n = (0*n+b)/(c*n+d) by Th5;
(a(#)f2).n = a*f2.n by VALUED_1:6;
hence (a(#)f2+f3).n = a*f2.n+f3.n by VALUED_1:1
.= (a*n+b)/(c*n+d) by A2,A3
.= rseq(a,b,c,d).n by Th5;
end;
A4: lim f2 = 1/c by Lm13;
A5: lim f3 = 0 by Th10;
thus lim(rseq(a,b,c,d)) = lim(a(#)f2)+lim f3 by A1,SEQ_2:6
.= a/c by A4,A5,SEQ_2:8;
end;
theorem Th12:
for a being non zero Real holds lim(rseq(a,b,a,d)) = 1
proof
let a be non zero Real;
thus lim(rseq(a,b,a,d)) = a/a by Th11
.= 1 by XCMPLX_1:60;
end;
begin :: Trigonometry
theorem Th13:
sin(PI*i) = 0
proof
per cases;
suppose i is even;
then consider j being Integer such that
A1: i = 2*j by INT_1:def 3,ABIAN:def 1;
thus sin(PI*i) = sin(2*PI*j+0) by A1
.= 0 by SIN_COS:31,COMPLEX2:8;
end;
suppose i is odd;
then consider j being Integer such that
A2: i = 2*j+1 by ABIAN:1;
thus sin(PI*i) = sin(2*PI*j+PI) by A2
.= 0 by SIN_COS:77,COMPLEX2:8;
end;
end;
theorem Th14:
cos(PI/2+PI*i) = 0
proof
per cases;
suppose i is even;
then consider j being Integer such that
A1: i = 2*j by INT_1:def 3,ABIAN:def 1;
thus cos (PI/2+PI*i) = cos (PI/2+2*PI*j) by A1
.= cos (PI/2) by COMPLEX2:9
.= 0 by SIN_COS:76;
end;
suppose i is odd;
then consider j being Integer such that
A2: i = 2*j+1 by ABIAN:1;
thus cos (PI/2+PI*i) = cos (PI+PI/2+2*PI*j) by A2
.= cos (PI+PI/2) by COMPLEX2:9
.= 0 by SIN_COS:76;
end;
end;
theorem Th15:
tan r = (cot r)" & cot r = (tan r)"
proof
thus tan r = (sin r*(cos r)")" "
.= ((sin r)"*(cos r)" ")" by XCMPLX_1:204
.= (cot r)";
thus cot r = (cos r*(sin r)")" "
.= ((cos r)"*(sin r)" ")" by XCMPLX_1:204
.= (tan r)";
end;
theorem Th16:
dom tan = union the set of all ]. -PI/2+PI*i,PI/2+PI*i .[ where i is Integer
proof
set S = the set of all ]. -PI/2+PI*i,PI/2+PI*i .[ where i is Integer;
set T = dom tan;
A1: dom sin = REAL & dom cos = REAL by FUNCT_2:def 1;
then T = REAL/\(REAL\cos"{0}) by RFUNCT_1:def 1;
then
A2: T = REAL \cos"{0} by XBOOLE_1:28;
thus T c= union S
proof
let x be object;
assume
A3: x in T;
then reconsider x as Element of REAL;
not x in cos"{0} by A2,A3,XBOOLE_0:def 5;
then not cos x in {0} by A1,FUNCT_1:def 7;
then
A4: cos x <> 0 by TARSKI:def 1;
set xP = (x-PI/2)/PI,E = [\xP/];
A5: ]. -PI/2+PI*(E+1),PI/2+PI*(E+1) .[ in S;
xP*PI = x-PI/2 by XCMPLX_1:87;
then
A6: x = PI/2+xP*PI;
then
A7: E<>xP by Th14,A4;
E <= xP < E+1 by INT_1:def 6,29;
then E