defpred S₁[ Nat] means for k, q, d being Element of NAT st q is prime & d divides k * (q |^ ($1 + 1)) & not d divides k * (q |^ $1) holds
q |^ ($1 + 1) divides d;
A1: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A2: for k, q, d being Element of NAT st q is prime & d divides k * (q |^ (n + 1)) & not d divides k * (q |^ n) holds
q |^ (n + 1) divides d ; :: thesis: S₁[n + 1]
for k, q, d being Element of NAT st q is prime & d divides k * (q |^ ((n + 1) + 1)) & not d divides k * (q |^ (n + 1)) holds
q |^ ((n + 1) + 1) divides d

proof

let k, q, d be Element of NAT ; :: thesis: ( q is prime & d divides k * (q |^ ((n + 1) + 1)) & not d divides k * (q |^ (n + 1)) implies q |^ ((n + 1) + 1) divides d )
assume A3: q is prime ; :: thesis: ( not d divides k * (q |^ ((n + 1) + 1)) or d divides k * (q |^ (n + 1)) or q |^ ((n + 1) + 1) divides d )
assume A4: d divides k * (q |^ ((n + 1) + 1)) ; :: thesis: ( d divides k * (q |^ (n + 1)) or q |^ ((n + 1) + 1) divides d )
then consider i being Nat such that
A5: k * (q |^ ((n + 1) + 1)) = d * i by NAT_D:def 3;
assume A6: not d divides k * (q |^ (n + 1)) ; :: thesis: q |^ ((n + 1) + 1) divides d
then not d divides k * (q * (q |^ n)) by NEWTON:6;
then A7: not d divides (k * q) * (q |^ n) ;
d divides k * (q * (q |^ (n + 1))) by A4, NEWTON:6;
then d divides (k * q) * (q |^ (n + 1)) ;
then q |^ (n + 1) divides d by A2, A3, A7;
then consider j being Nat such that
A8: d = (q |^ (n + 1)) * j by NAT_D:def 3;
A9: not q divides i

proof

assume q divides i ; :: thesis: contradiction
then consider i1 being Nat such that
A10: i = q * i1 by NAT_D:def 3;
k * ((q |^ (n + 1)) * q) = d * (q * i1) by A5, A10, NEWTON:6;
then (k * (q |^ (n + 1))) * q = (d * i1) * q ;
then k * (q |^ (n + 1)) = d * i1 by A3, XCMPLX_1:5;
hence contradiction by A6, NAT_D:def 3; :: thesis: verum

end;

k * (q |^ ((n + 1) + 1)) = k * ((q |^ (n + 1)) * q) by NEWTON:6
.= (k * q) * (q |^ (n + 1)) ;
then (k * q) * (q |^ (n + 1)) = (j * i) * (q |^ (n + 1)) by A5, A8;
then k * q = j * i by A3, XCMPLX_1:5;
then q divides j * i by NAT_D:def 3;
then q divides j by A3, A9, NEWTON:80;
then consider j1 being Nat such that
A11: j = q * j1 by NAT_D:def 3;
d = ((q |^ (n + 1)) * q) * j1 by A8, A11;
then d = (q |^ ((n + 1) + 1)) * j1 by NEWTON:6;
hence q |^ ((n + 1) + 1) divides d by NAT_D:def 3; :: thesis: verum

end;

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

end;

A12: S₁[ 0 ]

proof

let k, q, d be Element of NAT ; :: thesis: ( q is prime & d divides k * (q |^ (0 + 1)) & not d divides k * (q |^ 0) implies q |^ (0 + 1) divides d )
assume that
A13: q is prime and
A14: d divides k * (q |^ (0 + 1)) and
A15: not d divides k * (q |^ 0) ; :: thesis: q |^ (0 + 1) divides d
d divides k * q by A14;
then consider i being Nat such that
A16: k * q = d * i by NAT_D:def 3;
assume not q |^ (0 + 1) divides d ; :: thesis: contradiction
then A17: not q divides d ;
q divides d * i by A16, NAT_D:def 3;
then q divides i by A13, A17, NEWTON:80;
then consider j being Nat such that
A18: i = q * j by NAT_D:def 3;
(d * j) * q = k * q by A16, A18;
then A19: d * j = k by A13, XCMPLX_1:5;
not d divides k * 1 by A15, NEWTON:4;
hence contradiction by A19, NAT_D:def 3; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A12, A1);
hence for k, q, n, d being Element of NAT st q is prime & d divides k * (q |^ (n + 1)) & not d divides k * (q |^ n) holds
q |^ (n + 1) divides d ; :: thesis: verum