let HPS be Heptatonic_Pythagorean_Score; :: thesis: for frequency being Element of HPS holds
( (heptatonic_pythagorean_scale_ascending (HPS,frequency)) . 1 = 2 * (@ frequency) & (heptatonic_pythagorean_scale_ascending (HPS,frequency)) . 2 = (9 / 4) * (@ frequency) & (heptatonic_pythagorean_scale_ascending (HPS,frequency)) . 3 = (81 / 32) * (@ frequency) & (heptatonic_pythagorean_scale_ascending (HPS,frequency)) . 4 = (8 / 3) * (@ frequency) & (heptatonic_pythagorean_scale_ascending (HPS,frequency)) . 5 = 3 * (@ frequency) & (heptatonic_pythagorean_scale_ascending (HPS,frequency)) . 6 = (27 / 8) * (@ frequency) & (heptatonic_pythagorean_scale_ascending (HPS,frequency)) . 7 = (243 / 64) * (@ frequency) & (heptatonic_pythagorean_scale_ascending (HPS,frequency)) . 8 = 4 * (@ frequency) )
let frequency be Element of HPS; :: thesis: ( (heptatonic_pythagorean_scale_ascending (HPS,frequency)) . 1 = 2 * (@ frequency) & (heptatonic_pythagorean_scale_ascending (HPS,frequency)) . 2 = (9 / 4) * (@ frequency) & (heptatonic_pythagorean_scale_ascending (HPS,frequency)) . 3 = (81 / 32) * (@ frequency) & (heptatonic_pythagorean_scale_ascending (HPS,frequency)) . 4 = (8 / 3) * (@ frequency) & (heptatonic_pythagorean_scale_ascending (HPS,frequency)) . 5 = 3 * (@ frequency) & (heptatonic_pythagorean_scale_ascending (HPS,frequency)) . 6 = (27 / 8) * (@ frequency) & (heptatonic_pythagorean_scale_ascending (HPS,frequency)) . 7 = (243 / 64) * (@ frequency) & (heptatonic_pythagorean_scale_ascending (HPS,frequency)) . 8 = 4 * (@ frequency) )
set f2 = Octave (HPS,frequency);
consider fr being positive Real such that
A1: ( frequency = fr & Octave (HPS,frequency) = 2 * fr ) by Def15;
( (heptatonic_pythagorean_scale (HPS,(Octave (HPS,frequency)))) . 1 = 1 * (@ (Octave (HPS,frequency))) & (heptatonic_pythagorean_scale (HPS,(Octave (HPS,frequency)))) . 2 = (9 / 8) * (@ (Octave (HPS,frequency))) & (heptatonic_pythagorean_scale (HPS,(Octave (HPS,frequency)))) . 3 = (81 / 64) * (@ (Octave (HPS,frequency))) & (heptatonic_pythagorean_scale (HPS,(Octave (HPS,frequency)))) . 4 = (4 / 3) * (@ (Octave (HPS,frequency))) & (heptatonic_pythagorean_scale (HPS,(Octave (HPS,frequency)))) . 5 = (3 / 2) * (@ (Octave (HPS,frequency))) & (heptatonic_pythagorean_scale (HPS,(Octave (HPS,frequency)))) . 6 = (27 / 16) * (@ (Octave (HPS,frequency))) & (heptatonic_pythagorean_scale (HPS,(Octave (HPS,frequency)))) . 7 = (243 / 128) * (@ (Octave (HPS,frequency))) & (heptatonic_pythagorean_scale (HPS,(Octave (HPS,frequency)))) . 8 = 2 * (@ (Octave (HPS,frequency))) ) by Th88;
hence ( (heptatonic_pythagorean_scale_ascending (HPS,frequency)) . 1 = 2 * (@ frequency) & (heptatonic_pythagorean_scale_ascending (HPS,frequency)) . 2 = (9 / 4) * (@ frequency) & (heptatonic_pythagorean_scale_ascending (HPS,frequency)) . 3 = (81 / 32) * (@ frequency) & (heptatonic_pythagorean_scale_ascending (HPS,frequency)) . 4 = (8 / 3) * (@ frequency) & (heptatonic_pythagorean_scale_ascending (HPS,frequency)) . 5 = 3 * (@ frequency) & (heptatonic_pythagorean_scale_ascending (HPS,frequency)) . 6 = (27 / 8) * (@ frequency) & (heptatonic_pythagorean_scale_ascending (HPS,frequency)) . 7 = (243 / 64) * (@ frequency) & (heptatonic_pythagorean_scale_ascending (HPS,frequency)) . 8 = 4 * (@ frequency) ) by A1; :: thesis: verum