let n be Nat; :: thesis: for r being Real st 0 < r holds
ex s being Real st
( 0 < s & s < r & sqrt ((s * s) * n) < r )
let r be Real; :: thesis: ( 0 < r implies ex s being Real st
( 0 < s & s < r & sqrt ((s * s) * n) < r ) )
assume A1: 0 < r ; :: thesis: ex s being Real st
( 0 < s & s < r & sqrt ((s * s) * n) < r )
per cases ( 0 = n or 0 <> n ) ;
suppose A2: 0 = n ; :: thesis: ex s being Real st
( 0 < s & s < r & sqrt ((s * s) * n) < r )
set s = r / 2;
take r / 2 ; :: thesis: ( 0 < r / 2 & r / 2 < r & sqrt (((r / 2) * (r / 2)) * n) < r )
thus ( 0 < r / 2 & r / 2 < r & sqrt (((r / 2) * (r / 2)) * n) < r ) by A1, A2, SQUARE_1:17, XREAL_1:216; :: thesis: verum
end;
suppose A3: 0 <> n ; :: thesis: ex s being Real st
( 0 < s & s < r & sqrt ((s * s) * n) < r )
set s = r / (n + 1);
take r / (n + 1) ; :: thesis: ( 0 < r / (n + 1) & r / (n + 1) < r & sqrt (((r / (n + 1)) * (r / (n + 1))) * n) < r )
set s = r / (n + 1);
A4: n + 0 < n + 1 by XREAL_1:8;
thus 0 < r / (n + 1) by A1; :: thesis: ( r / (n + 1) < r & sqrt (((r / (n + 1)) * (r / (n + 1))) * n) < r )
0 + 1 <= n by A3, NAT_1:13;
then 1 * n <= n * n by XREAL_1:66;
then A6: ((r / (n + 1)) * (r / (n + 1))) * n <= ((r / (n + 1)) * (r / (n + 1))) * (n * n) by XREAL_1:66;
( 0 < 1 & 0 + 1 < n + 1 ) by A3, XREAL_1:8;
then 1 / (n + 1) < 1 by XREAL_1:191;
then (1 / (n + 1)) * r < r * 1 by A1, XREAL_1:68;
hence r / (n + 1) < r ; :: thesis: sqrt (((r / (n + 1)) * (r / (n + 1))) * n) < r
sqrt (((r / (n + 1)) * (r / (n + 1))) * n) <= sqrt (((r / (n + 1)) * n) ^2) by A6, SQUARE_1:26;
then A8: sqrt (((r / (n + 1)) * (r / (n + 1))) * n) <= (r / (n + 1)) * n by A1, SQUARE_1:22;
n / (n + 1) < 1 by A4, XREAL_1:191;
then (n / (n + 1)) * r < r * 1 by A1, XREAL_1:68;
hence sqrt (((r / (n + 1)) * (r / (n + 1))) * n) < r by A8, XXREAL_0:2; :: thesis: verum
end;
end;