let L be non trivial right_complementable well-unital distributive Abelian add-associative right_zeroed associative commutative domRing-like doubleLoopStr ; for z being rational_function of L ex z1 being rational_function of L ex z2 being non zero Polynomial of L st
( z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st
( z2 = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) )
let z be rational_function of L; ex z1 being rational_function of L ex z2 being non zero Polynomial of L st
( z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st
( z2 = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) )
defpred S1[ Nat] means for z being rational_function of L st max ((deg (z `1)),(deg (z `2))) = $1 holds
ex z1 being rational_function of L ex z2 being non zero Polynomial of L st
( z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st
( z2 = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) );
now for z being rational_function of L st max ((deg (z `1)),(deg (z `2))) = 0 holds
ex z1 being rational_function of L ex z2 being non zero Polynomial of L st
( z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st
( z2 = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) )let z be
rational_function of
L;
( max ((deg (z `1)),(deg (z `2))) = 0 implies ex z1 being rational_function of L ex z2 being non zero Polynomial of L st
( z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st
( z2 = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) ) )assume
max (
(deg (z `1)),
(deg (z `2)))
= 0
;
ex z1 being rational_function of L ex z2 being non zero Polynomial of L st
( z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st
( z2 = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) )then
deg (z `2) <= 0
by XXREAL_0:25;
then A1:
deg (z `2) = 0
;
hence
ex
z1 being
rational_function of
L ex
z2 being non
zero Polynomial of
L st
(
z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] &
z1 is
irreducible & ex
f being
FinSequence of
(Polynom-Ring L) st
(
z2 = Product f & ( for
i being
Element of
NAT st
i in dom f holds
ex
x being
Element of
L st
(
x is_a_common_root_of z `1 ,
z `2 &
f . i = rpoly (1,
x) ) ) ) )
by Lm1;
verum end;
then A5:
S1[ 0 ]
;
A6:
now for n being Nat st S1[n] holds
S1[n + 1]let n be
Nat;
( S1[n] implies S1[n + 1] )assume A7:
S1[
n]
;
S1[n + 1]
for
z being
rational_function of
L st
max (
(deg (z `1)),
(deg (z `2)))
= n + 1 holds
ex
z1 being
rational_function of
L ex
z2 being non
zero Polynomial of
L st
(
z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] &
z1 is
irreducible & ex
f being
FinSequence of
(Polynom-Ring L) st
(
z2 = Product f & ( for
i being
Element of
NAT st
i in dom f holds
ex
x being
Element of
L st
(
x is_a_common_root_of z `1 ,
z `2 &
f . i = rpoly (1,
x) ) ) ) )
proof
let z be
rational_function of
L;
( max ((deg (z `1)),(deg (z `2))) = n + 1 implies ex z1 being rational_function of L ex z2 being non zero Polynomial of L st
( z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st
( z2 = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) ) )
assume A8:
max (
(deg (z `1)),
(deg (z `2)))
= n + 1
;
ex z1 being rational_function of L ex z2 being non zero Polynomial of L st
( z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st
( z2 = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) )
per cases
( z is irreducible or z is reducible )
;
suppose
z is
reducible
;
ex z1 being rational_function of L ex z2 being non zero Polynomial of L st
( z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st
( z2 = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) )then
z `1 ,
z `2 have_common_roots
;
then consider x being
Element of
L such that A9:
x is_a_common_root_of z `1 ,
z `2
;
A10:
(
x is_a_root_of z `1 &
x is_a_root_of z `2 )
by A9;
consider q2 being
Polynomial of
L such that A11:
z `2 = (rpoly (1,x)) *' q2
by A10, HURWITZ:33;
consider q1 being
Polynomial of
L such that A12:
z `1 = (rpoly (1,x)) *' q1
by A10, HURWITZ:33;
q2 <> 0_. L
by A11, POLYNOM3:34;
then reconsider q2 =
q2 as non
zero Polynomial of
L by UPROOTS:def 5;
set q =
[q1,q2];
max (
(deg ([q1,q2] `1)),
(deg ([q1,q2] `2)))
= n
proof
A13:
deg (z `2) =
(deg (rpoly (1,x))) + (deg q2)
by A11, HURWITZ:23
.=
1
+ (deg q2)
by HURWITZ:27
;
per cases
( max ((deg (z `1)),(deg (z `2))) = deg (z `1) or max ((deg (z `1)),(deg (z `2))) = deg (z `2) )
by XXREAL_0:16;
suppose A14:
max (
(deg (z `1)),
(deg (z `2)))
= deg (z `1)
;
max ((deg ([q1,q2] `1)),(deg ([q1,q2] `2))) = nthen
z `1 <> 0_. L
by A8, HURWITZ:20;
then
q1 <> 0_. L
by A12, POLYNOM3:34;
then A15:
deg (z `1) =
(deg (rpoly (1,x))) + (deg q1)
by A12, HURWITZ:23
.=
1
+ (deg q1)
by HURWITZ:27
;
A16:
deg (z `2) <= n + 1
by A8, XXREAL_0:25;
((deg q2) + 1) - 1
<= (n + 1) - 1
by A13, A16, XREAL_1:9;
hence
max (
(deg ([q1,q2] `1)),
(deg ([q1,q2] `2)))
= n
by A15, A14, A8, XXREAL_0:def 10;
verum end; end;
end; then consider z1q being
rational_function of
L,
z2q being non
zero Polynomial of
L such that A19:
(
[q1,q2] = [(z2q *' (z1q `1)),(z2q *' (z1q `2))] &
z1q is
irreducible & ex
f being
FinSequence of
(Polynom-Ring L) st
(
z2q = Product f & ( for
i being
Element of
NAT st
i in dom f holds
ex
x being
Element of
L st
(
x is_a_common_root_of [q1,q2] `1 ,
[q1,q2] `2 &
f . i = rpoly (1,
x) ) ) ) )
by A7;
take z1 =
z1q;
ex z2 being non zero Polynomial of L st
( z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st
( z2 = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) )set z2 =
(rpoly (1,x)) *' z2q;
reconsider z2 =
(rpoly (1,x)) *' z2q as non
zero Polynomial of
L ;
take
z2
;
( z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st
( z2 = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) )consider fq being
FinSequence of
(Polynom-Ring L) such that A20:
(
z2q = Product fq & ( for
i being
Element of
NAT st
i in dom fq holds
ex
x being
Element of
L st
(
x is_a_common_root_of [q1,q2] `1 ,
[q1,q2] `2 &
fq . i = rpoly (1,
x) ) ) )
by A19;
reconsider rp =
rpoly (1,
x) as
Element of
(Polynom-Ring L) by POLYNOM3:def 10;
set f =
<*rp*> ^ fq;
A21:
Product (<*rp*> ^ fq) =
rp * (Product fq)
by GROUP_4:7
.=
z2
by A20, POLYNOM3:def 10
;
A22:
z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))]
A27:
now for i being Element of NAT st i in dom (<*rp*> ^ fq) holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & (<*rp*> ^ fq) . i = rpoly (1,x) )let i be
Element of
NAT ;
( i in dom (<*rp*> ^ fq) implies ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & (<*rp*> ^ fq) . i = rpoly (1,x) ) )assume A28:
i in dom (<*rp*> ^ fq)
;
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & (<*rp*> ^ fq) . i = rpoly (1,x) )now ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & (<*rp*> ^ fq) . i = rpoly (1,x) )per cases
( i in dom <*rp*> or ex n being Nat st
( n in dom fq & i = (len <*rp*>) + n ) )
by A28, FINSEQ_1:25;
suppose
ex
n being
Nat st
(
n in dom fq &
i = (len <*rp*>) + n )
;
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & (<*rp*> ^ fq) . i = rpoly (1,x) )then consider n being
Nat such that A31:
(
n in dom fq &
i = (len <*rp*>) + n )
;
(<*rp*> ^ fq) . i = fq . n
by A31, FINSEQ_1:def 7;
then consider y being
Element of
L such that A32:
(
y is_a_common_root_of [q1,q2] `1 ,
[q1,q2] `2 &
(<*rp*> ^ fq) . i = rpoly (1,
y) )
by A31, A20;
A33:
(
y is_a_root_of [q1,q2] `1 &
y is_a_root_of [q1,q2] `2 )
by A32;
then A34:
0. L = eval (
q1,
y)
by POLYNOM5:def 7;
A35:
eval (
(z `1),
y) =
(eval ((rpoly (1,x)),y)) * (eval (q1,y))
by A12, POLYNOM4:24
.=
0. L
by A34
;
A36:
0. L = eval (
q2,
y)
by A33, POLYNOM5:def 7;
eval (
(z `2),
y) =
(eval ((rpoly (1,x)),y)) * (eval (q2,y))
by A11, POLYNOM4:24
.=
0. L
by A36
;
then
(
y is_a_root_of z `1 &
y is_a_root_of z `2 )
by A35, POLYNOM5:def 7;
then
y is_a_common_root_of z `1 ,
z `2
;
hence
ex
x being
Element of
L st
(
x is_a_common_root_of z `1 ,
z `2 &
(<*rp*> ^ fq) . i = rpoly (1,
x) )
by A32;
verum end; end; end; hence
ex
x being
Element of
L st
(
x is_a_common_root_of z `1 ,
z `2 &
(<*rp*> ^ fq) . i = rpoly (1,
x) )
;
verum end; thus
(
z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] &
z1 is
irreducible & ex
f being
FinSequence of
(Polynom-Ring L) st
(
z2 = Product f & ( for
i being
Element of
NAT st
i in dom f holds
ex
x being
Element of
L st
(
x is_a_common_root_of z `1 ,
z `2 &
f . i = rpoly (1,
x) ) ) ) )
by A19, A21, A22, A27;
verum end; end;
end; hence
S1[
n + 1]
;
verum end;
A37:
for n being Nat holds S1[n]
from NAT_1:sch 2(A5, A6);
max ((deg (z `1)),(deg (z `2))) >= deg (z `2)
by XXREAL_0:25;
then
max ((deg (z `1)),(deg (z `2))) >= 0
;
then
max ((deg (z `1)),(deg (z `2))) in NAT
by INT_1:3;
hence
ex z1 being rational_function of L ex z2 being non zero Polynomial of L st
( z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st
( z2 = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) )
by A37; verum