now for frequency being Element of RAT_Music ex f, qr being positive Rational st
( f = frequency & qr = 2 * f & [f,qr] in octave RAT_Music )let frequency be
Element of
RAT_Music;
ex f, qr being positive Rational st
( f = frequency & qr = 2 * f & [f,qr] in octave RAT_Music )reconsider f =
frequency as
positive Rational by Th2;
reconsider qr = 2
* f as
positive Rational ;
reconsider q =
qr as
Element of
RAT_Music by Th2;
take f =
f;
ex qr being positive Rational st
( f = frequency & qr = 2 * f & [f,qr] in octave RAT_Music )take qr =
qr;
( f = frequency & qr = 2 * f & [f,qr] in octave RAT_Music )thus
f = frequency
;
( qr = 2 * f & [f,qr] in octave RAT_Music )thus
qr = 2
* f
;
[f,qr] in octave RAT_Musicreconsider n2 = 1,
n3 = 2 as
Element of
RAT_Music by Th20;
reconsider x =
[n2,n3],
y =
[frequency,q] as
Element of
[:RATPLUS,RATPLUS:] ;
reconsider z =
[frequency,q] as
Element of
[:RATPLUS,RATPLUS:] ;
consider x9,
y9 being
Element of
RATPLUS such that A1:
z = [x9,y9]
and A2:
RAT_ratio . z = RAT_ratio (
x9,
y9)
by Def05;
consider r,
s being
positive Rational such that A3:
(
x9 = r &
s = y9 &
RAT_ratio (
x9,
y9)
= s / r )
by Def04;
consider x99,
y99 being
Element of
RATPLUS such that A4:
x = [x99,y99]
and A5:
RAT_ratio . x = RAT_ratio (
x99,
y99)
by Def05;
consider r9,
s9 being
positive Rational such that A6:
(
x99 = r9 &
s9 = y99 &
RAT_ratio (
x99,
y99)
= s9 / r9 )
by Def04;
A7:
(
n2 = r9 &
n3 = s9 &
r = frequency &
s = q )
by A3, A1, A4, A6, XTUPLE_0:1;
now ( RAT_ratio . (n2,n3) = 2 / 1 & RAT_ratio . (frequency,q) = 2 )thus
RAT_ratio . (
n2,
n3)
= 2
/ 1
by BINOP_1:def 1, A7, A5, A6;
RAT_ratio . (frequency,q) = 2thus RAT_ratio . (
frequency,
q) =
RAT_ratio (
x9,
y9)
by A2, BINOP_1:def 1
.=
2
by A7, A3, XCMPLX_1:89
;
verum end; then
n2,
n3 equiv frequency,
q
by Def08a;
hence
[f,qr] in octave RAT_Music
by EQREL_1:18;
verum end;
hence
for frequency being Element of RAT_Music ex fr, qr being positive Rational st
( fr = frequency & qr = 2 * fr & [fr,qr] in octave RAT_Music )
; verum