let a, b be Real; :: thesis: 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; :: thesis: 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); :: thesis: ( C = circle (a,b,r) implies diameter C = 2 * r )
assume A1: C = circle (a,b,r) ; :: thesis: 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); :: thesis: ( x in C & y in C implies dist (x,y) <= 2 * r )
assume that
A4: x in C and
A5: y in C ; :: thesis: 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; :: thesis: 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; :: thesis: ( ( 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 ; :: thesis: 2 * r <= s
assume A14: s < 2 * r ; :: thesis: 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; :: thesis: verum

end;

A26: |[(a + r),b]| <> |[(a - r),b]|

proof

assume |[(a + r),b]| = |[(a - r),b]| ; :: thesis: contradiction
then ( a + r = a - r & b = b ) by SPPOL_2:1;
then r = 0 ;
hence contradiction ; :: thesis: verum

end;

A27: |[(a + r),b]| <> |[a,b]|

proof

assume |[(a + r),b]| = |[a,b]| ; :: thesis: contradiction
then ( a + r = a & b = b ) by SPPOL_2:1;
then r = 0 ;
hence contradiction ; :: thesis: verum

end;

|[(a + r),b]|,|[(a - r),b]|,|[a,b]| are_mutually_distinct

proof

|[(a - r),b]| <> |[a,b]|

proof

assume |[(a - r),b]| = |[a,b]| ; :: thesis: contradiction
then ( a - r = a & b = b ) by SPPOL_2:1;
then - r = 0 ;
hence contradiction ; :: thesis: verum

end;

hence |[(a + r),b]|,|[(a - r),b]|,|[a,b]| are_mutually_distinct by A26, A27; :: thesis: verum

end;

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; :: thesis: verum

end;

hence diameter C = 2 * r by A3, A12, A1, TBSP_1:def 8; :: thesis: verum