let HPS be Heptatonic_Pythagorean_Score; for frequency being Element of HPS holds (spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 4 = (27 / 16) * (@ frequency)
let frequency be Element of HPS; (spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 4 = (27 / 16) * (@ frequency)
set MS = HPS;
reconsider n2 = 3 as Nat ;
set q = Fourth (HPS,frequency);
(spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . n2 is Element of HPS
;
then reconsider r32 = (9 / 8) * (@ frequency) as Element of HPS by Th84;
A1: (spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 4 =
(spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . (n2 + 1)
.=
Fifth_reduct (HPS,frequency,((spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . n2))
by Def19
.=
Fifth_reduct (HPS,frequency,r32)
by Th84
;
consider r, s being positive Real such that
A2:
( r = r32 & s = (3 / 2) * r & Fifth (HPS,r32) = s )
by Th54;
A3:
ex fr being positive Real st
( frequency = fr & Octave (HPS,frequency) = 2 * fr )
by Def15;
( (27 / 16) * (@ frequency) < 2 * (@ frequency) & 1 * (@ frequency) < (27 / 16) * (@ frequency) )
by XREAL_1:68;
then
Fifth (HPS,r32) is_Between frequency, Octave (HPS,frequency)
by A2, A3;
hence
(spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 4 = (27 / 16) * (@ frequency)
by A2, A1, Def18; verum