let MS be satisfying_equiv satisfying_interval satisfying_Nat satisfying_harmonic_closed satisfying_linearite_harmonique satisfying_harmonique_stable satisfying_fifth_constructible MusicStruct ; for frequency being Element of MS holds fifth (MS,frequency) = fifth MS
let frequency be Element of MS; fifth (MS,frequency) = fifth MS
A0:
now for x being object st x in fifth (MS,frequency) holds
x in fifth MSlet x be
object ;
( x in fifth (MS,frequency) implies x in fifth MS )assume A1:
x in fifth (
MS,
frequency)
;
x in fifth MSthen consider x1,
x2 being
object such that A2:
x1 in the
carrier of
MS
and A3:
x2 in the
carrier of
MS
and A4:
x = [x1,x2]
by ZFMISC_1:def 2;
reconsider x1 =
x1,
x2 =
x2 as
Element of
MS by A2, A3;
reconsider y = 1,
y1 = 2,
y2 = 3 as
Element of
MS by Th20;
set z = 2
-harmonique (
MS,
frequency);
set t = 3
-harmonique (
MS,
frequency);
reconsider n = 2,
m = 3 as non
zero Nat ;
consider r1 being
positive Real such that A5:
y = r1
and A6:
n -harmonique (
MS,
y)
= n * r1
by Def09;
consider r2 being
positive Real such that A7:
y = r2
and A8:
m -harmonique (
MS,
y)
= m * r2
by Def09;
set a =
n -harmonique (
MS,
frequency);
set b =
m -harmonique (
MS,
frequency);
A9:
n -harmonique (
MS,
frequency),
m -harmonique (
MS,
frequency)
equiv x1,
x2
by A1, A4, EQREL_1:18;
y1,
y2 equiv n -harmonique (
MS,
frequency),
m -harmonique (
MS,
frequency)
by A5, A6, A7, A8, Def10;
then
y1,
y2 equiv x1,
x2
by A9, Th23;
hence
x in fifth MS
by A4, EQREL_1:18;
verum end;
now for x being object st x in fifth MS holds
x in fifth (MS,frequency)let x be
object ;
( x in fifth MS implies x in fifth (MS,frequency) )assume A11:
x in fifth MS
;
x in fifth (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;
reconsider y = 2,
z = 3 as
Element of
MS by Th20;
reconsider y9 =
y as
positive Real ;
reconsider n = 2,
m = 3 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);
A15:
n -harmonique (
MS,
frequency),
m -harmonique (
MS,
frequency)
equiv n -harmonique (
MS,
y),
m -harmonique (
MS,
y)
by Def10;
reconsider n0 = 1,
n1 = 2,
n2 = 3 as
Element of
MS by Th20;
consider r1 being
positive Real such that A16:
n0 = r1
and A17:
n -harmonique (
MS,
n0)
= n * r1
by Def09;
consider r2 being
positive Real such that A18:
n0 = r2
and A19:
m -harmonique (
MS,
n0)
= m * r2
by Def09;
A20:
n -harmonique (
MS,
n0),
m -harmonique (
MS,
n0)
equiv x1,
x2
by A16, A17, A18, A19, A11, A14, EQREL_1:18;
n -harmonique (
MS,
y),
m -harmonique (
MS,
y)
equiv n -harmonique (
MS,
n0),
m -harmonique (
MS,
n0)
by Def10;
then
n -harmonique (
MS,
y),
m -harmonique (
MS,
y)
equiv x1,
x2
by A20, Th23;
then
n -harmonique (
MS,
frequency),
m -harmonique (
MS,
frequency)
equiv x1,
x2
by A15, Th23;
hence
x in fifth (
MS,
frequency)
by A14, EQREL_1:18;
verum end;
hence
fifth (MS,frequency) = fifth MS
by A0; verum