let n be Nat; for R being domRing
for p being non zero Polynomial of R
for a being Element of R
for b being non zero Element of R holds
( (rpoly (1,a)) `^ n divides p iff (rpoly (1,a)) `^ n divides b * p )
let R be domRing; for p being non zero Polynomial of R
for a being Element of R
for b being non zero Element of R holds
( (rpoly (1,a)) `^ n divides p iff (rpoly (1,a)) `^ n divides b * p )
let p be non zero Polynomial of R; for a being Element of R
for b being non zero Element of R holds
( (rpoly (1,a)) `^ n divides p iff (rpoly (1,a)) `^ n divides b * p )
let a be Element of R; for b being non zero Element of R holds
( (rpoly (1,a)) `^ n divides p iff (rpoly (1,a)) `^ n divides b * p )
let b be non zero Element of R; ( (rpoly (1,a)) `^ n divides p iff (rpoly (1,a)) `^ n divides b * p )
defpred S1[ Nat] means ( (rpoly (1,a)) `^ $1 divides b * p implies (rpoly (1,a)) `^ $1 divides p );
then IA:
S1[ 0 ]
;
IS:
now for k being Nat st S1[k] holds
S1[k + 1]let k be
Nat;
( S1[k] implies S1[k + 1] )assume AS:
S1[
k]
;
S1[k + 1]now ( (rpoly (1,a)) `^ (k + 1) divides b * p implies (rpoly (1,a)) `^ (k + 1) divides p )assume
(rpoly (1,a)) `^ (k + 1) divides b * p
;
(rpoly (1,a)) `^ (k + 1) divides pthen consider r being
Polynomial of
R such that A1:
((rpoly (1,a)) `^ (k + 1)) *' r = b * p
by RING_4:1;
C:
((rpoly (1,a)) `^ k) *' ((rpoly (1,a)) *' r) =
(((rpoly (1,a)) `^ k) *' (rpoly (1,a))) *' r
by POLYNOM3:33
.=
b * p
by A1, POLYNOM5:19
;
then consider r1 being
Polynomial of
R such that A2:
((rpoly (1,a)) `^ k) *' r1 = p
by AS, RING_4:1;
reconsider r1 =
r1 as non
zero Polynomial of
R by A2;
(b * r1) *' ((rpoly (1,a)) `^ k) = ((rpoly (1,a)) *' r) *' ((rpoly (1,a)) `^ k)
by C, A2, RATFUNC1:5;
then
b * r1 = (rpoly (1,a)) *' r
by RATFUNC1:7;
then
rpoly (1,
a)
divides r1
by divi1b, RING_4:1;
then consider r2 being
Polynomial of
R such that A3:
(rpoly (1,a)) *' r2 = r1
by RING_4:1;
p =
(((rpoly (1,a)) `^ k) *' (rpoly (1,a))) *' r2
by A2, A3, POLYNOM3:33
.=
((rpoly (1,a)) `^ (k + 1)) *' r2
by POLYNOM5:19
;
hence
(rpoly (1,a)) `^ (k + 1) divides p
by RING_4:1;
verum end; hence
S1[
k + 1]
;
verum end;
for k being Nat holds S1[k]
from NAT_1:sch 2(IA, IS);
hence
( (rpoly (1,a)) `^ n divides p iff (rpoly (1,a)) `^ n divides b * p )
by divi1; verum