:: Several Integrability Formulas of Special Functions
:: by Cuiying Peng , Fuguo Ge and Xiquan Liang
::
:: Received August 28, 2007
:: Copyright (c) 2007 Association of Mizar Users
Lm1:
sin (PI / 4) > 0
Lm2:
sin (- (PI / 4)) < 0
theorem Th1: :: INTEGRA8:1
theorem Th2: :: INTEGRA8:2
theorem Th3: :: INTEGRA8:3
theorem Th4: :: INTEGRA8:4
theorem Th5: :: INTEGRA8:5
theorem Th6: :: INTEGRA8:6
theorem Th7: :: INTEGRA8:7
theorem Th8: :: INTEGRA8:8
theorem Th9: :: INTEGRA8:9
theorem Th10: :: INTEGRA8:10
theorem Th11: :: INTEGRA8:11
theorem Th12: :: INTEGRA8:12
Lm3:
cos (PI / 4) > 0
theorem Th13: :: INTEGRA8:13
theorem Th14: :: INTEGRA8:14
theorem Th15: :: INTEGRA8:15
theorem Th16: :: INTEGRA8:16
theorem Th17: :: INTEGRA8:17
theorem Th18: :: INTEGRA8:18
theorem Th19: :: INTEGRA8:19
Lm4:
for f1, f2 being PartFunc of REAL ,REAL holds (- f1) (#) (- f2) = f1 (#) f2
theorem Th20: :: INTEGRA8:20
theorem Th21: :: INTEGRA8:21
theorem Th22: :: INTEGRA8:22
theorem Th23: :: INTEGRA8:23
theorem :: INTEGRA8:24
theorem Th25: :: INTEGRA8:25
theorem Th26: :: INTEGRA8:26
theorem Th27: :: INTEGRA8:27
theorem Th28: :: INTEGRA8:28
theorem Th29: :: INTEGRA8:29
theorem Th30: :: INTEGRA8:30
theorem Th31: :: INTEGRA8:31
theorem Th32: :: INTEGRA8:32
theorem Th33: :: INTEGRA8:33
theorem Th34: :: INTEGRA8:34
theorem :: INTEGRA8:35
:: deftheorem defines Cst INTEGRA8:def 1 :
theorem Th36: :: INTEGRA8:36
theorem Th37: :: INTEGRA8:37
theorem :: INTEGRA8:38
Lm5:
dom sin = REAL
by FUNCT_2:def 1;
Lm6:
dom cos = REAL
by FUNCT_2:def 1;
Lm7:
dom (- sin ) = REAL
by FUNCT_2:def 1;
Lm8:
dom exp_R = REAL
by FUNCT_2:def 1;
Lm9:
dom sinh = REAL
by FUNCT_2:def 1;
Lm10:
dom cosh = REAL
by FUNCT_2:def 1;
Lm11:
for A being closed-interval Subset of REAL holds
( cos is_integrable_on A & cos | A is bounded )
theorem Th39: :: INTEGRA8:39
theorem :: INTEGRA8:40
theorem :: INTEGRA8:41
theorem :: INTEGRA8:42
theorem :: INTEGRA8:43
theorem :: INTEGRA8:44
theorem :: INTEGRA8:45
Lm12:
for A being closed-interval Subset of REAL holds
( - sin is_integrable_on A & (- sin ) | A is bounded )
theorem Th46: :: INTEGRA8:46
theorem :: INTEGRA8:47
theorem :: INTEGRA8:48
theorem :: INTEGRA8:49
theorem :: INTEGRA8:50
theorem :: INTEGRA8:51
theorem :: INTEGRA8:52
Lm13:
for A being closed-interval Subset of REAL holds
( exp_R is_integrable_on A & exp_R | A is bounded )
theorem Th53: :: INTEGRA8:53
theorem :: INTEGRA8:54
Lm14:
for A being closed-interval Subset of REAL holds sinh | A is continuous
Lm15:
for A being closed-interval Subset of REAL holds
( sinh is_integrable_on A & sinh | A is bounded )
theorem Th55: :: INTEGRA8:55
theorem :: INTEGRA8:56
Lm16:
for A being closed-interval Subset of REAL holds cosh | A is continuous
Lm17:
for A being closed-interval Subset of REAL holds
( cosh is_integrable_on A & cosh | A is bounded )
theorem Th57: :: INTEGRA8:57
theorem :: INTEGRA8:58
theorem :: INTEGRA8:59
theorem :: INTEGRA8:60
theorem :: INTEGRA8:61
Lm18:
dom (arcsin `| ].(- 1),1.[) = ].(- 1),1.[
by FDIFF_1:def 8, SIN_COS6:84;
theorem Th62: :: INTEGRA8:62
theorem Th63: :: INTEGRA8:63
theorem :: INTEGRA8:64
theorem :: INTEGRA8:65
theorem Th66: :: INTEGRA8:66
theorem Th67: :: INTEGRA8:67
theorem Th68: :: INTEGRA8:68
Lm19:
for A being closed-interval Subset of REAL holds
( sin is_integrable_on A & sin | A is bounded )
theorem Th69: :: INTEGRA8:69
theorem :: INTEGRA8:70
theorem :: INTEGRA8:71
theorem :: INTEGRA8:72
theorem :: INTEGRA8:73
theorem :: INTEGRA8:74
theorem :: INTEGRA8:75
theorem Th76: :: INTEGRA8:76
theorem :: INTEGRA8:77
theorem Th78: :: INTEGRA8:78
theorem :: INTEGRA8:79
theorem :: INTEGRA8:80
theorem :: INTEGRA8:81
theorem :: INTEGRA8:82
theorem :: INTEGRA8:83
theorem :: INTEGRA8:84
theorem :: INTEGRA8:85
theorem :: INTEGRA8:86
theorem :: INTEGRA8:87
theorem :: INTEGRA8:88
theorem :: INTEGRA8:89
theorem Th90: :: INTEGRA8:90
theorem :: INTEGRA8:91
theorem :: INTEGRA8:92
theorem :: INTEGRA8:93
theorem :: INTEGRA8:94
theorem :: INTEGRA8:95
theorem :: INTEGRA8:96
Lm20:
for A being closed-interval Subset of REAL holds
( cos (#) cos is_integrable_on A & (cos (#) cos ) | A is bounded )
theorem :: INTEGRA8:97
theorem :: INTEGRA8:98
theorem :: INTEGRA8:99
theorem :: INTEGRA8:100
Lm21:
for A being closed-interval Subset of REAL holds
( exp_R (#) (sin + cos ) is_integrable_on A & (exp_R (#) (sin + cos )) | A is bounded )
Lm22:
for A being closed-interval Subset of REAL holds
( exp_R (#) (cos - sin ) is_integrable_on A & (exp_R (#) (cos - sin )) | A is bounded )
theorem :: INTEGRA8:101
theorem :: INTEGRA8:102