defpred S_{1}[ Nat] means ex k being Nat st

( k = (10 |^ $1) - 1 & 9 divides k );

let n, k be Nat; :: thesis: ( k = (10 |^ n) - 1 implies 9 divides k )

.= 0 ;

then A6: S_{1}[ 0 ]
by NAT_D:6;

for k being Nat holds S_{1}[k]
from NAT_1:sch 2(A6, A1);

then A7: ex l being Nat st

( l = (10 |^ n) - 1 & 9 divides l ) ;

assume k = (10 |^ n) - 1 ; :: thesis: 9 divides k

hence 9 divides k by A7; :: thesis: verum

( k = (10 |^ $1) - 1 & 9 divides k );

let n, k be Nat; :: thesis: ( k = (10 |^ n) - 1 implies 9 divides k )

A1: now :: thesis: for k being Nat st S_{1}[k] holds

S_{1}[k + 1]

(10 |^ 0) - 1 =
1 - 1
by NEWTON:4
S

let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume S_{1}[k]
; :: thesis: S_{1}[k + 1]

then consider l being Nat such that

A2: l = (10 |^ k) - 1 and

A3: 9 divides l ;

consider m being Nat such that

A4: l = 9 * m by A3, NAT_D:def 3;

A5: 9 divides 9 * ((m * 10) + 1) by NAT_D:def 3;

(10 |^ (k + 1)) - 1 = (((9 * m) + 1) * 10) - 1 by A2, A4, NEWTON:6

.= 9 * ((m * 10) + 1) ;

hence S_{1}[k + 1]
by A5; :: thesis: verum

end;assume S

then consider l being Nat such that

A2: l = (10 |^ k) - 1 and

A3: 9 divides l ;

consider m being Nat such that

A4: l = 9 * m by A3, NAT_D:def 3;

A5: 9 divides 9 * ((m * 10) + 1) by NAT_D:def 3;

(10 |^ (k + 1)) - 1 = (((9 * m) + 1) * 10) - 1 by A2, A4, NEWTON:6

.= 9 * ((m * 10) + 1) ;

hence S

.= 0 ;

then A6: S

for k being Nat holds S

then A7: ex l being Nat st

( l = (10 |^ n) - 1 & 9 divides l ) ;

assume k = (10 |^ n) - 1 ; :: thesis: 9 divides k

hence 9 divides k by A7; :: thesis: verum