:: Several Integrability Formulas of Special Functions -- Part {II}
:: by Bo Li , Yanping Zhuang , Yanhong Men and Xiquan Liang
::
:: Received October 14, 2008
:: Copyright (c) 2008 Association of Mizar Users
A1:
( [#] REAL = dom (AffineMap (1 / 2),0 ) & [#] REAL = dom (sin * (AffineMap 2,0 )) )
by FUNCT_2:def 1;
A2:
dom ((1 / 4) (#) (sin * (AffineMap 2,0 ))) = [#] REAL
by FUNCT_2:def 1;
theorem Th1: :: INTEGR11:1
theorem Th2: :: INTEGR11:2
theorem Th3: :: INTEGR11:3
theorem Th4: :: INTEGR11:4
theorem Th5: :: INTEGR11:5
theorem Th6: :: INTEGR11:6
theorem Th7: :: INTEGR11:7
theorem Th8: :: INTEGR11:8
theorem Th9: :: INTEGR11:9
theorem Th10: :: INTEGR11:10
theorem Th11: :: INTEGR11:11
theorem Th12: :: INTEGR11:12
theorem Th13: :: INTEGR11:13
C:
( dom (AffineMap 2,0 ) = [#] REAL & dom ((AffineMap (1 / 2),0 ) - ((1 / 4) (#) (sin * (AffineMap 2,0 )))) = REAL )
by FUNCT_2:def 1;
theorem :: INTEGR11:14
theorem :: INTEGR11:15
theorem Th16: :: INTEGR11:16
theorem :: INTEGR11:17
theorem :: INTEGR11:18
theorem Th19: :: INTEGR11:19
theorem :: INTEGR11:20
theorem :: INTEGR11:21
theorem Th22: :: INTEGR11:22
theorem :: INTEGR11:23
theorem :: INTEGR11:24
theorem :: INTEGR11:25
theorem :: INTEGR11:26
theorem :: INTEGR11:27
theorem :: INTEGR11:28
theorem :: INTEGR11:29
theorem :: INTEGR11:30
theorem :: INTEGR11:31
theorem :: INTEGR11:32
theorem Th1: :: INTEGR11:33
theorem :: INTEGR11:34
theorem :: INTEGR11:35
theorem :: INTEGR11:36
theorem Th12: :: INTEGR11:37
theorem :: INTEGR11:38
theorem Th14: :: INTEGR11:39
theorem :: INTEGR11:40
theorem Th16: :: INTEGR11:41
theorem :: INTEGR11:42
theorem Th18: :: INTEGR11:43
theorem :: INTEGR11:44
theorem :: INTEGR11:45
theorem :: INTEGR11:46
theorem :: INTEGR11:47
theorem :: INTEGR11:48
theorem Th24: :: INTEGR11:49
theorem :: INTEGR11:50
theorem Th26: :: INTEGR11:51
theorem :: INTEGR11:52
theorem Th28: :: INTEGR11:53
theorem :: INTEGR11:54
theorem Th30: :: INTEGR11:55
theorem :: INTEGR11:56
theorem Th32: :: INTEGR11:57
theorem :: INTEGR11:58
theorem Th34: :: INTEGR11:59
theorem :: INTEGR11:60
theorem :: INTEGR11:61
theorem :: INTEGR11:62
theorem :: INTEGR11:63
theorem :: INTEGR11:64
theorem :: INTEGR11:65
theorem :: INTEGR11:66
theorem :: INTEGR11:67
theorem :: INTEGR11:68
theorem :: INTEGR11:69
theorem :: INTEGR11:70
theorem :: INTEGR11:71
theorem :: INTEGR11:72
theorem :: INTEGR11:73