let MS be MusicSpace; :: thesis: for frequency being Element of MS holds
( 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 )
let frequency be Element of MS; :: thesis: ( 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 )
consider r1, r2 being 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 being 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 being 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 being 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 being 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 being 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 / 8 & s3 / s2 = 9 / 8 & s4 / s3 = 32 / 27 & s5 / s4 = 9 / 8 & s6 / s5 = 32 / 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; :: thesis: verum