:: Trigonometric Functions and Existence of Circle Ratio
:: by Yuguang Yang and Yasunari Shidama
::
:: Received October 22, 1998
:: Copyright (c) 1998 Association of Mizar Users
:: 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: :: SIN_COS:1
theorem :: SIN_COS:2
canceled;
theorem Th3: :: SIN_COS:3
:: 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: :: SIN_COS:4
theorem Th5: :: SIN_COS:5
theorem Th6: :: SIN_COS:6
theorem Th7: :: SIN_COS:7
theorem Th8: :: SIN_COS:8
theorem Th9: :: SIN_COS:9
theorem Th10: :: SIN_COS:10
theorem Th11: :: SIN_COS:11
theorem Th12: :: SIN_COS:12
theorem Th13: :: SIN_COS:13
theorem Th14: :: SIN_COS:14
theorem Th15: :: SIN_COS:15
theorem Th16: :: SIN_COS:16
theorem Th17: :: SIN_COS:17
theorem Th18: :: SIN_COS:18
theorem Th19: :: SIN_COS:19
theorem Th20: :: SIN_COS:20
theorem Th21: :: SIN_COS:21
theorem Th22: :: SIN_COS:22
theorem Th23: :: SIN_COS:23
Lm2:
for z, w being complex number holds (Sum (z ExpSeq )) * (Sum (w ExpSeq )) = Sum ((z + w) ExpSeq )
:: deftheorem Def18 defines exp SIN_COS:def 18 :
:: deftheorem defines exp SIN_COS:def 19 :
theorem :: SIN_COS:24
:: 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 :: SIN_COS:25
canceled;
theorem :: SIN_COS:26
canceled;
theorem Th27: :: SIN_COS:27
Lm3:
for th being Real holds Sum ((th * <i> ) ExpSeq ) = (cos . th) + ((sin . th) * <i> )
theorem :: SIN_COS:28
Lm4:
for th being Real holds (Sum ((th * <i> ) ExpSeq )) *' = Sum ((- (th * <i> )) ExpSeq )
theorem :: SIN_COS:29
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 :: SIN_COS:30
theorem Th31: :: SIN_COS:31
theorem :: SIN_COS:32
theorem Th33: :: SIN_COS:33
theorem :: SIN_COS:34
:: deftheorem Def24 defines P_sin SIN_COS:def 24 :
:: deftheorem Def25 defines P_cos SIN_COS:def 25 :
theorem Th35: :: SIN_COS:35
theorem Th36: :: SIN_COS:36
theorem Th37: :: SIN_COS:37
theorem Th38: :: SIN_COS:38
theorem Th39: :: SIN_COS:39
theorem Th40: :: SIN_COS:40
theorem :: SIN_COS:41
deffunc H1( Real) -> Element of REAL = (2 * $1) + 1;
consider bq being Real_Sequence such that
Lm10:
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 ;
Lm11:
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: :: SIN_COS:42
theorem Th43: :: SIN_COS:43
theorem :: SIN_COS:44
canceled;
theorem :: SIN_COS:45
theorem Th46: :: SIN_COS:46
theorem Th47: :: SIN_COS:47
theorem Th48: :: SIN_COS:48
theorem Th49: :: SIN_COS:49
Lm13:
for n being Element of NAT
for z being complex number holds
( (z ExpSeq ) . 1 = z & (z ExpSeq ) . 0 = 1r & |.(z |^ n).| = |.z.| |^ n )
Lm14:
for th being Real holds Sum (th ExpSeq ) = Sum (th rExpSeq )
theorem Th50: :: SIN_COS:50
:: deftheorem Def26 defines exp_R SIN_COS:def 26 :
:: deftheorem defines exp_R SIN_COS:def 27 :
theorem Th51: :: SIN_COS:51
theorem :: SIN_COS:52
canceled;
theorem Th53: :: SIN_COS:53
theorem :: SIN_COS:54
Lm15:
for p, q being real number holds exp_R . (p + q) = (exp_R . p) * (exp_R . q)
theorem :: SIN_COS:55
Lm16:
exp_R . 0 = 1
theorem :: SIN_COS:56
theorem Th57: :: SIN_COS:57
theorem Th58: :: SIN_COS:58
theorem Th59: :: SIN_COS:59
theorem :: SIN_COS:60
:: deftheorem Def28 defines P_dt SIN_COS:def 28 :
:: deftheorem defines P_t SIN_COS:def 29 :
Lm17:
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) )
Lm18:
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: :: SIN_COS:61
theorem Th62: :: SIN_COS:62
theorem Th63: :: SIN_COS:63
theorem Th64: :: SIN_COS:64
theorem Th65: :: SIN_COS:65
theorem Th66: :: SIN_COS:66
theorem Th67: :: SIN_COS:67
theorem Th68: :: SIN_COS:68
theorem Th69: :: SIN_COS:69
theorem Th70: :: SIN_COS:70
theorem Th71: :: SIN_COS:71
theorem Th72: :: SIN_COS:72
theorem Th73: :: SIN_COS:73
theorem Th74: :: SIN_COS:74
:: deftheorem defines tan SIN_COS:def 30 :
:: deftheorem defines cot SIN_COS:def 31 :
theorem Th75: :: SIN_COS:75
Lm19:
( dom (tan | [.0 ,1.]) = [.0 ,1.] & ( for th being real number st th in [.0 ,1.] holds
(tan | [.0 ,1.]) . th = tan . th ) )
Lm20:
( tan is_differentiable_on ].0 ,1.[ & ( for th being real number st th in ].0 ,1.[ holds
diff tan ,th > 0 ) )
theorem Th76: :: SIN_COS:76
theorem Th77: :: SIN_COS:77
Lm21:
( tan . 0 = 0 & tan . 1 > 1 )
:: deftheorem Def32 defines PI SIN_COS:def 32 :
theorem Th78: :: SIN_COS:78
theorem Th79: :: SIN_COS:79
theorem :: SIN_COS:80
theorem Th81: :: SIN_COS:81
theorem :: SIN_COS:82
theorem Th83: :: SIN_COS:83
theorem :: SIN_COS:84
Lm22:
for th being real number st th in [.0 ,1.] holds
sin . th >= 0
theorem Th85: :: SIN_COS:85
theorem :: SIN_COS:86
theorem :: SIN_COS:87
canceled;
theorem :: SIN_COS:88
theorem :: SIN_COS:89
:: deftheorem defines !c SIN_COS:def 33 :