:: Several Differentiation Formulas of Special Functions -- Part {IV}
:: by Bo Li and Peng Wang
::
:: Received September 29, 2006
:: Copyright (c) 2006 Association of Mizar Users
theorem Th1: :: FDIFF_8:1
theorem Th2: :: FDIFF_8:2
theorem Th3: :: FDIFF_8:3
theorem :: FDIFF_8:4
Lm1:
right_open_halfline 0 = { g where g is Real : 0 < g }
by XXREAL_1:230;
theorem :: FDIFF_8:5
theorem Th6: :: FDIFF_8:6
theorem Th7: :: FDIFF_8:7
theorem :: FDIFF_8:8
theorem :: FDIFF_8:9
theorem :: FDIFF_8:10
theorem :: FDIFF_8:11
theorem :: FDIFF_8:12
theorem :: FDIFF_8:13
theorem :: FDIFF_8:14
theorem :: FDIFF_8:15
theorem :: FDIFF_8:16
theorem :: FDIFF_8:17
theorem :: FDIFF_8:18
theorem :: FDIFF_8:19
theorem :: FDIFF_8:20
theorem :: FDIFF_8:21
theorem :: FDIFF_8:22
theorem :: FDIFF_8:23
theorem :: FDIFF_8:24
theorem :: FDIFF_8:25
theorem :: FDIFF_8:26
theorem :: FDIFF_8:27
theorem :: FDIFF_8:28
theorem :: FDIFF_8:29
theorem :: FDIFF_8:30
theorem :: FDIFF_8:31
theorem :: FDIFF_8:32
theorem :: FDIFF_8:33
theorem :: FDIFF_8:34
theorem :: FDIFF_8:35