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

( k = (10 |^ (2 * $1)) - 1 & 11 divides k );

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

.= 0 ;

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

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

then A6: ex l being Nat st

( l = (10 |^ (2 * n)) - 1 & 11 divides l ) ;

assume k = (10 |^ (2 * n)) - 1 ; :: thesis: 11 divides k

hence 11 divides k by A6; :: thesis: verum

( k = (10 |^ (2 * $1)) - 1 & 11 divides k );

let n, k be Nat; :: thesis: ( k = (10 |^ (2 * n)) - 1 implies 11 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 |^ (2 * k)) - 1 and

A3: 11 divides l ;

consider m being Nat such that

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

(10 |^ (2 * (k + 1))) - 1 = (10 |^ ((2 * k) + 2)) - 1

.= (((11 * m) + 1) * (10 |^ (1 + 1))) - 1 by A2, A4, NEWTON:8

.= (((11 * m) + 1) * ((10 |^ 1) * 10)) - 1 by NEWTON:6

.= (((11 * m) + 1) * (10 * 10)) - 1

.= 11 * ((m * 100) + 9) ;

hence S_{1}[k + 1]
by NAT_D:def 3; :: thesis: verum

end;assume S

then consider l being Nat such that

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

A3: 11 divides l ;

consider m being Nat such that

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

(10 |^ (2 * (k + 1))) - 1 = (10 |^ ((2 * k) + 2)) - 1

.= (((11 * m) + 1) * (10 |^ (1 + 1))) - 1 by A2, A4, NEWTON:8

.= (((11 * m) + 1) * ((10 |^ 1) * 10)) - 1 by NEWTON:6

.= (((11 * m) + 1) * (10 * 10)) - 1

.= 11 * ((m * 100) + 9) ;

hence S

.= 0 ;

then A5: S

for k being Nat holds S

then A6: ex l being Nat st

( l = (10 |^ (2 * n)) - 1 & 11 divides l ) ;

assume k = (10 |^ (2 * n)) - 1 ; :: thesis: 11 divides k

hence 11 divides k by A6; :: thesis: verum