let a, b, n be Nat; :: thesis: ( a <= b implies a |^ n <= b |^ n )
per cases ( n = 0 or 1 <= n ) by NAT_1:14;
suppose A1: n = 0 ; :: thesis: ( a <= b implies a |^ n <= b |^ n )
( a |^ 0 = 1 & b |^ 0 = 1 ) by NEWTON:4;
hence ( a <= b implies a |^ n <= b |^ n ) by A1; :: thesis: verum
end;
suppose A1: 1 <= n ; :: thesis: ( a <= b implies a |^ n <= b |^ n )
assume a <= b ; :: thesis: a |^ n <= b |^ n
per cases then ( a < b or a = b ) by XXREAL_0:1;
suppose a < b ; :: thesis: a |^ n <= b |^ n
hence a |^ n <= b |^ n by A1, PREPOWER:10; :: thesis: verum
end;
suppose a = b ; :: thesis: a |^ n <= b |^ n
hence a |^ n <= b |^ n ; :: thesis: verum
end;
end;
end;
end;