let n be Nat; :: thesis: for T being _Theta
for alpha, epsilon being Real st alpha = (1 + (T * epsilon)) |^ n & 0 <= epsilon & epsilon <= 1 / (2 * n) holds
ex T1 being _Theta st alpha = 1 + (((T1 * 2) * n) * epsilon)
defpred S₁[ Nat] means for T being _Theta
for alpha, epsilon being Real st alpha = (1 + (T * epsilon)) |^ $1 & 0 <= epsilon & epsilon <= 1 / (2 * $1) holds
ex T1 being _Theta st alpha = 1 + (((T1 * 2) * $1) * epsilon);
A1: S₁[ 0 ]

proof

let T be _Theta; :: thesis: for alpha, epsilon being Real st alpha = (1 + (T * epsilon)) |^ 0 & 0 <= epsilon & epsilon <= 1 / (2 * 0) holds
ex T1 being _Theta st alpha = 1 + (((T1 * 2) * 0) * epsilon)
let alpha, epsilon be Real; :: thesis: ( alpha = (1 + (T * epsilon)) |^ 0 & 0 <= epsilon & epsilon <= 1 / (2 * 0) implies ex T1 being _Theta st alpha = 1 + (((T1 * 2) * 0) * epsilon) )
assume A2: ( alpha = (1 + (T * epsilon)) |^ 0 & 0 <= epsilon & epsilon <= 1 / (2 * 0) ) ; :: thesis: ex T1 being _Theta st alpha = 1 + (((T1 * 2) * 0) * epsilon)
take T ; :: thesis: alpha = 1 + (((T * 2) * 0) * epsilon)
thus alpha = 1 + (((T * 2) * 0) * epsilon) by A2, NEWTON:4; :: thesis: verum

end;

A3: for m being Nat st S₁[m] holds
S₁[m + 1]

proof

let m be Nat; :: thesis: ( S₁[m] implies S₁[m + 1] )
assume A4: S₁[m] ; :: thesis: S₁[m + 1]
set m1 = m + 1;
let T be _Theta; :: thesis: for alpha, epsilon being Real st alpha = (1 + (T * epsilon)) |^ (m + 1) & 0 <= epsilon & epsilon <= 1 / (2 * (m + 1)) holds
ex T1 being _Theta st alpha = 1 + (((T1 * 2) * (m + 1)) * epsilon)
let alpha, epsilon be Real; :: thesis: ( alpha = (1 + (T * epsilon)) |^ (m + 1) & 0 <= epsilon & epsilon <= 1 / (2 * (m + 1)) implies ex T1 being _Theta st alpha = 1 + (((T1 * 2) * (m + 1)) * epsilon) )
assume A5: ( alpha = (1 + (T * epsilon)) |^ (m + 1) & 0 <= epsilon & epsilon <= 1 / (2 * (m + 1)) ) ; :: thesis: ex T1 being _Theta st alpha = 1 + (((T1 * 2) * (m + 1)) * epsilon)

per cases ( m = 0 or m > 0 ) ;

suppose A6: m = 0 ; :: thesis: ex T1 being _Theta st alpha = 1 + (((T1 * 2) * (m + 1)) * epsilon)

1 <= m + 1 by NAT_1:11;
then ( 1 <= 2 * 1 & 2 * 1 <= 2 * (m + 1) ) by XREAL_1:66;
then 1 <= 2 * (m + 1) by XXREAL_0:2;
then reconsider I = 1 / (2 * (m + 1)) as _Theta by Def1, XREAL_1:183;
alpha = 1 + ((T * (I * (2 * (m + 1)))) * epsilon) by A5, A6;
then alpha = 1 + ((((T * I) * 2) * (m + 1)) * epsilon) ;
hence ex T1 being _Theta st alpha = 1 + (((T1 * 2) * (m + 1)) * epsilon) ; :: thesis: verum

end;

suppose A7: m > 0 ; :: thesis: ex T1 being _Theta st alpha = 1 + (((T1 * 2) * (m + 1)) * epsilon)

(2 * m) * 1 <= (2 * (m + 1)) * 1 by XREAL_1:64, NAT_1:11;
then 1 / (2 * (m + 1)) <= 1 / (2 * m) by A7, XREAL_1:102;
then A8: epsilon <= 1 / (2 * m) by A5, XXREAL_0:2;
then consider T1 being _Theta such that
A9: (1 + (T * epsilon)) |^ m = 1 + (((T1 * 2) * m) * epsilon) by A5, A4;
A10: (1 + (T * epsilon)) |^ (m + 1) = (1 + (T1 * ((2 * m) * epsilon))) * (1 + (T * epsilon)) by A9, NEWTON:6;
epsilon * (2 * m) <= (1 / (2 * m)) * (2 * m) by A8, XREAL_1:64;
then ( 0 <= (2 * m) * epsilon & (2 * m) * epsilon <= 1 ) by A5, XCMPLX_1:87, A7;
then consider T2 being _Theta such that
A11: (1 + (T * epsilon)) |^ (m + 1) = 1 + (T2 * (((2 * m) * epsilon) + (2 * epsilon))) by A5, A10, Th3;
take T2 ; :: thesis: alpha = 1 + (((T2 * 2) * (m + 1)) * epsilon)
thus alpha = 1 + (((T2 * 2) * (m + 1)) * epsilon) by A5, A11; :: thesis: verum

end;

end;

end;

for m being Nat holds S₁[m] from NAT_1:sch 2(A1, A3);
hence for T being _Theta
for alpha, epsilon being Real st alpha = (1 + (T * epsilon)) |^ n & 0 <= epsilon & epsilon <= 1 / (2 * n) holds
ex T1 being _Theta st alpha = 1 + (((T1 * 2) * n) * epsilon) ; :: thesis: verum