let n be Nat; :: thesis: for r being Real

for e, e1 being Point of (Euclid n) st n <> 0 & e1 in OpenHypercube (e,r) holds

dist (e1,e) < r * (sqrt n)

let r be Real; :: thesis: for e, e1 being Point of (Euclid n) st n <> 0 & e1 in OpenHypercube (e,r) holds

dist (e1,e) < r * (sqrt n)

let e, e1 be Point of (Euclid n); :: thesis: ( n <> 0 & e1 in OpenHypercube (e,r) implies dist (e1,e) < r * (sqrt n) )

assume that

A1: n <> 0 and

A2: e1 in OpenHypercube (e,r) ; :: thesis: dist (e1,e) < r * (sqrt n)

A3: dist (e1,e) = |.(e1 - e).| by EUCLID:def 6;

0 <= Sum (sqr (e1 - e)) by RVSUM_1:86;

then A4: sqrt (Sum (sqr (e1 - e))) < sqrt (n * (r ^2)) by A1, A2, Th15, SQUARE_1:27;

0 <= r by A1, A2;

then sqrt (r ^2) = r by SQUARE_1:22;

hence dist (e1,e) < r * (sqrt n) by A3, A4, SQUARE_1:29; :: thesis: verum

for e, e1 being Point of (Euclid n) st n <> 0 & e1 in OpenHypercube (e,r) holds

dist (e1,e) < r * (sqrt n)

let r be Real; :: thesis: for e, e1 being Point of (Euclid n) st n <> 0 & e1 in OpenHypercube (e,r) holds

dist (e1,e) < r * (sqrt n)

let e, e1 be Point of (Euclid n); :: thesis: ( n <> 0 & e1 in OpenHypercube (e,r) implies dist (e1,e) < r * (sqrt n) )

assume that

A1: n <> 0 and

A2: e1 in OpenHypercube (e,r) ; :: thesis: dist (e1,e) < r * (sqrt n)

A3: dist (e1,e) = |.(e1 - e).| by EUCLID:def 6;

0 <= Sum (sqr (e1 - e)) by RVSUM_1:86;

then A4: sqrt (Sum (sqr (e1 - e))) < sqrt (n * (r ^2)) by A1, A2, Th15, SQUARE_1:27;

0 <= r by A1, A2;

then sqrt (r ^2) = r by SQUARE_1:22;

hence dist (e1,e) < r * (sqrt n) by A3, A4, SQUARE_1:29; :: thesis: verum