let f1, f2, fn1, fm1, fn2, fm2 be Element of RAT_Music; for r1, r2 being positive Rational
for n, m being non zero Nat st fn1 = n * r1 & fm1 = m * r1 & fn2 = n * r2 & fm2 = m * r2 holds
fn1,fm1 equiv fn2,fm2
let r1, r2 be positive Rational; for n, m being non zero Nat st fn1 = n * r1 & fm1 = m * r1 & fn2 = n * r2 & fm2 = m * r2 holds
fn1,fm1 equiv fn2,fm2
now for n, m being non zero Nat st fn1 = n * r1 & fm1 = m * r1 & fn2 = n * r2 & fm2 = m * r2 holds
fn1,fm1 equiv fn2,fm2let n,
m be non
zero Nat;
( fn1 = n * r1 & fm1 = m * r1 & fn2 = n * r2 & fm2 = m * r2 implies fn1,fm1 equiv fn2,fm2 )assume A1:
(
fn1 = n * r1 &
fm1 = m * r1 &
fn2 = n * r2 &
fm2 = m * r2 )
;
fn1,fm1 equiv fn2,fm2reconsider z =
[fn1,fm1] as
Element of
[:RATPLUS,RATPLUS:] by ZFMISC_1:def 2;
consider x9,
y9 being
Element of
RATPLUS such that A2:
z = [x9,y9]
and A3:
RAT_ratio . z = RAT_ratio (
x9,
y9)
by Def05;
consider r,
s being
positive Rational such that A4:
(
x9 = r &
s = y9 &
RAT_ratio (
x9,
y9)
= s / r )
by Def04;
reconsider z9 =
[fn2,fm2] as
Element of
[:RATPLUS,RATPLUS:] by ZFMISC_1:def 2;
consider x99,
y99 being
Element of
RATPLUS such that A5:
z9 = [x99,y99]
and A6:
RAT_ratio . z9 = RAT_ratio (
x99,
y99)
by Def05;
consider r9,
s9 being
positive Rational such that A7:
(
x99 = r9 &
s9 = y99 &
RAT_ratio (
x99,
y99)
= s9 / r9 )
by Def04;
now ( RAT_ratio . (fn1,fm1) = s / r & RAT_ratio . (fn2,fm2) = s9 / r9 & s / r = s9 / r9 )thus
RAT_ratio . (
fn1,
fm1)
= s / r
by A3, A4, BINOP_1:def 1;
( RAT_ratio . (fn2,fm2) = s9 / r9 & s / r = s9 / r9 )thus
RAT_ratio . (
fn2,
fm2)
= s9 / r9
by A6, A7, BINOP_1:def 1;
s / r = s9 / r9
(
r = n * r1 &
s = m * r1 &
r9 = n * r2 &
s9 = m * r2 )
by A1, A2, A4, A5, A7, XTUPLE_0:1;
then
(
s / r = m / n &
s9 / r9 = m / n )
by XCMPLX_1:91;
hence
s / r = s9 / r9
;
verum end; hence
fn1,
fm1 equiv fn2,
fm2
by Th14;
verum end;
hence
for n, m being non zero Nat st fn1 = n * r1 & fm1 = m * r1 & fn2 = n * r2 & fm2 = m * r2 holds
fn1,fm1 equiv fn2,fm2
; verum