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