set S = REAL_Music ;
now for frequency being Element of REAL_Music
for n being non zero Nat ex harmonique being Element of REAL_Music st [frequency,harmonique] in Class ( the Equidistance of REAL_Music,[1,n])let frequency be
Element of
REAL_Music;
for n being non zero Nat ex harmonique being Element of REAL_Music st [frequency,harmonique] in Class ( the Equidistance of REAL_Music,[1,n])let n be non
zero Nat;
ex harmonique being Element of REAL_Music st [frequency,harmonique] in Class ( the Equidistance of REAL_Music,[1,n])reconsider f =
frequency as
positive Real by Th1;
reconsider harmonique =
n * f as
Element of
REAL_Music by Th1;
take harmonique =
harmonique;
[frequency,harmonique] in Class ( the Equidistance of REAL_Music,[1,n])reconsider x = 1,
y =
n as
Element of
REAL_Music by Th1;
reconsider z =
[x,y] as
Element of
[:REALPLUS,REALPLUS:] by ZFMISC_1:def 2;
consider x9,
y9 being
Element of
REALPLUS such that A1:
z = [x9,y9]
and A2:
REAL_ratio . z = REAL_ratio (
x9,
y9)
by Def02;
reconsider z9 =
[frequency,harmonique] as
Element of
[:REALPLUS,REALPLUS:] by ZFMISC_1:def 2;
consider x99,
y99 being
Element of
REALPLUS such that A3:
z9 = [x99,y99]
and A4:
REAL_ratio . z9 = REAL_ratio (
x99,
y99)
by Def02;
consider r,
s being
positive Real such that A5:
(
x9 = r &
s = y9 &
REAL_ratio (
x9,
y9)
= s / r )
by Def01;
A6:
(
r = 1 &
s = n )
by A5, A1, XTUPLE_0:1;
consider r9,
s9 being
positive Real such that A7:
(
x99 = r9 &
s9 = y99 &
REAL_ratio (
x99,
y99)
= s9 / r9 )
by Def01;
A8:
(
r9 = frequency &
s9 = harmonique )
by A7, A3, XTUPLE_0:1;
now ( the Ratio of REAL_Music . (x,y) = n & the Ratio of REAL_Music . (frequency,harmonique) = n )thus
the
Ratio of
REAL_Music . (
x,
y)
= n
by A5, A6, A2, BINOP_1:def 1;
the Ratio of REAL_Music . (frequency,harmonique) = nthus the
Ratio of
REAL_Music . (
frequency,
harmonique) =
REAL_ratio (
x99,
y99)
by A4, BINOP_1:def 1
.=
n
by A7, A8, XCMPLX_1:89
;
verum end; then
x,
y equiv frequency,
harmonique
by Th7;
hence
[frequency,harmonique] in Class ( the
Equidistance of
REAL_Music,
[1,n])
by EQREL_1:18;
verum end;
hence
for frequency being Element of REAL_Music
for n being non zero Nat ex harmonique being Element of REAL_Music st [frequency,harmonique] in Class ( the Equidistance of REAL_Music,[1,n])
; verum