let f1, f2, fn1, fm1, fn2, fm2 be Element of REAL_Music; for r1, r2 being positive Real
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 Real; 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 A0:
(
fn1 = n * r1 &
fm1 = m * r1 &
fn2 = n * r2 &
fm2 = m * r2 )
;
fn1,fm1 equiv fn2,fm2reconsider z =
[fn1,fm1] 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;
consider r,
s being
positive Real such that A3:
(
x9 = r &
s = y9 &
REAL_ratio (
x9,
y9)
= s / r )
by Def01;
reconsider z9 =
[fn2,fm2] as
Element of
[:REALPLUS,REALPLUS:] by ZFMISC_1:def 2;
consider x99,
y99 being
Element of
REALPLUS such that A4:
z9 = [x99,y99]
and A5:
REAL_ratio . z9 = REAL_ratio (
x99,
y99)
by Def02;
consider r9,
s9 being
positive Real such that A6:
(
x99 = r9 &
s9 = y99 &
REAL_ratio (
x99,
y99)
= s9 / r9 )
by Def01;
now ( REAL_ratio . (fn1,fm1) = s / r & REAL_ratio . (fn2,fm2) = s9 / r9 & s / r = s9 / r9 )thus
REAL_ratio . (
fn1,
fm1)
= s / r
by A3, A2, BINOP_1:def 1;
( REAL_ratio . (fn2,fm2) = s9 / r9 & s / r = s9 / r9 )thus
REAL_ratio . (
fn2,
fm2)
= s9 / r9
by A6, A5, BINOP_1:def 1;
s / r = s9 / r9
(
r = n * r1 &
s = m * r1 &
r9 = n * r2 &
s9 = m * r2 )
by A4, A6, A1, A3, A0, 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 Th7;
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