let n be positive Integer; :: thesis: 169 divides ((3 |^ ((3 * n) + 3)) - (26 * n)) - 27
reconsider k = n as Nat by TARSKI:1;
defpred S₁[ Nat] means 169 divides ((3 |^ ((3 * $1) + 3)) - (26 * $1)) - 27;
tt: 3 |^ (2 + 1) = (3 |^ (1 + 1)) * 3 by NEWTON:6
.= ((3 |^ (0 + 1)) * 3) * 3 by NEWTON:6
.= (3 * 3) * 3 by NEWTON:5 ;
((3 |^ ((3 * 1) + 3)) - (26 * 1)) - 27 = (3 |^ (5 + 1)) - 53
.= ((3 |^ (4 + 1)) * 3) - 53 by NEWTON:6
.= (((3 |^ (3 + 1)) * 3) * 3) - 53 by NEWTON:6
.= ((((3 |^ (2 + 1)) * 3) * 3) * 3) - 53 by NEWTON:6
.= 169 * 4 by tt ;
then o: S₁[1] by INT_1:def 3;

i: now :: thesis: for n being Nat st 1 <= n & S₁[n] holds
S₁[n + 1]

let n be Nat; :: thesis: ( 1 <= n & S₁[n] implies S₁[n + 1] )
assume n: ( 1 <= n & S₁[n] ) ; :: thesis: S₁[n + 1]
d: 13 divides 13 * 2 by INT_1:def 3;
e: (((3 |^ ((3 * (n + 1)) + 3)) - (26 * (n + 1))) - 27) - (((3 |^ ((3 * n) + 3)) - (26 * n)) - 27) = ((((3 |^ 3) * (3 |^ ((3 * n) + 3))) - (26 * (n + 1))) - 27) - (((3 |^ ((3 * n) + 3)) - (26 * n)) - 27) by NEWTON:8
.= 26 * ((3 |^ ((3 * n) + 3)) - 1) by tt ;
(3 |^ (2 + 1)) - 1 = ((3 |^ (1 + 1)) * 3) - 1 by NEWTON:6
.= (((3 |^ (0 + 1)) * 3) * 3) - 1 by NEWTON:6
.= ((3 * 3) * 3) - 1 by NEWTON:5 ;
then (3 |^ 3) - 1 = 13 * 2 ;
then t: 13 divides (3 |^ 3) - 1 by INT_1:def 3;
(3 |^ (3 * (n + 1))) - 1 = ((3 |^ 3) |^ (n + 1)) - 1 by NEWTON:9
.= ((3 |^ 3) |^ (n + 1)) - (1 |^ (n + 1)) by NEWTON:10 ;
then (3 |^ 3) - 1 divides (3 |^ ((3 * n) + 3)) - 1 by NEWTON01:33;
then 13 divides (3 |^ ((3 * n) + 3)) - 1 by t, INT_2:9;
then 13 * 13 divides (((3 |^ ((3 * (n + 1)) + 3)) - (26 * (n + 1))) - 27) - (((3 |^ (3 * (n + 1))) - (26 * n)) - 27) by d, e, NEWTON03:5;
then 169 divides - ((((3 |^ ((3 * (n + 1)) + 3)) - (26 * (n + 1))) - 27) - (((3 |^ ((3 * n) + 3)) - (26 * n)) - 27)) by INT_2:10;
then 169 divides (((3 |^ ((3 * n) + 3)) - (26 * n)) - 27) - (((3 |^ ((3 * (n + 1)) + 3)) - (26 * (n + 1))) - 27) ;
then 169 divides ((3 |^ ((3 * (n + 1)) + 3)) - (26 * (n + 1))) - 27 by n, INT_5:2;
hence S₁[n + 1] ; :: thesis: verum

end;

for k being Nat st 1 <= k holds
S₁[k] from NAT_1:sch 8(o, i);
then S₁[k] by NAT_1:14;
hence 169 divides ((3 |^ ((3 * n) + 3)) - (26 * n)) - 27 ; :: thesis: verum