complfld.miz



    begin

    definition

      :: COMPLFLD:def1

      func F_Complex -> strict doubleLoopStr means

      : Def1: the carrier of it = COMPLEX & the addF of it = addcomplex & the multF of it = multcomplex & ( 1. it ) = 1r & ( 0. it ) = 0c ;

      existence

      proof

        take doubleLoopStr (# COMPLEX , addcomplex , multcomplex , 1r , 0c #);

        thus thesis;

      end;

      uniqueness ;

    end

    registration

      cluster F_Complex -> non empty;

      coherence by Def1;

    end

    registration

      cluster the carrier of F_Complex -> complex-membered;

      coherence by Def1;

    end

    registration

      let a,b be Complex;

      let x,y be Element of F_Complex ;

      identify a + b with x + y when x = a, y = b;

      compatibility

      proof

        reconsider a9 = a, b9 = b as Element of COMPLEX by XCMPLX_0:def 2;

        assume x = a & y = b;

        

        hence (x + y) = ( addcomplex . (a9,b9)) by Def1

        .= (a + b) by BINOP_2:def 3;

      end;

      identify a * b with x * y when x = a, y = b;

      compatibility

      proof

        reconsider a9 = a, b9 = b as Element of COMPLEX by XCMPLX_0:def 2;

        assume x = a & y = b;

        

        hence (x * y) = ( multcomplex . (a9,b9)) by Def1

        .= (a * b) by BINOP_2:def 5;

      end;

    end

    registration

      cluster F_Complex -> well-unital;

      coherence

      proof

        let x be Element of F_Complex ;

        ( 1. F_Complex ) = 1r by Def1;

        hence thesis;

      end;

    end

    

     Lm1: ( 1_ F_Complex ) = 1r by Def1;

    

     Lm2: ( 1. F_Complex ) = 1r by Def1;

    registration

      cluster F_Complex -> add-associative right_zeroed right_complementable Abelian commutative associative left_unital right_unital distributive almost_left_invertible non degenerated;

      coherence

      proof

        thus F_Complex is add-associative;

        thus F_Complex is right_zeroed

        proof

          let x be Element of F_Complex ;

          reconsider x1 = x as Element of COMPLEX by Def1;

          

          thus (x + ( 0. F_Complex )) = (the addF of F_Complex . (x1, 0c )) by Def1

          .= ( addcomplex . (x1, 0c )) by Def1

          .= (x1 + 0c ) by BINOP_2:def 3

          .= x;

        end;

        thus F_Complex is right_complementable

        proof

          let x be Element of F_Complex ;

          reconsider x1 = x as Element of COMPLEX by Def1;

          ( - x1) in COMPLEX by XCMPLX_0:def 2;

          then

          reconsider y = ( - x1) as Element of F_Complex by Def1;

          take y;

          thus thesis by Def1;

        end;

        thus F_Complex is Abelian;

        thus F_Complex is commutative;

        thus F_Complex is associative;

        thus F_Complex is left_unital;

        thus F_Complex is right_unital;

        thus F_Complex is distributive;

        thus F_Complex is almost_left_invertible

        proof

          let x be Element of F_Complex ;

          reconsider x1 = x as Element of COMPLEX by Def1;

          assume

           A1: x <> ( 0. F_Complex );

          (x1 " ) in COMPLEX by XCMPLX_0:def 2;

          then

          reconsider y = (x1 " ) as Element of F_Complex by Def1;

          take y;

          x1 <> 0c by A1, Def1;

          hence thesis by Lm2, XCMPLX_0:def 7;

        end;

        ( 0. F_Complex ) <> ( 1. F_Complex ) by Def1, Lm1;

        hence F_Complex is non degenerated;

      end;

    end

    theorem :: COMPLFLD:1

    for x1,y1 be Element of F_Complex holds for x2,y2 be Complex st x1 = x2 & y1 = y2 holds (x1 + y1) = (x2 + y2);

    theorem :: COMPLFLD:2

    

     Th2: for x1 be Element of F_Complex holds for x2 be Complex st x1 = x2 holds ( - x1) = ( - x2)

    proof

      let x1 be Element of F_Complex ;

      let x2 be Complex;

      assume

       A1: x1 = x2;

      reconsider x2 as Element of COMPLEX by XCMPLX_0:def 2;

      ( - x2) in COMPLEX by XCMPLX_0:def 2;

      then

      reconsider x9 = ( - x2) as Element of F_Complex by Def1;

      (x1 + x9) = ( 0. F_Complex ) by A1, Def1;

      hence thesis by RLVECT_1:def 10;

    end;

    theorem :: COMPLFLD:3

    

     Th3: for x1,y1 be Element of F_Complex holds for x2,y2 be Complex st x1 = x2 & y1 = y2 holds (x1 - y1) = (x2 - y2)

    proof

      let x1,y1 be Element of F_Complex ;

      let x2,y2 be Complex;

      assume that

       A1: x1 = x2 and

       A2: y1 = y2;

      ( - y1) = ( - y2) by A2, Th2;

      hence thesis by A1;

    end;

    theorem :: COMPLFLD:4

    for x1,y1 be Element of F_Complex holds for x2,y2 be Complex st x1 = x2 & y1 = y2 holds (x1 * y1) = (x2 * y2);

    theorem :: COMPLFLD:5

    

     Th5: for x1 be Element of F_Complex holds for x2 be Complex st x1 = x2 & x1 <> ( 0. F_Complex ) holds (x1 " ) = (x2 " )

    proof

      let x1 be Element of F_Complex ;

      let x2 be Complex;

      reconsider x4 = x2 as Element of COMPLEX by XCMPLX_0:def 2;

      (x4 " ) in COMPLEX by XCMPLX_0:def 2;

      then

      reconsider x9 = (x4 " ) as Element of F_Complex by Def1;

      assume that

       A1: x1 = x2 and

       A2: x1 <> ( 0. F_Complex );

       0c = ( 0. F_Complex ) by Def1;

      then (x1 * x9) = ( 1. F_Complex ) by A1, A2, Lm2, XCMPLX_0:def 7;

      hence thesis by A2, VECTSP_1:def 10;

    end;

    theorem :: COMPLFLD:6

    

     Th6: for x1,y1 be Element of F_Complex holds for x2,y2 be Complex st x1 = x2 & y1 = y2 & y1 <> ( 0. F_Complex ) holds (x1 / y1) = (x2 / y2)

    proof

      let x1,y1 be Element of F_Complex ;

      let x2,y2 be Complex;

      assume that

       A1: x1 = x2 and

       A2: y1 = y2;

      assume y1 <> ( 0. F_Complex );

      then (y1 " ) = (y2 " ) by A2, Th5;

      hence thesis by A1, XCMPLX_0:def 9;

    end;

    theorem :: COMPLFLD:7

    

     Th7: ( 0. F_Complex ) = 0c by Def1;

    theorem :: COMPLFLD:8

    ( 1_ F_Complex ) = 1r by Def1;

    theorem :: COMPLFLD:9

    (( 1_ F_Complex ) + ( 1_ F_Complex )) <> ( 0. F_Complex ) by Def1, Lm1;

    definition

      let z be Element of F_Complex ;

      :: original: *'

      redefine

      func z *' -> Element of F_Complex ;

      coherence

      proof

        (z *' ) in COMPLEX by XCMPLX_0:def 2;

        hence thesis by Def1;

      end;

    end

    reserve z,z1,z2,z3,z4 for Element of F_Complex ;

    theorem :: COMPLFLD:10

    ( - z) = (( - ( 1_ F_Complex )) * z)

    proof

      reconsider z9 = z as Element of COMPLEX by Def1;

      

       A1: ( - 1r ) = ( - ( 1_ F_Complex )) by Lm1, Th2;

      

      thus ( - z) = ( - z9) by Th2

      .= (( - ( 1_ F_Complex )) * z) by A1;

    end;

    theorem :: COMPLFLD:11

    (z1 - ( - z2)) = (z1 + z2)

    proof

      reconsider z19 = z1, z29 = z2 as Element of COMPLEX by Def1;

      ( - z2) = ( - z29) by Th2;

      

      hence (z1 - ( - z2)) = (z19 - ( - z29)) by Th3

      .= (z1 + z2);

    end;

    theorem :: COMPLFLD:12

    z1 = ((z1 + z) - z)

    proof

      reconsider z19 = z1, z9 = z as Element of COMPLEX by Def1;

      

      thus ((z1 + z) - z) = ((z19 + z9) - z9) by Th3

      .= z1;

    end;

    theorem :: COMPLFLD:13

    z1 = ((z1 - z) + z)

    proof

      reconsider z19 = z1, z9 = z as Element of COMPLEX by Def1;

      (z1 - z) = (z19 - z9) by Th3;

      hence thesis;

    end;

    theorem :: COMPLFLD:14

    z1 <> ( 0. F_Complex ) & z2 <> ( 0. F_Complex ) & (z1 " ) = (z2 " ) implies z1 = z2

    proof

      reconsider z19 = z1, z29 = z2 as Element of COMPLEX by Def1;

      assume

       A1: z1 <> ( 0. F_Complex );

      assume

       A2: z2 <> ( 0. F_Complex );

      assume (z1 " ) = (z2 " );

      

      then (z19 " ) = (z2 " ) by A1, Th5

      .= (z29 " ) by A2, Th5;

      hence thesis by XCMPLX_1: 201;

    end;

    theorem :: COMPLFLD:15

    z2 <> ( 0. F_Complex ) & ((z1 * z2) = ( 1. F_Complex ) or (z2 * z1) = ( 1. F_Complex )) implies z1 = (z2 " )

    proof

      reconsider z19 = z1, z29 = z2 as Element of COMPLEX by Def1;

      assume

       A1: z2 <> ( 0. F_Complex );

      assume

       A2: (z1 * z2) = ( 1. F_Complex ) or (z2 * z1) = ( 1. F_Complex );

      per cases by A2;

        suppose

         A3: (z1 * z2) = ( 1. F_Complex );

        

         A4: (z2 " ) = (z29 " ) by A1, Th5;

        (z19 * z29) = 1r by A3, Def1;

        hence thesis by A1, A4, Th7, XCMPLX_0:def 7;

      end;

        suppose

         A5: (z2 * z1) = ( 1. F_Complex );

        

         A6: (z2 " ) = (z29 " ) by A1, Th5;

        (z29 * z19) = 1r by A5, Def1;

        hence thesis by A1, A6, Th7, XCMPLX_0:def 7;

      end;

    end;

    theorem :: COMPLFLD:16

    z2 <> ( 0. F_Complex ) & ((z1 * z2) = z3 or (z2 * z1) = z3) implies z1 = (z3 * (z2 " )) & z1 = ((z2 " ) * z3)

    proof

      reconsider z29 = z2 as Element of COMPLEX by Def1;

      assume

       A1: z2 <> ( 0. F_Complex );

      then

       A2: (z2 " ) = (z29 " ) by Th5;

      assume

       A3: (z1 * z2) = z3 or (z2 * z1) = z3;

      per cases by A3;

        suppose (z1 * z2) = z3;

        hence thesis by A1, A2, Th7, XCMPLX_1: 203;

      end;

        suppose (z2 * z1) = z3;

        hence thesis by A1, A2, Th7, XCMPLX_1: 203;

      end;

    end;

    theorem :: COMPLFLD:17

    (( 1. F_Complex ) " ) = ( 1. F_Complex )

    proof

      ( 1. F_Complex ) = ( 1r " ) by Def1;

      hence thesis by Th5;

    end;

    theorem :: COMPLFLD:18

    z1 <> ( 0. F_Complex ) & z2 <> ( 0. F_Complex ) implies ((z1 * z2) " ) = ((z1 " ) * (z2 " ))

    proof

      reconsider z19 = z1, z29 = z2 as Element of COMPLEX by Def1;

      assume

       A1: z1 <> ( 0. F_Complex );

      then

       A2: (z1 " ) = (z19 " ) by Th5;

      assume

       A3: z2 <> ( 0. F_Complex );

      then

       A4: (z2 " ) = (z29 " ) by Th5;

      (z1 * z2) <> ( 0. F_Complex ) by A1, A3, VECTSP_1: 12;

      

      hence ((z1 * z2) " ) = ((z19 * z29) " ) by Th5

      .= ((z1 " ) * (z2 " )) by A2, A4, XCMPLX_1: 204;

    end;

    theorem :: COMPLFLD:19

    z <> ( 0. F_Complex ) implies (( - z) " ) = ( - (z " ))

    proof

      reconsider z1 = z as Element of COMPLEX by Def1;

      

       A1: ( - z) = ( - z1) by Th2;

      assume

       A2: z <> ( 0. F_Complex );

      then

       A3: (z1 " ) = (z " ) by Th5;

      ( - z) <> ( 0. F_Complex ) by A2, VECTSP_1: 28;

      

      hence (( - z) " ) = (( - z1) " ) by A1, Th5

      .= ( - (z1 " )) by XCMPLX_1: 222

      .= ( - (z " )) by A3, Th2;

    end;

    theorem :: COMPLFLD:20

    z1 <> ( 0. F_Complex ) & z2 <> ( 0. F_Complex ) implies ((z1 " ) + (z2 " )) = ((z1 + z2) * ((z1 * z2) " ))

    proof

      reconsider z19 = z1, z29 = z2 as Element of COMPLEX by Def1;

      assume

       A1: z1 <> ( 0. F_Complex );

      then

       A2: (z1 " ) = (z19 " ) by Th5;

      assume

       A3: z2 <> ( 0. F_Complex );

      then (z1 * z2) <> ( 0. F_Complex ) by A1, VECTSP_1: 12;

      then

       A4: ((z1 * z2) " ) = ((z19 * z29) " ) by Th5;

      (z2 " ) = (z29 " ) by A3, Th5;

      hence thesis by A1, A2, A3, A4, Th7, XCMPLX_1: 211;

    end;

    theorem :: COMPLFLD:21

    z1 <> ( 0. F_Complex ) & z2 <> ( 0. F_Complex ) implies ((z1 " ) - (z2 " )) = ((z2 - z1) * ((z1 * z2) " ))

    proof

      reconsider z19 = z1, z29 = z2 as Element of COMPLEX by Def1;

      

       A1: (z2 - z1) = (z29 - z19) by Th3;

      assume

       A2: z1 <> ( 0. F_Complex );

      then

       A3: (z1 " ) = (z19 " ) by Th5;

      assume

       A4: z2 <> ( 0. F_Complex );

      then (z1 * z2) <> ( 0. F_Complex ) by A2, VECTSP_1: 12;

      then

       A5: ((z1 * z2) " ) = ((z19 * z29) " ) by Th5;

      (z2 " ) = (z29 " ) by A4, Th5;

      

      hence ((z1 " ) - (z2 " )) = ((z19 " ) - (z29 " )) by A3, Th3

      .= ((z2 - z1) * ((z1 * z2) " )) by A2, A4, A1, A5, Th7, XCMPLX_1: 212;

    end;

    theorem :: COMPLFLD:22

    z <> ( 0. F_Complex ) implies (z " ) = (( 1. F_Complex ) / z);

    theorem :: COMPLFLD:23

    (z / ( 1. F_Complex )) = z

    proof

      reconsider z1 = z as Element of COMPLEX by Def1;

      ( 1. F_Complex ) = 1r by Def1;

      

      hence (z / ( 1. F_Complex )) = (z1 / 1r ) by Th6

      .= z;

    end;

    theorem :: COMPLFLD:24

    z <> ( 0. F_Complex ) implies (z / z) = ( 1. F_Complex )

    proof

      reconsider z1 = z as Element of COMPLEX by Def1;

      assume

       A1: z <> ( 0. F_Complex );

      

      hence (z / z) = (z1 / z1) by Th6

      .= 1r by A1, Th7, XCMPLX_1: 60

      .= ( 1. F_Complex ) by Def1;

    end;

    theorem :: COMPLFLD:25

    z <> ( 0. F_Complex ) implies (( 0. F_Complex ) / z) = ( 0. F_Complex );

    theorem :: COMPLFLD:26

    

     Th26: z2 <> ( 0. F_Complex ) & (z1 / z2) = ( 0. F_Complex ) implies z1 = ( 0. F_Complex )

    proof

      reconsider z19 = z1, z29 = z2 as Element of COMPLEX by Def1;

      assume

       A1: z2 <> ( 0. F_Complex );

      assume (z1 / z2) = ( 0. F_Complex );

      then (z19 / z29) = ( 0. F_Complex ) by A1, Th6;

      hence thesis by A1, Th7;

    end;

    theorem :: COMPLFLD:27

    z2 <> ( 0. F_Complex ) & z4 <> ( 0. F_Complex ) implies ((z1 / z2) * (z3 / z4)) = ((z1 * z3) / (z2 * z4))

    proof

      reconsider z19 = z1, z29 = z2, z39 = z3, z49 = z4 as Element of COMPLEX by Def1;

      assume

       A1: z2 <> ( 0. F_Complex );

      assume

       A2: z4 <> ( 0. F_Complex );

      then

       A3: (z2 * z4) <> ( 0. F_Complex ) by A1, VECTSP_1: 12;

      

       A4: (z39 / z49) = (z3 / z4) by A2, Th6;

      (z19 / z29) = (z1 / z2) by A1, Th6;

      

      hence ((z1 / z2) * (z3 / z4)) = ((z19 * z39) / (z29 * z49)) by A4, XCMPLX_1: 76

      .= ((z1 * z3) / (z2 * z4)) by A3, Th6;

    end;

    theorem :: COMPLFLD:28

    z2 <> ( 0. F_Complex ) implies (z * (z1 / z2)) = ((z * z1) / z2);

    theorem :: COMPLFLD:29

    z2 <> ( 0. F_Complex ) & (z1 / z2) = ( 1. F_Complex ) implies z1 = z2

    proof

      reconsider z19 = z1, z29 = z2 as Element of COMPLEX by Def1;

      assume

       A1: z2 <> ( 0. F_Complex );

      assume (z1 / z2) = ( 1. F_Complex );

      then (z19 / z29) = ( 1. F_Complex ) by A1, Th6;

      then (z19 / z29) = 1 by Def1;

      hence thesis by XCMPLX_1: 58;

    end;

    theorem :: COMPLFLD:30

    z <> ( 0. F_Complex ) implies z1 = ((z1 * z) / z)

    proof

      reconsider z19 = z1, z9 = z as Element of COMPLEX by Def1;

      assume

       A1: z <> ( 0. F_Complex );

      

      hence z1 = ((z19 * z9) / z9) by Th7, XCMPLX_1: 89

      .= ((z1 * z) / z) by A1, Th6;

    end;

    theorem :: COMPLFLD:31

    z1 <> ( 0. F_Complex ) & z2 <> ( 0. F_Complex ) implies ((z1 / z2) " ) = (z2 / z1)

    proof

      reconsider z19 = z1, z29 = z2 as Element of COMPLEX by Def1;

      assume

       A1: z1 <> ( 0. F_Complex );

      assume

       A2: z2 <> ( 0. F_Complex );

      then

       A3: (z19 / z29) = (z1 / z2) by Th6;

      (z1 / z2) <> ( 0. F_Complex ) by A1, A2, Th26;

      

      hence ((z1 / z2) " ) = ((z19 / z29) " ) by A3, Th5

      .= (z29 / z19) by XCMPLX_1: 213

      .= (z2 / z1) by A1, Th6;

    end;

    theorem :: COMPLFLD:32

    z1 <> ( 0. F_Complex ) & z2 <> ( 0. F_Complex ) implies ((z1 " ) / (z2 " )) = (z2 / z1)

    proof

      reconsider z19 = z1, z29 = z2 as Element of COMPLEX by Def1;

      assume

       A1: z1 <> ( 0. F_Complex );

      assume z2 <> ( 0. F_Complex );

      then

       A2: (z2 " ) = (z29 " ) & (z2 " ) <> ( 0. F_Complex ) by Th5, VECTSP_1: 25;

      (z1 " ) = (z19 " ) by A1, Th5;

      

      hence ((z1 " ) / (z2 " )) = ((z19 " ) / (z29 " )) by A2, Th6

      .= (z29 / z19) by XCMPLX_1: 214

      .= (z2 / z1) by A1, Th6;

    end;

    theorem :: COMPLFLD:33

    z2 <> ( 0. F_Complex ) implies (z1 / (z2 " )) = (z1 * z2)

    proof

      reconsider z19 = z1, z29 = z2 as Element of COMPLEX by Def1;

      assume z2 <> ( 0. F_Complex );

      then (z2 " ) <> ( 0. F_Complex ) & (z2 " ) = (z29 " ) by Th5, VECTSP_1: 25;

      

      hence (z1 / (z2 " )) = (z19 / (z29 " )) by Th6

      .= (z1 * z2) by XCMPLX_1: 219;

    end;

    theorem :: COMPLFLD:34

    z1 <> ( 0. F_Complex ) & z2 <> ( 0. F_Complex ) implies ((z1 " ) / z2) = ((z1 * z2) " )

    proof

      reconsider z19 = z1, z29 = z2 as Element of COMPLEX by Def1;

      assume

       A1: z1 <> ( 0. F_Complex );

      assume

       A2: z2 <> ( 0. F_Complex );

      then

       A3: (z1 * z2) <> ( 0. F_Complex ) by A1, VECTSP_1: 12;

      (z1 " ) = (z19 " ) by A1, Th5;

      

      hence ((z1 " ) / z2) = ((z19 " ) / z29) by A2, Th6

      .= ((z19 * z29) " ) by XCMPLX_1: 221

      .= ((z1 * z2) " ) by A3, Th5;

    end;

    theorem :: COMPLFLD:35

    z1 <> ( 0. F_Complex ) & z2 <> ( 0. F_Complex ) implies ((z1 " ) * (z / z2)) = (z / (z1 * z2))

    proof

      reconsider z19 = z1, z29 = z2, z9 = z as Element of COMPLEX by Def1;

      assume

       A1: z1 <> ( 0. F_Complex );

      assume

       A2: z2 <> ( 0. F_Complex );

      then

       A3: (z1 * z2) <> ( 0. F_Complex ) by A1, VECTSP_1: 12;

      

       A4: (z9 / z29) = (z / z2) by A2, Th6;

      (z1 " ) = (z19 " ) by A1, Th5;

      

      hence ((z1 " ) * (z / z2)) = (z9 / (z19 * z29)) by A4, XCMPLX_1: 220

      .= (z / (z1 * z2)) by A3, Th6;

    end;

    theorem :: COMPLFLD:36

    z <> ( 0. F_Complex ) & z2 <> ( 0. F_Complex ) implies (z1 / z2) = ((z1 * z) / (z2 * z)) & (z1 / z2) = ((z * z1) / (z * z2))

    proof

      reconsider z19 = z1, z29 = z2, z9 = z as Element of COMPLEX by Def1;

      assume

       A1: z <> ( 0. F_Complex );

      assume

       A2: z2 <> ( 0. F_Complex );

      then

       A3: (z2 * z) <> ( 0. F_Complex ) by A1, VECTSP_1: 12;

      

      thus (z1 / z2) = (z19 / z29) by A2, Th6

      .= ((z19 * z9) / (z29 * z9)) by A1, Th7, XCMPLX_1: 91

      .= ((z1 * z) / (z2 * z)) by A3, Th6;

      hence thesis;

    end;

    theorem :: COMPLFLD:37

    z2 <> ( 0. F_Complex ) & z3 <> ( 0. F_Complex ) implies (z1 / (z2 * z3)) = ((z1 / z2) / z3)

    proof

      reconsider z19 = z1, z29 = z2, z39 = z3 as Element of COMPLEX by Def1;

      assume

       A1: z2 <> ( 0. F_Complex );

      then

       A2: (z1 / z2) = (z19 / z29) by Th6;

      assume

       A3: z3 <> ( 0. F_Complex );

      then (z2 * z3) <> ( 0. F_Complex ) by A1, VECTSP_1: 12;

      

      hence (z1 / (z2 * z3)) = (z19 / (z29 * z39)) by Th6

      .= ((z19 / z29) / z39) by XCMPLX_1: 78

      .= ((z1 / z2) / z3) by A3, A2, Th6;

    end;

    theorem :: COMPLFLD:38

    z2 <> ( 0. F_Complex ) & z3 <> ( 0. F_Complex ) implies ((z1 * z3) / z2) = (z1 / (z2 / z3))

    proof

      reconsider z19 = z1, z29 = z2, z39 = z3 as Element of COMPLEX by Def1;

      assume

       A1: z2 <> ( 0. F_Complex );

      assume

       A2: z3 <> ( 0. F_Complex );

      then

       A3: (z2 / z3) <> ( 0. F_Complex ) by A1, Th26;

      

       A4: (z2 / z3) = (z29 / z39) by A2, Th6;

      

      thus ((z1 * z3) / z2) = ((z19 * z39) / z29) by A1, Th6

      .= (z19 / (z29 / z39)) by XCMPLX_1: 77

      .= (z1 / (z2 / z3)) by A4, A3, Th6;

    end;

    theorem :: COMPLFLD:39

    z2 <> ( 0. F_Complex ) & z3 <> ( 0. F_Complex ) & z4 <> ( 0. F_Complex ) implies ((z1 / z2) / (z3 / z4)) = ((z1 * z4) / (z2 * z3))

    proof

      reconsider z19 = z1, z29 = z2, z39 = z3, z49 = z4 as Element of COMPLEX by Def1;

      assume

       A1: z2 <> ( 0. F_Complex );

      then

       A2: (z1 / z2) = (z19 / z29) by Th6;

      assume

       A3: z3 <> ( 0. F_Complex );

      then

       A4: (z2 * z3) <> ( 0. F_Complex ) by A1, VECTSP_1: 12;

      assume

       A5: z4 <> ( 0. F_Complex );

      then

       A6: (z3 / z4) = (z39 / z49) by Th6;

      (z3 / z4) <> ( 0. F_Complex ) by A3, A5, Th26;

      

      hence ((z1 / z2) / (z3 / z4)) = ((z19 / z29) / (z39 / z49)) by A2, A6, Th6

      .= ((z19 * z49) / (z29 * z39)) by XCMPLX_1: 84

      .= ((z1 * z4) / (z2 * z3)) by A4, Th6;

    end;

    theorem :: COMPLFLD:40

    z2 <> ( 0. F_Complex ) & z4 <> ( 0. F_Complex ) implies ((z1 / z2) + (z3 / z4)) = (((z1 * z4) + (z3 * z2)) / (z2 * z4))

    proof

      reconsider z19 = z1, z29 = z2, z39 = z3, z49 = z4 as Element of COMPLEX by Def1;

      assume

       A1: z2 <> ( 0. F_Complex );

      then

       A2: (z1 / z2) = (z19 / z29) by Th6;

      assume

       A3: z4 <> ( 0. F_Complex );

      then

       A4: (z2 * z4) <> ( 0. F_Complex ) by A1, VECTSP_1: 12;

      (z3 / z4) = (z39 / z49) by A3, Th6;

      

      hence ((z1 / z2) + (z3 / z4)) = (((z19 * z49) + (z39 * z29)) / (z29 * z49)) by A1, A3, A2, Th7, XCMPLX_1: 116

      .= (((z1 * z4) + (z3 * z2)) / (z2 * z4)) by A4, Th6;

    end;

    theorem :: COMPLFLD:41

    z <> ( 0. F_Complex ) implies ((z1 / z) + (z2 / z)) = ((z1 + z2) / z);

    theorem :: COMPLFLD:42

    z2 <> ( 0. F_Complex ) implies ( - (z1 / z2)) = (( - z1) / z2) & ( - (z1 / z2)) = (z1 / ( - z2))

    proof

      assume

       A1: z2 <> ( 0. F_Complex );

      then

       A2: ( - z2) <> ( 0. F_Complex ) by VECTSP_1: 28;

      reconsider z19 = z1, z29 = z2 as Element of COMPLEX by Def1;

      

       A3: ( - z1) = ( - z19) by Th2;

      (z1 / z2) = (z19 / z29) by A1, Th6;

      

      hence ( - (z1 / z2)) = ( - (z19 / z29)) by Th2

      .= (( - z19) / z29) by XCMPLX_1: 187

      .= (( - z1) / z2) by A3, A1, Th6;

      

       A4: ( - z2) = ( - z29) by Th2;

      (z1 / z2) = (z19 / z29) by A1, Th6;

      

      hence ( - (z1 / z2)) = ( - (z19 / z29)) by Th2

      .= (z19 / ( - z29)) by XCMPLX_1: 188

      .= (z1 / ( - z2)) by A4, A2, Th6;

    end;

    theorem :: COMPLFLD:43

    z2 <> ( 0. F_Complex ) implies (z1 / z2) = (( - z1) / ( - z2))

    proof

      reconsider z19 = z1, z29 = z2 as Element of COMPLEX by Def1;

      assume

       A1: z2 <> ( 0. F_Complex );

      then

       A2: ( - z2) <> ( 0. F_Complex ) by VECTSP_1: 28;

      

       A3: ( - z19) = ( - z1) & ( - z29) = ( - z2) by Th2;

      

      thus (z1 / z2) = (z19 / z29) by A1, Th6

      .= (( - z19) / ( - z29)) by XCMPLX_1: 191

      .= (( - z1) / ( - z2)) by A2, A3, Th6;

    end;

    theorem :: COMPLFLD:44

    z2 <> ( 0. F_Complex ) & z4 <> ( 0. F_Complex ) implies ((z1 / z2) - (z3 / z4)) = (((z1 * z4) - (z3 * z2)) / (z2 * z4))

    proof

      reconsider z19 = z1, z29 = z2, z39 = z3, z49 = z4 as Element of COMPLEX by Def1;

      

       A1: ((z1 * z4) - (z3 * z2)) = ((z19 * z49) - (z39 * z29)) by Th3;

      assume

       A2: z2 <> ( 0. F_Complex );

      then

       A3: (z19 / z29) = (z1 / z2) by Th6;

      assume

       A4: z4 <> ( 0. F_Complex );

      then

       A5: (z2 * z4) <> ( 0. F_Complex ) by A2, VECTSP_1: 12;

      (z39 / z49) = (z3 / z4) by A4, Th6;

      

      hence ((z1 / z2) - (z3 / z4)) = ((z19 / z29) - (z39 / z49)) by A3, Th3

      .= (((z19 * z49) - (z39 * z29)) / (z29 * z49)) by A2, A4, Th7, XCMPLX_1: 130

      .= (((z1 * z4) - (z3 * z2)) / (z2 * z4)) by A5, A1, Th6;

    end;

    theorem :: COMPLFLD:45

    z <> ( 0. F_Complex ) implies ((z1 / z) - (z2 / z)) = ((z1 - z2) / z)

    proof

      reconsider z9 = z, z19 = z1, z29 = z2 as Element of COMPLEX by Def1;

      

       A1: (z19 - z29) = (z1 - z2) by Th3;

      assume

       A2: z <> ( 0. F_Complex );

      then (z19 / z9) = (z1 / z) & (z29 / z9) = (z2 / z) by Th6;

      

      hence ((z1 / z) - (z2 / z)) = ((z19 / z9) - (z29 / z9)) by Th3

      .= ((z19 - z29) / z9) by XCMPLX_1: 120

      .= ((z1 - z2) / z) by A2, A1, Th6;

    end;

    theorem :: COMPLFLD:46

    z2 <> ( 0. F_Complex ) & ((z1 * z2) = z3 or (z2 * z1) = z3) implies z1 = (z3 / z2)

    proof

      reconsider z39 = z3, z29 = z2 as Element of COMPLEX by Def1;

      assume

       A1: z2 <> ( 0. F_Complex );

      assume

       A2: (z1 * z2) = z3 or (z2 * z1) = z3;

      per cases by A2;

        suppose (z1 * z2) = z3;

        

        hence z1 = (z39 / z29) by A1, Th7, XCMPLX_1: 89

        .= (z3 / z2) by A1, Th6;

      end;

        suppose (z2 * z1) = z3;

        

        hence z1 = (z39 / z29) by A1, Th7, XCMPLX_1: 89

        .= (z3 / z2) by A1, Th6;

      end;

    end;

    theorem :: COMPLFLD:47

    (( 0. F_Complex ) *' ) = ( 0. F_Complex )

    proof

      ( 0. F_Complex ) = 0c by Def1;

      hence thesis;

    end;

    theorem :: COMPLFLD:48

    

     Th48: (z *' ) = ( 0. F_Complex ) implies z = ( 0. F_Complex )

    proof

      assume (z *' ) = ( 0. F_Complex );

      then (z *' ) = 0c by Def1;

      then z = 0c by COMPLEX1: 29;

      hence thesis by Def1;

    end;

    theorem :: COMPLFLD:49

    (( 1. F_Complex ) *' ) = ( 1. F_Complex )

    proof

      ( 1. F_Complex ) = 1r by Def1;

      hence thesis;

    end;

    theorem :: COMPLFLD:50

    ((z *' ) *' ) = z;

    theorem :: COMPLFLD:51

    ((z1 + z2) *' ) = ((z1 *' ) + (z2 *' )) by COMPLEX1: 32;

    theorem :: COMPLFLD:52

    (( - z) *' ) = ( - (z *' ))

    proof

      reconsider z9 = z as Element of COMPLEX by Def1;

      ( - z) = ( - z9) by Th2;

      

      hence (( - z) *' ) = ( - (z9 *' )) by COMPLEX1: 33

      .= ( - (z *' )) by Th2;

    end;

    theorem :: COMPLFLD:53

    ((z1 - z2) *' ) = ((z1 *' ) - (z2 *' ))

    proof

      reconsider z19 = z1, z29 = z2 as Element of COMPLEX by Def1;

      (z19 - z29) = (z1 - z2) by Th3;

      

      hence ((z1 - z2) *' ) = ((z19 *' ) - (z29 *' )) by COMPLEX1: 34

      .= ((z1 *' ) - (z2 *' )) by Th3;

    end;

    theorem :: COMPLFLD:54

    ((z1 * z2) *' ) = ((z1 *' ) * (z2 *' )) by COMPLEX1: 35;

    theorem :: COMPLFLD:55

    z <> ( 0. F_Complex ) implies ((z " ) *' ) = ((z *' ) " )

    proof

      reconsider z1 = z as Element of COMPLEX by Def1;

      assume

       A1: z <> ( 0. F_Complex );

      then

       A2: (z *' ) <> ( 0. F_Complex ) by Th48;

      (z " ) = (z1 " ) by A1, Th5;

      

      hence ((z " ) *' ) = ((z1 *' ) " ) by COMPLEX1: 36

      .= ((z *' ) " ) by A2, Th5;

    end;

    theorem :: COMPLFLD:56

    z2 <> ( 0. F_Complex ) implies ((z1 / z2) *' ) = ((z1 *' ) / (z2 *' ))

    proof

      reconsider z19 = z1, z29 = z2 as Element of COMPLEX by Def1;

      assume

       A1: z2 <> ( 0. F_Complex );

      then

       A2: (z2 *' ) <> ( 0. F_Complex ) by Th48;

      (z19 / z29) = (z1 / z2) by A1, Th6;

      

      hence ((z1 / z2) *' ) = ((z19 *' ) / (z29 *' )) by COMPLEX1: 37

      .= ((z1 *' ) / (z2 *' )) by A2, Th6;

    end;

    theorem :: COMPLFLD:57

     |.( 0. F_Complex ).| = 0 by Def1, COMPLEX1: 44;

    theorem :: COMPLFLD:58

     |.z.| = 0 implies z = ( 0. F_Complex ) by Th7;

    theorem :: COMPLFLD:59

    z <> ( 0. F_Complex ) iff 0 < |.z.| by Th7, COMPLEX1: 47;

    theorem :: COMPLFLD:60

     |.( 1. F_Complex ).| = 1 by Def1, COMPLEX1: 48;

    theorem :: COMPLFLD:61

     |.( - z).| = |.z.|

    proof

      reconsider z1 = z as Element of COMPLEX by Def1;

      ( - z1) = ( - z) by Th2;

      hence thesis by COMPLEX1: 52;

    end;

    theorem :: COMPLFLD:62

     |.(z1 + z2).| <= ( |.z1.| + |.z2.|) by COMPLEX1: 56;

    theorem :: COMPLFLD:63

     |.(z1 - z2).| <= ( |.z1.| + |.z2.|)

    proof

      reconsider z19 = z1, z29 = z2 as Element of COMPLEX by Def1;

      (z19 - z29) = (z1 - z2) by Th3;

      hence thesis by COMPLEX1: 57;

    end;

    theorem :: COMPLFLD:64

    ( |.z1.| - |.z2.|) <= |.(z1 + z2).| by COMPLEX1: 58;

    theorem :: COMPLFLD:65

    ( |.z1.| - |.z2.|) <= |.(z1 - z2).|

    proof

      reconsider z19 = z1, z29 = z2 as Element of COMPLEX by Def1;

      (z19 - z29) = (z1 - z2) by Th3;

      hence thesis by COMPLEX1: 59;

    end;

    theorem :: COMPLFLD:66

     |.(z1 - z2).| = |.(z2 - z1).|

    proof

      reconsider z19 = z1, z29 = z2 as Element of COMPLEX by Def1;

      (z29 - z19) = (z2 - z1) & (z19 - z29) = (z1 - z2) by Th3;

      hence thesis by COMPLEX1: 60;

    end;

    theorem :: COMPLFLD:67

     |.(z1 - z2).| = 0 iff z1 = z2

    proof

      reconsider z19 = z1, z29 = z2 as Element of COMPLEX by Def1;

      thus |.(z1 - z2).| = 0 implies z1 = z2

      proof

        assume

         A1: |.(z1 - z2).| = 0 ;

        (z1 - z2) = (z19 - z29) by Th3;

        hence thesis by A1, COMPLEX1: 61;

      end;

      assume

       A2: z1 = z2;

      (z19 - z29) = (z1 - z2) by Th3;

      hence thesis by A2;

    end;

    theorem :: COMPLFLD:68

    z1 <> z2 iff 0 < |.(z1 - z2).|

    proof

      reconsider z19 = z1, z29 = z2 as Element of COMPLEX by Def1;

      thus z1 <> z2 implies 0 < |.(z1 - z2).|

      proof

        assume

         A1: z1 <> z2;

        (z1 - z2) = (z19 - z29) by Th3;

        hence thesis by A1, COMPLEX1: 62;

      end;

      assume

       A2: 0 < |.(z1 - z2).|;

      (z1 - z2) = (z19 - z29) by Th3;

      hence thesis by A2;

    end;

    theorem :: COMPLFLD:69

     |.(z1 - z2).| <= ( |.(z1 - z).| + |.(z - z2).|)

    proof

      reconsider z9 = z, z19 = z1, z29 = z2 as Element of COMPLEX by Def1;

      

       A1: (z9 - z29) = (z - z2) by Th3;

       |.(z19 - z29).| = |.(z1 - z2).| & |.(z19 - z9).| = |.(z1 - z).| by Th3;

      hence thesis by A1, COMPLEX1: 63;

    end;

    theorem :: COMPLFLD:70

     |.( |.z1.| - |.z2.|).| <= |.(z1 - z2).|

    proof

      reconsider z19 = z1, z29 = z2 as Element of COMPLEX by Def1;

      (z19 - z29) = (z1 - z2) by Th3;

      hence thesis by COMPLEX1: 64;

    end;

    theorem :: COMPLFLD:71

     |.(z1 * z2).| = ( |.z1.| * |.z2.|) by COMPLEX1: 65;

    theorem :: COMPLFLD:72

    z <> ( 0. F_Complex ) implies |.(z " ).| = ( |.z.| " )

    proof

      reconsider z1 = z as Element of COMPLEX by Def1;

      assume z <> ( 0. F_Complex );

      then (z " ) = (z1 " ) by Th5;

      hence thesis by COMPLEX1: 66;

    end;

    theorem :: COMPLFLD:73

    z2 <> ( 0. F_Complex ) implies ( |.z1.| / |.z2.|) = |.(z1 / z2).|

    proof

      reconsider z19 = z1, z29 = z2 as Element of COMPLEX by Def1;

      assume z2 <> ( 0. F_Complex );

      then (z19 / z29) = (z1 / z2) by Th6;

      hence thesis by COMPLEX1: 67;

    end;

    begin

    scheme :: COMPLFLD:sch1

    Regrwithout0 { P[ Nat] } :

P[1]

      provided

       A1: ex k be non zero Element of NAT st P[k]

       and

       A2: for k be non zero Element of NAT st k <> 1 & P[k] holds ex n be non zero Element of NAT st n < k & P[n];

      consider t be non zero Element of NAT such that

       A3: P[t] by A1;

      defpred R[ Nat] means P[($1 + 1)];

       A4:

      now

        let k be Nat;

        assume that

         A5: k <> 0 and

         A6: R[k];

        reconsider k1 = (k + 1) as non zero Element of NAT ;

        k > 0 by A5, NAT_1: 3;

        then (k + 1) > ( 0 + 1) by XREAL_1: 6;

        then

        consider n be non zero Element of NAT such that

         A7: n < k1 and

         A8: P[n] by A2, A6;

        consider l be Nat such that

         A9: n = (l + 1) by NAT_1: 6;

        take l;

        thus l < k by A7, A9, XREAL_1: 6;

        thus R[l] by A8, A9;

      end;

      ex s be Nat st t = (s + 1) by NAT_1: 6;

      then

       A10: ex k be Nat st R[k] by A3;

       R[ 0 ] from NAT_1:sch 7( A10, A4);

      hence thesis;

    end;

    theorem :: COMPLFLD:74

    

     Th74: for e be Element of F_Complex , n be Nat holds (( power F_Complex ) . (e,n)) = (e |^ n)

    proof

      let e be Element of F_Complex ;

      defpred P[ Nat] means (( power F_Complex ) . (e,$1)) = (e |^ $1);

       A1:

      now

        let n be Nat;

        reconsider n9 = n as Element of NAT by ORDINAL1:def 12;

        reconsider p = (( power F_Complex ) . (e,n9)) as Element of F_Complex ;

        assume

         A2: P[n];

        (( power F_Complex ) . (e,(n + 1))) = (p * e) by GROUP_1:def 7

        .= (e |^ (n + 1)) by A2, NEWTON: 6;

        hence P[(n + 1)];

      end;

      (( power F_Complex ) . (e, 0 )) = ( 1_ F_Complex ) by GROUP_1:def 7

      .= 1 by Def1;

      then

       A3: P[ 0 ] by NEWTON: 4;

      thus for n be Nat holds P[n] from NAT_1:sch 2( A3, A1);

    end;

    definition

      let x be Element of F_Complex ;

      let n be non zero Element of NAT ;

      :: original: CRoot

      redefine

      :: COMPLFLD:def2

      mode CRoot of n,x -> Element of F_Complex means

      : Def2: (( power F_Complex ) . (it ,n)) = x;

      coherence

      proof

        let e be CRoot of n, x;

        e is Element of COMPLEX by XCMPLX_0:def 2;

        hence thesis by Def1;

      end;

      compatibility

      proof

        let e be Element of F_Complex ;

        thus e is CRoot of n, x implies (( power F_Complex ) . (e,n)) = x

        proof

          assume e is CRoot of n, x;

          then (e |^ n) = x by COMPTRIG:def 2;

          hence thesis by Th74;

        end;

        assume (( power F_Complex ) . (e,n)) = x;

        hence (e |^ n) = x by Th74;

      end;

    end

    theorem :: COMPLFLD:75

    for x be Element of F_Complex holds for v be CRoot of 1, x holds v = x

    proof

      let x be Element of F_Complex ;

      let v be CRoot of 1, x;

      (( power F_Complex ) . (v,1)) = x by Def2;

      hence thesis by GROUP_1: 50;

    end;

    theorem :: COMPLFLD:76

    for n be non zero Element of NAT holds for v be CRoot of n, ( 0. F_Complex ) holds v = ( 0. F_Complex )

    proof

      let n be non zero Element of NAT ;

      let v be CRoot of n, ( 0. F_Complex );

      defpred P[ Element of omega ] means (( power F_Complex ) . (v,$1)) = ( 0. F_Complex );

       A1:

      now

        let k be non zero Element of NAT ;

        assume that

         A2: k <> 1 and

         A3: P[k];

        consider t be Nat such that

         A4: k = (t + 1) by NAT_1: 6;

        reconsider t as Element of NAT by ORDINAL1:def 12;

        reconsider t as non zero Element of NAT by A2, A4;

        take t;

        thus t < k by A4, NAT_1: 13;

        (( power F_Complex ) . (v,k)) = ((( power F_Complex ) . (v,t)) * v) by A4, GROUP_1:def 7;

        then (( power F_Complex ) . (v,t)) = ( 0. F_Complex ) or v = ( 0. F_Complex ) by A3, VECTSP_1: 12;

        hence P[t] by NAT_1: 3, VECTSP_1: 36;

      end;

      

       A5: ex n be non zero Element of NAT st P[n]

      proof

        take n;

        thus thesis by Def2;

      end;

       P[1] from Regrwithout0( A5, A1);

      hence thesis by GROUP_1: 50;

    end;

    theorem :: COMPLFLD:77

    for n be non zero Element of NAT holds for x be Element of F_Complex holds for v be CRoot of n, x st v = ( 0. F_Complex ) holds x = ( 0. F_Complex )

    proof

      let n be non zero Element of NAT ;

      let x be Element of F_Complex ;

      let v be CRoot of n, x;

      assume v = ( 0. F_Complex );

      then (( power F_Complex ) . (( 0. F_Complex ),n)) = x by Def2;

      hence thesis by NAT_1: 3, VECTSP_1: 36;

    end;