let MS be MusicSpace; :: thesis:
let frequency be Element of MS; :: thesis:
set r1 = penta_fondamentale (MS,frequency);
set r2 = penta_1 (MS,frequency);
set r3 = penta_2 (MS,frequency);
set r4 = penta_3 (MS,frequency);
set r5 = penta_4 (MS,frequency);
set r6 = penta_octave (MS,frequency);
the carrier of MS c= REALPLUS by Def07a;
then reconsider r91 = penta_fondamentale (MS,frequency), r92 = penta_1 (MS,frequency), r93 = penta_2 (MS,frequency), r94 = penta_3 (MS,frequency), r95 = penta_4 (MS,frequency), r96 = penta_octave (MS,frequency) 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 / 8 & r93 / r92 = 9 / 8 & r94 / r93 = 32 / 27 & r95 / r94 = 9 / 8 & r96 / r95 = 32 / 27 ) by Th68;
hence ex 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 & r2 / r1 = 9 / 8 & r3 / r2 = 9 / 8 & r4 / r3 = 32 / 27 & r5 / r4 = 9 / 8 & r6 / r5 = 32 / 27 ) by A1; :: thesis: