let m, n be Nat; ( n is odd & (3 |^ n) - (2 |^ m) = 1 implies ( n = m & m = 1 ) )
assume that
A1:
n is odd
and
A2:
(3 |^ n) - (2 |^ m) = 1
; ( n = m & m = 1 )
A3:
3 |^ n = 1 + (2 |^ m)
by A2;
consider k being Nat such that
A4:
n = (2 * k) + 1
by A1, ABIAN:9;
3 |^ (2 * k),1 are_congruent_mod 4
by Th68;
then
(3 |^ (2 * k)) * 3,1 * 3 are_congruent_mod 4
by Lm13, INT_1:18;
then
3 |^ n,3 are_congruent_mod 4
by A4, NEWTON:6;
then
2 |^ m,3 - 1 are_congruent_mod 4
by A2;
then (2 |^ m) mod 4 =
2 mod 4
by NAT_D:64
.=
2
by NAT_D:24
;
then A5:
m = 1
by Th69;
then
3 |^ n = 3 |^ 1
by A3;
hence
( n = m & m = 1 )
by A5, PEPIN:30; verum