let MS be non empty satisfying_Real satisfying_equiv satisfying_interval satisfying_commutativity satisfying_Nat satisfying_harmonic_closed satisfying_fifth_constructible classical_fifth satisfying_octave_constructible classical_octave satisfying_octave_descendent_constructible MusicStruct ; for fondamentale being Element of MS holds (spiral_of_fifths (MS,fondamentale,fondamentale)) . 5 = (243 / 128) * (@ fondamentale)
let fondamentale be Element of MS; (spiral_of_fifths (MS,fondamentale,fondamentale)) . 5 = (243 / 128) * (@ fondamentale)
reconsider n5 = 5, n4 = 4, n3 = 3, n2 = 2, n1 = 1, n0 = 0 as Nat ;
(spiral_of_fifths (MS,fondamentale,fondamentale)) . n4 is Element of MS
;
then reconsider r32 = (81 / 64) * (@ fondamentale) as Element of MS by Th61;
A1: (spiral_of_fifths (MS,fondamentale,fondamentale)) . 5 =
(spiral_of_fifths (MS,fondamentale,fondamentale)) . (n4 + 1)
.=
Fifth_reduct (MS,fondamentale,((spiral_of_fifths (MS,fondamentale,fondamentale)) . n4))
by Def19
.=
Fifth_reduct (MS,fondamentale,r32)
by Th61
;
consider r, s being positive Real such that
A2:
( r = r32 & s = (3 / 2) * r & Fifth (MS,r32) = s )
by Th54;
A3:
ex fr being positive Real st
( fondamentale = fr & Octave (MS,fondamentale) = 2 * fr )
by Def15;
( (243 / 128) * (@ fondamentale) < 2 * (@ fondamentale) & 1 * (@ fondamentale) < (243 / 128) * (@ fondamentale) )
by XREAL_1:68;
then
Fifth (MS,r32) is_Between fondamentale, Octave (MS,fondamentale)
by A2, A3;
hence
(spiral_of_fifths (MS,fondamentale,fondamentale)) . 5 = (243 / 128) * (@ fondamentale)
by A2, A1, Def18; verum