let n be Nat; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( (rpoly (1,a)) `^ n divides p iff (rpoly (1,a)) `^ n divides b * p )

defpred S_{1}[ Nat] means ( (rpoly (1,a)) `^ $1 divides b * p implies (rpoly (1,a)) `^ $1 divides p );

_{1}[ 0 ]
;

_{1}[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; :: thesis: verum

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; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( (rpoly (1,a)) `^ n divides p iff (rpoly (1,a)) `^ n divides b * p )

defpred S

now :: thesis: ( (rpoly (1,a)) `^ 0 divides b * p implies (rpoly (1,a)) `^ 0 divides p )

then IA:
Sassume
(rpoly (1,a)) `^ 0 divides b * p
; :: thesis: (rpoly (1,a)) `^ 0 divides p

(rpoly (1,a)) `^ 0 = 1_. R by POLYNOM5:15;

then ((rpoly (1,a)) `^ 0) *' p = p ;

hence (rpoly (1,a)) `^ 0 divides p by RING_4:1; :: thesis: verum

end;(rpoly (1,a)) `^ 0 = 1_. R by POLYNOM5:15;

then ((rpoly (1,a)) `^ 0) *' p = p ;

hence (rpoly (1,a)) `^ 0 divides p by RING_4:1; :: thesis: verum

IS: now :: thesis: for k being Nat st S_{1}[k] holds

S_{1}[k + 1]

for k being Nat holds SS

let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume AS: S_{1}[k]
; :: thesis: S_{1}[k + 1]

_{1}[k + 1]
; :: thesis: verum

end;assume AS: S

now :: thesis: ( (rpoly (1,a)) `^ (k + 1) divides b * p implies (rpoly (1,a)) `^ (k + 1) divides p )

hence
Sassume
(rpoly (1,a)) `^ (k + 1) divides b * p
; :: thesis: (rpoly (1,a)) `^ (k + 1) divides p

then 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; :: thesis: verum

end;then 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; :: thesis: verum

hence ( (rpoly (1,a)) `^ n divides p iff (rpoly (1,a)) `^ n divides b * p ) by divi1; :: thesis: verum