:: INT_3 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

definition
redefine func multint means :Def1: :: INT_3:def 1
for a, b being Element of INT holds it . a,b = multreal . a,b;
compatibility
for b1 being M6(K17(INT ,INT ), INT ) holds
( b1 = multint iff for a, b being Element of INT holds b1 . a,b = multreal . a,b )
proof end;
end;

:: deftheorem Def1 defines multint INT_3:def 1 :
for b1 being M6(K17(INT ,INT ), INT ) holds
( b1 = multint iff for a, b being Element of INT holds b1 . a,b = multreal . a,b );

definition
redefine func compint means :: INT_3:def 2
for a being Element of INT holds it . a = compreal . a;
compatibility
for b1 being M6( INT , INT ) holds
( b1 = compint iff for a being Element of INT holds b1 . a = compreal . a )
proof end;
end;

:: deftheorem defines compint INT_3:def 2 :
for b1 being M6( INT , INT ) holds
( b1 = compint iff for a being Element of INT holds b1 . a = compreal . a );

definition
func INT.Ring -> doubleLoopStr equals :: INT_3:def 3
 doubleLoopStr(# INT ,addint ,multint ,(In 1,INT ),(In 0,INT ) #);
coherence
doubleLoopStr(# INT ,addint ,multint ,(In 1,INT ),(In 0,INT ) #) is doubleLoopStr ;
end;

:: deftheorem defines INT.Ring INT_3:def 3 :
INT.Ring = doubleLoopStr(# INT ,addint ,multint ,(In 1,INT ),(In 0,INT ) #);

Lm1: for x being Element of INT.Ring holds x in REAL
proof end;

registration
cluster INT.Ring -> non empty strict ;
coherence
( INT.Ring is strict & not INT.Ring is empty )
proof end;
end;

set M = INT.Ring ;

Lm2: 0 = 0. INT.Ring
proof end;

Lm3: for a, b being Element of INT.Ring
for a', b' being Integer st a' = a & b' = b holds
a * b = a' * b'
proof end;

Lm4: for e, h being Element of INT.Ring st e = 1 holds
( h * e = h & e * h = h )
proof end;

registration
cluster INT.Ring -> non empty unital strict ;
coherence
INT.Ring is unital
proof end;
end;

Lm5: 1. INT.Ring = 1
proof end;

registration
cluster INT.Ring -> non empty unital associative commutative Abelian add-associative right_zeroed right_complementable strict distributive non degenerated domRing-like ;
coherence
( INT.Ring is Abelian & INT.Ring is add-associative & INT.Ring is right_zeroed & INT.Ring is right_complementable & INT.Ring is distributive & INT.Ring is commutative & INT.Ring is associative & INT.Ring is domRing-like & not INT.Ring is degenerated )
proof end;
end;

Lm6: for a being Element of INT.Ring
for a' being Integer st a' = a holds
- a' = - a
proof end;

definition
let a, b be Element of INT.Ring ;
pred a <= b means :Def4: :: INT_3:def 4
 ex a', b' being Integer st
( a' = a & b' = b & a' <= b' );
reflexivity
for a being Element of INT.Ring ex a', b' being Integer st
( a' = a & b' = a & a' <= b' )
proof end;
connectedness
for a, b being Element of INT.Ring st ( for a', b' being Integer holds
( not a' = a or not b' = b or not a' <= b' ) ) holds
ex a', b' being Integer st
( a' = b & b' = a & a' <= b' )
proof end;
end;

:: deftheorem Def4 defines <= INT_3:def 4 :
for a, b being Element of INT.Ring holds
( a <= b iff ex a', b' being Integer st
( a' = a & b' = b & a' <= b' ) );

notation
let a, b be Element of INT.Ring ;
synonym b >= a for a <= b;
antonym b < a for a <= b;
antonym a > b for a <= b;
end;

Lm7: for a, b being Element of INT.Ring holds
( a < b iff ( a <= b & a <> b ) )
proof end;

definition
let a be Element of INT.Ring ;
func abs a -> Element of INT.Ring equals :Def5: :: INT_3:def 5
a if a >= 0. INT.Ring
otherwise - a;
correctness
coherence
( ( a >= 0. INT.Ring implies a is Element of INT.Ring ) & ( not a >= 0. INT.Ring implies - a is Element of INT.Ring ) );
consistency
for b1 being Element of INT.Ring holds verum;
;
end;

:: deftheorem Def5 defines abs INT_3:def 5 :
for a being Element of INT.Ring holds
( ( a >= 0. INT.Ring implies abs a = a ) & ( not a >= 0. INT.Ring implies abs a = - a ) );

definition
func absint -> Function of the carrier of INT.Ring , NAT means :Def6: :: INT_3:def 6
for a being Element of INT.Ring holds it . a = absreal . a;
existence
ex b1 being Function of the carrier of INT.Ring , NAT st
for a being Element of INT.Ring holds b1 . a = absreal . a
proof end;
uniqueness
for b1, b2 being Function of the carrier of INT.Ring , NAT st ( for a being Element of INT.Ring holds b1 . a = absreal . a ) & ( for a being Element of INT.Ring holds b2 . a = absreal . a ) holds
b1 = b2
proof end;
end;

:: deftheorem Def6 defines absint INT_3:def 6 :
for b1 being Function of the carrier of INT.Ring , NAT holds
( b1 = absint iff for a being Element of INT.Ring holds b1 . a = absreal . a );

theorem Th1: :: INT_3:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being Element of INT.Ring holds absint . a = abs a
proof end;

Lm8: for a being Integer holds
( a = 0 or absreal . a >= 1 )
proof end;

Lm9: for a, b being Element of INT.Ring
for a', b' being Integer st a' = a & b' = b holds
a + b = a' + b'
proof end;

Lm10: for a, b being Element of INT.Ring st b <> 0. INT.Ring holds
for b' being Integer st b' = b & 0 <= b' holds
ex q, r being Element of INT.Ring st
( a = (q * b) + r & ( r = 0. INT.Ring or absint . r < absint . b ) )
proof end;

Lm11: for a, b being Element of INT.Ring st b <> 0. INT.Ring holds
for b' being Integer st b' = b & 0 <= b' holds
ex q, r being Element of INT.Ring st
( a = (q * b) + r & 0. INT.Ring <= r & r < abs b )
proof end;

theorem Th2: :: INT_3:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, q1, q2, r1, r2 being Element of INT.Ring st b <> 0. INT.Ring & a = (q1 * b) + r1 & 0. INT.Ring <= r1 & r1 < abs b & a = (q2 * b) + r2 & 0. INT.Ring <= r2 & r2 < abs b holds
( q1 = q2 & r1 = r2 )
proof end;

definition
let a, b be Element of INT.Ring ;
assume A1: b <> 0. INT.Ring ;
func a div b -> Element of INT.Ring means :Def7: :: INT_3:def 7
 ex r being Element of INT.Ring st
( a = (it * b) + r & 0. INT.Ring <= r & r < abs b );
existence
ex b1, r being Element of INT.Ring st
( a = (b1 * b) + r & 0. INT.Ring <= r & r < abs b )
proof end;
uniqueness
for b1, b2 being Element of INT.Ring st ex r being Element of INT.Ring st
( a = (b1 * b) + r & 0. INT.Ring <= r & r < abs b ) & ex r being Element of INT.Ring st
( a = (b2 * b) + r & 0. INT.Ring <= r & r < abs b ) holds
b1 = b2 by A1, Th2;
end;

:: deftheorem Def7 defines div INT_3:def 7 :
for a, b being Element of INT.Ring st b <> 0. INT.Ring holds
for b3 being Element of INT.Ring holds
( b3 = a div b iff ex r being Element of INT.Ring st
( a = (b3 * b) + r & 0. INT.Ring <= r & r < abs b ) );

definition
let a, b be Element of INT.Ring ;
assume A1: b <> 0. INT.Ring ;
func a mod b -> Element of INT.Ring means :Def8: :: INT_3:def 8
 ex q being Element of INT.Ring st
( a = (q * b) + it & 0. INT.Ring <= it & it < abs b );
existence
ex b1, q being Element of INT.Ring st
( a = (q * b) + b1 & 0. INT.Ring <= b1 & b1 < abs b )
proof end;
uniqueness
for b1, b2 being Element of INT.Ring st ex q being Element of INT.Ring st
( a = (q * b) + b1 & 0. INT.Ring <= b1 & b1 < abs b ) & ex q being Element of INT.Ring st
( a = (q * b) + b2 & 0. INT.Ring <= b2 & b2 < abs b ) holds
b1 = b2 by A1, Th2;
end;

:: deftheorem Def8 defines mod INT_3:def 8 :
for a, b being Element of INT.Ring st b <> 0. INT.Ring holds
for b3 being Element of INT.Ring holds
( b3 = a mod b iff ex q being Element of INT.Ring st
( a = (q * b) + b3 & 0. INT.Ring <= b3 & b3 < abs b ) );

theorem :: INT_3:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b being Element of INT.Ring st b <> 0. INT.Ring holds
a = ((a div b) * b) + (a mod b)
proof end;

definition
let I be non empty doubleLoopStr ;
attr I is Euclidian means :Def9: :: INT_3:def 9
 ex f being Function of the carrier of I, NAT st
for a, b being Element of I st b <> 0. I holds
ex q, r being Element of I st
( a = (q * b) + r & ( r = 0. I or f . r < f . b ) );
end;

:: deftheorem Def9 defines Euclidian INT_3:def 9 :
for I being non empty doubleLoopStr holds
( I is Euclidian iff ex f being Function of the carrier of I, NAT st
for a, b being Element of I st b <> 0. I holds
ex q, r being Element of I st
( a = (q * b) + r & ( r = 0. I or f . r < f . b ) ) );

registration
cluster INT.Ring -> non empty unital associative commutative Abelian add-associative right_zeroed right_complementable strict distributive non degenerated domRing-like Euclidian ;
coherence
INT.Ring is Euclidian
proof end;
end;

Lm12: for F being non empty associative commutative right_zeroed left_unital Field-like doubleLoopStr
for f being Function of the carrier of F, NAT
for a, b being Element of F st b <> 0. F holds
ex q, r being Element of F st
( a = (q * b) + r & ( r = 0. F or f . r < f . b ) )
proof end;

registration
cluster commutative strict non degenerated domRing-like Euclidian doubleLoopStr ;
existence
ex b1 being Ring st
( b1 is strict & b1 is Euclidian & b1 is domRing-like & not b1 is degenerated & b1 is distributive & b1 is commutative )
proof end;
end;

definition
mode EuclidianRing is commutative distributive non degenerated domRing-like Euclidian Ring;
end;

registration
cluster strict doubleLoopStr ;
existence
ex b1 being EuclidianRing st b1 is strict
proof end;
end;

definition
let E be non empty Euclidian doubleLoopStr ;
mode DegreeFunction of E -> Function of the carrier of E, NAT means :Def10: :: INT_3:def 10
for a, b being Element of E st b <> 0. E holds
ex q, r being Element of E st
( a = (q * b) + r & ( r = 0. E or it . r < it . b ) );
existence
ex b1 being Function of the carrier of E, NAT st
for a, b being Element of E st b <> 0. E holds
ex q, r being Element of E st
( a = (q * b) + r & ( r = 0. E or b1 . r < b1 . b ) ) by Def9;
end;

:: deftheorem Def10 defines DegreeFunction INT_3:def 10 :
for E being non empty Euclidian doubleLoopStr
for b2 being Function of the carrier of E, NAT holds
( b2 is DegreeFunction of E iff for a, b being Element of E st b <> 0. E holds
ex q, r being Element of E st
( a = (q * b) + r & ( r = 0. E or b2 . r < b2 . b ) ) );

theorem Th4: :: INT_3:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for E being EuclidianRing holds E is gcdDomain
proof end;

registration
cluster non empty associative commutative Abelian add-associative right_zeroed right_complementable right-distributive right_unital non degenerated domRing-like Euclidian -> non empty associative commutative Abelian add-associative right_zeroed right_complementable right-distributive right_unital non degenerated domRing-like gcd-like doubleLoopStr ;
coherence
for b1 being non empty associative commutative Abelian add-associative right_zeroed right_complementable right-distributive right_unital non degenerated domRing-like doubleLoopStr st b1 is Euclidian holds
b1 is gcd-like by Th4;
end;

definition
:: original: absint
redefine func absint -> DegreeFunction of INT.Ring ;
coherence
absint is DegreeFunction of INT.Ring
proof end;
end;

theorem Th5: :: INT_3:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F being non empty associative commutative right_zeroed left_unital Field-like doubleLoopStr holds F is Euclidian
proof end;

registration
cluster non empty associative commutative right_zeroed left_unital Field-like -> non empty Euclidian doubleLoopStr ;
coherence
for b1 being non empty doubleLoopStr st b1 is commutative & b1 is associative & b1 is left_unital & b1 is Field-like & b1 is right_zeroed & b1 is Field-like holds
b1 is Euclidian by Th5;
end;

theorem :: INT_3:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F being non empty associative commutative right_zeroed left_unital Field-like doubleLoopStr
for f being Function of the carrier of F, NAT holds f is DegreeFunction of F
proof end;

theorem :: INT_3:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th8: :: INT_3:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n, a, k being Integer holds
( ( n <> 0 implies (a + (n * k)) div n = (a div n) + k ) & (a + (n * k)) mod n = a mod n )
proof end;

theorem Th9: :: INT_3:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being natural number st n > 0 holds
for a being Integer holds
( a mod n >= 0 & a mod n < n )
proof end;

theorem Th10: :: INT_3:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n, a being Integer holds
( ( 0 <= a & a < n implies a mod n = a ) & ( 0 > a & a >= - n implies a mod n = n + a ) )
proof end;

theorem Th11: :: INT_3:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being natural number st n > 0 holds
for a being Integer holds
( a mod n = 0 iff n divides a )
proof end;

theorem Th12: :: INT_3:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n, a, b being Integer holds
( ( n <> 0 & a mod n = b mod n implies a,b are_congruent_mod n ) & ( a,b are_congruent_mod n implies a mod n = b mod n ) )
proof end;

theorem Th13: :: INT_3:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being natural number
for a being Integer holds (a mod n) mod n = a mod n
proof end;

theorem Th14: :: INT_3:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n, a, b being Integer holds (a + b) mod n = ((a mod n) + (b mod n)) mod n
proof end;

theorem Th15: :: INT_3:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n, a, b being Integer holds (a * b) mod n = ((a mod n) * (b mod n)) mod n
proof end;

theorem Th16: :: INT_3:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b being Integer ex s, t being Integer st a gcd b = (s * a) + (t * b)
proof end;

definition
let n be natural number ;
assume A1: n > 0 ;
func multint n -> BinOp of Segm n means :Def11: :: INT_3:def 11
for k, l being Element of Segm n holds it . k,l = (k * l) mod n;
existence
ex b1 being BinOp of Segm n st
for k, l being Element of Segm n holds b1 . k,l = (k * l) mod n
proof end;
uniqueness
for b1, b2 being BinOp of Segm n st ( for k, l being Element of Segm n holds b1 . k,l = (k * l) mod n ) & ( for k, l being Element of Segm n holds b2 . k,l = (k * l) mod n ) holds
b1 = b2
proof end;
end;

:: deftheorem Def11 defines multint INT_3:def 11 :
for n being natural number st n > 0 holds
for b2 being BinOp of Segm n holds
( b2 = multint n iff for k, l being Element of Segm n holds b2 . k,l = (k * l) mod n );

definition
let n be natural number ;
assume A1: n > 0 ;
func compint n -> UnOp of Segm n means :Def12: :: INT_3:def 12
for k being Element of Segm n holds it . k = (n - k) mod n;
existence
ex b1 being UnOp of Segm n st
for k being Element of Segm n holds b1 . k = (n - k) mod n
proof end;
uniqueness
for b1, b2 being UnOp of Segm n st ( for k being Element of Segm n holds b1 . k = (n - k) mod n ) & ( for k being Element of Segm n holds b2 . k = (n - k) mod n ) holds
b1 = b2
proof end;
end;

:: deftheorem Def12 defines compint INT_3:def 12 :
for n being natural number st n > 0 holds
for b2 being UnOp of Segm n holds
( b2 = compint n iff for k being Element of Segm n holds b2 . k = (n - k) mod n );

Lm13: for n being natural number st n > 0 holds
for a being natural number st a < n holds
for b being natural number st b = n - a holds
(n - a) mod n = b mod n
proof end;

theorem Th17: :: INT_3:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being natural number st n > 0 holds
for a, b being Element of Segm n holds
( ( a + b < n implies (addint n) . a,b = a + b ) & ( (addint n) . a,b = a + b implies a + b < n ) & ( a + b >= n implies (addint n) . a,b = (a + b) - n ) & ( (addint n) . a,b = (a + b) - n implies a + b >= n ) )
proof end;

Lm14: for a, b being natural number st b <> 0 holds
ex k being Nat st
( k * b <= a & a < (k + 1) * b )
proof end;

theorem Th18: :: INT_3:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being natural number st n > 0 holds
for a, b being Element of Segm n
for k being natural number holds
( ( k * n <= a * b & a * b < (k + 1) * n ) iff (multint n) . a,b = (a * b) - (k * n) )
proof end;

theorem :: INT_3:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being natural number st n > 0 holds
for a being Element of Segm n holds
( ( a = 0 implies (compint n) . a = 0 ) & ( (compint n) . a = 0 implies a = 0 ) & ( a <> 0 implies (compint n) . a = n - a ) & ( (compint n) . a = n - a implies a <> 0 ) )
proof end;

definition
let n be natural number ;
func INT.Ring n -> doubleLoopStr equals :: INT_3:def 13
 doubleLoopStr(# (Segm n),(addint n),(multint n),(In 1,(Segm n)),(In 0,(Segm n)) #);
coherence
doubleLoopStr(# (Segm n),(addint n),(multint n),(In 1,(Segm n)),(In 0,(Segm n)) #) is doubleLoopStr ;
end;

:: deftheorem defines INT.Ring INT_3:def 13 :
for n being natural number holds INT.Ring n = doubleLoopStr(# (Segm n),(addint n),(multint n),(In 1,(Segm n)),(In 0,(Segm n)) #);

registration
let n be natural number ;
cluster INT.Ring n -> non empty strict ;
coherence
( INT.Ring n is strict & not INT.Ring n is empty )
proof end;
end;

theorem Th20: :: INT_3:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
( INT.Ring 1 is degenerated & INT.Ring 1 is Ring & INT.Ring 1 is Field-like & INT.Ring 1 is unital & INT.Ring 1 is distributive & INT.Ring 1 is commutative )
proof end;

registration
cluster unital commutative strict Field-like degenerated Euclidian doubleLoopStr ;
existence
ex b1 being Ring st
( b1 is strict & b1 is degenerated & b1 is unital & b1 is distributive & b1 is Field-like & b1 is commutative ) by Th20;
end;

Lm15: now
let a, n be natural number ; :: thesis: ( n > 0 & a in Segm n & a > 0 implies n - a in Segm n )
assume A1: n > 0 ; :: thesis: ( a in Segm n & a > 0 implies n - a in Segm n )
assume a in Segm n ; :: thesis: ( a > 0 implies n - a in Segm n )
then a < n by A1, GR_CY_1:10;
then A2: n - a is Nat by INT_1:18;
assume a > 0 ; :: thesis: n - a in Segm n
then n - a < n - 0 by REAL_1:92;
hence n - a in Segm n by A2, GR_CY_1:10; :: thesis: verum
end;

Lm16: for n being natural number st 0 < n holds
for e, h being Element of (INT.Ring n) st e = 1 holds
( h * e = h & e * h = h )
proof end;

Lm17: now
let n be natural number ; :: thesis: ( 1 < n implies INT.Ring n is unital )
assume A1: 1 < n ; :: thesis: INT.Ring n is unital
thus INT.Ring n is unital :: thesis: verum
proof
set M = INT.Ring n;
reconsider e = 1 as Element of (INT.Ring n) by A1, GR_CY_1:10;
take e ; :: according to GROUP_1:def 2 :: thesis: for b1 being Element of the carrier of (INT.Ring n) holds
( b1 * e = b1 & e * b1 = b1 )
thus for b1 being Element of the carrier of (INT.Ring n) holds
( b1 * e = b1 & e * b1 = b1 ) by A1, Lm16; :: thesis: verum
end;
end;

Lm18: for n being natural number st 1 < n holds
1. (INT.Ring n) = 1
proof end;

theorem Th21: :: INT_3:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being natural number st n > 1 holds
( not INT.Ring n is degenerated & INT.Ring n is unital commutative distributive Ring )
proof end;

Lm19: for p being natural number st p > 0 holds
0. (INT.Ring p) = 0
proof end;

theorem Th22: :: INT_3:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being natural number st p > 1 holds
( INT.Ring p is non empty associative commutative Abelian add-associative right_zeroed right_complementable distributive left_unital Field-like non degenerated doubleLoopStr iff p is Prime )
proof end;

registration
let p be Prime;
cluster INT.Ring p -> non empty associative commutative Abelian add-associative right_zeroed right_complementable strict distributive left_unital Field-like non degenerated Euclidian ;
coherence
( INT.Ring p is add-associative & INT.Ring p is right_zeroed & INT.Ring p is right_complementable & INT.Ring p is Abelian & INT.Ring p is commutative & INT.Ring p is associative & INT.Ring p is left_unital & INT.Ring p is distributive & INT.Ring p is Field-like & not INT.Ring p is degenerated )
proof end;
end;

theorem :: INT_3:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
1. INT.Ring = 1 by Lm5;

theorem :: INT_3:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being natural number st 1 < n holds
1. (INT.Ring n) = 1 by Lm18;