let n be Nat; :: thesis: ( n >= 3 implies n + n < 2 |^ n )
assume AS: n >= 3 ; :: thesis: n + n < 2 |^ n
defpred S₁[ Nat] means $1 + $1 < 2 |^ $1;
IA: S₁[3]

proof

2 |^ (2 + 1) = (2 |^ (1 + 1)) * 2 by NEWTON:6
.= ((2 |^ 1) * (2 |^ 1)) * 2 by NEWTON:6
.= (2 * 2) * 2 ;
hence 2 |^ 3 > 3 + 3 ; :: thesis: verum

end;

IS: now :: thesis: for k being Nat st k >= 3 & S₁[k] holds
S₁[k + 1]

let k be Nat; :: thesis: ( k >= 3 & S₁[k] implies S₁[k + 1] )
assume A: k >= 3 ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume B: S₁[k] ; :: thesis: S₁[k + 1]
C: 2 |^ (k + 1) = (2 |^ k) * 2 by NEWTON:6
.= (2 |^ k) + (2 |^ k) ;
D: (2 |^ k) + (2 |^ k) > (k + k) + (k + k) by B, XREAL_1:8;
k > 1 by A, XXREAL_0:2;
then k + k > k + 1 by XREAL_1:8;
then (k + k) + (k + k) > (k + 1) + (k + 1) by XREAL_1:8;
hence S₁[k + 1] by C, D, XXREAL_0:2; :: thesis: verum

end;

for k being Nat st k >= 3 holds
S₁[k] from NAT_1:sch 8(IA, IS);
hence n + n < 2 |^ n by AS; :: thesis: verum