let q be Point of (TOP-REAL 2); for r being Real holds dist (|[0,0]|,(r * q)) = |.r.| * (dist (|[0,0]|,q))
let r be Real; dist (|[0,0]|,(r * q)) = |.r.| * (dist (|[0,0]|,q))
A1:
( r ^2 >= 0 & (q `1) ^2 >= 0 )
by XREAL_1:63;
A2:
(q `2) ^2 >= 0
by XREAL_1:63;
A3:
( |[0,0]| `1 = 0 & |[0,0]| `2 = 0 )
by EUCLID:52;
then A4: dist (|[0,0]|,q) =
sqrt (((0 - (q `1)) ^2) + ((0 - (q `2)) ^2))
by TOPREAL6:92
.=
sqrt (((q `1) ^2) + ((q `2) ^2))
;
thus dist (|[0,0]|,(r * q)) =
sqrt (((0 - ((r * q) `1)) ^2) + ((0 - ((r * q) `2)) ^2))
by A3, TOPREAL6:92
.=
sqrt ((((r * q) `1) ^2) + ((- ((r * q) `2)) ^2))
.=
sqrt (((r * (q `1)) ^2) + (((r * q) `2) ^2))
by TOPREAL3:4
.=
sqrt (((r ^2) * ((q `1) ^2)) + ((r * (q `2)) ^2))
by TOPREAL3:4
.=
sqrt ((r ^2) * (((q `1) ^2) + ((q `2) ^2)))
.=
(sqrt (r ^2)) * (sqrt (((q `1) ^2) + ((q `2) ^2)))
by A1, A2, SQUARE_1:29
.=
|.r.| * (dist (|[0,0]|,q))
by A4, COMPLEX1:72
; verum