let frequency be Element of RAT_Music; :: thesis: for n being non zero Nat ex harmonique being Element of RAT_Music st [frequency,harmonique] in Class ( the Equidistance of RAT_Music,[1,n])
let n be non zero Nat; :: thesis: ex harmonique being Element of RAT_Music st [frequency,harmonique] in Class ( the Equidistance of RAT_Music,[1,n])
reconsider f = frequency as positive Rational by Th2;
reconsider harmonique = n * f as Element of RAT_Music by Th2;
take harmonique = harmonique; :: thesis: [frequency,harmonique] in Class ( the Equidistance of RAT_Music,[1,n])
reconsider x = 1, y = n as Element of RAT_Music by Th2;
reconsider z = [x,y] as Element of [:RATPLUS,RATPLUS:] by ZFMISC_1:def 2;
consider x9, y9 being Element of RATPLUS such that
A1: z = [x9,y9] and
A2: RAT_ratio . z = RAT_ratio (x9,y9) by Def05;
reconsider z9 = [frequency,harmonique] as Element of [:RATPLUS,RATPLUS:] by ZFMISC_1:def 2;
consider x99, y99 being Element of RATPLUS such that
A3: z9 = [x99,y99] and
A4: RAT_ratio . z9 = RAT_ratio (x99,y99) by Def05;
consider r, s being positive Rational such that
A5: ( x9 = r & s = y9 & RAT_ratio (x9,y9) = s / r ) by Def04;
A6: ( r = 1 & s = n ) by A5, A1, XTUPLE_0:1;
consider r9, s9 being positive Rational such that
A7: ( x99 = r9 & s9 = y99 & RAT_ratio (x99,y99) = s9 / r9 ) by Def04;
A8: ( r9 = frequency & s9 = harmonique ) by A7, A3, XTUPLE_0:1;
then x,y equiv frequency,harmonique by Th14;
hence [frequency,harmonique] in Class ( the Equidistance of RAT_Music,[1,n]) by EQREL_1:18; :: thesis: verum