let t be 1 _greater Nat; :: thesis: for r being Real
for i being Nat st r in (Equal_Div_interval t) . i holds
[\(r * t)/] = i
let r be Real; :: thesis: for i being Nat st r in (Equal_Div_interval t) . i holds
[\(r * t)/] = i
let i be Nat; :: thesis: ( r in (Equal_Div_interval t) . i implies [\(r * t)/] = i )
assume A1: r in (Equal_Div_interval t) . i ; :: thesis: [\(r * t)/] = i
A2: i is Element of NAT by ORDINAL1:def 12;
r in [.(i * (t ")),((i * (t ")) + (t ")).[ by A1, A2, Def1;
then A3: ( i * (t ") <= r & r < (i * (t ")) + (t ") ) by XXREAL_1:3;
then (i * (t ")) * t <= r * t by XREAL_1:64;
then i * ((t ") * t) <= r * t ;
then A4: i * 1 <= r * t by Lm1;
t > 0 by Lm1;
then r * t < ((i + 1) * (t ")) * t by A3, XREAL_1:68;
then r * t < (i + 1) * ((t ") * t) ;
then A6: r * t < (i + 1) * 1 by Lm1;
reconsider s = r * t as Real ;
( i <= s & s - 1 < (i + 1) - 1 ) by A4, A6, XREAL_1:9;
hence [\(r * t)/] = i by INT_1:def 6; :: thesis: verum