let C be Simple_closed_curve; :: thesis: for n being Element of NAT
for p being Point of (TOP-REAL 2)
for I being Integer st I = [\(((((p `1 ) - (W-bound C)) / ((E-bound C) - (W-bound C))) * (2 |^ n)) + 2)/] holds
p `1 < (W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (I - 1))
let n be Element of NAT ; :: thesis: for p being Point of (TOP-REAL 2)
for I being Integer st I = [\(((((p `1 ) - (W-bound C)) / ((E-bound C) - (W-bound C))) * (2 |^ n)) + 2)/] holds
p `1 < (W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (I - 1))
let p be Point of (TOP-REAL 2); :: thesis: for I being Integer st I = [\(((((p `1 ) - (W-bound C)) / ((E-bound C) - (W-bound C))) * (2 |^ n)) + 2)/] holds
p `1 < (W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (I - 1))
set W = W-bound C;
set E = E-bound C;
set EW = (E-bound C) - (W-bound C);
set PW = (p `1 ) - (W-bound C);
let I be Integer; :: thesis: ( I = [\(((((p `1 ) - (W-bound C)) / ((E-bound C) - (W-bound C))) * (2 |^ n)) + 2)/] implies p `1 < (W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (I - 1)) )
assume A1: I = [\(((((p `1 ) - (W-bound C)) / ((E-bound C) - (W-bound C))) * (2 |^ n)) + 2)/] ; :: thesis: p `1 < (W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (I - 1))
set KI = I - 1;
I > (((((p `1 ) - (W-bound C)) / ((E-bound C) - (W-bound C))) * (2 |^ n)) + 2) - 1 by A1, INT_1:def 4;
then A2: I - 1 > (((((p `1 ) - (W-bound C)) / ((E-bound C) - (W-bound C))) * (2 |^ n)) + 1) - 1 by XREAL_1:11;
E-bound C > W-bound C by TOPREAL5:23;
then A3: ( (E-bound C) - (W-bound C) > 0 & 2 |^ n > 0 ) by NEWTON:102, XREAL_1:52;
then A4: ((E-bound C) - (W-bound C)) / (2 |^ n) > 0 by XREAL_1:141;
A5: (((E-bound C) - (W-bound C)) / (2 |^ n)) * ((((p `1 ) - (W-bound C)) / ((E-bound C) - (W-bound C))) * (2 |^ n)) = (p `1 ) - (W-bound C) by A3, Lm2;
A6: (W-bound C) + ((p `1 ) - (W-bound C)) = p `1 ;
(((E-bound C) - (W-bound C)) / (2 |^ n)) * (I - 1) > (((E-bound C) - (W-bound C)) / (2 |^ n)) * ((((p `1 ) - (W-bound C)) / ((E-bound C) - (W-bound C))) * (2 |^ n)) by A2, A4, XREAL_1:70;
hence p `1 < (W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (I - 1)) by A5, A6, XREAL_1:8; :: thesis: verum