let m, n be Nat; :: thesis: ( n is even & (3 |^ n) - (2 |^ m) = 1 implies ( n = 2 & m = 3 ) )
assume that
A1: n is even and
A2: (3 |^ n) - (2 |^ m) = 1 ; :: thesis: ( n = 2 & m = 3 )
consider k being Nat such that
A3: n = 2 * k by A1;
A4: 3 |^ (2 * k) = (3 |^ k) |^ 2 by NEWTON:9
.= (3 |^ k) ^2 by WSIERP_1:1 ;
A5: 2 |^ m = (3 |^ n) - 1 by A2;
(3 |^ k) + 1 divides ((3 |^ k) + 1) * ((3 |^ k) - 1) ;
then consider a being Nat such that
A6: (3 |^ k) + 1 = 2 |^ a by A5, A3, A4, NEWTON03:36, XPRIMES1:2;
(3 |^ k) - 1 divides ((3 |^ k) + 1) * ((3 |^ k) - 1) ;
then consider b being Nat such that
A7: (3 |^ k) - 1 = 2 |^ b by A5, A3, A4, NEWTON03:36, XPRIMES1:2;
(2 |^ a) - (2 |^ b) = 2 by A6, A7;
then (3 |^ k) + 1 = 4 by A6, Lm3, Th70;
then 3 |^ k = 3 |^ 1 ;
then k = 1 by PEPIN:30;
hence ( n = 2 & m = 3 ) by A3, A5, Lm8, Lm12, PEPIN:30; :: thesis: verum