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

proof

let n, m1, m2 be natural number ; :: thesis: for p being natural prime number st (p |^ 0 ) * n = m1 * m2 & not p divides n & not p divides m2 holds
p |^ 0 divides m1
let p be natural prime number ; :: thesis: ( (p |^ 0 ) * n = m1 * m2 & not p divides n & not p divides m2 implies p |^ 0 divides m1 )
assume ( (p |^ 0 ) * n = m1 * m2 & not p divides n & not p divides m2 ) ; :: thesis: p |^ 0 divides m1
p |^ 0 = 1 by NEWTON:9;
hence p |^ 0 divides m1 by NAT_D:6; :: thesis: verum

end;

A2: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A3: S₁[k] ; :: thesis: S₁[k + 1]
for n, m1, m2 being natural number
for p being natural prime number 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 natural number ; :: thesis: for p being natural prime number st (p |^ (k + 1)) * n = m1 * m2 & not p divides n & not p divides m2 holds
p |^ (k + 1) divides m1
let p be natural prime number ; :: thesis: ( (p |^ (k + 1)) * n = m1 * m2 & not p divides n & not p divides m2 implies p |^ (k + 1) divides m1 )
assume A4: (p |^ (k + 1)) * n = m1 * m2 ; :: thesis: ( p divides n or p divides m2 or p |^ (k + 1) divides m1 )
assume A5: not p divides n ; :: thesis: ( p divides m2 or p |^ (k + 1) divides m1 )
assume A6: not p divides m2 ; :: thesis: p |^ (k + 1) divides m1
reconsider p' = p as prime Element of NAT by ORDINAL1:def 13;
A7: (p |^ (k + 1)) * n = ((p |^ k) * p) * n by NEWTON:11
.= ((p |^ k) * n) * p ;
then p divides m1 * m2 by A4, NAT_D:def 3;
then p divides m1 by A6, NEWTON:98;
then consider m1' being natural number such that
A8: m1 = p * m1' by NAT_D:def 3;
((p |^ k) * n) * p' = (m1' * m2) * p' by A4, A7, A8;
then p |^ k divides m1' by A3, A5, A6, XCMPLX_1:5;
then consider m1'' being natural number such that
A9: m1' = (p |^ k) * m1'' by NAT_D:def 3;
m1 = ((p |^ k) * p) * m1'' by A8, A9
.= (p |^ (k + 1)) * m1'' by NEWTON:11 ;
hence p |^ (k + 1) divides m1 by NAT_D:def 3; :: thesis: verum

end;

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

end;

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