let a, b be Real; for r being positive Real
for C being Subset of (Euclid 2) st C = circle (a,b,r) holds
diameter C = 2 * r
let r be positive Real; for C being Subset of (Euclid 2) st C = circle (a,b,r) holds
diameter C = 2 * r
let C be Subset of (Euclid 2); ( C = circle (a,b,r) implies diameter C = 2 * r )
assume A1:
C = circle (a,b,r)
; diameter C = 2 * r
A2:
circle (a,b,r) = { p where p is Point of (TOP-REAL 2) : |.(p - |[a,b]|).| = r }
by JGRAPH_6:def 5;
A3:
for x, y being Point of (Euclid 2) st x in C & y in C holds
dist (x,y) <= 2 * r
proof
let x,
y be
Point of
(Euclid 2);
( x in C & y in C implies dist (x,y) <= 2 * r )
assume that A4:
x in C
and A5:
y in C
;
dist (x,y) <= 2 * r
consider JA being
Point of
(TOP-REAL 2) such that A6:
x = JA
and A7:
|.(JA - |[a,b]|).| = r
by A1, A4, A2;
consider JB being
Point of
(TOP-REAL 2) such that A8:
y = JB
and A9:
|.(JB - |[a,b]|).| = r
by A1, A5, A2;
reconsider KA =
JA,
KB =
JB as
Element of
REAL 2
by EUCLID:22;
reconsider O =
|[a,b]| as
Element of
REAL 2
by EUCLID:22;
reconsider O2 =
|[a,b]| as
Point of
(Euclid 2) by EUCLID:67;
A10:
dist (
x,
y)
<= (dist (x,O2)) + (dist (y,O2))
by METRIC_1:4;
dist (
y,
O2)
= |.(KB - O).|
by A8, SPPOL_1:5;
then
dist (
x,
y)
<= |.(KA - O).| + |.(KB - O).|
by A10, A6, SPPOL_1:5;
hence
dist (
x,
y)
<= 2
* r
by A7, A9;
verum
end;
A12:
C is bounded
by A1, JORDAN2C:11;
for s being Real st ( for x, y being Point of (Euclid 2) st x in C & y in C holds
dist (x,y) <= s ) holds
2 * r <= s
proof
let s be
Real;
( ( for x, y being Point of (Euclid 2) st x in C & y in C holds
dist (x,y) <= s ) implies 2 * r <= s )
assume A13:
for
x,
y being
Point of
(Euclid 2) st
x in C &
y in C holds
dist (
x,
y)
<= s
;
2 * r <= s
assume A14:
s < 2
* r
;
contradiction
set A1 =
|[(a + r),b]|;
set B1 =
|[(a - r),b]|;
A15:
|[(a + r),b]| - |[a,b]| =
|[((a + r) - a),(b - b)]|
by EUCLID:62
.=
|[r,0]|
;
A16:
|[(a - r),b]| - |[a,b]| =
|[((a - r) - a),(b - b)]|
by EUCLID:62
.=
|[(- r),0]|
;
A17:
(r ^2) + (0 ^2) =
(r ^2) + (0 * 0)
by SQUARE_1:def 1
.=
r ^2
;
(
Re (r + (0 * <i>)) = r &
Im (r + (0 * <i>)) = 0 )
by COMPLEX1:12;
then |.(cpx2euc (r + (0 * <i>))).| =
sqrt (r ^2)
by A17, EUCLID_3:24
.=
r
by SQUARE_1:22
;
then A18:
|.(|[(a + r),b]| - |[a,b]|).| = r
by A15, EUCLID_3:5;
then A19:
|[(a + r),b]| in circle (
a,
b,
r)
by A2;
A20:
|[(a + r),b]| in C
by A18, A1, A2;
A21:
((- r) ^2) + (0 ^2) =
((- r) ^2) + (0 * 0)
by SQUARE_1:def 1
.=
r ^2
by SQUARE_1:3
;
(
Re ((- r) + (0 * <i>)) = - r &
Im ((- r) + (0 * <i>)) = 0 )
by COMPLEX1:12;
then |.(cpx2euc ((- r) + (0 * <i>))).| =
sqrt (r ^2)
by A21, EUCLID_3:24
.=
r
by SQUARE_1:22
;
then A22:
|.|[(- r),0]|.| = r
by EUCLID_3:5;
then A23:
|[(a - r),b]| in circle (
a,
b,
r)
by A2, A16;
A24:
|[(a - r),b]| in C
by A1, A2, A22, A16;
A25:
|[a,b]| in LSeg (
|[(a + r),b]|,
|[(a - r),b]|)
proof
|[(a + r),b]| + |[(a - r),b]| = |[((a + r) + (a - r)),(b + b)]|
by EUCLID:56;
then (1 / 2) * (|[(a + r),b]| + |[(a - r),b]|) =
|[((1 / 2) * (2 * a)),((1 / 2) * (2 * b))]|
by EUCLID:58
.=
|[a,b]|
;
hence
|[a,b]| in LSeg (
|[(a + r),b]|,
|[(a - r),b]|)
by RLTOPSP1:69;
verum
end;
A26:
|[(a + r),b]| <> |[(a - r),b]|
A27:
|[(a + r),b]| <> |[a,b]|
|[(a + r),b]|,
|[(a - r),b]|,
|[a,b]| are_mutually_distinct
then A28:
|.(|[(a + r),b]| - |[(a - r),b]|).| = 2
* r
by A19, A23, A25, Thm38;
reconsider a1 =
|[(a + r),b]|,
b1 =
|[(a - r),b]| as
Point of
(Euclid 2) by EUCLID:67;
reconsider A2 =
|[(a + r),b]|,
B2 =
|[(a - r),b]| as
Element of
REAL 2
by EUCLID:22;
Euclid 2
= MetrStruct(#
(REAL 2),
(Pitag_dist 2) #)
by EUCLID:def 7;
then dist (
a1,
b1) =
(Pitag_dist 2) . (
|[(a + r),b]|,
|[(a - r),b]|)
by METRIC_1:def 1
.=
|.(A2 - B2).|
by EUCLID:def 6
.=
2
* r
by A28
;
hence
contradiction
by A14, A20, A24, A13;
verum
end;
hence
diameter C = 2 * r
by A3, A12, A1, TBSP_1:def 8; verum