defpred S₁[ Element of 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: 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 A2: ( q is prime & d divides k * (q |^ (0 + 1)) & not d divides k * (q |^ 0 ) ) ; :: thesis: q |^ (0 + 1) divides d
assume not q |^ (0 + 1) divides d ; :: thesis: contradiction
then A3: not q divides d by NEWTON:10;
A5: not d divides k * 1 by A2, NEWTON:9;
d divides k * q by A2, NEWTON:10;
then consider i being Nat such that
A6: k * q = d * i by NAT_D:def 3;
q divides d * i by A6, NAT_D:def 3;
then q divides i by A2, A3, NEWTON:98;
then consider j being Nat such that
A7: i = q * j by NAT_D:def 3;
(d * j) * q = k * q by A6, A7;
then d * j = k by A2, XCMPLX_1:5;
hence contradiction by A5, NAT_D:def 3; :: thesis: verum

end;

A8: for n being Element of NAT st S₁[n] holds
S₁[n + 1]

proof

let n be Element of NAT ; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A9: 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 A10: 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 A11: d divides k * (q |^ ((n + 1) + 1)) ; :: thesis: ( d divides k * (q |^ (n + 1)) or q |^ ((n + 1) + 1) divides d )
assume A12: not d divides k * (q |^ (n + 1)) ; :: thesis: q |^ ((n + 1) + 1) divides d
d divides k * (q * (q |^ (n + 1))) by A11, NEWTON:11;
then A13: d divides (k * q) * (q |^ (n + 1)) ;
not d divides k * (q * (q |^ n)) by A12, NEWTON:11;
then not d divides (k * q) * (q |^ n) ;
then A14: q |^ (n + 1) divides d by A9, A10, A13;
consider i being Nat such that
A15: k * (q |^ ((n + 1) + 1)) = d * i by A11, NAT_D:def 3;
consider j being Nat such that
A16: d = (q |^ (n + 1)) * j by A14, NAT_D:def 3;
k * (q |^ ((n + 1) + 1)) = k * ((q |^ (n + 1)) * q) by NEWTON:11
.= (k * q) * (q |^ (n + 1)) ;
then A17: (k * q) * (q |^ (n + 1)) = (j * i) * (q |^ (n + 1)) by A15, A16;
A18: not q divides i

proof

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

end;

k * q = j * i by A17, XCMPLX_1:5, A10;
then q divides j * i by NAT_D:def 3;
then q divides j by A10, A18, NEWTON:98;
then consider j1 being Nat such that
A21: j = q * j1 by NAT_D:def 3;
d = ((q |^ (n + 1)) * q) * j1 by A16, A21;
then d = (q |^ ((n + 1) + 1)) * j1 by NEWTON:11;
hence q |^ ((n + 1) + 1) divides d by NAT_D:def 3; :: thesis: verum

end;

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

end;

for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A1, A8);
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