let HPS be Heptatonic_Pythagorean_Score; for frequency being Element of HPS holds
( intrval ((hepta_4 (HPS,frequency)),(hepta_1 (HPS,(Octave (HPS,frequency))))) = 3 / 2 & intrval ((hepta_5 (HPS,frequency)),(hepta_2 (HPS,(Octave (HPS,frequency))))) = 3 / 2 & intrval ((hepta_6 (HPS,frequency)),(hepta_3 (HPS,(Octave (HPS,frequency))))) <> 3 / 2 & intrval ((hepta_octave (HPS,frequency)),(hepta_4 (HPS,(Octave (HPS,frequency))))) = 3 / 2 )
let frequency be Element of HPS; ( intrval ((hepta_4 (HPS,frequency)),(hepta_1 (HPS,(Octave (HPS,frequency))))) = 3 / 2 & intrval ((hepta_5 (HPS,frequency)),(hepta_2 (HPS,(Octave (HPS,frequency))))) = 3 / 2 & intrval ((hepta_6 (HPS,frequency)),(hepta_3 (HPS,(Octave (HPS,frequency))))) <> 3 / 2 & intrval ((hepta_octave (HPS,frequency)),(hepta_4 (HPS,(Octave (HPS,frequency))))) = 3 / 2 )
set gamme = heptatonic_pythagorean_scale (HPS,frequency);
A1:
( hepta_fondamental (HPS,frequency) = 1 * (@ frequency) & hepta_1 (HPS,frequency) = (9 / 8) * (@ frequency) & hepta_2 (HPS,frequency) = (81 / 64) * (@ frequency) & hepta_3 (HPS,frequency) = (4 / 3) * (@ frequency) & hepta_4 (HPS,frequency) = (3 / 2) * (@ frequency) & hepta_5 (HPS,frequency) = (27 / 16) * (@ frequency) & hepta_6 (HPS,frequency) = (243 / 128) * (@ frequency) )
by Th88;
set f2 = Octave (HPS,frequency);
set gamme2 = heptatonic_pythagorean_scale (HPS,(Octave (HPS,frequency)));
A2:
( (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 Th91;
A3:
ex fo being positive Real st
( frequency = fo & Octave (HPS,frequency) = 2 * fo )
by Def15;
now ( intrval ((hepta_4 (HPS,frequency)),(hepta_1 (HPS,(Octave (HPS,frequency))))) = 3 / 2 & intrval ((hepta_5 (HPS,frequency)),(hepta_2 (HPS,(Octave (HPS,frequency))))) = 3 / 2 & intrval ((hepta_6 (HPS,frequency)),(hepta_3 (HPS,(Octave (HPS,frequency))))) <> 3 / 2 & intrval ((hepta_octave (HPS,frequency)),(hepta_4 (HPS,(Octave (HPS,frequency))))) = 3 / 2 )thus intrval (
(hepta_4 (HPS,frequency)),
(hepta_1 (HPS,(Octave (HPS,frequency))))) =
((9 / 4) * (@ frequency)) / ((3 / 2) * (@ frequency))
by A2, A1, Def21
.=
(((9 / 4) / (3 / 2)) * (@ frequency)) / (@ frequency)
by XCMPLX_1:83
.=
3
/ 2
by XCMPLX_1:89
;
( intrval ((hepta_5 (HPS,frequency)),(hepta_2 (HPS,(Octave (HPS,frequency))))) = 3 / 2 & intrval ((hepta_6 (HPS,frequency)),(hepta_3 (HPS,(Octave (HPS,frequency))))) <> 3 / 2 & intrval ((hepta_octave (HPS,frequency)),(hepta_4 (HPS,(Octave (HPS,frequency))))) = 3 / 2 )thus intrval (
(hepta_5 (HPS,frequency)),
(hepta_2 (HPS,(Octave (HPS,frequency))))) =
((81 / 32) * (@ frequency)) / ((27 / 16) * (@ frequency))
by A2, A1, Def21
.=
(((81 / 32) / (27 / 16)) * (@ frequency)) / (@ frequency)
by XCMPLX_1:83
.=
3
/ 2
by XCMPLX_1:89
;
( intrval ((hepta_6 (HPS,frequency)),(hepta_3 (HPS,(Octave (HPS,frequency))))) <> 3 / 2 & intrval ((hepta_octave (HPS,frequency)),(hepta_4 (HPS,(Octave (HPS,frequency))))) = 3 / 2 ) intrval (
(hepta_6 (HPS,frequency)),
(hepta_3 (HPS,(Octave (HPS,frequency))))) =
((8 / 3) * (@ frequency)) / ((243 / 128) * (@ frequency))
by A2, A1, Def21
.=
(((8 / 3) / (243 / 128)) * (@ frequency)) / (@ frequency)
by XCMPLX_1:83
;
hence
intrval (
(hepta_6 (HPS,frequency)),
(hepta_3 (HPS,(Octave (HPS,frequency)))))
<> 3
/ 2
by XCMPLX_1:89;
intrval ((hepta_octave (HPS,frequency)),(hepta_4 (HPS,(Octave (HPS,frequency))))) = 3 / 2thus intrval (
(hepta_octave (HPS,frequency)),
(hepta_4 (HPS,(Octave (HPS,frequency))))) =
(3 * (@ frequency)) / (2 * (@ frequency))
by A3, A2, Def21
.=
((3 / 2) * (@ frequency)) / (@ frequency)
by XCMPLX_1:83
.=
3
/ 2
by XCMPLX_1:89
;
verum end;
hence
( intrval ((hepta_4 (HPS,frequency)),(hepta_1 (HPS,(Octave (HPS,frequency))))) = 3 / 2 & intrval ((hepta_5 (HPS,frequency)),(hepta_2 (HPS,(Octave (HPS,frequency))))) = 3 / 2 & intrval ((hepta_6 (HPS,frequency)),(hepta_3 (HPS,(Octave (HPS,frequency))))) <> 3 / 2 & intrval ((hepta_octave (HPS,frequency)),(hepta_4 (HPS,(Octave (HPS,frequency))))) = 3 / 2 )
; verum