let K be non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative Field-like doubleLoopStr ; :: thesis: for a, b being Element of K
for v being Valuation of K st K is having_valuation & a <> 0. K & v . a <= v . b holds
0 <= v . (b / a)
let a, b be Element of K; :: thesis: for v being Valuation of K st K is having_valuation & a <> 0. K & v . a <= v . b holds
0 <= v . (b / a)
let v be Valuation of K; :: thesis: ( K is having_valuation & a <> 0. K & v . a <= v . b implies 0 <= v . (b / a) )
assume that
A1: K is having_valuation and
A2: a <> 0. K ; :: thesis: ( not v . a <= v . b or 0 <= v . (b / a) )
assume v . a <= v . b ; :: thesis: 0 <= v . (b / a)
then 0 <= (v . b) - (v . a) by Lm4;
hence 0 <= v . (b / a) by A1, A2, Th22; :: thesis: verum