Lm26:
for n being Nat
for a being Real holds n * a = n * (In (a,F_Real))
Lm30:
for n being Nat
for z being Element of INT.Ring
for r being Integer st z = r holds
n * z = n * r
Lm1:
for n being Nat
for z being Element of INT.Ring holds n * z = (In (n,INT.Ring)) * z
Lm2:
for a being Integer
for n being Nat holds (In (a,INT)) |^ n = (In (a,INT.Ring)) |^ n
Lm3:
for n being Nat
for z being Element of INT.Ring
for r being Real st z = r holds
n * z = n * r
Lm14:
for z being Element of F_Real st z <> 0. F_Real holds
for n being Nat holds |.(power (z,n)).| = |.z.| to_power n
Lm15:
for m being positive Nat
for j being Nat
for ks being Real st j in Seg m & 0 <= ks & ks <= m holds
|.(j - ks).| <= m
Lm5:
for k being Nat holds eta (k,k) = k !
Lm16:
for m being positive Nat
for n being Nat
for m0 being Element of F_Real st m = m0 holds
m |^ n = m0 |^ n
Lm18:
for n being set
for p being finite-Support sequence of INT.Ring holds Support p = Support |.p.|
Lm19:
for n being Nat
for x being Element of F_Real st x > 0 holds
(power F_Real) . (x,n) = x to_power n
Lm22:
for m being positive Nat
for x0 being Element of F_Real
for s, z0 being Real st 0 < x0 & x0 <= m & 0 < s & s < 1 & 1 < z0 holds
|.(- (x0 * (z0 to_power (x0 * (1 - s))))).| <= m * (z0 to_power m)
Lm23:
for g being non zero Polynomial of INT.Ring holds rng |.g.| is finite
Lm4:
for i being Nat holds Roots (tau i) = {(In (i,INT.Ring))}
Lm6:
for f being Element of the carrier of (Polynom-Ring INT.Ring)
for n being non zero Nat
for i being Element of NAT holds
( ((~ ((tau 0) |^ n)) *' f) . (i + n) = f . i & ((~ ((tau 0) |^ n)) *' f) | (Segm n) = (Segm n) --> (0. INT.Ring) )
Lm7:
for p being prime odd Nat
for m being positive Nat
for i being Nat st i in Seg m holds
( (ff_0 (m,p)) /. i = (tau i) |^ p & (ff_0 (m,p)) . i = (tau i) |^ p & i in dom (ff_0 (m,p)) )
Lm8:
for i being Nat
for k being non zero Nat holds tau i divides (tau i) |^ k
Lm9:
for p being prime odd Nat
for m being positive Nat
for j being Nat st j in Seg m holds
Product (ff_0 (m,p)) = ((tau j) |^ p) * (Product (Del ((ff_0 (m,p)),j)))
Lm10:
for n, i being Nat holds (~ ((tau i) |^ n)) . 0 = (In ((- i),INT.Ring)) |^ n
Lm11:
for R being domRing
for k being Nat
for f being Element of the carrier of (Polynom-Ring R) holds ((Der1 R) |^ 0) . (f |^ k) = f |^ k
theorem Th29:
for
p being
prime odd Nat for
m being
positive Nat for
k,
j,
i being
Nat st
p + 1
< i &
i in dom (LBZ ((Der1 INT.Ring),k,(Product (Del ((ff_0 (m,p)),j))),((tau j) |^ p))) holds
(LBZ ((Der1 INT.Ring),k,(Product (Del ((ff_0 (m,p)),j))),((tau j) |^ p))) /. i = 0. (Polynom-Ring INT.Ring)
Lm12:
for p being prime odd Nat
for m being positive Nat
for g being non zero Polynomial of INT.Ring holds delta_1 (m,p,g) is FinSequence of INT.Ring
Lm13:
for i being Nat holds exp_R . i = (power F_Real) . ((In (number_e,F_Real)),i)
Lm17:
for p being prime odd Nat
for m being positive Nat
for x being Element of F_Real st 0 < x & x <= m holds
|.(eval ((~ (^ (Product (x. (m,p))))),x)).| <= m |^ (p * m)
Lm20:
for p being prime odd Nat
for m being positive Nat
for j being Element of F_Real st 0 < j & j <= m holds
eval ((~ (^ ((tau 0) |^ (p -' 1)))),j) <= m |^ (p -' 1)
Lm21:
for p being prime odd Nat
for m being positive Nat
for k being Element of F_Real st 0 < k & k <= m holds
|.((Eval (~ (^ (f_0 (m,p))))) . k).| <= m |^ ((p * m) + (p -' 1))
Lm24:
for p being prime odd Nat
for m being positive Nat
for g being non zero Polynomial of INT.Ring
for z0 being non zero Element of F_Real
for k being Nat st k in Seg m holds
( (delta (m,p,g,z0)) . k = (delta (m,p,g,z0)) /. k & (delta (m,p,g,z0)) . k = ((delta_1 (m,p,g)) . k) + ((delta_2 (m,p,g,z0)) . k) )
Lm25:
for p being prime odd Nat
for m being positive Nat
for g being non zero Polynomial of INT.Ring
for z0 being non zero Element of F_Real
for M being Nat st z0 = number_e & ( for i being Nat holds |.(g . i).| <= M ) holds
for k being Nat st k in Seg m holds
|.(((delta_1 (m,p,g)) . k) + ((delta_2 (m,p,g,z0)) . k)).| <= M * ((z0 to_power m) * (m |^ (p * (m + 1))))
Lm27:
for p being prime odd Nat
for m being positive Nat
for g being non zero Polynomial of INT.Ring
for z0 being non zero Element of F_Real
for M being Nat st z0 = number_e & ( for i being Nat holds |.(g . i).| <= M ) & ( for k being Nat st k in Seg m holds
|.(((delta_1 (m,p,g)) . k) + ((delta_2 (m,p,g,z0)) . k)).| <= M * ((z0 to_power m) * (m |^ (p * (m + 1)))) ) holds
Sum (delta (m,p,g,z0)) <= ((m * M) * (z0 to_power m)) * (m |^ (p * (m + 1)))
Lm28:
for p being prime odd Nat
for m being positive Nat
for g being non zero Polynomial of INT.Ring
for z0 being non zero Element of F_Real
for M being Nat st z0 = number_e & ( for i being Nat holds |.(g . i).| <= M ) & ( for k being Nat st k in Seg m holds
|.(((delta_1 (m,p,g)) . k) + ((delta_2 (m,p,g,z0)) . k)).| <= M * ((z0 to_power m) * (m |^ (p * (m + 1)))) ) holds
- (((m * M) * (z0 to_power m)) * (m |^ (p * (m + 1)))) <= Sum (delta (m,p,g,z0))
Lm8a:
for n being Nat
for f being Element of the carrier of (Polynom-Ring F_Rat) holds n * f = ((In (n,F_Rat)) | F_Rat) *' (~ f)
:: construct Polynomial
:: f(p,m) = x^{p-1}(1-x)^{p}(2-x)^{p}\cdots (n-x)^{p}
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::