music_s1.miz



    begin

    theorem :: MUSIC_S1:1

    

     Th1: for r be object holds r in ( REAL+ \ { 0 }) iff r is positive Real

    proof

      let r be object;

      hereby

        assume r in ( REAL+ \ { 0 });

        then r in { r where r be Real : 0 <= r } & not r in { 0 } by REAL_1: 1, XBOOLE_0:def 5;

        then r <> 0 & ex s be Real st r = s & 0 <= s by TARSKI:def 1;

        hence r is positive Real;

      end;

      assume r is positive Real;

      then r in { r where r be Real : 0 <= r } & not r in { 0 } by TARSKI:def 1;

      hence thesis by REAL_1: 1, XBOOLE_0:def 5;

    end;

    registration

      cluster positive for Rational;

      existence

      proof

        1 is positive;

        hence thesis;

      end;

    end

    definition

      :: MUSIC_S1:def1

      func RATPLUS -> non empty Subset of REAL+ equals the set of all r where r be positive Rational;

      coherence

      proof

        set X = the set of all r where r be positive Rational;

        

         A1: the positive Rational in X;

        X c= REAL+

        proof

          let x be object;

          assume x in X;

          then ex r be positive Rational st x = r;

          hence x in REAL+ by REAL_1: 1;

        end;

        hence thesis by A1;

      end;

    end

    theorem :: MUSIC_S1:2

    

     Th2: for r be object holds r is Element of RATPLUS iff r is positive Rational

    proof

      let r be object;

      hereby

        assume r is Element of RATPLUS ;

        then r in the set of all r where r be positive Rational;

        then ex s be positive Rational st r = s;

        hence r is positive Rational;

      end;

      assume r is positive Rational;

      then r in the set of all r where r be positive Rational;

      hence r is Element of RATPLUS ;

    end;

    theorem :: MUSIC_S1:3

     RAT+ c= RAT

    proof

       not [ 0 , 0 ] in RAT+

      proof

        assume

         A1: [ 0 , 0 ] in RAT+ ;

        reconsider i = 0 as Element of omega by ORDINAL1:def 12;

        (i,i) are_coprime & i <> {} & i <> 1 by A1, ARYTM_3: 33;

        hence contradiction;

      end;

      hence thesis by XBOOLE_1: 7, ZFMISC_1: 34, NUMBERS:def 3;

    end;

    definition

      :: MUSIC_S1:def2

      func REALPLUS -> non empty Subset of REAL+ equals ( REAL+ \ { 0 });

      coherence

      proof

        1 in REAL+ & not 1 in { 0 } by REAL_1: 1, TARSKI:def 1;

        hence thesis by XBOOLE_0:def 5;

      end;

    end

    theorem :: MUSIC_S1:4

    

     Th3: NATPLUS c= RATPLUS

    proof

      let x be object;

      assume

       A1: x in NATPLUS ;

      then

      reconsider y = x as Nat;

       0 < y by A1, NAT_LAT:def 6;

      hence thesis;

    end;

    theorem :: MUSIC_S1:5

    

     Th4: NATPLUS c= REALPLUS

    proof

      let x be object;

      assume

       A1: x in NATPLUS ;

      then

      reconsider y = x as Nat;

       0 < y by A1, NAT_LAT:def 6;

      hence thesis by Th1;

    end;

    theorem :: MUSIC_S1:6

    

     Th5: RATPLUS c= REALPLUS

    proof

      let x be object;

      assume x in RATPLUS ;

      then

      reconsider y = x as positive Rational by Th2;

       0 < y;

      hence thesis by Th1;

    end;

    begin

    definition

      struct ( 1-sorted) MusicStruct (# the carrier -> set,

the Equidistance -> Relation of [: the carrier, the carrier:], [: the carrier, the carrier:],

the Ratio -> Function of [: the carrier, the carrier:], the carrier #)

       attr strict strict;

    end

    definition

      let S be MusicStruct;

      let a,b,c,d be Element of S;

      :: MUSIC_S1:def3

      pred a,b equiv c,d means [ [a, b], [c, d]] in the Equidistance of S;

    end

    definition

      let x,y be Element of REALPLUS ;

      :: MUSIC_S1:def4

      func REAL_ratio (x,y) -> Element of REALPLUS means

      : Def01: ex r,s be positive Real st x = r & s = y & it = (s / r);

      existence

      proof

        reconsider r = x, s = y as positive Real by Th1;

        reconsider t = (s / r) as positive Real;

        t is Element of REALPLUS by Th1;

        hence thesis;

      end;

      uniqueness ;

    end

    theorem :: MUSIC_S1:7

    

     Th6: for a,b,c,d be Element of REALPLUS holds ( REAL_ratio (a,b)) = ( REAL_ratio (c,d)) iff ( REAL_ratio (b,a)) = ( REAL_ratio (d,c))

    proof

      let a,b,c,d be Element of REALPLUS ;

      consider r,s be positive Real such that

       A1: a = r & b = s & ( REAL_ratio (a,b)) = (s / r) by Def01;

      consider r9,s9 be positive Real such that

       A2: c = r9 & d = s9 & ( REAL_ratio (c,d)) = (s9 / r9) by Def01;

      consider r99,s99 be positive Real such that

       A3: b = r99 & a = s99 & ( REAL_ratio (b,a)) = (s99 / r99) by Def01;

      consider r999,s999 be positive Real such that

       A4: d = r999 & c = s999 & ( REAL_ratio (d,c)) = (s999 / r999) by Def01;

      hereby

        assume

         A5: ( REAL_ratio (a,b)) = ( REAL_ratio (c,d));

        (1 / (s / r)) = (r / s) by XCMPLX_1: 57;

        then (r / s) = (r9 / s9) by A5, A1, A2, XCMPLX_1: 57;

        hence ( REAL_ratio (b,a)) = ( REAL_ratio (d,c)) by A1, A2, A3, Def01;

      end;

      assume

       A6: ( REAL_ratio (b,a)) = ( REAL_ratio (d,c));

      (1 / (s99 / r99)) = (r99 / s99) by XCMPLX_1: 57;

      then (r99 / s99) = (r999 / s999) by A6, A3, A4, XCMPLX_1: 57;

      hence ( REAL_ratio (a,b)) = ( REAL_ratio (c,d)) by Def01, A2, A4, A3;

    end;

    definition

      :: MUSIC_S1:def5

      func REAL_ratio -> Function of [: REALPLUS , REALPLUS :], REALPLUS means

      : Def02: for x be Element of [: REALPLUS , REALPLUS :] holds ex y,z be Element of REALPLUS st x = [y, z] & (it . x) = ( REAL_ratio (y,z));

      existence

      proof

        defpred P[ object, object] means ex x,y be Element of REALPLUS st $1 = [x, y] & $2 = ( REAL_ratio (x,y));

        

         A1: for x be object st x in [: REALPLUS , REALPLUS :] holds ex y be object st y in REALPLUS & P[x, y]

        proof

          let x be object;

          assume x in [: REALPLUS , REALPLUS :];

          then

          consider y,z be object such that

           A2: y in REALPLUS & z in REALPLUS & x = [y, z] by ZFMISC_1:def 2;

          reconsider y, z as Element of REALPLUS by A2;

          ( REAL_ratio (y,z)) is Element of REALPLUS ;

          hence thesis by A2;

        end;

        consider f be Function of [: REALPLUS , REALPLUS :], REALPLUS such that

         A3: for x be object st x in [: REALPLUS , REALPLUS :] holds P[x, (f . x)] from FUNCT_2:sch 1( A1);

        take f;

        now

          let x be Element of [: REALPLUS , REALPLUS :];

          assume x is Element of [: REALPLUS , REALPLUS :];

          consider y,z be object such that

           A4: y in REALPLUS & z in REALPLUS & x = [y, z] by ZFMISC_1:def 2;

          reconsider y, z as Element of REALPLUS by A4;

          take y, z;

          thus x = [y, z] by A4;

          thus (f . x) = ( REAL_ratio (y,z))

          proof

            consider x9,y9 be Element of REALPLUS such that

             A5: x = [x9, y9] & (f . x) = ( REAL_ratio (x9,y9)) by A3;

            x9 = y & y9 = z by A4, A5, XTUPLE_0: 1;

            hence thesis by A5;

          end;

        end;

        hence thesis;

      end;

      uniqueness

      proof

        let f1,f2 be Function of [: REALPLUS , REALPLUS :], REALPLUS such that

         A6: for x be Element of [: REALPLUS , REALPLUS :] holds ex y,z be Element of REALPLUS st x = [y, z] & (f1 . x) = ( REAL_ratio (y,z)) and

         A7: for x be Element of [: REALPLUS , REALPLUS :] holds ex y,z be Element of REALPLUS st x = [y, z] & (f2 . x) = ( REAL_ratio (y,z));

        now

          ( dom f1) = [: REALPLUS , REALPLUS :] by PARTFUN1:def 2;

          hence ( dom f1) = ( dom f2) by PARTFUN1:def 2;

          hereby

            let x be object;

            assume x in ( dom f1);

            then

            reconsider y = x as Element of [: REALPLUS , REALPLUS :];

            consider z,t be Element of REALPLUS such that

             A8: y = [z, t] & (f1 . y) = ( REAL_ratio (z,t)) by A6;

            consider z9,t9 be Element of REALPLUS such that

             A9: y = [z9, t9] & (f2 . y) = ( REAL_ratio (z9,t9)) by A7;

            z = z9 & t = t9 by A8, A9, XTUPLE_0: 1;

            hence (f1 . x) = (f2 . x) by A8, A9;

          end;

        end;

        hence f1 = f2 by FUNCT_1: 2;

      end;

    end

    definition

      :: MUSIC_S1:def6

      func EQUIV_REAL_ratio -> Relation of [: REALPLUS , REALPLUS :], [: REALPLUS , REALPLUS :] means

      : Def03: for x,y be Element of [: REALPLUS , REALPLUS :] holds [x, y] in it iff ex a,b,c,d be Element of REALPLUS st x = [a, b] & y = [c, d] & ( REAL_ratio (a,b)) = ( REAL_ratio (c,d));

      existence

      proof

        defpred P[ object, object] means ex a,b,c,d be Element of REALPLUS st $1 = [a, b] & $2 = [c, d] & ( REAL_ratio (a,b)) = ( REAL_ratio (c,d));

        consider R be Relation of [: REALPLUS , REALPLUS :], [: REALPLUS , REALPLUS :] such that

         A1: for x,y be object holds [x, y] in R iff x in [: REALPLUS , REALPLUS :] & y in [: REALPLUS , REALPLUS :] & P[x, y] from RELSET_1:sch 1;

        for x,y be Element of [: REALPLUS , REALPLUS :] holds [x, y] in R iff ex a,b,c,d be Element of REALPLUS st x = [a, b] & y = [c, d] & ( REAL_ratio (a,b)) = ( REAL_ratio (c,d)) by A1;

        hence thesis;

      end;

      uniqueness

      proof

        let R1,R2 be Relation of [: REALPLUS , REALPLUS :], [: REALPLUS , REALPLUS :] such that

         A2: for x,y be Element of [: REALPLUS , REALPLUS :] holds [x, y] in R1 iff ex a,b,c,d be Element of REALPLUS st x = [a, b] & y = [c, d] & ( REAL_ratio (a,b)) = ( REAL_ratio (c,d)) and

         A3: for x,y be Element of [: REALPLUS , REALPLUS :] holds [x, y] in R2 iff ex a,b,c,d be Element of REALPLUS st x = [a, b] & y = [c, d] & ( REAL_ratio (a,b)) = ( REAL_ratio (c,d));

        for x,y be object holds [x, y] in R1 iff [x, y] in R2

        proof

          let x,y be object;

          hereby

            assume

             A4: [x, y] in R1;

            then

            reconsider x9 = x, y9 = y as Element of [: REALPLUS , REALPLUS :] by ZFMISC_1: 87;

            ex a,b,c,d be Element of REALPLUS st x9 = [a, b] & y9 = [c, d] & ( REAL_ratio (a,b)) = ( REAL_ratio (c,d)) by A4, A2;

            hence [x, y] in R2 by A3;

          end;

          assume

           A5: [x, y] in R2;

          then

          reconsider x9 = x, y9 = y as Element of [: REALPLUS , REALPLUS :] by ZFMISC_1: 87;

          ex a,b,c,d be Element of REALPLUS st x9 = [a, b] & y9 = [c, d] & ( REAL_ratio (a,b)) = ( REAL_ratio (c,d)) by A3, A5;

          hence [x, y] in R1 by A2;

        end;

        hence thesis;

      end;

    end

    definition

      :: MUSIC_S1:def7

      func REAL_Music -> MusicStruct equals MusicStruct (# REALPLUS , EQUIV_REAL_ratio , REAL_ratio #);

      coherence ;

    end

    theorem :: MUSIC_S1:8

    

     Th7: REAL_Music is non empty & the carrier of REAL_Music c= REALPLUS & (for f1,f2,f3,f4 be Element of REAL_Music holds ((f1,f2) equiv (f3,f4) iff (the Ratio of REAL_Music . (f1,f2)) = (the Ratio of REAL_Music . (f3,f4))))

    proof

      set T = REAL_Music ;

      thus T is non empty;

      thus the carrier of T c= REALPLUS ;

      thus for f1,f2,f3,f4 be Element of T holds ((f1,f2) equiv (f3,f4) iff (the Ratio of T . (f1,f2)) = (the Ratio of T . (f3,f4)))

      proof

        let f1,f2,f3,f4 be Element of T;

        reconsider x = [f1, f2], y = [f3, f4] as Element of [: REALPLUS , REALPLUS :] by ZFMISC_1:def 2;

        consider y9,z9 be Element of REALPLUS such that

         A1: x = [y9, z9] and

         A2: ( REAL_ratio . x) = ( REAL_ratio (y9,z9)) by Def02;

        consider y99,z99 be Element of REALPLUS such that

         A3: y = [y99, z99] and

         A4: ( REAL_ratio . y) = ( REAL_ratio (y99,z99)) by Def02;

        hereby

          assume (f1,f2) equiv (f3,f4);

          then

          consider a,b,c,d be Element of REALPLUS such that

           A5: x = [a, b] & y = [c, d] and

           A6: ( REAL_ratio (a,b)) = ( REAL_ratio (c,d)) by Def03;

          y9 = a & z9 = b & y99 = c & z99 = d by A1, A3, A5, XTUPLE_0: 1;

          then a = f1 & b = f2 & c = f3 & d = f4 & (the Ratio of T . (a,b)) = ( REAL_ratio (a,b)) & (the Ratio of T . (c,d)) = ( REAL_ratio (c,d)) by XTUPLE_0: 1, A2, A4, A5, BINOP_1:def 1;

          hence (the Ratio of T . (f1,f2)) = (the Ratio of T . (f3,f4)) by A6;

        end;

        assume

         A7: (the Ratio of T . (f1,f2)) = (the Ratio of T . (f3,f4));

        ( REAL_ratio (y9,z9)) = ( REAL_ratio . (f1,f2)) by A2, BINOP_1:def 1

        .= ( REAL_ratio (y99,z99)) by A7, A4, BINOP_1:def 1;

        hence (f1,f2) equiv (f3,f4) by A1, A3, Def03;

      end;

    end;

    theorem :: MUSIC_S1:9

    

     Th8: for f1,f2,f3 be Element of REAL_Music st (the Ratio of REAL_Music . (f1,f2)) = (the Ratio of REAL_Music . (f1,f3)) holds f2 = f3

    proof

      set S = REAL_Music ;

      let f1,f2,f3 be Element of S;

      assume

       A1: (the Ratio of S . (f1,f2)) = (the Ratio of S . (f1,f3));

      reconsider x = [f1, f2], y = [f1, f3] as Element of [: REALPLUS , REALPLUS :] by ZFMISC_1:def 2;

      consider y9,z9 be Element of REALPLUS such that

       A2: x = [y9, z9] and

       A3: ( REAL_ratio . x) = ( REAL_ratio (y9,z9)) by Def02;

      consider y99,z99 be Element of REALPLUS such that

       A4: y = [y99, z99] and

       A5: ( REAL_ratio . y) = ( REAL_ratio (y99,z99)) by Def02;

      consider r,s be positive Real such that

       A6: y9 = r & s = z9 & ( REAL_ratio (y9,z9)) = (s / r) by Def01;

      consider r9,s9 be positive Real such that

       A7: y99 = r9 & s9 = z99 & ( REAL_ratio (y99,z99)) = (s9 / r9) by Def01;

      

       A8: y9 = f1 & z9 = f2 & y99 = f1 & z99 = f3 by A2, A4, XTUPLE_0: 1;

      ( REAL_ratio . (f1,f2)) = ( REAL_ratio (y9,z9)) & ( REAL_ratio . (f1,f3)) = ( REAL_ratio (y99,z99)) by A5, A3, BINOP_1:def 1;

      hence thesis by A6, A7, A8, A1, XCMPLX_1: 53;

    end;

    theorem :: MUSIC_S1:10

     NATPLUS c= the carrier of REAL_Music by Th4;

    theorem :: MUSIC_S1:11

    

     Th9: for frequency be Element of REAL_Music holds for n be non zero Nat holds ex harmonique be Element of REAL_Music st [frequency, harmonique] in ( Class (the Equidistance of REAL_Music , [1, n]))

    proof

      set S = REAL_Music ;

      now

        let frequency be Element of S;

        let n be non zero Nat;

        reconsider f = frequency as positive Real by Th1;

        reconsider harmonique = (n * f) as Element of S by Th1;

        take harmonique;

        reconsider x = 1, y = n as Element of S by Th1;

        reconsider z = [x, y] as Element of [: REALPLUS , REALPLUS :] by ZFMISC_1:def 2;

        consider x9,y9 be Element of REALPLUS such that

         A1: z = [x9, y9] and

         A2: ( REAL_ratio . z) = ( REAL_ratio (x9,y9)) by Def02;

        reconsider z9 = [frequency, harmonique] as Element of [: REALPLUS , REALPLUS :] by ZFMISC_1:def 2;

        consider x99,y99 be Element of REALPLUS such that

         A3: z9 = [x99, y99] and

         A4: ( REAL_ratio . z9) = ( REAL_ratio (x99,y99)) by Def02;

        consider r,s be positive Real such that

         A5: x9 = r & s = y9 & ( REAL_ratio (x9,y9)) = (s / r) by Def01;

        

         A6: r = 1 & s = n by A5, A1, XTUPLE_0: 1;

        consider r9,s9 be positive Real such that

         A7: x99 = r9 & s9 = y99 & ( REAL_ratio (x99,y99)) = (s9 / r9) by Def01;

        

         A8: r9 = frequency & s9 = harmonique by A7, A3, XTUPLE_0: 1;

        now

          thus (the Ratio of S . (x,y)) = n by A5, A6, A2, BINOP_1:def 1;

          

          thus (the Ratio of S . (frequency,harmonique)) = ( REAL_ratio (x99,y99)) by A4, BINOP_1:def 1

          .= n by A7, A8, XCMPLX_1: 89;

        end;

        then (x,y) equiv (frequency,harmonique) by Th7;

        hence [frequency, harmonique] in ( Class (the Equidistance of S, [1, n])) by EQREL_1: 18;

      end;

      hence thesis;

    end;

    theorem :: MUSIC_S1:12

    

     Th10: for f1,f2,f3 be Element of REAL_Music st (the Ratio of REAL_Music . (f1,f1)) = (the Ratio of REAL_Music . (f2,f3)) holds f2 = f3

    proof

      let f1,f2,f3 be Element of REAL_Music ;

      assume

       A1: (the Ratio of REAL_Music . (f1,f1)) = (the Ratio of REAL_Music . (f2,f3));

      reconsider x = [f1, f1], y = [f2, f3] as Element of [: REALPLUS , REALPLUS :] by ZFMISC_1:def 2;

      consider y9,z9 be Element of REALPLUS such that

       A2: x = [y9, z9] and

       A3: ( REAL_ratio . x) = ( REAL_ratio (y9,z9)) by Def02;

      consider y99,z99 be Element of REALPLUS such that

       A4: y = [y99, z99] and

       A5: ( REAL_ratio . y) = ( REAL_ratio (y99,z99)) by Def02;

      consider r,s be positive Real such that

       A6: y9 = r & s = z9 & ( REAL_ratio (y9,z9)) = (s / r) by Def01;

      consider r9,s9 be positive Real such that

       A7: y99 = r9 & s9 = z99 & ( REAL_ratio (y99,z99)) = (s9 / r9) by Def01;

      

       A8: y9 = f1 & z9 = f1 & y99 = f2 & z99 = f3 by A2, A4, XTUPLE_0: 1;

      ( REAL_ratio . (f1,f1)) = ( REAL_ratio (y9,z9)) & ( REAL_ratio . (f2,f3)) = ( REAL_ratio (y99,z99)) by A5, A3, BINOP_1:def 1;

      hence f2 = f3 by A7, A8, XCMPLX_1: 58, XCMPLX_1: 60, A6, A1;

    end;

    theorem :: MUSIC_S1:13

    

     Th11: for f1,f2,fn1,fm1,fn2,fm2 be Element of REAL_Music holds for r1,r2 be positive Real holds for n,m be non zero Nat st fn1 = (n * r1) & fm1 = (m * r1) & fn2 = (n * r2) & fm2 = (m * r2) holds (fn1,fm1) equiv (fn2,fm2)

    proof

      let f1,f2,fn1,fm1,fn2,fm2 be Element of REAL_Music ;

      let r1,r2 be positive Real;

      now

        let n,m be non zero Nat;

        assume

         A0: fn1 = (n * r1) & fm1 = (m * r1) & fn2 = (n * r2) & fm2 = (m * r2);

        reconsider z = [fn1, fm1] as Element of [: REALPLUS , REALPLUS :] by ZFMISC_1:def 2;

        consider x9,y9 be Element of REALPLUS such that

         A1: z = [x9, y9] and

         A2: ( REAL_ratio . z) = ( REAL_ratio (x9,y9)) by Def02;

        consider r,s be positive Real such that

         A3: x9 = r & s = y9 & ( REAL_ratio (x9,y9)) = (s / r) by Def01;

        reconsider z9 = [fn2, fm2] as Element of [: REALPLUS , REALPLUS :] by ZFMISC_1:def 2;

        consider x99,y99 be Element of REALPLUS such that

         A4: z9 = [x99, y99] and

         A5: ( REAL_ratio . z9) = ( REAL_ratio (x99,y99)) by Def02;

        consider r9,s9 be positive Real such that

         A6: x99 = r9 & s9 = y99 & ( REAL_ratio (x99,y99)) = (s9 / r9) by Def01;

        now

          thus ( REAL_ratio . (fn1,fm1)) = (s / r) by A3, A2, BINOP_1:def 1;

          thus ( REAL_ratio . (fn2,fm2)) = (s9 / r9) by A6, A5, BINOP_1:def 1;

          r = (n * r1) & s = (m * r1) & r9 = (n * r2) & s9 = (m * r2) by A4, A6, A1, A3, A0, XTUPLE_0: 1;

          then (s / r) = (m qua Real / n qua Real) & (s9 / r9) = (m qua Real / n qua Real) by XCMPLX_1: 91;

          hence (s / r) = (s9 / r9);

        end;

        hence (fn1,fm1) equiv (fn2,fm2) by Th7;

      end;

      hence thesis;

    end;

    theorem :: MUSIC_S1:14

    

     Th12: for f1,f2,f3,f4 be Element of REAL_Music holds ((the Ratio of REAL_Music . (f1,f2)) = (the Ratio of REAL_Music . (f3,f4))) iff (the Ratio of REAL_Music . (f2,f1)) = (the Ratio of REAL_Music . (f4,f3))

    proof

      let f1,f2,f3,f4 be Element of REAL_Music ;

      set MS = REAL_Music ;

      reconsider x = [f1, f2], y = [f3, f4] as Element of [: REALPLUS , REALPLUS :] by ZFMISC_1:def 2;

      consider y9,z9 be Element of REALPLUS such that

       A1: x = [y9, z9] and

       A2: ( REAL_ratio . x) = ( REAL_ratio (y9,z9)) by Def02;

      consider y99,z99 be Element of REALPLUS such that

       A3: y = [y99, z99] and

       A4: ( REAL_ratio . y) = ( REAL_ratio (y99,z99)) by Def02;

      reconsider x1 = [z9, y9], y1 = [z99, y99] as Element of [: REALPLUS , REALPLUS :];

      consider y19,z19 be Element of REALPLUS such that

       A5: x1 = [y19, z19] and

       A6: ( REAL_ratio . x1) = ( REAL_ratio (y19,z19)) by Def02;

      consider y199,z199 be Element of REALPLUS such that

       A7: y1 = [y199, z199] and

       A8: ( REAL_ratio . y1) = ( REAL_ratio (y199,z199)) by Def02;

      

       A9: f1 = y9 & f2 = z9 & f3 = y99 & f4 = z99 by A1, A3, XTUPLE_0: 1;

      then

       A10: f1 = z19 & f2 = y19 & f3 = z199 & f4 = y199 by A5, A7, XTUPLE_0: 1;

      

       A11: (the Ratio of MS . (f2,f1)) = ( REAL_ratio (y19,z19)) & (the Ratio of MS . (f4,f3)) = ( REAL_ratio (y199,z199)) by A9, BINOP_1:def 1, A6, A8;

      hereby

        assume

         A12: ((the Ratio of MS . (f1,f2)) = (the Ratio of MS . (f3,f4)));

        ( REAL_ratio (y9,z9)) = ( REAL_ratio . (f1,f2)) by A2, BINOP_1:def 1

        .= ( REAL_ratio (y99,z99)) by A12, A4, BINOP_1:def 1;

        hence (the Ratio of MS . (f2,f1)) = (the Ratio of MS . (f4,f3)) by A9, A10, A11, Th6;

      end;

      assume

       A13: (the Ratio of MS . (f2,f1)) = (the Ratio of MS . (f4,f3));

      ( REAL_ratio . (f1,f2)) = ( REAL_ratio (z19,y19)) by BINOP_1:def 1, A9, A10, A2

      .= ( REAL_ratio (z199,y199)) by A13, A11, Th6

      .= ( REAL_ratio . (f3,f4)) by BINOP_1:def 1, A9, A10, A4;

      hence ((the Ratio of MS . (f1,f2)) = (the Ratio of MS . (f3,f4)));

    end;

    begin

    definition

      let x,y be Element of RATPLUS ;

      :: MUSIC_S1:def8

      func RAT_ratio (x,y) -> Element of RATPLUS means

      : Def04: ex r,s be positive Rational st x = r & s = y & it = (s / r);

      existence

      proof

        reconsider r = x, s = y as positive Rational by Th2;

        reconsider t = (s / r) as positive Rational;

        t is Element of RATPLUS by Th2;

        hence thesis;

      end;

      uniqueness ;

    end

    theorem :: MUSIC_S1:15

    

     Th13: for a,b,c,d be Element of RATPLUS holds ( RAT_ratio (a,b)) = ( RAT_ratio (c,d)) iff ( RAT_ratio (b,a)) = ( RAT_ratio (d,c))

    proof

      let a,b,c,d be Element of RATPLUS ;

      consider r,s be positive Rational such that

       A1: a = r & b = s & ( RAT_ratio (a,b)) = (s / r) by Def04;

      consider r9,s9 be positive Rational such that

       A2: c = r9 & d = s9 & ( RAT_ratio (c,d)) = (s9 / r9) by Def04;

      consider r99,s99 be positive Rational such that

       A3: b = r99 & a = s99 & ( RAT_ratio (b,a)) = (s99 / r99) by Def04;

      consider r999,s999 be positive Rational such that

       A4: d = r999 & c = s999 & ( RAT_ratio (d,c)) = (s999 / r999) by Def04;

      hereby

        assume

         A5: ( RAT_ratio (a,b)) = ( RAT_ratio (c,d));

        (1 / (s / r)) = (r / s) by XCMPLX_1: 57;

        hence ( RAT_ratio (b,a)) = ( RAT_ratio (d,c)) by A1, A2, A3, A4, A5, XCMPLX_1: 57;

      end;

      assume

       A6: ( RAT_ratio (b,a)) = ( RAT_ratio (d,c));

      (1 / (s99 / r99)) = (r99 / s99) by XCMPLX_1: 57;

      hence ( RAT_ratio (a,b)) = ( RAT_ratio (c,d)) by A1, A2, A3, A4, A6, XCMPLX_1: 57;

    end;

    definition

      :: MUSIC_S1:def9

      func RAT_ratio -> Function of [: RATPLUS , RATPLUS :], RATPLUS means

      : Def05: for x be Element of [: RATPLUS , RATPLUS :] holds ex y,z be Element of RATPLUS st x = [y, z] & (it . x) = ( RAT_ratio (y,z));

      existence

      proof

        defpred P[ object, object] means ex x,y be Element of RATPLUS st $1 = [x, y] & $2 = ( RAT_ratio (x,y));

        

         A1: for x be object st x in [: RATPLUS , RATPLUS :] holds ex y be object st y in RATPLUS & P[x, y]

        proof

          let x be object;

          assume x in [: RATPLUS , RATPLUS :];

          then

          consider y,z be object such that

           A2: y in RATPLUS & z in RATPLUS & x = [y, z] by ZFMISC_1:def 2;

          reconsider y, z as Element of RATPLUS by A2;

          ( RAT_ratio (y,z)) is Element of RATPLUS ;

          hence thesis by A2;

        end;

        consider f be Function of [: RATPLUS , RATPLUS :], RATPLUS such that

         A3: for x be object st x in [: RATPLUS , RATPLUS :] holds P[x, (f . x)] from FUNCT_2:sch 1( A1);

        take f;

        now

          let x be Element of [: RATPLUS , RATPLUS :];

          assume x is Element of [: RATPLUS , RATPLUS :];

          consider y,z be object such that

           A4: y in RATPLUS & z in RATPLUS & x = [y, z] by ZFMISC_1:def 2;

          reconsider y, z as Element of RATPLUS by A4;

          take y, z;

          thus x = [y, z] by A4;

          thus (f . x) = ( RAT_ratio (y,z))

          proof

            consider x9,y9 be Element of RATPLUS such that

             A5: x = [x9, y9] & (f . x) = ( RAT_ratio (x9,y9)) by A3;

            x9 = y & y9 = z by A4, A5, XTUPLE_0: 1;

            hence thesis by A5;

          end;

        end;

        hence thesis;

      end;

      uniqueness

      proof

        let f1,f2 be Function of [: RATPLUS , RATPLUS :], RATPLUS such that

         A6: for x be Element of [: RATPLUS , RATPLUS :] holds ex y,z be Element of RATPLUS st x = [y, z] & (f1 . x) = ( RAT_ratio (y,z)) and

         A7: for x be Element of [: RATPLUS , RATPLUS :] holds ex y,z be Element of RATPLUS st x = [y, z] & (f2 . x) = ( RAT_ratio (y,z));

        now

          ( dom f1) = [: RATPLUS , RATPLUS :] by PARTFUN1:def 2;

          hence ( dom f1) = ( dom f2) by PARTFUN1:def 2;

          hereby

            let x be object;

            assume x in ( dom f1);

            then

            reconsider y = x as Element of [: RATPLUS , RATPLUS :];

            consider z,t be Element of RATPLUS such that

             A8: y = [z, t] & (f1 . y) = ( RAT_ratio (z,t)) by A6;

            consider z9,t9 be Element of RATPLUS such that

             A9: y = [z9, t9] & (f2 . y) = ( RAT_ratio (z9,t9)) by A7;

            z = z9 & t = t9 by A8, A9, XTUPLE_0: 1;

            hence (f1 . x) = (f2 . x) by A8, A9;

          end;

        end;

        hence f1 = f2 by FUNCT_1: 2;

      end;

    end

    definition

      :: MUSIC_S1:def10

      func EQUIV_RAT_ratio -> Relation of [: RATPLUS , RATPLUS :], [: RATPLUS , RATPLUS :] means

      : Def06: for x,y be Element of [: RATPLUS , RATPLUS :] holds [x, y] in it iff ex a,b,c,d be Element of RATPLUS st x = [a, b] & y = [c, d] & ( RAT_ratio (a,b)) = ( RAT_ratio (c,d));

      existence

      proof

        defpred P[ object, object] means ex a,b,c,d be Element of RATPLUS st $1 = [a, b] & $2 = [c, d] & ( RAT_ratio (a,b)) = ( RAT_ratio (c,d));

        consider R be Relation of [: RATPLUS , RATPLUS :], [: RATPLUS , RATPLUS :] such that

         A1: for x,y be object holds [x, y] in R iff x in [: RATPLUS , RATPLUS :] & y in [: RATPLUS , RATPLUS :] & P[x, y] from RELSET_1:sch 1;

        for x,y be Element of [: RATPLUS , RATPLUS :] holds [x, y] in R iff ex a,b,c,d be Element of RATPLUS st x = [a, b] & y = [c, d] & ( RAT_ratio (a,b)) = ( RAT_ratio (c,d)) by A1;

        hence thesis;

      end;

      uniqueness

      proof

        let R1,R2 be Relation of [: RATPLUS , RATPLUS :], [: RATPLUS , RATPLUS :] such that

         A2: for x,y be Element of [: RATPLUS , RATPLUS :] holds [x, y] in R1 iff ex a,b,c,d be Element of RATPLUS st x = [a, b] & y = [c, d] & ( RAT_ratio (a,b)) = ( RAT_ratio (c,d)) and

         A3: for x,y be Element of [: RATPLUS , RATPLUS :] holds [x, y] in R2 iff ex a,b,c,d be Element of RATPLUS st x = [a, b] & y = [c, d] & ( RAT_ratio (a,b)) = ( RAT_ratio (c,d));

        for x,y be object holds [x, y] in R1 iff [x, y] in R2

        proof

          let x,y be object;

          hereby

            assume

             A4: [x, y] in R1;

            then

            reconsider x9 = x, y9 = y as Element of [: RATPLUS , RATPLUS :] by ZFMISC_1: 87;

            ex a,b,c,d be Element of RATPLUS st x9 = [a, b] & y9 = [c, d] & ( RAT_ratio (a,b)) = ( RAT_ratio (c,d)) by A4, A2;

            hence [x, y] in R2 by A3;

          end;

          assume

           A5: [x, y] in R2;

          then

          reconsider x9 = x, y9 = y as Element of [: RATPLUS , RATPLUS :] by ZFMISC_1: 87;

          ex a,b,c,d be Element of RATPLUS st x9 = [a, b] & y9 = [c, d] & ( RAT_ratio (a,b)) = ( RAT_ratio (c,d)) by A3, A5;

          hence [x, y] in R1 by A2;

        end;

        hence thesis;

      end;

    end

    definition

      :: MUSIC_S1:def11

      func RAT_Music -> MusicStruct equals MusicStruct (# RATPLUS , EQUIV_RAT_ratio , RAT_ratio #);

      coherence ;

    end

    theorem :: MUSIC_S1:16

    

     Th14: RAT_Music is non empty & the carrier of RAT_Music c= REALPLUS & (for f1,f2,f3,f4 be Element of RAT_Music holds ((f1,f2) equiv (f3,f4) iff (the Ratio of RAT_Music . (f1,f2)) = (the Ratio of RAT_Music . (f3,f4))))

    proof

      set T = RAT_Music ;

      thus T is non empty;

      thus the carrier of T c= REALPLUS by Th5;

      thus for f1,f2,f3,f4 be Element of T holds ((f1,f2) equiv (f3,f4) iff (the Ratio of T . (f1,f2)) = (the Ratio of T . (f3,f4)))

      proof

        let f1,f2,f3,f4 be Element of T;

        reconsider x = [f1, f2], y = [f3, f4] as Element of [: RATPLUS , RATPLUS :] by ZFMISC_1:def 2;

        consider y9,z9 be Element of RATPLUS such that

         A1: x = [y9, z9] and

         A2: ( RAT_ratio . x) = ( RAT_ratio (y9,z9)) by Def05;

        consider y99,z99 be Element of RATPLUS such that

         A3: y = [y99, z99] and

         A4: ( RAT_ratio . y) = ( RAT_ratio (y99,z99)) by Def05;

        hereby

          assume (f1,f2) equiv (f3,f4);

          then

          consider a,b,c,d be Element of RATPLUS such that

           A5: x = [a, b] & y = [c, d] and

           A6: ( RAT_ratio (a,b)) = ( RAT_ratio (c,d)) by Def06;

          y9 = a & z9 = b & y99 = c & z99 = d by A1, A3, A5, XTUPLE_0: 1;

          then a = f1 & b = f2 & c = f3 & d = f4 & (the Ratio of T . (a,b)) = ( RAT_ratio (a,b)) & (the Ratio of T . (c,d)) = ( RAT_ratio (c,d)) by XTUPLE_0: 1, A2, A4, A5, BINOP_1:def 1;

          hence (the Ratio of T . (f1,f2)) = (the Ratio of T . (f3,f4)) by A6;

        end;

        assume

         A7: (the Ratio of T . (f1,f2)) = (the Ratio of T . (f3,f4));

        ( RAT_ratio (y9,z9)) = ( RAT_ratio . (f1,f2)) by A2, BINOP_1:def 1

        .= ( RAT_ratio (y99,z99)) by A7, A4, BINOP_1:def 1;

        hence (f1,f2) equiv (f3,f4) by A1, A3, Def06;

      end;

    end;

    theorem :: MUSIC_S1:17

    

     Th15: for f1,f2,f3 be Element of RAT_Music st (the Ratio of RAT_Music . (f1,f2)) = (the Ratio of RAT_Music . (f1,f3)) holds f2 = f3

    proof

      set S = RAT_Music ;

      let f1,f2,f3 be Element of S;

      assume

       A1: (the Ratio of S . (f1,f2)) = (the Ratio of S . (f1,f3));

      reconsider x = [f1, f2], y = [f1, f3] as Element of [: RATPLUS , RATPLUS :] by ZFMISC_1:def 2;

      consider y9,z9 be Element of RATPLUS such that

       A2: x = [y9, z9] and

       A3: ( RAT_ratio . x) = ( RAT_ratio (y9,z9)) by Def05;

      consider y99,z99 be Element of RATPLUS such that

       A4: y = [y99, z99] and

       A5: ( RAT_ratio . y) = ( RAT_ratio (y99,z99)) by Def05;

      consider r,s be positive Rational such that

       A6: y9 = r & s = z9 & ( RAT_ratio (y9,z9)) = (s / r) by Def04;

      consider r9,s9 be positive Rational such that

       A7: y99 = r9 & s9 = z99 & ( RAT_ratio (y99,z99)) = (s9 / r9) by Def04;

      

       A8: y9 = f1 & z9 = f2 & y99 = f1 & z99 = f3 by A2, A4, XTUPLE_0: 1;

      ( RAT_ratio . (f1,f2)) = ( RAT_ratio (y9,z9)) & ( RAT_ratio . (f1,f3)) = ( RAT_ratio (y99,z99)) by A5, A3, BINOP_1:def 1;

      hence thesis by A6, A7, A8, A1, XCMPLX_1: 53;

    end;

    theorem :: MUSIC_S1:18

     NATPLUS c= the carrier of RAT_Music by Th3;

    theorem :: MUSIC_S1:19

    

     Th16: for frequency be Element of RAT_Music holds for n be non zero Nat holds ex harmonique be Element of RAT_Music st [frequency, harmonique] in ( Class (the Equidistance of RAT_Music , [1, n]))

    proof

      set S = RAT_Music ;

      now

        let frequency be Element of S;

        let n be non zero Nat;

        reconsider f = frequency as positive Rational by Th2;

        reconsider harmonique = (n * f) as Element of S by Th2;

        take harmonique;

        reconsider x = 1, y = n as Element of S by Th2;

        reconsider z = [x, y] as Element of [: RATPLUS , RATPLUS :] by ZFMISC_1:def 2;

        consider x9,y9 be Element of RATPLUS such that

         A1: z = [x9, y9] and

         A2: ( RAT_ratio . z) = ( RAT_ratio (x9,y9)) by Def05;

        reconsider z9 = [frequency, harmonique] as Element of [: RATPLUS , RATPLUS :] by ZFMISC_1:def 2;

        consider x99,y99 be Element of RATPLUS such that

         A3: z9 = [x99, y99] and

         A4: ( RAT_ratio . z9) = ( RAT_ratio (x99,y99)) by Def05;

        consider r,s be positive Rational such that

         A5: x9 = r & s = y9 & ( RAT_ratio (x9,y9)) = (s / r) by Def04;

        

         A6: r = 1 & s = n by A5, A1, XTUPLE_0: 1;

        consider r9,s9 be positive Rational such that

         A7: x99 = r9 & s9 = y99 & ( RAT_ratio (x99,y99)) = (s9 / r9) by Def04;

        

         A8: r9 = frequency & s9 = harmonique by A7, A3, XTUPLE_0: 1;

        now

          thus (the Ratio of S . (x,y)) = n by A5, A6, A2, BINOP_1:def 1;

          

          thus (the Ratio of S . (frequency,harmonique)) = ( RAT_ratio (x99,y99)) by A4, BINOP_1:def 1

          .= n by A7, A8, XCMPLX_1: 89;

        end;

        then (x,y) equiv (frequency,harmonique) by Th14;

        hence [frequency, harmonique] in ( Class (the Equidistance of S, [1, n])) by EQREL_1: 18;

      end;

      hence thesis;

    end;

    theorem :: MUSIC_S1:20

    

     Th17: for f1,f2,f3 be Element of RAT_Music st (the Ratio of RAT_Music . (f1,f1)) = (the Ratio of RAT_Music . (f2,f3)) holds f2 = f3

    proof

      let f1,f2,f3 be Element of RAT_Music ;

      assume

       A1: (the Ratio of RAT_Music . (f1,f1)) = (the Ratio of RAT_Music . (f2,f3));

      set S = RAT_Music ;

      reconsider x = [f1, f1], y = [f2, f3] as Element of [: RATPLUS , RATPLUS :] by ZFMISC_1:def 2;

      consider y9,z9 be Element of RATPLUS such that

       A2: x = [y9, z9] and

       A3: ( RAT_ratio . x) = ( RAT_ratio (y9,z9)) by Def05;

      consider y99,z99 be Element of RATPLUS such that

       A4: y = [y99, z99] and

       A5: ( RAT_ratio . y) = ( RAT_ratio (y99,z99)) by Def05;

      consider r,s be positive Rational such that

       A6: y9 = r & s = z9 & ( RAT_ratio (y9,z9)) = (s / r) by Def04;

      consider r9,s9 be positive Rational such that

       A7: y99 = r9 & s9 = z99 & ( RAT_ratio (y99,z99)) = (s9 / r9) by Def04;

      

       A8: y9 = f1 & z9 = f1 & y99 = f2 & z99 = f3 by A2, A4, XTUPLE_0: 1;

      ( RAT_ratio . (f1,f1)) = ( RAT_ratio (y9,z9)) & ( RAT_ratio . (f2,f3)) = ( RAT_ratio (y99,z99)) by A5, A3, BINOP_1:def 1;

      hence f2 = f3 by A7, A8, XCMPLX_1: 58, XCMPLX_1: 60, A6, A1;

    end;

    theorem :: MUSIC_S1:21

    for frequency be Element of RAT_Music holds ex r be positive Real st frequency = r & (for n be non zero Nat holds (n * r) is Element of RAT_Music )

    proof

      let frequency be Element of RAT_Music ;

      reconsider r = frequency as positive Rational by Th2;

      take r;

      now

        let n be non zero Nat;

        (n * r) in RATPLUS ;

        hence (n * r) is Element of RAT_Music ;

      end;

      hence thesis;

    end;

    theorem :: MUSIC_S1:22

    

     Th18: for f1,f2,fn1,fm1,fn2,fm2 be Element of RAT_Music holds for r1,r2 be positive Rational holds for n,m be non zero Nat st fn1 = (n * r1) & fm1 = (m * r1) & fn2 = (n * r2) & fm2 = (m * r2) holds (fn1,fm1) equiv (fn2,fm2)

    proof

      let f1,f2,fn1,fm1,fn2,fm2 be Element of RAT_Music ;

      let r1,r2 be positive Rational;

      now

        let n,m be non zero Nat;

        assume

         A1: fn1 = (n * r1) & fm1 = (m * r1) & fn2 = (n * r2) & fm2 = (m * r2);

        reconsider z = [fn1, fm1] as Element of [: RATPLUS , RATPLUS :] by ZFMISC_1:def 2;

        consider x9,y9 be Element of RATPLUS such that

         A2: z = [x9, y9] and

         A3: ( RAT_ratio . z) = ( RAT_ratio (x9,y9)) by Def05;

        consider r,s be positive Rational such that

         A4: x9 = r & s = y9 & ( RAT_ratio (x9,y9)) = (s / r) by Def04;

        reconsider z9 = [fn2, fm2] as Element of [: RATPLUS , RATPLUS :] by ZFMISC_1:def 2;

        consider x99,y99 be Element of RATPLUS such that

         A5: z9 = [x99, y99] and

         A6: ( RAT_ratio . z9) = ( RAT_ratio (x99,y99)) by Def05;

        consider r9,s9 be positive Rational such that

         A7: x99 = r9 & s9 = y99 & ( RAT_ratio (x99,y99)) = (s9 / r9) by Def04;

        now

          thus ( RAT_ratio . (fn1,fm1)) = (s / r) by A3, A4, BINOP_1:def 1;

          thus ( RAT_ratio . (fn2,fm2)) = (s9 / r9) by A6, A7, BINOP_1:def 1;

          r = (n * r1) & s = (m * r1) & r9 = (n * r2) & s9 = (m * r2) by A1, A2, A4, A5, A7, XTUPLE_0: 1;

          then (s / r) = (m qua Real / n qua Real) & (s9 / r9) = (m qua Real / n qua Real) by XCMPLX_1: 91;

          hence (s / r) = (s9 / r9);

        end;

        hence (fn1,fm1) equiv (fn2,fm2) by Th14;

      end;

      hence thesis;

    end;

    theorem :: MUSIC_S1:23

    

     Th19: for f1,f2,f3,f4 be Element of RAT_Music holds ((the Ratio of RAT_Music . (f1,f2)) = (the Ratio of RAT_Music . (f3,f4))) iff (the Ratio of RAT_Music . (f2,f1)) = (the Ratio of RAT_Music . (f4,f3))

    proof

      let f1,f2,f3,f4 be Element of RAT_Music ;

      set MS = RAT_Music ;

      reconsider x = [f1, f2], y = [f3, f4] as Element of [: RATPLUS , RATPLUS :] by ZFMISC_1:def 2;

      consider y9,z9 be Element of RATPLUS such that

       A1: x = [y9, z9] and

       A2: ( RAT_ratio . x) = ( RAT_ratio (y9,z9)) by Def05;

      consider y99,z99 be Element of RATPLUS such that

       A3: y = [y99, z99] and

       A4: ( RAT_ratio . y) = ( RAT_ratio (y99,z99)) by Def05;

      reconsider x1 = [z9, y9], y1 = [z99, y99] as Element of [: RATPLUS , RATPLUS :];

      consider y19,z19 be Element of RATPLUS such that

       A5: x1 = [y19, z19] and

       A6: ( RAT_ratio . x1) = ( RAT_ratio (y19,z19)) by Def05;

      consider y199,z199 be Element of RATPLUS such that

       A7: y1 = [y199, z199] and

       A8: ( RAT_ratio . y1) = ( RAT_ratio (y199,z199)) by Def05;

      

       A9: f1 = y9 & f2 = z9 & f3 = y99 & f4 = z99 by A1, A3, XTUPLE_0: 1;

      then

       A10: f1 = z19 & f2 = y19 & f3 = z199 & f4 = y199 by A5, A7, XTUPLE_0: 1;

      

       A11: (the Ratio of MS . (f2,f1)) = ( RAT_ratio (y19,z19)) & (the Ratio of MS . (f4,f3)) = ( RAT_ratio (y199,z199)) by A9, BINOP_1:def 1, A6, A8;

      hereby

        assume

         A12: ((the Ratio of MS . (f1,f2)) = (the Ratio of MS . (f3,f4)));

        ( RAT_ratio (y9,z9)) = ( RAT_ratio . (f1,f2)) by A2, BINOP_1:def 1

        .= ( RAT_ratio (y99,z99)) by A12, A4, BINOP_1:def 1;

        hence (the Ratio of MS . (f2,f1)) = (the Ratio of MS . (f4,f3)) by A9, A10, A11, Th13;

      end;

      assume

       A13: (the Ratio of MS . (f2,f1)) = (the Ratio of MS . (f4,f3));

      ( RAT_ratio . (f1,f2)) = ( RAT_ratio (z19,y19)) by BINOP_1:def 1, A9, A10, A2

      .= ( RAT_ratio (z199,y199)) by A13, A11, Th13

      .= ( RAT_ratio . (f3,f4)) by BINOP_1:def 1, A9, A10, A4;

      hence ((the Ratio of MS . (f1,f2)) = (the Ratio of MS . (f3,f4)));

    end;

    begin

    definition

      let S be MusicStruct;

      :: MUSIC_S1:def12

      attr S is satisfying_Real means

      : Def07a: the carrier of S c= REALPLUS ;

      :: MUSIC_S1:def13

      attr S is satisfying_equiv means

      : Def08a: for f1,f2,f3,f4 be Element of S holds ((f1,f2) equiv (f3,f4) iff (the Ratio of S . (f1,f2)) = (the Ratio of S . (f3,f4)));

      :: MUSIC_S1:def14

      attr S is satisfying_interval means

      : Def09a: for f1,f2,f3 be Element of S st (the Ratio of S . (f1,f2)) = (the Ratio of S . (f1,f3)) holds f2 = f3;

      :: MUSIC_S1:def15

      attr S is satisfying_tonic means

      : Def10a: for f1,f2,f3 be Element of S st (the Ratio of S . (f1,f1)) = (the Ratio of S . (f2,f3)) holds f2 = f3;

      :: MUSIC_S1:def16

      attr S is satisfying_commutativity means

      : Def11a: for f1,f2,f3,f4 be Element of S holds (the Ratio of S . (f1,f2)) = (the Ratio of S . (f3,f4)) iff (the Ratio of S . (f2,f1)) = (the Ratio of S . (f4,f3));

      :: MUSIC_S1:def17

      attr S is satisfying_Nat means

      : Def12a: NATPLUS c= the carrier of S;

      :: MUSIC_S1:def18

      attr S is satisfying_harmonic_closed means

      : Def13a: for frequency be Element of S holds for n be non zero Nat holds ex harmonique be Element of S st [frequency, harmonique] in ( Class (the Equidistance of S, [1, n]));

    end

    registration

      cluster satisfying_harmonic_closed satisfying_Nat satisfying_commutativity satisfying_tonic satisfying_interval satisfying_equiv satisfying_Real non empty for MusicStruct;

      existence

      proof

        set MS = REAL_Music ;

        take MS;

        thus thesis by Th7, Th8, Th9, Th4, Th10, Th12;

      end;

    end

    definition

      :: original: REAL_Music

      redefine

      func REAL_Music -> satisfying_harmonic_closed satisfying_Nat satisfying_commutativity satisfying_tonic satisfying_interval satisfying_equiv satisfying_Real non empty MusicStruct ;

      coherence

      proof

         REAL_Music is satisfying_harmonic_closed & REAL_Music is satisfying_Nat & REAL_Music is satisfying_commutativity & REAL_Music is satisfying_tonic & REAL_Music is satisfying_interval & REAL_Music is satisfying_equiv & REAL_Music is satisfying_Real by Th9, Th4, Th12, Th10, Th8, Th7;

        hence thesis;

      end;

    end

    definition

      :: original: RAT_Music

      redefine

      func RAT_Music -> satisfying_harmonic_closed satisfying_Nat satisfying_commutativity satisfying_tonic satisfying_interval satisfying_equiv satisfying_Real non empty MusicStruct ;

      coherence

      proof

         RAT_Music is satisfying_harmonic_closed & RAT_Music is satisfying_Nat & RAT_Music is satisfying_commutativity & RAT_Music is satisfying_tonic & RAT_Music is satisfying_interval & RAT_Music is satisfying_equiv & RAT_Music is satisfying_Real by Th14, Th16, Th3, Th19, Th17, Th15;

        hence thesis;

      end;

    end

    theorem :: MUSIC_S1:24

    

     Th20: for S be satisfying_Nat MusicStruct holds for n be non zero Nat holds n is Element of S

    proof

      let S be satisfying_Nat MusicStruct;

      let n be non zero Nat;

      

       A1: NATPLUS c= the carrier of S by Def12a;

      n in NATPLUS by NAT_LAT:def 6;

      hence thesis by A1;

    end;

    theorem :: MUSIC_S1:25

    

     Th21: for MS be satisfying_equiv MusicStruct holds for a,b be Element of MS holds (a,b) equiv (a,b)

    proof

      let MS be satisfying_equiv MusicStruct;

      let a,b be Element of MS;

      (the Ratio of MS . (a,b)) = (the Ratio of MS . (a,b));

      hence thesis by Def08a;

    end;

    theorem :: MUSIC_S1:26

    

     Th22: for MS be satisfying_equiv MusicStruct holds for a,b,c,d be Element of MS holds (a,b) equiv (c,d) iff (c,d) equiv (a,b)

    proof

      let MS be satisfying_equiv MusicStruct;

      let a,b,c,d be Element of MS;

      hereby

        assume (a,b) equiv (c,d);

        then (the Ratio of MS . (a,b)) = (the Ratio of MS . (c,d)) by Def08a;

        hence (c,d) equiv (a,b) by Def08a;

      end;

      assume (c,d) equiv (a,b);

      then (the Ratio of MS . (a,b)) = (the Ratio of MS . (c,d)) by Def08a;

      hence (a,b) equiv (c,d) by Def08a;

    end;

    theorem :: MUSIC_S1:27

    

     Th23: for MS be satisfying_equiv MusicStruct holds for a,b,c,d,e,f be Element of MS holds (a,b) equiv (c,d) & (c,d) equiv (e,f) implies (a,b) equiv (e,f)

    proof

      let MS be satisfying_equiv MusicStruct;

      let a,b,c,d,e,f be Element of MS;

      assume (a,b) equiv (c,d) & (c,d) equiv (e,f);

      then (the Ratio of MS . (a,b)) = (the Ratio of MS . (c,d)) & (the Ratio of MS . (c,d)) = (the Ratio of MS . (e,f)) by Def08a;

      hence thesis by Def08a;

    end;

    theorem :: MUSIC_S1:28

    

     Th24: for S be satisfying_interval satisfying_equiv MusicStruct holds for a,b,c be Element of S holds ((a,b) equiv (a,c) iff b = c)

    proof

      let S be satisfying_interval satisfying_equiv MusicStruct;

      let a,b,c be Element of S;

      now

        assume (a,b) equiv (a,c);

        then (the Ratio of S . (a,b)) = (the Ratio of S . (a,c)) by Def08a;

        hence b = c by Def09a;

      end;

      hence thesis by Th21;

    end;

    reserve MS for satisfying_equiv MusicStruct;

    reserve a,b,c,d,e,f for Element of MS;

    theorem :: MUSIC_S1:29

    (a,a) equiv (a,a)

    proof

      (the Ratio of MS . (a,a)) = (the Ratio of MS . (a,a));

      hence thesis by Def08a;

    end;

    theorem :: MUSIC_S1:30

    

     Th25: the Equidistance of MS is_reflexive_in [:the carrier of MS, the carrier of MS:]

    proof

      set R = the Equidistance of MS, C = [:the carrier of MS, the carrier of MS:];

      now

        let x be object;

        assume x in C;

        then

        consider y,z be object such that

         A1: y in the carrier of MS and

         A2: z in the carrier of MS and

         A3: x = [y, z] by ZFMISC_1:def 2;

        reconsider y, z as Element of MS by A1, A2;

        (y,z) equiv (y,z) by Th21;

        hence [x, x] in R by A3;

      end;

      hence thesis by RELAT_2:def 1;

    end;

    theorem :: MUSIC_S1:31

    MS is non empty implies the Equidistance of MS is reflexive & ( field the Equidistance of MS) = [:the carrier of MS, the carrier of MS:]

    proof

      assume

       A1: MS is non empty;

      the Equidistance of MS is_reflexive_in [:the carrier of MS, the carrier of MS:] by Th25;

      hence thesis by A1, PARTIT_2: 21;

    end;

    theorem :: MUSIC_S1:32

    

     Th26: the Equidistance of MS is_symmetric_in [:the carrier of MS, the carrier of MS:]

    proof

      set R = the Equidistance of MS, C = [:the carrier of MS, the carrier of MS:];

      now

        let x,y be object;

        assume that

         A1: x in C and

         A2: y in C and

         A3: [x, y] in R;

        consider x1,x2 be object such that

         A4: x1 in the carrier of MS and

         A5: x2 in the carrier of MS and

         A6: x = [x1, x2] by A1, ZFMISC_1:def 2;

        consider y1,y2 be object such that

         A7: y1 in the carrier of MS and

         A8: y2 in the carrier of MS and

         A9: y = [y1, y2] by A2, ZFMISC_1:def 2;

        reconsider x1, x2, y1, y2 as Element of MS by A4, A5, A7, A8;

        (x1,x2) equiv (y1,y2) by A3, A6, A9;

        then (y1,y2) equiv (x1,x2) by Th22;

        hence [y, x] in R by A6, A9;

      end;

      hence thesis by RELAT_2:def 3;

    end;

    theorem :: MUSIC_S1:33

    

     Th27: the Equidistance of MS is_transitive_in [:the carrier of MS, the carrier of MS:]

    proof

      set R = the Equidistance of MS, C = [:the carrier of MS, the carrier of MS:];

      now

        let x,y,z be object;

        assume that

         A1: x in C and

         A2: y in C and

         A3: z in C and

         A4: [x, y] in R and

         A5: [y, z] in R;

        consider x1,x2 be object such that

         A6: x1 in the carrier of MS and

         A7: x2 in the carrier of MS and

         A8: x = [x1, x2] by A1, ZFMISC_1:def 2;

        consider y1,y2 be object such that

         A9: y1 in the carrier of MS and

         A10: y2 in the carrier of MS and

         A11: y = [y1, y2] by A2, ZFMISC_1:def 2;

        consider z1,z2 be object such that

         A12: z1 in the carrier of MS and

         A13: z2 in the carrier of MS and

         A14: z = [z1, z2] by A3, ZFMISC_1:def 2;

        reconsider x1, x2, y1, y2, z1, z2 as Element of MS by A6, A7, A9, A10, A12, A13;

        (x1,x2) equiv (y1,y2) & (y1,y2) equiv (z1,z2) by A4, A5, A8, A11, A14;

        then (x1,x2) equiv (z1,z2) by Th23;

        hence [x, z] in R by A8, A14;

      end;

      hence thesis by RELAT_2:def 8;

    end;

    theorem :: MUSIC_S1:34

    the Equidistance of MS is Equivalence_Relation of [:the carrier of MS, the carrier of MS:]

    proof

      set R = the Equidistance of MS, C = [:the carrier of MS, the carrier of MS:];

      now

        ( dom R) = C by Th25, TAXONOM1: 3;

        hence R is total by PARTFUN1:def 2;

        ( field R) = C & R is_symmetric_in C by Th25, Th26, PARTIT_2: 9;

        hence R is symmetric by RELAT_2:def 11;

        ( field R) = C & R is_transitive_in C by Th25, Th27, PARTIT_2: 9;

        hence R is transitive by RELAT_2:def 16;

      end;

      hence thesis;

    end;

    theorem :: MUSIC_S1:35

    

     Th28: for MS be satisfying_commutativity satisfying_equiv MusicStruct holds for a,b,c,d be Element of MS holds (a,b) equiv (c,d) iff (b,a) equiv (d,c)

    proof

      let MS be satisfying_commutativity satisfying_equiv MusicStruct;

      let a,b,c,d be Element of MS;

      hereby

        assume (a,b) equiv (c,d);

        then (the Ratio of MS . (a,b)) = (the Ratio of MS . (c,d)) by Def08a;

        then (the Ratio of MS . (b,a)) = (the Ratio of MS . (d,c)) by Def11a;

        hence (b,a) equiv (d,c) by Def08a;

      end;

      assume (b,a) equiv (d,c);

      then (the Ratio of MS . (b,a)) = (the Ratio of MS . (d,c)) by Def08a;

      then (the Ratio of MS . (a,b)) = (the Ratio of MS . (c,d)) by Def11a;

      hence (a,b) equiv (c,d) by Def08a;

    end;

    theorem :: MUSIC_S1:36

    

     Th29: for S be satisfying_tonic satisfying_equiv MusicStruct holds for a,b,c be Element of S st (a,a) equiv (b,c) holds b = c

    proof

      let S be satisfying_tonic satisfying_equiv MusicStruct;

      let a,b,c be Element of S;

      assume (a,a) equiv (b,c);

      then (the Ratio of S . (a,a)) = (the Ratio of S . (b,c)) by Def08a;

      hence thesis by Def10a;

    end;

    definition

      let S be satisfying_Nat satisfying_interval satisfying_harmonic_closed satisfying_equiv MusicStruct;

      let frequency be Element of S;

      let n be non zero Nat;

      :: MUSIC_S1:def19

      func n -harmonique (S,frequency) -> Element of S means

      : Def08b: [frequency, it ] in ( Class (the Equidistance of S, [1, n]));

      existence by Def13a;

      uniqueness

      proof

        let h1,h2 be Element of S such that

         A1: [frequency, h1] in ( Class (the Equidistance of S, [1, n])) and

         A2: [frequency, h2] in ( Class (the Equidistance of S, [1, n]));

        reconsider x = 1, y = n as Element of S by Th20;

        now

          (x,y) equiv (frequency,h1) by A1, EQREL_1: 18;

          hence (the Ratio of S . (x,y)) = (the Ratio of S . (frequency,h1)) by Def08a;

          (x,y) equiv (frequency,h2) by A2, EQREL_1: 18;

          hence (the Ratio of S . (x,y)) = (the Ratio of S . (frequency,h2)) by Def08a;

        end;

        then (frequency,h1) equiv (frequency,h2) by Def08a;

        hence thesis by Th24;

      end;

    end

    definition

      let S be satisfying_Nat satisfying_interval satisfying_harmonic_closed satisfying_equiv MusicStruct;

      :: MUSIC_S1:def20

      attr S is satisfying_linearite_harmonique means

      : Def09: for frequency be Element of S holds for n be non zero Nat holds ex fr be positive Real st frequency = fr & (n -harmonique (S,frequency)) = (n * fr);

    end

    theorem :: MUSIC_S1:37

    

     Th30: REAL_Music is satisfying_linearite_harmonique

    proof

      set MS = REAL_Music ;

      now

        let frequency be Element of MS;

        let n be non zero Nat;

        reconsider fr = frequency as positive Real by Th1;

        take fr;

        thus frequency = fr;

        reconsider n1 = 1, n2 = n as Element of MS by Th20;

        reconsider f2 = (n * fr) as Element of MS by Th1;

        reconsider x = [n1, n2], y = [frequency, f2] as Element of [: REALPLUS , REALPLUS :];

        now

          thus [frequency, (n -harmonique (MS,frequency))] in ( Class (the Equidistance of MS, [1, n])) by Def08b;

          now

            thus (the Ratio of MS . (n1,n2)) = ( REAL_ratio . (n1,n2));

            thus (the Ratio of MS . (frequency,f2)) = ( REAL_ratio . (frequency,f2));

            now

              reconsider n19 = n1, n29 = n2, fr9 = fr, f29 = f2 as Element of REALPLUS ;

              consider r,s be positive Real such that

               A1: n19 = r & n29 = s & ( REAL_ratio (n19,n29)) = (s / r) by Def01;

              consider r9,s9 be positive Real such that

               A2: fr9 = r9 & f29 = s9 & ( REAL_ratio (fr9,f29)) = (s9 / r9) by Def01;

              consider y9,z9 be Element of REALPLUS such that

               A3: x = [y9, z9] and

               A4: ( REAL_ratio . x) = ( REAL_ratio (y9,z9)) by Def02;

              consider y99,z99 be Element of REALPLUS such that

               A5: y = [y99, z99] and

               A6: ( REAL_ratio . y) = ( REAL_ratio (y99,z99)) by Def02;

              

               A7: y9 = n1 & z9 = n2 & y99 = frequency & z99 = f2 by A3, A5, XTUPLE_0: 1;

              hence ( REAL_ratio . (n1,n2)) = n by A1, A4, BINOP_1:def 1;

              

              thus ( REAL_ratio . (frequency,f2)) = (s9 / r9) by A2, A7, A6, BINOP_1:def 1

              .= n by A2, XCMPLX_1: 89;

            end;

            hence ( REAL_ratio . (n1,n2)) = ( REAL_ratio . (frequency,f2));

          end;

          then (n1,n2) equiv (frequency,f2) by Def08a;

          hence [frequency, f2] in ( Class (the Equidistance of MS, [1, n])) by EQREL_1: 18;

        end;

        hence (n -harmonique (MS,frequency)) = (n * fr) by Def08b;

      end;

      hence thesis;

    end;

    theorem :: MUSIC_S1:38

    

     Th31: RAT_Music is satisfying_linearite_harmonique

    proof

      set MS = RAT_Music ;

      now

        let frequency be Element of MS;

        let n be non zero Nat;

        reconsider fr = frequency as positive Rational by Th2;

        reconsider fr2 = fr as positive Real;

        take fr2;

        thus frequency = fr2;

        reconsider n1 = 1, n2 = n as Element of MS by Th20;

        reconsider f2 = (n * fr) as Element of MS by Th2;

        reconsider x = [n1, n2], y = [frequency, f2] as Element of [: RATPLUS , RATPLUS :];

        now

          thus [frequency, (n -harmonique (MS,frequency))] in ( Class (the Equidistance of MS, [1, n])) by Def08b;

          now

            thus (the Ratio of MS . (n1,n2)) = ( RAT_ratio . (n1,n2));

            thus (the Ratio of MS . (frequency,f2)) = ( RAT_ratio . (frequency,f2));

            now

              reconsider n19 = n1, n29 = n2, fr9 = fr, f29 = f2 as Element of RATPLUS ;

              consider r,s be positive Rational such that

               A1: n19 = r & n29 = s & ( RAT_ratio (n19,n29)) = (s / r) by Def04;

              consider r9,s9 be positive Rational such that

               A2: fr9 = r9 & f29 = s9 & ( RAT_ratio (fr9,f29)) = (s9 / r9) by Def04;

              consider y9,z9 be Element of RATPLUS such that

               A3: x = [y9, z9] and

               A4: ( RAT_ratio . x) = ( RAT_ratio (y9,z9)) by Def05;

              consider y99,z99 be Element of RATPLUS such that

               A5: y = [y99, z99] and

               A6: ( RAT_ratio . y) = ( RAT_ratio (y99,z99)) by Def05;

              

               A7: y9 = n1 & z9 = n2 & y99 = frequency & z99 = f2 by A3, A5, XTUPLE_0: 1;

              hence ( RAT_ratio . (n1,n2)) = n by A1, A4, BINOP_1:def 1;

              

              thus ( RAT_ratio . (frequency,f2)) = (s9 / r9) by A2, A7, A6, BINOP_1:def 1

              .= n by A2, XCMPLX_1: 89;

            end;

            hence ( RAT_ratio . (n1,n2)) = ( RAT_ratio . (frequency,f2));

          end;

          then (n1,n2) equiv (frequency,f2) by Def08a;

          hence [frequency, f2] in ( Class (the Equidistance of MS, [1, n])) by EQREL_1: 18;

        end;

        hence (n -harmonique (MS,frequency)) = (n * fr2) by Def08b;

      end;

      hence thesis;

    end;

    registration

      cluster satisfying_linearite_harmonique for satisfying_harmonic_closed satisfying_Nat satisfying_commutativity satisfying_tonic satisfying_interval satisfying_equiv satisfying_Real non empty MusicStruct;

      existence by Th30;

    end

    definition

      :: original: REAL_Music

      redefine

      func REAL_Music -> satisfying_linearite_harmonique satisfying_harmonic_closed satisfying_Nat satisfying_commutativity satisfying_tonic satisfying_interval satisfying_equiv satisfying_Real non empty MusicStruct ;

      coherence by Th30;

    end

    definition

      :: original: RAT_Music

      redefine

      func RAT_Music -> satisfying_linearite_harmonique satisfying_harmonic_closed satisfying_Nat satisfying_commutativity satisfying_tonic satisfying_interval satisfying_equiv satisfying_Real non empty MusicStruct ;

      coherence by Th31;

    end

    definition

      let MS be satisfying_harmonic_closed satisfying_Nat satisfying_interval satisfying_equiv MusicStruct;

      :: MUSIC_S1:def21

      attr MS is satisfying_harmonique_stable means

      : Def10: for f1,f2 be Element of MS holds for n,m be non zero Nat holds ((n -harmonique (MS,f1)),(m -harmonique (MS,f1))) equiv ((n -harmonique (MS,f2)),(m -harmonique (MS,f2)));

    end

    theorem :: MUSIC_S1:39

    

     Th32: REAL_Music is satisfying_harmonique_stable

    proof

      set MS = REAL_Music ;

      let f1,f2 be Element of MS;

      let n,m be non zero Nat;

      reconsider r1 = f1, r2 = f2 as positive Real by Th1;

      (ex fr1 be positive Real st fr1 = f1 & (n -harmonique (MS,f1)) = (n * fr1)) & (ex fr2 be positive Real st fr2 = f1 & (m -harmonique (MS,f1)) = (m * fr2)) & (ex fr3 be positive Real st fr3 = f2 & (n -harmonique (MS,f2)) = (n * fr3)) & (ex fr4 be positive Real st fr4 = f2 & (m -harmonique (MS,f2)) = (m * fr4)) by Def09;

      hence ((n -harmonique (MS,f1)),(m -harmonique (MS,f1))) equiv ((n -harmonique (MS,f2)),(m -harmonique (MS,f2))) by Th11;

    end;

    theorem :: MUSIC_S1:40

    

     Th33: RAT_Music is satisfying_harmonique_stable

    proof

      set MS = RAT_Music ;

      now

        let f1,f2 be Element of MS;

        let n,m be non zero Nat;

        set fn1 = (n -harmonique (MS,f1)), fm1 = (m -harmonique (MS,f1)), fn2 = (n -harmonique (MS,f2)), fm2 = (m -harmonique (MS,f2));

        reconsider r1 = f1, r2 = f2 as positive Rational by Th2;

        consider fr1 be positive Real such that

         A1: fr1 = f1 and

         A2: (n -harmonique (MS,f1)) = (n * fr1) by Def09;

        consider fr2 be positive Real such that

         A3: fr2 = f1 and

         A4: (m -harmonique (MS,f1)) = (m * fr2) by Def09;

        consider fr3 be positive Real such that

         A5: fr3 = f2 and

         A6: (n -harmonique (MS,f2)) = (n * fr3) by Def09;

        consider fr4 be positive Real such that

         A7: fr4 = f2 and

         A8: (m -harmonique (MS,f2)) = (m * fr4) by Def09;

        fn1 = (n * r1) & fm1 = (m * r1) & fn2 = (n * r2) & fm2 = (m * r2) by A1, A2, A3, A4, A5, A6, A7, A8;

        hence ((n -harmonique (MS,f1)),(m -harmonique (MS,f1))) equiv ((n -harmonique (MS,f2)),(m -harmonique (MS,f2))) by Th18;

      end;

      hence thesis;

    end;

    registration

      cluster satisfying_harmonique_stable for satisfying_linearite_harmonique satisfying_harmonic_closed satisfying_Nat satisfying_commutativity satisfying_tonic satisfying_interval satisfying_equiv satisfying_Real non empty MusicStruct;

      existence by Th32;

    end

    definition

      :: original: REAL_Music

      redefine

      func REAL_Music -> satisfying_harmonique_stable satisfying_linearite_harmonique satisfying_harmonic_closed satisfying_Nat satisfying_commutativity satisfying_tonic satisfying_interval satisfying_equiv satisfying_Real non empty MusicStruct ;

      coherence by Th32;

    end

    definition

      :: original: RAT_Music

      redefine

      func RAT_Music -> satisfying_harmonique_stable satisfying_linearite_harmonique satisfying_harmonic_closed satisfying_Nat satisfying_commutativity satisfying_tonic satisfying_interval satisfying_equiv satisfying_Real non empty MusicStruct ;

      coherence by Th33;

    end

    definition

      let MS be satisfying_harmonic_closed satisfying_Nat satisfying_interval satisfying_equiv MusicStruct;

      let frequency be Element of MS;

      :: MUSIC_S1:def22

      func unison (MS,frequency) -> Subset of [:the carrier of MS, the carrier of MS:] equals ( Class (the Equidistance of MS, [(1 -harmonique (MS,frequency)), (1 -harmonique (MS,frequency))]));

      coherence ;

      :: MUSIC_S1:def23

      func octave (MS,frequency) -> Subset of [:the carrier of MS, the carrier of MS:] equals ( Class (the Equidistance of MS, [(1 -harmonique (MS,frequency)), (2 -harmonique (MS,frequency))]));

      coherence ;

      :: MUSIC_S1:def24

      func fifth (MS,frequency) -> Subset of [:the carrier of MS, the carrier of MS:] equals ( Class (the Equidistance of MS, [(2 -harmonique (MS,frequency)), (3 -harmonique (MS,frequency))]));

      coherence ;

      :: MUSIC_S1:def25

      func fourth (MS,frequency) -> Subset of [:the carrier of MS, the carrier of MS:] equals ( Class (the Equidistance of MS, [(3 -harmonique (MS,frequency)), (4 -harmonique (MS,frequency))]));

      coherence ;

      :: MUSIC_S1:def26

      func major_sixth (MS,frequency) -> Subset of [:the carrier of MS, the carrier of MS:] equals ( Class (the Equidistance of MS, [(3 -harmonique (MS,frequency)), (5 -harmonique (MS,frequency))]));

      coherence ;

      :: MUSIC_S1:def27

      func major_third (MS,frequency) -> Subset of [:the carrier of MS, the carrier of MS:] equals ( Class (the Equidistance of MS, [(4 -harmonique (MS,frequency)), (5 -harmonique (MS,frequency))]));

      coherence ;

      :: MUSIC_S1:def28

      func minor_third (MS,frequency) -> Subset of [:the carrier of MS, the carrier of MS:] equals ( Class (the Equidistance of MS, [(5 -harmonique (MS,frequency)), (6 -harmonique (MS,frequency))]));

      coherence ;

      :: MUSIC_S1:def29

      func minor_sixth (MS,frequency) -> Subset of [:the carrier of MS, the carrier of MS:] equals ( Class (the Equidistance of MS, [(5 -harmonique (MS,frequency)), (8 -harmonique (MS,frequency))]));

      coherence ;

      :: MUSIC_S1:def30

      func major_tone (MS,frequency) -> Subset of [:the carrier of MS, the carrier of MS:] equals ( Class (the Equidistance of MS, [(8 -harmonique (MS,frequency)), (9 -harmonique (MS,frequency))]));

      coherence ;

      :: MUSIC_S1:def31

      func minor_tone (MS,frequency) -> Subset of [:the carrier of MS, the carrier of MS:] equals ( Class (the Equidistance of MS, [(9 -harmonique (MS,frequency)), (10 -harmonique (MS,frequency))]));

      coherence ;

    end

    definition

      let MS be satisfying_harmonic_closed satisfying_Nat satisfying_interval satisfying_equiv MusicStruct;

      :: MUSIC_S1:def32

      func unison (MS) -> Subset of [:the carrier of MS, the carrier of MS:] equals ( Class (the Equidistance of MS, [1, 1]));

      coherence ;

      :: MUSIC_S1:def33

      func octave (MS) -> Subset of [:the carrier of MS, the carrier of MS:] equals ( Class (the Equidistance of MS, [1, 2]));

      coherence ;

      :: MUSIC_S1:def34

      func fifth (MS) -> Subset of [:the carrier of MS, the carrier of MS:] equals ( Class (the Equidistance of MS, [2, 3]));

      coherence ;

      :: MUSIC_S1:def35

      func fourth (MS) -> Subset of [:the carrier of MS, the carrier of MS:] equals ( Class (the Equidistance of MS, [3, 4]));

      coherence ;

      :: MUSIC_S1:def36

      func major_sixth (MS) -> Subset of [:the carrier of MS, the carrier of MS:] equals ( Class (the Equidistance of MS, [3, 5]));

      coherence ;

      :: MUSIC_S1:def37

      func major_third (MS) -> Subset of [:the carrier of MS, the carrier of MS:] equals ( Class (the Equidistance of MS, [4, 5]));

      coherence ;

      :: MUSIC_S1:def38

      func minor_third (MS) -> Subset of [:the carrier of MS, the carrier of MS:] equals ( Class (the Equidistance of MS, [5, 6]));

      coherence ;

      :: MUSIC_S1:def39

      func minor_sixth (MS) -> Subset of [:the carrier of MS, the carrier of MS:] equals ( Class (the Equidistance of MS, [5, 8]));

      coherence ;

      :: MUSIC_S1:def40

      func major_tone (MS) -> Subset of [:the carrier of MS, the carrier of MS:] equals ( Class (the Equidistance of MS, [8, 9]));

      coherence ;

      :: MUSIC_S1:def41

      func minor_tone (MS) -> Subset of [:the carrier of MS, the carrier of MS:] equals ( Class (the Equidistance of MS, [9, 10]));

      coherence ;

    end

    definition

      let S be satisfying_harmonic_closed satisfying_Nat satisfying_interval satisfying_equiv MusicStruct;

      :: MUSIC_S1:def42

      attr S is satisfying_fifth_constructible means

      : Def11: for frequency be Element of S holds ex q be Element of S st [frequency, q] in ( fifth S);

    end

    theorem :: MUSIC_S1:41

    

     Th34: for frequency be Element of REAL_Music holds ex fr,qr be positive Real st fr = frequency & qr = ((3 qua Real / 2) * fr) & [fr, qr] in ( fifth REAL_Music )

    proof

      set MS = REAL_Music ;

      now

        let frequency be Element of MS;

        reconsider f = frequency as positive Real by Th1;

        reconsider qr = ((3 qua Real / 2) * f) as positive Real;

        reconsider q = qr as Element of MS by Th1;

        take f, qr;

        thus f = frequency;

        thus qr = ((3 qua Real / 2) * f);

        reconsider n2 = 2, n3 = 3 as Element of MS by Th20;

        reconsider x = [n2, n3], y = [frequency, q] as Element of [: REALPLUS , REALPLUS :];

        reconsider z = [frequency, q] as Element of [: REALPLUS , REALPLUS :];

        consider x9,y9 be Element of REALPLUS such that

         A1: z = [x9, y9] and

         A2: ( REAL_ratio . z) = ( REAL_ratio (x9,y9)) by Def02;

        consider r,s be positive Real such that

         A3: x9 = r & s = y9 & ( REAL_ratio (x9,y9)) = (s / r) by Def01;

        consider x99,y99 be Element of REALPLUS such that

         A4: x = [x99, y99] and

         A5: ( REAL_ratio . x) = ( REAL_ratio (x99,y99)) by Def02;

        consider r9,s9 be positive Real such that

         A6: x99 = r9 & s9 = y99 & ( REAL_ratio (x99,y99)) = (s9 / r9) by Def01;

        

         A7: n2 = r9 & n3 = s9 & r = frequency & s = q by A3, A1, A4, A6, XTUPLE_0: 1;

        now

          thus ( REAL_ratio . (n2,n3)) = (3 qua Real / 2 qua Real) by A6, A7, A5, BINOP_1:def 1;

          

          thus ( REAL_ratio . (frequency,q)) = (s / r) by A2, A3, BINOP_1:def 1

          .= (3 qua Real / 2) by A7, XCMPLX_1: 89;

        end;

        then (n2,n3) equiv (frequency,q) by Def08a;

        hence [f, qr] in ( fifth MS) by EQREL_1: 18;

      end;

      hence thesis;

    end;

    theorem :: MUSIC_S1:42

    

     Th35: REAL_Music is satisfying_fifth_constructible

    proof

      set MS = REAL_Music ;

      let frequency be Element of MS;

      consider fr,qr be positive Real such that

       A1: fr = frequency and qr = ((3 qua Real / 2) * fr) and

       A2: [fr, qr] in ( fifth MS) by Th34;

      fr is Element of MS & qr is Element of MS by Th1;

      hence thesis by A1, A2;

    end;

    theorem :: MUSIC_S1:43

    

     Th36: for frequency be Element of RAT_Music holds ex fr,qr be positive Rational st fr = frequency & qr = ((3 qua Rational / 2) * fr) & [fr, qr] in ( fifth RAT_Music )

    proof

      set MS = RAT_Music ;

      now

        let frequency be Element of MS;

        reconsider f = frequency as positive Rational by Th2;

        reconsider qr = ((3 qua Rational / 2) * f) as positive Rational;

        reconsider q = qr as Element of MS by Th2;

        take f, qr;

        thus f = frequency;

        thus qr = ((3 qua Rational / 2) * f);

        reconsider n2 = 2, n3 = 3 as Element of MS by Th20;

        reconsider x = [n2, n3], y = [frequency, q] as Element of [: RATPLUS , RATPLUS :];

        reconsider z = [frequency, q] as Element of [: RATPLUS , RATPLUS :];

        consider x9,y9 be Element of RATPLUS such that

         A1: z = [x9, y9] and

         A2: ( RAT_ratio . z) = ( RAT_ratio (x9,y9)) by Def05;

        consider r,s be positive Rational such that

         A3: x9 = r & s = y9 & ( RAT_ratio (x9,y9)) = (s / r) by Def04;

        consider x99,y99 be Element of RATPLUS such that

         A4: x = [x99, y99] and

         A5: ( RAT_ratio . x) = ( RAT_ratio (x99,y99)) by Def05;

        consider r9,s9 be positive Rational such that

         A6: x99 = r9 & s9 = y99 & ( RAT_ratio (x99,y99)) = (s9 / r9) by Def04;

        

         A7: n2 = r9 & n3 = s9 & r = frequency & s = q by A3, A1, A4, A6, XTUPLE_0: 1;

        now

          thus ( RAT_ratio . (n2,n3)) = (3 qua Real / 2 qua Real) by A5, A6, A7, BINOP_1:def 1;

          

          thus ( RAT_ratio . (frequency,q)) = ( RAT_ratio (x9,y9)) by A2, BINOP_1:def 1

          .= (3 qua Rational / 2) by A3, A7, XCMPLX_1: 89;

        end;

        then (n2,n3) equiv (frequency,q) by Def08a;

        hence [f, qr] in ( fifth MS) by EQREL_1: 18;

      end;

      hence thesis;

    end;

    theorem :: MUSIC_S1:44

    

     Th37: RAT_Music is satisfying_fifth_constructible

    proof

      set MS = RAT_Music ;

      let frequency be Element of MS;

      consider fr,qr be positive Rational such that

       A1: fr = frequency and qr = ((3 qua Rational / 2) * fr) and

       A2: [fr, qr] in ( fifth MS) by Th36;

      fr is Element of MS & qr is Element of MS by Th2;

      hence thesis by A1, A2;

    end;

    registration

      cluster satisfying_fifth_constructible for satisfying_harmonique_stable satisfying_linearite_harmonique satisfying_harmonic_closed satisfying_Nat satisfying_commutativity satisfying_tonic satisfying_interval satisfying_equiv satisfying_Real non empty MusicStruct;

      existence by Th35;

    end

    definition

      :: original: REAL_Music

      redefine

      func REAL_Music -> satisfying_fifth_constructible satisfying_harmonique_stable satisfying_linearite_harmonique satisfying_harmonic_closed satisfying_Nat satisfying_commutativity satisfying_tonic satisfying_interval satisfying_equiv satisfying_Real non empty MusicStruct ;

      coherence by Th35;

    end

    definition

      :: original: RAT_Music

      redefine

      func RAT_Music -> satisfying_fifth_constructible satisfying_harmonique_stable satisfying_linearite_harmonique satisfying_harmonic_closed satisfying_Nat satisfying_commutativity satisfying_tonic satisfying_interval satisfying_equiv satisfying_Real non empty MusicStruct ;

      coherence by Th37;

    end

    definition

      let MS be satisfying_fifth_constructible satisfying_harmonic_closed satisfying_Nat satisfying_interval satisfying_equiv MusicStruct;

      let frequency be Element of MS;

      :: MUSIC_S1:def43

      func Fifth (MS,frequency) -> Element of MS means

      : Def11bis: [frequency, it ] in ( fifth MS);

      existence by Def11;

      uniqueness

      proof

        let q1,q2 be Element of MS such that

         A1: [frequency, q1] in ( fifth MS) and

         A2: [frequency, q2] in ( fifth MS);

        reconsider n2 = 2, n3 = 3 as Element of MS by Th20;

        

         A3: (n2,n3) equiv (frequency,q1) by A1, EQREL_1: 18;

        (n2,n3) equiv (frequency,q2) by A2, EQREL_1: 18;

        then (frequency,q2) equiv (n2,n3) by Th22;

        hence thesis by A3, Th23, Th24;

      end;

    end

    theorem :: MUSIC_S1:45

    for MS be satisfying_fifth_constructible satisfying_harmonique_stable satisfying_linearite_harmonique satisfying_harmonic_closed satisfying_Nat satisfying_interval satisfying_equiv MusicStruct holds for frequency be Element of MS holds ( fifth (MS,frequency)) = ( fifth MS)

    proof

      let MS be satisfying_fifth_constructible satisfying_harmonique_stable satisfying_linearite_harmonique satisfying_harmonic_closed satisfying_Nat satisfying_interval satisfying_equiv MusicStruct;

      let frequency be Element of MS;

       A0:

      now

        let x be object;

        assume

         A1: x in ( fifth (MS,frequency));

        then

        consider x1,x2 be object such that

         A2: x1 in the carrier of MS and

         A3: x2 in the carrier of MS and

         A4: x = [x1, x2] by ZFMISC_1:def 2;

        reconsider x1, x2 as Element of MS by A2, A3;

        reconsider y = 1, y1 = 2, y2 = 3 as Element of MS by Th20;

        set z = (2 -harmonique (MS,frequency)), t = (3 -harmonique (MS,frequency));

        reconsider n = 2, m = 3 as non zero Nat;

        consider r1 be positive Real such that

         A5: y = r1 and

         A6: (n -harmonique (MS,y)) = (n * r1) by Def09;

        consider r2 be positive Real such that

         A7: y = r2 and

         A8: (m -harmonique (MS,y)) = (m * r2) by Def09;

        set a = (n -harmonique (MS,frequency)), b = (m -harmonique (MS,frequency));

        

         A9: (a,b) equiv (x1,x2) by A1, A4, EQREL_1: 18;

        (y1,y2) equiv (a,b) by A5, A6, A7, A8, Def10;

        then (y1,y2) equiv (x1,x2) by A9, Th23;

        hence x in ( fifth MS) by A4, EQREL_1: 18;

      end;

      now

        let x be object;

        assume

         A11: x in ( fifth MS);

        then

        consider x1,x2 be object such that

         A12: x1 in the carrier of MS and

         A13: x2 in the carrier of MS and

         A14: x = [x1, x2] by ZFMISC_1:def 2;

        reconsider x1, x2 as Element of MS by A12, A13;

        reconsider y = 2, z = 3 as Element of MS by Th20;

        reconsider y9 = y as positive Real;

        reconsider n = 2, m = 3 as non zero Nat;

        set a = (n -harmonique (MS,frequency)), b = (m -harmonique (MS,frequency)), c = (n -harmonique (MS,y)), d = (m -harmonique (MS,y));

        

         A15: (a,b) equiv (c,d) by Def10;

        reconsider n0 = 1, n1 = 2, n2 = 3 as Element of MS by Th20;

        consider r1 be positive Real such that

         A16: n0 = r1 and

         A17: (n -harmonique (MS,n0)) = (n * r1) by Def09;

        consider r2 be positive Real such that

         A18: n0 = r2 and

         A19: (m -harmonique (MS,n0)) = (m * r2) by Def09;

        

         A20: ((n -harmonique (MS,n0)),(m -harmonique (MS,n0))) equiv (x1,x2) by A16, A17, A18, A19, A11, A14, EQREL_1: 18;

        (c,d) equiv ((n -harmonique (MS,n0)),(m -harmonique (MS,n0))) by Def10;

        then (c,d) equiv (x1,x2) by A20, Th23;

        then (a,b) equiv (x1,x2) by A15, Th23;

        hence x in ( fifth (MS,frequency)) by A14, EQREL_1: 18;

      end;

      hence thesis by A0;

    end;

    theorem :: MUSIC_S1:46

    

     Th38: for frequency be Element of REAL_Music holds ex fr be positive Real st frequency = fr & ( Fifth ( REAL_Music ,frequency)) = ((3 qua Real / 2) * fr)

    proof

      set MS = REAL_Music ;

      let frequency be Element of MS;

      reconsider fr = frequency as positive Real by Th1;

      take fr;

      thus frequency = fr;

      consider fr9,qr9 be positive Real such that

       A1: fr9 = frequency and

       A2: qr9 = ((3 qua Real / 2) * fr9) and

       A3: [fr9, qr9] in ( fifth MS) by Th34;

      reconsider qr9 as Element of MS by Th1;

      qr9 = ( Fifth (MS,frequency)) by A1, A3, Def11bis;

      hence thesis by A1, A2;

    end;

    theorem :: MUSIC_S1:47

    

     Th39: for frequency be Element of RAT_Music holds ex fr be positive Rational st frequency = fr & ( Fifth ( RAT_Music ,frequency)) = ((3 qua Rational / 2) * fr)

    proof

      set MS = RAT_Music ;

      let frequency be Element of MS;

      reconsider fr = frequency as positive Rational by Th2;

      take fr;

      thus frequency = fr;

      consider fr9,qr9 be positive Rational such that

       A1: fr9 = frequency and

       A2: qr9 = ((3 qua Rational / 2) * fr9) and

       A3: [fr9, qr9] in ( fifth MS) by Th36;

      reconsider qr9 as Element of MS by Th2;

      qr9 = ( Fifth (MS,frequency)) by A1, A3, Def11bis;

      hence thesis by A1, A2;

    end;

    definition

      let MS be satisfying_fifth_constructible satisfying_harmonic_closed satisfying_Nat satisfying_interval satisfying_equiv MusicStruct;

      :: MUSIC_S1:def44

      attr MS is classical_fifth means

      : Def12: for frequency be Element of MS holds ex fr be positive Real st frequency = fr & ( Fifth (MS,frequency)) = ((3 qua Real / 2) * fr);

    end

    registration

      cluster classical_fifth for satisfying_fifth_constructible satisfying_harmonique_stable satisfying_linearite_harmonique satisfying_harmonic_closed satisfying_Nat satisfying_commutativity satisfying_tonic satisfying_interval satisfying_equiv satisfying_Real non empty MusicStruct;

      existence

      proof

        take REAL_Music ;

        thus thesis by Th38;

      end;

    end

    definition

      :: original: REAL_Music

      redefine

      func REAL_Music -> classical_fifth satisfying_fifth_constructible satisfying_harmonique_stable satisfying_linearite_harmonique satisfying_harmonic_closed satisfying_Nat satisfying_commutativity satisfying_tonic satisfying_interval satisfying_equiv satisfying_Real non empty MusicStruct ;

      coherence by Def12, Th38;

    end

    definition

      :: original: RAT_Music

      redefine

      func RAT_Music -> classical_fifth satisfying_fifth_constructible satisfying_harmonique_stable satisfying_linearite_harmonique satisfying_harmonic_closed satisfying_Nat satisfying_commutativity satisfying_tonic satisfying_interval satisfying_equiv satisfying_Real non empty MusicStruct ;

      coherence

      proof

        now

          thus RAT_Music is satisfying_fifth_constructible satisfying_harmonique_stable satisfying_linearite_harmonique satisfying_harmonic_closed satisfying_Nat satisfying_commutativity satisfying_tonic satisfying_interval satisfying_equiv satisfying_Real non empty MusicStruct;

          for frequency be Element of RAT_Music holds ex fr be positive Real st frequency = fr & ( Fifth ( RAT_Music ,frequency)) = ((3 qua Real / 2) * fr)

          proof

            let frequency be Element of RAT_Music ;

            ex fr be positive Rational st frequency = fr & ( Fifth ( RAT_Music ,frequency)) = ((3 qua Rational / 2) * fr) by Th39;

            hence thesis;

          end;

          hence thesis by Def12;

        end;

        hence thesis;

      end;

    end

    begin

    theorem :: MUSIC_S1:48

    

     Th40: for MS be satisfying_harmonic_closed satisfying_Nat satisfying_tonic satisfying_interval satisfying_equiv MusicStruct holds for frequency be Element of MS holds (1 -harmonique (MS,frequency)) = frequency

    proof

      let MS be satisfying_harmonic_closed satisfying_Nat satisfying_tonic satisfying_interval satisfying_equiv MusicStruct;

      let frequency be Element of MS;

      

       A1: NATPLUS c= the carrier of MS by Def12a;

      1 in NATPLUS by NAT_LAT:def 6;

      then

      reconsider x = 1 as Element of MS by A1;

       [frequency, (1 -harmonique (MS,frequency))] in ( Class (the Equidistance of MS, [1, 1])) by Def08b;

      then (x,x) equiv (frequency,(1 -harmonique (MS,frequency))) by EQREL_1: 18;

      hence thesis by Th29;

    end;

    theorem :: MUSIC_S1:49

    for MS be satisfying_harmonique_stable satisfying_harmonic_closed satisfying_Nat satisfying_tonic satisfying_interval satisfying_equiv MusicStruct holds for a,b be Element of MS holds (a,a) equiv (b,b)

    proof

      let MS be satisfying_harmonique_stable satisfying_harmonic_closed satisfying_Nat satisfying_tonic satisfying_interval satisfying_equiv MusicStruct;

      let a,b be Element of MS;

      (1 -harmonique (MS,a)) = a & (1 -harmonique (MS,b)) = b by Th40;

      hence thesis by Def10;

    end;

    theorem :: MUSIC_S1:50

    for MS be satisfying_harmonique_stable satisfying_linearite_harmonique satisfying_harmonic_closed satisfying_Nat satisfying_tonic satisfying_interval satisfying_equiv MusicStruct holds for frequency be Element of MS holds ( octave (MS,frequency)) = ( octave MS)

    proof

      let MS be satisfying_harmonique_stable satisfying_linearite_harmonique satisfying_harmonic_closed satisfying_Nat satisfying_tonic satisfying_interval satisfying_equiv MusicStruct;

      let frequency be Element of MS;

       A1:

      now

        let x be object;

        assume

         A2: x in ( octave (MS,frequency));

        then

        consider x1,x2 be object such that

         A3: x1 in the carrier of MS and

         A4: x2 in the carrier of MS and

         A5: x = [x1, x2] by ZFMISC_1:def 2;

        reconsider x1, x2 as Element of MS by A3, A4;

        

         A6: NATPLUS c= the carrier of MS by Def12a;

        1 in NATPLUS & 2 in NATPLUS by NAT_LAT:def 6;

        then

        reconsider y1 = 1, y2 = 2 as Element of MS by A6;

        set z = (1 -harmonique (MS,frequency)), t = (2 -harmonique (MS,frequency));

        reconsider n = 1, m = 2 as non zero Nat;

        consider r2 be positive Real such that

         A7: y1 = r2 and

         A8: (m -harmonique (MS,y1)) = (m * r2) by Def09;

        set a = (n -harmonique (MS,frequency)), b = (m -harmonique (MS,frequency));

        

         A9: y1 = (n -harmonique (MS,y1)) by Th40;

        

         A10: (a,b) equiv (x1,x2) by A2, A5, EQREL_1: 18;

        (y1,y2) equiv (a,b) by A9, A7, A8, Def10;

        then (y1,y2) equiv (x1,x2) by A10, Th23;

        hence x in ( octave MS) by A5, EQREL_1: 18;

      end;

      now

        let x be object;

        assume

         A11: x in ( octave MS);

        then

        consider x1,x2 be object such that

         A12: x1 in the carrier of MS and

         A13: x2 in the carrier of MS and

         A14: x = [x1, x2] by ZFMISC_1:def 2;

        reconsider x1, x2 as Element of MS by A12, A13;

        

         A15: NATPLUS c= the carrier of MS by Def12a;

        1 in NATPLUS & 2 in NATPLUS by NAT_LAT:def 6;

        then

        reconsider y = 1, z = 2 as Element of MS by A15;

        reconsider y9 = y as positive Real;

        reconsider n = 1, m = 2 as non zero Nat;

        set a = (n -harmonique (MS,frequency)), b = (m -harmonique (MS,frequency)), c = (n -harmonique (MS,y)), d = (m -harmonique (MS,y));

        

         A16: (a,b) equiv (c,d) by Def10;

        reconsider n1 = 1, n2 = 2 as Element of MS by Th20;

        consider r1 be positive Real such that

         A17: n1 = r1 and

         A18: (n -harmonique (MS,n1)) = (n * r1) by Def09;

        consider r2 be positive Real such that

         A19: n1 = r2 and

         A20: (m -harmonique (MS,n1)) = (m * r2) by Def09;

        (n1,n2) equiv (x1,x2) by A11, A14, EQREL_1: 18;

        then (a,b) equiv (x1,x2) by A16, A17, A18, A19, A20, Th23;

        hence x in ( octave (MS,frequency)) by A14, EQREL_1: 18;

      end;

      hence thesis by A1;

    end;

    theorem :: MUSIC_S1:51

    for MS be satisfying_fifth_constructible satisfying_harmonic_closed satisfying_Nat satisfying_interval satisfying_equiv non empty MusicStruct holds for frequency be Element of MS holds (ex seq be sequence of MS st (seq . 0 ) = frequency & (for n be Nat holds [(seq . n), (seq . (n + 1))] in ( fifth MS)))

    proof

      let MS be satisfying_fifth_constructible satisfying_harmonic_closed satisfying_Nat satisfying_interval satisfying_equiv non empty MusicStruct;

      let frequency be Element of MS;

      defpred P[ set, set, set] means ex x,y be positive Real st [$2, $3] in ( fifth MS);

      

       A1: for n be Nat holds for x be Element of MS holds ex y be Element of MS st P[n, x, y]

      proof

        let n be Nat;

        let x be Element of MS;

        ex q be Element of MS st [x, q] in ( fifth MS) by Def11;

        hence thesis;

      end;

      consider seq be sequence of MS such that

       A2: (seq . 0 ) = frequency and

       A3: for n be Nat holds P[n, (seq . n), (seq . (n + 1))] from RECDEF_1:sch 2( A1);

      take seq;

      now

        thus (seq . 0 ) = frequency by A2;

        hereby

          let n be Nat;

           P[n, (seq . n), (seq . (n + 1))] by A3;

          hence [(seq . n), (seq . (n + 1))] in ( fifth MS);

        end;

      end;

      hence thesis;

    end;

    definition

      let MS be MusicStruct;

      let a,b,c be Element of MS;

      :: MUSIC_S1:def45

      pred b is_Between a,c means ex r1,r2,r3 be positive Real st a = r1 & b = r2 & c = r3 & r1 <= r2 < r3;

    end

    definition

      let S be satisfying_harmonic_closed satisfying_Nat satisfying_interval satisfying_equiv MusicStruct;

      :: MUSIC_S1:def46

      attr S is satisfying_octave_constructible means

      : Def13: for frequency be Element of S holds ex o be Element of S st [frequency, o] in ( octave S);

    end

    theorem :: MUSIC_S1:52

    

     Th41: for frequency be Element of REAL_Music holds ex fr,qr be positive Real st fr = frequency & qr = (2 * fr) & [fr, qr] in ( octave REAL_Music )

    proof

      set MS = REAL_Music ;

      now

        let frequency be Element of MS;

        reconsider f = frequency as positive Real by Th1;

        reconsider qr = (2 * f) as positive Real;

        reconsider q = qr as Element of MS by Th1;

        take f, qr;

        thus f = frequency;

        thus qr = (2 * f);

        reconsider n2 = 1, n3 = 2 as Element of MS by Th20;

        reconsider x = [n2, n3], y = [frequency, q] as Element of [: REALPLUS , REALPLUS :];

        reconsider z = [frequency, q] as Element of [: REALPLUS , REALPLUS :];

        consider x9,y9 be Element of REALPLUS such that

         A1: z = [x9, y9] and

         A2: ( REAL_ratio . z) = ( REAL_ratio (x9,y9)) by Def02;

        consider r,s be positive Real such that

         A3: x9 = r & s = y9 & ( REAL_ratio (x9,y9)) = (s / r) by Def01;

        consider x99,y99 be Element of REALPLUS such that

         A4: x = [x99, y99] and

         A5: ( REAL_ratio . x) = ( REAL_ratio (x99,y99)) by Def02;

        consider r9,s9 be positive Real such that

         A6: x99 = r9 & s9 = y99 & ( REAL_ratio (x99,y99)) = (s9 / r9) by Def01;

        

         A7: n2 = r9 & n3 = s9 & r = frequency & s = q by A3, A1, A4, A6, XTUPLE_0: 1;

        now

          thus ( REAL_ratio . (n2,n3)) = (2 qua Real / 1 qua Real) by A7, A6, A5, BINOP_1:def 1;

          

          thus ( REAL_ratio . (frequency,q)) = ( REAL_ratio . z) by BINOP_1:def 1

          .= 2 by A2, A3, A7, XCMPLX_1: 89;

        end;

        then (n2,n3) equiv (frequency,q) by Def08a;

        hence [f, qr] in ( octave MS) by EQREL_1: 18;

      end;

      hence thesis;

    end;

    theorem :: MUSIC_S1:53

    

     Th42: REAL_Music is satisfying_octave_constructible

    proof

      let frequency be Element of REAL_Music ;

      consider fr,qr be positive Real such that

       A1: fr = frequency and qr = (2 * fr) and

       A2: [fr, qr] in ( octave REAL_Music ) by Th41;

      fr is Element of REAL_Music & qr is Element of REAL_Music by Th1;

      hence thesis by A1, A2;

    end;

    theorem :: MUSIC_S1:54

    

     Th43: for frequency be Element of RAT_Music holds ex fr,qr be positive Rational st fr = frequency & qr = (2 * fr) & [fr, qr] in ( octave RAT_Music )

    proof

      now

        let frequency be Element of RAT_Music ;

        reconsider f = frequency as positive Rational by Th2;

        reconsider qr = (2 * f) as positive Rational;

        reconsider q = qr as Element of RAT_Music by Th2;

        take f, qr;

        thus f = frequency;

        thus qr = (2 * f);

        reconsider n2 = 1, n3 = 2 as Element of RAT_Music by Th20;

        reconsider x = [n2, n3], y = [frequency, q] as Element of [: RATPLUS , RATPLUS :];

        reconsider z = [frequency, q] as Element of [: RATPLUS , RATPLUS :];

        consider x9,y9 be Element of RATPLUS such that

         A1: z = [x9, y9] and

         A2: ( RAT_ratio . z) = ( RAT_ratio (x9,y9)) by Def05;

        consider r,s be positive Rational such that

         A3: x9 = r & s = y9 & ( RAT_ratio (x9,y9)) = (s / r) by Def04;

        consider x99,y99 be Element of RATPLUS such that

         A4: x = [x99, y99] and

         A5: ( RAT_ratio . x) = ( RAT_ratio (x99,y99)) by Def05;

        consider r9,s9 be positive Rational such that

         A6: x99 = r9 & s9 = y99 & ( RAT_ratio (x99,y99)) = (s9 / r9) by Def04;

        

         A7: n2 = r9 & n3 = s9 & r = frequency & s = q by A3, A1, A4, A6, XTUPLE_0: 1;

        now

          thus ( RAT_ratio . (n2,n3)) = (2 qua Rational / 1) by BINOP_1:def 1, A7, A5, A6;

          

          thus ( RAT_ratio . (frequency,q)) = ( RAT_ratio (x9,y9)) by A2, BINOP_1:def 1

          .= 2 by A7, A3, XCMPLX_1: 89;

        end;

        then (n2,n3) equiv (frequency,q) by Def08a;

        hence [f, qr] in ( octave RAT_Music ) by EQREL_1: 18;

      end;

      hence thesis;

    end;

    theorem :: MUSIC_S1:55

    

     Th44: RAT_Music is satisfying_octave_constructible

    proof

      let frequency be Element of RAT_Music ;

      consider fr,qr be positive Rational such that

       A1: fr = frequency and qr = (2 * fr) and

       A2: [fr, qr] in ( octave RAT_Music ) by Th43;

      fr is Element of RAT_Music & qr is Element of RAT_Music by Th2;

      hence thesis by A1, A2;

    end;

    registration

      cluster satisfying_octave_constructible for classical_fifth satisfying_fifth_constructible satisfying_harmonique_stable satisfying_linearite_harmonique satisfying_harmonic_closed satisfying_Nat satisfying_commutativity satisfying_tonic satisfying_interval satisfying_equiv satisfying_Real non empty MusicStruct;

      existence by Th42;

    end

    definition

      :: original: REAL_Music

      redefine

      func REAL_Music -> satisfying_octave_constructible classical_fifth satisfying_fifth_constructible satisfying_harmonique_stable satisfying_linearite_harmonique satisfying_harmonic_closed satisfying_Nat satisfying_commutativity satisfying_tonic satisfying_interval satisfying_equiv satisfying_Real non empty MusicStruct ;

      coherence by Th42;

    end

    definition

      :: original: RAT_Music

      redefine

      func RAT_Music -> satisfying_octave_constructible classical_fifth satisfying_fifth_constructible satisfying_harmonique_stable satisfying_linearite_harmonique satisfying_harmonic_closed satisfying_Nat satisfying_commutativity satisfying_tonic satisfying_interval satisfying_equiv satisfying_Real non empty MusicStruct ;

      coherence by Th44;

    end

    definition

      let MS be satisfying_octave_constructible satisfying_harmonic_closed satisfying_Nat satisfying_interval satisfying_equiv MusicStruct;

      let frequency be Element of MS;

      :: MUSIC_S1:def47

      func Octave (MS,frequency) -> Element of MS means

      : Def14: [frequency, it ] in ( octave MS);

      existence by Def13;

      uniqueness

      proof

        let q1,q2 be Element of MS such that

         A1: [frequency, q1] in ( octave MS) and

         A2: [frequency, q2] in ( octave MS);

        reconsider n1 = 1, n2 = 2 as Element of MS by Th20;

        

         A3: (n1,n2) equiv (frequency,q1) by A1, EQREL_1: 18;

        (n1,n2) equiv (frequency,q2) by A2, EQREL_1: 18;

        then (frequency,q2) equiv (n1,n2) by Th22;

        hence thesis by A3, Th23, Th24;

      end;

    end

    definition

      let MS be satisfying_Real non empty MusicStruct;

      let r be Element of MS;

      :: MUSIC_S1:def48

      func @ r -> positive Real equals r;

      coherence

      proof

        the carrier of MS c= REALPLUS by Def07a;

        hence thesis by Th1;

      end;

    end

    definition

      let MS be satisfying_octave_constructible satisfying_harmonic_closed satisfying_Nat satisfying_interval satisfying_equiv MusicStruct;

      :: MUSIC_S1:def49

      attr MS is classical_octave means

      : Def15: for frequency be Element of MS holds ex fr be positive Real st frequency = fr & ( Octave (MS,frequency)) = (2 * fr);

    end

    theorem :: MUSIC_S1:56

    

     Th45: REAL_Music is classical_octave

    proof

      set MS = REAL_Music ;

      for frequency be Element of MS holds ex fr be positive Real st frequency = fr & ( Octave (MS,frequency)) = (2 * fr)

      proof

        let frequency be Element of MS;

        consider fr,qr be positive Real such that

         A1: fr = frequency and

         A2: qr = (2 * fr) and

         A3: [fr, qr] in ( octave MS) by Th41;

        reconsider qr as Element of MS by Th1;

         [frequency, qr] in ( octave MS) by A1, A3;

        then ( Octave (MS,frequency)) = (2 * fr) by Def14, A2;

        hence thesis by A1;

      end;

      hence thesis;

    end;

    theorem :: MUSIC_S1:57

    

     Th46: RAT_Music is classical_octave

    proof

      set MS = RAT_Music ;

      for frequency be Element of MS holds ex fr be positive Real st frequency = fr & ( Octave (MS,frequency)) = (2 * fr)

      proof

        let frequency be Element of MS;

        consider fr,qr be positive Rational such that

         A1: fr = frequency and

         A2: qr = (2 * fr) and

         A3: [fr, qr] in ( octave MS) by Th43;

        reconsider qr as Element of MS by Th2;

         [frequency, qr] in ( octave MS) by A1, A3;

        then ( Octave (MS,frequency)) = (2 * fr) by Def14, A2;

        hence thesis by A1;

      end;

      hence thesis;

    end;

    registration

      cluster classical_octave for satisfying_octave_constructible classical_fifth satisfying_fifth_constructible satisfying_harmonique_stable satisfying_linearite_harmonique satisfying_harmonic_closed satisfying_Nat satisfying_commutativity satisfying_tonic satisfying_interval satisfying_equiv satisfying_Real non empty MusicStruct;

      existence by Th45;

    end

    definition

      :: original: REAL_Music

      redefine

      func REAL_Music -> classical_octave satisfying_octave_constructible classical_fifth satisfying_fifth_constructible satisfying_harmonique_stable satisfying_linearite_harmonique satisfying_harmonic_closed satisfying_Nat satisfying_commutativity satisfying_tonic satisfying_interval satisfying_equiv satisfying_Real non empty MusicStruct ;

      coherence by Th45;

    end

    definition

      :: original: RAT_Music

      redefine

      func RAT_Music -> classical_octave satisfying_octave_constructible classical_fifth satisfying_fifth_constructible satisfying_harmonique_stable satisfying_linearite_harmonique satisfying_harmonic_closed satisfying_Nat satisfying_commutativity satisfying_tonic satisfying_interval satisfying_equiv satisfying_Real non empty MusicStruct ;

      coherence by Th46;

    end

    definition

      let MS be satisfying_octave_constructible satisfying_harmonic_closed satisfying_Nat satisfying_interval satisfying_equiv MusicStruct;

      :: MUSIC_S1:def50

      attr MS is satisfying_octave_descendent_constructible means

      : Def16: for frequency be Element of MS holds ex o be Element of MS st [o, frequency] in ( octave MS);

    end

    theorem :: MUSIC_S1:58

    

     Th47: for frequency be Element of REAL_Music holds ex fr,qr be positive Real st fr = frequency & qr = ((1 qua Real / 2) * fr) & [qr, fr] in ( octave REAL_Music )

    proof

      set MS = REAL_Music ;

      now

        let frequency be Element of MS;

        reconsider f = frequency as positive Real by Th1;

        reconsider qr = ((1 qua Real / 2) * f) as positive Real;

        reconsider q = qr as Element of MS by Th1;

        take f, qr;

        thus f = frequency;

        thus qr = ((1 qua Real / 2) * f);

        reconsider n2 = 2, n3 = 1 as Element of MS by Th20;

        reconsider x = [n2, n3], y = [frequency, q] as Element of [: REALPLUS , REALPLUS :];

        reconsider z = [frequency, q] as Element of [: REALPLUS , REALPLUS :];

        consider x9,y9 be Element of REALPLUS such that

         A1: z = [x9, y9] and

         A2: ( REAL_ratio . z) = ( REAL_ratio (x9,y9)) by Def02;

        consider r,s be positive Real such that

         A3: x9 = r & s = y9 & ( REAL_ratio (x9,y9)) = (s / r) by Def01;

        consider x99,y99 be Element of REALPLUS such that

         A4: x = [x99, y99] and

         A5: ( REAL_ratio . x) = ( REAL_ratio (x99,y99)) by Def02;

        consider r9,s9 be positive Real such that

         A6: x99 = r9 & s9 = y99 & ( REAL_ratio (x99,y99)) = (s9 / r9) by Def01;

        

         A7: n2 = r9 & n3 = s9 & r = frequency & s = q by A3, A1, A4, A6, XTUPLE_0: 1;

        now

          thus ( REAL_ratio . (n2,n3)) = (1 qua Real / 2 qua Real) by A6, A7, A5, BINOP_1:def 1;

          

          thus ( REAL_ratio . (frequency,q)) = (s / r) by A3, A2, BINOP_1:def 1

          .= (1 qua Real / 2) by A7, XCMPLX_1: 89;

        end;

        then (n2,n3) equiv (frequency,q) by Def08a;

        then (n3,n2) equiv (q,frequency) by Th28;

        hence [qr, f] in ( octave MS) by EQREL_1: 18;

      end;

      hence thesis;

    end;

    theorem :: MUSIC_S1:59

    

     Th48: REAL_Music is satisfying_octave_descendent_constructible

    proof

      let frequency be Element of REAL_Music ;

      consider fr,qr be positive Real such that

       A2: fr = frequency and qr = ((1 qua Real / 2) * fr) and

       A4: [qr, fr] in ( octave REAL_Music ) by Th47;

      fr is Element of REAL_Music & qr is Element of REAL_Music by Th1;

      hence thesis by A2, A4;

    end;

    theorem :: MUSIC_S1:60

    

     Th49: for frequency be Element of RAT_Music holds ex fr,qr be positive Rational st fr = frequency & qr = ((1 qua Rational / 2) * fr) & [qr, fr] in ( octave RAT_Music )

    proof

      set MS = RAT_Music ;

      now

        let frequency be Element of MS;

        reconsider f = frequency as positive Rational by Th2;

        reconsider qr = ((1 qua Rational / 2) * f) as positive Rational;

        reconsider q = qr as Element of MS by Th2;

        take f, qr;

        thus f = frequency;

        thus qr = ((1 qua Rational / 2) * f);

        reconsider n2 = 2, n3 = 1 as Element of MS by Th20;

        reconsider x = [n2, n3], y = [frequency, q] as Element of [: RATPLUS , RATPLUS :];

        reconsider z = [frequency, q] as Element of [: RATPLUS , RATPLUS :];

        consider x9,y9 be Element of RATPLUS such that

         A1: z = [x9, y9] and

         A2: ( RAT_ratio . z) = ( RAT_ratio (x9,y9)) by Def05;

        consider r,s be positive Rational such that

         A3: x9 = r & s = y9 & ( RAT_ratio (x9,y9)) = (s / r) by Def04;

        consider x99,y99 be Element of RATPLUS such that

         A4: x = [x99, y99] and

         A5: ( RAT_ratio . x) = ( RAT_ratio (x99,y99)) by Def05;

        consider r9,s9 be positive Rational such that

         A6: x99 = r9 & s9 = y99 & ( RAT_ratio (x99,y99)) = (s9 / r9) by Def04;

        

         A7: n2 = r9 & n3 = s9 & r = frequency & s = q by A3, A1, A4, A6, XTUPLE_0: 1;

        now

          thus ( RAT_ratio . (n2,n3)) = (1 qua Real / 2 qua Real) by A6, A7, A5, BINOP_1:def 1;

          

          thus ( RAT_ratio . (frequency,q)) = (s / r) by A2, A3, BINOP_1:def 1

          .= (1 qua Rational / 2) by A7, XCMPLX_1: 89;

        end;

        then (n2,n3) equiv (frequency,q) by Def08a;

        then (n3,n2) equiv (q,frequency) by Th28;

        hence [qr, f] in ( octave MS) by EQREL_1: 18;

      end;

      hence thesis;

    end;

    theorem :: MUSIC_S1:61

    

     Th50: RAT_Music is satisfying_octave_descendent_constructible

    proof

      let frequency be Element of RAT_Music ;

      consider fr,qr be positive Rational such that

       A1: fr = frequency and qr = ((1 qua Rational / 2) * fr) and

       A2: [qr, fr] in ( octave RAT_Music ) by Th49;

      fr is Element of RAT_Music & qr is Element of RAT_Music by Th2;

      hence thesis by A1, A2;

    end;

    registration

      cluster satisfying_octave_descendent_constructible for classical_octave satisfying_octave_constructible classical_fifth satisfying_fifth_constructible satisfying_harmonique_stable satisfying_linearite_harmonique satisfying_harmonic_closed satisfying_Nat satisfying_commutativity satisfying_tonic satisfying_interval satisfying_equiv satisfying_Real non empty MusicStruct;

      existence by Th48;

    end

    definition

      :: original: REAL_Music

      redefine

      func REAL_Music -> satisfying_octave_descendent_constructible classical_octave satisfying_octave_constructible classical_fifth satisfying_fifth_constructible satisfying_harmonique_stable satisfying_linearite_harmonique satisfying_harmonic_closed satisfying_Nat satisfying_commutativity satisfying_tonic satisfying_interval satisfying_equiv satisfying_Real non empty MusicStruct ;

      coherence by Th48;

    end

    definition

      :: original: RAT_Music

      redefine

      func RAT_Music -> satisfying_octave_descendent_constructible classical_octave satisfying_octave_constructible classical_fifth satisfying_fifth_constructible satisfying_harmonique_stable satisfying_linearite_harmonique satisfying_harmonic_closed satisfying_Nat satisfying_commutativity satisfying_tonic satisfying_interval satisfying_equiv satisfying_Real non empty MusicStruct ;

      coherence by Th50;

    end

    definition

      let MS be satisfying_octave_descendent_constructible satisfying_octave_constructible satisfying_fifth_constructible satisfying_harmonic_closed satisfying_Nat satisfying_commutativity satisfying_interval satisfying_equiv MusicStruct;

      let frequency be Element of MS;

      :: MUSIC_S1:def51

      func Octave_descendent (MS,frequency) -> Element of MS means

      : Def17: [it , frequency] in ( octave MS);

      existence by Def16;

      uniqueness

      proof

        let q1,q2 be Element of MS such that

         A1: [q1, frequency] in ( octave MS) and

         A2: [q2, frequency] in ( octave MS);

        reconsider n1 = 1, n2 = 2 as Element of MS by Th20;

        

         A3: (n1,n2) equiv (q1,frequency) by A1, EQREL_1: 18;

        (n1,n2) equiv (q2,frequency) by A2, EQREL_1: 18;

        then (q2,frequency) equiv (n1,n2) by Th22;

        then (q2,frequency) equiv (q1,frequency) by A3, Th23;

        hence thesis by Th24, Th28;

      end;

    end

    theorem :: MUSIC_S1:62

    

     Th51: for MS be satisfying_octave_descendent_constructible classical_octave satisfying_octave_constructible satisfying_fifth_constructible satisfying_harmonic_closed satisfying_Nat satisfying_commutativity satisfying_interval satisfying_equiv satisfying_Real non empty MusicStruct holds for frequency be Element of MS holds ex r be positive Real st frequency = r & ( Octave_descendent (MS,frequency)) = (r / 2)

    proof

      let MS be satisfying_octave_descendent_constructible classical_octave satisfying_octave_constructible satisfying_fifth_constructible satisfying_harmonic_closed satisfying_Nat satisfying_commutativity satisfying_interval satisfying_equiv satisfying_Real non empty MusicStruct;

      let frequency be Element of MS;

      

       A1: the carrier of MS c= REALPLUS by Def07a;

      then

      reconsider r = frequency as positive Real by Th1;

      reconsider r2 = (r / 2) as positive Real;

      set ff = ( Octave_descendent (MS,frequency));

      reconsider rff = ff as positive Real by A1, Th1;

      

       A2: [ff, frequency] in ( octave MS) & [ff, ( Octave (MS,ff))] in ( octave MS) by Def14, Def17;

      ex fr be positive Real st ff = fr & ( Octave (MS,ff)) = (2 * fr) by Def15;

      then frequency = (2 * rff) by A2, Def14;

      then rff = (r / 2);

      hence thesis;

    end;

    theorem :: MUSIC_S1:63

    

     Th52: for MS1,MS2 be classical_octave satisfying_octave_constructible classical_fifth satisfying_fifth_constructible satisfying_harmonic_closed satisfying_Nat satisfying_interval satisfying_equiv MusicStruct holds for f1 be Element of MS1 holds for f2 be Element of MS2 st f1 = f2 holds ( Fifth (MS1,f1)) = ( Fifth (MS2,f2)) & ( Octave (MS1,f1)) = ( Octave (MS2,f2))

    proof

      let MS1,MS2 be classical_octave satisfying_octave_constructible classical_fifth satisfying_fifth_constructible satisfying_harmonic_closed satisfying_Nat satisfying_interval satisfying_equiv MusicStruct;

      let f1 be Element of MS1;

      let f2 be Element of MS2;

      assume

       A1: f1 = f2;

      consider fr1 be positive Real such that

       A2: f1 = fr1 & ( Fifth (MS1,f1)) = ((3 qua Real / 2) * fr1) by Def12;

      consider fr2 be positive Real such that

       A3: f2 = fr2 & ( Fifth (MS2,f2)) = ((3 qua Real / 2) * fr2) by Def12;

      thus ( Fifth (MS1,f1)) = ( Fifth (MS2,f2)) by A1, A2, A3;

      (ex fr be positive Real st f1 = fr & ( Octave (MS1,f1)) = (2 * fr)) & (ex fr be positive Real st f2 = fr & ( Octave (MS2,f2)) = (2 * fr)) by Def15;

      hence thesis by A1;

    end;

    theorem :: MUSIC_S1:64

    

     Th53: for MS1,MS2 be satisfying_octave_descendent_constructible classical_octave satisfying_octave_constructible satisfying_fifth_constructible satisfying_harmonic_closed satisfying_Nat satisfying_commutativity satisfying_interval satisfying_equiv satisfying_Real non empty MusicStruct holds for frequency1 be Element of MS1 holds for frequency2 be Element of MS2 st frequency1 = frequency2 holds ( Octave_descendent (MS1,frequency1)) = ( Octave_descendent (MS2,frequency2))

    proof

      let MS1,MS2 be satisfying_octave_descendent_constructible classical_octave satisfying_octave_constructible satisfying_fifth_constructible satisfying_harmonic_closed satisfying_Nat satisfying_commutativity satisfying_interval satisfying_equiv satisfying_Real non empty MusicStruct;

      let frequency1 be Element of MS1;

      let frequency2 be Element of MS2;

      assume

       A1: frequency1 = frequency2;

      consider r1 be positive Real such that

       A2: frequency1 = r1 & ( Octave_descendent (MS1,frequency1)) = (r1 / 2) by Th51;

      consider r2 be positive Real such that

       A3: frequency2 = r2 & ( Octave_descendent (MS2,frequency2)) = (r2 / 2) by Th51;

      thus thesis by A1, A2, A3;

    end;

    definition

      let MS be satisfying_octave_descendent_constructible satisfying_octave_constructible satisfying_fifth_constructible satisfying_harmonic_closed satisfying_Nat satisfying_commutativity satisfying_interval satisfying_equiv MusicStruct;

      let fondamentale,frequency be Element of MS;

      :: MUSIC_S1:def52

      func Fifth_reduct (MS,fondamentale,frequency) -> Element of MS equals

      : Def18: ( Fifth (MS,frequency)) if ( Fifth (MS,frequency)) is_Between (fondamentale,( Octave (MS,fondamentale)))

      otherwise ( Octave_descendent (MS,( Fifth (MS,frequency))));

      correctness ;

    end

    theorem :: MUSIC_S1:65

    for MS1,MS2 be satisfying_octave_descendent_constructible classical_octave satisfying_octave_constructible classical_fifth satisfying_fifth_constructible satisfying_harmonic_closed satisfying_Nat satisfying_commutativity satisfying_interval satisfying_equiv satisfying_Real non empty MusicStruct holds for frequency1,fondamentale1 be Element of MS1 holds for frequency2,fondamentale2 be Element of MS2 st frequency1 = frequency2 & fondamentale1 = fondamentale2 holds ( Fifth_reduct (MS1,fondamentale1,frequency1)) = ( Fifth_reduct (MS2,fondamentale2,frequency2))

    proof

      let MS1,MS2 be satisfying_octave_descendent_constructible classical_octave satisfying_octave_constructible classical_fifth satisfying_fifth_constructible satisfying_harmonic_closed satisfying_Nat satisfying_commutativity satisfying_interval satisfying_equiv satisfying_Real non empty MusicStruct;

      let frequency1,fondamentale1 be Element of MS1;

      let frequency2,fondamentale2 be Element of MS2;

      assume that

       A1: frequency1 = frequency2 and

       A2: fondamentale1 = fondamentale2;

      per cases ;

        suppose

         A3: ( Fifth (MS1,frequency1)) is_Between (fondamentale1,( Octave (MS1,fondamentale1)));

        then

         A4: ( Fifth_reduct (MS1,fondamentale1,frequency1)) = ( Fifth (MS1,frequency1)) by Def18;

        ( Fifth (MS1,frequency1)) = ( Fifth (MS2,frequency2)) & fondamentale1 = fondamentale2 & ( Octave (MS2,fondamentale2)) = ( Octave (MS1,fondamentale1)) by A1, A2, Th52;

        then ( Fifth (MS2,frequency2)) is_Between (fondamentale2,( Octave (MS2,fondamentale2))) by A3;

        then ( Fifth (MS2,frequency2)) = ( Fifth_reduct (MS2,fondamentale2,frequency2)) by Def18;

        hence thesis by A4, A1, Th52;

      end;

        suppose

         A5: not ( Fifth (MS1,frequency1)) is_Between (fondamentale1,( Octave (MS1,fondamentale1)));

        then

         A6: ( Fifth_reduct (MS1,fondamentale1,frequency1)) = ( Octave_descendent (MS1,( Fifth (MS1,frequency1)))) by Def18;

        ( Fifth (MS1,frequency1)) = ( Fifth (MS2,frequency2)) & fondamentale1 = fondamentale2 & ( Octave (MS2,fondamentale2)) = ( Octave (MS1,fondamentale1)) by A1, A2, Th52;

        then not ( Fifth (MS2,frequency2)) is_Between (fondamentale2,( Octave (MS2,fondamentale2))) by A5;

        then

         A7: ( Fifth_reduct (MS2,fondamentale2,frequency2)) = ( Octave_descendent (MS2,( Fifth (MS2,frequency2)))) by Def18;

        ( Fifth (MS1,frequency1)) = ( Fifth (MS2,frequency2)) by A1, Th52;

        hence thesis by A6, A7, Th53;

      end;

    end;

    theorem :: MUSIC_S1:66

    

     Th54: for MS be classical_fifth satisfying_fifth_constructible satisfying_harmonic_closed satisfying_Nat satisfying_interval satisfying_equiv MusicStruct holds for frequency be Element of MS holds ex r,s be positive Real st r = frequency & s = ((3 qua Real / 2) * r) & ( Fifth (MS,frequency)) = s

    proof

      let MS be classical_fifth satisfying_fifth_constructible satisfying_harmonic_closed satisfying_Nat satisfying_interval satisfying_equiv MusicStruct;

      let frequency be Element of MS;

      consider fr be positive Real such that

       A1: frequency = fr & ( Fifth (MS,frequency)) = ((3 qua Real / 2) * fr) by Def12;

      reconsider s = ((3 qua Real / 2) * fr) as positive Real;

      take fr, s;

      thus thesis by A1;

    end;

    theorem :: MUSIC_S1:67

    

     Th55: for MS be satisfying_octave_descendent_constructible classical_octave satisfying_octave_constructible classical_fifth satisfying_fifth_constructible satisfying_harmonic_closed satisfying_Nat satisfying_interval satisfying_equiv MusicStruct holds for fondamentale,frequency be Element of MS st frequency is_Between (fondamentale,( Octave (MS,fondamentale))) holds ex r1,r2,r3 be positive Real st fondamentale = r1 & frequency = r2 & ( Octave (MS,fondamentale)) = (2 * r1) & r1 <= r2 <= (2 * r1)

    proof

      let MS be satisfying_octave_descendent_constructible classical_octave satisfying_octave_constructible classical_fifth satisfying_fifth_constructible satisfying_harmonic_closed satisfying_Nat satisfying_interval satisfying_equiv MusicStruct;

      let fondamentale,frequency be Element of MS;

      assume

       A1: frequency is_Between (fondamentale,( Octave (MS,fondamentale)));

      ex r9 be positive Real st fondamentale = r9 & ( Octave (MS,fondamentale)) = (2 * r9) by Def15;

      hence thesis by A1;

    end;

    theorem :: MUSIC_S1:68

    

     Th56: for MS be satisfying_octave_descendent_constructible classical_octave satisfying_octave_constructible classical_fifth satisfying_fifth_constructible satisfying_harmonic_closed satisfying_Nat satisfying_commutativity satisfying_interval satisfying_equiv satisfying_Real non empty MusicStruct holds for fondamentale,frequency be Element of MS st frequency is_Between (fondamentale,( Octave (MS,fondamentale))) holds ( Fifth_reduct (MS,fondamentale,frequency)) is_Between (fondamentale,( Octave (MS,fondamentale)))

    proof

      let MS be satisfying_octave_descendent_constructible classical_octave satisfying_octave_constructible classical_fifth satisfying_fifth_constructible satisfying_harmonic_closed satisfying_Nat satisfying_commutativity satisfying_interval satisfying_equiv satisfying_Real non empty MusicStruct;

      let fondamentale,frequency be Element of MS;

      assume frequency is_Between (fondamentale,( Octave (MS,fondamentale)));

      then

      consider r1,r2,r3 be positive Real such that

       A1: fondamentale = r1 & frequency = r2 & ( Octave (MS,fondamentale)) = (2 * r1) & r1 <= r2 <= (2 * r1) by Th55;

      consider fr be positive Real such that

       A2: frequency = fr & ( Fifth (MS,frequency)) = ((3 qua Real / 2) * fr) by Def12;

      per cases ;

        suppose ( Fifth (MS,frequency)) is_Between (fondamentale,( Octave (MS,fondamentale)));

        hence thesis by Def18;

      end;

        suppose

         A3: not ( Fifth (MS,frequency)) is_Between (fondamentale,( Octave (MS,fondamentale)));

        

         A4: ex r be positive Real st ( Fifth (MS,frequency)) = r & ( Octave_descendent (MS,( Fifth (MS,frequency)))) = (r / 2) by Th51;

        per cases by A2, A1, A3;

          suppose

           A5: ((3 qua Real / 2) * r2) < r1;

          reconsider r32 = (3 qua Real / 2) as non zero positive Real;

          (r1 * (1 / r32)) < (1 * r1) by XREAL_1: 68;

          then

           A6: (r1 / r32) < r1 by XCMPLX_1: 99;

          ((r32 * r2) / r32) < (r1 / r32) by A5, XREAL_1: 74;

          then r2 < (r1 / r32) by XCMPLX_1: 89;

          hence thesis by A1, A6, XXREAL_0: 2;

        end;

          suppose (2 * r1) <= ((3 qua Real / 2) * r2);

          then

           A7: ((2 * r1) / 2) <= (((3 qua Real / 2) * r2) / 2) by XREAL_1: 72;

          reconsider r34 = (3 qua Real / 4) as positive Real;

          

           A8: ((3 qua Real / 2) * r1) < (2 * r1) by XREAL_1: 68;

          ((3 qua Real / 4) * r2) <= ((3 qua Real / 4) * (2 * r1)) by A1, XREAL_1: 66;

          then ((3 qua Real / 4) * r2) < (2 * r1) by A8, XXREAL_0: 2;

          hence thesis by A2, A7, A1, A4, A3, Def18;

        end;

      end;

    end;

    definition

      mode MusicSpace is satisfying_octave_descendent_constructible classical_octave satisfying_octave_constructible classical_fifth satisfying_fifth_constructible satisfying_harmonique_stable satisfying_linearite_harmonique satisfying_harmonic_closed satisfying_Nat satisfying_commutativity satisfying_tonic satisfying_interval satisfying_equiv satisfying_Real non empty MusicStruct;

    end

    theorem :: MUSIC_S1:69

     REAL_Music is MusicSpace;

    theorem :: MUSIC_S1:70

     RAT_Music is MusicSpace;

    begin

    theorem :: MUSIC_S1:71

    

     Th56BIS: for MS be satisfying_octave_descendent_constructible satisfying_octave_constructible satisfying_fifth_constructible satisfying_harmonic_closed satisfying_Nat satisfying_commutativity satisfying_interval satisfying_equiv non empty MusicStruct holds for fondamentale,frequency be Element of MS holds (ex seq be sequence of MS st ((seq . 0 ) = frequency & for n be Nat holds (seq . (n + 1)) = ( Fifth_reduct (MS,fondamentale,(seq . n)))))

    proof

      let MS be satisfying_octave_descendent_constructible satisfying_octave_constructible satisfying_fifth_constructible satisfying_harmonic_closed satisfying_Nat satisfying_commutativity satisfying_interval satisfying_equiv non empty MusicStruct;

      let fondamentale,frequency be Element of MS;

      defpred P[ set, set, set] means ex x,y be Element of MS st x = $2 & y = $3 & y = ( Fifth_reduct (MS,fondamentale,x));

      

       A1: for n be Nat holds for x be Element of MS holds ex y be Element of MS st P[n, x, y]

      proof

        let n be Nat;

        let x be Element of MS;

        reconsider y = ( Fifth_reduct (MS,fondamentale,x)) as Element of MS;

        take y;

        thus thesis;

      end;

      consider seq be sequence of MS such that

       A2: (seq . 0 ) = frequency and

       A3: for n be Nat holds P[n, (seq . n), (seq . (n + 1))] from RECDEF_1:sch 2( A1);

      reconsider seq as sequence of MS;

      now

        thus (seq . 0 ) = frequency by A2;

        hereby

          let n be Nat;

          consider x,y be Element of MS such that

           A4: x = (seq . n) and

           A5: y = (seq . (n + 1)) and

           A6: y = ( Fifth_reduct (MS,fondamentale,x)) by A3;

          reconsider m = (n + 1) as non zero Nat;

          reconsider m9 = (m - 1) as Nat;

          thus (seq . (n + 1)) = ( Fifth_reduct (MS,fondamentale,(seq . n))) by A4, A5, A6;

        end;

      end;

      hence thesis;

    end;

    definition

      let MS be satisfying_octave_descendent_constructible satisfying_octave_constructible satisfying_fifth_constructible satisfying_harmonic_closed satisfying_Nat satisfying_commutativity satisfying_interval satisfying_equiv non empty MusicStruct;

      let fondamentale,frequency be Element of MS;

      :: MUSIC_S1:def53

      func spiral_of_fifths (MS,fondamentale,frequency) -> sequence of MS means

      : Def19: (it . 0 ) = frequency & for n be Nat holds (it . (n + 1)) = ( Fifth_reduct (MS,fondamentale,(it . n)));

      existence by Th56BIS;

      uniqueness

      proof

        let seq1,seq2 be sequence of MS such that

         A1: (seq1 . 0 ) = frequency & for n be Nat holds (seq1 . (n + 1)) = ( Fifth_reduct (MS,fondamentale,(seq1 . n))) and

         A2: (seq2 . 0 ) = frequency & for n be Nat holds (seq2 . (n + 1)) = ( Fifth_reduct (MS,fondamentale,(seq2 . n)));

        defpred P[ Nat] means (seq1 . $1) = (seq2 . $1);

        

         A3: P[ 0 ] by A1, A2;

        

         A4: for k be Nat st P[k] holds P[(k + 1)]

        proof

          let k be Nat;

          assume

           A5: P[k];

          (seq1 . (k + 1)) = ( Fifth_reduct (MS,fondamentale,(seq1 . k))) by A1

          .= (seq2 . (k + 1)) by A2, A5;

          hence thesis;

        end;

        

         A6: for k be Nat holds P[k] from NAT_1:sch 2( A3, A4);

        now

          ( dom seq1) = NAT by PARTFUN1:def 2;

          hence ( dom seq1) = ( dom seq2) by PARTFUN1:def 2;

          thus for x be object st x in ( dom seq1) holds (seq1 . x) = (seq2 . x) by A6;

        end;

        hence thesis by FUNCT_1:def 11;

      end;

    end

    reserve MS for satisfying_octave_descendent_constructible classical_octave satisfying_octave_constructible classical_fifth satisfying_fifth_constructible satisfying_harmonic_closed satisfying_Nat satisfying_commutativity satisfying_interval satisfying_equiv satisfying_Real non empty MusicStruct,

fondamentale,frequency for Element of MS;

    theorem :: MUSIC_S1:72

    

     Th57: frequency is_Between (fondamentale,( Octave (MS,fondamentale))) implies for n be Nat holds (( spiral_of_fifths (MS,fondamentale,frequency)) . n) is_Between (fondamentale,( Octave (MS,fondamentale)))

    proof

      assume

       A1: frequency is_Between (fondamentale,( Octave (MS,fondamentale)));

      let n be Nat;

      defpred P[ Nat] means (( spiral_of_fifths (MS,fondamentale,frequency)) . $1) is_Between (fondamentale,( Octave (MS,fondamentale)));

      

       A2: P[ 0 ] by Def19, A1;

      

       A3: for k be Nat st P[k] holds P[(k + 1)]

      proof

        let k be Nat;

        assume

         A4: P[k];

        (( spiral_of_fifths (MS,fondamentale,frequency)) . (k + 1)) = ( Fifth_reduct (MS,fondamentale,(( spiral_of_fifths (MS,fondamentale,frequency)) . k))) by Def19;

        hence thesis by A4, Th56;

      end;

      for k be Nat holds P[k] from NAT_1:sch 2( A2, A3);

      hence thesis;

    end;

    theorem :: MUSIC_S1:73

    

     Th58: (( spiral_of_fifths (MS,fondamentale,fondamentale)) . 1) = ((3 qua Real / 2) * ( @ fondamentale))

    proof

      reconsider n1 = 1, n0 = 0 as Nat;

      

       A1: (( spiral_of_fifths (MS,fondamentale,fondamentale)) . 1) = (( spiral_of_fifths (MS,fondamentale,fondamentale)) . (n0 + 1))

      .= ( Fifth_reduct (MS,fondamentale,(( spiral_of_fifths (MS,fondamentale,fondamentale)) . n0))) by Def19

      .= ( Fifth_reduct (MS,fondamentale,fondamentale)) by Def19;

      consider r,s be positive Real such that

       A2: r = fondamentale & s = ((3 qua Real / 2) * r) & ( Fifth (MS,fondamentale)) = s by Th54;

      

       A3: ex fr be positive Real st fondamentale = fr & ( Octave (MS,fondamentale)) = (2 * fr) by Def15;

      (1 * r) <= ((3 qua Real / 2) * r) & ((3 qua Real / 2) * r) < (2 * r) by XREAL_1: 68;

      then ( Fifth (MS,fondamentale)) is_Between (fondamentale,( Octave (MS,fondamentale))) by A2, A3;

      hence thesis by A1, A2, Def18;

    end;

    theorem :: MUSIC_S1:74

    

     Th59: (( spiral_of_fifths (MS,fondamentale,fondamentale)) . 2) = ((9 qua Real / 8) * ( @ fondamentale))

    proof

      reconsider n2 = 2, n1 = 1, n0 = 0 as Nat;

      (( spiral_of_fifths (MS,fondamentale,fondamentale)) . n1) is Element of MS;

      then

      reconsider r32 = ((3 qua Real / 2) * ( @ fondamentale)) as Element of MS by Th58;

      

       A1: (( spiral_of_fifths (MS,fondamentale,fondamentale)) . 2) = (( spiral_of_fifths (MS,fondamentale,fondamentale)) . (n1 + 1))

      .= ( Fifth_reduct (MS,fondamentale,(( spiral_of_fifths (MS,fondamentale,fondamentale)) . n1))) by Def19

      .= ( Fifth_reduct (MS,fondamentale,r32)) by Th58;

      consider r,s be positive Real such that

       A2: r = r32 & s = ((3 qua Real / 2) * r) & ( Fifth (MS,r32)) = s by Th54;

      

       A3: ( Fifth (MS,r32)) = ((9 qua Real / 4) * ( @ fondamentale)) by A2;

      

       A4: ex r be positive Real st ( Fifth (MS,r32)) = r & ( Octave_descendent (MS,( Fifth (MS,r32)))) = (r / 2) by Th51;

       not ( Fifth (MS,r32)) is_Between (fondamentale,( Octave (MS,fondamentale)))

      proof

        assume

         A5: ( Fifth (MS,r32)) is_Between (fondamentale,( Octave (MS,fondamentale)));

        

         A6: ex fr be positive Real st fondamentale = fr & ( Octave (MS,fondamentale)) = (2 * fr) by Def15;

        thus contradiction by A5, A6, A3, XREAL_1: 68;

      end;

      hence thesis by A1, A2, A4, Def18;

    end;

    theorem :: MUSIC_S1:75

    

     Th60: (( spiral_of_fifths (MS,fondamentale,fondamentale)) . 3) = ((27 qua Real / 16) * ( @ fondamentale))

    proof

      reconsider n3 = 3, n2 = 2, n1 = 1, n0 = 0 as Nat;

      (( spiral_of_fifths (MS,fondamentale,fondamentale)) . n2) is Element of MS;

      then

      reconsider r32 = ((9 qua Real / 8) * ( @ fondamentale)) as Element of MS by Th59;

      

       A1: (( spiral_of_fifths (MS,fondamentale,fondamentale)) . 3) = (( spiral_of_fifths (MS,fondamentale,fondamentale)) . (n2 + 1))

      .= ( Fifth_reduct (MS,fondamentale,(( spiral_of_fifths (MS,fondamentale,fondamentale)) . n2))) by Def19

      .= ( Fifth_reduct (MS,fondamentale,r32)) by Th59;

      consider r,s be positive Real such that

       A2: r = r32 & s = ((3 qua Real / 2) * r) & ( Fifth (MS,r32)) = s by Th54;

      

       A3: ex fr be positive Real st fondamentale = fr & ( Octave (MS,fondamentale)) = (2 * fr) by Def15;

      ((27 qua Real / 16) * ( @ fondamentale)) < (2 * ( @ fondamentale)) & (1 * ( @ fondamentale)) < ((27 qua Real / 16) * ( @ fondamentale)) by XREAL_1: 68;

      then ( Fifth (MS,r32)) is_Between (fondamentale,( Octave (MS,fondamentale))) by A2, A3;

      hence thesis by A2, A1, Def18;

    end;

    theorem :: MUSIC_S1:76

    

     Th61: (( spiral_of_fifths (MS,fondamentale,fondamentale)) . 4) = ((81 qua Real / 64) * ( @ fondamentale))

    proof

      reconsider n4 = 4, n3 = 3, n2 = 2, n1 = 1, n0 = 0 as Nat;

      (( spiral_of_fifths (MS,fondamentale,fondamentale)) . n3) is Element of MS;

      then

      reconsider r32 = ((27 qua Real / 16) * ( @ fondamentale)) as Element of MS by Th60;

      

       A1: (( spiral_of_fifths (MS,fondamentale,fondamentale)) . 4) = (( spiral_of_fifths (MS,fondamentale,fondamentale)) . (n3 + 1))

      .= ( Fifth_reduct (MS,fondamentale,(( spiral_of_fifths (MS,fondamentale,fondamentale)) . n3))) by Def19

      .= ( Fifth_reduct (MS,fondamentale,r32)) by Th60;

      consider r,s be positive Real such that

       A2: r = r32 & s = ((3 qua Real / 2) * r) & ( Fifth (MS,r32)) = s by Th54;

      

       A3: ( Fifth (MS,r32)) = ((81 qua Real / 32) * ( @ fondamentale)) by A2;

      

       A4: ex fr be positive Real st fondamentale = fr & ( Octave (MS,fondamentale)) = (2 * fr) by Def15;

      

       A5: ex r be positive Real st ( Fifth (MS,r32)) = r & ( Octave_descendent (MS,( Fifth (MS,r32)))) = (r / 2) by Th51;

       not ( Fifth (MS,r32)) is_Between (fondamentale,( Octave (MS,fondamentale))) by A3, A4, XREAL_1: 68;

      hence thesis by A1, A2, A5, Def18;

    end;

    theorem :: MUSIC_S1:77

    (( spiral_of_fifths (MS,fondamentale,fondamentale)) . 5) = ((243 qua Real / 128) * ( @ fondamentale))

    proof

      reconsider n5 = 5, n4 = 4, n3 = 3, n2 = 2, n1 = 1, n0 = 0 as Nat;

      (( spiral_of_fifths (MS,fondamentale,fondamentale)) . n4) is Element of MS;

      then

      reconsider r32 = ((81 qua Real / 64) * ( @ fondamentale)) as Element of MS by Th61;

      

       A1: (( spiral_of_fifths (MS,fondamentale,fondamentale)) . 5) = (( spiral_of_fifths (MS,fondamentale,fondamentale)) . (n4 + 1))

      .= ( Fifth_reduct (MS,fondamentale,(( spiral_of_fifths (MS,fondamentale,fondamentale)) . n4))) by Def19

      .= ( Fifth_reduct (MS,fondamentale,r32)) by Th61;

      consider r,s be positive Real such that

       A2: r = r32 & s = ((3 qua Real / 2) * r) & ( Fifth (MS,r32)) = s by Th54;

      

       A3: ex fr be positive Real st fondamentale = fr & ( Octave (MS,fondamentale)) = (2 * fr) by Def15;

      ((243 qua Real / 128) * ( @ fondamentale)) < (2 * ( @ fondamentale)) & (1 * ( @ fondamentale)) < ((243 qua Real / 128) * ( @ fondamentale)) by XREAL_1: 68;

      then ( Fifth (MS,r32)) is_Between (fondamentale,( Octave (MS,fondamentale))) by A2, A3;

      hence thesis by A2, A1, Def18;

    end;

    theorem :: MUSIC_S1:78

    

     Th62: (( @ (( spiral_of_fifths (MS,frequency,frequency)) . 2)) / ( @ frequency)) = ((3 * 3) qua Real / ((2 * 2) * 2))

    proof

      (( @ (( spiral_of_fifths (MS,frequency,frequency)) . 2)) / ( @ frequency)) = (((9 qua Real / 8) * ( @ frequency)) / ( @ frequency)) by Th59

      .= ((3 * 3) qua Real / ((2 * 2) * 2)) by XCMPLX_1: 89;

      hence thesis;

    end;

    theorem :: MUSIC_S1:79

    

     Th63: (( @ (( spiral_of_fifths (MS,frequency,frequency)) . 4)) / ( @ (( spiral_of_fifths (MS,frequency,frequency)) . 2))) = ((3 * 3) qua Real / ((2 * 2) * 2))

    proof

      (( spiral_of_fifths (MS,frequency,frequency)) . 4) = ((81 qua Real / 64) * ( @ frequency)) & (( spiral_of_fifths (MS,frequency,frequency)) . 2) = ((9 qua Real / 8) * ( @ frequency)) by Th59, Th61;

      then (( @ (( spiral_of_fifths (MS,frequency,frequency)) . 4)) / ( @ (( spiral_of_fifths (MS,frequency,frequency)) . 2))) = ((81 qua Real / 64) / (9 qua Real / 8)) by XCMPLX_1: 91;

      hence thesis;

    end;

    theorem :: MUSIC_S1:80

    

     Th64: (( @ (( spiral_of_fifths (MS,frequency,frequency)) . 1)) / ( @ (( spiral_of_fifths (MS,frequency,frequency)) . 4))) = (32 qua Real / 27)

    proof

      (( spiral_of_fifths (MS,frequency,frequency)) . 4) = ((81 qua Real / 64) * ( @ frequency)) & (( spiral_of_fifths (MS,frequency,frequency)) . 1) = ((3 qua Real / 2) * ( @ frequency)) by Th58, Th61;

      

      then (( @ (( spiral_of_fifths (MS,frequency,frequency)) . 1)) / ( @ (( spiral_of_fifths (MS,frequency,frequency)) . 4))) = ((3 qua Real / 2) / (81 qua Real / 64)) by XCMPLX_1: 91

      .= (32 qua Real / 27);

      hence thesis;

    end;

    theorem :: MUSIC_S1:81

    

     Th65: (( @ (( spiral_of_fifths (MS,frequency,frequency)) . 3)) / ( @ (( spiral_of_fifths (MS,frequency,frequency)) . 1))) = (9 qua Real / 8)

    proof

      (( spiral_of_fifths (MS,frequency,frequency)) . 3) = ((27 qua Real / 16) * ( @ frequency)) & (( spiral_of_fifths (MS,frequency,frequency)) . 1) = ((3 qua Real / 2) * ( @ frequency)) by Th58, Th60;

      

      then (( @ (( spiral_of_fifths (MS,frequency,frequency)) . 3)) / ( @ (( spiral_of_fifths (MS,frequency,frequency)) . 1))) = ((27 qua Real / 16) / (3 qua Real / 2)) by XCMPLX_1: 91

      .= (9 qua Real / 8);

      hence thesis;

    end;

    theorem :: MUSIC_S1:82

    

     Th66: (( @ ( Octave (MS,frequency))) / ( @ (( spiral_of_fifths (MS,frequency,frequency)) . 3))) = (32 qua Real / 27)

    proof

      now

        thus (( spiral_of_fifths (MS,frequency,frequency)) . 3) = ((27 qua Real / 16) * ( @ frequency)) by Th60;

        ex fr be positive Real st frequency = fr & ( Octave (MS,frequency)) = (2 * fr) by Def15;

        hence ( @ ( Octave (MS,frequency))) = (2 * ( @ frequency));

      end;

      

      then (( @ ( Octave (MS,frequency))) / ( @ (( spiral_of_fifths (MS,frequency,frequency)) . 3))) = ((4 qua Real / 2) / (27 qua Real / 16)) by XCMPLX_1: 91

      .= (32 qua Real / 27);

      hence thesis;

    end;

    definition

      let MS be MusicSpace;

      let scale be Element of (2 -tuples_on the carrier of MS);

      :: MUSIC_S1:def54

      attr scale is monotonic means ex frequency be Element of MS, r1,r2 be positive Real st (scale . 1) = frequency & (scale . 1) = r1 & (scale . 2) = r2 & r1 < r2 & (scale . 2) = ( Octave (MS,frequency));

    end

    definition

      let MS be MusicSpace;

      let scale be Element of (3 -tuples_on the carrier of MS);

      :: MUSIC_S1:def55

      attr scale is ditonic means ex frequency be Element of MS, r1,r2,r3 be positive Real st (scale . 1) = frequency & (scale . 1) = r1 & (scale . 2) = r2 & (scale . 3) = r3 & r1 < r2 < r3 & (scale . 3) = ( Octave (MS,frequency));

    end

    definition

      let MS be MusicSpace;

      let scale be Element of (4 -tuples_on the carrier of MS);

      :: MUSIC_S1:def56

      attr scale is tritonic means ex frequency be Element of MS, r1,r2,r3,r4 be positive Real st (scale . 1) = frequency & (scale . 1) = r1 & (scale . 2) = r2 & (scale . 3) = r3 & (scale . 4) = r4 & r1 < r2 < r3 & r3 < r4 & (scale . 4) = ( Octave (MS,frequency));

    end

    definition

      let MS be MusicSpace;

      let scale be Element of (5 -tuples_on the carrier of MS);

      :: MUSIC_S1:def57

      attr scale is tetratonic means ex frequency be Element of MS, r1,r2,r3,r4,r5 be positive Real st (scale . 1) = frequency & (scale . 1) = r1 & (scale . 2) = r2 & (scale . 3) = r3 & (scale . 4) = r4 & (scale . 5) = r5 & r1 < r2 < r3 & r3 < r4 < r5 & (scale . 5) = ( Octave (MS,frequency));

    end

    definition

      let MS be MusicSpace;

      let n be natural Number;

      let scale be Element of (n -tuples_on the carrier of MS);

      :: MUSIC_S1:def58

      attr scale is pentatonic means n = 6 & ex frequency be Element of MS, r1,r2,r3,r4,r5,r6 be positive Real st (scale . 1) = frequency & (scale . 1) = r1 & (scale . 2) = r2 & (scale . 3) = r3 & (scale . 4) = r4 & (scale . 5) = r5 & (scale . 6) = r6 & r1 < r2 < r3 & r3 < r4 < r5 & r5 < r6 & (scale . 6) = ( Octave (MS,frequency));

    end

    definition

      let MS be MusicSpace;

      let scale be Element of (7 -tuples_on the carrier of MS);

      :: MUSIC_S1:def59

      attr scale is hexatonic means ex frequency be Element of MS, r1,r2,r3,r4,r5,r6,r7 be positive Real st (scale . 1) = frequency & (scale . 1) = r1 & (scale . 2) = r2 & (scale . 3) = r3 & (scale . 4) = r4 & (scale . 5) = r5 & (scale . 6) = r6 & (scale . 7) = r7 & r1 < r2 < r3 & r3 < r4 < r5 & r5 < r6 < r7 & (scale . 7) = ( Octave (MS,frequency));

    end

    definition

      let MS be MusicSpace;

      let n be natural Number;

      let scale be Element of (n -tuples_on the carrier of MS);

      :: MUSIC_S1:def60

      attr scale is heptatonic means n = 8 & ex frequency be Element of MS, r1,r2,r3,r4,r5,r6,r7,r8 be positive Real st (scale . 1) = frequency & (scale . 1) = r1 & (scale . 2) = r2 & (scale . 3) = r3 & (scale . 4) = r4 & (scale . 5) = r5 & (scale . 6) = r6 & (scale . 7) = r7 & (scale . 8) = r8 & r1 < r2 < r3 & r3 < r4 < r5 & r5 < r6 < r7 & r7 < r8 & (scale . 8) = ( Octave (MS,frequency));

    end

    definition

      let MS be MusicSpace;

      let scale be Element of (9 -tuples_on the carrier of MS);

      :: MUSIC_S1:def61

      attr scale is octatonic means ex frequency be Element of MS, r1,r2,r3,r4,r5,r6,r7,r8,r9 be positive Real st (scale . 1) = frequency & (scale . 1) = r1 & (scale . 2) = r2 & (scale . 3) = r3 & (scale . 4) = r4 & (scale . 5) = r5 & (scale . 6) = r6 & (scale . 7) = r7 & (scale . 8) = r8 & (scale . 9) = r9 & r1 < r2 < r3 & r3 < r4 < r5 & r5 < r6 < r7 & r7 < r8 < r9 & (scale . 9) = ( Octave (MS,frequency));

    end

    begin

    definition

      let MS be MusicSpace;

      let frequency be Element of MS;

      :: MUSIC_S1:def62

      func pentatonic_pythagorean_scale (MS,frequency) -> Element of (6 -tuples_on the carrier of MS) means

      : Def20: (it . 1) = frequency & (it . 2) = (( spiral_of_fifths (MS,frequency,frequency)) . 2) & (it . 3) = (( spiral_of_fifths (MS,frequency,frequency)) . 4) & (it . 4) = (( spiral_of_fifths (MS,frequency,frequency)) . 1) & (it . 5) = (( spiral_of_fifths (MS,frequency,frequency)) . 3) & (it . 6) = ( Octave (MS,frequency));

      existence

      proof

        defpred P[ set, set] means ($1 = 1 implies $2 = frequency) & ($1 = 2 implies $2 = (( spiral_of_fifths (MS,frequency,frequency)) . 2)) & ($1 = 3 implies $2 = (( spiral_of_fifths (MS,frequency,frequency)) . 4)) & ($1 = 4 implies $2 = (( spiral_of_fifths (MS,frequency,frequency)) . 1)) & ($1 = 5 implies $2 = (( spiral_of_fifths (MS,frequency,frequency)) . 3)) & ($1 = 6 implies $2 = ( Octave (MS,frequency)));

        

         A1: for k be Nat st k in ( Seg 6) holds ex x be Element of MS st P[k, x]

        proof

          let k be Nat;

          assume k in ( Seg 6);

          then 1 <= k <= 6 by FINSEQ_1: 1;

          then k = 1 or ... or k = 6;

          hence thesis;

        end;

        consider p be FinSequence of the carrier of MS such that

         A2: ( dom p) = ( Seg 6) and

         A3: for k be Nat st k in ( Seg 6) holds P[k, (p . k)] from FINSEQ_1:sch 5( A1);

        ( len p) = 6 by A2, FINSEQ_1:def 3;

        then

        reconsider p as Element of (6 -tuples_on the carrier of MS) by FINSEQ_2: 92;

        take p;

        1 in ( Seg 6) & 2 in ( Seg 6) & 3 in ( Seg 6) & 4 in ( Seg 6) & 5 in ( Seg 6) & 6 in ( Seg 6) by FINSEQ_1: 1;

        hence thesis by A3;

      end;

      uniqueness

      proof

        let p1,p2 be Element of (6 -tuples_on the carrier of MS) such that

         A4: (p1 . 1) = frequency & (p1 . 2) = (( spiral_of_fifths (MS,frequency,frequency)) . 2) & (p1 . 3) = (( spiral_of_fifths (MS,frequency,frequency)) . 4) & (p1 . 4) = (( spiral_of_fifths (MS,frequency,frequency)) . 1) & (p1 . 5) = (( spiral_of_fifths (MS,frequency,frequency)) . 3) & (p1 . 6) = ( Octave (MS,frequency)) and

         A5: (p2 . 1) = frequency & (p2 . 2) = (( spiral_of_fifths (MS,frequency,frequency)) . 2) & (p2 . 3) = (( spiral_of_fifths (MS,frequency,frequency)) . 4) & (p2 . 4) = (( spiral_of_fifths (MS,frequency,frequency)) . 1) & (p2 . 5) = (( spiral_of_fifths (MS,frequency,frequency)) . 3) & (p2 . 6) = ( Octave (MS,frequency));

        now

          ( len p1) = 6 & ( len p2) = 6 by FINSEQ_2: 132;

          then ( dom p1) = ( Seg 6) & ( dom p2) = ( Seg 6) by FINSEQ_1:def 3;

          hence ( dom p1) = ( dom p2);

          hereby

            let i be object;

            assume

             A6: i in ( dom p1);

            then

            reconsider j = i as Nat;

            j in ( Seg ( len p1)) by A6, FINSEQ_1:def 3;

            then j in ( Seg 6) by FINSEQ_2: 132;

            then 1 <= j <= 6 by FINSEQ_1: 1;

            then j = 1 or ... or j = 6;

            hence (p1 . i) = (p2 . i) by A4, A5;

          end;

        end;

        hence thesis by FUNCT_1:def 11;

      end;

    end

    reserve MS for MusicSpace,

fondamentale,frequency,f1,f2 for Element of MS;

    theorem :: MUSIC_S1:83

    

     Th67: ( pentatonic_pythagorean_scale (MS,frequency)) is pentatonic

    proof

      set scale = ( pentatonic_pythagorean_scale (MS,frequency));

      

       A1: (scale . 1) = frequency & (scale . 2) = (( spiral_of_fifths (MS,frequency,frequency)) . 2) & (scale . 3) = (( spiral_of_fifths (MS,frequency,frequency)) . 4) & (scale . 4) = (( spiral_of_fifths (MS,frequency,frequency)) . 1) & (scale . 5) = (( spiral_of_fifths (MS,frequency,frequency)) . 3) & (scale . 6) = ( Octave (MS,frequency)) by Def20;

      scale in (6 -tuples_on the carrier of MS);

      then scale in { s where s be Element of (the carrier of MS * ) : ( len s) = 6 } by FINSEQ_2:def 4;

      then

      consider s be Element of (the carrier of MS * ) such that

       A2: s = scale and

       A3: ( len s) = 6;

      ( dom s) = ( Seg 6) by A3, FINSEQ_1:def 3;

      then

      reconsider g1 = (scale . 1), g2 = (scale . 2), g3 = (scale . 3), g4 = (scale . 4), g5 = (scale . 5), g6 = (scale . 6) as Element of the carrier of MS by A2, FINSEQ_1: 1, FINSEQ_2: 11;

      now

        reconsider frequency = g1 as Element of MS;

        take frequency;

        reconsider r1 = ( @ frequency), r2 = ( @ g2), r3 = ( @ g3), r4 = ( @ g4), r5 = ( @ g5), r6 = ( @ g6) as positive Real;

        take r1, r2, r3, r4, r5, r6;

        thus (scale . 1) = frequency & (scale . 1) = r1 & (scale . 2) = r2 & (scale . 3) = r3 & (scale . 4) = r4 & (scale . 5) = r5 & (scale . 6) = r6;

        now

          thus r1 = (1 * ( @ frequency));

          thus r2 = ((9 qua Real / 8) * ( @ frequency)) by Th59, A1;

          thus r3 = ((81 qua Real / 64) * ( @ frequency)) by A1, Th61;

          thus r4 = ((3 qua Real / 2) * ( @ frequency)) by A1, Th58;

          thus r5 = ((27 qua Real / 16) * ( @ frequency)) by A1, Th60;

          ex fr be positive Real st frequency = fr & ( Octave (MS,frequency)) = (2 * fr) by Def15;

          hence r6 = (2 * ( @ frequency)) by A1;

        end;

        hence r1 < r2 < r3 & r3 < r4 < r5 & r5 < r6 by XREAL_1: 68;

        thus (scale . 6) = ( Octave (MS,frequency)) by A1;

      end;

      hence thesis;

    end;

    definition

      let MS be MusicSpace;

      let f1,f2 be Element of MS;

      :: MUSIC_S1:def63

      func intrval (f1,f2) -> positive Real means

      : Def21: ex r1,r2 be positive Real st r1 = f1 & r2 = f2 & it = (r2 / r1);

      existence

      proof

        reconsider r = (( @ f2) / ( @ f1)) as positive Real;

        take r;

        thus thesis;

      end;

      uniqueness ;

    end

    definition

      :: MUSIC_S1:def64

      func pythagorean_tone -> positive Real equals (9 qua Real / 8);

      coherence ;

    end

    definition

      :: MUSIC_S1:def65

      func pentatonic_pythagorean_semiditone -> positive Real equals (32 qua Real / 27);

      coherence ;

    end

    definition

      :: MUSIC_S1:def66

      func major_third_pythagorean_tone -> positive Real equals ( pythagorean_tone * pythagorean_tone );

      coherence ;

    end

    definition

      :: MUSIC_S1:def67

      func pure_major_third -> positive Real equals (5 qua Real / 4);

      coherence ;

    end

    definition

      :: MUSIC_S1:def68

      func syntonic_comma -> positive Real equals ( major_third_pythagorean_tone / pure_major_third );

      coherence ;

    end

    theorem :: MUSIC_S1:84

     syntonic_comma = (81 qua Real / 80);

    theorem :: MUSIC_S1:85

     pythagorean_tone < pentatonic_pythagorean_semiditone ;

    theorem :: MUSIC_S1:86

    (((( pythagorean_tone * pythagorean_tone ) * pentatonic_pythagorean_semiditone ) * pythagorean_tone ) * pentatonic_pythagorean_semiditone ) = 2;

    definition

      let MS be MusicSpace;

      let frequency be Element of MS;

      :: MUSIC_S1:def69

      func penta_fondamentale (MS,frequency) -> Element of MS equals (( pentatonic_pythagorean_scale (MS,frequency)) . 1);

      coherence by Def20;

      :: MUSIC_S1:def70

      func penta_1 (MS,frequency) -> Element of MS equals (( pentatonic_pythagorean_scale (MS,frequency)) . 2);

      coherence

      proof

        (( pentatonic_pythagorean_scale (MS,frequency)) . 2) = (( spiral_of_fifths (MS,frequency,frequency)) . 2) by Def20;

        hence thesis;

      end;

      :: MUSIC_S1:def71

      func penta_2 (MS,frequency) -> Element of MS equals (( pentatonic_pythagorean_scale (MS,frequency)) . 3);

      coherence

      proof

        (( pentatonic_pythagorean_scale (MS,frequency)) . 3) = (( spiral_of_fifths (MS,frequency,frequency)) . 4) by Def20;

        hence thesis;

      end;

      :: MUSIC_S1:def72

      func penta_3 (MS,frequency) -> Element of MS equals (( pentatonic_pythagorean_scale (MS,frequency)) . 4);

      coherence

      proof

        (( pentatonic_pythagorean_scale (MS,frequency)) . 4) = (( spiral_of_fifths (MS,frequency,frequency)) . 1) by Def20;

        hence thesis;

      end;

      :: MUSIC_S1:def73

      func penta_4 (MS,frequency) -> Element of MS equals (( pentatonic_pythagorean_scale (MS,frequency)) . 5);

      coherence

      proof

        (( pentatonic_pythagorean_scale (MS,frequency)) . 5) = (( spiral_of_fifths (MS,frequency,frequency)) . 3) by Def20;

        hence thesis;

      end;

      :: MUSIC_S1:def74

      func penta_octave (MS,frequency) -> Element of MS equals ( Octave (MS,frequency));

      coherence ;

    end

    theorem :: MUSIC_S1:87

    ex r1,r2 be Element of REALPLUS st ( intrval (f1,f2)) = ( REAL_ratio (r1,r2))

    proof

      the carrier of MS c= REALPLUS by Def07a;

      then

      reconsider r1 = f1, r2 = f2 as Element of REALPLUS ;

      consider r,s be positive Real such that

       A1: r1 = r & r2 = s & ( REAL_ratio (r1,r2)) = (s / r) by Def01;

      ( intrval (f1,f2)) = (s / r) & ( REAL_ratio (r1,r2)) = (s / r) by A1, Def21;

      hence thesis;

    end;

    theorem :: MUSIC_S1:88

    

     Th68: for r1,r2,r3,r4,r5,r6 be positive Real st (( pentatonic_pythagorean_scale (MS,frequency)) . 1) = r1 & (( pentatonic_pythagorean_scale (MS,frequency)) . 2) = r2 & (( pentatonic_pythagorean_scale (MS,frequency)) . 3) = r3 & (( pentatonic_pythagorean_scale (MS,frequency)) . 4) = r4 & (( pentatonic_pythagorean_scale (MS,frequency)) . 5) = r5 & (( pentatonic_pythagorean_scale (MS,frequency)) . 6) = r6 holds (r2 / r1) = (9 qua Real / 8) & (r3 / r2) = (9 qua Real / 8) & (r4 / r3) = (32 qua Real / 27) & (r5 / r4) = (9 qua Real / 8) & (r6 / r5) = (32 qua Real / 27)

    proof

      let r1,r2,r3,r4,r5,r6 be positive Real;

      assume

       A1: (( pentatonic_pythagorean_scale (MS,frequency)) . 1) = r1 & (( pentatonic_pythagorean_scale (MS,frequency)) . 2) = r2 & (( pentatonic_pythagorean_scale (MS,frequency)) . 3) = r3 & (( pentatonic_pythagorean_scale (MS,frequency)) . 4) = r4 & (( pentatonic_pythagorean_scale (MS,frequency)) . 5) = r5 & (( pentatonic_pythagorean_scale (MS,frequency)) . 6) = r6;

      set gamme = ( pentatonic_pythagorean_scale (MS,frequency));

      

       A2: (gamme . 1) = frequency & (gamme . 2) = (( spiral_of_fifths (MS,frequency,frequency)) . 2) & (gamme . 3) = (( spiral_of_fifths (MS,frequency,frequency)) . 4) & (gamme . 4) = (( spiral_of_fifths (MS,frequency,frequency)) . 1) & (gamme . 5) = (( spiral_of_fifths (MS,frequency,frequency)) . 3) & (gamme . 6) = ( Octave (MS,frequency)) by Def20;

      gamme is pentatonic by Th67;

      then

      consider frequency be Element of MS, r1,r2,r3,r4,r5,r6 be positive Real such that

       A3: (gamme . 1) = frequency & (gamme . 1) = r1 & (gamme . 2) = r2 & (gamme . 3) = r3 & (gamme . 4) = r4 & (gamme . 5) = r5 & (gamme . 6) = r6 & r1 < r2 < r3 & r3 < r4 < r5 & r5 < r6 & (gamme . 6) = ( Octave (MS,frequency));

      (( @ (( spiral_of_fifths (MS,frequency,frequency)) . 2)) / ( @ frequency)) = ((3 * 3) qua Real / ((2 * 2) * 2)) & (( @ (( spiral_of_fifths (MS,frequency,frequency)) . 4)) / ( @ (( spiral_of_fifths (MS,frequency,frequency)) . 2))) = ((3 * 3) qua Real / ((2 * 2) * 2)) & (( @ (( spiral_of_fifths (MS,frequency,frequency)) . 1)) / ( @ (( spiral_of_fifths (MS,frequency,frequency)) . 4))) = (32 qua Real / 27) & (( @ (( spiral_of_fifths (MS,frequency,frequency)) . 3)) / ( @ (( spiral_of_fifths (MS,frequency,frequency)) . 1))) = (9 qua Real / 8) & (( @ ( Octave (MS,frequency))) / ( @ (( spiral_of_fifths (MS,frequency,frequency)) . 3))) = (32 qua Real / 27) by Th62, Th63, Th64, Th65, Th66;

      hence thesis by A1, A2, A3;

    end;

    theorem :: MUSIC_S1:89

    

     Th69: ex r1,r2,r3,r4,r5,r6 be positive Real st (( pentatonic_pythagorean_scale (MS,frequency)) . 1) = r1 & (( pentatonic_pythagorean_scale (MS,frequency)) . 2) = r2 & (( pentatonic_pythagorean_scale (MS,frequency)) . 3) = r3 & (( pentatonic_pythagorean_scale (MS,frequency)) . 4) = r4 & (( pentatonic_pythagorean_scale (MS,frequency)) . 5) = r5 & (( pentatonic_pythagorean_scale (MS,frequency)) . 6) = r6 & (r2 / r1) = (9 qua Real / 8) & (r3 / r2) = (9 qua Real / 8) & (r4 / r3) = (32 qua Real / 27) & (r5 / r4) = (9 qua Real / 8) & (r6 / r5) = (32 qua Real / 27)

    proof

      set r1 = ( penta_fondamentale (MS,frequency)), r2 = ( penta_1 (MS,frequency)), r3 = ( penta_2 (MS,frequency)), r4 = ( penta_3 (MS,frequency)), r5 = ( penta_4 (MS,frequency)), r6 = ( penta_octave (MS,frequency));

      the carrier of MS c= REALPLUS by Def07a;

      then

      reconsider r91 = r1, r92 = r2, r93 = r3, r94 = r4, r95 = r5, r96 = r6 as positive Real by Th1;

      

       A1: (( pentatonic_pythagorean_scale (MS,frequency)) . 1) = r91 & (( pentatonic_pythagorean_scale (MS,frequency)) . 2) = r92 & (( pentatonic_pythagorean_scale (MS,frequency)) . 3) = r93 & (( pentatonic_pythagorean_scale (MS,frequency)) . 4) = r94 & (( pentatonic_pythagorean_scale (MS,frequency)) . 5) = r95 & (( pentatonic_pythagorean_scale (MS,frequency)) . 6) = r96 by Def20;

      then (r92 / r91) = (9 qua Real / 8) & (r93 / r92) = (9 qua Real / 8) & (r94 / r93) = (32 qua Real / 27) & (r95 / r94) = (9 qua Real / 8) & (r96 / r95) = (32 qua Real / 27) by Th68;

      hence thesis by A1;

    end;

    theorem :: MUSIC_S1:90

    (9 qua Real / 8) = (9 qua Rational / 8);

    theorem :: MUSIC_S1:91

    ( intrval (( penta_fondamentale (MS,frequency)),( penta_1 (MS,frequency)))) = pythagorean_tone & ( intrval (( penta_1 (MS,frequency)),( penta_2 (MS,frequency)))) = pythagorean_tone & ( intrval (( penta_2 (MS,frequency)),( penta_3 (MS,frequency)))) = pentatonic_pythagorean_semiditone & ( intrval (( penta_3 (MS,frequency)),( penta_4 (MS,frequency)))) = pythagorean_tone & ( intrval (( penta_4 (MS,frequency)),( penta_octave (MS,frequency)))) = pentatonic_pythagorean_semiditone

    proof

      consider r1,r2 be positive Real such that

       A1: r1 = ( penta_fondamentale (MS,frequency)) & r2 = ( penta_1 (MS,frequency)) & ( intrval (( penta_fondamentale (MS,frequency)),( penta_1 (MS,frequency)))) = (r2 / r1) by Def21;

      consider r3,r4 be positive Real such that

       A2: r3 = ( penta_1 (MS,frequency)) & r4 = ( penta_2 (MS,frequency)) & ( intrval (( penta_1 (MS,frequency)),( penta_2 (MS,frequency)))) = (r4 / r3) by Def21;

      consider r5,r6 be positive Real such that

       A3: r5 = ( penta_2 (MS,frequency)) & r6 = ( penta_3 (MS,frequency)) & ( intrval (( penta_2 (MS,frequency)),( penta_3 (MS,frequency)))) = (r6 / r5) by Def21;

      consider r7,r8 be positive Real such that

       A4: r7 = ( penta_3 (MS,frequency)) & r8 = ( penta_4 (MS,frequency)) & ( intrval (( penta_3 (MS,frequency)),( penta_4 (MS,frequency)))) = (r8 / r7) by Def21;

      consider r9,r10 be positive Real such that

       A5: r9 = ( penta_4 (MS,frequency)) & r10 = ( penta_octave (MS,frequency)) & ( intrval (( penta_4 (MS,frequency)),( penta_octave (MS,frequency)))) = (r10 / r9) by Def21;

      ex s1,s2,s3,s4,s5,s6 be positive Real st (( pentatonic_pythagorean_scale (MS,frequency)) . 1) = s1 & (( pentatonic_pythagorean_scale (MS,frequency)) . 2) = s2 & (( pentatonic_pythagorean_scale (MS,frequency)) . 3) = s3 & (( pentatonic_pythagorean_scale (MS,frequency)) . 4) = s4 & (( pentatonic_pythagorean_scale (MS,frequency)) . 5) = s5 & (( pentatonic_pythagorean_scale (MS,frequency)) . 6) = s6 & (s2 / s1) = (9 qua Real / 8) & (s3 / s2) = (9 qua Real / 8) & (s4 / s3) = (32 qua Real / 27) & (s5 / s4) = (9 qua Real / 8) & (s6 / s5) = (32 qua Real / 27) by Th69;

      hence ( intrval (( penta_fondamentale (MS,frequency)),( penta_1 (MS,frequency)))) = pythagorean_tone & ( intrval (( penta_1 (MS,frequency)),( penta_2 (MS,frequency)))) = pythagorean_tone & ( intrval (( penta_2 (MS,frequency)),( penta_3 (MS,frequency)))) = pentatonic_pythagorean_semiditone & ( intrval (( penta_3 (MS,frequency)),( penta_4 (MS,frequency)))) = pythagorean_tone & ( intrval (( penta_4 (MS,frequency)),( penta_octave (MS,frequency)))) = pentatonic_pythagorean_semiditone by A1, A2, A3, A4, A5, Def20;

    end;

    theorem :: MUSIC_S1:92

    ( Fifth (MS,frequency)) is_Between (frequency,( Octave (MS,frequency)))

    proof

      consider fr be positive Real such that

       A1: frequency = fr & ( Fifth (MS,frequency)) = ((3 qua Real / 2) * fr) by Def12;

      

       A2: ex fr be positive Real st frequency = fr & ( Octave (MS,frequency)) = (2 * fr) by Def15;

      reconsider x = ((3 qua Real / 2) * fr) as positive Real;

      (1 * fr) <= x < (2 * fr) by XREAL_1: 68;

      hence thesis by A2, A1;

    end;

    theorem :: MUSIC_S1:93

    

     Th70: for r1,r2 be positive Real st f1 = r1 & f2 = r2 & r2 = ((4 qua Real / 3) * r1) holds ( Fifth (MS,f2)) = (2 * r1) & not ( Fifth (MS,f2)) is_Between (f1,( Octave (MS,f1)))

    proof

      let r1,r2 be positive Real;

      assume that

       A1: f1 = r1 and

       A2: f2 = r2 and

       A3: r2 = ((4 qua Real / 3) * r1);

      

       A4: ex fr be positive Real st f2 = fr & ( Fifth (MS,f2)) = ((3 qua Real / 2) * fr) by Def12;

      hence ( Fifth (MS,f2)) = (2 * r1) by A2, A3;

      ex fr be positive Real st f1 = fr & ( Octave (MS,f1)) = (2 * fr) by Def15;

      hence not ( Fifth (MS,f2)) is_Between (f1,( Octave (MS,f1))) by A4, A3, A2, A1;

    end;

    theorem :: MUSIC_S1:94

    

     Th71: for r1,r2 be positive Real st f1 = r1 & f2 = r2 & r2 = ((4 qua Real / 3) * r1) holds (( Fifth (MS,f2)) is_Between (fondamentale,( Octave (MS,fondamentale))) implies ( Octave_descendent (MS,( Fifth_reduct (MS,fondamentale,f2)))) = f1) & ( not ( Fifth (MS,f2)) is_Between (fondamentale,( Octave (MS,fondamentale))) implies ( Fifth_reduct (MS,fondamentale,f2)) = f1)

    proof

      let r1,r2 be positive Real;

      assume that

       A1: f1 = r1 & f2 = r2 and

       A2: r2 = ((4 qua Real / 3) * r1);

      thus ( Fifth (MS,f2)) is_Between (fondamentale,( Octave (MS,fondamentale))) implies ( Octave_descendent (MS,( Fifth_reduct (MS,fondamentale,f2)))) = f1

      proof

        assume

         A3: ( Fifth (MS,f2)) is_Between (fondamentale,( Octave (MS,fondamentale)));

        

         A4: ex fr be positive Real st f2 = fr & ( Fifth (MS,f2)) = ((3 qua Real / 2) * fr) by Def12;

        ex r be positive Real st ( Fifth_reduct (MS,fondamentale,f2)) = r & ( Octave_descendent (MS,( Fifth_reduct (MS,fondamentale,f2)))) = (r / 2) by Th51;

        

        then ( Octave_descendent (MS,( Fifth_reduct (MS,fondamentale,f2)))) = ((2 qua Real * r1) / 2) by A3, A4, Def18, A1, A2

        .= f1 by A1;

        hence thesis;

      end;

      thus not ( Fifth (MS,f2)) is_Between (fondamentale,( Octave (MS,fondamentale))) implies ( Fifth_reduct (MS,fondamentale,f2)) = f1

      proof

        assume

         A5: not ( Fifth (MS,f2)) is_Between (fondamentale,( Octave (MS,fondamentale)));

        consider fr be positive Real such that

         A6: f2 = fr & ( Fifth (MS,f2)) = ((3 qua Real / 2) * fr) by Def12;

        ex r be positive Real st ( Fifth (MS,f2)) = r & ( Octave_descendent (MS,( Fifth (MS,f2)))) = (r / 2) by Th51;

        hence thesis by A1, A2, A6, A5, Def18;

      end;

    end;

    theorem :: MUSIC_S1:95

    for r1,r2 be positive Real st f1 = r1 & f2 = r2 & r2 = ((4 qua Real / 3) * r1) holds ( Fifth_reduct (MS,f1,f2)) = f1

    proof

      let r1,r2 be positive Real;

      assume

       A1: f1 = r1 & f2 = r2 & r2 = ((4 qua Real / 3) * r1);

      then (( Fifth (MS,f2)) is_Between (f1,( Octave (MS,f1))) implies ( Octave_descendent (MS,( Fifth_reduct (MS,f1,f2)))) = f1) & ( not ( Fifth (MS,f2)) is_Between (f1,( Octave (MS,f1))) implies ( Fifth_reduct (MS,f1,f2)) = f1) by Th71;

      hence thesis by A1, Th70;

    end;

    begin

    definition

      let S be MusicSpace;

      :: MUSIC_S1:def75

      attr S is satisfying_fourth_constructible means

      : Def22: for frequency be Element of S holds ex q be Element of S st [frequency, q] in ( fourth S);

    end

    theorem :: MUSIC_S1:96

    

     Th78: for MS be MusicSpace st MS = REAL_Music holds for frequency be Element of MS holds ex fr,qr be positive Real st fr = frequency & qr = ((4 qua Real / 3) * fr) & [fr, qr] in ( fourth MS)

    proof

      let MS be MusicSpace;

      assume

       A1: MS = REAL_Music ;

      now

        let frequency be Element of MS;

        reconsider f = frequency as positive Real by A1, Th1;

        reconsider qr = ((4 qua Real / 3) * f) as positive Real;

        reconsider q = qr as Element of MS by A1, Th1;

        take f, qr;

        thus f = frequency;

        thus qr = ((4 qua Real / 3) * f);

        reconsider n2 = 3, n3 = 4 as Element of MS by Th20;

        reconsider x = [n2, n3], y = [frequency, q] as Element of [: REALPLUS , REALPLUS :] by A1;

        reconsider z = [frequency, q] as Element of [: REALPLUS , REALPLUS :] by A1;

        consider x9,y9 be Element of REALPLUS such that

         A2: z = [x9, y9] and

         A3: ( REAL_ratio . z) = ( REAL_ratio (x9,y9)) by Def02;

        consider r,s be positive Real such that

         A4: x9 = r & s = y9 & ( REAL_ratio (x9,y9)) = (s / r) by Def01;

        consider x99,y99 be Element of REALPLUS such that

         A5: x = [x99, y99] and

         A6: ( REAL_ratio . x) = ( REAL_ratio (x99,y99)) by Def02;

        consider r9,s9 be positive Real such that

         A7: x99 = r9 & s9 = y99 & ( REAL_ratio (x99,y99)) = (s9 / r9) by Def01;

        

         A8: n2 = r9 & n3 = s9 & r = frequency & s = q by A4, A2, A5, A7, XTUPLE_0: 1;

        now

          thus ( REAL_ratio . (n2,n3)) = (4 qua Real / 3 qua Real) by A7, A8, A6, BINOP_1:def 1;

          

          thus ( REAL_ratio . (frequency,q)) = (s / r) by A3, A4, BINOP_1:def 1

          .= (4 qua Real / 3) by A8, XCMPLX_1: 89;

        end;

        then (n2,n3) equiv (frequency,q) by A1, Def08a;

        hence [f, qr] in ( fourth MS) by EQREL_1: 18;

      end;

      hence thesis;

    end;

    theorem :: MUSIC_S1:97

    

     Th79: REAL_Music is satisfying_fourth_constructible

    proof

      set MS = REAL_Music ;

      let frequency be Element of MS;

      consider fr,qr be positive Real such that

       A1: fr = frequency and qr = ((4 qua Real / 3) * fr) and

       A2: [fr, qr] in ( fourth MS) by Th78;

      fr is Element of MS & qr is Element of MS by Th1;

      hence thesis by A1, A2;

    end;

    registration

      cluster satisfying_fourth_constructible for MusicSpace;

      existence by Th79;

    end

    definition

      let MS be satisfying_fourth_constructible MusicSpace;

      let frequency be Element of MS;

      :: MUSIC_S1:def76

      func Fourth (MS,frequency) -> Element of MS means

      : Def23: [frequency, it ] in ( fourth MS);

      existence by Def22;

      uniqueness

      proof

        let q1,q2 be Element of MS such that

         A1: [frequency, q1] in ( fourth MS) and

         A2: [frequency, q2] in ( fourth MS);

        reconsider n2 = 3, n3 = 4 as Element of MS by Th20;

        

         A3: (n2,n3) equiv (frequency,q1) by A1, EQREL_1: 18;

        (n2,n3) equiv (frequency,q2) by A2, EQREL_1: 18;

        then (frequency,q2) equiv (n2,n3) by Th22;

        hence thesis by Th24, A3, Th23;

      end;

    end

    definition

      let MS be satisfying_fourth_constructible MusicSpace;

      :: MUSIC_S1:def77

      attr MS is classical_fourth means

      : Def24: for frequency be Element of MS holds ex fr be positive Real st frequency = fr & ( Fourth (MS,frequency)) = ((4 qua Real / 3) * fr);

    end

    theorem :: MUSIC_S1:98

    

     Th80: for MS be satisfying_fourth_constructible MusicSpace st MS = REAL_Music holds for frequency be Element of MS holds ex fr be positive Real st frequency = fr & ( Fourth (MS,frequency)) = ((4 qua Real / 3) * fr)

    proof

      let MS be satisfying_fourth_constructible MusicSpace;

      assume

       A1: MS = REAL_Music ;

      let frequency be Element of MS;

      reconsider fr = frequency as positive Real by A1, Th1;

      take fr;

      thus frequency = fr;

      consider fr9,qr9 be positive Real such that

       A2: fr9 = frequency and

       A3: qr9 = ((4 qua Real / 3) * fr9) and

       A4: [fr9, qr9] in ( fourth MS) by A1, Th78;

      reconsider qr9 as Element of MS by A1, Th1;

      qr9 = ( Fourth (MS,frequency)) by A2, A4, Def23;

      hence thesis by A2, A3;

    end;

    registration

      cluster classical_fourth for satisfying_fourth_constructible MusicSpace;

      existence

      proof

        reconsider MS = REAL_Music as satisfying_fourth_constructible MusicSpace by Th79;

        take MS;

        thus thesis by Th80;

      end;

    end

    definition

      let MS be satisfying_Real non empty MusicStruct;

      :: MUSIC_S1:def78

      attr MS is satisfying_euclidean means

      : Def25: for f1,f2 be Element of MS holds (the Ratio of MS . (f1,f2)) = (( @ f2) / ( @ f1));

    end

    registration

      cluster satisfying_euclidean for satisfying_Real non empty MusicStruct;

      existence

      proof

        reconsider MS = REAL_Music as MusicSpace;

        now

          let f1,f2 be Element of REAL_Music ;

          reconsider x = [f1, f2] as Element of [: REALPLUS , REALPLUS :];

          consider y9,z9 be Element of REALPLUS such that

           A1: x = [y9, z9] and

           A2: ( REAL_ratio . x) = ( REAL_ratio (y9,z9)) by Def02;

          consider y99,z99 be Element of REALPLUS such that

           A3: x = [y99, z99] and ( REAL_ratio . x) = ( REAL_ratio (y99,z99)) by Def02;

          consider r,s be positive Real such that

           A4: y99 = r & s = z99 & ( REAL_ratio (y99,z99)) = (s / r) by Def01;

          

           A5: s = ( @ f2) & r = ( @ f1) by A4, A3, XTUPLE_0: 1;

          

           A6: y99 = y9 & z99 = z9 by A1, A3, XTUPLE_0: 1;

          thus (the Ratio of REAL_Music . (f1,f2)) = (( @ f2) / ( @ f1)) by A2, BINOP_1:def 1, A5, A6, A4;

        end;

        then MS is satisfying_euclidean;

        hence thesis;

      end;

    end

    registration

      cluster satisfying_euclidean -> satisfying_interval for satisfying_Real non empty MusicStruct;

      coherence

      proof

        let S be satisfying_Real non empty MusicStruct;

        assume

         A1: S is satisfying_euclidean;

        now

          let f1,f2,f3 be Element of S;

          assume (the Ratio of S . (f1,f2)) = (the Ratio of S . (f1,f3));

          then (( @ f2) / ( @ f1)) = (the Ratio of S . (f1,f3)) by A1;

          then (( @ f2) / ( @ f1)) = (( @ f3) / ( @ f1)) by A1;

          hence f2 = f3 by XCMPLX_1: 53;

        end;

        hence thesis;

      end;

    end

    registration

      cluster satisfying_euclidean -> satisfying_tonic for satisfying_Real non empty MusicStruct;

      coherence

      proof

        let S be satisfying_Real non empty MusicStruct;

        assume

         A1: S is satisfying_euclidean;

        now

          let f1,f2,f3 be Element of S;

          assume (the Ratio of S . (f1,f1)) = (the Ratio of S . (f2,f3));

          then (( @ f1) / ( @ f1)) = (the Ratio of S . (f2,f3)) by A1;

          then (( @ f1) / ( @ f1)) = (( @ f3) / ( @ f2)) by A1;

          hence f2 = f3 by XCMPLX_1: 58, XCMPLX_1: 60;

        end;

        hence thesis;

      end;

    end

    registration

      cluster satisfying_euclidean -> satisfying_commutativity for satisfying_Real non empty MusicStruct;

      coherence

      proof

        let S be satisfying_Real non empty MusicStruct;

        assume

         A1: S is satisfying_euclidean;

        now

          let f1,f2,f3,f4 be Element of S;

          assume (the Ratio of S . (f2,f1)) = (the Ratio of S . (f4,f3));

          

          then

           A2: (( @ f1) / ( @ f2)) = (the Ratio of S . (f4,f3)) by A1

          .= (( @ f3) / ( @ f4)) by A1;

          

          thus (the Ratio of S . (f1,f2)) = (( @ f2) / ( @ f1)) by A1

          .= (1 / (( @ f1) / ( @ f2))) by XCMPLX_1: 57

          .= (( @ f4) / ( @ f3)) by A2, XCMPLX_1: 57

          .= (the Ratio of S . (f3,f4)) by A1;

        end;

        hence thesis;

      end;

    end

    registration

      cluster satisfying_euclidean for classical_fourth satisfying_fourth_constructible MusicSpace;

      existence

      proof

        reconsider MS = REAL_Music as satisfying_fourth_constructible MusicSpace by Th79;

        

         A1: MS is classical_fourth by Th80;

        now

          let f1,f2 be Element of REAL_Music ;

          reconsider x = [f1, f2] as Element of [: REALPLUS , REALPLUS :];

          consider y9,z9 be Element of REALPLUS such that

           A2: x = [y9, z9] and

           A3: ( REAL_ratio . x) = ( REAL_ratio (y9,z9)) by Def02;

          consider y99,z99 be Element of REALPLUS such that

           A4: x = [y99, z99] and ( REAL_ratio . x) = ( REAL_ratio (y99,z99)) by Def02;

          consider r,s be positive Real such that

           A5: y99 = r & s = z99 & ( REAL_ratio (y99,z99)) = (s / r) by Def01;

          

           A6: s = ( @ f2) & r = ( @ f1) by A5, A4, XTUPLE_0: 1;

          

           A7: y99 = y9 & z99 = z9 by A2, A4, XTUPLE_0: 1;

          thus (the Ratio of REAL_Music . (f1,f2)) = (( @ f2) / ( @ f1)) by A7, A5, A3, BINOP_1:def 1, A6;

        end;

        then MS is satisfying_euclidean;

        hence thesis by A1;

      end;

    end

    definition

      mode Heptatonic_Pythagorean_Score is classical_fourth satisfying_fourth_constructible MusicSpace;

    end

    reserve HPS for Heptatonic_Pythagorean_Score,

frequency for Element of HPS;

    definition

      let HPS be Heptatonic_Pythagorean_Score;

      let frequency be Element of HPS;

      :: MUSIC_S1:def79

      func heptatonic_pythagorean_scale (HPS,frequency) -> Element of (8 -tuples_on the carrier of HPS) means

      : Def26: (it . 1) = (( spiral_of_fifths (HPS,frequency,( Fourth (HPS,frequency)))) . 1) & (it . 2) = (( spiral_of_fifths (HPS,frequency,( Fourth (HPS,frequency)))) . 3) & (it . 3) = (( spiral_of_fifths (HPS,frequency,( Fourth (HPS,frequency)))) . 5) & (it . 4) = ( Fourth (HPS,frequency)) & (it . 5) = (( spiral_of_fifths (HPS,frequency,( Fourth (HPS,frequency)))) . 2) & (it . 6) = (( spiral_of_fifths (HPS,frequency,( Fourth (HPS,frequency)))) . 4) & (it . 7) = (( spiral_of_fifths (HPS,frequency,( Fourth (HPS,frequency)))) . 6) & (it . 8) = ( Octave (HPS,(( spiral_of_fifths (HPS,frequency,( Fourth (HPS,frequency)))) . 1)));

      existence

      proof

        set MS = HPS;

        defpred P[ set, set] means ($1 = 1 implies $2 = (( spiral_of_fifths (MS,frequency,( Fourth (MS,frequency)))) . 1)) & ($1 = 2 implies $2 = (( spiral_of_fifths (MS,frequency,( Fourth (MS,frequency)))) . 3)) & ($1 = 3 implies $2 = (( spiral_of_fifths (MS,frequency,( Fourth (MS,frequency)))) . 5)) & ($1 = 4 implies $2 = ( Fourth (MS,frequency))) & ($1 = 5 implies $2 = (( spiral_of_fifths (MS,frequency,( Fourth (MS,frequency)))) . 2)) & ($1 = 6 implies $2 = (( spiral_of_fifths (MS,frequency,( Fourth (MS,frequency)))) . 4)) & ($1 = 7 implies $2 = (( spiral_of_fifths (MS,frequency,( Fourth (MS,frequency)))) . 6)) & ($1 = 8 implies $2 = ( Octave (MS,(( spiral_of_fifths (MS,frequency,( Fourth (MS,frequency)))) . 1))));

        

         A1: for k be Nat st k in ( Seg 8) holds ex x be Element of MS st P[k, x]

        proof

          let k be Nat;

          assume k in ( Seg 8);

          then 1 <= k <= 8 by FINSEQ_1: 1;

          then k = 1 or ... or k = 8;

          hence thesis;

        end;

        consider p be FinSequence of the carrier of MS such that

         A2: ( dom p) = ( Seg 8) and

         A3: for k be Nat st k in ( Seg 8) holds P[k, (p . k)] from FINSEQ_1:sch 5( A1);

        ( len p) = 8 by A2, FINSEQ_1:def 3;

        then

        reconsider p as Element of (8 -tuples_on the carrier of MS) by FINSEQ_2: 92;

        take p;

        1 in ( Seg 8) & 2 in ( Seg 8) & 3 in ( Seg 8) & 4 in ( Seg 8) & 5 in ( Seg 8) & 6 in ( Seg 8) & 7 in ( Seg 8) & 8 in ( Seg 8) by FINSEQ_1: 1;

        hence thesis by A3;

      end;

      uniqueness

      proof

        set MS = HPS;

        let p1,p2 be Element of (8 -tuples_on the carrier of MS) such that

         A4: (p1 . 1) = (( spiral_of_fifths (MS,frequency,( Fourth (MS,frequency)))) . 1) & (p1 . 2) = (( spiral_of_fifths (MS,frequency,( Fourth (MS,frequency)))) . 3) & (p1 . 3) = (( spiral_of_fifths (MS,frequency,( Fourth (MS,frequency)))) . 5) & (p1 . 4) = ( Fourth (MS,frequency)) & (p1 . 5) = (( spiral_of_fifths (MS,frequency,( Fourth (MS,frequency)))) . 2) & (p1 . 6) = (( spiral_of_fifths (MS,frequency,( Fourth (MS,frequency)))) . 4) & (p1 . 7) = (( spiral_of_fifths (MS,frequency,( Fourth (MS,frequency)))) . 6) & (p1 . 8) = ( Octave (MS,(( spiral_of_fifths (MS,frequency,( Fourth (MS,frequency)))) . 1))) and

         A5: (p2 . 1) = (( spiral_of_fifths (MS,frequency,( Fourth (MS,frequency)))) . 1) & (p2 . 2) = (( spiral_of_fifths (MS,frequency,( Fourth (MS,frequency)))) . 3) & (p2 . 3) = (( spiral_of_fifths (MS,frequency,( Fourth (MS,frequency)))) . 5) & (p2 . 4) = ( Fourth (MS,frequency)) & (p2 . 5) = (( spiral_of_fifths (MS,frequency,( Fourth (MS,frequency)))) . 2) & (p2 . 6) = (( spiral_of_fifths (MS,frequency,( Fourth (MS,frequency)))) . 4) & (p2 . 7) = (( spiral_of_fifths (MS,frequency,( Fourth (MS,frequency)))) . 6) & (p2 . 8) = ( Octave (MS,(( spiral_of_fifths (MS,frequency,( Fourth (MS,frequency)))) . 1)));

        now

          ( len p1) = 8 & ( len p2) = 8 by FINSEQ_2: 132;

          then ( dom p1) = ( Seg 8) & ( dom p2) = ( Seg 8) by FINSEQ_1:def 3;

          hence ( dom p1) = ( dom p2);

          hereby

            let i be object;

            assume

             A6: i in ( dom p1);

            then

            reconsider j = i as Nat;

            j in ( Seg ( len p1)) by A6, FINSEQ_1:def 3;

            then j in ( Seg 8) by FINSEQ_2: 132;

            then 1 <= j <= 8 by FINSEQ_1: 1;

            then j = 1 or ... or j = 8;

            hence (p1 . i) = (p2 . i) by A4, A5;

          end;

        end;

        hence thesis by FUNCT_1:def 11;

      end;

    end

    theorem :: MUSIC_S1:99

    

     Th81: ( Fourth (HPS,frequency)) is_Between (frequency,( Octave (HPS,frequency)))

    proof

      set MS = HPS;

      consider fr be positive Real such that

       A1: frequency = fr and

       A2: ( Fourth (MS,frequency)) = ((4 qua Real / 3) * fr) by Def24;

      consider fr2 be positive Real such that

       A3: frequency = fr2 and

       A4: ( Octave (MS,frequency)) = (2 * fr2) by Def15;

      (1 * fr) <= ((4 qua Real / 3) * fr) < (2 * fr) by XREAL_1: 68;

      hence thesis by A3, A4, A1, A2;

    end;

    theorem :: MUSIC_S1:100

    for n be Nat holds (( spiral_of_fifths (HPS,frequency,( Fourth (HPS,frequency)))) . n) is_Between (frequency,( Octave (HPS,frequency))) by Th57, Th81;

    theorem :: MUSIC_S1:101

    

     Th82: (( spiral_of_fifths (HPS,frequency,( Fourth (HPS,frequency)))) . 1) = frequency

    proof

      set MS = HPS;

      set q = ( Fourth (MS,frequency)), f1 = (( spiral_of_fifths (MS,frequency,q)) . 1);

      consider frq be positive Real such that

       A1: frequency = frq & ( Fourth (MS,frequency)) = ((4 qua Real / 3) * frq) by Def24;

      reconsider n1 = 1, n0 = 0 as Nat;

      

       A2: (( spiral_of_fifths (MS,frequency,q)) . 1) = (( spiral_of_fifths (MS,frequency,q)) . (n0 + 1))

      .= ( Fifth_reduct (MS,frequency,(( spiral_of_fifths (MS,frequency,q)) . n0))) by Def19

      .= ( Fifth_reduct (MS,frequency,q)) by Def19;

      consider r,s be positive Real such that

       A3: r = q & s = ((3 qua Real / 2) * r) & ( Fifth (MS,q)) = s by Th54;

      consider fr2 be positive Real such that

       A4: frequency = fr2 and

       A5: ( Octave (MS,frequency)) = (2 * fr2) by Def15;

      consider ro be positive Real such that

       A6: ( Fifth (MS,q)) = ro and

       A7: ( Octave_descendent (MS,( Fifth (MS,q)))) = (ro / 2) by Th51;

       not ( Fifth (MS,q)) is_Between (frequency,( Octave (MS,frequency))) by A3, A1, A4, A5;

      hence thesis by A2, A6, A7, A3, A1, Def18;

    end;

    theorem :: MUSIC_S1:102

    

     Th83: (( spiral_of_fifths (HPS,frequency,( Fourth (HPS,frequency)))) . 2) = ((3 qua Real / 2) * ( @ frequency))

    proof

      set MS = HPS;

      set q = ( Fourth (MS,frequency));

      reconsider n1 = 1 as Nat;

      

       A1: (( spiral_of_fifths (MS,frequency,q)) . 2) = (( spiral_of_fifths (MS,frequency,q)) . (n1 + 1))

      .= ( Fifth_reduct (MS,frequency,(( spiral_of_fifths (MS,frequency,q)) . n1))) by Def19

      .= ( Fifth_reduct (MS,frequency,frequency)) by Th82;

      consider r,s be positive Real such that

       A2: r = frequency & s = ((3 qua Real / 2) * r) & ( Fifth (MS,frequency)) = s by Th54;

      

       A3: ex fr be positive Real st frequency = fr & ( Octave (MS,frequency)) = (2 * fr) by Def15;

      (1 * r) <= ((3 qua Real / 2) * r) & ((3 qua Real / 2) * r) < (2 * r) by XREAL_1: 68;

      then ( Fifth (MS,frequency)) is_Between (frequency,( Octave (MS,frequency))) by A2, A3;

      hence thesis by A1, A2, Def18;

    end;

    theorem :: MUSIC_S1:103

    

     Th84: (( spiral_of_fifths (HPS,frequency,( Fourth (HPS,frequency)))) . 3) = ((9 qua Real / 8) * ( @ frequency))

    proof

      set MS = HPS;

      set q = ( Fourth (MS,frequency));

      reconsider n1 = 2 as Nat;

      (( spiral_of_fifths (MS,frequency,q)) . n1) is Element of MS;

      then

      reconsider r32 = ((3 qua Real / 2) * ( @ frequency)) as Element of MS by Th83;

      

       A1: (( spiral_of_fifths (MS,frequency,q)) . 3) = (( spiral_of_fifths (MS,frequency,q)) . (n1 + 1))

      .= ( Fifth_reduct (MS,frequency,(( spiral_of_fifths (MS,frequency,q)) . n1))) by Def19

      .= ( Fifth_reduct (MS,frequency,r32)) by Th83;

      consider r,s be positive Real such that

       A2: r = r32 & s = ((3 qua Real / 2) * r) & ( Fifth (MS,r32)) = s by Th54;

      

       A3: (2 * ( @ frequency)) < ((9 qua Real / 4) * ( @ frequency)) by XREAL_1: 68;

      

       A4: ex r be positive Real st ( Fifth (MS,r32)) = r & ( Octave_descendent (MS,( Fifth (MS,r32)))) = (r / 2) by Th51;

       not ( Fifth (MS,r32)) is_Between (frequency,( Octave (MS,frequency)))

      proof

        assume

         A5: ( Fifth (MS,r32)) is_Between (frequency,( Octave (MS,frequency)));

        ex fr be positive Real st frequency = fr & ( Octave (MS,frequency)) = (2 * fr) by Def15;

        hence contradiction by A5, A2, A3;

      end;

      hence thesis by A1, A2, A4, Def18;

    end;

    theorem :: MUSIC_S1:104

    

     Th85: (( spiral_of_fifths (HPS,frequency,( Fourth (HPS,frequency)))) . 4) = ((27 qua Real / 16) * ( @ frequency))

    proof

      set MS = HPS;

      reconsider n2 = 3 as Nat;

      set q = ( Fourth (MS,frequency));

      (( spiral_of_fifths (MS,frequency,q)) . n2) is Element of MS;

      then

      reconsider r32 = ((9 qua Real / 8) * ( @ frequency)) as Element of MS by Th84;

      

       A1: (( spiral_of_fifths (MS,frequency,q)) . 4) = (( spiral_of_fifths (MS,frequency,q)) . (n2 + 1))

      .= ( Fifth_reduct (MS,frequency,(( spiral_of_fifths (MS,frequency,q)) . n2))) by Def19

      .= ( Fifth_reduct (MS,frequency,r32)) by Th84;

      consider r,s be positive Real such that

       A2: r = r32 & s = ((3 qua Real / 2) * r) & ( Fifth (MS,r32)) = s by Th54;

      

       A3: ex fr be positive Real st frequency = fr & ( Octave (MS,frequency)) = (2 * fr) by Def15;

      ((27 qua Real / 16) * ( @ frequency)) < (2 * ( @ frequency)) & (1 * ( @ frequency)) < ((27 qua Real / 16) * ( @ frequency)) by XREAL_1: 68;

      then ( Fifth (MS,r32)) is_Between (frequency,( Octave (MS,frequency))) by A2, A3;

      hence thesis by A2, A1, Def18;

    end;

    theorem :: MUSIC_S1:105

    

     Th86: (( spiral_of_fifths (HPS,frequency,( Fourth (HPS,frequency)))) . 5) = ((81 qua Real / 64) * ( @ frequency))

    proof

      set MS = HPS;

      set q = ( Fourth (MS,frequency));

      reconsider n3 = 4 as Nat;

      (( spiral_of_fifths (MS,frequency,q)) . n3) is Element of MS;

      then

      reconsider r32 = ((27 qua Real / 16) * ( @ frequency)) as Element of MS by Th85;

      

       A1: (( spiral_of_fifths (MS,frequency,q)) . 5) = (( spiral_of_fifths (MS,frequency,q)) . (n3 + 1))

      .= ( Fifth_reduct (MS,frequency,(( spiral_of_fifths (MS,frequency,q)) . n3))) by Def19

      .= ( Fifth_reduct (MS,frequency,r32)) by Th85;

      consider r,s be positive Real such that

       A2: r = r32 & s = ((3 qua Real / 2) * r) & ( Fifth (MS,r32)) = s by Th54;

      

       A3: ex fr be positive Real st frequency = fr & ( Octave (MS,frequency)) = (2 * fr) by Def15;

      

       A4: not ( @ frequency) <= ((81 qua Real / 32) * ( @ frequency)) <= (2 * ( @ frequency)) by XREAL_1: 68;

      

       A5: ex r be positive Real st ( Fifth (MS,r32)) = r & ( Octave_descendent (MS,( Fifth (MS,r32)))) = (r / 2) by Th51;

       not ( Fifth (MS,r32)) is_Between (frequency,( Octave (MS,frequency))) by A4, A2, A3;

      hence thesis by A1, A2, A5, Def18;

    end;

    theorem :: MUSIC_S1:106

    

     Th87: (( spiral_of_fifths (HPS,frequency,( Fourth (HPS,frequency)))) . 6) = ((243 qua Real / 128) * ( @ frequency))

    proof

      set MS = HPS;

      reconsider n4 = 5 as Nat;

      set q = ( Fourth (MS,frequency));

      (( spiral_of_fifths (MS,frequency,q)) . n4) is Element of MS;

      then

      reconsider r32 = ((81 qua Real / 64) * ( @ frequency)) as Element of MS by Th86;

      

       A1: (( spiral_of_fifths (MS,frequency,q)) . 6) = (( spiral_of_fifths (MS,frequency,q)) . (n4 + 1))

      .= ( Fifth_reduct (MS,frequency,(( spiral_of_fifths (MS,frequency,q)) . n4))) by Def19

      .= ( Fifth_reduct (MS,frequency,r32)) by Th86;

      consider r,s be positive Real such that

       A2: r = r32 & s = ((3 qua Real / 2) * r) & ( Fifth (MS,r32)) = s by Th54;

      

       A3: ex fr be positive Real st frequency = fr & ( Octave (MS,frequency)) = (2 * fr) by Def15;

      ((243 qua Real / 128) * ( @ frequency)) < (2 * ( @ frequency)) & (1 * ( @ frequency)) < ((243 qua Real / 128) * ( @ frequency)) by XREAL_1: 68;

      then ( Fifth (MS,r32)) is_Between (frequency,( Octave (MS,frequency))) by A2, A3;

      hence thesis by A2, A1, Def18;

    end;

    theorem :: MUSIC_S1:107

    

     Th88: (( heptatonic_pythagorean_scale (HPS,frequency)) . 1) = (1 * ( @ frequency)) & (( heptatonic_pythagorean_scale (HPS,frequency)) . 2) = ((9 qua Real / 8) * ( @ frequency)) & (( heptatonic_pythagorean_scale (HPS,frequency)) . 3) = ((81 qua Real / 64) * ( @ frequency)) & (( heptatonic_pythagorean_scale (HPS,frequency)) . 4) = ((4 qua Real / 3) * ( @ frequency)) & (( heptatonic_pythagorean_scale (HPS,frequency)) . 5) = ((3 qua Real / 2) * ( @ frequency)) & (( heptatonic_pythagorean_scale (HPS,frequency)) . 6) = ((27 qua Real / 16) * ( @ frequency)) & (( heptatonic_pythagorean_scale (HPS,frequency)) . 7) = ((243 qua Real / 128) * ( @ frequency)) & (( heptatonic_pythagorean_scale (HPS,frequency)) . 8) = (2 * ( @ frequency))

    proof

      set MS = HPS;

      set gamme = ( heptatonic_pythagorean_scale (MS,frequency));

      

       A1: (gamme . 1) = (( spiral_of_fifths (MS,frequency,( Fourth (MS,frequency)))) . 1) & (gamme . 2) = (( spiral_of_fifths (MS,frequency,( Fourth (MS,frequency)))) . 3) & (gamme . 3) = (( spiral_of_fifths (MS,frequency,( Fourth (MS,frequency)))) . 5) & (gamme . 4) = ( Fourth (MS,frequency)) & (gamme . 5) = (( spiral_of_fifths (MS,frequency,( Fourth (MS,frequency)))) . 2) & (gamme . 6) = (( spiral_of_fifths (MS,frequency,( Fourth (MS,frequency)))) . 4) & (gamme . 7) = (( spiral_of_fifths (MS,frequency,( Fourth (MS,frequency)))) . 6) & (gamme . 8) = ( Octave (MS,(( spiral_of_fifths (MS,frequency,( Fourth (MS,frequency)))) . 1))) by Def26;

      gamme in (8 -tuples_on the carrier of MS);

      then gamme in { s where s be Element of (the carrier of MS * ) : ( len s) = 8 } by FINSEQ_2:def 4;

      then

      consider s be Element of (the carrier of MS * ) such that

       A2: s = gamme and

       A3: ( len s) = 8;

      ( dom s) = ( Seg 8) by A3, FINSEQ_1:def 3;

      then

      reconsider g1 = (gamme . 4), g2 = (gamme . 1), g3 = (gamme . 5), g4 = (gamme . 2), g5 = (gamme . 6), g6 = (gamme . 3), g7 = (gamme . 7), g8 = (gamme . 8) as Element of the carrier of MS by A2, FINSEQ_1: 1, FINSEQ_2: 11;

      reconsider frequency2 = g1 as Element of MS;

      reconsider r1 = ( @ frequency2), r2 = ( @ g2), r3 = ( @ g3), r4 = ( @ g4), r5 = ( @ g5), r6 = ( @ g6), r7 = ( @ g7), r8 = ( @ g8) as positive Real;

      

       A4: ex fr be positive Real st frequency = fr & ( Octave (MS,frequency)) = (2 * fr) by Def15;

      

       A5: r8 = ( Octave (MS,(( spiral_of_fifths (MS,frequency,( Fourth (MS,frequency)))) . 1))) by Def26

      .= (2 * ( @ frequency)) by A4, Th82;

      ex fr be positive Real st frequency = fr & ( Fourth (MS,frequency)) = ((4 qua Real / 3) * fr) by Def24;

      hence thesis by A5, A1, Th82, Th84, Th86, Th83, Th85, Th87;

    end;

    theorem :: MUSIC_S1:108

    

     Th88BIS: ( heptatonic_pythagorean_scale (HPS,frequency)) is heptatonic

    proof

      set MS = HPS;

      set gamme = ( heptatonic_pythagorean_scale (MS,frequency));

      now

        now

          reconsider r1 = (1 * ( @ frequency)), r2 = ((9 qua Real / 8) * ( @ frequency)), r3 = ((81 qua Real / 64) * ( @ frequency)), r4 = ((4 qua Real / 3) * ( @ frequency)), r5 = ((3 qua Real / 2) * ( @ frequency)), r6 = ((27 qua Real / 16) * ( @ frequency)), r7 = ((243 qua Real / 128) * ( @ frequency)), r8 = (2 * ( @ frequency)) as positive Real;

          take r1, r2, r3, r4, r5, r6, r7, r8;

          (( heptatonic_pythagorean_scale (MS,frequency)) . 1) = (1 * ( @ frequency)) & (( heptatonic_pythagorean_scale (MS,frequency)) . 2) = ((9 qua Real / 8) * ( @ frequency)) & (( heptatonic_pythagorean_scale (MS,frequency)) . 3) = ((81 qua Real / 64) * ( @ frequency)) & (( heptatonic_pythagorean_scale (MS,frequency)) . 4) = ((4 qua Real / 3) * ( @ frequency)) & (( heptatonic_pythagorean_scale (MS,frequency)) . 5) = ((3 qua Real / 2) * ( @ frequency)) & (( heptatonic_pythagorean_scale (MS,frequency)) . 6) = ((27 qua Real / 16) * ( @ frequency)) & (( heptatonic_pythagorean_scale (MS,frequency)) . 7) = ((243 qua Real / 128) * ( @ frequency)) & (( heptatonic_pythagorean_scale (MS,frequency)) . 8) = (2 * ( @ frequency)) by Th88;

          hence (gamme . 1) = frequency & (gamme . 1) = r1 & (gamme . 2) = r2 & (gamme . 3) = r3 & (gamme . 4) = r4 & (gamme . 5) = r5 & (gamme . 6) = r6 & (gamme . 7) = r7 & (gamme . 8) = r8;

          thus r1 < r2 & r2 < r3 & r3 < r4 & r4 < r5 & r5 < r6 & r6 < r7 & r7 < r8 by XREAL_1: 98;

        end;

        hence ex frequency be Element of MS, r1,r2,r3,r4,r5,r6,r7,r8 be positive Real st (gamme . 1) = r1 & (gamme . 2) = r2 & (gamme . 3) = r3 & (gamme . 4) = r4 & (gamme . 5) = r5 & (gamme . 6) = r6 & (gamme . 7) = r7 & (gamme . 8) = r8 & r1 < r2 < r3 & r3 < r4 < r5 & r5 < r6 & r6 < r7 & r7 < r8;

        

         A1: ex fr be positive Real st frequency = fr & ( Octave (MS,frequency)) = (2 * fr) by Def15;

        (( heptatonic_pythagorean_scale (MS,frequency)) . 1) = (1 * ( @ frequency)) & (( heptatonic_pythagorean_scale (MS,frequency)) . 2) = ((9 qua Real / 8) * ( @ frequency)) & (( heptatonic_pythagorean_scale (MS,frequency)) . 3) = ((81 qua Real / 64) * ( @ frequency)) & (( heptatonic_pythagorean_scale (MS,frequency)) . 4) = ((4 qua Real / 3) * ( @ frequency)) & (( heptatonic_pythagorean_scale (MS,frequency)) . 5) = ((3 qua Real / 2) * ( @ frequency)) & (( heptatonic_pythagorean_scale (MS,frequency)) . 6) = ((27 qua Real / 16) * ( @ frequency)) & (( heptatonic_pythagorean_scale (MS,frequency)) . 7) = ((243 qua Real / 128) * ( @ frequency)) & (( heptatonic_pythagorean_scale (MS,frequency)) . 8) = (2 * ( @ frequency)) by Th88;

        hence (gamme . 8) = ( Octave (MS,frequency)) & (gamme . 1) = frequency by A1;

      end;

      hence thesis;

    end;

    definition

      :: MUSIC_S1:def80

      func heptatonic_pythagorean_semitone -> positive Real equals (256 qua Real / 243);

      coherence ;

    end

    notation

      synonym limma_pythagoricien for heptatonic_pythagorean_semitone ;

    end

    notation

      synonym diatonic_tone for pythagorean_tone ;

    end

    theorem :: MUSIC_S1:109

    ( pythagorean_tone / 2) < heptatonic_pythagorean_semitone ;

    theorem :: MUSIC_S1:110

    (((((( pythagorean_tone * pythagorean_tone ) * heptatonic_pythagorean_semitone ) * pythagorean_tone ) * pythagorean_tone ) * pythagorean_tone ) * heptatonic_pythagorean_semitone ) = 2;

    definition

      let HPS be Heptatonic_Pythagorean_Score;

      let frequency be Element of HPS;

      :: MUSIC_S1:def81

      func hepta_fondamental (HPS,frequency) -> Element of HPS equals (( heptatonic_pythagorean_scale (HPS,frequency)) . 1);

      coherence

      proof

        (( heptatonic_pythagorean_scale (HPS,frequency)) . 1) = (( spiral_of_fifths (HPS,frequency,( Fourth (HPS,frequency)))) . 1) by Def26;

        hence thesis;

      end;

      :: MUSIC_S1:def82

      func hepta_1 (HPS,frequency) -> Element of HPS equals (( heptatonic_pythagorean_scale (HPS,frequency)) . 2);

      coherence

      proof

        (( heptatonic_pythagorean_scale (HPS,frequency)) . 2) = (( spiral_of_fifths (HPS,frequency,( Fourth (HPS,frequency)))) . 3) by Def26;

        hence thesis;

      end;

      :: MUSIC_S1:def83

      func hepta_2 (HPS,frequency) -> Element of HPS equals (( heptatonic_pythagorean_scale (HPS,frequency)) . 3);

      coherence

      proof

        (( heptatonic_pythagorean_scale (HPS,frequency)) . 3) = (( spiral_of_fifths (HPS,frequency,( Fourth (HPS,frequency)))) . 5) by Def26;

        hence thesis;

      end;

      :: MUSIC_S1:def84

      func hepta_3 (HPS,frequency) -> Element of HPS equals (( heptatonic_pythagorean_scale (HPS,frequency)) . 4);

      coherence

      proof

        (( heptatonic_pythagorean_scale (HPS,frequency)) . 4) = ( Fourth (HPS,frequency)) by Def26;

        hence thesis;

      end;

      :: MUSIC_S1:def85

      func hepta_4 (HPS,frequency) -> Element of HPS equals (( heptatonic_pythagorean_scale (HPS,frequency)) . 5);

      coherence

      proof

        (( heptatonic_pythagorean_scale (HPS,frequency)) . 5) = (( spiral_of_fifths (HPS,frequency,( Fourth (HPS,frequency)))) . 2) by Def26;

        hence thesis;

      end;

      :: MUSIC_S1:def86

      func hepta_5 (HPS,frequency) -> Element of HPS equals (( heptatonic_pythagorean_scale (HPS,frequency)) . 6);

      coherence

      proof

        (( heptatonic_pythagorean_scale (HPS,frequency)) . 6) = (( spiral_of_fifths (HPS,frequency,( Fourth (HPS,frequency)))) . 4) by Def26;

        hence thesis;

      end;

      :: MUSIC_S1:def87

      func hepta_6 (HPS,frequency) -> Element of HPS equals (( heptatonic_pythagorean_scale (HPS,frequency)) . 7);

      coherence

      proof

        (( heptatonic_pythagorean_scale (HPS,frequency)) . 7) = (( spiral_of_fifths (HPS,frequency,( Fourth (HPS,frequency)))) . 6) by Def26;

        hence thesis;

      end;

      :: MUSIC_S1:def88

      func hepta_octave (HPS,frequency) -> Element of HPS equals ( Octave (HPS,frequency));

      coherence ;

    end

    

     Lem89: for r1,r2,r3,r4,r5,r6,r7,r8 be positive Real st (( heptatonic_pythagorean_scale (HPS,frequency)) . 1) = r1 & (( heptatonic_pythagorean_scale (HPS,frequency)) . 2) = r2 & (( heptatonic_pythagorean_scale (HPS,frequency)) . 3) = r3 & (( heptatonic_pythagorean_scale (HPS,frequency)) . 4) = r4 & (( heptatonic_pythagorean_scale (HPS,frequency)) . 5) = r5 & (( heptatonic_pythagorean_scale (HPS,frequency)) . 6) = r6 & (( heptatonic_pythagorean_scale (HPS,frequency)) . 7) = r7 & (( heptatonic_pythagorean_scale (HPS,frequency)) . 8) = r8 holds (r2 / r1) = (9 qua Real / 8) & (r3 / r2) = (9 qua Real / 8) & (r4 / r3) = (256 qua Real / 243) & (r5 / r4) = (9 qua Real / 8) & (r6 / r5) = (9 qua Real / 8) & (r7 / r6) = (9 qua Real / 8) & (r8 / r7) = (256 qua Real / 243)

    proof

      set MS = HPS;

      let r1,r2,r3,r4,r5,r6,r7,r8 be positive Real;

      assume (( heptatonic_pythagorean_scale (MS,frequency)) . 1) = r1 & (( heptatonic_pythagorean_scale (MS,frequency)) . 2) = r2 & (( heptatonic_pythagorean_scale (MS,frequency)) . 3) = r3 & (( heptatonic_pythagorean_scale (MS,frequency)) . 4) = r4 & (( heptatonic_pythagorean_scale (MS,frequency)) . 5) = r5 & (( heptatonic_pythagorean_scale (MS,frequency)) . 6) = r6 & (( heptatonic_pythagorean_scale (MS,frequency)) . 7) = r7 & (( heptatonic_pythagorean_scale (MS,frequency)) . 8) = r8;

      then r1 = (1 * ( @ frequency)) & r2 = ((9 qua Real / 8) * ( @ frequency)) & r3 = ((81 qua Real / 64) * ( @ frequency)) & r4 = ((4 qua Real / 3) * ( @ frequency)) & r5 = ((3 qua Real / 2) * ( @ frequency)) & r6 = ((27 qua Real / 16) * ( @ frequency)) & r7 = ((243 qua Real / 128) * ( @ frequency)) & r8 = (2 * ( @ frequency)) by Th88;

      then (r2 / r1) = (((9 qua Real / 8) * ( @ frequency)) / (1 * ( @ frequency))) & (r3 / r2) = ((81 qua Real / 64) / (9 qua Real / 8)) & (r4 / r3) = ((4 qua Real / 3) / (81 qua Real / 64)) & (r5 / r4) = ((3 qua Real / 2) / (4 qua Real / 3)) & (r6 / r5) = ((27 qua Real / 16) / (3 qua Real / 2)) & (r7 / r6) = ((243 qua Real / 128) / (27 qua Real / 16)) & (r8 / r7) = (2 qua Real / (243 qua Real / 128)) by XCMPLX_1: 91;

      hence thesis by XCMPLX_1: 89;

    end;

    

     Lem90: ex r1,r2,r3,r4,r5,r6,r7,r8 be positive Real st (( heptatonic_pythagorean_scale (HPS,frequency)) . 1) = r1 & (( heptatonic_pythagorean_scale (HPS,frequency)) . 2) = r2 & (( heptatonic_pythagorean_scale (HPS,frequency)) . 3) = r3 & (( heptatonic_pythagorean_scale (HPS,frequency)) . 4) = r4 & (( heptatonic_pythagorean_scale (HPS,frequency)) . 5) = r5 & (( heptatonic_pythagorean_scale (HPS,frequency)) . 6) = r6 & (( heptatonic_pythagorean_scale (HPS,frequency)) . 7) = r7 & (( heptatonic_pythagorean_scale (HPS,frequency)) . 8) = r8 & (r2 / r1) = (9 qua Real / 8) & (r3 / r2) = (9 qua Real / 8) & (r4 / r3) = (256 qua Real / 243) & (r5 / r4) = (9 qua Real / 8) & (r6 / r5) = (9 qua Real / 8) & (r7 / r6) = (9 qua Real / 8) & (r8 / r7) = (256 qua Real / 243)

    proof

      set MS = HPS;

      set r1 = ( hepta_fondamental (MS,frequency)), r2 = ( hepta_1 (MS,frequency)), r3 = ( hepta_2 (MS,frequency)), r4 = ( hepta_3 (MS,frequency)), r5 = ( hepta_4 (MS,frequency)), r6 = ( hepta_5 (MS,frequency)), r7 = ( hepta_6 (MS,frequency)), r8 = ( hepta_octave (MS,frequency));

      the carrier of MS c= REALPLUS by Def07a;

      then

      reconsider r91 = r1, r92 = r2, r93 = r3, r94 = r4, r95 = r5, r96 = r6, r97 = r7, r98 = r8 as positive Real by Th1;

      take r91, r92, r93, r94, r95, r96, r97;

      

       A1: ex fr be positive Real st frequency = fr & ( Octave (MS,frequency)) = (2 * fr) by Def15;

      

       A2: (( heptatonic_pythagorean_scale (MS,frequency)) . 1) = (1 * ( @ frequency)) & (( heptatonic_pythagorean_scale (MS,frequency)) . 2) = ((9 qua Real / 8) * ( @ frequency)) & (( heptatonic_pythagorean_scale (MS,frequency)) . 3) = ((81 qua Real / 64) * ( @ frequency)) & (( heptatonic_pythagorean_scale (MS,frequency)) . 4) = ((4 qua Real / 3) * ( @ frequency)) & (( heptatonic_pythagorean_scale (MS,frequency)) . 5) = ((3 qua Real / 2) * ( @ frequency)) & (( heptatonic_pythagorean_scale (MS,frequency)) . 6) = ((27 qua Real / 16) * ( @ frequency)) & (( heptatonic_pythagorean_scale (MS,frequency)) . 7) = ((243 qua Real / 128) * ( @ frequency)) & (( heptatonic_pythagorean_scale (MS,frequency)) . 8) = (2 * ( @ frequency)) by Th88;

      r1 = (1 * ( @ frequency)) & r2 = ((9 qua Real / 8) * ( @ frequency)) & r3 = ((81 qua Real / 64) * ( @ frequency)) & r4 = ((4 qua Real / 3) * ( @ frequency)) & r5 = ((3 qua Real / 2) * ( @ frequency)) & r6 = ((27 qua Real / 16) * ( @ frequency)) & r7 = ((243 qua Real / 128) * ( @ frequency)) & r8 = (2 * ( @ frequency)) by Th88, A1;

      then (( heptatonic_pythagorean_scale (MS,frequency)) . 1) = r91 & (( heptatonic_pythagorean_scale (MS,frequency)) . 2) = r92 & (( heptatonic_pythagorean_scale (MS,frequency)) . 3) = r93 & (( heptatonic_pythagorean_scale (MS,frequency)) . 4) = r94 & (( heptatonic_pythagorean_scale (MS,frequency)) . 5) = r95 & (( heptatonic_pythagorean_scale (MS,frequency)) . 6) = r96 & (( heptatonic_pythagorean_scale (MS,frequency)) . 7) = r97 & (( heptatonic_pythagorean_scale (MS,frequency)) . 8) = r98 by Th88;

      then (r92 / r91) = (9 qua Real / 8) & (r93 / r92) = (9 qua Real / 8) & (r94 / r93) = (256 qua Real / 243) & (r95 / r94) = (9 qua Real / 8) & (r96 / r95) = (9 qua Real / 8) & (r97 / r96) = (9 qua Real / 8) & (r98 / r97) = (256 qua Real / 243) by Lem89;

      hence thesis by A1, A2;

    end;

    theorem :: MUSIC_S1:111

    

     Th90: ( intrval (( hepta_fondamental (HPS,frequency)),( hepta_1 (HPS,frequency)))) = pythagorean_tone & ( intrval (( hepta_1 (HPS,frequency)),( hepta_2 (HPS,frequency)))) = pythagorean_tone & ( intrval (( hepta_2 (HPS,frequency)),( hepta_3 (HPS,frequency)))) = heptatonic_pythagorean_semitone & ( intrval (( hepta_3 (HPS,frequency)),( hepta_4 (HPS,frequency)))) = pythagorean_tone & ( intrval (( hepta_4 (HPS,frequency)),( hepta_5 (HPS,frequency)))) = pythagorean_tone & ( intrval (( hepta_5 (HPS,frequency)),( hepta_6 (HPS,frequency)))) = pythagorean_tone & ( intrval (( hepta_6 (HPS,frequency)),( hepta_octave (HPS,frequency)))) = heptatonic_pythagorean_semitone

    proof

      set MS = HPS;

      

       A1: ex fr be positive Real st frequency = fr & ( Octave (MS,frequency)) = (2 * fr) by Def15;

      

       A2: (( heptatonic_pythagorean_scale (MS,frequency)) . 8) = (2 * ( @ frequency)) by Th88;

      ex r1,r2,r3,r4,r5,r6,r7,r8 be positive Real st (( heptatonic_pythagorean_scale (MS,frequency)) . 1) = r1 & (( heptatonic_pythagorean_scale (MS,frequency)) . 2) = r2 & (( heptatonic_pythagorean_scale (MS,frequency)) . 3) = r3 & (( heptatonic_pythagorean_scale (MS,frequency)) . 4) = r4 & (( heptatonic_pythagorean_scale (MS,frequency)) . 5) = r5 & (( heptatonic_pythagorean_scale (MS,frequency)) . 6) = r6 & (( heptatonic_pythagorean_scale (MS,frequency)) . 7) = r7 & (( heptatonic_pythagorean_scale (MS,frequency)) . 8) = r8 & (r2 / r1) = (9 qua Real / 8) & (r3 / r2) = (9 qua Real / 8) & (r4 / r3) = (256 qua Real / 243) & (r5 / r4) = (9 qua Real / 8) & (r6 / r5) = (9 qua Real / 8) & (r7 / r6) = (9 qua Real / 8) & (r8 / r7) = (256 qua Real / 243) by Lem90;

      hence thesis by A1, A2, Def21;

    end;

    reserve HPS for Heptatonic_Pythagorean_Score,

frequency for Element of HPS;

    definition

      let MS be MusicSpace;

      let n be natural Number;

      let scale be Element of (n -tuples_on the carrier of MS);

      assume scale is heptatonic;

      :: MUSIC_S1:def89

      attr scale is perfect_fifth means

      : Def27: [(scale . 1), (scale . 5)] in ( fifth MS) & [(scale . 2), (scale . 6)] in ( fifth MS) & [(scale . 3), (scale . 7)] in ( fifth MS) & [(scale . 4), (scale . 8)] in ( fifth MS);

    end

    theorem :: MUSIC_S1:112

    for HPS be satisfying_euclidean Heptatonic_Pythagorean_Score holds for frequency be Element of HPS holds ( heptatonic_pythagorean_scale (HPS,frequency)) is perfect_fifth

    proof

      let HPS be satisfying_euclidean Heptatonic_Pythagorean_Score;

      let frequency be Element of HPS;

      

       A1: ( heptatonic_pythagorean_scale (HPS,frequency)) is heptatonic by Th88BIS;

      set gamme = ( heptatonic_pythagorean_scale (HPS,frequency));

      

       A2: ( hepta_fondamental (HPS,frequency)) = (1 * ( @ frequency)) & ( hepta_1 (HPS,frequency)) = ((9 qua Real / 8) * ( @ frequency)) & ( hepta_2 (HPS,frequency)) = ((81 qua Real / 64) * ( @ frequency)) & ( hepta_3 (HPS,frequency)) = ((4 qua Real / 3) * ( @ frequency)) & ( hepta_4 (HPS,frequency)) = ((3 qua Real / 2) * ( @ frequency)) & ( hepta_5 (HPS,frequency)) = ((27 qua Real / 16) * ( @ frequency)) & ( hepta_6 (HPS,frequency)) = ((243 qua Real / 128) * ( @ frequency)) by Th88;

      

       A3: ex fo be positive Real st frequency = fo & ( Octave (HPS,frequency)) = (2 * fo) by Def15;

      then ( hepta_octave (HPS,frequency)) = (2 * ( @ frequency));

      then

       A4: ( hepta_octave (HPS,frequency)) = (gamme . 8) by Th88;

      

       A5: (the Ratio of HPS . (( hepta_fondamental (HPS,frequency)),( hepta_4 (HPS,frequency)))) = (( @ ( hepta_4 (HPS,frequency))) / ( @ ( hepta_fondamental (HPS,frequency)))) by Def25

      .= (3 qua Real / 2) by A2, XCMPLX_1: 89;

      

       A6: (the Ratio of HPS . (( hepta_1 (HPS,frequency)),( hepta_5 (HPS,frequency)))) = (( @ ( hepta_5 (HPS,frequency))) / ( @ ( hepta_1 (HPS,frequency)))) by Def25

      .= (((27 qua Real / 16) / (9 qua Real / 8)) * (( @ frequency) / ( @ frequency))) by A2, XCMPLX_1: 76

      .= (3 qua Real / 2) by XCMPLX_1: 88;

      

       A7: (the Ratio of HPS . (( hepta_2 (HPS,frequency)),( hepta_6 (HPS,frequency)))) = (( @ ( hepta_6 (HPS,frequency))) / ( @ ( hepta_2 (HPS,frequency)))) by Def25

      .= (((243 qua Real / 128) / (81 qua Real / 64)) * (( @ frequency) / ( @ frequency))) by A2, XCMPLX_1: 76

      .= (3 qua Real / 2) by XCMPLX_1: 88;

      

       A8: (the Ratio of HPS . (( hepta_3 (HPS,frequency)),( hepta_octave (HPS,frequency)))) = (( @ ( hepta_octave (HPS,frequency))) / ( @ ( hepta_3 (HPS,frequency)))) by Def25

      .= ((2 qua Real * ( @ frequency)) / ((4 qua Real / 3) * ( @ frequency))) by Th88, A3

      .= ((2 qua Real / (4 qua Real / 3)) * (( @ frequency) / ( @ frequency))) by XCMPLX_1: 76

      .= (3 qua Real / 2) by XCMPLX_1: 88;

      reconsider n2 = 2, n3 = 3 as Element of HPS by Th20;

      (the Ratio of HPS . (n2,n3)) = (( @ n3) / ( @ n2)) by Def25

      .= (3 qua Real / 2);

      then (n2,n3) equiv (( hepta_fondamental (HPS,frequency)),( hepta_4 (HPS,frequency))) & (n2,n3) equiv (( hepta_1 (HPS,frequency)),( hepta_5 (HPS,frequency))) & (n2,n3) equiv (( hepta_2 (HPS,frequency)),( hepta_6 (HPS,frequency))) & (n2,n3) equiv (( hepta_3 (HPS,frequency)),( hepta_octave (HPS,frequency))) by A5, A6, A7, A8, Def08a;

      then [( hepta_fondamental (HPS,frequency)), ( hepta_4 (HPS,frequency))] in ( fifth HPS) & [( hepta_1 (HPS,frequency)), ( hepta_5 (HPS,frequency))] in ( fifth HPS) & [( hepta_2 (HPS,frequency)), ( hepta_6 (HPS,frequency))] in ( fifth HPS) & [( hepta_3 (HPS,frequency)), ( hepta_octave (HPS,frequency))] in ( fifth HPS) by EQREL_1: 18;

      hence thesis by A4, A1, Def27;

    end;

    definition

      let HPS be Heptatonic_Pythagorean_Score;

      let frequency be Element of HPS;

      :: MUSIC_S1:def90

      func heptatonic_pythagorean_scale_ascending (HPS,frequency) -> Element of (8 -tuples_on the carrier of HPS) equals ( heptatonic_pythagorean_scale (HPS,( Octave (HPS,frequency))));

      coherence ;

    end

    theorem :: MUSIC_S1:113

    

     Th91: (( heptatonic_pythagorean_scale_ascending (HPS,frequency)) . 1) = (2 * ( @ frequency)) & (( heptatonic_pythagorean_scale_ascending (HPS,frequency)) . 2) = ((9 qua Real / 4) * ( @ frequency)) & (( heptatonic_pythagorean_scale_ascending (HPS,frequency)) . 3) = ((81 qua Real / 32) * ( @ frequency)) & (( heptatonic_pythagorean_scale_ascending (HPS,frequency)) . 4) = ((8 qua Real / 3) * ( @ frequency)) & (( heptatonic_pythagorean_scale_ascending (HPS,frequency)) . 5) = (3 qua Real * ( @ frequency)) & (( heptatonic_pythagorean_scale_ascending (HPS,frequency)) . 6) = ((27 qua Real / 8) * ( @ frequency)) & (( heptatonic_pythagorean_scale_ascending (HPS,frequency)) . 7) = ((243 qua Real / 64) * ( @ frequency)) & (( heptatonic_pythagorean_scale_ascending (HPS,frequency)) . 8) = (4 * ( @ frequency))

    proof

      set f2 = ( Octave (HPS,frequency));

      consider fr be positive Real such that

       A1: frequency = fr & ( Octave (HPS,frequency)) = (2 * fr) by Def15;

      (( heptatonic_pythagorean_scale (HPS,f2)) . 1) = (1 * ( @ f2)) & (( heptatonic_pythagorean_scale (HPS,f2)) . 2) = ((9 qua Real / 8) * ( @ f2)) & (( heptatonic_pythagorean_scale (HPS,f2)) . 3) = ((81 qua Real / 64) * ( @ f2)) & (( heptatonic_pythagorean_scale (HPS,f2)) . 4) = ((4 qua Real / 3) * ( @ f2)) & (( heptatonic_pythagorean_scale (HPS,f2)) . 5) = ((3 qua Real / 2) * ( @ f2)) & (( heptatonic_pythagorean_scale (HPS,f2)) . 6) = ((27 qua Real / 16) * ( @ f2)) & (( heptatonic_pythagorean_scale (HPS,f2)) . 7) = ((243 qua Real / 128) * ( @ f2)) & (( heptatonic_pythagorean_scale (HPS,f2)) . 8) = (2 * ( @ f2)) by Th88;

      hence thesis by A1;

    end;

    theorem :: MUSIC_S1:114

    (( heptatonic_pythagorean_scale (HPS,frequency)) . 8) = (( heptatonic_pythagorean_scale_ascending (HPS,frequency)) . 1)

    proof

      (( heptatonic_pythagorean_scale (HPS,frequency)) . 8) = (2 * ( @ frequency)) & (( heptatonic_pythagorean_scale_ascending (HPS,frequency)) . 1) = (2 * ( @ frequency)) by Th88, Th91;

      hence thesis;

    end;

    theorem :: MUSIC_S1:115

    

     Th92: ( intrval (( hepta_4 (HPS,frequency)),( hepta_1 (HPS,( Octave (HPS,frequency)))))) = (3 qua Real / 2) & ( intrval (( hepta_5 (HPS,frequency)),( hepta_2 (HPS,( Octave (HPS,frequency)))))) = (3 qua Real / 2) & ( intrval (( hepta_6 (HPS,frequency)),( hepta_3 (HPS,( Octave (HPS,frequency)))))) <> (3 qua Real / 2) & ( intrval (( hepta_octave (HPS,frequency)),( hepta_4 (HPS,( Octave (HPS,frequency)))))) = (3 qua Real / 2)

    proof

      set gamme = ( heptatonic_pythagorean_scale (HPS,frequency));

      

       A1: ( hepta_fondamental (HPS,frequency)) = (1 * ( @ frequency)) & ( hepta_1 (HPS,frequency)) = ((9 qua Real / 8) * ( @ frequency)) & ( hepta_2 (HPS,frequency)) = ((81 qua Real / 64) * ( @ frequency)) & ( hepta_3 (HPS,frequency)) = ((4 qua Real / 3) * ( @ frequency)) & ( hepta_4 (HPS,frequency)) = ((3 qua Real / 2) * ( @ frequency)) & ( hepta_5 (HPS,frequency)) = ((27 qua Real / 16) * ( @ frequency)) & ( hepta_6 (HPS,frequency)) = ((243 qua Real / 128) * ( @ frequency)) by Th88;

      set f2 = ( Octave (HPS,frequency));

      set gamme2 = ( heptatonic_pythagorean_scale (HPS,f2));

      

       A2: (( heptatonic_pythagorean_scale_ascending (HPS,frequency)) . 1) = (2 * ( @ frequency)) & (( heptatonic_pythagorean_scale_ascending (HPS,frequency)) . 2) = ((9 qua Real / 4) * ( @ frequency)) & (( heptatonic_pythagorean_scale_ascending (HPS,frequency)) . 3) = ((81 qua Real / 32) * ( @ frequency)) & (( heptatonic_pythagorean_scale_ascending (HPS,frequency)) . 4) = ((8 qua Real / 3) * ( @ frequency)) & (( heptatonic_pythagorean_scale_ascending (HPS,frequency)) . 5) = (3 qua Real * ( @ frequency)) & (( heptatonic_pythagorean_scale_ascending (HPS,frequency)) . 6) = ((27 qua Real / 8) * ( @ frequency)) & (( heptatonic_pythagorean_scale_ascending (HPS,frequency)) . 7) = ((243 qua Real / 64) * ( @ frequency)) & (( heptatonic_pythagorean_scale_ascending (HPS,frequency)) . 8) = (4 * ( @ frequency)) by Th91;

      

       A3: ex fo be positive Real st frequency = fo & ( Octave (HPS,frequency)) = (2 * fo) by Def15;

      now

        

        thus ( intrval (( hepta_4 (HPS,frequency)),( hepta_1 (HPS,( Octave (HPS,frequency)))))) = (((9 qua Real / 4) * ( @ frequency)) / ((3 qua Real / 2) * ( @ frequency))) by A2, A1, Def21

        .= ((((9 qua Real / 4) / (3 qua Real / 2)) * ( @ frequency)) / ( @ frequency)) by XCMPLX_1: 83

        .= (3 qua Real / 2) by XCMPLX_1: 89;

        

        thus ( intrval (( hepta_5 (HPS,frequency)),( hepta_2 (HPS,( Octave (HPS,frequency)))))) = (((81 qua Real / 32) * ( @ frequency)) / ((27 qua Real / 16) * ( @ frequency))) by A2, A1, Def21

        .= ((((81 qua Real / 32) / (27 qua Real / 16)) * ( @ frequency)) / ( @ frequency)) by XCMPLX_1: 83

        .= (3 qua Real / 2) by XCMPLX_1: 89;

        ( intrval (( hepta_6 (HPS,frequency)),( hepta_3 (HPS,( Octave (HPS,frequency)))))) = (((8 qua Real / 3) * ( @ frequency)) / ((243 qua Real / 128) * ( @ frequency))) by A2, A1, Def21

        .= ((((8 qua Real / 3) / (243 qua Real / 128)) * ( @ frequency)) / ( @ frequency)) by XCMPLX_1: 83;

        hence ( intrval (( hepta_6 (HPS,frequency)),( hepta_3 (HPS,( Octave (HPS,frequency)))))) <> (3 qua Real / 2) by XCMPLX_1: 89;

        

        thus ( intrval (( hepta_octave (HPS,frequency)),( hepta_4 (HPS,( Octave (HPS,frequency)))))) = ((3 qua Real * ( @ frequency)) / (2 * ( @ frequency))) by A3, A2, Def21

        .= (((3 qua Real / 2) * ( @ frequency)) / ( @ frequency)) by XCMPLX_1: 83

        .= (3 qua Real / 2) by XCMPLX_1: 89;

      end;

      hence thesis;

    end;

    theorem :: MUSIC_S1:116

    

     Th93: for HPS be satisfying_euclidean Heptatonic_Pythagorean_Score holds for f1,f2 be Element of HPS holds ( intrval (f1,f2)) = (the Ratio of HPS . (f1,f2))

    proof

      let HPS be satisfying_euclidean Heptatonic_Pythagorean_Score;

      let f1,f2 be Element of HPS;

      (the Ratio of HPS . (f1,f2)) = (( @ f2) / ( @ f1)) by Def25;

      hence thesis by Def21;

    end;

    theorem :: MUSIC_S1:117

    for HPS be satisfying_euclidean Heptatonic_Pythagorean_Score holds for frequency be Element of HPS holds [(( heptatonic_pythagorean_scale (HPS,frequency)) . 5), (( heptatonic_pythagorean_scale_ascending (HPS,frequency)) . 2)] in ( fifth HPS) & [(( heptatonic_pythagorean_scale (HPS,frequency)) . 6), (( heptatonic_pythagorean_scale_ascending (HPS,frequency)) . 3)] in ( fifth HPS) & not [(( heptatonic_pythagorean_scale (HPS,frequency)) . 7), (( heptatonic_pythagorean_scale_ascending (HPS,frequency)) . 4)] in ( fifth HPS)

    proof

      let HPS be satisfying_euclidean Heptatonic_Pythagorean_Score;

      let frequency be Element of HPS;

      

       A1: ( intrval (( hepta_4 (HPS,frequency)),( hepta_1 (HPS,( Octave (HPS,frequency)))))) = (3 qua Real / 2) & ( intrval (( hepta_5 (HPS,frequency)),( hepta_2 (HPS,( Octave (HPS,frequency)))))) = (3 qua Real / 2) & ( intrval (( hepta_6 (HPS,frequency)),( hepta_3 (HPS,( Octave (HPS,frequency)))))) <> (3 qua Real / 2) & ( intrval (( hepta_octave (HPS,frequency)),( hepta_4 (HPS,( Octave (HPS,frequency)))))) = (3 qua Real / 2) by Th92;

      reconsider n2 = 2, n3 = 3 as Element of HPS by Th20;

      (the Ratio of HPS . (n2,n3)) = (( @ n3) / ( @ n2)) by Def25

      .= (3 qua Real / 2);

      then (the Ratio of HPS . (( hepta_4 (HPS,frequency)),( hepta_1 (HPS,( Octave (HPS,frequency)))))) = (the Ratio of HPS . (n2,n3)) & (the Ratio of HPS . (( hepta_5 (HPS,frequency)),( hepta_2 (HPS,( Octave (HPS,frequency)))))) = (the Ratio of HPS . (n2,n3)) & (the Ratio of HPS . (( hepta_6 (HPS,frequency)),( hepta_3 (HPS,( Octave (HPS,frequency)))))) <> (the Ratio of HPS . (n2,n3)) by A1, Th93;

      then (n2,n3) equiv (( hepta_4 (HPS,frequency)),( hepta_1 (HPS,( Octave (HPS,frequency))))) & (n2,n3) equiv (( hepta_5 (HPS,frequency)),( hepta_2 (HPS,( Octave (HPS,frequency))))) & not (n2,n3) equiv (( hepta_6 (HPS,frequency)),( hepta_3 (HPS,( Octave (HPS,frequency))))) by Def08a;

      hence thesis by EQREL_1: 18;

    end;

    definition

      let HPS be MusicSpace;

      let n be non zero natural Number;

      let scale be Element of (n -tuples_on the carrier of HPS);

      let i be Nat;

      :: MUSIC_S1:def91

      func # (scale,i) -> Element of HPS equals

      : Def28: (scale . i) if i in ( Seg n)

      otherwise the Element of HPS;

      correctness

      proof

        per cases ;

          suppose

           A1: i in ( Seg n);

          scale is Element of ( Funcs (( Seg n),the carrier of HPS)) by FINSEQ_2: 93;

          then ( dom scale) = ( Seg n) & ( rng scale) c= the carrier of HPS by FUNCT_2: 92;

          then (scale . i) in ( rng scale) by A1, FUNCT_1:def 3;

          hence thesis;

        end;

          suppose not i in ( Seg n);

          hence thesis;

        end;

      end;

    end

    definition

      let HPS be MusicSpace;

      let n be non zero natural Number;

      let scale be Element of (n -tuples_on the carrier of HPS);

      assume scale is heptatonic;

      :: MUSIC_S1:def92

      attr scale is dorian means ex t1,t2 be positive Real st ((((((t1 * t1) * t1) * t1) * t1) * t2) * t2) = 2 & ( intrval (( # (scale,1)),( # (scale,2)))) = t1 & ( intrval (( # (scale,2)),( # (scale,3)))) = t2 & ( intrval (( # (scale,3)),( # (scale,4)))) = t1 & ( intrval (( # (scale,4)),( # (scale,5)))) = t1 & ( intrval (( # (scale,5)),( # (scale,6)))) = t1 & ( intrval (( # (scale,6)),( # (scale,7)))) = t2 & ( intrval (( # (scale,7)),( # (scale,8)))) = t1;

    end

    definition

      let HPS be MusicSpace;

      let n be non zero natural Number;

      let scale be Element of (n -tuples_on the carrier of HPS);

      assume scale is heptatonic;

      :: MUSIC_S1:def93

      attr scale is hypodorian means ex t1,t2 be positive Real st ((((((t1 * t1) * t1) * t1) * t1) * t2) * t2) = 2 & ( intrval (( # (scale,1)),( # (scale,2)))) = t1 & ( intrval (( # (scale,2)),( # (scale,3)))) = t2 & ( intrval (( # (scale,3)),( # (scale,4)))) = t1 & ( intrval (( # (scale,4)),( # (scale,5)))) = t1 & ( intrval (( # (scale,5)),( # (scale,6)))) = t2 & ( intrval (( # (scale,6)),( # (scale,7)))) = t1 & ( intrval (( # (scale,7)),( # (scale,8)))) = t1;

    end

    definition

      let HPS be MusicSpace;

      let n be non zero natural Number;

      let scale be Element of (n -tuples_on the carrier of HPS);

      assume scale is heptatonic;

      :: MUSIC_S1:def94

      attr scale is phrygian means ex t1,t2 be positive Real st ((((((t1 * t1) * t1) * t1) * t1) * t2) * t2) = 2 & ( intrval (( # (scale,1)),( # (scale,2)))) = t1 & ( intrval (( # (scale,2)),( # (scale,3)))) = t2 & ( intrval (( # (scale,3)),( # (scale,4)))) = t1 & ( intrval (( # (scale,4)),( # (scale,5)))) = t2 & ( intrval (( # (scale,5)),( # (scale,6)))) = t1 & ( intrval (( # (scale,6)),( # (scale,7)))) = t1 & ( intrval (( # (scale,7)),( # (scale,8)))) = t1;

    end

    definition

      let HPS be MusicSpace;

      let n be non zero natural Number;

      let scale be Element of (n -tuples_on the carrier of HPS);

      assume scale is heptatonic;

      :: MUSIC_S1:def95

      attr scale is hypophrygian means ex t1,t2 be positive Real st ((((((t1 * t1) * t1) * t1) * t1) * t2) * t2) = 2 & ( intrval (( # (scale,1)),( # (scale,2)))) = t2 & ( intrval (( # (scale,2)),( # (scale,3)))) = t1 & ( intrval (( # (scale,3)),( # (scale,4)))) = t1 & ( intrval (( # (scale,4)),( # (scale,5)))) = t2 & ( intrval (( # (scale,5)),( # (scale,6)))) = t1 & ( intrval (( # (scale,6)),( # (scale,7)))) = t1 & ( intrval (( # (scale,7)),( # (scale,8)))) = t1;

    end

    definition

      let HPS be MusicSpace;

      let n be non zero natural Number;

      let scale be Element of (n -tuples_on the carrier of HPS);

      assume scale is heptatonic;

      :: MUSIC_S1:def96

      attr scale is lydian means ex t1,t2 be positive Real st ((((((t1 * t1) * t1) * t1) * t1) * t2) * t2) = 2 & ( intrval (( # (scale,1)),( # (scale,2)))) = t1 & ( intrval (( # (scale,2)),( # (scale,3)))) = t1 & ( intrval (( # (scale,3)),( # (scale,4)))) = t2 & ( intrval (( # (scale,4)),( # (scale,5)))) = t1 & ( intrval (( # (scale,5)),( # (scale,6)))) = t1 & ( intrval (( # (scale,6)),( # (scale,7)))) = t2 & ( intrval (( # (scale,7)),( # (scale,8)))) = t1;

    end

    definition

      let HPS be MusicSpace;

      let n be non zero natural Number;

      let scale be Element of (n -tuples_on the carrier of HPS);

      assume scale is heptatonic;

      :: MUSIC_S1:def97

      attr scale is hypolydian means ex t1,t2 be positive Real st ((((((t1 * t1) * t1) * t1) * t1) * t2) * t2) = 2 & ( intrval (( # (scale,1)),( # (scale,2)))) = t1 & ( intrval (( # (scale,2)),( # (scale,3)))) = t1 & ( intrval (( # (scale,3)),( # (scale,4)))) = t2 & ( intrval (( # (scale,4)),( # (scale,5)))) = t1 & ( intrval (( # (scale,5)),( # (scale,6)))) = t1 & ( intrval (( # (scale,6)),( # (scale,7)))) = t1 & ( intrval (( # (scale,7)),( # (scale,8)))) = t2;

    end

    definition

      let HPS be MusicSpace;

      let n be non zero natural Number;

      let scale be Element of (n -tuples_on the carrier of HPS);

      assume scale is heptatonic;

      :: MUSIC_S1:def98

      attr scale is mixolydian means ex t1,t2 be positive Real st ((((((t1 * t1) * t1) * t1) * t1) * t2) * t2) = 2 & ( intrval (( # (scale,1)),( # (scale,2)))) = t1 & ( intrval (( # (scale,2)),( # (scale,3)))) = t1 & ( intrval (( # (scale,3)),( # (scale,4)))) = t2 & ( intrval (( # (scale,4)),( # (scale,5)))) = t1 & ( intrval (( # (scale,5)),( # (scale,6)))) = t1 & ( intrval (( # (scale,6)),( # (scale,7)))) = t2 & ( intrval (( # (scale,7)),( # (scale,8)))) = t1;

    end

    definition

      let HPS be MusicSpace;

      let n be non zero natural Number;

      let scale be Element of (n -tuples_on the carrier of HPS);

      assume scale is heptatonic;

      :: MUSIC_S1:def99

      attr scale is hypomixolydian means ex t1,t2 be positive Real st ((((((t1 * t1) * t1) * t1) * t1) * t2) * t2) = 2 & ( intrval (( # (scale,1)),( # (scale,2)))) = t1 & ( intrval (( # (scale,2)),( # (scale,3)))) = t2 & ( intrval (( # (scale,3)),( # (scale,4)))) = t1 & ( intrval (( # (scale,4)),( # (scale,5)))) = t1 & ( intrval (( # (scale,5)),( # (scale,6)))) = t1 & ( intrval (( # (scale,6)),( # (scale,7)))) = t2 & ( intrval (( # (scale,7)),( # (scale,8)))) = t1;

    end

    definition

      let HPS be MusicSpace;

      let n be non zero natural Number;

      let scale be Element of (n -tuples_on the carrier of HPS);

      assume scale is heptatonic;

      :: MUSIC_S1:def100

      attr scale is eolian means ex t1,t2 be positive Real st ((((((t1 * t1) * t1) * t1) * t1) * t2) * t2) = 2 & ( intrval (( # (scale,1)),( # (scale,2)))) = t1 & ( intrval (( # (scale,2)),( # (scale,3)))) = t2 & ( intrval (( # (scale,3)),( # (scale,4)))) = t1 & ( intrval (( # (scale,4)),( # (scale,5)))) = t1 & ( intrval (( # (scale,5)),( # (scale,6)))) = t2 & ( intrval (( # (scale,6)),( # (scale,7)))) = t1 & ( intrval (( # (scale,7)),( # (scale,8)))) = t1;

    end

    definition

      let HPS be MusicSpace;

      let n be non zero natural Number;

      let scale be Element of (n -tuples_on the carrier of HPS);

      assume scale is heptatonic;

      :: MUSIC_S1:def101

      attr scale is hypoeolian means ex t1,t2 be positive Real st ((((((t1 * t1) * t1) * t1) * t1) * t2) * t2) = 2 & ( intrval (( # (scale,1)),( # (scale,2)))) = t2 & ( intrval (( # (scale,2)),( # (scale,3)))) = t1 & ( intrval (( # (scale,3)),( # (scale,4)))) = t1 & ( intrval (( # (scale,4)),( # (scale,5)))) = t1 & ( intrval (( # (scale,5)),( # (scale,6)))) = t2 & ( intrval (( # (scale,6)),( # (scale,7)))) = t1 & ( intrval (( # (scale,7)),( # (scale,8)))) = t1;

    end

    definition

      let HPS be MusicSpace;

      let n be non zero natural Number;

      let scale be Element of (n -tuples_on the carrier of HPS);

      assume scale is heptatonic;

      :: MUSIC_S1:def102

      attr scale is ionan means

      : Def29: ex t1,t2 be positive Real st ((((((t1 * t1) * t1) * t1) * t1) * t2) * t2) = 2 & ( intrval (( # (scale,1)),( # (scale,2)))) = t1 & ( intrval (( # (scale,2)),( # (scale,3)))) = t1 & ( intrval (( # (scale,3)),( # (scale,4)))) = t2 & ( intrval (( # (scale,4)),( # (scale,5)))) = t1 & ( intrval (( # (scale,5)),( # (scale,6)))) = t1 & ( intrval (( # (scale,6)),( # (scale,7)))) = t1 & ( intrval (( # (scale,7)),( # (scale,8)))) = t2;

    end

    definition

      let HPS be MusicSpace;

      let n be non zero natural Number;

      let scale be Element of (n -tuples_on the carrier of HPS);

      assume scale is heptatonic;

      :: MUSIC_S1:def103

      attr scale is hypoionan means ex t1,t2 be positive Real st ((((((t1 * t1) * t1) * t1) * t1) * t2) * t2) = 2 & ( intrval (( # (scale,1)),( # (scale,2)))) = t1 & ( intrval (( # (scale,2)),( # (scale,3)))) = t1 & ( intrval (( # (scale,3)),( # (scale,4)))) = t2 & ( intrval (( # (scale,4)),( # (scale,5)))) = t1 & ( intrval (( # (scale,5)),( # (scale,6)))) = t1 & ( intrval (( # (scale,6)),( # (scale,7)))) = t2 & ( intrval (( # (scale,7)),( # (scale,8)))) = t1;

    end

    theorem :: MUSIC_S1:118

    ( heptatonic_pythagorean_scale (HPS,frequency)) is ionan

    proof

      set scale = ( heptatonic_pythagorean_scale (HPS,frequency));

      

       A1: scale is heptatonic by Th88BIS;

      reconsider t1 = pythagorean_tone , t2 = heptatonic_pythagorean_semitone as positive Real;

      ex r be positive Real st r = frequency & ( Octave (HPS,frequency)) = (2 * r) by Def15;

      then

       A2: ( hepta_octave (HPS,frequency)) = (2 * ( @ frequency));

      1 in ( Seg 8) & 2 in ( Seg 8) & 3 in ( Seg 8) & 4 in ( Seg 8) & 5 in ( Seg 8) & 6 in ( Seg 8) & 7 in ( Seg 8) & 8 in ( Seg 8) by FINSEQ_1: 1;

      then (scale . 1) = ( # (scale,1)) & (scale . 2) = ( # (scale,2)) & (scale . 3) = ( # (scale,3)) & (scale . 4) = ( # (scale,4)) & (scale . 5) = ( # (scale,5)) & (scale . 6) = ( # (scale,6)) & (scale . 7) = ( # (scale,7)) & (scale . 8) = ( # (scale,8)) by Def28;

      then ( hepta_fondamental (HPS,frequency)) = ( # (scale,1)) & ( hepta_1 (HPS,frequency)) = ( # (scale,2)) & ( hepta_2 (HPS,frequency)) = ( # (scale,3)) & ( hepta_3 (HPS,frequency)) = ( # (scale,4)) & ( hepta_4 (HPS,frequency)) = ( # (scale,5)) & ( hepta_5 (HPS,frequency)) = ( # (scale,6)) & ( hepta_6 (HPS,frequency)) = ( # (scale,7)) & ( hepta_octave (HPS,frequency)) = ( # (scale,8)) by A2, Th88;

      then ((((((t1 * t1) * t1) * t1) * t1) * t2) * t2) = 2 & ( intrval (( # (scale,1)),( # (scale,2)))) = t1 & ( intrval (( # (scale,2)),( # (scale,3)))) = t1 & ( intrval (( # (scale,3)),( # (scale,4)))) = t2 & ( intrval (( # (scale,4)),( # (scale,5)))) = t1 & ( intrval (( # (scale,5)),( # (scale,6)))) = t1 & ( intrval (( # (scale,6)),( # (scale,7)))) = t1 & ( intrval (( # (scale,7)),( # (scale,8)))) = t2 by Th90;

      hence thesis by A1, Def29;

    end;