defpred S1[ Nat] means for n, m1, m2 being Nat
for p being prime Nat 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 S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A2: S1[k] ; :: thesis: S1[k + 1]
for n, m1, m2 being Nat
for p being prime Nat 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 Nat 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 Nat; :: 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 S1[k + 1] ; :: thesis: verum
end;
A9: S1[ 0 ]
proof
let n, m1, m2 be Nat; :: thesis: for p being prime Nat st (p |^ 0) * n = m1 * m2 & not p divides n & not p divides m2 holds
p |^ 0 divides m1
let p be prime Nat; :: 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 S1[k] from NAT_1:sch 2(A9, A1);
 hence for r, n, m1, m2 being Nat
for p being prime Nat st (p |^ r) * n = m1 * m2 & not p divides n & not p divides m2 holds
p |^ r divides m1 ; :: thesis: verum