environ
vocabularies HIDDEN, NUMBERS, FINSEQ_1, SUBSET_1, RELAT_1, FUNCT_1, CARD_1, CARD_3, FINSEQ_2, ARYTM_3, ORDINAL4, TARSKI, NAT_1, XXREAL_0, REAL_1, ARYTM_1, XBOOLE_0, RLVECT_1, ALGSTR_0, SUPINF_2, PARTFUN1, FINSET_1, FUNCT_2, ZFMISC_1, PRE_POLY, FUNCT_4, FUNCOP_1, VALUED_0, PBOOLE, SGRAPH1, FINSOP_1, BINOP_1, GROUP_1, STRUCT_0, POLYNOM1, POLYNOM3, AFINSQ_1, MESFUNC1, ALGSEQ_1, VECTSP_1, POLYNOM5, LATTICES, VECTSP_2, COMPLFLD, POLYNOM2, FVSUM_1, MEMBERED, CLASSES1, UPROOTS, FUNCT_7;
notations HIDDEN, TARSKI, XBOOLE_0, XTUPLE_0, XCMPLX_0, XXREAL_0, SUBSET_1, ORDINAL1, CARD_1, NUMBERS, XREAL_0, ZFMISC_1, REAL_1, VECTSP_2, BINOP_1, RELAT_1, FUNCT_1, PBOOLE, RELSET_1, PARTFUN1, FINSEQ_1, FINSEQ_2, DOMAIN_1, FUNCT_2, XXREAL_2, VALUED_0, NAT_1, NAT_D, STRUCT_0, ALGSTR_0, RLVECT_1, VFUNCT_1, VECTSP_1, FINSOP_1, NORMSP_1, GROUP_4, RVSUM_1, ALGSEQ_1, COMPLFLD, POLYNOM3, POLYNOM4, POLYNOM5, FINSET_1, MCART_1, FUNCT_4, FUNCOP_1, CLASSES1, FVSUM_1, WSIERP_1, MEMBERED, GROUP_1, RECDEF_1, PRE_POLY;
definitions TARSKI, VECTSP_2, FUNCT_1, POLYNOM5;
theorems GROUP_1, CARD_1, FINSEQ_1, NAT_1, FUNCT_1, FUNCT_2, RELAT_1, TARSKI, XBOOLE_0, XBOOLE_1, VECTSP_1, POLYNOM5, INT_1, AXIOMS, RVSUM_1, FVSUM_1, FINSEQ_3, FINSEQ_2, POLYNOM4, POLYNOM3, FUNCT_7, ALGSEQ_1, RLVECT_1, PBOOLE, FUNCOP_1, MATRIX_3, VECTSP_2, CARD_2, FINSEQ_5, GRAPH_5, RFINSEQ, WELLORD2, CARD_3, ORDINAL1, FINSOP_1, MONOID_0, INTEGRA1, FUNCT_4, XREAL_1, GROUP_4, XXREAL_0, PARTFUN1, XXREAL_2, NAT_D, FINSEQ_4, CLASSES1, PRE_POLY, TREES_9, XREAL_0, NUMBERS;
schemes NAT_1, FUNCT_1, FUNCT_2, FRAENKEL, ALGSEQ_1, FINSEQ_1, CLASSES1, INT_1;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, FINSET_1, NUMBERS, XXREAL_0, XREAL_0, NAT_1, INT_1, BINOP_2, CARD_1, MEMBERED, FINSEQ_1, STRUCT_0, VECTSP_1, COMPLFLD, ALGSTR_1, PRE_POLY, POLYNOM3, POLYNOM4, POLYNOM5, FINSEQ_2, VALUED_0, XXREAL_2, FUNCT_2, RELSET_1, GROUP_1, VFUNCT_1;
constructors HIDDEN, WELLORD2, SETWISEO, REAL_1, FINSEQOP, FINSOP_1, NAT_D, WSIERP_1, VECTSP_2, REALSET2, ALGSTR_1, GROUP_4, MATRIX_1, GOBOARD1, POLYNOM2, POLYNOM4, POLYNOM5, RECDEF_1, BINOP_2, CLASSES1, XXREAL_2, RELSET_1, FUNCT_7, FVSUM_1, VFUNCT_1, XTUPLE_0, ALGSEQ_1, BINOP_1, NUMBERS;
requirements HIDDEN, NUMERALS, BOOLE, SUBSET, ARITHM, REAL;
equalities POLYNOM3, POLYNOM5, FINSEQ_2, RVSUM_1, GROUP_4, RLVECT_1, FUNCOP_1, RELAT_1, STRUCT_0;
expansions FUNCT_1, POLYNOM5, RELAT_1;
reconsider jj = 1 as Element of REAL by XREAL_0:def 1;
scheme
IndFinSeq0{
F1()
-> Nat,
P1[
set ] } :
provided
A1:
P1[1]
and A2:
for
i being
Element of
NAT st 1
<= i &
i < F1() &
P1[
i] holds
P1[
i + 1]
Lm1:
now for L being domRing
for p being non-zero Polynomial of L holds
( Roots p is finite & ex n being Element of NAT st
( n = card (Roots p) & n < len p ) )
let L be
domRing;
for p being non-zero Polynomial of L holds
( Roots p is finite & ex n being Element of NAT st
( n = card (Roots p) & n < len p ) )let p be
non-zero Polynomial of
L;
( Roots p is finite & ex n being Element of NAT st
( n = card (Roots p) & n < len p ) )defpred S1[
Nat]
means for
p being
Polynomial of
L st
len p = $1 holds
(
Roots p is
finite & ex
n being
Element of
NAT st
(
n = card (Roots p) &
n < len p ) );
p <> 0_. L
by Def4;
then
len p <> 0
by POLYNOM4:5;
then A1:
len p >= 0 + 1
by NAT_1:13;
A2:
for
n being
Nat st
n >= 1 &
S1[
n] holds
S1[
n + 1]
proof
let n be
Nat;
( n >= 1 & S1[n] implies S1[n + 1] )
assume that
n >= 1
and A3:
S1[
n]
;
S1[n + 1]
let p be
Polynomial of
L;
( len p = n + 1 implies ( Roots p is finite & ex n being Element of NAT st
( n = card (Roots p) & n < len p ) ) )
assume A4:
len p = n + 1
;
( Roots p is finite & ex n being Element of NAT st
( n = card (Roots p) & n < len p ) )
per cases
( p is with_roots or not p is with_roots )
;
suppose
p is
with_roots
;
( Roots p is finite & ex n being Element of NAT st
( n = card (Roots p) & n < len p ) )
then consider x being
Element of
L such that A5:
x is_a_root_of p
;
set r =
<%(- x),(1. L)%>;
set pq =
poly_quotient (
p,
x);
A6:
p = <%(- x),(1. L)%> *' (poly_quotient (p,x))
by A5, Th47;
then A7:
Roots p = (Roots <%(- x),(1. L)%>) \/ (Roots (poly_quotient (p,x)))
by Th20;
A8:
Roots <%(- x),(1. L)%> = {x}
by Th45;
then reconsider Rr =
Roots <%(- x),(1. L)%> as
finite set ;
A9:
(len (poly_quotient (p,x))) + 1
= len p
by A4, A5, Def6;
then consider k being
Element of
NAT such that A10:
k = card (Roots (poly_quotient (p,x)))
and A11:
k < len (poly_quotient (p,x))
by A3, A4;
reconsider Rpq =
Roots (poly_quotient (p,x)) as
finite set by A3, A4, A9;
reconsider Rp =
Rpq \/ Rr as
finite set ;
card Rr = 1
by A8, CARD_1:30;
then A12:
card Rp <= k + 1
by A10, CARD_2:43;
Roots (poly_quotient (p,x)) is
finite
by A3, A4, A9;
hence
Roots p is
finite
by A8, A7;
ex n being Element of NAT st
( n = card (Roots p) & n < len p )take m =
card Rp;
( m = card (Roots p) & m < len p )thus
m = card (Roots p)
by A6, Th20;
m < len p
k + 1
< n + 1
by A4, A9, A11, XREAL_1:8;
hence
m < len p
by A4, A12, XXREAL_0:2;
verum
end;
end;
end;
A16:
S1[1]
for
n being
Nat st
n >= 1 holds
S1[
n]
from NAT_1:sch 8(A16, A2);
hence
(
Roots p is
finite & ex
n being
Element of
NAT st
(
n = card (Roots p) &
n < len p ) )
by A1;
verum
end;