:: Several Differentiation Formulas of Special Functions -- Part {III}
:: by Bo Li , Yan Zhang and Xiquan Liang
::
:: Received March 22, 2006
:: Copyright (c) 2006 Association of Mizar Users
theorem Th1: :: FDIFF_7:1
theorem Th2: :: FDIFF_7:2
theorem Th3: :: FDIFF_7:3
Lm1:
for x being Real holds 2 * ((cos . (x / 2)) ^2 ) = 1 + (cos . x)
Lm2:
for x being Real holds 2 * ((sin . (x / 2)) ^2 ) = 1 - (cos . x)
theorem :: FDIFF_7:4
theorem :: FDIFF_7:5
theorem Th6: :: FDIFF_7:6
theorem Th7: :: FDIFF_7:7
theorem :: FDIFF_7:8
theorem :: FDIFF_7:9
theorem Th10: :: FDIFF_7:10
theorem Th11: :: FDIFF_7:11
theorem :: FDIFF_7:12
theorem :: FDIFF_7:13
theorem Th14: :: FDIFF_7:14
theorem Th15: :: FDIFF_7:15
theorem Th16: :: FDIFF_7:16
theorem Th17: :: FDIFF_7:17
theorem :: FDIFF_7:18
theorem :: FDIFF_7:19
theorem :: FDIFF_7:20
theorem :: FDIFF_7:21
theorem Th22: :: FDIFF_7:22
theorem :: FDIFF_7:23
theorem :: FDIFF_7:24
theorem Th25: :: FDIFF_7:25
theorem Th26: :: FDIFF_7:26
theorem Th27: :: FDIFF_7:27
theorem :: FDIFF_7:28
theorem :: FDIFF_7:29
theorem :: FDIFF_7:30
theorem :: FDIFF_7:31
Lm3:
right_open_halfline 0 = { g where g is Real : 0 < g }
by XXREAL_1:230;
theorem :: FDIFF_7:32
theorem :: FDIFF_7:33
theorem :: FDIFF_7:34
theorem :: FDIFF_7:35
theorem :: FDIFF_7:36
theorem :: FDIFF_7:37
theorem Th38: :: FDIFF_7:38
theorem Th39: :: FDIFF_7:39
theorem :: FDIFF_7:40
theorem :: FDIFF_7:41
theorem :: FDIFF_7:42
theorem :: FDIFF_7:43
theorem :: FDIFF_7:44
theorem :: FDIFF_7:45
theorem Th46: :: FDIFF_7:46
theorem Th47: :: FDIFF_7:47
theorem :: FDIFF_7:48
theorem :: FDIFF_7:49
theorem :: FDIFF_7:50
theorem :: FDIFF_7:51