:: Several Differentiable Formulas of Special Functions -- Part {II}
:: by Yan Zhang , Bo Li and Xiquan Liang
::
:: Received November 23, 2005
:: Copyright (c) 2005 Association of Mizar Users
Lm1:
for x being Real holds 1 - (cos (2 * x)) = 2 * ((sin x) ^2 )
Lm2:
for x being Real holds 1 + (cos (2 * x)) = 2 * ((cos x) ^2 )
Lm3:
for x being Real st sin . x > 0 holds
sin . x = ((1 - (cos . x)) * (1 + (cos . x))) #R (1 / 2)
Lm4:
for x being Real st sin . x > 0 & cos . x < 1 & cos . x > - 1 holds
(sin . x) / ((1 - (cos . x)) #R (1 / 2)) = (1 + (cos . x)) #R (1 / 2)
theorem Th1: :: FDIFF_6:1
theorem Th2: :: FDIFF_6:2
Lm5:
for x being Real st sin . x > 0 & cos . x < 1 & cos . x > - 1 holds
(sin . x) / ((1 + (cos . x)) #R (1 / 2)) = (1 - (cos . x)) #R (1 / 2)
theorem Th3: :: FDIFF_6:3
theorem Th4: :: FDIFF_6:4
theorem Th5: :: FDIFF_6:5
theorem :: FDIFF_6:6
theorem Th7: :: FDIFF_6:7
theorem :: FDIFF_6:8
theorem :: FDIFF_6:9
theorem :: FDIFF_6:10
theorem Th11: :: FDIFF_6:11
theorem :: FDIFF_6:12
theorem :: FDIFF_6:13
theorem Th14: :: FDIFF_6:14
theorem :: FDIFF_6:15
theorem Th16: :: FDIFF_6:16
theorem :: FDIFF_6:17
theorem :: FDIFF_6:18
theorem :: FDIFF_6:19
theorem :: FDIFF_6:20
theorem :: FDIFF_6:21
theorem :: FDIFF_6:22
theorem Th23: :: FDIFF_6:23
theorem :: FDIFF_6:24
theorem Th25: :: FDIFF_6:25
theorem :: FDIFF_6:26
theorem Th27: :: FDIFF_6:27
theorem :: FDIFF_6:28
theorem Th29: :: FDIFF_6:29
theorem :: FDIFF_6:30
theorem Th31: :: FDIFF_6:31
theorem :: FDIFF_6:32
theorem :: FDIFF_6:33
theorem :: FDIFF_6:34
theorem :: FDIFF_6:35
theorem :: FDIFF_6:36
theorem :: FDIFF_6:37
theorem :: FDIFF_6:38
theorem :: FDIFF_6:39
theorem :: FDIFF_6:40
Lm6:
for Z being open Subset of REAL
for f1 being PartFunc of REAL ,REAL st Z c= dom (f1 + (2 (#) sin )) & ( for x being Real st x in Z holds
f1 . x = 1 ) holds
( f1 + (2 (#) sin ) is_differentiable_on Z & ( for x being Real st x in Z holds
((f1 + (2 (#) sin )) `| Z) . x = 2 * (cos . x) ) )
theorem :: FDIFF_6:41
Lm7:
for Z being open Subset of REAL
for f1 being PartFunc of REAL ,REAL st Z c= dom (f1 + (2 (#) cos )) & ( for x being Real st x in Z holds
f1 . x = 1 ) holds
( f1 + (2 (#) cos ) is_differentiable_on Z & ( for x being Real st x in Z holds
((f1 + (2 (#) cos )) `| Z) . x = - (2 * (sin . x)) ) )
theorem :: FDIFF_6:42
theorem Th43: :: FDIFF_6:43
theorem :: FDIFF_6:44
theorem :: FDIFF_6:45
theorem Th46: :: FDIFF_6:46
theorem :: FDIFF_6:47
theorem :: FDIFF_6:48
theorem :: FDIFF_6:49
theorem :: FDIFF_6:50