let a, b be Real; :: thesis: for g being positive Real holds
( (a ^2) + (b ^2) = g ^2 iff |[a,b]| in circle (0,0,g) )
let g be positive Real; :: thesis: ( (a ^2) + (b ^2) = g ^2 iff |[a,b]| in circle (0,0,g) )
hereby :: thesis: ( |[a,b]| in circle (0,0,g) implies (a ^2) + (b ^2) = g ^2 )
assume A1: (a ^2) + (b ^2) = g ^2 ; :: thesis: |[a,b]| in circle (0,0,g)
reconsider p = |[a,b]| as Point of (TOP-REAL 2) ;
|.(p - |[0,0]|).| = g
proof
A2: |.(p - |[0,0]|).| ^2 = |.|[(a - 0),(b - 0)]|.| ^2 by EUCLID:62
.= g ^2 by A1, TOPGEN_5:9 ;
- g < 0 ;
hence |.(p - |[0,0]|).| = g by A2, SQUARE_1:40; :: thesis: verum
end;
hence |[a,b]| in circle (0,0,g) ; :: thesis: verum
end;
assume A3: |[a,b]| in circle (0,0,g) ; :: thesis: (a ^2) + (b ^2) = g ^2
thus (a ^2) + (b ^2) = |.|[(a - 0),(b - 0)]|.| ^2 by TOPGEN_5:9
.= |.(|[a,b]| - |[0,0]|).| ^2 by EUCLID:62
.= g ^2 by A3, TOPREAL9:43 ; :: thesis: verum