euclid_2.miz



    begin

    reserve i,n for Nat,

x,y,a for Real,

v for Element of (n -tuples_on REAL ),

p,p1,p2,p3,q,q1,q2 for Point of ( TOP-REAL n);

    theorem :: EUCLID_2:1

    

     Th1: (( mlt (v,( 0* n))) . i) = 0

    proof

      

       A1: ( 0* n) = (n |-> 0 qua set) by EUCLID:def 4;

      set v0 = (( 0* n) . i);

      

       A2: ( dom ( 0* n)) = ( Seg n) by FINSEQ_2: 124;

      i in ( Seg n) or not i in ( Seg n);

      then

       A3: v0 = 0 by A1, A2, FUNCOP_1: 7, FUNCT_1:def 2;

      (( mlt (v,( 0* n))) . i) = ((v . i) * v0) by RVSUM_1: 60

      .= 0 by A3;

      hence thesis;

    end;

    theorem :: EUCLID_2:2

    

     Th2: ( mlt (v,( 0* n))) = ( 0* n)

    proof

      ( len ( 0* n)) = n by CARD_1:def 7;

      then

      reconsider z = ( 0* n) as Element of (n -tuples_on REAL ) by FINSEQ_2: 92;

      

       A1: ( len ( 0* n)) = n by CARD_1:def 7;

      

       A2: for j be Nat st j in ( dom ( 0* n)) holds (( mlt (v,( 0* n))) . j) = (( 0* n) . j)

      proof

        let j be Nat;

        assume j in ( dom ( 0* n));

        

        thus (( mlt (v,( 0* n))) . j) = 0 by Th1

        .= ((n |-> 0 ) . j)

        .= (( 0* n) . j) by EUCLID:def 4;

      end;

      ( len ( mlt (v,z))) = n by CARD_1:def 7;

      then ( dom ( mlt (v,( 0* n)))) = ( dom ( 0* n)) by A1, FINSEQ_3: 29;

      hence thesis by A2, FINSEQ_1: 13;

    end;

    begin

    theorem :: EUCLID_2:3

    for y1,y2 be real-valued FinSequence, x1,x2 be Element of ( REAL n) st x1 = y1 & x2 = y2 holds |(y1, y2)| = ((1 / 4) * (( |.(x1 + x2).| ^2 ) - ( |.(x1 - x2).| ^2 )))

    proof

      let y1,y2 be real-valued FinSequence, x1,x2 be Element of ( REAL n);

      assume

       A1: x1 = y1 & x2 = y2;

      reconsider w1 = x1, w2 = x2 as Element of (n -tuples_on REAL ) by EUCLID:def 1;

      set v1 = ( sqr (x1 + x2)), v2 = ( sqr (x1 - x2));

      set z1 = (x1 + x2), z2 = (x1 - x2);

      

       A2: ((1 / 4) * (( |.(x1 + x2).| ^2 ) - ( |.(x1 - x2).| ^2 ))) = ((1 / 4) * ((( sqrt ( Sum ( sqr z1))) ^2 ) - ( |.z2.| ^2 ))) by EUCLID:def 5

      .= ((1 / 4) * ((( sqrt ( Sum ( sqr z1))) ^2 ) - (( sqrt ( Sum ( sqr z2))) ^2 ))) by EUCLID:def 5;

      ( Sum ( sqr (x1 + x2))) >= 0 by RVSUM_1: 86;

      then

       A3: (( sqrt ( Sum ( sqr (x1 + x2)))) ^2 ) = ( Sum ( sqr (x1 + x2))) by SQUARE_1:def 2;

      

       A4: (( Sum ( sqr (x1 + x2))) - ( Sum ( sqr (x1 - x2)))) = ( Sum (v1 - v2)) by RVSUM_1: 90;

      ( Sum ( sqr (x1 - x2))) >= 0 by RVSUM_1: 86;

      then

       A5: (( sqrt ( Sum ( sqr (x1 - x2)))) ^2 ) = ( Sum ( sqr (x1 - x2))) by SQUARE_1:def 2;

      

       A6: (((2 * ( mlt (w1,w2))) + ( sqr w2)) + (2 * ( mlt (w1,w2)))) = ((2 * ( mlt (w1,w2))) + ((2 * ( mlt (w1,w2))) + ( sqr w2)))

      .= (((2 * ( mlt (w1,w2))) + (2 * ( mlt (w1,w2)))) + ( sqr w2)) by FINSEQOP: 28;

      

       A7: (( sqr w1) + ((2 * ( mlt (w1,w2))) + ( sqr w2))) = (((2 * ( mlt (w1,w2))) + ( sqr w2)) + ( sqr w1));

      (v1 - v2) = (((( sqr w1) + (2 * ( mlt (w1,w2)))) + ( sqr w2)) - ( sqr (w1 - w2))) by RVSUM_1: 68

      .= (((( sqr w1) + (2 * ( mlt (w1,w2)))) + ( sqr w2)) - ((( sqr w1) - (2 * ( mlt (w1,w2)))) + ( sqr w2))) by RVSUM_1: 69

      .= ((((2 * ( mlt (w1,w2))) + ( sqr w2)) + ( sqr w1)) - ((( sqr w1) - (2 * ( mlt (w1,w2)))) + ( sqr w2))) by A7, FINSEQOP: 28

      .= (((((2 * ( mlt (w1,w2))) + ( sqr w2)) + ( sqr w1)) - (( sqr w1) - (2 * ( mlt (w1,w2))))) - ( sqr w2)) by RVSUM_1: 39

      .= ((((((2 * ( mlt (w1,w2))) + ( sqr w2)) + ( sqr w1)) - ( sqr w1)) + (2 * ( mlt (w1,w2)))) - ( sqr w2)) by RVSUM_1: 41

      .= ((((2 * ( mlt (w1,w2))) + ( sqr w2)) + (2 * ( mlt (w1,w2)))) - ( sqr w2)) by RVSUM_1: 42

      .= ((2 * ( mlt (w1,w2))) + (2 * ( mlt (w1,w2)))) by A6, RVSUM_1: 42

      .= ((2 + 2) * ( mlt (w1,w2))) by RVSUM_1: 50

      .= (4 * ( mlt (w1,w2)));

      

      then ((1 / 4) * (( |.(x1 + x2).| ^2 ) - ( |.(x1 - x2).| ^2 ))) = ((1 / 4) * (4 * ( Sum ( mlt (w1,w2))))) by A2, A3, A5, A4, RVSUM_1: 87

      .= ( Sum ( mlt (w1,w2)));

      hence thesis by A1;

    end;

     Lm1:

    now

      let x be real-valued FinSequence;

      ( rng x) c= REAL ;

      hence x is FinSequence of REAL by FINSEQ_1:def 4;

    end;

    theorem :: EUCLID_2:4

    

     Th4: for x be real-valued FinSequence holds ( |.x.| ^2 ) = |(x, x)|

    proof

      let x be real-valued FinSequence;

      

       A1: 0 <= |(x, x)| by RVSUM_1: 119;

      ( |.x.| ^2 ) = (( sqrt ( Sum ( sqr x))) ^2 ) by EUCLID:def 5

      .= |(x, x)| by A1, SQUARE_1:def 2;

      hence thesis;

    end;

    theorem :: EUCLID_2:5

    

     Th5: for x be real-valued FinSequence holds |.x.| = ( sqrt |(x, x)|)

    proof

      let x be real-valued FinSequence;

       |.x.| = ( sqrt ( |.x.| ^2 )) by EUCLID: 9, SQUARE_1: 22

      .= ( sqrt |(x, x)|) by Th4;

      hence thesis;

    end;

    ::$Canceled

    theorem :: EUCLID_2:7

    

     Th6: for x be real-valued FinSequence holds |(x, x)| = 0 iff x = ( 0* ( len x))

    proof

      let x be real-valued FinSequence;

      thus |(x, x)| = 0 implies x = ( 0* ( len x))

      proof

        x is FinSequence of REAL by Lm1;

        then

        reconsider y = x as Element of ( REAL ( len x)) by EUCLID: 76;

        assume |(x, x)| = 0 ;

        then ( |.x.| ^2 ) = 0 by Th4;

        then |.x.| = 0 by XCMPLX_1: 6;

        then y = ( 0* ( len x)) by EUCLID: 8;

        hence thesis;

      end;

      assume x = ( 0* ( len x));

      then |.x.| = 0 by EUCLID: 7;

      then |(x, x)| = ( 0 ^2 ) by Th4;

      hence thesis;

    end;

    theorem :: EUCLID_2:8

    for x be real-valued FinSequence holds |(x, x)| = 0 iff |.x.| = 0

    proof

      let x be real-valued FinSequence;

      

       A1: |(x, x)| = ( 0 ^2 ) implies |.x.| = 0

      proof

        assume |(x, x)| = ( 0 ^2 );

        then x = ( 0* ( len x)) by Th6;

        hence thesis by EUCLID: 7;

      end;

       |.x.| = 0 implies |(x, x)| = ( 0 ^2 ) by Th4;

      hence thesis by A1;

    end;

    theorem :: EUCLID_2:9

    

     Th8: for x be real-valued FinSequence holds |(x, ( 0* ( len x)))| = 0

    proof

      let x be real-valued FinSequence;

      set n = ( len x);

      x is FinSequence of REAL by Lm1;

      then

      reconsider p1 = x as Element of (n -tuples_on REAL ) by FINSEQ_2: 92;

      

       A1: ( 0* n) = (n |-> 0 ) by EUCLID:def 4;

       |(x, ( 0* n))| = ( Sum ( mlt (p1,( 0* n))))

      .= ( Sum ( 0* n)) by Th2

      .= 0 by A1, RVSUM_1: 81;

      hence thesis;

    end;

    theorem :: EUCLID_2:10

    for x be real-valued FinSequence holds |(( 0* ( len x)), x)| = 0 by Th8;

    theorem :: EUCLID_2:11

    

     Th10: for x,y be real-valued FinSequence st ( len x) = ( len y) holds ( |.(x + y).| ^2 ) = ((( |.x.| ^2 ) + (2 * |(y, x)|)) + ( |.y.| ^2 ))

    proof

      let x,y be real-valued FinSequence;

      assume

       A1: ( len x) = ( len y);

      ( |.(x + y).| ^2 ) = |((x + y), (x + y))| by Th4

      .= (( |(x, x)| + (2 * |(x, y)|)) + |(y, y)|) by A1, RVSUM_1: 128

      .= ((( |.x.| ^2 ) + (2 * |(y, x)|)) + |(y, y)|) by Th4

      .= ((( |.x.| ^2 ) + (2 * |(y, x)|)) + ( |.y.| ^2 )) by Th4;

      hence thesis;

    end;

    theorem :: EUCLID_2:12

    

     Th11: for x,y be real-valued FinSequence st ( len x) = ( len y) holds ( |.(x - y).| ^2 ) = ((( |.x.| ^2 ) - (2 * |(y, x)|)) + ( |.y.| ^2 ))

    proof

      let x,y be real-valued FinSequence;

      assume

       A1: ( len x) = ( len y);

      ( |.(x - y).| ^2 ) = |((x - y), (x - y))| by Th4

      .= (( |(x, x)| - (2 * |(x, y)|)) + |(y, y)|) by A1, RVSUM_1: 129

      .= ((( |.x.| ^2 ) - (2 * |(y, x)|)) + |(y, y)|) by Th4

      .= ((( |.x.| ^2 ) - (2 * |(y, x)|)) + ( |.y.| ^2 )) by Th4;

      hence thesis;

    end;

    theorem :: EUCLID_2:13

    for x,y be real-valued FinSequence st ( len x) = ( len y) holds (( |.(x + y).| ^2 ) + ( |.(x - y).| ^2 )) = (2 * (( |.x.| ^2 ) + ( |.y.| ^2 )))

    proof

      let x,y be real-valued FinSequence;

      assume

       A1: ( len x) = ( len y);

      

      then (( |.(x + y).| ^2 ) + ( |.(x - y).| ^2 )) = (((( |.x.| ^2 ) + (2 * |(y, x)|)) + ( |.y.| ^2 )) + ( |.(x - y).| ^2 )) by Th10

      .= (((( |.x.| ^2 ) + (2 * |(x, y)|)) + ( |.y.| ^2 )) + ((( |.x.| ^2 ) - (2 * |(y, x)|)) + ( |.y.| ^2 ))) by A1, Th11

      .= (2 * (( |.x.| ^2 ) + ( |.y.| ^2 )));

      hence thesis;

    end;

    theorem :: EUCLID_2:14

    for x,y be real-valued FinSequence st ( len x) = ( len y) holds (( |.(x + y).| ^2 ) - ( |.(x - y).| ^2 )) = (4 * |(x, y)|)

    proof

      let x,y be real-valued FinSequence;

      assume

       A1: ( len x) = ( len y);

      

      then (( |.(x + y).| ^2 ) - ( |.(x - y).| ^2 )) = (((( |.x.| ^2 ) + (2 * |(y, x)|)) + ( |.y.| ^2 )) - ( |.(x - y).| ^2 )) by Th10

      .= (((( |.x.| ^2 ) + (2 * |(x, y)|)) + ( |.y.| ^2 )) - ((( |.x.| ^2 ) - (2 * |(y, x)|)) + ( |.y.| ^2 ))) by A1, Th11

      .= (4 * |(x, y)|);

      hence thesis;

    end;

    theorem :: EUCLID_2:15

    

     Th14: for x,y be real-valued FinSequence st ( len x) = ( len y) holds |. |(x, y)|.| <= ( |.x.| * |.y.|)

    proof

      let x,y be real-valued FinSequence;

      assume

       A1: ( len x) = ( len y);

      

       A2: x = ( 0* ( len x)) implies |. |(x, y)|.| <= (( sqrt |(x, x)|) * ( sqrt |(y, y)|))

      proof

        assume x = ( 0* ( len x));

        then |(x, y)| = 0 & |(x, x)| = 0 by A1, Th8;

        hence thesis by ABSVALUE: 2, SQUARE_1: 17;

      end;

      

       A3: x <> ( 0* ( len x)) implies |. |(x, y)|.| <= (( sqrt |(x, x)|) * ( sqrt |(y, y)|))

      proof

        

         A4: for t be Real holds ((( |(x, x)| * (t ^2 )) + ((2 * |(x, y)|) * t)) + |(y, y)|) >= 0

        proof

          let t be Real;

          set s = (t ^2 );

          

           A5: ( len (t * x)) = ( len x) by RVSUM_1: 117;

           |(((t * x) + y), ((t * x) + y))| >= 0 by RVSUM_1: 119;

          then (( |((t * x), (t * x))| + (2 * |((t * x), y)|)) + |(y, y)|) >= 0 by A1, A5, RVSUM_1: 128;

          then (((t * |((t * x), x)|) + (2 * |((t * x), y)|)) + |(y, y)|) >= 0 by A5, RVSUM_1: 121;

          then (((t * (t * |(x, x)|)) + (2 * |((t * x), y)|)) + |(y, y)|) >= 0 by A1, RVSUM_1: 121;

          then ((( |(x, x)| * s) + (2 * ( |(x, y)| * t))) + |(y, y)|) >= 0 by A1, RVSUM_1: 121;

          hence thesis;

        end;

        set w = |. |(x, y)|.|, u = |(x, y)|;

        

         A6: |(x, x)| >= 0 by RVSUM_1: 119;

        assume x <> ( 0* ( len x));

        then |(x, x)| <> 0 by Th6;

        then |(x, x)| > 0 by A6, XXREAL_0: 1;

        then ( delta ( |(x, x)|,(2 * |(x, y)|), |(y, y)|)) <= 0 by A4, QUIN_1: 10;

        then (((2 * u) ^2 ) - ((4 * |(x, x)|) * |(y, y)|)) <= 0 by QUIN_1:def 1;

        then (4 * ((u ^2 ) - ( |(x, x)| * |(y, y)|))) <= 0 ;

        then (( |(x, y)| ^2 ) - ( |(x, x)| * |(y, y)|)) <= ( 0 / 4) by XREAL_1: 77;

        then ( |(x, y)| ^2 ) <= ( |(x, x)| * |(y, y)|) by XREAL_1: 50;

        then 0 <= (w ^2 ) & ( |. |(x, y)|.| ^2 ) <= ( |(x, x)| * |(y, y)|) by COMPLEX1: 75, XREAL_1: 63;

        then ( sqrt ( |. |(x, y)|.| ^2 )) <= ( sqrt ( |(x, x)| * |(y, y)|)) by SQUARE_1: 26;

        then

         A7: |. |(x, y)|.| <= ( sqrt ( |(x, x)| * |(y, y)|)) by COMPLEX1: 46, SQUARE_1: 22;

         |(y, y)| >= 0 by RVSUM_1: 119;

        hence thesis by A6, A7, SQUARE_1: 29;

      end;

      ( sqrt |(x, x)|) = |.x.| by Th5;

      hence thesis by A2, A3, Th5;

    end;

    theorem :: EUCLID_2:16

    

     Th15: for x,y be real-valued FinSequence st ( len x) = ( len y) holds |.(x + y).| <= ( |.x.| + |.y.|)

    proof

      let x,y be real-valued FinSequence;

      assume

       A1: ( len x) = ( len y);

      then |(x, y)| <= |. |(x, y)|.| & |. |(x, y)|.| <= ( |.x.| * |.y.|) by Th14, ABSVALUE: 4;

      then |(x, y)| <= ( |.x.| * |.y.|) by XXREAL_0: 2;

      then (2 * |(x, y)|) <= (2 * ( |.x.| * |.y.|)) by XREAL_1: 64;

      then

       A2: (( |.x.| ^2 ) + (2 * |(x, y)|)) <= (( |.x.| ^2 ) + (2 * ( |.x.| * |.y.|))) by XREAL_1: 7;

      ( |.(x + y).| ^2 ) = ((( |.x.| ^2 ) + (2 * |(y, x)|)) + ( |.y.| ^2 )) by A1, Th10;

      then

       A3: ( |.(x + y).| ^2 ) <= ((( |.x.| ^2 ) + ((2 * |.x.|) * |.y.|)) + ( |.y.| ^2 )) by A2, XREAL_1: 7;

       0 <= ( |.(x + y).| ^2 ) by XREAL_1: 63;

      then ( sqrt ( |.(x + y).| ^2 )) <= ( sqrt (( |.x.| + |.y.|) ^2 )) by A3, SQUARE_1: 26;

      then

       A4: |.(x + y).| <= ( sqrt (( |.x.| + |.y.|) ^2 )) by EUCLID: 9, SQUARE_1: 22;

       0 <= |.x.| & 0 <= |.y.| by EUCLID: 9;

      then ( 0 + 0 ) <= ( |.x.| + |.y.|) by XREAL_1: 7;

      hence thesis by A4, SQUARE_1: 22;

    end;

    begin

    ::$Canceled

    theorem :: EUCLID_2:18

    

     Th16: |((p1 + p2), p3)| = ( |(p1, p3)| + |(p2, p3)|)

    proof

      reconsider f1 = p1, f2 = p2, f3 = p3 as FinSequence of REAL by EUCLID: 24;

      reconsider q1 = p1, q2 = p2 as Element of ( REAL n) by EUCLID: 22;

      ( len f2) = n by CARD_1:def 7;

      then

       A1: ( len f1) = ( len f2) & ( len f2) = ( len f3) by CARD_1:def 7;

      thus thesis by A1, RVSUM_1: 120;

    end;

    theorem :: EUCLID_2:19

    

     Th17: for x be Real holds |((x * p1), p2)| = (x * |(p1, p2)|)

    proof

      let x be Real;

      reconsider f1 = p1, f2 = p2 as FinSequence of REAL by EUCLID: 24;

      reconsider q1 = p1 as Element of ( REAL n) by EUCLID: 22;

      ( len f1) = n & ( len f2) = n by CARD_1:def 7;

      hence thesis by RVSUM_1: 121;

    end;

    theorem :: EUCLID_2:20

    for x be Real holds |(p1, (x * p2))| = (x * |(p1, p2)|) by Th17;

    theorem :: EUCLID_2:21

    

     Th19: |(( - p1), p2)| = ( - |(p1, p2)|)

    proof

       |(( - p1), p2)| = |((( - 1) * p1), p2)|

      .= (( - 1) * |(p1, p2)|) by Th17;

      hence thesis;

    end;

    theorem :: EUCLID_2:22

     |(p1, ( - p2))| = ( - |(p1, p2)|) by Th19;

    theorem :: EUCLID_2:23

     |(( - p1), ( - p2))| = |(p1, p2)|

    proof

       |(( - p1), ( - p2))| = ( - |(p1, ( - p2))|) by Th19

      .= ( - ( - |(p1, p2)|)) by Th19;

      hence thesis;

    end;

    theorem :: EUCLID_2:24

    

     Th22: |((p1 - p2), p3)| = ( |(p1, p3)| - |(p2, p3)|)

    proof

       |((p1 - p2), p3)| = ( |(p1, p3)| + |(( - p2), p3)|) by Th16

      .= ( |(p1, p3)| + ( - |(p2, p3)|)) by Th19;

      hence thesis;

    end;

    theorem :: EUCLID_2:25

     |(((x * p1) + (y * p2)), p3)| = ((x * |(p1, p3)|) + (y * |(p2, p3)|))

    proof

       |(((x * p1) + (y * p2)), p3)| = ( |((x * p1), p3)| + |((y * p2), p3)|) by Th16

      .= ((x * |(p1, p3)|) + |((y * p2), p3)|) by Th17

      .= ((x * |(p1, p3)|) + (y * |(p2, p3)|)) by Th17;

      hence thesis;

    end;

    theorem :: EUCLID_2:26

     |(p, (q1 + q2))| = ( |(p, q1)| + |(p, q2)|) by Th16;

    theorem :: EUCLID_2:27

     |(p, (q1 - q2))| = ( |(p, q1)| - |(p, q2)|) by Th22;

    theorem :: EUCLID_2:28

    

     Th26: |((p1 + p2), (q1 + q2))| = ((( |(p1, q1)| + |(p1, q2)|) + |(p2, q1)|) + |(p2, q2)|)

    proof

      

       A1: |((p1 + p2), q1)| = ( |(p1, q1)| + |(p2, q1)|) & |((p1 + p2), q2)| = ( |(p1, q2)| + |(p2, q2)|) by Th16;

       |((p1 + p2), (q1 + q2))| = ( |((p1 + p2), q1)| + |((p1 + p2), q2)|) by Th16

      .= ((( |(p1, q1)| + |(p1, q2)|) + |(p2, q1)|) + |(p2, q2)|) by A1;

      hence thesis;

    end;

    theorem :: EUCLID_2:29

    

     Th27: |((p1 - p2), (q1 - q2))| = ((( |(p1, q1)| - |(p1, q2)|) - |(p2, q1)|) + |(p2, q2)|)

    proof

      

       A1: |(p1, (q1 - q2))| = ( |(p1, q1)| - |(p1, q2)|) & |(p2, (q1 - q2))| = ( |(p2, q1)| - |(p2, q2)|) by Th22;

       |((p1 - p2), (q1 - q2))| = ( |(p1, (q1 - q2))| - |(p2, (q1 - q2))|) by Th22

      .= ((( |(p1, q1)| - |(p1, q2)|) - |(p2, q1)|) + |(p2, q2)|) by A1;

      hence thesis;

    end;

    theorem :: EUCLID_2:30

    

     Th28: |((p + q), (p + q))| = (( |(p, p)| + (2 * |(p, q)|)) + |(q, q)|)

    proof

      (( |(p, p)| + |(p, q)|) + |(p, q)|) = ( |(p, p)| + (2 * |(p, q)|));

      hence thesis by Th26;

    end;

    theorem :: EUCLID_2:31

    

     Th29: |((p - q), (p - q))| = (( |(p, p)| - (2 * |(p, q)|)) + |(q, q)|)

    proof

       |((p - q), (p - q))| = ((( |(p, p)| - |(p, q)|) - |(p, q)|) + |(q, q)|) by Th27

      .= (( |(p, p)| - (2 * |(p, q)|)) + |(q, q)|);

      hence thesis;

    end;

    theorem :: EUCLID_2:32

    

     Th30: |(p, ( 0. ( TOP-REAL n)))| = 0

    proof

      reconsider f1 = p as FinSequence of REAL by EUCLID: 24;

      ( len f1) = n by CARD_1:def 7;

      then ( 0* ( len f1)) = ( 0. ( TOP-REAL n)) by EUCLID: 70;

      hence thesis by Th8;

    end;

    theorem :: EUCLID_2:33

     |(( 0. ( TOP-REAL n)), p)| = 0 by Th30;

    theorem :: EUCLID_2:34

     |(( 0. ( TOP-REAL n)), ( 0. ( TOP-REAL n)))| = 0 by Th30;

    theorem :: EUCLID_2:35

    

     Th33: |(p, p)| >= 0 by RVSUM_1: 119;

    theorem :: EUCLID_2:36

    

     Th34: |(p, p)| = ( |.p.| ^2 ) by Th4;

    theorem :: EUCLID_2:37

    

     Th35: |.p.| = ( sqrt |(p, p)|)

    proof

       |.p.| = ( sqrt ( |.p.| ^2 )) by SQUARE_1: 22, TOPRNS_1: 25

      .= ( sqrt |(p, p)|) by Th34;

      hence thesis;

    end;

    theorem :: EUCLID_2:38

    

     Th36: 0 <= |.p.|

    proof

       |.p.| = ( sqrt |(p, p)|) & 0 <= |(p, p)| by Th33, Th35;

      hence thesis by SQUARE_1:def 2;

    end;

    theorem :: EUCLID_2:39

    

     Th37: |.( 0. ( TOP-REAL n)).| = 0 by TOPRNS_1: 23;

    theorem :: EUCLID_2:40

    

     Th38: |(p, p)| = 0 iff |.p.| = 0

    proof

      

       A1: |(p, p)| = ( 0 ^2 ) implies |.p.| = 0

      proof

        assume |(p, p)| = ( 0 ^2 );

        then ( |.p.| ^2 ) = 0 by Th34;

        hence thesis by XCMPLX_1: 6;

      end;

       |.p.| = 0 implies |(p, p)| = ( 0 ^2 ) by Th34;

      hence thesis by A1;

    end;

    theorem :: EUCLID_2:41

    

     Th39: |(p, p)| = 0 iff p = ( 0. ( TOP-REAL n))

    proof

       |(p, p)| = 0 implies p = ( 0. ( TOP-REAL n))

      proof

        assume |(p, p)| = 0 ;

        then n in NAT & |.p.| = 0 by Th38, ORDINAL1:def 12;

        hence thesis by TOPRNS_1: 24;

      end;

      hence thesis by Th30;

    end;

    theorem :: EUCLID_2:42

     |.p.| = 0 iff p = ( 0. ( TOP-REAL n)) by Th37, TOPRNS_1: 24;

    theorem :: EUCLID_2:43

    p <> ( 0. ( TOP-REAL n)) iff |(p, p)| > 0

    proof

      p <> ( 0. ( TOP-REAL n)) implies |(p, p)| > 0

      proof

        assume p <> ( 0. ( TOP-REAL n));

        then

         A1: |(p, p)| <> 0 by Th39;

         0 <= |(p, p)| by Th33;

        hence thesis by A1, XXREAL_0: 1;

      end;

      hence thesis by Th39;

    end;

    theorem :: EUCLID_2:44

    p <> ( 0. ( TOP-REAL n)) iff |.p.| > 0

    proof

      p <> ( 0. ( TOP-REAL n)) implies |.p.| > 0

      proof

        assume

         A1: p <> ( 0. ( TOP-REAL n));

        n in NAT & 0 <= |.p.| by Th36, ORDINAL1:def 12;

        hence thesis by A1, TOPRNS_1: 24, XXREAL_0: 1;

      end;

      hence thesis by Th37;

    end;

    theorem :: EUCLID_2:45

    

     Th43: ( |.(p + q).| ^2 ) = ((( |.p.| ^2 ) + (2 * |(q, p)|)) + ( |.q.| ^2 ))

    proof

      ( |.(p + q).| ^2 ) = |((p + q), (p + q))| by Th34

      .= (( |(p, p)| + (2 * |(q, p)|)) + |(q, q)|) by Th28

      .= ((( |.p.| ^2 ) + (2 * |(q, p)|)) + |(q, q)|) by Th34

      .= ((( |.p.| ^2 ) + (2 * |(q, p)|)) + ( |.q.| ^2 )) by Th34;

      hence thesis;

    end;

    theorem :: EUCLID_2:46

    

     Th44: ( |.(p - q).| ^2 ) = ((( |.p.| ^2 ) - (2 * |(q, p)|)) + ( |.q.| ^2 ))

    proof

      ( |.(p - q).| ^2 ) = |((p - q), (p - q))| by Th34

      .= (( |(p, p)| - (2 * |(q, p)|)) + |(q, q)|) by Th29

      .= ((( |.p.| ^2 ) - (2 * |(q, p)|)) + |(q, q)|) by Th34

      .= ((( |.p.| ^2 ) - (2 * |(q, p)|)) + ( |.q.| ^2 )) by Th34;

      hence thesis;

    end;

    theorem :: EUCLID_2:47

    (( |.(p + q).| ^2 ) + ( |.(p - q).| ^2 )) = (2 * (( |.p.| ^2 ) + ( |.q.| ^2 )))

    proof

      

       A1: ((( |.p.| ^2 ) - (2 * |(p, q)|)) + ( |.q.| ^2 )) = ((( |.p.| ^2 ) + ( |.q.| ^2 )) - (2 * |(p, q)|));

      (( |.(p + q).| ^2 ) + ( |.(p - q).| ^2 )) = (((( |.p.| ^2 ) + (2 * |(p, q)|)) + ( |.q.| ^2 )) + ( |.(p - q).| ^2 )) by Th43

      .= (((( |.p.| ^2 ) + ( |.q.| ^2 )) + (2 * |(p, q)|)) + ((( |.p.| ^2 ) + ( |.q.| ^2 )) - (2 * |(p, q)|))) by A1, Th44

      .= (2 * (( |.p.| ^2 ) + ( |.q.| ^2 )));

      hence thesis;

    end;

    theorem :: EUCLID_2:48

    (( |.(p + q).| ^2 ) - ( |.(p - q).| ^2 )) = (4 * |(p, q)|)

    proof

      (( |.(p + q).| ^2 ) - ( |.(p - q).| ^2 )) = (((( |.p.| ^2 ) + (2 * |(p, q)|)) + ( |.q.| ^2 )) - ( |.(p - q).| ^2 )) by Th43

      .= (((( |.p.| ^2 ) + (2 * |(p, q)|)) + ( |.q.| ^2 )) - ((( |.p.| ^2 ) - (2 * |(p, q)|)) + ( |.q.| ^2 ))) by Th44

      .= (4 * |(p, q)|);

      hence thesis;

    end;

    theorem :: EUCLID_2:49

     |(p, q)| = ((1 / 4) * (( |.(p + q).| ^2 ) - ( |.(p - q).| ^2 )))

    proof

      (( |.(p + q).| ^2 ) - ( |.(p - q).| ^2 )) = (((( |.p.| ^2 ) + (2 * |(p, q)|)) + ( |.q.| ^2 )) - ( |.(p - q).| ^2 )) by Th43

      .= (((( |.p.| ^2 ) + (2 * |(p, q)|)) + ( |.q.| ^2 )) - ((( |.p.| ^2 ) - (2 * |(p, q)|)) + ( |.q.| ^2 ))) by Th44

      .= (4 * |(p, q)|);

      hence thesis;

    end;

    theorem :: EUCLID_2:50

     |(p, q)| <= ( |(p, p)| + |(q, q)|)

    proof

       0 <= |(p, p)| & 0 <= |(q, q)| by Th33;

      then ( 0 + 0 ) <= ( |(p, p)| + |(q, q)|) by XREAL_1: 7;

      then

       A1: ( 0 / 2) <= (( |(p, p)| + |(q, q)|) / 2) by XREAL_1: 72;

       |((p - q), (p - q))| = (( |(p, p)| - (2 * |(p, q)|)) + |(q, q)|) by Th29

      .= (( |(p, p)| + |(q, q)|) - (2 * |(p, q)|));

      then (2 * |(p, q)|) <= (( |(p, p)| + |(q, q)|) - 0 ) by Th33, XREAL_1: 11;

      then ((2 * |(p, q)|) / 2) <= (( |(p, p)| + |(q, q)|) / 2) by XREAL_1: 72;

      then ( 0 + |(p, q)|) <= ((( |(p, p)| + |(q, q)|) / 2) + (( |(p, p)| + |(q, q)|) / 2)) by A1, XREAL_1: 7;

      hence thesis;

    end;

    theorem :: EUCLID_2:51

     |. |(p, q)|.| <= ( |.p.| * |.q.|)

    proof

      ( len p) = n & ( len q) = n by CARD_1:def 7;

      hence thesis by Th14;

    end;

    theorem :: EUCLID_2:52

     |.(p + q).| <= ( |.p.| + |.q.|)

    proof

      

       A1: ( len p) = n & ( len q) = n by CARD_1:def 7;

      thus thesis by A1, Th15;

    end;

    theorem :: EUCLID_2:53

    

     Th51: (p,( 0. ( TOP-REAL n))) are_orthogonal by Th30;

    theorem :: EUCLID_2:54

    (( 0. ( TOP-REAL n)),p) are_orthogonal by Th51;

    theorem :: EUCLID_2:55

    

     Th53: (p,p) are_orthogonal iff p = ( 0. ( TOP-REAL n)) by Th39;

    theorem :: EUCLID_2:56

    

     Th54: (p,q) are_orthogonal implies ((a * p),q) are_orthogonal

    proof

      assume (p,q) are_orthogonal ;

      then |(p, q)| = 0 ;

      then (a * |(p, q)|) = 0 ;

      then |((a * p), q)| = 0 by Th17;

      hence thesis;

    end;

    theorem :: EUCLID_2:57

    (p,q) are_orthogonal implies (p,(a * q)) are_orthogonal by Th54;

    theorem :: EUCLID_2:58

    (for q holds (p,q) are_orthogonal ) implies p = ( 0. ( TOP-REAL n)) by Th53;