let HPS be satisfying_euclidean Heptatonic_Pythagorean_Score; :: thesis: for frequency being Element of HPS holds heptatonic_pythagorean_scale (HPS,frequency) is perfect_fifth
let frequency be Element of HPS; :: thesis: heptatonic_pythagorean_scale (HPS,frequency) is perfect_fifth
A1: heptatonic_pythagorean_scale (HPS,frequency) is heptatonic by Th88BIS;
set gamme = heptatonic_pythagorean_scale (HPS,frequency);
A2: ( 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;
A3: ex fo being positive Real st
( frequency = fo & Octave (HPS,frequency) = 2 * fo ) by Def15;
then hepta_octave (HPS,frequency) = 2 * (@ frequency) ;
then A4: hepta_octave (HPS,frequency) = (heptatonic_pythagorean_scale (HPS,frequency)) . 8 by Th88;
A5: the Ratio of HPS . ((hepta_fondamental (HPS,frequency)),(hepta_4 (HPS,frequency))) = (@ (hepta_4 (HPS,frequency))) / (@ (hepta_fondamental (HPS,frequency))) by Def25
.= 3 / 2 by A2, XCMPLX_1:89 ;
A6: the Ratio of HPS . ((hepta_1 (HPS,frequency)),(hepta_5 (HPS,frequency))) = (@ (hepta_5 (HPS,frequency))) / (@ (hepta_1 (HPS,frequency))) by Def25
.= ((27 / 16) / (9 / 8)) * ((@ frequency) / (@ frequency)) by A2, XCMPLX_1:76
.= 3 / 2 by XCMPLX_1:88 ;
A7: the Ratio of HPS . ((hepta_2 (HPS,frequency)),(hepta_6 (HPS,frequency))) = (@ (hepta_6 (HPS,frequency))) / (@ (hepta_2 (HPS,frequency))) by Def25
.= ((243 / 128) / (81 / 64)) * ((@ frequency) / (@ frequency)) by A2, XCMPLX_1:76
.= 3 / 2 by XCMPLX_1:88 ;
A8: the Ratio of HPS . ((hepta_3 (HPS,frequency)),(hepta_octave (HPS,frequency))) = (@ (hepta_octave (HPS,frequency))) / (@ (hepta_3 (HPS,frequency))) by Def25
.= (2 * (@ frequency)) / ((4 / 3) * (@ frequency)) by Th88, A3
.= (2 / (4 / 3)) * ((@ frequency) / (@ frequency)) by XCMPLX_1:76
.= 3 / 2 by XCMPLX_1:88 ;
reconsider n2 = 2, n3 = 3 as Element of HPS by Th20;
the Ratio of HPS . (n2,n3) = (@ n3) / (@ n2) by Def25
.= 3 / 2 ;
then ( n2,n3 equiv hepta_fondamental (HPS,frequency), hepta_4 (HPS,frequency) & n2,n3 equiv hepta_1 (HPS,frequency), hepta_5 (HPS,frequency) & n2,n3 equiv hepta_2 (HPS,frequency), hepta_6 (HPS,frequency) & n2,n3 equiv hepta_3 (HPS,frequency), hepta_octave (HPS,frequency) ) by A5, A6, A7, A8, Def08a;
then ( [(hepta_fondamental (HPS,frequency)),(hepta_4 (HPS,frequency))] in fifth HPS & [(hepta_1 (HPS,frequency)),(hepta_5 (HPS,frequency))] in fifth HPS & [(hepta_2 (HPS,frequency)),(hepta_6 (HPS,frequency))] in fifth HPS & [(hepta_3 (HPS,frequency)),(hepta_octave (HPS,frequency))] in fifth HPS ) by EQREL_1:18;
hence heptatonic_pythagorean_scale (HPS,frequency) is perfect_fifth by A4, A1, Def27; :: thesis: verum