let seq be Real_Sequence; :: thesis: ( seq is divergent_to+infty implies 2 to_power seq is divergent_to+infty )
assume A1: seq is divergent_to+infty ; :: thesis: 2 to_power seq is divergent_to+infty
let r be Real; :: according to LIMFUNC1:def 4 :: thesis: ex b₁ being set st
for b₂ being set holds
( not b₁ <= b₂ or not (2 to_power seq) . b₂ <= r )
consider p being Nat such that
A2: p > r by SEQ_4:3;
consider n being Nat such that
A3: for m being Nat st n <= m holds
p < seq . m by A1;
take n ; :: thesis: for b₁ being set holds
( not n <= b₁ or not (2 to_power seq) . b₁ <= r )
let m be Nat; :: thesis: ( not n <= m or not (2 to_power seq) . m <= r )
assume m >= n ; :: thesis: not (2 to_power seq) . m <= r
then p < seq . m by A3;
then A4: 2 to_power p < 2 to_power (seq . m) by POWER:39;
p < 2 to_power p by NEWTON:86;
then p < 2 to_power (seq . m) by A4, XXREAL_0:2;
then r < 2 to_power (seq . m) by A2, XXREAL_0:2;
hence not (2 to_power seq) . m <= r by Def1; :: thesis: verum