let m, n be Nat; :: thesis: ( n <> 0 & (2 |^ m) - (3 |^ n) = 1 implies ( m = 2 & n = 1 ) )
assume that
A1: n <> 0 and
A2: (2 |^ m) - (3 |^ n) = 1 ; :: thesis: ( m = 2 & n = 1 )
A3: 3 |^ 0 = 1 by NEWTON:4;

per cases ( m <= 2 or m >= 2 + 1 ) by NAT_1:13;

suppose m <= 2 ; :: thesis: ( m = 2 & n = 1 )

then not not m = 0 & ... & not m = 2 ;

per cases then ( m = 0 or m = 1 or m = 2 ) ;

suppose m = 0 ; :: thesis: ( m = 2 & n = 1 )

then (2 |^ 0) - (3 |^ n) = 1 by A2;
hence ( m = 2 & n = 1 ) by Lm1; :: thesis: verum

end;

suppose m = 1 ; :: thesis: ( m = 2 & n = 1 )

then (2 |^ 1) - (3 |^ n) = 1 by A2;
hence ( m = 2 & n = 1 ) by A1, A3, PEPIN:30; :: thesis: verum

end;

suppose A4: m = 2 ; :: thesis: ( m = 2 & n = 1 )

then (2 |^ 2) - (3 |^ n) = 1 by A2;
then 3 |^ n = 3 |^ 1 by Lm3;
hence ( m = 2 & n = 1 ) by A4, PEPIN:30; :: thesis: verum

end;

end;

end;

suppose A5: m >= 2 + 1 ; :: thesis: ( m = 2 & n = 1 )

not 8 divides (3 |^ n) + 1 by Th66;
hence ( m = 2 & n = 1 ) by A2, A5, Lm12, NEWTON:89; :: thesis: verum

end;

end;