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

for x being Element of K st x <> 0. K holds

ex i being Integer st v . x = i * (least-positive (rng v))

let v be Valuation of K; :: thesis: ( K is having_valuation implies for x being Element of K st x <> 0. K holds

ex i being Integer st v . x = i * (least-positive (rng v)) )

assume A1: K is having_valuation ; :: thesis: for x being Element of K st x <> 0. K holds

ex i being Integer st v . x = i * (least-positive (rng v))

let x be Element of K; :: thesis: ( x <> 0. K implies ex i being Integer st v . x = i * (least-positive (rng v)) )

assume A2: x <> 0. K ; :: thesis: ex i being Integer st v . x = i * (least-positive (rng v))

reconsider vx = v . x as Element of INT by A1, A2, Def8;

reconsider l = least-positive (rng v) as Integer by A1, Th35;

A3: v . x = ((vx div l) * l) + (vx mod l) by INT_1:59;

for x being Element of K st x <> 0. K holds

ex i being Integer st v . x = i * (least-positive (rng v))

let v be Valuation of K; :: thesis: ( K is having_valuation implies for x being Element of K st x <> 0. K holds

ex i being Integer st v . x = i * (least-positive (rng v)) )

assume A1: K is having_valuation ; :: thesis: for x being Element of K st x <> 0. K holds

ex i being Integer st v . x = i * (least-positive (rng v))

let x be Element of K; :: thesis: ( x <> 0. K implies ex i being Integer st v . x = i * (least-positive (rng v)) )

assume A2: x <> 0. K ; :: thesis: ex i being Integer st v . x = i * (least-positive (rng v))

reconsider vx = v . x as Element of INT by A1, A2, Def8;

reconsider l = least-positive (rng v) as Integer by A1, Th35;

A3: v . x = ((vx div l) * l) + (vx mod l) by INT_1:59;

per cases
( vx mod l = 0 or vx mod l <> 0 )
;

end;

suppose A4:
vx mod l = 0
; :: thesis: ex i being Integer st v . x = i * (least-positive (rng v))

take
vx div l
; :: thesis: v . x = (vx div l) * (least-positive (rng v))

thus v . x = (vx div l) * (least-positive (rng v)) by A3, A4, XXREAL_3:def 5; :: thesis: verum

end;thus v . x = (vx div l) * (least-positive (rng v)) by A3, A4, XXREAL_3:def 5; :: thesis: verum

suppose A5:
vx mod l <> 0
; :: thesis: ex i being Integer st v . x = i * (least-positive (rng v))

consider k being Element of K such that

A6: l = v . k by A1, Lm5, FUNCT_2:113;

set d = vx div l;

set kd = k |^ (vx div l);

set kD = (k |^ (vx div l)) " ;

A7: k <> 0. K by A1, A6, Def8;

then A8: (vx div l) * (v . k) = v . (k |^ (vx div l)) by A1, Th29;

A9: - (v . (k |^ (vx div l))) = v . ((k |^ (vx div l)) ") by A1, A7, Th16, Th21;

A10: (vx div l) * l = (vx div l) * (v . k) by A6, XXREAL_3:def 5;

A11: v . (x * ((k |^ (vx div l)) ")) = (v . x) - ((vx div l) * l) by A8, A9, A10, A1, Def8

.= vx - ((vx div l) * l) by Lm1

.= vx mod l by A3 ;

then A12: 0 <= v . (x * ((k |^ (vx div l)) ")) by INT_1:57;

A13: v . (x * ((k |^ (vx div l)) ")) < l by A11, INT_1:58;

v . (x * ((k |^ (vx div l)) ")) in rng v by FUNCT_2:4;

hence ex i being Integer st v . x = i * (least-positive (rng v)) by A12, A5, A11, A13, Def2; :: thesis: verum

end;A6: l = v . k by A1, Lm5, FUNCT_2:113;

set d = vx div l;

set kd = k |^ (vx div l);

set kD = (k |^ (vx div l)) " ;

A7: k <> 0. K by A1, A6, Def8;

then A8: (vx div l) * (v . k) = v . (k |^ (vx div l)) by A1, Th29;

A9: - (v . (k |^ (vx div l))) = v . ((k |^ (vx div l)) ") by A1, A7, Th16, Th21;

A10: (vx div l) * l = (vx div l) * (v . k) by A6, XXREAL_3:def 5;

A11: v . (x * ((k |^ (vx div l)) ")) = (v . x) - ((vx div l) * l) by A8, A9, A10, A1, Def8

.= vx - ((vx div l) * l) by Lm1

.= vx mod l by A3 ;

then A12: 0 <= v . (x * ((k |^ (vx div l)) ")) by INT_1:57;

A13: v . (x * ((k |^ (vx div l)) ")) < l by A11, INT_1:58;

v . (x * ((k |^ (vx div l)) ")) in rng v by FUNCT_2:4;

hence ex i being Integer st v . x = i * (least-positive (rng v)) by A12, A5, A11, A13, Def2; :: thesis: verum