let a, b be Nat; :: thesis: for n being non zero Nat st n -root b is irrational & n -root b > a holds
ex c being Nat st
( a |^ n < b & b < (a + (2 * c)) |^ n )
let n be non zero Nat; :: thesis: ( n -root b is irrational & n -root b > a implies ex c being Nat st
( a |^ n < b & b < (a + (2 * c)) |^ n ) )
assume A1: ( n -root b is irrational & n -root b > a ) ; :: thesis: ex c being Nat st
( a |^ n < b & b < (a + (2 * c)) |^ n )
then consider k being Nat such that
A2: ( k |^ n < b & b < (k + 1) |^ n ) by Th22;
A3: (n -root b) |^ n > a |^ n by A1, NEWTON02:40;
then a |^ n < (k + 1) |^ n by A2, XXREAL_0:2;
then a < k + 1 by NEWTON02:41;
then consider l being Nat such that
A5: k + 1 = a + l by NAT_1:10;
reconsider l = l as non zero Nat by A3, A2, A5;
(a + l) + l > (a + l) + 0 by XREAL_1:6;
then (a + (2 * l)) |^ n > (k + 1) |^ n by A5, NEWTON02:40;
then (a + (2 * l)) |^ n > b by A2, XXREAL_0:2;
hence ex c being Nat st
( a |^ n < b & b < (a + (2 * c)) |^ n ) by A3; :: thesis: verum