let p be INT -valued Polynomial of F_Real; for e being Element of F_Real st e is_a_root_of p holds
for k, l being Integer st l <> 0 & e = k / l & k,l are_coprime holds
( k divides p . 0 & l divides LC p )
let e be Element of F_Real; ( e is_a_root_of p implies for k, l being Integer st l <> 0 & e = k / l & k,l are_coprime holds
( k divides p . 0 & l divides LC p ) )
assume A1:
e is_a_root_of p
; for k, l being Integer st l <> 0 & e = k / l & k,l are_coprime holds
( k divides p . 0 & l divides LC p )
let k, l be Integer; ( l <> 0 & e = k / l & k,l are_coprime implies ( k divides p . 0 & l divides LC p ) )
assume A2:
( l <> 0 & e = k / l & k,l are_coprime )
; ( k divides p . 0 & l divides LC p )
consider F being FinSequence of F_Real such that
A3:
( 0. F_Real = Sum F & len F = len p & ( for n being Element of NAT st n in dom F holds
F . n = (p . (n -' 1)) * ((power F_Real) . (e,(n -' 1))) ) )
by A1, POLYNOM4:def 2;
per cases
( len F = 0 or len F > 0 )
;
suppose A5:
len F > 0
;
( k divides p . 0 & l divides LC p )set n =
len p;
A6:
len p >= 1
by A5, A3, NAT_1:14;
reconsider n1 =
(len p) - 1 as
Element of
NAT by NAT_1:20, A5, A3;
A7:
(len p) -' 1
= n1
by A5, A3, NAT_1:14, XREAL_1:233;
A8:
l |^ ((len p) -' 1) <> 0
by A2, CARD_4:3;
reconsider k1 =
k,
l1 =
l as
Element of
F_Real by XREAL_0:def 1;
set ln =
(power F_Real) . (
l1,
n1);
set G =
((power F_Real) . (l1,n1)) * F;
reconsider FF =
F as
Element of
(len F) -tuples_on the
carrier of
F_Real by FINSEQ_2:92;
set GG =
((power F_Real) . (l1,n1)) * FF;
A9:
len (((power F_Real) . (l1,n1)) * FF) = len F
by FINSEQ_2:132;
then A10:
dom (((power F_Real) . (l1,n1)) * F) = dom F
by FINSEQ_3:29;
A11:
Sum (((power F_Real) . (l1,n1)) * F) = ((power F_Real) . (l1,n1)) * (Sum F)
by FVSUM_1:73;
rng (((power F_Real) . (l1,n1)) * F) c= INT
proof
let o be
object ;
TARSKI:def 3 ( not o in rng (((power F_Real) . (l1,n1)) * F) or o in INT )
assume
o in rng (((power F_Real) . (l1,n1)) * F)
;
o in INT
then consider b being
object such that A12:
(
b in dom (((power F_Real) . (l1,n1)) * F) &
o = (((power F_Real) . (l1,n1)) * F) . b )
by FUNCT_1:def 3;
reconsider b =
b as
Element of
NAT by A12;
b in Seg (len p)
by A12, A9, A3, FINSEQ_1:def 3;
then
( 1
<= b &
b <= len p &
b -' 1
<= b )
by FINSEQ_1:1, NAT_D:35;
then
(
b -' 1
= b - 1 &
b - 1
<= n1 )
by XREAL_1:233, XREAL_1:9;
then consider c being
Nat such that A13:
n1 = (b -' 1) + c
by NAT_1:10;
rng F c= the
carrier of
F_Real
;
then reconsider a9 =
F . b as
Element of
F_Real by A12, A10, FUNCT_1:3;
A14:
l |^ (b -' 1) <> 0
by A2, CARD_4:3;
(
b in dom (((power F_Real) . (l1,n1)) * F) &
a9 = F . b implies
(((power F_Real) . (l1,n1)) * F) . b = ((power F_Real) . (l1,n1)) * a9 )
by FVSUM_1:50;
then (((power F_Real) . (l1,n1)) * F) . b =
((power F_Real) . (l1,n1)) * ((p . (b -' 1)) * ((power F_Real) . (e,(b -' 1))))
by A3, A12, A10
.=
(p . (b -' 1)) * (((power F_Real) . (l1,n1)) * ((power F_Real) . (e,(b -' 1))))
.=
(p . (b -' 1)) * ((l1 |^ n1) * ((power F_Real) . (e,(b -' 1))))
by Th48
.=
(p . (b -' 1)) * ((l1 |^ n1) * ((k / l) |^ (b -' 1)))
by A2, Th48
.=
(p . (b -' 1)) * ((l |^ n1) * ((k |^ (b -' 1)) / (l |^ (b -' 1))))
by PREPOWER:8
.=
((p . (b -' 1)) * (k |^ (b -' 1))) * ((l |^ n1) / (l |^ (b -' 1)))
.=
((p . (b -' 1)) * (k |^ (b -' 1))) * (((l |^ c) * (l |^ (b -' 1))) / (l |^ (b -' 1)))
by A13, NEWTON:8
.=
((p . (b -' 1)) * (k |^ (b -' 1))) * ((l |^ c) * ((l |^ (b -' 1)) / (l |^ (b -' 1))))
.=
((p . (b -' 1)) * (k |^ (b -' 1))) * ((l |^ c) * 1)
by XCMPLX_1:60, A14
.=
((p . (b -' 1)) * (k |^ (b -' 1))) * (l |^ c)
;
hence
o in INT
by INT_1:def 2, A12;
verum
end; then reconsider G1 =
((power F_Real) . (l1,n1)) * F as
INT -valued non
empty FinSequence by A9, A5, RELAT_1:def 19;
A15:
1
in dom (((power F_Real) . (l1,n1)) * F)
by A9, A6, A3, FINSEQ_3:25;
A16:
Sum G1 = Sum (((power F_Real) . (l1,n1)) * F)
by Th49;
A17:
Sum G1 = 0
by A3, A11, Th49;
reconsider Gn0 =
G1 /^ 1 as
INT -valued FinSequence ;
((power F_Real) . (l1,n1)) * F = <*((((power F_Real) . (l1,n1)) * F) /. 1)*> ^ Gn0
by FINSEQ_5:29;
then
(Sum Gn0) + ((((power F_Real) . (l1,n1)) * F) /. 1) = 0
by RVSUM_1:76, A16, A11, A3;
then
(Sum Gn0) + ((((power F_Real) . (l1,n1)) * F) . 1) = 0
by A15, PARTFUN1:def 6;
then A18:
Sum Gn0 = - (G1 . 1)
;
rng F c= the
carrier of
F_Real
;
then reconsider a9 =
F . 1 as
Element of
F_Real by A15, A10, FUNCT_1:3;
A19:
G1 . 1 =
((power F_Real) . (l1,n1)) * a9
by FVSUM_1:50, A15
.=
((power F_Real) . (l1,n1)) * ((p . (1 -' 1)) * ((power F_Real) . (e,(1 -' 1))))
by A6, A3, FINSEQ_3:25
.=
((p . (1 -' 1)) * ((power F_Real) . (l1,n1))) * ((power F_Real) . (e,(1 -' 1)))
.=
((p . (1 -' 1)) * ((power F_Real) . (l1,n1))) * ((power F_Real) . (e,0))
by XREAL_1:232
.=
((p . 0) * ((power F_Real) . (l1,n1))) * ((power F_Real) . (e,0))
by XREAL_1:232
.=
((p . 0) * ((power F_Real) . (l1,n1))) * (1_ F_Real)
by GROUP_1:def 7
.=
(p . 0) * (l |^ n1)
by Th48
;
for
i being
Nat st
i in dom Gn0 holds
k divides Gn0 . i
proof
let i be
Nat;
( i in dom Gn0 implies k divides Gn0 . i )
assume A20:
i in dom Gn0
;
k divides Gn0 . i
then A21:
1
+ i in dom G1
by FINSEQ_5:26;
rng F c= the
carrier of
F_Real
;
then reconsider a9 =
F . (1 + i) as
Element of
F_Real by A21, A10, FUNCT_1:3;
A22:
l |^ i <> 0
by A2, CARD_4:3;
A23:
( 1
<= i &
i <= len Gn0 )
by A20, FINSEQ_3:25;
i + 1
in Seg (len p)
by A3, A21, A9, FINSEQ_1:def 3;
then
i + 1
<= len p
by FINSEQ_1:1;
then
(i + 1) - 1
<= (len p) - 1
by XREAL_1:9;
then consider d being
Nat such that A24:
n1 = i + d
by NAT_1:10;
Gn0 . i =
((((power F_Real) . (l1,n1)) * F) /^ 1) /. i
by A20, PARTFUN1:def 6
.=
(((power F_Real) . (l1,n1)) * F) /. (1 + i)
by FINSEQ_5:27, A20
.=
(((power F_Real) . (l1,n1)) * F) . (1 + i)
by A21, PARTFUN1:def 6
.=
((power F_Real) . (l1,n1)) * a9
by FVSUM_1:50, A21
.=
((power F_Real) . (l1,n1)) * ((p . ((1 + i) -' 1)) * ((power F_Real) . (e,((1 + i) -' 1))))
by A3, A21, A10
.=
((power F_Real) . (l1,n1)) * ((p . i) * ((power F_Real) . (e,((1 + i) -' 1))))
by NAT_D:34
.=
((power F_Real) . (l1,n1)) * ((p . i) * ((power F_Real) . (e,i)))
by NAT_D:34
.=
(p . i) * (((power F_Real) . (l1,n1)) * ((power F_Real) . (e,i)))
.=
(p . i) * ((l1 |^ n1) * ((power F_Real) . (e,i)))
by Th48
.=
(p . i) * ((l1 |^ n1) * (e |^ i))
by Th48
.=
(p . i) * ((l |^ n1) * ((k |^ i) / (l |^ i)))
by A2, PREPOWER:8
.=
((p . i) * (k |^ i)) * ((l |^ (d + i)) / (l |^ i))
by A24
.=
((p . i) * (k |^ i)) * (((l |^ d) * (l |^ i)) / (l |^ i))
by NEWTON:8
.=
((p . i) * (k |^ i)) * ((l |^ d) * ((l |^ i) / (l |^ i)))
.=
((p . i) * (k |^ i)) * ((l |^ d) * 1)
by XCMPLX_1:60, A22
.=
((p . i) * (l |^ d)) * (k |^ i)
;
hence
k divides Gn0 . i
by A23, Th4, INT_2:2;
verum
end; then
k divides G1 . 1
by A18, NEWTON04:80, INT_2:10;
hence
k divides p . 0
by A19, A2, WSIERP_1:10, INT_2:25;
l divides LC preconsider Gn1 =
G1 | (Seg n1) as
INT -valued FinSequence by FINSEQ_1:15;
A25:
len (((power F_Real) . (l1,n1)) * FF) = len F
by FINSEQ_2:132;
then A26:
len G1 = n1 + 1
by A3;
G1 = Gn1 ^ <*(G1 . (n1 + 1))*>
by A25, A3, FINSEQ_3:55;
then
(Sum Gn1) + (G1 . (n1 + 1)) = 0
by RVSUM_1:74, A17;
then A27:
Sum Gn1 =
- (G1 . (n1 + 1))
.=
- (G1 . (len p))
;
A28:
len p in dom F
by FINSEQ_3:25, A6, A3;
rng F c= the
carrier of
F_Real
;
then reconsider a9 =
F . (len p) as
Element of
F_Real by A28, FUNCT_1:3;
len p in dom G1
by A25, A3, FINSEQ_3:25, A6;
then A29:
G1 . (len p) =
((power F_Real) . (l1,n1)) * a9
by FVSUM_1:50
.=
((power F_Real) . (l1,n1)) * ((p . ((len p) -' 1)) * ((power F_Real) . (e,((len p) -' 1))))
by A6, A3, FINSEQ_3:25
.=
(p . ((len p) -' 1)) * (((power F_Real) . (l1,n1)) * ((power F_Real) . (e,((len p) -' 1))))
.=
(p . ((len p) -' 1)) * ((l1 |^ n1) * ((power F_Real) . (e,((len p) -' 1))))
by Th48
.=
(p . ((len p) -' 1)) * ((l1 |^ n1) * (e |^ ((len p) -' 1)))
by Th48
.=
(p . ((len p) -' 1)) * ((l |^ n1) * ((k |^ ((len p) -' 1)) / (l |^ ((len p) -' 1))))
by A2, PREPOWER:8
.=
((p . ((len p) -' 1)) * (k |^ ((len p) -' 1))) * ((l |^ ((len p) -' 1)) / (l |^ ((len p) -' 1)))
by A7
.=
((p . ((len p) -' 1)) * (k |^ ((len p) -' 1))) * 1
by A8, XCMPLX_1:60
.=
(LC p) * (k |^ ((len p) -' 1))
;
for
i being
Nat st
i in dom Gn1 holds
l divides Gn1 . i
proof
let i be
Nat;
( i in dom Gn1 implies l divides Gn1 . i )
assume A30:
i in dom Gn1
;
l divides Gn1 . i
then
i in Seg n1
by A26, FINSEQ_3:54;
then A31:
( 1
<= i &
i <= n1 &
i -' 1
<= i )
by FINSEQ_1:1, NAT_D:35;
then consider d being
Nat such that A32:
n1 = (i -' 1) + d
by XXREAL_0:2, NAT_1:10;
i - i <= ((len p) - 1) - i
by A31, XREAL_1:9;
then A33:
0 + 1
<= (((len p) - i) - 1) + 1
by XREAL_1:6;
A34:
(len p) - 1
= (i - 1) + d
by A32, A31, XREAL_1:233;
A35:
Gn1 . i = G1 . i
by A30, FUNCT_1:47;
A36:
dom Gn1 c= dom G1
by RELAT_1:60;
rng F c= the
carrier of
F_Real
;
then reconsider a9 =
F . i as
Element of
F_Real by A36, A10, A30, FUNCT_1:3;
A37:
l |^ (i -' 1) <> 0
by A2, CARD_4:3;
G1 . i =
((power F_Real) . (l1,n1)) * a9
by A36, A30, FVSUM_1:50
.=
((power F_Real) . (l1,n1)) * ((p . (i -' 1)) * ((power F_Real) . (e,(i -' 1))))
by A3, A36, A30, A10
.=
(p . (i -' 1)) * (((power F_Real) . (l1,n1)) * ((power F_Real) . (e,(i -' 1))))
.=
(p . (i -' 1)) * ((l1 |^ n1) * ((power F_Real) . (e,(i -' 1))))
by Th48
.=
(p . (i -' 1)) * ((l1 |^ n1) * (e |^ (i -' 1)))
by Th48
.=
(p . (i -' 1)) * ((l |^ n1) * ((k |^ (i -' 1)) / (l |^ (i -' 1))))
by A2, PREPOWER:8
.=
((p . (i -' 1)) * (k |^ (i -' 1))) * ((l |^ n1) / (l |^ (i -' 1)))
.=
((p . (i -' 1)) * (k |^ (i -' 1))) * (((l |^ d) * (l |^ (i -' 1))) / (l |^ (i -' 1)))
by A32, NEWTON:8
.=
((p . (i -' 1)) * (k |^ (i -' 1))) * ((l |^ d) * ((l |^ (i -' 1)) / (l |^ (i -' 1))))
.=
((p . (i -' 1)) * (k |^ (i -' 1))) * ((l |^ d) * 1)
by XCMPLX_1:60, A37
.=
((p . (i -' 1)) * (k |^ (i -' 1))) * (l |^ d)
;
hence
l divides Gn1 . i
by A35, A34, A33, Th4, INT_2:2;
verum
end; then
l divides G1 . (len p)
by A27, NEWTON04:80, INT_2:10;
hence
l divides LC p
by A29, A2, WSIERP_1:10, INT_2:25;
verum end;