environ
vocabularies HIDDEN, NUMBERS, REAL_1, XREAL_0, SUBSET_1, COMSEQ_1, SEQ_1, FDIFF_1, XXREAL_0, CARD_1, COMPLEX1, FUNCT_1, RELAT_1, XCMPLX_0, ARYTM_3, NAT_1, REALSET1, NEWTON, ARYTM_1, VALUED_1, SERIES_1, PREPOWER, CARD_3, SEQ_2, ORDINAL2, SQUARE_1, VALUED_0, XXREAL_2, FUNCT_2, TARSKI, RCOMP_1, XXREAL_1, PARTFUN1, XBOOLE_0, FCONT_1, SIN_COS, FUNCT_7, ORDINAL1;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XXREAL_0, XREAL_0, ABIAN, XCMPLX_0, COMPLEX1, REAL_1, RELAT_1, FUNCT_1, RELSET_1, FCONT_1, FUNCT_2, VALUED_1, SEQ_1, SEQ_2, FDIFF_1, SERIES_1, NAT_1, NEWTON, SQUARE_1, PARTFUN1, VALUED_0, RCOMP_1, NAT_D, RFUNCT_1, COMSEQ_1, COMSEQ_2, COMSEQ_3, PREPOWER;
definitions FUNCT_2;
theorems NAT_1, ABSVALUE, INT_1, SEQ_1, SEQ_2, SERIES_1, SEQM_3, SEQ_4, PREPOWER, COMPLEX1, COMSEQ_1, COMSEQ_2, SQUARE_1, COMSEQ_3, FCONT_2, RCOMP_1, FUNCT_1, FDIFF_1, FDIFF_2, FCONT_1, TARSKI, FUNCT_2, RFUNCT_1, SUBSET_1, POWER, ROLLE, NEWTON, RELAT_1, XREAL_0, XBOOLE_0, XBOOLE_1, XCMPLX_0, XCMPLX_1, XREAL_1, XXREAL_0, ORDINAL1, VALUED_1, XXREAL_1, VALUED_0, NUMBERS;
schemes NAT_1, SEQ_1, COMSEQ_1, CLASSES1, FUNCT_2;
registrations XBOOLE_0, ORDINAL1, RELSET_1, FUNCT_2, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, SQUARE_1, NAT_1, MEMBERED, RCOMP_1, COMSEQ_2, FDIFF_1, NEWTON, COMSEQ_3, VALUED_0, VALUED_1, SEQ_4, FCONT_3, ABIAN, SEQ_2, INT_1;
constructors HIDDEN, PARTFUN1, FUNCT_4, ARYTM_0, REAL_1, SQUARE_1, NAT_1, RCOMP_1, RFUNCT_1, COMSEQ_2, RFUNCT_2, FCONT_1, FDIFF_1, PREPOWER, COMSEQ_3, NAT_D, RECDEF_1, SEQM_3, SERIES_1, SEQ_2, VALUED_1, RELSET_1, ABIAN, BINOP_2, RVSUM_1, XXREAL_2, NUMBERS;
requirements HIDDEN, REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
equalities COMSEQ_3, SQUARE_1, SUBSET_1, VALUED_1, XCMPLX_0, COMPLEX1;
expansions COMSEQ_3, VALUED_1, FUNCT_2;
1 in NAT
;
then reconsider jj = 1 as Element of REAL by NUMBERS:19;
theorem Th2:
for
k,
m being
Nat holds
( (
0 < k implies
((k -' 1) !) * k = k ! ) & (
k <= m implies
((m -' k) !) * ((m + 1) - k) = ((m + 1) -' k) ! ) )
Lm1:
for p1, p2, g1, g2 being Real holds
( (p1 + (g1 * <i>)) * (p2 + (g2 * <i>)) = ((p1 * p2) - (g1 * g2)) + (((p1 * g2) + (p2 * g1)) * <i>) & (p2 + (g2 * <i>)) *' = p2 + ((- g2) * <i>) )
Lm2:
for z, w being Complex holds (Sum (z ExpSeq)) * (Sum (w ExpSeq)) = Sum ((z + w) ExpSeq)
Lm3:
for th being Real holds Sum ((th * <i>) ExpSeq) = (cos . th) + ((sin . th) * <i>)
Lm4:
for th being Real holds (Sum ((th * <i>) ExpSeq)) *' = Sum ((- (th * <i>)) ExpSeq)
Lm5:
for th, th1 being Real st th = th1 holds
( |.(Sum ((th * <i>) ExpSeq)).| = 1 & |.(sin . th1).| <= 1 & |.(cos . th1).| <= 1 )
deffunc H1( Real) -> set = (2 * $1) + 1;
consider bq being Real_Sequence such that
Lm6:
for n being Nat holds bq . n = H1(n)
from SEQ_1:sch 1();
bq is increasing sequence of NAT
then reconsider bq = bq as increasing sequence of NAT ;
Lm7:
for n being Nat
for th, th1, th2, th3 being Real holds
( th |^ (2 * n) = (th |^ n) |^ 2 & (- 1) |^ (2 * n) = 1 & (- 1) |^ ((2 * n) + 1) = - 1 )
theorem Th38:
for
k,
n being
Nat st
n <= k holds
n ! <= k !
Lm8:
for n being Nat
for z being Complex holds
( (z ExpSeq) . 1 = z & (z ExpSeq) . 0 = 1r & |.(z |^ n).| = |.z.| |^ n )
Lm9:
for th being Real holds Sum (th ExpSeq) = Sum (th rExpSeq)
Lm10:
for p, q being Real holds exp_R . (p + q) = (exp_R . p) * (exp_R . q)
Lm11:
exp_R . 0 = 1
Lm12:
for p being Real
for z being Complex holds
( Re ((p * <i>) * z) = - (p * (Im z)) & Im ((p * <i>) * z) = p * (Re z) & Re (p * z) = p * (Re z) & Im (p * z) = p * (Im z) )
Lm13:
for p being Real
for z being Complex st p > 0 holds
( Re (z / (p * <i>)) = (Im z) / p & Im (z / (p * <i>)) = - ((Re z) / p) & |.(z / p).| = |.z.| / p )
Lm14:
( dom (tan | [.0,1.]) = [.0,1.] & ( for th being Real st th in [.0,1.] holds
(tan | [.0,1.]) . th = tan . th ) )
Lm15:
( tan is_differentiable_on ].0,1.[ & ( for th being Real st th in ].0,1.[ holds
diff (tan,th) > 0 ) )
Lm16:
( tan . 0 = 0 & tan . 1 > 1 )
Lm17:
for th being Real st th in [.0,1.] holds
sin . th >= 0