let m be Nat; :: thesis: 3 |^ m divides (2 |^ (3 |^ m)) + 1
defpred S₁[ Nat] means 3 |^ $1 divides (2 |^ (3 |^ $1)) + 1;
A1: S₁[ 0 ]

proof

3 |^ 0 = 1 by NEWTON:4;
hence S₁[ 0 ] by INT_2:12; :: thesis: verum

end;

A2: for m being Nat st S₁[m] holds
S₁[m + 1]

proof

let m be Nat; :: thesis: ( S₁[m] implies S₁[m + 1] )
set a = 3 |^ m;
given k being Nat such that A3: (2 |^ (3 |^ m)) + 1 = (3 |^ m) * k ; :: according to NAT_D:def 3 :: thesis: S₁[m + 1]
set z = (3 |^ m) * k;

per cases ( m = 0 or 0 < m ) ;

suppose A4: m = 0 ; :: thesis: S₁[m + 1]

(2 |^ (3 |^ 1)) + 1 = ((2 * 2) * 2) + 1 by POLYEQ_5:2
.= 3 * 3 ;
then 3 |^ 1 divides (2 |^ (3 |^ 1)) + 1 ;
hence S₁[m + 1] by A4; :: thesis: verum

end;

suppose 0 < m ; :: thesis: S₁[m + 1]

then reconsider m1 = m - 1 as Nat ;
set t = ((((((3 |^ m1) * (3 |^ m)) * k) * k) * k) - (3 * (((3 |^ m1) * k) * k))) + k;
A5: 3 |^ (m + 1) = 3 * (3 |^ m) by NEWTON:6;
A6: ((3 |^ m) * k) |^ 3 = (((3 |^ m) * k) * ((3 |^ m) * k)) * ((3 |^ m) * k) by POLYEQ_5:2
.= (((((3 |^ m) * (3 |^ m)) * (3 |^ m)) * k) * k) * k
.= ((((3 |^ (m + (m1 + 1))) * (3 |^ m)) * k) * k) * k by NEWTON:8
.= ((((3 |^ ((m + 1) + m1)) * (3 |^ m)) * k) * k) * k
.= (((((3 |^ (m + 1)) * (3 |^ m1)) * (3 |^ m)) * k) * k) * k by NEWTON:8
.= (3 |^ (m + 1)) * (((((3 |^ m1) * (3 |^ m)) * k) * k) * k) ;
A7: ((3 |^ m) * k) |^ 2 = ((3 |^ m) * k) * ((3 |^ m) * k) by POLYEQ_5:1
.= (((3 |^ m) * (3 |^ m)) * k) * k
.= ((3 |^ (m + (m1 + 1))) * k) * k by NEWTON:8
.= ((3 |^ ((m + 1) + m1)) * k) * k
.= (((3 |^ (m + 1)) * (3 |^ m1)) * k) * k by NEWTON:8
.= (3 |^ (m + 1)) * (((3 |^ m1) * k) * k) ;
2 |^ (3 |^ (m + 1)) = (((3 |^ m) * k) - 1) |^ 3 by A3, A5, NEWTON:9
.= (((((3 |^ m) * k) |^ 3) - ((3 * (((3 |^ m) * k) |^ 2)) * 1)) + ((3 * (1 |^ 2)) * ((3 |^ m) * k))) - (1 |^ 3) by POLYEQ_5:5
.= ((3 |^ (m + 1)) * (((((((3 |^ m1) * (3 |^ m)) * k) * k) * k) - (3 * (((3 |^ m1) * k) * k))) + k)) - 1 by A5, A6, A7 ;
then 3 |^ (m + 1) divides (2 |^ (3 |^ (m + 1))) + 1 ;
hence S₁[m + 1] ; :: thesis: verum

end;

end;

end;

for m being Nat holds S₁[m] from NAT_1:sch 2(A1, A2);
hence 3 |^ m divides (2 |^ (3 |^ m)) + 1 ; :: thesis: verum