defpred S₁[ Nat] means for n, m1, m2 being Nat
for p being Prime st (p |^ $1) * n = m1 * m2 & not p divides n & not p divides m2 holds
p |^ $1 divides m1;
A1: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A2: S₁[k] ; :: thesis: S₁[k + 1]
for n, m1, m2 being Nat
for p being Prime st (p |^ (k + 1)) * n = m1 * m2 & not p divides n & not p divides m2 holds
p |^ (k + 1) divides m1

proof

let n, m1, m2 be Nat; :: thesis: for p being Prime st (p |^ (k + 1)) * n = m1 * m2 & not p divides n & not p divides m2 holds
p |^ (k + 1) divides m1
let p be Prime; :: thesis: ( (p |^ (k + 1)) * n = m1 * m2 & not p divides n & not p divides m2 implies p |^ (k + 1) divides m1 )
assume A3: (p |^ (k + 1)) * n = m1 * m2 ; :: thesis: ( p divides n or p divides m2 or p |^ (k + 1) divides m1 )
reconsider p9 = p as prime Element of NAT by ORDINAL1:def 12;
assume A4: not p divides n ; :: thesis: ( p divides m2 or p |^ (k + 1) divides m1 )
assume A5: not p divides m2 ; :: thesis: p |^ (k + 1) divides m1
A6: (p |^ (k + 1)) * n = ((p |^ k) * p) * n by NEWTON:6
.= ((p |^ k) * n) * p ;
then p divides m1 * m2 by A3, NAT_D:def 3;
then p divides m1 by A5, NEWTON:80;
then consider m19 being Nat such that
A7: m1 = p * m19 by NAT_D:def 3;
((p |^ k) * n) * p9 = (m19 * m2) * p9 by A3, A6, A7;
then p |^ k divides m19 by A2, A4, A5, XCMPLX_1:5;
then consider m199 being Nat such that
A8: m19 = (p |^ k) * m199 by NAT_D:def 3;
m1 = ((p |^ k) * p) * m199 by A7, A8
.= (p |^ (k + 1)) * m199 by NEWTON:6 ;
hence p |^ (k + 1) divides m1 by NAT_D:def 3; :: thesis: verum

end;

hence S₁[k + 1] ; :: thesis: verum

end;

A9: S₁[ 0 ]

proof

let n, m1, m2 be Nat; :: thesis: for p being Prime st (p |^ 0) * n = m1 * m2 & not p divides n & not p divides m2 holds
p |^ 0 divides m1
let p be Prime; :: thesis: ( (p |^ 0) * n = m1 * m2 & not p divides n & not p divides m2 implies p |^ 0 divides m1 )
assume that
(p |^ 0) * n = m1 * m2 and
not p divides n and
not p divides m2 ; :: thesis: p |^ 0 divides m1
p |^ 0 = 1 by NEWTON:4;
hence p |^ 0 divides m1 by NAT_D:6; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A9, A1);
hence for r, n, m1, m2 being Nat
for p being Prime st (p |^ r) * n = m1 * m2 & not p divides n & not p divides m2 holds
p |^ r divides m1 ; :: thesis: verum