let HPS be Heptatonic_Pythagorean_Score; :: thesis: for frequency being Element of HPS holds heptatonic_pythagorean_scale (HPS,frequency) is ionan
let frequency be Element of HPS; :: thesis: heptatonic_pythagorean_scale (HPS,frequency) is ionan
set scale = heptatonic_pythagorean_scale (HPS,frequency);
A1: heptatonic_pythagorean_scale (HPS,frequency) is heptatonic by Th88BIS;
reconsider t1 = pythagorean_tone , t2 = heptatonic_pythagorean_semitone as positive Real ;
ex r being positive Real st
( r = frequency & Octave (HPS,frequency) = 2 * r ) by Def15;
then A2: hepta_octave (HPS,frequency) = 2 * (@ frequency) ;
( 1 in Seg 8 & 2 in Seg 8 & 3 in Seg 8 & 4 in Seg 8 & 5 in Seg 8 & 6 in Seg 8 & 7 in Seg 8 & 8 in Seg 8 ) by FINSEQ_1:1;
then ( (heptatonic_pythagorean_scale (HPS,frequency)) . 1 = # ((heptatonic_pythagorean_scale (HPS,frequency)),1) & (heptatonic_pythagorean_scale (HPS,frequency)) . 2 = # ((heptatonic_pythagorean_scale (HPS,frequency)),2) & (heptatonic_pythagorean_scale (HPS,frequency)) . 3 = # ((heptatonic_pythagorean_scale (HPS,frequency)),3) & (heptatonic_pythagorean_scale (HPS,frequency)) . 4 = # ((heptatonic_pythagorean_scale (HPS,frequency)),4) & (heptatonic_pythagorean_scale (HPS,frequency)) . 5 = # ((heptatonic_pythagorean_scale (HPS,frequency)),5) & (heptatonic_pythagorean_scale (HPS,frequency)) . 6 = # ((heptatonic_pythagorean_scale (HPS,frequency)),6) & (heptatonic_pythagorean_scale (HPS,frequency)) . 7 = # ((heptatonic_pythagorean_scale (HPS,frequency)),7) & (heptatonic_pythagorean_scale (HPS,frequency)) . 8 = # ((heptatonic_pythagorean_scale (HPS,frequency)),8) ) by Def28;
then ( hepta_fondamental (HPS,frequency) = # ((heptatonic_pythagorean_scale (HPS,frequency)),1) & hepta_1 (HPS,frequency) = # ((heptatonic_pythagorean_scale (HPS,frequency)),2) & hepta_2 (HPS,frequency) = # ((heptatonic_pythagorean_scale (HPS,frequency)),3) & hepta_3 (HPS,frequency) = # ((heptatonic_pythagorean_scale (HPS,frequency)),4) & hepta_4 (HPS,frequency) = # ((heptatonic_pythagorean_scale (HPS,frequency)),5) & hepta_5 (HPS,frequency) = # ((heptatonic_pythagorean_scale (HPS,frequency)),6) & hepta_6 (HPS,frequency) = # ((heptatonic_pythagorean_scale (HPS,frequency)),7) & hepta_octave (HPS,frequency) = # ((heptatonic_pythagorean_scale (HPS,frequency)),8) ) by A2, Th88;
then ( (((((t1 * t1) * t1) * t1) * t1) * t2) * t2 = 2 & intrval ((# ((heptatonic_pythagorean_scale (HPS,frequency)),1)),(# ((heptatonic_pythagorean_scale (HPS,frequency)),2))) = t1 & intrval ((# ((heptatonic_pythagorean_scale (HPS,frequency)),2)),(# ((heptatonic_pythagorean_scale (HPS,frequency)),3))) = t1 & intrval ((# ((heptatonic_pythagorean_scale (HPS,frequency)),3)),(# ((heptatonic_pythagorean_scale (HPS,frequency)),4))) = t2 & intrval ((# ((heptatonic_pythagorean_scale (HPS,frequency)),4)),(# ((heptatonic_pythagorean_scale (HPS,frequency)),5))) = t1 & intrval ((# ((heptatonic_pythagorean_scale (HPS,frequency)),5)),(# ((heptatonic_pythagorean_scale (HPS,frequency)),6))) = t1 & intrval ((# ((heptatonic_pythagorean_scale (HPS,frequency)),6)),(# ((heptatonic_pythagorean_scale (HPS,frequency)),7))) = t1 & intrval ((# ((heptatonic_pythagorean_scale (HPS,frequency)),7)),(# ((heptatonic_pythagorean_scale (HPS,frequency)),8))) = t2 ) by Th90;
hence heptatonic_pythagorean_scale (HPS,frequency) is ionan by A1, Def29; :: thesis: verum