let L be non trivial right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative domRing-like doubleLoopStr ; for z being rational_function of L holds degree z <= max ((degree (z `1)),(degree (z `2)))
let z be rational_function of L; degree z <= max ((degree (z `1)),(degree (z `2)))
per cases
( z is zero or not z is zero )
;
suppose A5:
not
z is
zero
;
degree z <= max ((degree (z `1)),(degree (z `2)))defpred S1[
Nat]
means for
z being non
zero rational_function of
L st
max (
(degree (z `1)),
(degree (z `2)))
= $1 holds
max (
(degree ((NF z) `1)),
(degree ((NF z) `2)))
<= max (
(degree (z `1)),
(degree (z `2)));
now for z being non zero rational_function of L
for z1 being rational_function of L
for z2 being non zero Polynomial of L
for f being FinSequence of (Polynom-Ring L) st max ((degree (z `1)),(degree (z `2))) = 0 holds
max ((degree ((NF z) `1)),(degree ((NF z) `2))) <= max ((degree (z `1)),(degree (z `2)))let z be non
zero rational_function of
L;
for z1 being rational_function of L
for z2 being non zero Polynomial of L
for f being FinSequence of (Polynom-Ring L) st max ((degree (z `1)),(degree (z `2))) = 0 holds
max ((degree ((NF z) `1)),(degree ((NF z) `2))) <= max ((degree (z `1)),(degree (z `2)))let z1 be
rational_function of
L;
for z2 being non zero Polynomial of L
for f being FinSequence of (Polynom-Ring L) st max ((degree (z `1)),(degree (z `2))) = 0 holds
max ((degree ((NF z) `1)),(degree ((NF z) `2))) <= max ((degree (z `1)),(degree (z `2)))let z2 be non
zero Polynomial of
L;
for f being FinSequence of (Polynom-Ring L) st max ((degree (z `1)),(degree (z `2))) = 0 holds
max ((degree ((NF z) `1)),(degree ((NF z) `2))) <= max ((degree (z `1)),(degree (z `2)))let f be
FinSequence of
(Polynom-Ring L);
( max ((degree (z `1)),(degree (z `2))) = 0 implies max ((degree ((NF z) `1)),(degree ((NF z) `2))) <= max ((degree (z `1)),(degree (z `2))) )assume A6:
max (
(degree (z `1)),
(degree (z `2)))
= 0
;
max ((degree ((NF z) `1)),(degree ((NF z) `2))) <= max ((degree (z `1)),(degree (z `2)))then
z is
irreducible
;
then
degree z = max (
(degree (z `1)),
(degree (z `2)))
by Lm6;
hence
max (
(degree ((NF z) `1)),
(degree ((NF z) `2)))
<= max (
(degree (z `1)),
(degree (z `2)))
;
verum end; then A11:
S1[
0 ]
;
A12:
now for n being Nat st S1[n] holds
S1[n + 1]let n be
Nat;
( S1[n] implies S1[n + 1] )assume A13:
S1[
n]
;
S1[n + 1]now for z being non zero rational_function of L st max ((degree (z `1)),(degree (z `2))) = n + 1 holds
max ((degree ((NF z) `1)),(degree ((NF z) `2))) <= max ((degree (z `1)),(degree (z `2)))let z be non
zero rational_function of
L;
( max ((degree (z `1)),(degree (z `2))) = n + 1 implies max ((degree ((NF b1) `1)),(degree ((NF b1) `2))) <= max ((degree (b1 `1)),(degree (b1 `2))) )assume A14:
max (
(degree (z `1)),
(degree (z `2)))
= n + 1
;
max ((degree ((NF b1) `1)),(degree ((NF b1) `2))) <= max ((degree (b1 `1)),(degree (b1 `2)))per cases
( z is irreducible or z is reducible )
;
suppose
z is
reducible
;
max ((degree ((NF b1) `1)),(degree ((NF b1) `2))) <= max ((degree (b1 `1)),(degree (b1 `2)))then
z `1 ,
z `2 have_common_roots
;
then consider x being
Element of
L such that A15:
x is_a_common_root_of z `1 ,
z `2
;
A16:
(
x is_a_root_of z `1 &
x is_a_root_of z `2 )
by A15;
consider q2 being
Polynomial of
L such that A17:
z `2 = (rpoly (1,x)) *' q2
by A16, HURWITZ:33;
consider q1 being
Polynomial of
L such that A18:
z `1 = (rpoly (1,x)) *' q1
by A16, HURWITZ:33;
q1 <> 0_. L
by Def9, A18, POLYNOM3:34;
then reconsider q1 =
q1 as non
zero Polynomial of
L by UPROOTS:def 5;
q2 <> 0_. L
by A17, POLYNOM3:34;
then reconsider q2 =
q2 as non
zero Polynomial of
L by UPROOTS:def 5;
set q =
[q1,q2];
not
[q1,q2] is
zero
;
then reconsider q =
[q1,q2] as non
zero rational_function of
L ;
z =
[((rpoly (1,x)) *' q1),((rpoly (1,x)) *' q2)]
by Th19, A18, A17
.=
[((rpoly (1,x)) *' (q `1)),((rpoly (1,x)) *' q2)]
.=
[((rpoly (1,x)) *' (q `1)),((rpoly (1,x)) *' (q `2))]
;
then A19:
NF z = NF q
by Th26;
A20:
n <= n + 1
by NAT_1:11;
A21:
deg (z `1) =
(deg (rpoly (1,x))) + (deg q1)
by A18, HURWITZ:23
.=
1
+ (deg q1)
by HURWITZ:27
.=
1
+ (deg (q `1))
;
deg (z `2) =
(deg (rpoly (1,x))) + (deg q2)
by A17, HURWITZ:23
.=
1
+ (deg q2)
by HURWITZ:27
.=
1
+ (deg (q `2))
;
then A22:
max (
(degree (z `1)),
(degree (z `2)))
= 1
+ (max ((degree (q `1)),(degree (q `2))))
by A21, Th4;
then
max (
(degree ((NF z) `1)),
(degree ((NF z) `2)))
<= max (
(degree (q `1)),
(degree (q `2)))
by A13, A19, A14;
hence
max (
(degree ((NF z) `1)),
(degree ((NF z) `2)))
<= max (
(degree (z `1)),
(degree (z `2)))
by A20, A22, A14, XXREAL_0:2;
verum end; end; end; hence
S1[
n + 1]
;
verum end; A23:
for
n being
Nat holds
S1[
n]
from NAT_1:sch 2(A11, A12);
max (
(degree (z `1)),
(degree (z `2)))
>= 0
by XXREAL_0:25;
then
max (
(degree (z `1)),
(degree (z `2)))
in NAT
by INT_1:3;
hence
degree z <= max (
(degree (z `1)),
(degree (z `2)))
by A5, A23;
verum end; end;