let MS be non empty satisfying_Real satisfying_equiv satisfying_interval satisfying_commutativity satisfying_Nat satisfying_harmonic_closed satisfying_fifth_constructible classical_fifth satisfying_octave_constructible classical_octave satisfying_octave_descendent_constructible MusicStruct ; :: thesis: for fondamentale, frequency being Element of MS st frequency is_Between fondamentale, Octave (MS,fondamentale) holds
Fifth_reduct (MS,fondamentale,frequency) is_Between fondamentale, Octave (MS,fondamentale)
let fondamentale, frequency be Element of MS; :: thesis: ( frequency is_Between fondamentale, Octave (MS,fondamentale) implies Fifth_reduct (MS,fondamentale,frequency) is_Between fondamentale, Octave (MS,fondamentale) )
assume frequency is_Between fondamentale, Octave (MS,fondamentale) ; :: thesis: Fifth_reduct (MS,fondamentale,frequency) is_Between fondamentale, Octave (MS,fondamentale)
then consider r1, r2, r3 being positive Real such that
A1: ( fondamentale = r1 & frequency = r2 & Octave (MS,fondamentale) = 2 * r1 & r1 <= r2 & r2 <= 2 * r1 ) by Th55;
consider fr being positive Real such that
A2: ( frequency = fr & Fifth (MS,frequency) = (3 / 2) * fr ) by Def12;

per cases ( Fifth (MS,frequency) is_Between fondamentale, Octave (MS,fondamentale) or not Fifth (MS,frequency) is_Between fondamentale, Octave (MS,fondamentale) ) ;

suppose Fifth (MS,frequency) is_Between fondamentale, Octave (MS,fondamentale) ; :: thesis: Fifth_reduct (MS,fondamentale,frequency) is_Between fondamentale, Octave (MS,fondamentale)

hence Fifth_reduct (MS,fondamentale,frequency) is_Between fondamentale, Octave (MS,fondamentale) by Def18; :: thesis: verum

end;

suppose A3: not Fifth (MS,frequency) is_Between fondamentale, Octave (MS,fondamentale) ; :: thesis: Fifth_reduct (MS,fondamentale,frequency) is_Between fondamentale, Octave (MS,fondamentale)

A4: ex r being positive Real st
( Fifth (MS,frequency) = r & Octave_descendent (MS,(Fifth (MS,frequency))) = r / 2 ) by Th51;

per cases ( (3 / 2) * r2 < r1 or 2 * r1 <= (3 / 2) * r2 ) by A2, A1, A3;

suppose A5: (3 / 2) * r2 < r1 ; :: thesis: Fifth_reduct (MS,fondamentale,frequency) is_Between fondamentale, Octave (MS,fondamentale)

reconsider r32 = 3 / 2 as non zero positive Real ;
r1 * (1 / r32) < 1 * r1 by XREAL_1:68;
then A6: r1 / r32 < r1 by XCMPLX_1:99;
(r32 * r2) / r32 < r1 / r32 by A5, XREAL_1:74;
then r2 < r1 / r32 by XCMPLX_1:89;
hence Fifth_reduct (MS,fondamentale,frequency) is_Between fondamentale, Octave (MS,fondamentale) by A1, A6, XXREAL_0:2; :: thesis: verum

end;

suppose 2 * r1 <= (3 / 2) * r2 ; :: thesis: Fifth_reduct (MS,fondamentale,frequency) is_Between fondamentale, Octave (MS,fondamentale)

then A7: (2 * r1) / 2 <= ((3 / 2) * r2) / 2 by XREAL_1:72;
reconsider r34 = 3 / 4 as positive Real ;
A8: (3 / 2) * r1 < 2 * r1 by XREAL_1:68;
(3 / 4) * r2 <= (3 / 4) * (2 * r1) by A1, XREAL_1:66;
then (3 / 4) * r2 < 2 * r1 by A8, XXREAL_0:2;
hence Fifth_reduct (MS,fondamentale,frequency) is_Between fondamentale, Octave (MS,fondamentale) by A2, A7, A1, A4, A3, Def18; :: thesis: verum

end;

end;

end;

end;