let K be non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative Field-like doubleLoopStr ; :: thesis: for v being Valuation of K st K is having_valuation holds

least-positive (rng v) is integer

let v be Valuation of K; :: thesis: ( K is having_valuation implies least-positive (rng v) is integer )

set l = least-positive (rng v);

assume A1: K is having_valuation ; :: thesis: least-positive (rng v) is integer

then consider a being Element of K such that

A2: v . a <> 0 and

A3: v . a <> +infty by Def8;

A4: dom v = the carrier of K by FUNCT_2:def 1;

then A5: v . a in rng v by FUNCT_1:def 3;

assume not least-positive (rng v) is integer ; :: thesis: contradiction

then A6: least-positive (rng v) = +infty by Def1;

A7: a <> 0. K by A1, A3, Def8;

then v . a in INT by A1, Def8;

then reconsider va = v . a as Real ;

least-positive (rng v) is integer

let v be Valuation of K; :: thesis: ( K is having_valuation implies least-positive (rng v) is integer )

set l = least-positive (rng v);

assume A1: K is having_valuation ; :: thesis: least-positive (rng v) is integer

then consider a being Element of K such that

A2: v . a <> 0 and

A3: v . a <> +infty by Def8;

A4: dom v = the carrier of K by FUNCT_2:def 1;

then A5: v . a in rng v by FUNCT_1:def 3;

assume not least-positive (rng v) is integer ; :: thesis: contradiction

then A6: least-positive (rng v) = +infty by Def1;

A7: a <> 0. K by A1, A3, Def8;

then v . a in INT by A1, Def8;

then reconsider va = v . a as Real ;

per cases
( va is positive or not va is positive )
;

end;

suppose
va is positive
; :: thesis: contradiction

then
least-positive (rng v) <= v . a
by A5, Def2;

hence contradiction by A3, A6, XXREAL_0:4; :: thesis: verum

end;hence contradiction by A3, A6, XXREAL_0:4; :: thesis: verum

suppose
not va is positive
; :: thesis: contradiction

then reconsider va = va as non positive Real ;

reconsider va = va as negative Real by A2;

set b = a " ;

a " <> 0. K by A7, VECTSP_2:13;

then A8: v . (a ") in INT by A1, Def8;

A9: v . (a ") in rng v by A4, FUNCT_1:def 3;

v . (a ") = - (v . a) by A1, A7, Th21

.= - va by XXREAL_3:def 3 ;

then least-positive (rng v) <= v . (a ") by A9, Def2;

hence contradiction by A8, A6, XXREAL_0:4; :: thesis: verum

end;reconsider va = va as negative Real by A2;

set b = a " ;

a " <> 0. K by A7, VECTSP_2:13;

then A8: v . (a ") in INT by A1, Def8;

A9: v . (a ") in rng v by A4, FUNCT_1:def 3;

v . (a ") = - (v . a) by A1, A7, Th21

.= - va by XXREAL_3:def 3 ;

then least-positive (rng v) <= v . (a ") by A9, Def2;

hence contradiction by A8, A6, XXREAL_0:4; :: thesis: verum