let MS be MusicSpace; 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; 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; ( (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 )
; ( 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; verum