let C be Simple_closed_curve; :: thesis: for n being Element of 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
(S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (J - 2)) <= p `2
let n be Element of 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
(S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (J - 2)) <= p `2
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
(S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (J - 2)) <= p `2
set E = N-bound C;
set W = S-bound C;
set EW = (N-bound C) - (S-bound C);
set PW = (p `2 ) - (S-bound C);
set KI = [\((((p `2 ) - (S-bound C)) / ((N-bound C) - (S-bound C))) * (2 |^ n))/];
let I be Integer; :: thesis: ( I = [\(((((p `2 ) - (S-bound C)) / ((N-bound C) - (S-bound C))) * (2 |^ n)) + 2)/] implies (S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (I - 2)) <= p `2 )
assume I = [\(((((p `2 ) - (S-bound C)) / ((N-bound C) - (S-bound C))) * (2 |^ n)) + 2)/] ; :: thesis: (S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (I - 2)) <= p `2
then A1: I - 2 = [\((((p `2 ) - (S-bound C)) / ((N-bound C) - (S-bound C))) * (2 |^ n))/] by Lm1;
N-bound C > S-bound C by TOPREAL5:22;
then A2: ( (N-bound C) - (S-bound C) > 0 & 2 |^ n > 0 ) by NEWTON:102, XREAL_1:52;
A4: (((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 A2, Lm2;
A5: (S-bound C) + ((p `2 ) - (S-bound C)) = p `2 ;
[\((((p `2 ) - (S-bound C)) / ((N-bound C) - (S-bound C))) * (2 |^ n))/] <= (((p `2 ) - (S-bound C)) / ((N-bound C) - (S-bound C))) * (2 |^ n) by INT_1:def 4;
then (((N-bound C) - (S-bound C)) / (2 |^ n)) * [\((((p `2 ) - (S-bound C)) / ((N-bound C) - (S-bound C))) * (2 |^ n))/] <= (((N-bound C) - (S-bound C)) / (2 |^ n)) * ((((p `2 ) - (S-bound C)) / ((N-bound C) - (S-bound C))) * (2 |^ n)) by A2, XREAL_1:66;
hence (S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (I - 2)) <= p `2 by A1, A4, A5, XREAL_1:8; :: thesis: verum