environ
vocabularies HIDDEN, NUMBERS, POWER, SQUARE_1, ARYTM_3, RELAT_1, CARD_1, XXREAL_0, ARYTM_1, COMPLEX1, SIN_COS, FUNCT_3, POLYEQ_1, SIN_COS2, FUNCT_1, NEWTON, SIN_COS7, REAL_1;
notations HIDDEN, ORDINAL1, FUNCT_1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, SQUARE_1, NEWTON, QUIN_1, COMPLEX1, SIN_COS, SIN_COS2, POWER, POLYEQ_1;
definitions ;
theorems SQUARE_1, ABSVALUE, SIN_COS, NEWTON, XCMPLX_1, QUIN_1, SIN_COS2, TAYLOR_1, POWER, POLYEQ_1, XREAL_1, COMPLEX1, ASYMPT_1, XXREAL_0;
schemes ;
registrations XXREAL_0, XREAL_0, SQUARE_1, QUIN_1, SIN_COS, VALUED_0, RELSET_1, SIN_COS2, NEWTON, XCMPLX_0, NAT_1, ORDINAL1;
constructors HIDDEN, REAL_1, SQUARE_1, NAT_1, BINOP_2, QUIN_1, POWER, POLYEQ_1, SIN_COS, SIN_COS2, VALUED_1, NEWTON;
requirements HIDDEN, REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
equalities SQUARE_1, XCMPLX_0;
expansions ;
Lm1:
number_e <> 1
by TAYLOR_1:11;
Lm2:
for x, y being Real st x ^2 < 1 & y < 1 holds
(x ^2) * y < 1
Lm3:
for x being Real st 1 <= x holds
(x ^2) - 1 >= 0
Lm4:
for x being Real st x ^2 < 1 holds
(x + 1) / (1 - x) > 0
theorem Th15:
for
x being
Real st
0 < x &
x < 1 holds
(1 + x) / (1 - x) > 0
Lm5:
for x being Real st 0 < x & x < 1 holds
0 < 1 - (x ^2)
Lm6:
for x being Real holds (x ^2) + 1 > 0
theorem Th32:
for
t being
Real st
- 1
< t &
t < 1 holds
0 < (t + 1) / (1 - t)
Lm7:
for t being Real st ( 1 < t or t < - 1 ) holds
0 < (t + 1) / (t - 1)
Lm8:
for x being Real holds sqrt ((x ^2) + 1) > x
Lm9:
for x, y being Real holds ((sqrt ((x ^2) + 1)) * (sqrt ((y ^2) + 1))) - (x * y) > 0
Lm10:
for y being Real st 1 <= y holds
y + (sqrt ((y ^2) - 1)) > 0
Lm11:
for t being Real st 0 < t holds
- 1 < ((t ^2) - 1) / ((t ^2) + 1)
Lm12:
for t being Real st 0 < t & t <> 1 & not 1 < ((t ^2) + 1) / ((t ^2) - 1) holds
((t ^2) + 1) / ((t ^2) - 1) < - 1
Lm13:
for t being Real st 0 < t holds
0 < (2 * t) / (1 + (t ^2))
;
Lm14:
for t being Real st 0 < t holds
(2 * t) / (1 + (t ^2)) <= 1
Lm15:
for t being Real st 0 < t holds
(1 - (sqrt (1 + (t ^2)))) / t < 0
Lm16:
for t being Real st 0 < t & t <= 1 holds
0 <= 1 - (t ^2)
Lm17:
for t being Real st 0 < t & t <= 1 holds
0 <= 4 - (4 * (t ^2))
Lm18:
for t being Real st 0 < t & t <= 1 holds
0 < 1 + (sqrt (1 - (t ^2)))
Lm19:
for t being Real st 0 < t & t <= 1 holds
0 < (1 + (sqrt (1 - (t ^2)))) / t
Lm20:
for t being Real st 0 < t & t <> 1 holds
(2 * t) / ((t ^2) - 1) <> 0
Lm21:
for t being Real st t < 0 holds
(1 + (sqrt (1 + (t ^2)))) / t < 0