let HPS be Heptatonic_Pythagorean_Score; :: thesis: for frequency being Element of HPS ex r1, r2, r3, r4, r5, r6, r7, r8 being positive Real st
( (heptatonic_pythagorean_scale (HPS,frequency)) . 1 = r1 & (heptatonic_pythagorean_scale (HPS,frequency)) . 2 = r2 & (heptatonic_pythagorean_scale (HPS,frequency)) . 3 = r3 & (heptatonic_pythagorean_scale (HPS,frequency)) . 4 = r4 & (heptatonic_pythagorean_scale (HPS,frequency)) . 5 = r5 & (heptatonic_pythagorean_scale (HPS,frequency)) . 6 = r6 & (heptatonic_pythagorean_scale (HPS,frequency)) . 7 = r7 & (heptatonic_pythagorean_scale (HPS,frequency)) . 8 = r8 & r2 / r1 = 9 / 8 & r3 / r2 = 9 / 8 & r4 / r3 = 256 / 243 & r5 / r4 = 9 / 8 & r6 / r5 = 9 / 8 & r7 / r6 = 9 / 8 & r8 / r7 = 256 / 243 )
let frequency be Element of HPS; :: thesis: ex r1, r2, r3, r4, r5, r6, r7, r8 being positive Real st
( (heptatonic_pythagorean_scale (HPS,frequency)) . 1 = r1 & (heptatonic_pythagorean_scale (HPS,frequency)) . 2 = r2 & (heptatonic_pythagorean_scale (HPS,frequency)) . 3 = r3 & (heptatonic_pythagorean_scale (HPS,frequency)) . 4 = r4 & (heptatonic_pythagorean_scale (HPS,frequency)) . 5 = r5 & (heptatonic_pythagorean_scale (HPS,frequency)) . 6 = r6 & (heptatonic_pythagorean_scale (HPS,frequency)) . 7 = r7 & (heptatonic_pythagorean_scale (HPS,frequency)) . 8 = r8 & r2 / r1 = 9 / 8 & r3 / r2 = 9 / 8 & r4 / r3 = 256 / 243 & r5 / r4 = 9 / 8 & r6 / r5 = 9 / 8 & r7 / r6 = 9 / 8 & r8 / r7 = 256 / 243 )
set MS = HPS;
set r1 = hepta_fondamental (HPS,frequency);
set r2 = hepta_1 (HPS,frequency);
set r3 = hepta_2 (HPS,frequency);
set r4 = hepta_3 (HPS,frequency);
set r5 = hepta_4 (HPS,frequency);
set r6 = hepta_5 (HPS,frequency);
set r7 = hepta_6 (HPS,frequency);
set r8 = hepta_octave (HPS,frequency);
the carrier of HPS c= REALPLUS by Def07a;
then reconsider r91 = hepta_fondamental (HPS,frequency), r92 = hepta_1 (HPS,frequency), r93 = hepta_2 (HPS,frequency), r94 = hepta_3 (HPS,frequency), r95 = hepta_4 (HPS,frequency), r96 = hepta_5 (HPS,frequency), r97 = hepta_6 (HPS,frequency), r98 = hepta_octave (HPS,frequency) as positive Real by Th1;
take r91 ; :: thesis: ex r2, r3, r4, r5, r6, r7, r8 being positive Real st
( (heptatonic_pythagorean_scale (HPS,frequency)) . 1 = r91 & (heptatonic_pythagorean_scale (HPS,frequency)) . 2 = r2 & (heptatonic_pythagorean_scale (HPS,frequency)) . 3 = r3 & (heptatonic_pythagorean_scale (HPS,frequency)) . 4 = r4 & (heptatonic_pythagorean_scale (HPS,frequency)) . 5 = r5 & (heptatonic_pythagorean_scale (HPS,frequency)) . 6 = r6 & (heptatonic_pythagorean_scale (HPS,frequency)) . 7 = r7 & (heptatonic_pythagorean_scale (HPS,frequency)) . 8 = r8 & r2 / r91 = 9 / 8 & r3 / r2 = 9 / 8 & r4 / r3 = 256 / 243 & r5 / r4 = 9 / 8 & r6 / r5 = 9 / 8 & r7 / r6 = 9 / 8 & r8 / r7 = 256 / 243 )
take r92 ; :: thesis: ex r3, r4, r5, r6, r7, r8 being positive Real st
( (heptatonic_pythagorean_scale (HPS,frequency)) . 1 = r91 & (heptatonic_pythagorean_scale (HPS,frequency)) . 2 = r92 & (heptatonic_pythagorean_scale (HPS,frequency)) . 3 = r3 & (heptatonic_pythagorean_scale (HPS,frequency)) . 4 = r4 & (heptatonic_pythagorean_scale (HPS,frequency)) . 5 = r5 & (heptatonic_pythagorean_scale (HPS,frequency)) . 6 = r6 & (heptatonic_pythagorean_scale (HPS,frequency)) . 7 = r7 & (heptatonic_pythagorean_scale (HPS,frequency)) . 8 = r8 & r92 / r91 = 9 / 8 & r3 / r92 = 9 / 8 & r4 / r3 = 256 / 243 & r5 / r4 = 9 / 8 & r6 / r5 = 9 / 8 & r7 / r6 = 9 / 8 & r8 / r7 = 256 / 243 )
take r93 ; :: thesis: ex r4, r5, r6, r7, r8 being positive Real st
( (heptatonic_pythagorean_scale (HPS,frequency)) . 1 = r91 & (heptatonic_pythagorean_scale (HPS,frequency)) . 2 = r92 & (heptatonic_pythagorean_scale (HPS,frequency)) . 3 = r93 & (heptatonic_pythagorean_scale (HPS,frequency)) . 4 = r4 & (heptatonic_pythagorean_scale (HPS,frequency)) . 5 = r5 & (heptatonic_pythagorean_scale (HPS,frequency)) . 6 = r6 & (heptatonic_pythagorean_scale (HPS,frequency)) . 7 = r7 & (heptatonic_pythagorean_scale (HPS,frequency)) . 8 = r8 & r92 / r91 = 9 / 8 & r93 / r92 = 9 / 8 & r4 / r93 = 256 / 243 & r5 / r4 = 9 / 8 & r6 / r5 = 9 / 8 & r7 / r6 = 9 / 8 & r8 / r7 = 256 / 243 )
take r94 ; :: thesis: ex r5, r6, r7, r8 being positive Real st
( (heptatonic_pythagorean_scale (HPS,frequency)) . 1 = r91 & (heptatonic_pythagorean_scale (HPS,frequency)) . 2 = r92 & (heptatonic_pythagorean_scale (HPS,frequency)) . 3 = r93 & (heptatonic_pythagorean_scale (HPS,frequency)) . 4 = r94 & (heptatonic_pythagorean_scale (HPS,frequency)) . 5 = r5 & (heptatonic_pythagorean_scale (HPS,frequency)) . 6 = r6 & (heptatonic_pythagorean_scale (HPS,frequency)) . 7 = r7 & (heptatonic_pythagorean_scale (HPS,frequency)) . 8 = r8 & r92 / r91 = 9 / 8 & r93 / r92 = 9 / 8 & r94 / r93 = 256 / 243 & r5 / r94 = 9 / 8 & r6 / r5 = 9 / 8 & r7 / r6 = 9 / 8 & r8 / r7 = 256 / 243 )
take r95 ; :: thesis: ex r6, r7, r8 being positive Real st
( (heptatonic_pythagorean_scale (HPS,frequency)) . 1 = r91 & (heptatonic_pythagorean_scale (HPS,frequency)) . 2 = r92 & (heptatonic_pythagorean_scale (HPS,frequency)) . 3 = r93 & (heptatonic_pythagorean_scale (HPS,frequency)) . 4 = r94 & (heptatonic_pythagorean_scale (HPS,frequency)) . 5 = r95 & (heptatonic_pythagorean_scale (HPS,frequency)) . 6 = r6 & (heptatonic_pythagorean_scale (HPS,frequency)) . 7 = r7 & (heptatonic_pythagorean_scale (HPS,frequency)) . 8 = r8 & r92 / r91 = 9 / 8 & r93 / r92 = 9 / 8 & r94 / r93 = 256 / 243 & r95 / r94 = 9 / 8 & r6 / r95 = 9 / 8 & r7 / r6 = 9 / 8 & r8 / r7 = 256 / 243 )
take r96 ; :: thesis: ex r7, r8 being positive Real st
( (heptatonic_pythagorean_scale (HPS,frequency)) . 1 = r91 & (heptatonic_pythagorean_scale (HPS,frequency)) . 2 = r92 & (heptatonic_pythagorean_scale (HPS,frequency)) . 3 = r93 & (heptatonic_pythagorean_scale (HPS,frequency)) . 4 = r94 & (heptatonic_pythagorean_scale (HPS,frequency)) . 5 = r95 & (heptatonic_pythagorean_scale (HPS,frequency)) . 6 = r96 & (heptatonic_pythagorean_scale (HPS,frequency)) . 7 = r7 & (heptatonic_pythagorean_scale (HPS,frequency)) . 8 = r8 & r92 / r91 = 9 / 8 & r93 / r92 = 9 / 8 & r94 / r93 = 256 / 243 & r95 / r94 = 9 / 8 & r96 / r95 = 9 / 8 & r7 / r96 = 9 / 8 & r8 / r7 = 256 / 243 )
take r97 ; :: thesis: ex r8 being positive Real st
( (heptatonic_pythagorean_scale (HPS,frequency)) . 1 = r91 & (heptatonic_pythagorean_scale (HPS,frequency)) . 2 = r92 & (heptatonic_pythagorean_scale (HPS,frequency)) . 3 = r93 & (heptatonic_pythagorean_scale (HPS,frequency)) . 4 = r94 & (heptatonic_pythagorean_scale (HPS,frequency)) . 5 = r95 & (heptatonic_pythagorean_scale (HPS,frequency)) . 6 = r96 & (heptatonic_pythagorean_scale (HPS,frequency)) . 7 = r97 & (heptatonic_pythagorean_scale (HPS,frequency)) . 8 = r8 & r92 / r91 = 9 / 8 & r93 / r92 = 9 / 8 & r94 / r93 = 256 / 243 & r95 / r94 = 9 / 8 & r96 / r95 = 9 / 8 & r97 / r96 = 9 / 8 & r8 / r97 = 256 / 243 )
A1: ex fr being positive Real st
( frequency = fr & Octave (HPS,frequency) = 2 * fr ) by Def15;
A2: ( (heptatonic_pythagorean_scale (HPS,frequency)) . 1 = 1 * (@ frequency) & (heptatonic_pythagorean_scale (HPS,frequency)) . 2 = (9 / 8) * (@ frequency) & (heptatonic_pythagorean_scale (HPS,frequency)) . 3 = (81 / 64) * (@ frequency) & (heptatonic_pythagorean_scale (HPS,frequency)) . 4 = (4 / 3) * (@ frequency) & (heptatonic_pythagorean_scale (HPS,frequency)) . 5 = (3 / 2) * (@ frequency) & (heptatonic_pythagorean_scale (HPS,frequency)) . 6 = (27 / 16) * (@ frequency) & (heptatonic_pythagorean_scale (HPS,frequency)) . 7 = (243 / 128) * (@ frequency) & (heptatonic_pythagorean_scale (HPS,frequency)) . 8 = 2 * (@ frequency) ) by Th88;
( 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) & hepta_octave (HPS,frequency) = 2 * (@ frequency) ) by Th88, A1;
then ( (heptatonic_pythagorean_scale (HPS,frequency)) . 1 = r91 & (heptatonic_pythagorean_scale (HPS,frequency)) . 2 = r92 & (heptatonic_pythagorean_scale (HPS,frequency)) . 3 = r93 & (heptatonic_pythagorean_scale (HPS,frequency)) . 4 = r94 & (heptatonic_pythagorean_scale (HPS,frequency)) . 5 = r95 & (heptatonic_pythagorean_scale (HPS,frequency)) . 6 = r96 & (heptatonic_pythagorean_scale (HPS,frequency)) . 7 = r97 & (heptatonic_pythagorean_scale (HPS,frequency)) . 8 = r98 ) by Th88;
then ( r92 / r91 = 9 / 8 & r93 / r92 = 9 / 8 & r94 / r93 = 256 / 243 & r95 / r94 = 9 / 8 & r96 / r95 = 9 / 8 & r97 / r96 = 9 / 8 & r98 / r97 = 256 / 243 ) by Lem89;
hence ex r8 being positive Real st
( (heptatonic_pythagorean_scale (HPS,frequency)) . 1 = r91 & (heptatonic_pythagorean_scale (HPS,frequency)) . 2 = r92 & (heptatonic_pythagorean_scale (HPS,frequency)) . 3 = r93 & (heptatonic_pythagorean_scale (HPS,frequency)) . 4 = r94 & (heptatonic_pythagorean_scale (HPS,frequency)) . 5 = r95 & (heptatonic_pythagorean_scale (HPS,frequency)) . 6 = r96 & (heptatonic_pythagorean_scale (HPS,frequency)) . 7 = r97 & (heptatonic_pythagorean_scale (HPS,frequency)) . 8 = r8 & r92 / r91 = 9 / 8 & r93 / r92 = 9 / 8 & r94 / r93 = 256 / 243 & r95 / r94 = 9 / 8 & r96 / r95 = 9 / 8 & r97 / r96 = 9 / 8 & r8 / r97 = 256 / 243 ) by A1, A2; :: thesis: verum