assume
not number_e is transcendental
; contradiction
then consider g being INT -valued Polynomial of F_Rat such that
A2:
( @ g is irreducible & Ext_eval (g,(In (number_e,F_Real))) = 0 & deg g >= 2 & g . 0 <> 0. F_Rat )
by LMM;
reconsider g0 = g as Polynomial of INT.Ring by Th46;
A4:
deg (~ (@ g0)) = deg (~ (@ g))
by FIELD_4:20;
then
deg g0 in NAT
by A2, INT_1:3;
then A5:
g0 <> 0_. INT.Ring
by FIELD_1:1;
reconsider g0 = g as non zero Polynomial of INT.Ring by A5, UPROOTS:def 5;
reconsider m0 = deg g0 as positive Nat by A2, A4;
number_e <> 0. F_Real
;
then reconsider z0 = number_e as non zero Element of F_Real by XREAL_0:def 1, STRUCT_0:def 12;
reconsider g1 = g as Polynomial of F_Real by FIELD_4:8;
0 = eval ((~ (@ g1)),z0)
by A2, FIELD_4:26;
then A8:
Ext_eval ((~ (@ g0)),z0) = 0
by FIELD_4:26;
set g00 = g0 . 0;
consider M0 being Nat such that
A9:
for i being Nat holds |.(g0 . i).| <= M0
by Th43;
0 < |.(g0 . 0).|
by A2, GAUSSINT:def 14;
then reconsider M0 = M0 as non zero Nat by A9;
consider n1 being Nat such that
A10:
for n being Nat st n1 <= n holds
|.((((m0 |^ (m0 + 1)) |^ n) / (n !)) - 0).| < 1 / (2 * (((m0 * M0) * (m0 |^ (m0 + 1))) * (z0 to_power m0)))
by Th45;
reconsider M00 = (m0 * M0) * (m0 |^ (m0 + 1)) as Nat ;
consider p1 being Prime such that
A11:
(n1 + m0) + M0 < p1
by NEWTON:72;
2 <= (n1 + M0) + m0
by A2, A4, XREAL_1:38;
then
2 < p1
by XXREAL_0:2, A11;
then reconsider p1 = p1 as prime odd Nat by PEPIN:17;
1 < p1
by INT_2:def 4;
then A14:
p1 -' 1 = p1 - 1
by XREAL_1:233;
A15:
2 - 1 <= m0 - 1
by A2, A4, XREAL_1:9;
A16:
((n1 + m0) + M0) - 1 < p1 - 1
by A11, XREAL_1:8;
n1 <= n1 + M0
by XREAL_1:31;
then
n1 < (n1 + M0) + (m0 - 1)
by A15, XREAL_1:39;
then A17:
n1 < p1 -' 1
by A14, A16, XXREAL_0:2;
m0 <= m0 + (n1 + M0)
by XREAL_1:31;
then A18:
m0 < p1
by A11, XXREAL_0:2;
M0 <= M0 + (n1 + m0)
by XREAL_1:31;
then A19:
M0 < p1
by A11, XXREAL_0:2;
A20:
Sum (delta (m0,p1,g0,z0)) = (Sum (delta_1 (m0,p1,g0))) + (Sum (delta_2 (m0,p1,g0,z0)))
proof
A22:
len (delta_2 (m0,p1,g0,z0)) = m0
by Def6;
len (delta_1 (m0,p1,g0)) = m0
by Def5;
then dom (delta_1 (m0,p1,g0)) =
Seg m0
by FINSEQ_1:def 3
.=
dom (delta_2 (m0,p1,g0,z0))
by A22, FINSEQ_1:def 3
;
hence
Sum (delta (m0,p1,g0,z0)) = (Sum (delta_1 (m0,p1,g0))) + (Sum (delta_2 (m0,p1,g0,z0)))
by BINOM:7;
verum
end;
Sum (delta_1 (m0,p1,g0)) in INT.Ring
by Th36;
then reconsider S1 = Sum (delta_1 (m0,p1,g0)) as Element of INT.Ring ;
set pp1ft = p1 ! ;
reconsider p1ft = (p1 -' 1) ! as Nat ;
reconsider sgm0ft = In (((((- 1) |^ m0) * (m0 !)) |^ p1),INT.Ring) as Element of INT.Ring ;
reconsider p0 = p1 -' 1 as Nat ;
p0 + 1 =
(p1 - 1) + 1
.=
p1
;
then A25:
p1 ! = p1ft * p1
by SIN_COS:1;
consider u being Element of INT.Ring such that
A26:
('F' (f_0 (m0,p1))) . 0 = (((p1 -' 1) !) * (In (((((- 1) |^ m0) * (m0 !)) |^ p1),INT.Ring))) + ((In ((p1 !),INT.Ring)) * u)
by Th33;
A27:
( (Sum (delta_2 (m0,p1,g0,z0))) / ((p1 -' 1) !) is Element of INT.Ring & (Sum (delta_2 (m0,p1,g0,z0))) / ((p1 -' 1) !) = ((In (((((- 1) |^ m0) * (m0 !)) |^ p1),INT.Ring)) + (p1 * u)) * (g0 . 0) )
proof
A28:
Sum (delta_2 (m0,p1,g0,z0)) = ((g0 . 0) * (('F' (f_0 (m0,p1))) . 0)) - ((Ext_eval (g0,z0)) * (('F' (f_0 (m0,p1))) . 0))
by Th37;
set sgmp1u =
sgm0ft + (p1 * u);
A29:
('F' (f_0 (m0,p1))) . 0 =
(p1ft * sgm0ft) + ((p1ft * p1) * u)
by A25, A26, Lm1
.=
(p1ft * sgm0ft) + (p1ft * (p1 * u))
by E_TRANS1:1
.=
p1ft * (sgm0ft + (p1 * u))
by RINGDER1:1
;
reconsider xfr = 1
/ p1ft as
Element of
F_Rat by GAUSSINT:def 14, RAT_1:def 2;
p1ft in NAT
by ORDINAL1:def 12;
then A30:
(p1ft * (sgm0ft + (p1 * u))) * (g0 . 0) =
p1ft * ((sgm0ft + (p1 * u)) * (g0 . 0))
by BINOM:19
.=
p1ft * ((sgm0ft + (p1 * u)) * (g0 . 0))
;
reconsider sgmg00 =
(sgm0ft + (p1 * u)) * (g0 . 0) as
Real ;
(Sum (delta_2 (m0,p1,g0,z0))) / p1ft =
(sgmg00 * p1ft) / p1ft
by Lm3, A30, A29, A28, A8
.=
(sgm0ft + (p1 * u)) * (g0 . 0)
by XCMPLX_1:89
;
hence
(
(Sum (delta_2 (m0,p1,g0,z0))) / ((p1 -' 1) !) is
Element of
INT.Ring &
(Sum (delta_2 (m0,p1,g0,z0))) / ((p1 -' 1) !) = ((In (((((- 1) |^ m0) * (m0 !)) |^ p1),INT.Ring)) + (p1 * u)) * (g0 . 0) )
;
verum
end;
A32:
Sum (delta_1 (m0,p1,g0)) in {(In ((p1 !),INT.Ring))} -Ideal
by Th38;
Sum (delta_1 (m0,p1,g0)) in { ((In ((p1 !),INT.Ring)) * r) where r is Element of INT.Ring : verum }
by A32, IDEAL_1:64;
then consider v being Element of INT.Ring such that
A33:
Sum (delta_1 (m0,p1,g0)) = (In ((p1 !),INT.Ring)) * v
;
reconsider vr = v as Real ;
A34:
(Sum (delta_1 (m0,p1,g0))) / ((p1 -' 1) !) = p1 * v
A35:
( (Sum (delta (m0,p1,g0,z0))) / ((p1 -' 1) !) in INT.Ring & (Sum (delta (m0,p1,g0,z0))) / ((p1 -' 1) !) = ((Sum (delta_1 (m0,p1,g0))) / ((p1 -' 1) !)) + ((Sum (delta_2 (m0,p1,g0,z0))) / ((p1 -' 1) !)) )
proof
reconsider S2p1 =
(Sum (delta_2 (m0,p1,g0,z0))) / ((p1 -' 1) !) as
Element of
INT.Ring by A27;
reconsider S1p1 =
(Sum (delta_1 (m0,p1,g0))) / ((p1 -' 1) !) as
Element of
INT.Ring by A34;
(Sum (delta (m0,p1,g0,z0))) / ((p1 -' 1) !) = S1p1 + S2p1
by A20;
hence
(
(Sum (delta (m0,p1,g0,z0))) / ((p1 -' 1) !) in INT.Ring &
(Sum (delta (m0,p1,g0,z0))) / ((p1 -' 1) !) = ((Sum (delta_1 (m0,p1,g0))) / ((p1 -' 1) !)) + ((Sum (delta_2 (m0,p1,g0,z0))) / ((p1 -' 1) !)) )
;
verum
end;
A37:
for k being Nat st k in Seg m0 holds
|.(((delta_1 (m0,p1,g0)) . k) + ((delta_2 (m0,p1,g0,z0)) . k)).| <= M0 * ((z0 to_power m0) * (m0 |^ (p1 * (m0 + 1))))
by A9, Lm25;
A40: ((m0 * M0) * (z0 to_power m0)) * (m0 |^ (p1 * (m0 + 1))) =
((m0 * M0) * (z0 to_power m0)) * ((m0 |^ (m0 + 1)) |^ ((p1 - 1) + 1))
by NEWTON:9
.=
((m0 * M0) * (z0 to_power m0)) * ((m0 |^ (m0 + 1)) * ((m0 |^ (m0 + 1)) |^ (p1 - 1)))
by NEWTON:6
.=
(M00 * (z0 to_power m0)) * ((m0 |^ (m0 + 1)) |^ (p1 - 1))
;
|.((((m0 |^ (m0 + 1)) |^ p0) / (p0 !)) - 0).| < 1 / (2 * (M00 * (z0 to_power m0)))
by A10, A17;
then A41:
((m0 |^ (m0 + 1)) |^ p0) / (p0 !) <= 1 / (2 * (M00 * (z0 to_power m0)))
by ABSVALUE:def 1;
A38:
|.((Sum (delta (m0,p1,g0,z0))) / ((p1 -' 1) !)).| <= 1 / 2
proof
reconsider x =
M00 * (z0 to_power m0) as
Real ;
x * (1 / (2 * x)) = 1
/ 2
by TAYLOR_1:11, XCMPLX_1:92;
then A43:
(M00 * (z0 to_power m0)) * (((m0 |^ (m0 + 1)) |^ p0) / (p0 !)) <= 1
/ 2
by A41, TAYLOR_1:11, XREAL_1:64;
A44:
(- (((m0 * M0) * (z0 to_power m0)) * (m0 |^ (p1 * (m0 + 1))))) / ((p1 -' 1) !) <= (Sum (delta (m0,p1,g0,z0))) / ((p1 -' 1) !)
by XREAL_1:72, Lm28, A37, A9;
reconsider mMzmp1 =
((m0 * M0) * (z0 to_power m0)) * (m0 |^ (p1 * (m0 + 1))) as
Real ;
reconsider M00zmp0 =
(M00 * (z0 to_power m0)) * ((m0 |^ (m0 + 1)) |^ (p1 - 1)) as
Real ;
A45:
(- mMzmp1) / ((p1 -' 1) !) = - (M00zmp0 / ((p1 -' 1) !))
by A40;
- (1 / 2) <= - (M00zmp0 / ((p1 -' 1) !))
by A14, A43, XREAL_1:24;
then A46:
- (1 / 2) <= (Sum (delta (m0,p1,g0,z0))) / ((p1 -' 1) !)
by A44, A45, XXREAL_0:2;
(Sum (delta (m0,p1,g0,z0))) / ((p1 -' 1) !) <= M00zmp0 / ((p1 -' 1) !)
by A40, XREAL_1:72, Lm27, A37, A9;
then
(Sum (delta (m0,p1,g0,z0))) / ((p1 -' 1) !) <= 1
/ 2
by A14, A43, XXREAL_0:2;
hence
|.((Sum (delta (m0,p1,g0,z0))) / ((p1 -' 1) !)).| <= 1
/ 2
by A46, ABSVALUE:5;
verum
end;
A49:
(Sum (delta (m0,p1,g0,z0))) / ((p1 -' 1) !) = 0
A50:
- (p1 * v) = ((In (((((- 1) |^ m0) * (m0 !)) |^ p1),INT.Ring)) * (g0 . 0)) + ((p1 * u) * (g0 . 0))
by A27, A49, A34, A35;
A51: (In (((((- 1) |^ m0) * (m0 !)) |^ p1),INT.Ring)) * (g0 . 0) =
((((- 1) |^ m0) |^ p1) * ((m0 !) |^ p1)) * (g0 . 0)
by NEWTON:7
.=
(((- 1) |^ (m0 * p1)) * ((m0 !) |^ p1)) * (g0 . 0)
by NEWTON:9
;
reconsider uI = u, vI = v, g0I = g0 . 0 as Integer ;
p1 in NAT
by ORDINAL1:def 12;
then (p1 * u) * (g0 . 0) =
p1 * (u * (g0 . 0))
by BINOM:19
.=
p1 * (uI * g0I)
by Lm30
;
then A54:
(- (p1 * v)) - ((p1 * u) * (g0 . 0)) = (- (p1 * vI)) - (p1 * (uI * g0I))
by Lm3;
|.(- 1).| = - (- 1)
by ABSVALUE:def 1;
then A55: |.((- 1) |^ (m0 * p1)).| =
1 |^ (m0 * p1)
by TAYLOR_2:1
.=
1
;
A56: |.((((- 1) |^ (m0 * p1)) * ((m0 !) |^ p1)) * g0I).| =
|.(((- 1) |^ (m0 * p1)) * ((m0 !) |^ p1)).| * |.g0I.|
by COMPLEX1:65
.=
(|.((- 1) |^ (m0 * p1)).| * |.((m0 !) |^ p1).|) * |.g0I.|
by COMPLEX1:65
.=
|.(((m0 !) |^ p1) * g0I).|
by COMPLEX1:65, A55
;
|.(g0 . 0).| <= M0
by A9;
then A57:
|.(g0 . 0).| < p1
by A19, XXREAL_0:2;
p1 = |.p1.|
by ABSVALUE:def 1;
then A59:
not p1 divides g0I
by INT_2:16, INT_2:27, A57, A2, GAUSSINT:def 14;
not p1 divides (m0 !) |^ p1
by NAT_3:5, A18, NAT_4:19;
then
not |.p1.| divides |.((((- 1) |^ (m0 * p1)) * ((m0 !) |^ p1)) * g0I).|
by A56, NAT_6:7, A59, INT_2:16;
then A61:
not p1 divides (((- 1) |^ (m0 * p1)) * ((m0 !) |^ p1)) * g0I
by INT_2:16;
(- (p1 * vI)) - (p1 * (uI * g0I)) = p1 * ((- vI) - (uI * g0I))
;
hence
contradiction
by A61, A50, A51, A54; verum