let x, y, p, q be real number ; :: thesis: for n being Nat
for e1, e2, e3, e4, e5, e6 being Point of (Euclid n)
for p1, p2, p3, p4 being Point of (TOP-REAL n) st e1 = p1 & e2 = p2 & e3 = p3 & e4 = p4 & e5 = (x * p1) + (y * p3) & e6 = (x * p2) + (y * p4) & dist (e1,e2) < p & dist (e3,e4) < q & x <> 0 & y <> 0 holds
dist (e5,e6) < ((abs x) * p) + ((abs y) * q)
let n be Nat; :: thesis: for e1, e2, e3, e4, e5, e6 being Point of (Euclid n)
for p1, p2, p3, p4 being Point of (TOP-REAL n) st e1 = p1 & e2 = p2 & e3 = p3 & e4 = p4 & e5 = (x * p1) + (y * p3) & e6 = (x * p2) + (y * p4) & dist (e1,e2) < p & dist (e3,e4) < q & x <> 0 & y <> 0 holds
dist (e5,e6) < ((abs x) * p) + ((abs y) * q)
let e1, e2, e3, e4, e5, e6 be Point of (Euclid n); :: thesis: for p1, p2, p3, p4 being Point of (TOP-REAL n) st e1 = p1 & e2 = p2 & e3 = p3 & e4 = p4 & e5 = (x * p1) + (y * p3) & e6 = (x * p2) + (y * p4) & dist (e1,e2) < p & dist (e3,e4) < q & x <> 0 & y <> 0 holds
dist (e5,e6) < ((abs x) * p) + ((abs y) * q)
let p1, p2, p3, p4 be Point of (TOP-REAL n); :: thesis: ( e1 = p1 & e2 = p2 & e3 = p3 & e4 = p4 & e5 = (x * p1) + (y * p3) & e6 = (x * p2) + (y * p4) & dist (e1,e2) < p & dist (e3,e4) < q & x <> 0 & y <> 0 implies dist (e5,e6) < ((abs x) * p) + ((abs y) * q) )
assume that
A1: e1 = p1 and
A2: e2 = p2 and
A3: e3 = p3 and
A4: e4 = p4 and
A5: e5 = (x * p1) + (y * p3) and
A6: e6 = (x * p2) + (y * p4) and
A7: dist (e1,e2) < p and
A8: dist (e3,e4) < q and
A9: x <> 0 and
A10: y <> 0 ; :: thesis: dist (e5,e6) < ((abs x) * p) + ((abs y) * q)
reconsider f1 = e1, f2 = e2, f3 = e3, f4 = e4, f5 = e5, f6 = e6 as Element of REAL n by A1, A2, A3, A4, A5, A6, EUCLID:22;
A11: ( x * f2 = x * p2 & y * f4 = y * p4 ) by A2, A4, EUCLID:65;
( x * f1 = x * p1 & y * f3 = y * p3 ) by A1, A3, EUCLID:65;
then A12: f5 = (x * f1) + (y * f3) by A5, EUCLID:64;
A13: 0 < abs y by A10, COMPLEX1:47;
A14: n in NAT by ORDINAL1:def 12;
then dist (e3,e4) = |.(f3 - f4).| by SPPOL_1:5;
then A15: (abs y) * |.(f3 - f4).| < (abs y) * q by A8, A13, XREAL_1:68;
A16: 0 < abs x by A9, COMPLEX1:47;
dist (e1,e2) = |.(f1 - f2).| by A14, SPPOL_1:5;
then (abs x) * |.(f1 - f2).| < (abs x) * p by A7, A16, XREAL_1:68;
then A17: ((abs x) * |.(f1 - f2).|) + ((abs y) * |.(f3 - f4).|) < ((abs x) * p) + ((abs y) * q) by A15, XREAL_1:8;
|.((x * (f1 - f2)) + (y * (f3 - f4))).| <= |.(x * (f1 - f2)).| + |.(y * (f3 - f4)).| by EUCLID:12;
then |.((x * (f1 - f2)) + (y * (f3 - f4))).| <= |.(x * (f1 - f2)).| + ((abs y) * |.(f3 - f4).|) by EUCLID:11;
then A18: |.((x * (f1 - f2)) + (y * (f3 - f4))).| <= ((abs x) * |.(f1 - f2).|) + ((abs y) * |.(f3 - f4).|) by EUCLID:11;
dist (e5,e6) = |.(f5 - f6).| by A14, SPPOL_1:5
.= |.(((x * f1) + (y * f3)) - ((x * f2) + (y * f4))).| by A6, A12, A11, EUCLID:64
.= |.(((x * f1) - (x * f2)) + ((y * f3) - (y * f4))).| by Th9
.= |.((x * (f1 - f2)) + ((y * f3) - (y * f4))).| by Th7
.= |.((x * (f1 - f2)) + (y * (f3 - f4))).| by Th7 ;
hence dist (e5,e6) < ((abs x) * p) + ((abs y) * q) by A18, A17, XXREAL_0:2; :: thesis: verum