let m, n be Nat; :: thesis: ( not (3 |^ n) - (2 |^ m) = 1 or ( n = m & m = 1 ) or ( n = 2 & m = 3 ) )

per cases ( n is odd or n is even ) ;

suppose n is odd ; :: thesis: ( not (3 |^ n) - (2 |^ m) = 1 or ( n = m & m = 1 ) or ( n = 2 & m = 3 ) )

hence ( not (3 |^ n) - (2 |^ m) = 1 or ( n = m & m = 1 ) or ( n = 2 & m = 3 ) ) by Th71; :: thesis: verum

end;

suppose n is even ; :: thesis: ( not (3 |^ n) - (2 |^ m) = 1 or ( n = m & m = 1 ) or ( n = 2 & m = 3 ) )

hence ( not (3 |^ n) - (2 |^ m) = 1 or ( n = m & m = 1 ) or ( n = 2 & m = 3 ) ) by Th72; :: thesis: verum

end;

end;