set M = { (p - (u *' s)) where u is Polynomial of L : 1 = 1 } ;
defpred S1[ Nat] means ex t being Polynomial of L st
( t in { (p - (u *' s)) where u is Polynomial of L : 1 = 1 } & len t = $1 );
p =
p + (0_. L)
by POLYNOM3:29
.=
p + (- (0_. L))
by Th9
.=
p - ((0_. L) *' s)
by POLYNOM4:5
;
then
p in { (p - (u *' s)) where u is Polynomial of L : 1 = 1 }
;
then
ex t being Polynomial of L st
( t in { (p - (u *' s)) where u is Polynomial of L : 1 = 1 } & len t = len p )
;
then A2:
ex k being Nat st S1[k]
;
consider k being Nat such that
A3:
( S1[k] & ( for n being Nat st S1[n] holds
k <= n ) )
from NAT_1:sch 5(A2);
consider f being Polynomial of L such that
A4:
( f in { (p - (u *' s)) where u is Polynomial of L : 1 = 1 } & len f = k )
by A3;
consider g being Polynomial of L such that
A5:
( f = p - (g *' s) & 1 = 1 )
by A4;
take
g
; :: thesis: ex t being Polynomial of L st
( p = (g *' s) + t & deg t < deg s )
A6: (g *' s) + (p - (g *' s)) =
((g *' s) + (- (g *' s))) + p
by POLYNOM3:26
.=
((g *' s) - (g *' s)) + p
.=
(0_. L) + p
by POLYNOM3:30
.=
p
by POLYNOM3:29
;
len s <> 0
by A1, POLYNOM4:8;
then A7:
len s > 0
;
then A8:
s . ((len s) - 1) <> 0. L
by Lm7;
(len s) + 1 > 0 + 1
by A7, XREAL_1:8;
then
len s >= 1
by NAT_1:13;
then A9:
(len s) - 1 >= 1 - 1
by XREAL_1:11;
then A10:
s . ((len s) -' 1) <> 0. L
by A8, XREAL_0:def 2;
per cases
( f = 0_. L or f <> 0_. L )
;
suppose
f <> 0_. L
;
:: thesis: ex t being Polynomial of L st
( p = (g *' s) + t & deg t < deg s )then
len f <> 0
by POLYNOM4:8;
then
len f > 0
;
then
(len f) + 1
> 0 + 1
by XREAL_1:8;
then
len f >= 1
by NAT_1:13;
then A12:
(len f) - 1
>= 1
- 1
by XREAL_1:11;
then reconsider k' =
(len f) - 1 as
Element of
NAT by INT_1:16;
dom f = NAT
by FUNCT_2:def 1;
then A13:
k' in dom f
;
A14:
k = k' + 1
by A4;
now assume
deg f >= deg s
;
:: thesis: contradictionthen reconsider degn =
(deg f) - (deg s) as
Element of
NAT by INT_1:18;
set al =
(f . ((len f) -' 1)) * ((s . ((len s) -' 1)) " );
set g1 =
(0_. L) +* ({degn} --> ((f . ((len f) -' 1)) * ((s . ((len s) -' 1)) " )));
A15:
dom ({degn} --> ((f . ((len f) -' 1)) * ((s . ((len s) -' 1)) " ))) = {degn}
by FUNCOP_1:19;
A16:
degn in {degn}
by TARSKI:def 1;
A17:
dom (0_. L) = NAT
by FUNCT_2:def 1;
then
{degn} c= NAT
by TARSKI:def 3;
then
(dom (0_. L)) \/ (dom ({degn} --> ((f . ((len f) -' 1)) * ((s . ((len s) -' 1)) " )))) = NAT
by A15, A17, XBOOLE_1:12;
then A18:
dom ((0_. L) +* ({degn} --> ((f . ((len f) -' 1)) * ((s . ((len s) -' 1)) " )))) = NAT
by FUNCT_4:def 1;
then reconsider g1 =
(0_. L) +* ({degn} --> ((f . ((len f) -' 1)) * ((s . ((len s) -' 1)) " ))) as
sequence of
L by A18, FUNCT_2:5;
A20:
degn in {degn}
by TARSKI:def 1;
then
degn in dom ({degn} --> ((f . ((len f) -' 1)) * ((s . ((len s) -' 1)) " )))
by FUNCOP_1:19;
then A21:
g1 . degn =
({degn} --> ((f . ((len f) -' 1)) * ((s . ((len s) -' 1)) " ))) . degn
by FUNCT_4:14
.=
(f . ((len f) -' 1)) * ((s . ((len s) -' 1)) " )
by A20, FUNCOP_1:13
;
A22:
for
j being
Nat st
j <> degn holds
g1 . j = 0. L
ex
l being
Nat st
for
i being
Nat st
i >= l holds
g1 . i = 0. L
then reconsider g1 =
g1 as
Polynomial of
L by ALGSEQ_1:def 2;
set s1 =
p - ((g + g1) *' s);
A25:
p - ((g + g1) *' s) in { (p - (u *' s)) where u is Polynomial of L : 1 = 1 }
;
now let i be
Nat;
:: thesis: ( i >= k' implies (p - ((g + g1) *' s)) . b1 = 0. L )A26:
i in NAT
by ORDINAL1:def 13;
assume A27:
i >= k'
;
:: thesis: (p - ((g + g1) *' s)) . b1 = 0. LA28:
(p - ((g + g1) *' s)) - f =
(p + (- ((g + g1) *' s))) + ((- p) + (- (- (g *' s))))
by A5, Th11
.=
((p + (- ((g + g1) *' s))) + (- p)) + (- (- (g *' s)))
by POLYNOM3:26
.=
((p - p) + (- ((g + g1) *' s))) + (- (- (g *' s)))
by POLYNOM3:26
.=
((0_. L) + (- ((g + g1) *' s))) + (- (- (g *' s)))
by POLYNOM3:30
.=
(- ((g + g1) *' s)) + (- (- (g *' s)))
by POLYNOM3:29
.=
((- (g + g1)) *' s) + (- (- (g *' s)))
by Th12
.=
(((- g) + (- g1)) *' s) + (- (- (g *' s)))
by Th11
.=
(((- g) + (- g1)) *' s) + (g *' s)
by Lm4
.=
(((- g) *' s) + ((- g1) *' s)) + (g *' s)
by POLYNOM3:33
.=
((- g1) *' s) + (((- g) *' s) + (g *' s))
by POLYNOM3:26
.=
((- g1) *' s) + ((g *' s) - (g *' s))
by Th12
.=
((- g1) *' s) + (0_. L)
by POLYNOM3:30
.=
(- g1) *' s
by POLYNOM3:29
.=
- (g1 *' s)
by Th12
;
A29:
p - ((g + g1) *' s) =
(p - ((g + g1) *' s)) + (0_. L)
by POLYNOM3:29
.=
(p - ((g + g1) *' s)) + (f - f)
by POLYNOM3:30
.=
((p - ((g + g1) *' s)) + (- f)) + f
by POLYNOM3:26
.=
f - (g1 *' s)
by A28
;
A30:
(
dom f = NAT &
dom (g1 *' s) = NAT )
by FUNCT_2:def 1;
A31:
(p - ((g + g1) *' s)) . i =
(f . i) + ((- (g1 *' s)) . i)
by A26, A29, NORMSP_1:def 5
.=
(f . i) + (- ((g1 *' s) . i))
by A26, BHSP_1:def 10
.=
(f /. i) + (- ((g1 *' s) . i))
by A26, A30, PARTFUN1:def 8
.=
(f /. i) + (- ((g1 *' s) /. i))
by A26, A30, PARTFUN1:def 8
;
consider sf being
FinSequence of
L such that A32:
(
len sf = i + 1 &
(g1 *' s) . i = Sum sf & ( for
m being
Element of
NAT st
m in dom sf holds
sf . m = (g1 . (m -' 1)) * (s . ((i + 1) -' m)) ) )
by A26, POLYNOM3:def 11;
A33:
dom sf = Seg (len sf)
by FINSEQ_1:def 3;
degn + 1
= k - (deg s)
by A4;
then A34:
degn + 1
<= k
by A9, XREAL_1:45;
A39:
i + 1
>= k
by A14, A27, XREAL_1:8;
then A40:
i + 1
>= degn + 1
by A34, XXREAL_0:2;
A41:
(i + 1) - (degn + 1) is
Element of
NAT
by A34, A39, INT_1:18, XXREAL_0:2;
A42:
i in NAT
by ORDINAL1:def 13;
1
<= degn + 1
by NAT_1:11;
then A43:
degn + 1
in dom sf
by A32, A33, A40;
then A44:
Sum sf =
sf /. (degn + 1)
by A37, POLYNOM2:5
.=
sf . (degn + 1)
by A43, PARTFUN1:def 8
.=
(g1 . ((degn + 1) -' 1)) * (s . ((i + 1) -' (degn + 1)))
by A32, A43
.=
((f . ((len f) -' 1)) * ((s . ((len s) -' 1)) " )) * (s . ((i + 1) -' (degn + 1)))
by A21, NAT_D:34
;
per cases
( i > k' or i = k' )
by A27, XXREAL_0:1;
suppose A45:
i > k'
;
:: thesis: (p - ((g + g1) *' s)) . b1 = 0. Lthen
i + 1
> k' + 1
by XREAL_1:8;
then
i >= len f
by NAT_1:13;
then
f . i = 0. L
by ALGSEQ_1:22;
then A46:
f /. i = 0. L
by A30, A42, PARTFUN1:def 8;
A47:
(i + 1) -' (degn + 1) = (i - k') + ((len s) - 1)
by A41, XREAL_0:def 2;
reconsider e =
i - k' as
Element of
NAT by A45, INT_1:18;
i - k' > k' - k'
by A45, XREAL_1:11;
then
e + 1
> 0 + 1
by XREAL_1:8;
then
e >= 1
by NAT_1:13;
then
(i - k') - 1
>= 1
- 1
by XREAL_1:11;
then
((i - k') - 1) + (len s) >= 0 + (len s)
by XREAL_1:8;
then
s . ((i + 1) -' (degn + 1)) = 0. L
by A47, ALGSEQ_1:22;
then
Sum sf = 0. L
by A44, VECTSP_1:36;
hence (p - ((g + g1) *' s)) . i =
(0. L) + (- (0. L))
by A30, A31, A32, A42, A46, PARTFUN1:def 8
.=
(0. L) + (0. L)
by RLVECT_1:25
.=
0. L
by RLVECT_1:def 7
;
:: thesis: verum end; suppose A48:
i = k'
;
:: thesis: (p - ((g + g1) *' s)) . b1 = 0. L(i + 1) -' (degn + 1) =
(i + 1) - (degn + 1)
by A41, XREAL_0:def 2
.=
(len s) -' 1
by A9, A48, XREAL_0:def 2
;
then Sum sf =
(f . ((len f) -' 1)) * (((s . ((len s) -' 1)) " ) * (s . ((len s) -' 1)))
by A44, GROUP_1:def 4
.=
(f . ((len f) -' 1)) * (1_ L)
by A10, VECTSP_1:def 22
.=
f . ((len f) -' 1)
by VECTSP_1:def 13
.=
f . ((len f) - 1)
by A12, XREAL_0:def 2
.=
f /. ((len f) - 1)
by A13, PARTFUN1:def 8
;
hence (p - ((g + g1) *' s)) . i =
(f /. ((len f) - 1)) + (- (f /. ((len f) - 1)))
by A30, A31, A32, A48, PARTFUN1:def 8
.=
0. L
by RLVECT_1:16
;
:: thesis: verum end; end; then
k' is_at_least_length_of p - ((g + g1) *' s)
by ALGSEQ_1:def 3;
then
len (p - ((g + g1) *' s)) <= k'
by ALGSEQ_1:def 4;
then
len (p - ((g + g1) *' s)) < k
by A14, NAT_1:13;
hence
contradiction
by A3, A25;
:: thesis: verum end; hence
ex
t being
Polynomial of
L st
(
p = (g *' s) + t &
deg t < deg s )
by A5, A6;
:: thesis: verum end;