let L be Field; for p, q being Polynomial of L st len p <> 0 & len q > 1 holds
len (Subst (p,q)) = ((((len p) * (len q)) - (len p)) - (len q)) + 2
let p, q be Polynomial of L; ( len p <> 0 & len q > 1 implies len (Subst (p,q)) = ((((len p) * (len q)) - (len p)) - (len q)) + 2 )
assume that
A1:
len p <> 0
and
A2:
len q > 1
; len (Subst (p,q)) = ((((len p) * (len q)) - (len p)) - (len q)) + 2
consider F being FinSequence of the carrier of (Polynom-Ring L) such that
A3:
Subst (p,q) = Sum F
and
A4:
len F = len p
and
A5:
for n being Element of NAT st n in dom F holds
F . n = (p . (n -' 1)) * (q `^ (n -' 1))
by Def6;
A6:
0 + 1 <= len F
by A1, A4, NAT_1:13;
then A7:
1 in dom F
by FINSEQ_3:25;
reconsider k = ((((len p) * (len q)) - (len p)) - (len q)) + 1 as Element of NAT by A1, A2, Th1, INT_1:3;
len p >= 0 + 1
by A1, NAT_1:13;
then A8:
(len p) - 1 >= 0
;
A9: len (q `^ ((len F) -' 1)) =
((((len p) -' 1) * (len q)) - ((len p) -' 1)) + 1
by A2, A4, Th23
.=
((((len p) -' 1) * (len q)) - ((len p) - 1)) + 1
by A8, XREAL_0:def 2
.=
((((len p) - 1) * (len q)) - ((len p) - 1)) + 1
by A8, XREAL_0:def 2
.=
((((len p) * (len q)) - (len p)) - (len q)) + (1 + 1)
;
A10:
len (Subst (p,q)) >= ((((len p) * (len q)) - (len p)) - (len q)) + (1 + 1)
proof
set lF1 =
(len F) -' 1;
set F1 =
F | ((len F) -' 1);
reconsider sF1 =
Sum (F | ((len F) -' 1)) as
Polynomial of
L by POLYNOM3:def 10;
A11:
len F = ((len F) -' 1) + 1
by A6, XREAL_1:235;
then A12:
F = (F | ((len F) -' 1)) ^ <*(F /. (len F))*>
by FINSEQ_5:21;
then A13:
Sum F = (Sum (F | ((len F) -' 1))) + (F /. (len F))
by FVSUM_1:71;
A14:
len F = (len (F | ((len F) -' 1))) + 1
by A12, FINSEQ_2:16;
assume A15:
len (Subst (p,q)) < ((((len p) * (len q)) - (len p)) - (len q)) + (1 + 1)
;
contradiction
then
len (Subst (p,q)) < k + 1
;
then
len (Subst (p,q)) <= k
by NAT_1:13;
then A16:
(Subst (p,q)) . k = 0. L
by ALGSEQ_1:8;
now contradictionper cases
( len (F | ((len F) -' 1)) <> {} or len (F | ((len F) -' 1)) = {} )
;
suppose A17:
len (F | ((len F) -' 1)) <> {}
;
contradictiondefpred S1[
Nat]
means for
F2 being
Polynomial of
L st
F2 = Sum ((F | ((len F) -' 1)) | $1) holds
len F2 <= ((($1 * (len q)) - (len q)) - $1) + 2;
A18:
(F | ((len F) -' 1)) | (len (F | ((len F) -' 1))) = F | ((len F) -' 1)
by FINSEQ_1:58;
A19:
for
n being non
zero Nat st
S1[
n] holds
S1[
n + 1]
proof
let n be non
zero Nat;
( S1[n] implies S1[n + 1] )
assume A20:
for
F2 being
Polynomial of
L st
F2 = Sum ((F | ((len F) -' 1)) | n) holds
len F2 <= (((n * (len q)) - (len q)) - n) + 2
;
S1[n + 1]
len q >= 0 + (1 + 1)
by A2, NAT_1:13;
then
(len q) - 2
>= 0
by XREAL_1:19;
then
(((n * (len q)) - n) + 1) + 0 <= (((n * (len q)) - n) + 1) + ((len q) - 2)
by XREAL_1:7;
then
(
((((n * (len q)) - (len q)) - n) + 2) + 0 <= ((((n * (len q)) - (len q)) - n) + 2) + 1 &
(((n * (len q)) - n) + 1) - ((len q) - 2) <= ((n * (len q)) - n) + 1 )
by XREAL_1:6, XREAL_1:20;
then A21:
(((n * (len q)) - (len q)) - n) + 2
<= ((n * (len q)) - n) + 1
by XXREAL_0:2;
reconsider F3 =
Sum ((F | ((len F) -' 1)) | n) as
Polynomial of
L by POLYNOM3:def 10;
let F2 be
Polynomial of
L;
( F2 = Sum ((F | ((len F) -' 1)) | (n + 1)) implies len F2 <= ((((n + 1) * (len q)) - (len q)) - (n + 1)) + 2 )
assume A22:
F2 = Sum ((F | ((len F) -' 1)) | (n + 1))
;
len F2 <= ((((n + 1) * (len q)) - (len q)) - (n + 1)) + 2
len F3 <= (((n * (len q)) - (len q)) - n) + 2
by A20;
then A23:
len F3 <= ((n * (len q)) - n) + 1
by A21, XXREAL_0:2;
now len F2 <= ((((n + 1) * (len q)) - (len q)) - (n + 1)) + 2per cases
( n + 1 <= len (F | ((len F) -' 1)) or n + 1 > len (F | ((len F) -' 1)) )
;
suppose A24:
n + 1
<= len (F | ((len F) -' 1))
;
len F2 <= ((((n + 1) * (len q)) - (len q)) - (n + 1)) + 2reconsider nn =
n as
Element of
NAT by ORDINAL1:def 12;
A25:
n + 1
>= 1
by NAT_1:11;
reconsider maxFq =
max (
(len F3),
(len ((p . nn) * (q `^ nn)))) as
Element of
NAT by ORDINAL1:def 12;
A26:
(
maxFq >= len F3 &
maxFq >= len ((p . nn) * (q `^ nn)) )
by XXREAL_0:25;
len ((p . nn) * (q `^ nn)) <= ((n * (len q)) - n) + 1
then A29:
maxFq <= ((n * (len q)) - n) + 1
by A23, XXREAL_0:28;
len (F | ((len F) -' 1)) <= len F
by A14, NAT_1:11;
then
n + 1
<= len F
by A24, XXREAL_0:2;
then A30:
n + 1
in dom F
by A25, FINSEQ_3:25;
A31:
n + 1
in dom (F | ((len F) -' 1))
by A24, A25, FINSEQ_3:25;
then A32:
(F | ((len F) -' 1)) /. (n + 1) =
(F | ((len F) -' 1)) . (n + 1)
by PARTFUN1:def 6
.=
F . (n + 1)
by A12, A31, FINSEQ_1:def 7
.=
(p . ((n + 1) -' 1)) * (q `^ ((n + 1) -' 1))
by A5, A30
.=
(p . nn) * (q `^ ((n + 1) -' 1))
by NAT_D:34
.=
(p . nn) * (q `^ nn)
by NAT_D:34
;
(F | ((len F) -' 1)) | (nn + 1) = ((F | ((len F) -' 1)) | nn) ^ <*((F | ((len F) -' 1)) /. (nn + 1))*>
by A24, FINSEQ_5:82;
then F2 =
(Sum ((F | ((len F) -' 1)) | n)) + ((F | ((len F) -' 1)) /. (n + 1))
by A22, FVSUM_1:71
.=
F3 + ((p . nn) * (q `^ nn))
by A32, POLYNOM3:def 10
;
then
len F2 <= maxFq
by A26, POLYNOM4:6;
hence
len F2 <= ((((n + 1) * (len q)) - (len q)) - (n + 1)) + 2
by A29, XXREAL_0:2;
verum end; end; end;
hence
len F2 <= ((((n + 1) * (len q)) - (len q)) - (n + 1)) + 2
;
verum
end;
0 + (len q) >= 1
+ 1
by A2, NAT_1:13;
then
2
- (len q) <= 0
by XREAL_1:20;
then A36:
(2 - (len q)) + k <= 0 + k
by XREAL_1:6;
0 + 1
<= len (F | ((len F) -' 1))
by A17, NAT_1:13;
then A37:
1
in dom (F | ((len F) -' 1))
by FINSEQ_3:25;
A38:
S1[1]
for
n being non
zero Nat holds
S1[
n]
from NAT_1:sch 10(A38, A19);
then
len sF1 <= ((((len (F | ((len F) -' 1))) * (len q)) - (len q)) - (len (F | ((len F) -' 1)))) + 2
by A17, A18;
then A40:
sF1 . k = 0. L
by A4, A14, A36, ALGSEQ_1:8, XXREAL_0:2;
A41:
len F in dom F
by A6, FINSEQ_3:25;
then F /. (len F) =
F . (len F)
by PARTFUN1:def 6
.=
(p . ((len F) -' 1)) * (q `^ ((len F) -' 1))
by A5, A41
;
then
Subst (
p,
q)
= sF1 + ((p . ((len F) -' 1)) * (q `^ ((len F) -' 1)))
by A3, A13, POLYNOM3:def 10;
then A42:
(Subst (p,q)) . k =
(sF1 . k) + (((p . ((len F) -' 1)) * (q `^ ((len F) -' 1))) . k)
by NORMSP_1:def 2
.=
((p . ((len F) -' 1)) * (q `^ ((len F) -' 1))) . k
by A40, RLVECT_1:def 4
.=
(p . ((len F) -' 1)) * ((q `^ ((len F) -' 1)) . k)
by Def4
;
len (q `^ ((len F) -' 1)) = k + 1
by A9;
then A43:
(q `^ ((len F) -' 1)) . k <> 0. L
by ALGSEQ_1:10;
p . ((len F) -' 1) <> 0. L
by A4, A11, ALGSEQ_1:10;
hence
contradiction
by A16, A42, A43, VECTSP_1:12;
verum end; suppose A44:
len (F | ((len F) -' 1)) = {}
;
contradictionA45:
F /. 1 =
F . 1
by A7, PARTFUN1:def 6
.=
(p . (1 -' 1)) * (q `^ (1 -' 1))
by A5, A7
.=
(p . 0) * (q `^ (1 -' 1))
by XREAL_1:232
.=
(p . 0) * (q `^ 0)
by XREAL_1:232
.=
(p . 0) * (1_. L)
by Th15
.=
<%(p . 0)%>
by Th29
;
A46:
0. (Polynom-Ring L) = 0_. L
by POLYNOM3:def 10;
A47:
len F = 0 + 1
by A12, A44, FINSEQ_2:16;
then A48:
p . 0 <> 0. L
by A4, ALGSEQ_1:10;
F | ((len F) -' 1) = <*> the
carrier of
(Polynom-Ring L)
by A44;
then Sum F =
(0. (Polynom-Ring L)) + (F /. 1)
by A13, A47, RLVECT_1:43
.=
(0_. L) + <%(p . 0)%>
by A45, A46, POLYNOM3:def 10
.=
<%(p . 0)%>
by POLYNOM3:28
;
hence
contradiction
by A3, A4, A15, A47, A48, Th33;
verum end; end; end;
hence
contradiction
;
verum
end;
defpred S1[ Nat] means for F1 being Polynomial of L st F1 = Sum (F | $1) holds
len F1 <= len (q `^ ($1 -' 1));
A49:
for n being non zero Nat st S1[n] holds
S1[n + 1]
proof
let n be non
zero Nat;
( S1[n] implies S1[n + 1] )
assume A50:
for
F1 being
Polynomial of
L st
F1 = Sum (F | n) holds
len F1 <= len (q `^ (n -' 1))
;
S1[n + 1]
reconsider nn =
n as
Element of
NAT by ORDINAL1:def 12;
reconsider F2 =
Sum (F | n) as
Polynomial of
L by POLYNOM3:def 10;
let F1 be
Polynomial of
L;
( F1 = Sum (F | (n + 1)) implies len F1 <= len (q `^ ((n + 1) -' 1)) )
assume A51:
F1 = Sum (F | (n + 1))
;
len F1 <= len (q `^ ((n + 1) -' 1))
(n * (len q)) + ((len q) -' 1) >= n * (len q)
by NAT_1:11;
then A52:
(n * (len q)) - ((len q) -' 1) <= n * (len q)
by XREAL_1:20;
len q >= 0 + 1
by A2;
then
(len q) - 1
>= 0
;
then
(n * (len q)) - ((len q) - 1) <= n * (len q)
by A52, XREAL_0:def 2;
then
(((n * (len q)) - (len q)) + 1) - n <= (n * (len q)) - n
by XREAL_1:9;
then A53:
((((n * (len q)) - (len q)) - n) + 1) + 1
<= ((n * (len q)) - n) + 1
by XREAL_1:6;
len (q `^ (n -' 1)) =
(((n -' 1) * (len q)) - (n -' 1)) + 1
by A2, Th23
.=
(((n - 1) * (len q)) - (n -' 1)) + 1
by XREAL_0:def 2
.=
(((n * (len q)) - (1 * (len q))) - (n - 1)) + 1
by XREAL_0:def 2
.=
((((n * (len q)) - (len q)) - n) + 1) + 1
;
then A54:
len (q `^ (n -' 1)) <= len (q `^ nn)
by A2, A53, Th23;
per cases
( n + 1 <= len F or n + 1 > len F )
;
suppose A55:
n + 1
<= len F
;
len F1 <= len (q `^ ((n + 1) -' 1))reconsider maxFq =
max (
(len F2),
(len ((p . nn) * (q `^ nn)))) as
Element of
NAT by ORDINAL1:def 12;
(
p . n <> 0. L or
p . n = 0. L )
;
then A56:
len ((p . nn) * (q `^ nn)) <= len (q `^ nn)
by Th24, Th25;
len F2 <= len (q `^ (n -' 1))
by A50;
then
len F2 <= len (q `^ nn)
by A54, XXREAL_0:2;
then A57:
maxFq <= len (q `^ nn)
by A56, XXREAL_0:28;
F | (n + 1) = (F | n) ^ <*(F /. (nn + 1))*>
by A55, FINSEQ_5:82;
then A58:
F1 = (Sum (F | n)) + (F /. (n + 1))
by A51, FVSUM_1:71;
n + 1
>= 1
by NAT_1:11;
then A59:
n + 1
in dom F
by A55, FINSEQ_3:25;
then F /. (n + 1) =
F . (n + 1)
by PARTFUN1:def 6
.=
(p . ((n + 1) -' 1)) * (q `^ ((n + 1) -' 1))
by A5, A59
.=
(p . nn) * (q `^ ((n + 1) -' 1))
by NAT_D:34
.=
(p . nn) * (q `^ nn)
by NAT_D:34
;
then A60:
F1 = F2 + ((p . nn) * (q `^ nn))
by A58, POLYNOM3:def 10;
(
maxFq >= len F2 &
maxFq >= len ((p . nn) * (q `^ nn)) )
by XXREAL_0:25;
then
len F1 <= maxFq
by A60, POLYNOM4:6;
then
len F1 <= len (q `^ nn)
by A57, XXREAL_0:2;
hence
len F1 <= len (q `^ ((n + 1) -' 1))
by NAT_D:34;
verum end; end;
end;
A63:
F | (len F) = F
by FINSEQ_1:58;
A64:
S1[1]
for n being non zero Nat holds S1[n]
from NAT_1:sch 10(A64, A49);
then
len (Subst (p,q)) <= len (q `^ ((len F) -' 1))
by A1, A3, A4, A63;
hence
len (Subst (p,q)) = ((((len p) * (len q)) - (len p)) - (len q)) + 2
by A9, A10, XXREAL_0:1; verum