set MS = REAL_Music ;
now for frequency being Element of REAL_Music
for n being non zero Nat ex fr being positive Real st
( frequency = fr & n -harmonique (REAL_Music,frequency) = n * fr )let frequency be
Element of
REAL_Music;
for n being non zero Nat ex fr being positive Real st
( frequency = fr & n -harmonique (REAL_Music,frequency) = n * fr )let n be non
zero Nat;
ex fr being positive Real st
( frequency = fr & n -harmonique (REAL_Music,frequency) = n * fr )reconsider fr =
frequency as
positive Real by Th1;
take fr =
fr;
( frequency = fr & n -harmonique (REAL_Music,frequency) = n * fr )thus
frequency = fr
;
n -harmonique (REAL_Music,frequency) = n * frreconsider n1 = 1,
n2 =
n as
Element of
REAL_Music by Th20;
reconsider f2 =
n * fr as
Element of
REAL_Music by Th1;
reconsider x =
[n1,n2],
y =
[frequency,f2] as
Element of
[:REALPLUS,REALPLUS:] ;
now ( [frequency,(n -harmonique (REAL_Music,frequency))] in Class ( the Equidistance of REAL_Music,[1,n]) & [frequency,f2] in Class ( the Equidistance of REAL_Music,[1,n]) )thus
[frequency,(n -harmonique (REAL_Music,frequency))] in Class ( the
Equidistance of
REAL_Music,
[1,n])
by Def08b;
[frequency,f2] in Class ( the Equidistance of REAL_Music,[1,n])now ( the Ratio of REAL_Music . (n1,n2) = REAL_ratio . (n1,n2) & the Ratio of REAL_Music . (frequency,f2) = REAL_ratio . (frequency,f2) & REAL_ratio . (n1,n2) = REAL_ratio . (frequency,f2) )thus
the
Ratio of
REAL_Music . (
n1,
n2)
= REAL_ratio . (
n1,
n2)
;
( the Ratio of REAL_Music . (frequency,f2) = REAL_ratio . (frequency,f2) & REAL_ratio . (n1,n2) = REAL_ratio . (frequency,f2) )thus
the
Ratio of
REAL_Music . (
frequency,
f2)
= REAL_ratio . (
frequency,
f2)
;
REAL_ratio . (n1,n2) = REAL_ratio . (frequency,f2)now ( REAL_ratio . (n1,n2) = n & REAL_ratio . (frequency,f2) = n )reconsider n19 =
n1,
n29 =
n2,
fr9 =
fr,
f29 =
f2 as
Element of
REALPLUS ;
consider r,
s being
positive Real such that A1:
(
n19 = r &
n29 = s &
REAL_ratio (
n19,
n29)
= s / r )
by Def01;
consider r9,
s9 being
positive Real such that A2:
(
fr9 = r9 &
f29 = s9 &
REAL_ratio (
fr9,
f29)
= s9 / r9 )
by Def01;
consider y9,
z9 being
Element of
REALPLUS such that A3:
x = [y9,z9]
and A4:
REAL_ratio . x = REAL_ratio (
y9,
z9)
by Def02;
consider y99,
z99 being
Element of
REALPLUS such that A5:
y = [y99,z99]
and A6:
REAL_ratio . y = REAL_ratio (
y99,
z99)
by Def02;
A7:
(
y9 = n1 &
z9 = n2 &
y99 = frequency &
z99 = f2 )
by A3, A5, XTUPLE_0:1;
hence
REAL_ratio . (
n1,
n2)
= n
by A1, A4, BINOP_1:def 1;
REAL_ratio . (frequency,f2) = nthus REAL_ratio . (
frequency,
f2) =
s9 / r9
by A2, A7, A6, BINOP_1:def 1
.=
n
by A2, XCMPLX_1:89
;
verum end; hence
REAL_ratio . (
n1,
n2)
= REAL_ratio . (
frequency,
f2)
;
verum end; then
n1,
n2 equiv frequency,
f2
by Def08a;
hence
[frequency,f2] in Class ( the
Equidistance of
REAL_Music,
[1,n])
by EQREL_1:18;
verum end; hence
n -harmonique (
REAL_Music,
frequency)
= n * fr
by Def08b;
verum end;
hence
REAL_Music is satisfying_linearite_harmonique
; verum