let HPS be Heptatonic_Pythagorean_Score; :: thesis: for frequency being Element of HPS holds (spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 1 = frequency
let frequency be Element of HPS; :: thesis: (spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 1 = frequency
set MS = HPS;
set q = Fourth (HPS,frequency);
set f1 = (spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 1;
consider frq being positive Real such that
A1: ( frequency = frq & Fourth (HPS,frequency) = (4 / 3) * frq ) by Def24;
reconsider n1 = 1, n0 = 0 as Nat ;
A2: (spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 1 = (spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . (n0 + 1)
.= Fifth_reduct (HPS,frequency,((spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . n0)) by Def19
.= Fifth_reduct (HPS,frequency,(Fourth (HPS,frequency))) by Def19 ;
consider r, s being positive Real such that
A3: ( r = Fourth (HPS,frequency) & s = (3 / 2) * r & Fifth (HPS,(Fourth (HPS,frequency))) = s ) by Th54;
consider fr2 being positive Real such that
A4: frequency = fr2 and
A5: Octave (HPS,frequency) = 2 * fr2 by Def15;
consider ro being positive Real such that
A6: Fifth (HPS,(Fourth (HPS,frequency))) = ro and
A7: Octave_descendent (HPS,(Fifth (HPS,(Fourth (HPS,frequency))))) = ro / 2 by Th51;
not Fifth (HPS,(Fourth (HPS,frequency))) is_Between frequency, Octave (HPS,frequency) by A3, A1, A4, A5;
hence (spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 1 = frequency by A2, A6, A7, A3, A1, Def18; :: thesis: verum