let MS be MusicSpace; :: thesis: for 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) = 2 * r1 & not Fifth (MS,f2) is_Between f1, Octave (MS,f1) )
let f1, f2 be Element of MS; :: thesis: for r1, r2 being positive Real st f1 = r1 & f2 = r2 & r2 = (4 / 3) * r1 holds
( Fifth (MS,f2) = 2 * r1 & not Fifth (MS,f2) is_Between f1, Octave (MS,f1) )
let r1, r2 be positive Real; :: thesis: ( f1 = r1 & f2 = r2 & r2 = (4 / 3) * r1 implies ( Fifth (MS,f2) = 2 * r1 & not Fifth (MS,f2) is_Between f1, Octave (MS,f1) ) )
assume that
A1: f1 = r1 and
A2: f2 = r2 and
A3: r2 = (4 / 3) * r1 ; :: thesis: ( Fifth (MS,f2) = 2 * r1 & not Fifth (MS,f2) is_Between f1, Octave (MS,f1) )
A4: ex fr being positive Real st
( f2 = fr & Fifth (MS,f2) = (3 / 2) * fr ) by Def12;
hence Fifth (MS,f2) = 2 * r1 by A2, A3; :: thesis: not Fifth (MS,f2) is_Between f1, Octave (MS,f1)
ex fr being positive Real st
( f1 = fr & Octave (MS,f1) = 2 * fr ) by Def15;
hence not Fifth (MS,f2) is_Between f1, Octave (MS,f1) by A4, A3, A2, A1; :: thesis: verum