let MS be MusicSpace; for fondamentale, f1, f2 being Element of MS
for r1, r2 being positive Real st f1 = r1 & f2 = r2 & r2 = (4 / 3) * r1 holds
( ( Fifth (MS,f2) is_Between fondamentale, Octave (MS,fondamentale) implies Octave_descendent (MS,(Fifth_reduct (MS,fondamentale,f2))) = f1 ) & ( not Fifth (MS,f2) is_Between fondamentale, Octave (MS,fondamentale) implies Fifth_reduct (MS,fondamentale,f2) = f1 ) )
let fondamentale, f1, f2 be Element of MS; for r1, r2 being positive Real st f1 = r1 & f2 = r2 & r2 = (4 / 3) * r1 holds
( ( Fifth (MS,f2) is_Between fondamentale, Octave (MS,fondamentale) implies Octave_descendent (MS,(Fifth_reduct (MS,fondamentale,f2))) = f1 ) & ( not Fifth (MS,f2) is_Between fondamentale, Octave (MS,fondamentale) implies Fifth_reduct (MS,fondamentale,f2) = f1 ) )
let r1, r2 be positive Real; ( f1 = r1 & f2 = r2 & r2 = (4 / 3) * r1 implies ( ( Fifth (MS,f2) is_Between fondamentale, Octave (MS,fondamentale) implies Octave_descendent (MS,(Fifth_reduct (MS,fondamentale,f2))) = f1 ) & ( not Fifth (MS,f2) is_Between fondamentale, Octave (MS,fondamentale) implies Fifth_reduct (MS,fondamentale,f2) = f1 ) ) )
assume that
A1:
( f1 = r1 & f2 = r2 )
and
A2:
r2 = (4 / 3) * r1
; ( ( Fifth (MS,f2) is_Between fondamentale, Octave (MS,fondamentale) implies Octave_descendent (MS,(Fifth_reduct (MS,fondamentale,f2))) = f1 ) & ( not Fifth (MS,f2) is_Between fondamentale, Octave (MS,fondamentale) implies Fifth_reduct (MS,fondamentale,f2) = f1 ) )
thus
( Fifth (MS,f2) is_Between fondamentale, Octave (MS,fondamentale) implies Octave_descendent (MS,(Fifth_reduct (MS,fondamentale,f2))) = f1 )
( not Fifth (MS,f2) is_Between fondamentale, Octave (MS,fondamentale) implies Fifth_reduct (MS,fondamentale,f2) = f1 )proof
assume A3:
Fifth (
MS,
f2)
is_Between fondamentale,
Octave (
MS,
fondamentale)
;
Octave_descendent (MS,(Fifth_reduct (MS,fondamentale,f2))) = f1
A4:
ex
fr being
positive Real st
(
f2 = fr &
Fifth (
MS,
f2)
= (3 / 2) * fr )
by Def12;
ex
r being
positive Real st
(
Fifth_reduct (
MS,
fondamentale,
f2)
= r &
Octave_descendent (
MS,
(Fifth_reduct (MS,fondamentale,f2)))
= r / 2 )
by Th51;
then Octave_descendent (
MS,
(Fifth_reduct (MS,fondamentale,f2))) =
(2 * r1) / 2
by A3, A4, Def18, A1, A2
.=
f1
by A1
;
hence
Octave_descendent (
MS,
(Fifth_reduct (MS,fondamentale,f2)))
= f1
;
verum
end;
thus
( not Fifth (MS,f2) is_Between fondamentale, Octave (MS,fondamentale) implies Fifth_reduct (MS,fondamentale,f2) = f1 )
verumproof
assume A5:
not
Fifth (
MS,
f2)
is_Between fondamentale,
Octave (
MS,
fondamentale)
;
Fifth_reduct (MS,fondamentale,f2) = f1
consider fr being
positive Real such that A6:
(
f2 = fr &
Fifth (
MS,
f2)
= (3 / 2) * fr )
by Def12;
ex
r being
positive Real st
(
Fifth (
MS,
f2)
= r &
Octave_descendent (
MS,
(Fifth (MS,f2)))
= r / 2 )
by Th51;
hence
Fifth_reduct (
MS,
fondamentale,
f2)
= f1
by A1, A2, A6, A5, Def18;
verum
end;