let MS be satisfying_equiv satisfying_interval satisfying_tonic satisfying_Nat satisfying_harmonic_closed satisfying_linearite_harmonique satisfying_harmonique_stable MusicStruct ; for frequency being Element of MS holds octave (MS,frequency) = octave MS
let frequency be Element of MS; octave (MS,frequency) = octave MS
A1:
now for x being object st x in octave (MS,frequency) holds
x in octave MSlet x be
object ;
( x in octave (MS,frequency) implies x in octave MS )assume A2:
x in octave (
MS,
frequency)
;
x in octave MSthen consider x1,
x2 being
object such that A3:
x1 in the
carrier of
MS
and A4:
x2 in the
carrier of
MS
and A5:
x = [x1,x2]
by ZFMISC_1:def 2;
reconsider x1 =
x1,
x2 =
x2 as
Element of
MS by A3, A4;
A6:
NATPLUS c= the
carrier of
MS
by Def12a;
( 1
in NATPLUS & 2
in NATPLUS )
by NAT_LAT:def 6;
then reconsider y1 = 1,
y2 = 2 as
Element of
MS by A6;
set z = 1
-harmonique (
MS,
frequency);
set t = 2
-harmonique (
MS,
frequency);
reconsider n = 1,
m = 2 as non
zero Nat ;
consider r2 being
positive Real such that A7:
y1 = r2
and A8:
m -harmonique (
MS,
y1)
= m * r2
by Def09;
set a =
n -harmonique (
MS,
frequency);
set b =
m -harmonique (
MS,
frequency);
A9:
y1 = n -harmonique (
MS,
y1)
by Th40;
A10:
n -harmonique (
MS,
frequency),
m -harmonique (
MS,
frequency)
equiv x1,
x2
by A2, A5, EQREL_1:18;
y1,
y2 equiv n -harmonique (
MS,
frequency),
m -harmonique (
MS,
frequency)
by A9, A7, A8, Def10;
then
y1,
y2 equiv x1,
x2
by A10, Th23;
hence
x in octave MS
by A5, EQREL_1:18;
verum end;
now for x being object st x in octave MS holds
x in octave (MS,frequency)let x be
object ;
( x in octave MS implies x in octave (MS,frequency) )assume A11:
x in octave MS
;
x in octave (MS,frequency)then consider x1,
x2 being
object such that A12:
x1 in the
carrier of
MS
and A13:
x2 in the
carrier of
MS
and A14:
x = [x1,x2]
by ZFMISC_1:def 2;
reconsider x1 =
x1,
x2 =
x2 as
Element of
MS by A12, A13;
A15:
NATPLUS c= the
carrier of
MS
by Def12a;
( 1
in NATPLUS & 2
in NATPLUS )
by NAT_LAT:def 6;
then reconsider y = 1,
z = 2 as
Element of
MS by A15;
reconsider y9 =
y as
positive Real ;
reconsider n = 1,
m = 2 as non
zero Nat ;
set a =
n -harmonique (
MS,
frequency);
set b =
m -harmonique (
MS,
frequency);
set c =
n -harmonique (
MS,
y);
set d =
m -harmonique (
MS,
y);
A16:
n -harmonique (
MS,
frequency),
m -harmonique (
MS,
frequency)
equiv n -harmonique (
MS,
y),
m -harmonique (
MS,
y)
by Def10;
reconsider n1 = 1,
n2 = 2 as
Element of
MS by Th20;
consider r1 being
positive Real such that A17:
n1 = r1
and A18:
n -harmonique (
MS,
n1)
= n * r1
by Def09;
consider r2 being
positive Real such that A19:
n1 = r2
and A20:
m -harmonique (
MS,
n1)
= m * r2
by Def09;
n1,
n2 equiv x1,
x2
by A11, A14, EQREL_1:18;
then
n -harmonique (
MS,
frequency),
m -harmonique (
MS,
frequency)
equiv x1,
x2
by A16, A17, A18, A19, A20, Th23;
hence
x in octave (
MS,
frequency)
by A14, EQREL_1:18;
verum end;
hence
octave (MS,frequency) = octave MS
by A1; verum