let HPS be Heptatonic_Pythagorean_Score; :: thesis:
let frequency be Element of HPS; :: thesis:
set MS = HPS;
set gamme = heptatonic_pythagorean_scale (HPS,frequency);
A1: ( (heptatonic_pythagorean_scale (HPS,frequency)) . 1 = (spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 1 & (heptatonic_pythagorean_scale (HPS,frequency)) . 2 = (spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 3 & (heptatonic_pythagorean_scale (HPS,frequency)) . 3 = (spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 5 & (heptatonic_pythagorean_scale (HPS,frequency)) . 4 = Fourth (HPS,frequency) & (heptatonic_pythagorean_scale (HPS,frequency)) . 5 = (spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 2 & (heptatonic_pythagorean_scale (HPS,frequency)) . 6 = (spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 4 & (heptatonic_pythagorean_scale (HPS,frequency)) . 7 = (spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 6 & (heptatonic_pythagorean_scale (HPS,frequency)) . 8 = Octave (HPS,((spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 1)) ) by Def26;
heptatonic_pythagorean_scale (HPS,frequency) in 8 -tuples_on the carrier of HPS ;
then heptatonic_pythagorean_scale (HPS,frequency) in { s where s is Element of the carrier of HPS * : len s = 8 } by FINSEQ_2:def 4;
then consider s being Element of the carrier of HPS * such that
A2: s = heptatonic_pythagorean_scale (HPS,frequency) and
A3: len s = 8 ;
dom s = Seg 8 by A3, FINSEQ_1:def 3;
then reconsider g1 = (heptatonic_pythagorean_scale (HPS,frequency)) . 4, g2 = (heptatonic_pythagorean_scale (HPS,frequency)) . 1, g3 = (heptatonic_pythagorean_scale (HPS,frequency)) . 5, g4 = (heptatonic_pythagorean_scale (HPS,frequency)) . 2, g5 = (heptatonic_pythagorean_scale (HPS,frequency)) . 6, g6 = (heptatonic_pythagorean_scale (HPS,frequency)) . 3, g7 = (heptatonic_pythagorean_scale (HPS,frequency)) . 7, g8 = (heptatonic_pythagorean_scale (HPS,frequency)) . 8 as Element of the carrier of HPS by A2, FINSEQ_1:1, FINSEQ_2:11;
reconsider frequency2 = g1 as Element of HPS ;
reconsider r1 = @ frequency2, r2 = @ g2, r3 = @ g3, r4 = @ g4, r5 = @ g5, r6 = @ g6, r7 = @ g7, r8 = @ g8 as positive Real ;
A4: ex fr being positive Real st
( frequency = fr & Octave (HPS,frequency) = 2 * fr ) by Def15;
A5: r8 = Octave (HPS,((spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 1)) by Def26
.= 2 * (@ frequency) by A4, Th82 ;
ex fr being positive Real st
( frequency = fr & Fourth (HPS,frequency) = (4 / 3) * fr ) by Def24;
hence ( (heptatonic_pythagorean_scale (HPS,frequency)) . 1 = 1 * (@ frequency) & (heptatonic_pythagorean_scale (HPS,frequency)) . 2 = (9 / 8) * (@ frequency) & (heptatonic_pythagorean_scale (HPS,frequency)) . 3 = (81 / 64) * (@ frequency) & (heptatonic_pythagorean_scale (HPS,frequency)) . 4 = (4 / 3) * (@ frequency) & (heptatonic_pythagorean_scale (HPS,frequency)) . 5 = (3 / 2) * (@ frequency) & (heptatonic_pythagorean_scale (HPS,frequency)) . 6 = (27 / 16) * (@ frequency) & (heptatonic_pythagorean_scale (HPS,frequency)) . 7 = (243 / 128) * (@ frequency) & (heptatonic_pythagorean_scale (HPS,frequency)) . 8 = 2 * (@ frequency) ) by A5, A1, Th82, Th84, Th86, Th83, Th85, Th87; :: thesis: