let n be Element of NAT ; :: thesis: for x being Real st |.x.| <= 1 holds

|.(x |^ n).| <= 1

let x be Real; :: thesis: ( |.x.| <= 1 implies |.(x |^ n).| <= 1 )

defpred S_{1}[ Nat] means |.(x |^ $1).| <= 1;

assume A1: |.x.| <= 1 ; :: thesis: |.(x |^ n).| <= 1

A2: for k being Nat st S_{1}[k] holds

S_{1}[k + 1]

.= 1 by ABSVALUE:def 1 ;

then A4: S_{1}[ 0 ]
;

for k being Nat holds S_{1}[k]
from NAT_1:sch 2(A4, A2);

hence |.(x |^ n).| <= 1 ; :: thesis: verum

|.(x |^ n).| <= 1

let x be Real; :: thesis: ( |.x.| <= 1 implies |.(x |^ n).| <= 1 )

defpred S

assume A1: |.x.| <= 1 ; :: thesis: |.(x |^ n).| <= 1

A2: for k being Nat st S

S

proof

|.(x |^ 0).| =
|.1.|
by NEWTON:4
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

A3: |.(x |^ (k + 1)).| = |.((x |^ k) * x).| by NEWTON:6

.= |.(x |^ k).| * |.x.| by COMPLEX1:65 ;

assume S_{1}[k]
; :: thesis: S_{1}[k + 1]

hence S_{1}[k + 1]
by A1, A3, COMPLEX1:46, XREAL_1:160; :: thesis: verum

end;A3: |.(x |^ (k + 1)).| = |.((x |^ k) * x).| by NEWTON:6

.= |.(x |^ k).| * |.x.| by COMPLEX1:65 ;

assume S

hence S

.= 1 by ABSVALUE:def 1 ;

then A4: S

for k being Nat holds S

hence |.(x |^ n).| <= 1 ; :: thesis: verum