let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A0: S₁[n] ; :: thesis: S₁[n + 1]
let i be Nat; :: thesis: ( 2 <= i implies i |^ (n + 1) >= (n + 1) + 1 )
assume A4: 2 <= i ; :: thesis: i |^ (n + 1) >= (n + 1) + 1
i |^ n >= n + 1 by A0, A4;
then A2: i * (i |^ n) >= i * (n + 1) by XREAL_1:64;
A1: i |^ (n + 1) = i * (i |^ n) by Th6;
A3: 2 + n <= i + n by A4, XREAL_1:6;
1 <= i by A4, XXREAL_0:2;
then i * n >= n by XREAL_1:151;
then (i * n) + i >= n + i by XREAL_1:6;
then i * (i |^ n) >= n + i by A2, XXREAL_0:2;
hence i |^ (n + 1) >= (n + 1) + 1 by A1, A3, XXREAL_0:2; :: thesis: verum