let MS be MusicSpace; :: thesis: for frequency being Element of MS
for r1, r2, r3, r4, r5, r6 being 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 / 8 & r3 / r2 = 9 / 8 & r4 / r3 = 32 / 27 & r5 / r4 = 9 / 8 & r6 / r5 = 32 / 27 )
let frequency be Element of MS; :: thesis: for r1, r2, r3, r4, r5, r6 being 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 / 8 & r3 / r2 = 9 / 8 & r4 / r3 = 32 / 27 & r5 / r4 = 9 / 8 & r6 / r5 = 32 / 27 )
let r1, r2, r3, r4, r5, r6 be positive Real; :: thesis: ( (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 implies ( r2 / r1 = 9 / 8 & r3 / r2 = 9 / 8 & r4 / r3 = 32 / 27 & r5 / r4 = 9 / 8 & r6 / r5 = 32 / 27 ) )
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 ) ; :: thesis: ( r2 / r1 = 9 / 8 & r3 / r2 = 9 / 8 & r4 / r3 = 32 / 27 & r5 / r4 = 9 / 8 & r6 / r5 = 32 / 27 )
set gamme = pentatonic_pythagorean_scale (MS,frequency);
A2: ( (pentatonic_pythagorean_scale (MS,frequency)) . 1 = frequency & (pentatonic_pythagorean_scale (MS,frequency)) . 2 = (spiral_of_fifths (MS,frequency,frequency)) . 2 & (pentatonic_pythagorean_scale (MS,frequency)) . 3 = (spiral_of_fifths (MS,frequency,frequency)) . 4 & (pentatonic_pythagorean_scale (MS,frequency)) . 4 = (spiral_of_fifths (MS,frequency,frequency)) . 1 & (pentatonic_pythagorean_scale (MS,frequency)) . 5 = (spiral_of_fifths (MS,frequency,frequency)) . 3 & (pentatonic_pythagorean_scale (MS,frequency)) . 6 = Octave (MS,frequency) ) by Def20;
pentatonic_pythagorean_scale (MS,frequency) is pentatonic by Th67;
then consider frequency being Element of MS, r1, r2, r3, r4, r5, r6 being positive Real such that
A3: ( (pentatonic_pythagorean_scale (MS,frequency)) . 1 = frequency & (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 & r1 < r2 & r2 < r3 & r3 < r4 & r4 < r5 & r5 < r6 & (pentatonic_pythagorean_scale (MS,frequency)) . 6 = Octave (MS,frequency) ) ;
( (@ ((spiral_of_fifths (MS,frequency,frequency)) . 2)) / (@ frequency) = (3 * 3) / ((2 * 2) * 2) & (@ ((spiral_of_fifths (MS,frequency,frequency)) . 4)) / (@ ((spiral_of_fifths (MS,frequency,frequency)) . 2)) = (3 * 3) / ((2 * 2) * 2) & (@ ((spiral_of_fifths (MS,frequency,frequency)) . 1)) / (@ ((spiral_of_fifths (MS,frequency,frequency)) . 4)) = 32 / 27 & (@ ((spiral_of_fifths (MS,frequency,frequency)) . 3)) / (@ ((spiral_of_fifths (MS,frequency,frequency)) . 1)) = 9 / 8 & (@ (Octave (MS,frequency))) / (@ ((spiral_of_fifths (MS,frequency,frequency)) . 3)) = 32 / 27 ) by Th62, Th63, Th64, Th65, Th66;
hence ( r2 / r1 = 9 / 8 & r3 / r2 = 9 / 8 & r4 / r3 = 32 / 27 & r5 / r4 = 9 / 8 & r6 / r5 = 32 / 27 ) by A1, A2, A3; :: thesis: verum