let HPS be Heptatonic_Pythagorean_Score; :: thesis:
let frequency be Element of HPS; :: thesis:
set MS = HPS;
A1: ex fr being positive Real st
( frequency = fr & Octave (HPS,frequency) = 2 * fr ) by Def15;
A2: (heptatonic_pythagorean_scale (HPS,frequency)) . 8 = 2 * (@ frequency) by Th88;
ex r1, r2, r3, r4, r5, r6, r7, r8 being positive Real st
( (heptatonic_pythagorean_scale (HPS,frequency)) . 1 = r1 & (heptatonic_pythagorean_scale (HPS,frequency)) . 2 = r2 & (heptatonic_pythagorean_scale (HPS,frequency)) . 3 = r3 & (heptatonic_pythagorean_scale (HPS,frequency)) . 4 = r4 & (heptatonic_pythagorean_scale (HPS,frequency)) . 5 = r5 & (heptatonic_pythagorean_scale (HPS,frequency)) . 6 = r6 & (heptatonic_pythagorean_scale (HPS,frequency)) . 7 = r7 & (heptatonic_pythagorean_scale (HPS,frequency)) . 8 = r8 & r2 / r1 = 9 / 8 & r3 / r2 = 9 / 8 & r4 / r3 = 256 / 243 & r5 / r4 = 9 / 8 & r6 / r5 = 9 / 8 & r7 / r6 = 9 / 8 & r8 / r7 = 256 / 243 ) by Lem90;
hence ( intrval ((hepta_fondamental (HPS,frequency)),(hepta_1 (HPS,frequency))) = pythagorean_tone & intrval ((hepta_1 (HPS,frequency)),(hepta_2 (HPS,frequency))) = pythagorean_tone & intrval ((hepta_2 (HPS,frequency)),(hepta_3 (HPS,frequency))) = heptatonic_pythagorean_semitone & intrval ((hepta_3 (HPS,frequency)),(hepta_4 (HPS,frequency))) = pythagorean_tone & intrval ((hepta_4 (HPS,frequency)),(hepta_5 (HPS,frequency))) = pythagorean_tone & intrval ((hepta_5 (HPS,frequency)),(hepta_6 (HPS,frequency))) = pythagorean_tone & intrval ((hepta_6 (HPS,frequency)),(hepta_octave (HPS,frequency))) = heptatonic_pythagorean_semitone ) by A1, A2, Def21; :: thesis: