let HPS be Heptatonic_Pythagorean_Score; for frequency being Element of HPS holds heptatonic_pythagorean_scale (HPS,frequency) is heptatonic
let frequency be Element of HPS; heptatonic_pythagorean_scale (HPS,frequency) is heptatonic
set MS = HPS;
set gamme = heptatonic_pythagorean_scale (HPS,frequency);
now ( ex 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 & r1 < r2 & r2 < r3 & r3 < r4 & r4 < r5 & r5 < r6 & r6 < r7 & r7 < r8 ) & (heptatonic_pythagorean_scale (HPS,frequency)) . 8 = Octave (HPS,frequency) & (heptatonic_pythagorean_scale (HPS,frequency)) . 1 = frequency )now ex r1, r2, r3, r4, r5, r6, r7, r8 being positive Real st
( (heptatonic_pythagorean_scale (HPS,frequency)) . 1 = frequency & (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 & r1 < r2 & r2 < r3 & r3 < r4 & r4 < r5 & r5 < r6 & r6 < r7 & r7 < r8 )reconsider r1 = 1
* (@ frequency),
r2 =
(9 / 8) * (@ frequency),
r3 =
(81 / 64) * (@ frequency),
r4 =
(4 / 3) * (@ frequency),
r5 =
(3 / 2) * (@ frequency),
r6 =
(27 / 16) * (@ frequency),
r7 =
(243 / 128) * (@ frequency),
r8 = 2
* (@ frequency) as
positive Real ;
take r1 =
r1;
ex r2, r3, r4, r5, r6, r7, r8 being positive Real st
( (heptatonic_pythagorean_scale (HPS,frequency)) . 1 = frequency & (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 & r1 < r2 & r2 < r3 & r3 < r4 & r4 < r5 & r5 < r6 & r6 < r7 & r7 < r8 )take r2 =
r2;
ex r3, r4, r5, r6, r7, r8 being positive Real st
( (heptatonic_pythagorean_scale (HPS,frequency)) . 1 = frequency & (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 & r1 < r2 & r2 < r3 & r3 < r4 & r4 < r5 & r5 < r6 & r6 < r7 & r7 < r8 )take r3 =
r3;
ex r4, r5, r6, r7, r8 being positive Real st
( (heptatonic_pythagorean_scale (HPS,frequency)) . 1 = frequency & (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 & r1 < r2 & r2 < r3 & r3 < r4 & r4 < r5 & r5 < r6 & r6 < r7 & r7 < r8 )take r4 =
r4;
ex r5, r6, r7, r8 being positive Real st
( (heptatonic_pythagorean_scale (HPS,frequency)) . 1 = frequency & (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 & r1 < r2 & r2 < r3 & r3 < r4 & r4 < r5 & r5 < r6 & r6 < r7 & r7 < r8 )take r5 =
r5;
ex r6, r7, r8 being positive Real st
( (heptatonic_pythagorean_scale (HPS,frequency)) . 1 = frequency & (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 & r1 < r2 & r2 < r3 & r3 < r4 & r4 < r5 & r5 < r6 & r6 < r7 & r7 < r8 )take r6 =
r6;
ex r7, r8 being positive Real st
( (heptatonic_pythagorean_scale (HPS,frequency)) . 1 = frequency & (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 & r1 < r2 & r2 < r3 & r3 < r4 & r4 < r5 & r5 < r6 & r6 < r7 & r7 < r8 )take r7 =
r7;
ex r8 being positive Real st
( (heptatonic_pythagorean_scale (HPS,frequency)) . 1 = frequency & (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 & r1 < r2 & r2 < r3 & r3 < r4 & r4 < r5 & r5 < r6 & r6 < r7 & r7 < r8 )take r8 =
r8;
( (heptatonic_pythagorean_scale (HPS,frequency)) . 1 = frequency & (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 & r1 < r2 & r2 < r3 & r3 < r4 & r4 < r5 & r5 < r6 & r6 < r7 & r7 < r8 )
(
(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;
hence
(
(heptatonic_pythagorean_scale (HPS,frequency)) . 1
= frequency &
(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 )
;
( r1 < r2 & r2 < r3 & r3 < r4 & r4 < r5 & r5 < r6 & r6 < r7 & r7 < r8 )thus
(
r1 < r2 &
r2 < r3 &
r3 < r4 &
r4 < r5 &
r5 < r6 &
r6 < r7 &
r7 < r8 )
by XREAL_1:98;
verum end; hence
ex
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 &
r1 < r2 &
r2 < r3 &
r3 < r4 &
r4 < r5 &
r5 < r6 &
r6 < r7 &
r7 < r8 )
;
( (heptatonic_pythagorean_scale (HPS,frequency)) . 8 = Octave (HPS,frequency) & (heptatonic_pythagorean_scale (HPS,frequency)) . 1 = frequency )A1:
ex
fr being
positive Real st
(
frequency = fr &
Octave (
HPS,
frequency)
= 2
* fr )
by Def15;
(
(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;
hence
(
(heptatonic_pythagorean_scale (HPS,frequency)) . 8
= Octave (
HPS,
frequency) &
(heptatonic_pythagorean_scale (HPS,frequency)) . 1
= frequency )
by A1;
verum
hence
heptatonic_pythagorean_scale (HPS,frequency) is heptatonic
; verum