A1: 2 |^ 2 = 2 |^ (1 + 1)
.= (2 |^ 1) * 2 by NEWTON:6
.= 2 * 2 ;
A2: 2 |^ 3 = 2 |^ (2 + 1)
.= (2 |^ 2) * 2 by NEWTON:6
.= 8 by A1 ;
A3: 2 |^ 4 = 2 |^ (3 + 1)
.= (2 |^ 3) * 2 by NEWTON:6
.= 16 by A2 ;
reconsider e = 1 as odd Nat by Lm5;
take e ; :: according to NAT_6:def 5 :: thesis: ex n being positive Nat st
( 2 |^ n > e & 17 = (e * (2 |^ n)) + 1 )
take 4 ; :: thesis: ( 2 |^ 4 > e & 17 = (e * (2 |^ 4)) + 1 )
thus ( 2 |^ 4 > e & 17 = (e * (2 |^ 4)) + 1 ) by A3; :: thesis: verum