let C be Simple_closed_curve; :: thesis: for n being Nat
for p being Point of (TOP-REAL 2)
for J being Integer st J = [\(((((p `2) - (S-bound C)) / ((N-bound C) - (S-bound C))) * (2 |^ n)) + 2)/] holds
p `2 < (S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (J - 1))
let n be Nat; :: thesis: for p being Point of (TOP-REAL 2)
for J being Integer st J = [\(((((p `2) - (S-bound C)) / ((N-bound C) - (S-bound C))) * (2 |^ n)) + 2)/] holds
p `2 < (S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (J - 1))
let p be Point of (TOP-REAL 2); :: thesis: for J being Integer st J = [\(((((p `2) - (S-bound C)) / ((N-bound C) - (S-bound C))) * (2 |^ n)) + 2)/] holds
p `2 < (S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (J - 1))
set W = S-bound C;
set E = N-bound C;
set EW = (N-bound C) - (S-bound C);
set PW = (p `2) - (S-bound C);
let I be Integer; :: thesis: ( I = [\(((((p `2) - (S-bound C)) / ((N-bound C) - (S-bound C))) * (2 |^ n)) + 2)/] implies p `2 < (S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (I - 1)) )
set KI = I - 1;
A1: 2 |^ n > 0 by NEWTON:83;
assume I = [\(((((p `2) - (S-bound C)) / ((N-bound C) - (S-bound C))) * (2 |^ n)) + 2)/] ; :: thesis: p `2 < (S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (I - 1))
then I > (((((p `2) - (S-bound C)) / ((N-bound C) - (S-bound C))) * (2 |^ n)) + 2) - 1 by INT_1:def 6;
then A2: I - 1 > (((((p `2) - (S-bound C)) / ((N-bound C) - (S-bound C))) * (2 |^ n)) + 1) - 1 by XREAL_1:9;
A3: (S-bound C) + ((p `2) - (S-bound C)) = p `2 ;
A4: (N-bound C) - (S-bound C) > 0 by TOPREAL5:16, XREAL_1:50;
then A5: ((N-bound C) - (S-bound C)) / (2 |^ n) > 0 by A1, XREAL_1:139;
(((N-bound C) - (S-bound C)) / (2 |^ n)) * ((((p `2) - (S-bound C)) / ((N-bound C) - (S-bound C))) * (2 |^ n)) = (p `2) - (S-bound C) by A4, A1, Lm2;
then (((N-bound C) - (S-bound C)) / (2 |^ n)) * (I - 1) > (p `2) - (S-bound C) by A2, A5, XREAL_1:68;
hence p `2 < (S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (I - 1)) by A3, XREAL_1:6; :: thesis: verum