begin
Lm1:
for p1, p2, g1, g2 being Element of REAL holds
( (p1 + (g1 * <i>)) * (p2 + (g2 * <i>)) = ((p1 * p2) - (g1 * g2)) + (((p1 * g2) + (p2 * g1)) * <i>) & (p2 + (g2 * <i>)) *' = p2 + ((- g2) * <i>) )
Lm2:
for z, w being complex number holds (Sum (z ExpSeq)) * (Sum (w ExpSeq)) = Sum ((z + w) ExpSeq)
begin
begin
Lm3:
for th being Real holds Sum ((th * <i>) ExpSeq) = (cos . th) + ((sin . th) * <i>)
Lm4:
for th being Real holds (Sum ((th * <i>) ExpSeq)) *' = Sum ((- (th * <i>)) ExpSeq)
Lm5:
for th being Real
for th1 being real number st th = th1 holds
( |.(Sum ((th * <i>) ExpSeq)).| = 1 & abs (sin . th1) <= 1 & abs (cos . th1) <= 1 )
deffunc H1( Real) -> Element of REAL = (2 * $1) + 1;
consider bq being Real_Sequence such that
Lm6:
for n being Element of NAT holds bq . n = H1(n)
from SEQ_1:sch 1();
bq is increasing sequence of NAT
then reconsider bq = bq as increasing sequence of NAT ;
Lm7:
for n being Element of NAT
for th, th1, th2, th3 being real number holds
( th |^ (2 * n) = (th |^ n) |^ 2 & (- 1) |^ (2 * n) = 1 & (- 1) |^ ((2 * n) + 1) = - 1 )
Lm8:
for n being Element of NAT
for z being complex number holds
( (z ExpSeq) . 1 = z & (z ExpSeq) . 0 = 1r & |.(z |^ n).| = |.z.| |^ n )
Lm9:
for th being Real holds Sum (th ExpSeq) = Sum (th rExpSeq)
Lm10:
for p, q being real number holds exp_R . (p + q) = (exp_R . p) * (exp_R . q)
Lm11:
exp_R . 0 = 1
begin
Lm12:
for p being Real
for z being complex number holds
( Re ((p * <i>) * z) = - (p * (Im z)) & Im ((p * <i>) * z) = p * (Re z) & Re (p * z) = p * (Re z) & Im (p * z) = p * (Im z) )
Lm13:
for p being real number
for z being complex number st p > 0 holds
( Re (z / (p * <i>)) = (Im z) / p & Im (z / (p * <i>)) = - ((Re z) / p) & |.(z / p).| = |.z.| / p )
Lm14:
( dom (tan | [.0,1.]) = [.0,1.] & ( for th being real number st th in [.0,1.] holds
(tan | [.0,1.]) . th = tan . th ) )
Lm15:
( tan is_differentiable_on ].0,1.[ & ( for th being real number st th in ].0,1.[ holds
diff (tan,th) > 0 ) )
Lm16:
( tan . 0 = 0 & tan . 1 > 1 )
begin
begin
Lm17:
for th being real number st th in [.0,1.] holds
sin . th >= 0
begin