begin
:: deftheorem SIN_COS:def 1 :
canceled;
:: deftheorem Def2 defines CHK SIN_COS:def 2 :
:: deftheorem SIN_COS:def 3 :
canceled;
:: deftheorem Def4 defines Prod_complex_n SIN_COS:def 4 :
:: deftheorem Def5 defines Prod_real_n SIN_COS:def 5 :
:: deftheorem defines !c SIN_COS:def 6 :
:: deftheorem defines ! SIN_COS:def 7 :
:: deftheorem Def8 defines ExpSeq SIN_COS:def 8 :
:: deftheorem Def9 defines rExpSeq SIN_COS:def 9 :
theorem Th1:
theorem
canceled;
theorem Th3:
:: deftheorem Def10 defines Coef SIN_COS:def 10 :
:: deftheorem Def11 defines Coef_e SIN_COS:def 11 :
:: deftheorem Def12 defines Shift SIN_COS:def 12 :
:: deftheorem Def13 defines Expan SIN_COS:def 13 :
:: deftheorem Def14 defines Expan_e SIN_COS:def 14 :
:: deftheorem Def15 defines Alfa SIN_COS:def 15 :
:: deftheorem defines Conj SIN_COS:def 16 :
:: deftheorem Def17 defines Conj SIN_COS:def 17 :
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> ) )
theorem Th4:
theorem Th5:
theorem Th6:
theorem Th7:
theorem Th8:
theorem Th9:
theorem Th10:
theorem Th11:
theorem Th12:
theorem Th13:
theorem Th14:
theorem Th15:
theorem Th16:
theorem Th17:
theorem Th18:
theorem Th19:
theorem Th20:
theorem Th21:
theorem Th22:
theorem Th23:
Lm2:
for z, w being complex number holds (Sum (z ExpSeq )) * (Sum (w ExpSeq )) = Sum ((z + w) ExpSeq )
begin
:: deftheorem Def18 defines exp SIN_COS:def 18 :
:: deftheorem defines exp SIN_COS:def 19 :
theorem
begin
:: deftheorem Def20 defines sin SIN_COS:def 20 :
:: deftheorem defines sin SIN_COS:def 21 :
:: deftheorem Def22 defines cos SIN_COS:def 22 :
:: deftheorem defines cos SIN_COS:def 23 :
theorem
canceled;
theorem
canceled;
theorem Th27:
Lm3:
for th being Real holds Sum ((th * <i> ) ExpSeq ) = (cos . th) + ((sin . th) * <i> )
theorem
Lm4:
for th being Real holds (Sum ((th * <i> ) ExpSeq )) *' = Sum ((- (th * <i> )) ExpSeq )
theorem
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 )
theorem
theorem Th31:
theorem
theorem Th33:
theorem
:: deftheorem Def24 defines P_sin SIN_COS:def 24 :
:: deftheorem Def25 defines P_cos SIN_COS:def 25 :
theorem Th35:
theorem Th36:
theorem Th37:
theorem Th38:
theorem Th39:
theorem Th40:
theorem
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();
Lm7:
bq is increasing sequence of NAT
reconsider bq = bq as increasing sequence of NAT by Lm7;
Lm8:
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 )
theorem Th42:
theorem Th43:
theorem
canceled;
theorem
theorem Th46:
theorem Th47:
theorem Th48:
theorem Th49:
Lm9:
for n being Element of NAT
for z being complex number holds
( (z ExpSeq ) . 1 = z & (z ExpSeq ) . 0 = 1r & |.(z |^ n).| = |.z.| |^ n )
Lm10:
for th being Real holds Sum (th ExpSeq ) = Sum (th rExpSeq )
theorem Th50:
:: deftheorem Def26 defines exp_R SIN_COS:def 26 :
:: deftheorem defines exp_R SIN_COS:def 27 :
theorem Th51:
theorem
canceled;
theorem Th53:
theorem
Lm11:
for p, q being real number holds exp_R . (p + q) = (exp_R . p) * (exp_R . q)
theorem
Lm12:
exp_R . 0 = 1
theorem
theorem Th57:
theorem Th58:
theorem Th59:
theorem
begin
:: deftheorem Def28 defines P_dt SIN_COS:def 28 :
:: deftheorem defines P_t SIN_COS:def 29 :
Lm13:
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) )
Lm14:
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 )
theorem Th61:
theorem Th62:
theorem Th63:
theorem Th64:
theorem Th65:
theorem Th66:
theorem Th67:
theorem Th68:
theorem Th69:
theorem Th70:
theorem Th71:
theorem Th72:
theorem Th73:
theorem Th74:
:: deftheorem defines tan SIN_COS:def 30 :
:: deftheorem defines cot SIN_COS:def 31 :
theorem Th75:
Lm15:
( dom (tan | [.0 ,1.]) = [.0 ,1.] & ( for th being real number st th in [.0 ,1.] holds
(tan | [.0 ,1.]) . th = tan . th ) )
Lm16:
( tan is_differentiable_on ].0 ,1.[ & ( for th being real number st th in ].0 ,1.[ holds
diff tan ,th > 0 ) )
theorem Th76:
theorem Th77:
Lm17:
( tan . 0 = 0 & tan . 1 > 1 )
begin
:: deftheorem Def32 defines PI SIN_COS:def 32 :
theorem Th78:
begin
theorem Th79:
theorem
theorem Th81:
theorem
theorem Th83:
theorem
Lm18:
for th being real number st th in [.0 ,1.] holds
sin . th >= 0
theorem Th85:
theorem
begin
theorem
canceled;
theorem
theorem
:: deftheorem defines !c SIN_COS:def 33 :