:: NAT_D semantic presentation

begin


Lm1: now__::_thesis:_for_k,_l_being_Nat_holds_k_div_l_is_Nat
let k, l be Nat; ::_thesis: k div l is Nat
 k div l in NAT by INT_1:3, INT_1:55;
hence  k div l is Nat ; ::_thesis: verum
end;

Lm2: now__::_thesis:_for_k,_l_being_Nat_holds_k_mod_l_is_Nat
let k, l be Nat; ::_thesis: k mod l is Nat
 k mod l in NAT by INT_1:3, INT_1:57;
hence  k mod l is Nat ; ::_thesis: verum
end;

definition
let k, l be Nat;
:: original: div
redefine funck div l ->  Nat means :Def1: :: NAT_D:def 1
( ex t being Nat st
( k = (l * it) + t & t < l ) or ( it = 0 & l = 0 ) );
compatibility
 for b1 being Nat holds
( b1 = k div l iff ( ex t being Nat st
( k = (l * b1) + t & t < l ) or ( b1 = 0 & l = 0 ) ) )
proof
let r be Nat; ::_thesis: ( r = k div l iff ( ex t being Nat st
( k = (l * r) + t & t < l ) or ( r = 0 & l = 0 ) ) )
percases ( l = 0 or l > 0 ) ;
suppose l = 0 ; ::_thesis: ( r = k div l iff ( ex t being Nat st
( k = (l * r) + t & t < l ) or ( r = 0 & l = 0 ) ) )
hence  ( r = k div l iff ( ex t being Nat st
( k = (l * r) + t & t < l ) or ( r = 0 & l = 0 ) ) ) by INT_1:48; ::_thesis: verum
end;
supposeA1: l > 0 ; ::_thesis: ( r = k div l iff ( ex t being Nat st
( k = (l * r) + t & t < l ) or ( r = 0 & l = 0 ) ) )
then A2: k = (l * (k div l)) + (k mod l) by INT_1:59;
A3: k mod l is Nat by Lm2;
hence  ( not r = k div l or ex t being Nat st
( k = (l * r) + t & t < l ) or ( r = 0 & l = 0 ) ) by A1, A2, INT_1:58; ::_thesis: ( ( ex t being Nat st
( k = (l * r) + t & t < l ) or ( r = 0 & l = 0 ) ) implies r = k div l )
assume A4: ( ex t being Nat st
( k = (l * r) + t & t < l ) or ( r = 0 & l = 0 ) ) ; ::_thesis: r = k div l
A5: k mod l < l by A1, INT_1:58;
 k div l is Nat by Lm1;
hence  r = k div l by A2, A3, A4, A5, NAT_1:18; ::_thesis: verum
end;
end;
end;
coherence
 k div l is Nat by Lm1;
end;

:: deftheorem Def1 defines div NAT_D:def_1_:_
 for k, l, b3 being Nat holds
( b3 = k div l iff ( ex t being Nat st
( k = (l * b3) + t & t < l ) or ( b3 = 0 & l = 0 ) ) );

definition
let k, l be Nat;
:: original: mod
redefine funck mod l ->  Nat means :Def2: :: NAT_D:def 2
( ex t being Nat st
( k = (l * t) + it & it < l ) or ( it = 0 & l = 0 ) );
compatibility
 for b1 being Nat holds
( b1 = k mod l iff ( ex t being Nat st
( k = (l * t) + b1 & b1 < l ) or ( b1 = 0 & l = 0 ) ) )
proof
let r be Nat; ::_thesis: ( r = k mod l iff ( ex t being Nat st
( k = (l * t) + r & r < l ) or ( r = 0 & l = 0 ) ) )
percases ( l = 0 or l > 0 ) ;
suppose l = 0 ; ::_thesis: ( r = k mod l iff ( ex t being Nat st
( k = (l * t) + r & r < l ) or ( r = 0 & l = 0 ) ) )
hence  ( r = k mod l iff ( ex t being Nat st
( k = (l * t) + r & r < l ) or ( r = 0 & l = 0 ) ) ) by INT_1:def_10; ::_thesis: verum
end;
supposeA1: l > 0 ; ::_thesis: ( r = k mod l iff ( ex t being Nat st
( k = (l * t) + r & r < l ) or ( r = 0 & l = 0 ) ) )
then A2: k = (l * (k div l)) + (k mod l) by INT_1:59;
hence  ( not r = k mod l or ex t being Nat st
( k = (l * t) + r & r < l ) or ( r = 0 & l = 0 ) ) by A1, INT_1:58; ::_thesis: ( ( ex t being Nat st
( k = (l * t) + r & r < l ) or ( r = 0 & l = 0 ) ) implies r = k mod l )
assume A3: ( ex t being Nat st
( k = (l * t) + r & r < l ) or ( r = 0 & l = 0 ) ) ; ::_thesis: r = k mod l
A4: k mod l < l by A1, INT_1:58;
 k mod l is Nat by Lm2;
hence  r = k mod l by A2, A3, A4, NAT_1:18; ::_thesis: verum
end;
end;
end;
coherence
 k mod l is Nat by Lm2;
end;

:: deftheorem Def2 defines mod NAT_D:def_2_:_
 for k, l, b3 being Nat holds
( b3 = k mod l iff ( ex t being Nat st
( k = (l * t) + b3 & b3 < l ) or ( b3 = 0 & l = 0 ) ) );

definition
let k, l be Nat;
:: original: div
redefine funck div l ->  Element of NAT ;
coherence
 k div l is Element of NAT
proof
 k div l is Nat ;
hence  k div l is Element of NAT by ORDINAL1:def_12; ::_thesis: verum
end;
:: original: mod
redefine funck mod l ->  Element of NAT ;
coherence
 k mod l is Element of NAT
proof
 k mod l is Nat ;
hence  k mod l is Element of NAT by ORDINAL1:def_12; ::_thesis: verum
end;
end;

theorem Th1: :: NAT_D:1
for i, j being Nat st 0 < i holds
j mod i < i
proof
let i, j be Nat; ::_thesis: ( 0 < i implies j mod i < i )
assume  0 < i ; ::_thesis: j mod i < i
then  ex t being Nat st
( j = (i * t) + (j mod i) & j mod i < i ) by Def2;
hence  j mod i < i ; ::_thesis: verum
end;

theorem :: NAT_D:2
for i, j being Nat st 0 < i holds
j = (i * (j div i)) + (j mod i) by INT_1:59;

definition
let k, l be Nat;
:: original: divides
redefine predk divides l means :Def3: :: NAT_D:def 3
 ex t being Nat st l = k * t;
compatibility
 ( k divides l iff ex t being Nat st l = k * t )
proof
hereby  ::_thesis: ( ex t being Nat st l = k * t implies k divides l )
assume A1: k divides l ; ::_thesis: ex t being Nat st l = k * t
thus  ex t being Nat st l = k * t ::_thesis: verum
proof
consider t being Integer such that
A2: l = k * t by A1, INT_1:def_3;
percases ( 0 < l or l = 0 ) ;
suppose 0 < l ; ::_thesis: ex t being Nat st l = k * t
then  0 <= t by A2;
then reconsider t = t as Element of NAT by INT_1:3;
take  t ; ::_thesis: l = k * t
thus  l = k * t by A2; ::_thesis: verum
end;
supposeA3: l = 0 ; ::_thesis: ex t being Nat st l = k * t
take  0 ; ::_thesis: l = k * 0
thus  l = k * 0 by A3; ::_thesis: verum
end;
end;
end;
end;
assume  ex t being Nat st l = k * t ; ::_thesis: k divides l
hence  k divides l by INT_1:def_3; ::_thesis: verum
end;
reflexivity
 for k being Nat ex t being Nat st k = k * t
proof
let i be Nat; ::_thesis: ex t being Nat st i = i * t
 i = i * 1 ;
hence  ex t being Nat st i = i * t ; ::_thesis: verum
end;
end;

:: deftheorem Def3 defines divides NAT_D:def_3_:_
 for k, l being Nat holds
( k divides l iff ex t being Nat st l = k * t );

theorem Th3: :: NAT_D:3
for j, i being Nat holds
( j divides i iff i = j * (i div j) )
proof
let j, i be Nat; ::_thesis: ( j divides i iff i = j * (i div j) )
thus  ( j divides i implies i = j * (i div j) ) ::_thesis: ( i = j * (i div j) implies j divides i )
proof
assume  j divides i ; ::_thesis: i = j * (i div j)
then consider k being Nat such that
A1: i = j * k by Def3;
A2: i = (j * k) + 0 by A1;
now__::_thesis:_(_j_<>_0_implies_i_=_j_*_(i_div_j)_)
assume A3: j <> 0 ; ::_thesis: i = j * (i div j)
then A4: i = (j * (i div j)) + (i mod j) by INT_1:59;
 i mod j < j by A3, Th1;
hence  i = j * (i div j) by A2, A4, NAT_1:18; ::_thesis: verum
end;
hence  i = j * (i div j) by A1; ::_thesis: verum
end;
assume  i = j * (i div j) ; ::_thesis: j divides i
hence  j divides i by Def3; ::_thesis: verum
end;

theorem :: NAT_D:4
for i, j, h being Nat st i divides j & j divides h holds
i divides h
proof
let i, j, h be Nat; ::_thesis: ( i divides j & j divides h implies i divides h )
assume that
A1: i divides j and
A2: j divides h ; ::_thesis: i divides h
A3: j = i * (j div i) by A1, Th3;
 h = j * (h div j) by A2, Th3;
then  h = i * ((j div i) * (h div j)) by A3;
hence  i divides h by Def3; ::_thesis: verum
end;

theorem Th5: :: NAT_D:5
for i, j being Nat st i divides j & j divides i holds
i = j
proof
let i, j be Nat; ::_thesis: ( i divides j & j divides i implies i = j )
assume that
A1: i divides j and
A2: j divides i ; ::_thesis: i = j
A3: j = i * (j div i) by A1, Th3;
 i = j * (i div j) by A2, Th3;
then A4: i * 1 = (i * (j div i)) * (i div j) by A3
.= i * ((j div i) * (i div j)) ;
A5: ( i = 0 implies i = j ) by A3;
 ( (j div i) * (i div j) = 1 implies i = j )
proof
assume  (j div i) * (i div j) = 1 ; ::_thesis: i = j
then  j div i = 1 by NAT_1:15;
hence  i = j by A3; ::_thesis: verum
end;
hence  i = j by A4, A5, XCMPLX_1:5; ::_thesis: verum
end;

theorem Th6: :: NAT_D:6
for i being Nat holds
( i divides 0 & 1 divides i )
proof
let i be Nat; ::_thesis: ( i divides 0 & 1 divides i )
 0 = i * 0 ;
hence  i divides 0 by Def3; ::_thesis: 1 divides i
 i = i * 1 ;
hence  1 divides i by Def3; ::_thesis: verum
end;

theorem :: NAT_D:7
for j, i being Nat st 0 < j & i divides j holds
i <= j
proof
let j, i be Nat; ::_thesis: ( 0 < j & i divides j implies i <= j )
assume that
A1: 0 < j and
A2: i divides j ; ::_thesis: i <= j
A3: j = i * (j div i) by A2, Th3;
then  j div i <> 0 by A1;
then consider m being Nat such that
A4: j div i = m + 1 by NAT_1:6;
 i * (m + 1) = i + (i * m) ;
hence  i <= j by A3, A4, NAT_1:11; ::_thesis: verum
end;

theorem Th8: :: NAT_D:8
for i, j, h being Nat st i divides j & i divides h holds
i divides j + h
proof
let i, j, h be Nat; ::_thesis: ( i divides j & i divides h implies i divides j + h )
assume that
A1: i divides j and
A2: i divides h ; ::_thesis: i divides j + h
A3: j = i * (j div i) by A1, Th3;
 h = i * (h div i) by A2, Th3;
then  j + h = i * ((j div i) + (h div i)) by A3;
hence  i divides j + h by Def3; ::_thesis: verum
end;

theorem Th9: :: NAT_D:9
for i, j, h being Nat st i divides j holds
i divides j * h
proof
let i, j, h be Nat; ::_thesis: ( i divides j implies i divides j * h )
assume  i divides j ; ::_thesis: i divides j * h
then consider l being Nat such that
A1: j = i * l by Def3;
 (i * l) * h = i * (l * h) ;
hence  i divides j * h by A1, Def3; ::_thesis: verum
end;

theorem Th10: :: NAT_D:10
for i, j, h being Nat st i divides j & i divides j + h holds
i divides h
proof
let i, j, h be Nat; ::_thesis: ( i divides j & i divides j + h implies i divides h )
assume that
A1: i divides j and
A2: i divides j + h ; ::_thesis: i divides h
consider t being Nat such that
A3: j + h = i * t by A2, Def3;
consider u being Nat such that
A4: j = i * u by A1, Def3;
now__::_thesis:_(_i_<>_0_implies_i_divides_h_)
assume A5: i <> 0 ; ::_thesis: i divides h
then A6: h = (i * (h div i)) + (h mod i) by INT_1:59;
A7: j + ((i * (h div i)) + (h mod i)) = (i * (u + (h div i))) + (h mod i) by A4;
A8: h mod i < i by A5, Th1;
 j + h = (i * t) + 0 by A3;
then  h mod i = 0 by A6, A7, A8, NAT_1:18;
hence  i divides h by A6, Th3; ::_thesis: verum
end;
hence  i divides h by A3; ::_thesis: verum
end;

theorem Th11: :: NAT_D:11
for i, j, h being Nat st i divides j & i divides h holds
i divides j mod h
proof
let i, j, h be Nat; ::_thesis: ( i divides j & i divides h implies i divides j mod h )
assume that
A1: i divides j and
A2: i divides h ; ::_thesis: i divides j mod h
A3: now__::_thesis:_(_h_=_0_implies_i_divides_j_mod_h_)
assume  h = 0 ; ::_thesis: i divides j mod h
then  j mod h = 0 by Def2;
hence  i divides j mod h by Th6; ::_thesis: verum
end;
now__::_thesis:_(_h_<>_0_implies_i_divides_j_mod_h_)
assume  h <> 0 ; ::_thesis: i divides j mod h
then A4: j = (h * (j div h)) + (j mod h) by INT_1:59;
 i divides h * (j div h) by A2, Th9;
hence  i divides j mod h by A1, A4, Th10; ::_thesis: verum
end;
hence  i divides j mod h by A3; ::_thesis: verum
end;

definition
let k, n be Nat;
redefine func k lcm n means :Def4: :: NAT_D:def 4
( k divides it & n divides it & ( for m being Nat st k divides m & n divides m holds
it divides m ) );
compatibility
 for b1 being set holds
( b1 = k lcm n iff ( k divides b1 & n divides b1 & ( for m being Nat st k divides m & n divides m holds
b1 divides m ) ) )
proof
let IT be Nat; ::_thesis: ( IT = k lcm n iff ( k divides IT & n divides IT & ( for m being Nat st k divides m & n divides m holds
IT divides m ) ) )
thus  ( IT = k lcm n implies ( k divides IT & n divides IT & ( for m being Nat st k divides m & n divides m holds
IT divides m ) ) ) by INT_2:def_1; ::_thesis: ( k divides IT & n divides IT & ( for m being Nat st k divides m & n divides m holds
IT divides m ) implies IT = k lcm n )
assume that
A1: k divides IT and
A2: n divides IT and
A3: for m being Nat st k divides m & n divides m holds
IT divides m ; ::_thesis: IT = k lcm n
 for m being Integer st k divides m & n divides m holds
IT divides m
proof
let m be Integer; ::_thesis: ( k divides m & n divides m implies IT divides m )
 m in INT by INT_1:def_2;
then consider i being Element of NAT  such that
A4: ( m = i or m = - i ) by INT_1:def_1;
assume that
A5: k divides m and
A6: n divides m ; ::_thesis: IT divides m
A7: k divides i by A4, A5, INT_2:10;
 n divides i by A4, A6, INT_2:10;
then  IT divides i by A3, A7;
hence  IT divides m by A4, INT_2:10; ::_thesis: verum
end;
hence  IT = k lcm n by A1, A2, INT_2:def_1; ::_thesis: verum
end;
end;

:: deftheorem Def4 defines lcm NAT_D:def_4_:_
 for k, n being Nat
for b3 being set holds
( b3 = k lcm n iff ( k divides b3 & n divides b3 & ( for m being Nat st k divides m & n divides m holds
b3 divides m ) ) );

definition
let k, n be Nat;
:: original: lcm
redefine funck lcm n ->  Element of NAT ;
coherence
 k lcm n is Element of NAT by ORDINAL1:def_12;
end;

definition
let k, n be Nat;
redefine func k gcd n means :Def5: :: NAT_D:def 5
( it divides k & it divides n & ( for m being Nat st m divides k & m divides n holds
m divides it ) );
compatibility
 for b1 being set holds
( b1 = k gcd n iff ( b1 divides k & b1 divides n & ( for m being Nat st m divides k & m divides n holds
m divides b1 ) ) )
proof
let IT be Nat; ::_thesis: ( IT = k gcd n iff ( IT divides k & IT divides n & ( for m being Nat st m divides k & m divides n holds
m divides IT ) ) )
thus  ( IT = k gcd n implies ( IT divides k & IT divides n & ( for m being Nat st m divides k & m divides n holds
m divides IT ) ) ) by INT_2:def_2; ::_thesis: ( IT divides k & IT divides n & ( for m being Nat st m divides k & m divides n holds
m divides IT ) implies IT = k gcd n )
assume that
A1: IT divides k and
A2: IT divides n and
A3: for m being Nat st m divides k & m divides n holds
m divides IT ; ::_thesis: IT = k gcd n
 for m being Integer st m divides k & m divides n holds
m divides IT
proof
let m be Integer; ::_thesis: ( m divides k & m divides n implies m divides IT )
 m in INT by INT_1:def_2;
then consider i being Element of NAT  such that
A4: ( m = i or m = - i ) by INT_1:def_1;
assume that
A5: m divides k and
A6: m divides n ; ::_thesis: m divides IT
A7: i divides k by A4, A5, INT_2:10;
 i divides n by A4, A6, INT_2:10;
then  i divides IT by A3, A7;
hence  m divides IT by A4, INT_2:10; ::_thesis: verum
end;
hence  IT = k gcd n by A1, A2, INT_2:def_2; ::_thesis: verum
end;
end;

:: deftheorem Def5 defines gcd NAT_D:def_5_:_
 for k, n being Nat
for b3 being set holds
( b3 = k gcd n iff ( b3 divides k & b3 divides n & ( for m being Nat st m divides k & m divides n holds
m divides b3 ) ) );

definition
let k, n be Nat;
:: original: gcd
redefine funck gcd n ->  Element of NAT ;
coherence
 k gcd n is Element of NAT by ORDINAL1:def_12;
end;

scheme :: NAT_D:sch 1
Euklides{ F1( Nat) ->  Nat, F2() ->  Nat, F3() ->  Nat } :
 ex n being Element of NAT st
( F1(n) = F2() gcd F3() & F1((n + 1)) = 0 )
provided
A1: ( 0 < F3() & F3() < F2() ) and
A2: ( F1(0) = F2() & F1(1) = F3() ) and
A3: for n being Element of NAT holds F1((n + 2)) = F1(n) mod F1((n + 1))
proof
defpred S1[ Nat] means  ex n being Element of NAT st $1 = F1(n);
A4: ex k being Nat st S1[k] by A2;
A5: for k being Nat st k <> 0 & S1[k] holds
ex n being Nat st
( n < k & S1[n] )
proof
let k be Nat; ::_thesis: ( k <> 0 & S1[k] implies ex n being Nat st
( n < k & S1[n] ) )
assume that
A6: k <> 0 and
A7: ex n being Element of NAT st k = F1(n) ; ::_thesis: ex n being Nat st
( n < k & S1[n] )
consider n being Element of NAT  such that
A8: k = F1(n) by A7;
reconsider Q = F1((n + 1)) as Element of NAT by ORDINAL1:def_12;
A9: ( n = 0 implies Q < k ) by A1, A2, A8;
now__::_thesis:_(_ex_m_being_Nat_st_n_=_m_+_1_implies_(_F1((n_+_1))_<_k_&_ex_m_being_Element_of_NAT_st_F1((n_+_1))_=_F1(m)_)_)
given m being Nat such that A10: n = m + 1 ; ::_thesis: ( F1((n + 1)) < k & ex m being Element of NAT st F1((n + 1)) = F1(m) )
reconsider m1 = m as Element of NAT by ORDINAL1:def_12;
 F1((m1 + 2)) = F1(m1) mod F1((m1 + 1)) by A3;
hence  F1((n + 1)) < k by A6, A8, A10, Th1; ::_thesis: ex m being Element of NAT st F1((n + 1)) = F1(m)
take m = n + 1; ::_thesis: F1((n + 1)) = F1(m)
thus  F1((n + 1)) = F1(m) ; ::_thesis: verum
end;
hence  ex n being Nat st
( n < k & S1[n] ) by A9, NAT_1:6; ::_thesis: verum
end;
A11: S1[ 0 ] from NAT_1:sch_7(A4, A5);
defpred S2[ Nat] means  0 = F1($1);
A12: ex n being Nat st S2[n] by A11;
consider k being Nat such that
A13: ( S2[k] & ( for n being Nat st S2[n] holds
k <= n ) ) from NAT_1:sch_5(A12);
consider n being Nat such that
A14: k = n + 1 by A1, A2, A13, NAT_1:6;
reconsider n = n as Element of NAT by ORDINAL1:def_12;
take  n ; ::_thesis: ( F1(n) = F2() gcd F3() & F1((n + 1)) = 0 )
defpred S3[ Nat] means ( F1(n) divides F1($1) & F1(n) divides F1(($1 + 1)) );
 S3[n] by A13, A14, Th6;
then A15: ex k being Nat st S3[k] ;
A16: for k being Nat st k <> 0 & S3[k] holds
ex m being Nat st
( m < k & S3[m] )
proof
let l be Nat; ::_thesis: ( l <> 0 & S3[l] implies ex m being Nat st
( m < l & S3[m] ) )
assume that
A17: l <> 0 and
A18: F1(n) divides F1(l) and
A19: F1(n) divides F1((l + 1)) ; ::_thesis: ex m being Nat st
( m < l & S3[m] )
consider m being Nat such that
A20: l = m + 1 by A17, NAT_1:6;
reconsider m = m as Element of NAT by ORDINAL1:def_12;
take  m ; ::_thesis: ( m < l & S3[m] )
A21: m <= m + 1 by NAT_1:11;
 m <> m + 1 ;
hence  m < l by A20, A21, XXREAL_0:1; ::_thesis: S3[m]
A22: now__::_thesis:_(_F1((m_+_1))_=_0_implies_F1(n)_divides_F1(m)_)
assume A23: F1((m + 1)) = 0 ; ::_thesis: F1(n) divides F1(m)
now__::_thesis:_(_m_+_1_<>_k_implies_F1(n)_divides_F1(m)_)
assume A24: m + 1 <> k ; ::_thesis: F1(n) divides F1(m)
 k <= m + 1 by A13, A23;
then  k < m + 1 by A24, XXREAL_0:1;
then A25: k <= m by NAT_1:13;
defpred S4[ Nat] means ( k <= $1 implies F1($1) = 0 );
A26: S4[ 0 ] by A13;
A27: for m being Nat st S4[m] holds
S4[m + 1]
proof
let m be Nat; ::_thesis: ( S4[m] implies S4[m + 1] )
assume that
A28: ( k <= m implies F1(m) = 0 ) and
A29: k <= m + 1 ; ::_thesis: F1((m + 1)) = 0
now__::_thesis:_(_k_<>_m_+_1_implies_F1((m_+_1))_=_0_)
assume  k <> m + 1 ; ::_thesis: F1((m + 1)) = 0
then A30: k < m + 1 by A29, XXREAL_0:1;
then consider l being Nat such that
A31: m = l + 1 by A1, A2, A28, NAT_1:6, NAT_1:13;
reconsider l = l as Element of NAT by ORDINAL1:def_12;
 F1((l + 2)) = F1(l) mod F1((l + 1)) by A3;
hence  F1((m + 1)) = 0 by A28, A30, A31, Def2, NAT_1:13; ::_thesis: verum
end;
hence  F1((m + 1)) = 0 by A13; ::_thesis: verum
end;
 for m being Nat holds S4[m] from NAT_1:sch_2(A26, A27);
then  F1(m) = 0 by A25;
hence  F1(n) divides F1(m) by Th6; ::_thesis: verum
end;
hence  F1(n) divides F1(m) by A14; ::_thesis: verum
end;
now__::_thesis:_(_F1((m_+_1))_<>_0_implies_F1(n)_divides_F1(m)_)
assume A32: F1((m + 1)) <> 0 ; ::_thesis: F1(n) divides F1(m)
 F1((m + 2)) = F1(m) mod F1((m + 1)) by A3;
then A33: F1(m) = (F1((m + 1)) * (F1(m) div F1((m + 1)))) + F1((m + 2)) by A32, INT_1:59;
 F1(n) divides F1((m + 1)) * (F1(m) div F1((m + 1))) by A18, A20, Th9;
hence  F1(n) divides F1(m) by A19, A20, A33, Th8; ::_thesis: verum
end;
hence  F1(n) divides F1(m) by A22; ::_thesis: F1(n) divides F1((m + 1))
thus  F1(n) divides F1((m + 1)) by A18, A20; ::_thesis: verum
end;
now__::_thesis:_(_F1(n)_divides_F2()_&_F1(n)_divides_F3()_&_(_for_m_being_Nat_st_m_divides_F2()_&_m_divides_F3()_holds_
m_divides_F1(n)_)_)
 S3[ 0 ] from NAT_1:sch_7(A15, A16);
hence  ( F1(n) divides F2() & F1(n) divides F3() ) by A2; ::_thesis: for m being Nat st m divides F2() & m divides F3() holds
m divides F1(n)
let m be Nat; ::_thesis: ( m divides F2() & m divides F3() implies m divides F1(n) )
defpred S4[ Nat] means ( m divides F1($1) & m divides F1(($1 + 1)) );
assume that
A34: m divides F2() and
A35: m divides F3() ; ::_thesis: m divides F1(n)
A36: S4[ 0 ] by A2, A34, A35;
A37: for k being Element of NAT st S4[k] holds
S4[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S4[k] implies S4[k + 1] )
assume that
A38: m divides F1(k) and
A39: m divides F1((k + 1)) ; ::_thesis: S4[k + 1]
thus  m divides F1((k + 1)) by A39; ::_thesis: m divides F1(((k + 1) + 1))
 F1((k + 2)) = F1(k) mod F1((k + 1)) by A3;
hence  m divides F1(((k + 1) + 1)) by A38, A39, Th11; ::_thesis: verum
end;
 for k being Element of NAT holds S4[k] from NAT_1:sch_1(A36, A37);
hence  m divides F1(n) ; ::_thesis: verum
end;
hence  F1(n) = F2() gcd F3() by Def5; ::_thesis: F1((n + 1)) = 0
thus  F1((n + 1)) = 0 by A13, A14; ::_thesis: verum
end;

theorem :: NAT_D:12
for n being Nat holds
( n mod 2 = 0 or n mod 2 = 1 )
proof
let n be Nat; ::_thesis: ( n mod 2 = 0 or n mod 2 = 1 )
assume A1: n mod 2 <> 0 ; ::_thesis: n mod 2 = 1
A2: 2 = 1 + 1 ;
 n mod 2 < 2 by Th1;
then A3: n mod 2 <= 1 by A2, NAT_1:13;
 n mod 2 >= 1 by A1, NAT_1:14;
hence  n mod 2 = 1 by A3, XXREAL_0:1; ::_thesis: verum
end;

theorem :: NAT_D:13
for k, n being Nat holds (k * n) mod k = 0
proof
let k, n be Nat; ::_thesis: (k * n) mod k = 0
percases ( k = 0 or k <> 0 ) ;
suppose k = 0 ; ::_thesis: (k * n) mod k = 0
hence  (k * n) mod k = 0 by Def2; ::_thesis: verum
end;
supposeA1: k <> 0 ; ::_thesis: (k * n) mod k = 0
 k * n = (k * n) + 0 ;
hence  (k * n) mod k = 0 by A1, Def2; ::_thesis: verum
end;
end;
end;

theorem :: NAT_D:14
for k being Nat st k > 1 holds
1 mod k = 1
proof
let k be Nat; ::_thesis: ( k > 1 implies 1 mod k = 1 )
assume A1: k > 1 ; ::_thesis: 1 mod k = 1
 1 = (k * 0) + 1 ;
hence  1 mod k = 1 by A1, Def2; ::_thesis: verum
end;

theorem :: NAT_D:15
for k, n, l, m being Nat st k mod n = 0 & l = k - (m * n) holds
l mod n = 0
proof
let k, n, l, m be Nat; ::_thesis: ( k mod n = 0 & l = k - (m * n) implies l mod n = 0 )
assume that
A1: k mod n = 0 and
A2: l = k - (m * n) ; ::_thesis: l mod n = 0
percases ( n = 0 or n <> 0 ) ;
suppose n = 0 ; ::_thesis: l mod n = 0
hence  l mod n = 0 by A1, A2; ::_thesis: verum
end;
suppose n <> 0 ; ::_thesis: l mod n = 0
then consider t being Nat such that
A3: k = (n * t) + 0 and
A4: 0 < n by A1, Def2;
A5: l = (n * (t - m)) + 0 by A2, A3;
now__::_thesis:_not_t_<_m_+_0
assume  t < m + 0 ; ::_thesis: contradiction
then  t - m < 0 by XREAL_1:19;
then  l < n * 0 by A4, A5, XREAL_1:68;
hence  contradiction ; ::_thesis: verum
end;
then  t - m is Element of NAT by NAT_1:21;
hence  l mod n = 0 by A4, A5, Def2; ::_thesis: verum
end;
end;
end;

theorem :: NAT_D:16
for n, k, l being Nat st n <> 0 & k mod n = 0 & l < n holds
(k + l) mod n = l
proof
let n, k, l be Nat; ::_thesis: ( n <> 0 & k mod n = 0 & l < n implies (k + l) mod n = l )
assume that
A1: n <> 0 and
A2: k mod n = 0 and
A3: l < n ; ::_thesis: (k + l) mod n = l
 ex t being Nat st
( k = (n * t) + 0 & 0 < n ) by A1, A2, Def2;
hence  (k + l) mod n = l by A3, Def2; ::_thesis: verum
end;

theorem :: NAT_D:17
for k, n, l being Nat st k mod n = 0 holds
(k + l) mod n = l mod n
proof
let k, n, l be Nat; ::_thesis: ( k mod n = 0 implies (k + l) mod n = l mod n )
assume A1: k mod n = 0 ; ::_thesis: (k + l) mod n = l mod n
percases ( n = 0 or n <> 0 ) ;
supposeA2: n = 0 ; ::_thesis: (k + l) mod n = l mod n
hence (k + l) mod n = 0 by Def2
.= l mod n by A2, Def2 ;
::_thesis: verum
end;
supposeA3: n <> 0 ; ::_thesis: (k + l) mod n = l mod n
then consider m being Nat such that
A4: k = (n * m) + 0 and
 0 < n by A1, Def2;
consider t being Nat such that
A5: l = (n * t) + (l mod n) and
A6: l mod n < n by A3, Def2;
 k + l = (n * (m + t)) + (l mod n) by A4, A5;
hence  (k + l) mod n = l mod n by A6, Def2; ::_thesis: verum
end;
end;
end;

theorem :: NAT_D:18
for k, n being Nat st k <> 0 holds
(k * n) div k = n
proof
let k, n be Nat; ::_thesis: ( k <> 0 implies (k * n) div k = n )
assume A1: k <> 0 ; ::_thesis: (k * n) div k = n
 k * n = (k * n) + 0 ;
hence  (k * n) div k = n by A1, Def1; ::_thesis: verum
end;

theorem :: NAT_D:19
for k, n, l being Nat st k mod n = 0 holds
(k + l) div n = (k div n) + (l div n)
proof
let k, n, l be Nat; ::_thesis: ( k mod n = 0 implies (k + l) div n = (k div n) + (l div n) )
assume A1: k mod n = 0 ; ::_thesis: (k + l) div n = (k div n) + (l div n)
percases ( n <> 0 or n = 0 ) ;
supposeA2: n <> 0 ; ::_thesis: (k + l) div n = (k div n) + (l div n)
then A3: k = (n * (k div n)) + 0 by A1, INT_1:59;
A4: ex t being Nat st
( l = (n * t) + (l mod n) & l mod n < n ) by A2, Def2;
 l = (n * (l div n)) + (l mod n) by A2, INT_1:59;
then  k + l = (n * ((k div n) + (l div n))) + (l mod n) by A3;
hence  (k + l) div n = (k div n) + (l div n) by A4, Def1; ::_thesis: verum
end;
supposeA5: n = 0 ; ::_thesis: (k + l) div n = (k div n) + (l div n)
then A6: (k + l) div n = 0 by Def1;
 k div n = 0 by A5, Def1;
hence  (k + l) div n = (k div n) + (l div n) by A5, A6, Def1; ::_thesis: verum
end;
end;
end;

begin

theorem :: NAT_D:20
for k, m being Nat st k <> 0 holds
(m * k) div k = m
proof
let k, m be Nat; ::_thesis: ( k <> 0 implies (m * k) div k = m )
assume  k <> 0 ; ::_thesis: (m * k) div k = m
then  ( ( m * k = (k * m) + 0 & 0 < k ) or ( m = 0 & k = 0 ) ) ;
hence  (m * k) div k = m by Def1; ::_thesis: verum
end;

theorem Th21: :: NAT_D:21
for m, n, k being Nat holds m mod n = ((n * k) + m) mod n
proof
let m, n, k be Nat; ::_thesis: m mod n = ((n * k) + m) mod n
percases ( n > 0 or n = 0 ) ;
supposeA1: n > 0 ; ::_thesis: m mod n = ((n * k) + m) mod n
 for t being Nat st m mod n = t holds
((n * k) + m) mod n = t
proof
let t be Nat; ::_thesis: ( m mod n = t implies ((n * k) + m) mod n = t )
assume  m mod n = t ; ::_thesis: ((n * k) + m) mod n = t
then consider q being Nat such that
A2: m = (n * q) + t and
A3: t < n by A1, Def2;
 ex p being Nat st
( (n * k) + m = (n * p) + t & t < n )
proof
reconsider p = k + q as Element of NAT by ORDINAL1:def_12;
take  p ; ::_thesis: ( (n * k) + m = (n * p) + t & t < n )
thus  ( (n * k) + m = (n * p) + t & t < n ) by A2, A3; ::_thesis: verum
end;
hence  ((n * k) + m) mod n = t by Def2; ::_thesis: verum
end;
hence  m mod n = ((n * k) + m) mod n ; ::_thesis: verum
end;
suppose n = 0 ; ::_thesis: m mod n = ((n * k) + m) mod n
hence  m mod n = ((n * k) + m) mod n ; ::_thesis: verum
end;
end;
end;

theorem Th22: :: NAT_D:22
for p, s, n being Nat holds (p + s) mod n = ((p mod n) + s) mod n
proof
let p, s, n be Nat; ::_thesis: (p + s) mod n = ((p mod n) + s) mod n
percases ( n > 0 or n = 0 ) ;
suppose n > 0 ; ::_thesis: (p + s) mod n = ((p mod n) + s) mod n
then (p + s) mod n = (((n * (p div n)) + (p mod n)) + s) mod n by INT_1:59
.= ((n * (p div n)) + ((p mod n) + s)) mod n
.= ((p mod n) + s) mod n by Th21 ;
hence  (p + s) mod n = ((p mod n) + s) mod n ; ::_thesis: verum
end;
supposeA1: n = 0 ; ::_thesis: (p + s) mod n = ((p mod n) + s) mod n
hence (p + s) mod n = 0 by Def2
.= ((p mod n) + s) mod n by A1, Def2 ;
::_thesis: verum
end;
end;
end;

theorem :: NAT_D:23
for p, s, n being Nat holds (p + s) mod n = (p + (s mod n)) mod n by Th22;

theorem Th24: :: NAT_D:24
for k, n being Nat st k < n holds
k mod n = k
proof
let k, n be Nat; ::_thesis: ( k < n implies k mod n = k )
assume A1: k < n ; ::_thesis: k mod n = k
 k = (n * 0) + k ;
hence  k mod n = k by A1, Def2; ::_thesis: verum
end;

theorem Th25: :: NAT_D:25
for n being Nat holds n mod n = 0
proof
let n be Nat; ::_thesis: n mod n = 0
percases ( n > 0 or n = 0 ) ;
supposeA1: n > 0 ; ::_thesis: n mod n = 0
 n = (n * 1) + 0 ;
hence  n mod n = 0 by A1, Def2; ::_thesis: verum
end;
suppose n = 0 ; ::_thesis: n mod n = 0
hence  n mod n = 0 by Def2; ::_thesis: verum
end;
end;
end;

theorem :: NAT_D:26
for n being Nat holds 0 = 0 mod n
proof
let n be Nat; ::_thesis: 0 = 0 mod n
 ( n = 0 or n > 0 ) ;
hence  0 = 0 mod n by Def2, Th24; ::_thesis: verum
end;

theorem Th27: :: NAT_D:27
for i, j being Nat st i < j holds
i div j = 0
proof
let i, j be Nat; ::_thesis: ( i < j implies i div j = 0 )
assume A1: i < j ; ::_thesis: i div j = 0
percases ( ex j1 being Nat st
( i = (j * (i div j)) + j1 & j1 < j ) or ( i div j = 0 & j = 0 ) ) by Def1;
suppose ex j1 being Nat st
( i = (j * (i div j)) + j1 & j1 < j ) ; ::_thesis: i div j = 0
then consider j1 being Nat such that
A2: i = (j * (i div j)) + j1 and
 j1 < j ;
assume  i div j <> 0 ; ::_thesis: contradiction
then consider k being Nat such that
A3: i div j = k + 1 by NAT_1:6;
 i = j + ((j * k) + j1) by A2, A3;
hence  contradiction by A1, NAT_1:11; ::_thesis: verum
end;
suppose ( i div j = 0 & j = 0 ) ; ::_thesis: i div j = 0
hence  i div j = 0 ; ::_thesis: verum
end;
end;
end;

theorem Th28: :: NAT_D:28
for m, n being Nat st m > 0 holds
n gcd m = m gcd (n mod m)
proof
let m, n be Nat; ::_thesis: ( m > 0 implies n gcd m = m gcd (n mod m) )
set r = n mod m;
set x = n gcd m;
set y = m gcd (n mod m);
assume  m > 0 ; ::_thesis: n gcd m = m gcd (n mod m)
then consider t being Nat such that
A1: n = (m * t) + (n mod m) and
 n mod m < m by Def2;
reconsider t = t as Element of NAT by ORDINAL1:def_12;
A2: n gcd m divides n by Def5;
A3: n gcd m divides m by Def5;
then  n gcd m divides n mod m by A2, Th11;
then A4: n gcd m divides m gcd (n mod m) by A3, Def5;
A5: m gcd (n mod m) divides m by Def5;
A6: m gcd (n mod m) divides n mod m by Def5;
 m gcd (n mod m) divides m * t by A5, Th9;
then  m gcd (n mod m) divides n by A1, A6, Th8;
then  m gcd (n mod m) divides n gcd m by A5, Def5;
hence  n gcd m = m gcd (n mod m) by A4, Th5; ::_thesis: verum
end;

scheme :: NAT_D:sch 2
INDI{ F1() ->  Element of NAT , F2() ->  Element of NAT , P1[ set ] } :
 P1[F2()]
provided
A1: P1[ 0 ] and
A2: F1() > 0 and
A3: for i, j being Nat st P1[F1() * i] & j <> 0 & j <= F1() holds
P1[(F1() * i) + j]
proof
defpred S1[ Nat] means P1[F1() * $1];
A4: S1[ 0 ] by A1;
A5: now__::_thesis:_for_i_being_Nat_st_S1[i]_holds_
S1[i_+_1]
let i be Nat; ::_thesis: ( S1[i] implies S1[i + 1] )
assume A6: S1[i] ; ::_thesis: S1[i + 1]
 F1() * (i + 1) = (F1() * i) + F1() ;
hence  S1[i + 1] by A2, A3, A6; ::_thesis: verum
end;
A7: for i being Nat holds S1[i] from NAT_1:sch_2(A4, A5);
percases ( F2() mod F1() = 0 or F2() mod F1() <> 0 ) ;
suppose F2() mod F1() = 0 ; ::_thesis: P1[F2()]
then  F2() = (F1() * (F2() div F1())) + 0 by A2, INT_1:59;
hence  P1[F2()] by A7; ::_thesis: verum
end;
supposeA8: F2() mod F1() <> 0 ; ::_thesis: P1[F2()]
A9: F2() = (F1() * (F2() div F1())) + (F2() mod F1()) by A2, INT_1:59;
 F2() mod F1() <= F1() by A2, Th1;
hence  P1[F2()] by A3, A7, A8, A9; ::_thesis: verum
end;
end;
end;

theorem :: NAT_D:29
for i, j being Nat holds i * j = (i lcm j) * (i gcd j)
proof
let i, j be Nat; ::_thesis: i * j = (i lcm j) * (i gcd j)
A1: ( i <> 0 & j <> 0 implies i * j = (i lcm j) * (i gcd j) )
proof
assume that
A2: i <> 0 and
A3: j <> 0 ; ::_thesis: i * j = (i lcm j) * (i gcd j)
A4: ( i divides i implies i divides i * j ) by Th9;
 ( j divides j implies j divides j * i ) by Th9;
then  i lcm j divides i * j by A4, Def4;
then consider c being Nat such that
A5: i * j = (i lcm j) * c by Def3;
A6: i divides i lcm j by Def4;
A7: j divides i lcm j by Def4;
consider d being Nat such that
A8: i lcm j = i * d by A6, Def3;
consider e being Nat such that
A9: i lcm j = j * e by A7, Def3;
 i * j = i * (c * d) by A5, A8;
then A10: j = c * d by A2, XCMPLX_1:5;
 i * j = j * (c * e) by A5, A9;
then  i = c * e by A3, XCMPLX_1:5;
then A11: c divides i by Def3;
A12: c divides j by A10, Def3;
 for f being Nat st f divides i & f divides j holds
f divides c
proof
let f be Nat; ::_thesis: ( f divides i & f divides j implies f divides c )
assume that
A13: f divides i and
A14: f divides j ; ::_thesis: f divides c
consider g being Nat such that
A15: i = f * g by A13, Def3;
consider h being Nat such that
A16: j = f * h by A14, Def3;
A17: j * g = (g * h) * f by A16;
 i * h = (g * h) * f by A15;
then A18: i divides (g * h) * f by Def3;
 j divides (g * h) * f by A17, Def3;
then  i lcm j divides (g * h) * f by A18, Def4;
then consider z being Nat such that
A19: (g * h) * f = (i lcm j) * z by Def3;
A20: c * (i lcm j) = (g * (h * f)) * f by A5, A15, A16
.= ((i lcm j) * z) * f by A19
.= (z * f) * (i lcm j) ;
 i lcm j <> 0 by A2, A3, INT_2:4;
then  c = f * z by A20, XCMPLX_1:5;
hence  f divides c by Def3; ::_thesis: verum
end;
hence  i * j = (i lcm j) * (i gcd j) by A5, A11, A12, Def5; ::_thesis: verum
end;
 ( ( i = 0 or j = 0 ) implies i * j = (i lcm j) * (i gcd j) )
proof
assume A21: ( i = 0 or j = 0 ) ; ::_thesis: i * j = (i lcm j) * (i gcd j)
then i * j = 0 * (i gcd j)
.= (i lcm j) * (i gcd j) by A21, INT_2:4 ;
hence  i * j = (i lcm j) * (i gcd j) ; ::_thesis: verum
end;
hence  i * j = (i lcm j) * (i gcd j) by A1; ::_thesis: verum
end;

theorem :: NAT_D:30
for i, j being Integer st i >= 0 & j > 0 holds
i gcd j = j gcd (i mod j)
proof
let i, j be Integer; ::_thesis: ( i >= 0 & j > 0 implies i gcd j = j gcd (i mod j) )
assume that
A1: i >= 0 and
A2: j > 0 ; ::_thesis: i gcd j = j gcd (i mod j)
A3: abs j > 0 by A2, ABSVALUE:def_1;
thus i gcd j = (abs i) gcd (abs j) by INT_2:34
.= (abs j) gcd ((abs i) mod (abs j)) by A3, Th28
.= (abs j) gcd (abs ((abs i) mod (abs j))) by ABSVALUE:def_1
.= j gcd ((abs i) mod (abs j)) by INT_2:34
.= j gcd (i mod j) by A1, A2, INT_2:32 ; ::_thesis: verum
end;

theorem :: NAT_D:31
for i being Nat holds i lcm i = i
proof
let i be Nat; ::_thesis: i lcm i = i
 for m being Nat st i divides m & i divides m holds
i divides m ;
hence  i lcm i = i by Def4; ::_thesis: verum
end;

theorem :: NAT_D:32
for i being Nat holds i gcd i = i
proof
let i be Nat; ::_thesis: i gcd i = i
 for m being Nat st m divides i & m divides i holds
m divides i ;
hence  i gcd i = i by Def5; ::_thesis: verum
end;

theorem :: NAT_D:33
for i, j being Nat st i < j & i <> 0 holds
not i / j is integer
proof
let i, j be Nat; ::_thesis: ( i < j & i <> 0 implies not i / j is integer )
assume that
A1: i < j and
A2: i <> 0 ; ::_thesis: not i / j is integer
assume  i / j is integer ; ::_thesis: contradiction
then reconsider r = i / j as Integer ;
r = [\r/] by INT_1:25
.= i div j by INT_1:def_9 ;
hence  contradiction by A1, A2, Th27, XCMPLX_1:50; ::_thesis: verum
end;

definition
let i, j be Nat;
:: original: -'
redefine funci -' j ->  Element of NAT ;
coherence
 i -' j is Element of NAT
proof
 ( ( i -' j = i - j & 0 <= i -' j ) or i -' j = 0 ) by XREAL_0:def_2;
hence  i -' j is Element of NAT by INT_1:3; ::_thesis: verum
end;
end;

theorem Th34: :: NAT_D:34
for i, j being Nat holds (i + j) -' j = i
proof
let i, j be Nat; ::_thesis: (i + j) -' j = i
 (i + j) - j >= 0 ;
hence  (i + j) -' j = i by XREAL_0:def_2; ::_thesis: verum
end;


theorem Th35: :: NAT_D:35
for a, b being Nat holds a -' b <= a
proof
let a, b be Nat; ::_thesis: a -' b <= a
 a - b <= a - 0 by XREAL_1:230;
hence  a -' b <= a by XREAL_0:def_2; ::_thesis: verum
end;


theorem Th36: :: NAT_D:36
for n, i being Nat st n -' i = 0 holds
n <= i
proof
let n, i be Nat; ::_thesis: ( n -' i = 0 implies n <= i )
assume A1: n -' i = 0 ; ::_thesis: n <= i
assume  i < n ; ::_thesis: contradiction
then  i + 1 <= n by NAT_1:13;
then  (i + 1) - i <= n - i by XREAL_1:9;
hence  contradiction by A1, XREAL_0:def_2; ::_thesis: verum
end;

theorem :: NAT_D:37
for i, j, k being Nat st i <= j holds
(j + k) -' i = (j + k) - i by NAT_1:12, XREAL_1:233;

theorem :: NAT_D:38
for i, j, k being Nat st i <= j holds
(j + k) -' i = (j -' i) + k
proof
let i, j, k be Nat; ::_thesis: ( i <= j implies (j + k) -' i = (j -' i) + k )
assume A1: i <= j ; ::_thesis: (j + k) -' i = (j -' i) + k
hence (j + k) -' i = (j + k) - i by NAT_1:12, XREAL_1:233
.= (j - i) + k
.= (j -' i) + k by A1, XREAL_1:233 ;
::_thesis: verum
end;


theorem Th39: :: NAT_D:39
for i, i1 being Nat st ( i -' i1 >= 1 or i - i1 >= 1 ) holds
i -' i1 = i - i1
proof
let i, i1 be Nat; ::_thesis: ( ( i -' i1 >= 1 or i - i1 >= 1 ) implies i -' i1 = i - i1 )
assume A1: ( i -' i1 >= 1 or i - i1 >= 1 ) ; ::_thesis: i -' i1 = i - i1
percases ( i -' i1 >= 1 or i - i1 >= 1 ) by A1;
suppose i -' i1 >= 1 ; ::_thesis: i -' i1 = i - i1
hence  i -' i1 = i - i1 by XREAL_0:def_2; ::_thesis: verum
end;
suppose i - i1 >= 1 ; ::_thesis: i -' i1 = i - i1
hence  i -' i1 = i - i1 by XREAL_0:def_2; ::_thesis: verum
end;
end;
end;

theorem :: NAT_D:40
for n being Nat holds n -' 0 = n
proof
let n be Nat; ::_thesis: n -' 0 = n
n -' 0 = n - 0 by XREAL_0:def_2
.= n ;
hence  n -' 0 = n ; ::_thesis: verum
end;

theorem :: NAT_D:41
for i1, i2, n being Nat st i1 <= i2 holds
n -' i2 <= n -' i1
proof
let i1, i2, n be Nat; ::_thesis: ( i1 <= i2 implies n -' i2 <= n -' i1 )
assume A1: i1 <= i2 ; ::_thesis: n -' i2 <= n -' i1
percases ( i2 <= n or i2 > n ) ;
supposeA2: i2 <= n ; ::_thesis: n -' i2 <= n -' i1
then A3: n -' i1 = n - i1 by A1, XREAL_1:233, XXREAL_0:2;
 n -' i2 = n - i2 by A2, XREAL_1:233;
hence  n -' i2 <= n -' i1 by A1, A3, XREAL_1:10; ::_thesis: verum
end;
suppose i2 > n ; ::_thesis: n -' i2 <= n -' i1
then  n - i2 < 0 by XREAL_1:49;
hence  n -' i2 <= n -' i1 by XREAL_0:def_2; ::_thesis: verum
end;
end;
end;

theorem Th42: :: NAT_D:42
for i1, i2, n being Nat st i1 <= i2 holds
i1 -' n <= i2 -' n
proof
let i1, i2, n be Nat; ::_thesis: ( i1 <= i2 implies i1 -' n <= i2 -' n )
assume A1: i1 <= i2 ; ::_thesis: i1 -' n <= i2 -' n
percases ( i1 - n >= 0 or i1 - n < 0 ) ;
suppose i1 - n >= 0 ; ::_thesis: i1 -' n <= i2 -' n
then A2: i1 -' n = i1 - n by XREAL_0:def_2;
 i1 - n <= i2 - n by A1, XREAL_1:9;
hence  i1 -' n <= i2 -' n by A2, XREAL_0:def_2; ::_thesis: verum
end;
suppose i1 - n < 0 ; ::_thesis: i1 -' n <= i2 -' n
hence  i1 -' n <= i2 -' n by XREAL_0:def_2; ::_thesis: verum
end;
end;
end;

theorem Th43: :: NAT_D:43
for i, i1 being Nat st ( i -' i1 >= 1 or i - i1 >= 1 ) holds
(i -' i1) + i1 = i
proof
let i, i1 be Nat; ::_thesis: ( ( i -' i1 >= 1 or i - i1 >= 1 ) implies (i -' i1) + i1 = i )
assume  ( i -' i1 >= 1 or i - i1 >= 1 ) ; ::_thesis: (i -' i1) + i1 = i
then (i -' i1) + i1 = (i - i1) + i1 by Th39
.= i ;
hence  (i -' i1) + i1 = i ; ::_thesis: verum
end;

theorem :: NAT_D:44
for i1, i2 being Nat st i1 <= i2 holds
i1 -' 1 <= i2
proof
let i1, i2 be Nat; ::_thesis: ( i1 <= i2 implies i1 -' 1 <= i2 )
assume A1: i1 <= i2 ; ::_thesis: i1 -' 1 <= i2
percases ( i1 - 1 >= 0 or i1 - 1 < 0 ) ;
suppose i1 - 1 >= 0 ; ::_thesis: i1 -' 1 <= i2
then  i1 -' 1 = i1 - 1 by XREAL_0:def_2;
then  i1 -' 1 <= (i1 - 1) + 1 by NAT_1:12;
hence  i1 -' 1 <= i2 by A1, XXREAL_0:2; ::_thesis: verum
end;
suppose i1 - 1 < 0 ; ::_thesis: i1 -' 1 <= i2
hence  i1 -' 1 <= i2 by XREAL_0:def_2; ::_thesis: verum
end;
end;
end;

theorem Th45: :: NAT_D:45
for i being Nat holds i -' 2 = (i -' 1) -' 1
proof
let i be Nat; ::_thesis: i -' 2 = (i -' 1) -' 1
percases ( i >= 2 or i < 2 ) ;
supposeA1: i >= 2 ; ::_thesis: i -' 2 = (i -' 1) -' 1
then  1 <= i by XXREAL_0:2;
then  i - 1 >= 0 by XREAL_1:48;
then A2: i -' 1 = i - 1 by XREAL_0:def_2;
 i - 1 >= (1 + 1) - 1 by A1, XREAL_1:9;
then  (i - 1) - 1 >= 1 - 1 by XREAL_1:9;
then  (i -' 1) -' 1 = i - 2 by A2, XREAL_0:def_2;
hence  i -' 2 = (i -' 1) -' 1 by XREAL_0:def_2; ::_thesis: verum
end;
supposeA3: i < 2 ; ::_thesis: i -' 2 = (i -' 1) -' 1
then  i - 2 < 2 - 2 by XREAL_1:9;
then A4: i -' 2 = 0 by XREAL_0:def_2;
A5: (i + 1) - 1 <= (1 + 1) - 1 by A3, NAT_1:13;
now__::_thesis:_(_(_1_<=_i_&_i_-'_2_=_(i_-'_1)_-'_1_)_or_(_i_<_1_&_i_-'_2_=_(i_-'_1)_-'_1_)_)
percases ( 1 <= i or i < 1 ) ;
case 1 <= i ; ::_thesis: i -' 2 = (i -' 1) -' 1
then  i = 1 by A5, XXREAL_0:1;
then  (i -' 1) -' 1 = 0 -' 1 by XREAL_1:232;
hence  i -' 2 = (i -' 1) -' 1 by A4, Th35; ::_thesis: verum
end;
case i < 1 ; ::_thesis: i -' 2 = (i -' 1) -' 1
then  i - 1 < 1 - 1 by XREAL_1:9;
then  (i -' 1) -' 1 = 0 -' 1 by XREAL_0:def_2;
hence  i -' 2 = (i -' 1) -' 1 by A4, Th35; ::_thesis: verum
end;
end;
end;
hence  i -' 2 = (i -' 1) -' 1 ; ::_thesis: verum
end;
end;
end;

theorem Th46: :: NAT_D:46
for i1, i2 being Nat st i1 + 1 <= i2 holds
( i1 -' 1 < i2 & i1 -' 2 < i2 & i1 <= i2 )
proof
let i1, i2 be Nat; ::_thesis: ( i1 + 1 <= i2 implies ( i1 -' 1 < i2 & i1 -' 2 < i2 & i1 <= i2 ) )
assume A1: i1 + 1 <= i2 ; ::_thesis: ( i1 -' 1 < i2 & i1 -' 2 < i2 & i1 <= i2 )
then A2: i1 < i2 by NAT_1:13;
 i1 -' 1 <= i1 by Th35;
hence A3: i1 -' 1 < i2 by A2, XXREAL_0:2; ::_thesis: ( i1 -' 2 < i2 & i1 <= i2 )
A4: (i1 -' 1) -' 1 = i1 -' 2 by Th45;
 (i1 -' 1) -' 1 <= i1 -' 1 by Th35;
hence  i1 -' 2 < i2 by A3, A4, XXREAL_0:2; ::_thesis: i1 <= i2
thus  i1 <= i2 by A1, NAT_1:13; ::_thesis: verum
end;

theorem :: NAT_D:47
for i1, i2 being Nat st ( i1 + 2 <= i2 or (i1 + 1) + 1 <= i2 ) holds
( i1 + 1 < i2 & (i1 + 1) -' 1 < i2 & (i1 + 1) -' 2 < i2 & i1 + 1 <= i2 & (i1 -' 1) + 1 < i2 & ((i1 -' 1) + 1) -' 1 < i2 & i1 < i2 & i1 -' 1 < i2 & i1 -' 2 < i2 & i1 <= i2 )
proof
let i1, i2 be Nat; ::_thesis: ( ( i1 + 2 <= i2 or (i1 + 1) + 1 <= i2 ) implies ( i1 + 1 < i2 & (i1 + 1) -' 1 < i2 & (i1 + 1) -' 2 < i2 & i1 + 1 <= i2 & (i1 -' 1) + 1 < i2 & ((i1 -' 1) + 1) -' 1 < i2 & i1 < i2 & i1 -' 1 < i2 & i1 -' 2 < i2 & i1 <= i2 ) )
assume  ( i1 + 2 <= i2 or (i1 + 1) + 1 <= i2 ) ; ::_thesis: ( i1 + 1 < i2 & (i1 + 1) -' 1 < i2 & (i1 + 1) -' 2 < i2 & i1 + 1 <= i2 & (i1 -' 1) + 1 < i2 & ((i1 -' 1) + 1) -' 1 < i2 & i1 < i2 & i1 -' 1 < i2 & i1 -' 2 < i2 & i1 <= i2 )
then  (i1 + 1) + 1 <= i2 ;
hence A1: ( i1 + 1 < i2 & (i1 + 1) -' 1 < i2 & (i1 + 1) -' 2 < i2 & i1 + 1 <= i2 ) by Th46, NAT_1:13; ::_thesis: ( (i1 -' 1) + 1 < i2 & ((i1 -' 1) + 1) -' 1 < i2 & i1 < i2 & i1 -' 1 < i2 & i1 -' 2 < i2 & i1 <= i2 )
 i1 -' 1 <= i1 by Th35;
then  (i1 -' 1) + 1 <= i1 + 1 by XREAL_1:6;
then A2: (i1 -' 1) + 1 < i2 by A1, XXREAL_0:2;
 ((i1 -' 1) + 1) -' 1 <= (i1 -' 1) + 1 by Th35;
hence  ( (i1 -' 1) + 1 < i2 & ((i1 -' 1) + 1) -' 1 < i2 ) by A2, XXREAL_0:2; ::_thesis: ( i1 < i2 & i1 -' 1 < i2 & i1 -' 2 < i2 & i1 <= i2 )
thus  ( i1 < i2 & i1 -' 1 < i2 & i1 -' 2 < i2 & i1 <= i2 ) by A1, Th46, NAT_1:13; ::_thesis: verum
end;

theorem :: NAT_D:48
for i1, i2 being Nat st ( i1 <= i2 or i1 <= i2 -' 1 ) holds
( i1 < i2 + 1 & i1 <= i2 + 1 & i1 < (i2 + 1) + 1 & i1 <= (i2 + 1) + 1 & i1 < i2 + 2 & i1 <= i2 + 2 )
proof
let i1, i2 be Nat; ::_thesis: ( ( i1 <= i2 or i1 <= i2 -' 1 ) implies ( i1 < i2 + 1 & i1 <= i2 + 1 & i1 < (i2 + 1) + 1 & i1 <= (i2 + 1) + 1 & i1 < i2 + 2 & i1 <= i2 + 2 ) )
assume A1: ( i1 <= i2 or i1 <= i2 -' 1 ) ; ::_thesis: ( i1 < i2 + 1 & i1 <= i2 + 1 & i1 < (i2 + 1) + 1 & i1 <= (i2 + 1) + 1 & i1 < i2 + 2 & i1 <= i2 + 2 )
A2: now__::_thesis:_(_i1_<=_i2_implies_(_i1_<_i2_+_1_&_i1_<=_i2_+_1_&_i1_<_(i2_+_1)_+_1_&_i1_<=_(i2_+_1)_+_1_&_i1_<_i2_+_2_&_i1_<=_i2_+_2_)_)
assume  i1 <= i2 ; ::_thesis: ( i1 < i2 + 1 & i1 <= i2 + 1 & i1 < (i2 + 1) + 1 & i1 <= (i2 + 1) + 1 & i1 < i2 + 2 & i1 <= i2 + 2 )
then A3: i1 < i2 + 1 by NAT_1:13;
 (i2 + 1) + 1 = i2 + (1 + 1) ;
hence  ( i1 < i2 + 1 & i1 <= i2 + 1 & i1 < (i2 + 1) + 1 & i1 <= (i2 + 1) + 1 & i1 < i2 + 2 & i1 <= i2 + 2 ) by A3, NAT_1:13; ::_thesis: verum
end;
now__::_thesis:_(_i1_<=_i2_-'_1_implies_(_i1_<_i2_+_1_&_i1_<=_i2_+_1_&_i1_<_(i2_+_1)_+_1_&_i1_<=_(i2_+_1)_+_1_&_i1_<_i2_+_2_&_i1_<=_i2_+_2_)_)
assume A4: i1 <= i2 -' 1 ; ::_thesis: ( i1 < i2 + 1 & i1 <= i2 + 1 & i1 < (i2 + 1) + 1 & i1 <= (i2 + 1) + 1 & i1 < i2 + 2 & i1 <= i2 + 2 )
 i2 -' 1 <= i2 by Th35;
hence  ( i1 < i2 + 1 & i1 <= i2 + 1 & i1 < (i2 + 1) + 1 & i1 <= (i2 + 1) + 1 & i1 < i2 + 2 & i1 <= i2 + 2 ) by A2, A4, XXREAL_0:2; ::_thesis: verum
end;
hence  ( i1 < i2 + 1 & i1 <= i2 + 1 & i1 < (i2 + 1) + 1 & i1 <= (i2 + 1) + 1 & i1 < i2 + 2 & i1 <= i2 + 2 ) by A1, A2; ::_thesis: verum
end;

theorem :: NAT_D:49
for i1, i2 being Nat st ( i1 < i2 or i1 + 1 <= i2 ) holds
i1 <= i2 -' 1
proof
let i1, i2 be Nat; ::_thesis: ( ( i1 < i2 or i1 + 1 <= i2 ) implies i1 <= i2 -' 1 )
assume A1: ( i1 < i2 or i1 + 1 <= i2 ) ; ::_thesis: i1 <= i2 -' 1
percases ( i1 < i2 or i1 + 1 <= i2 ) by A1;
supposeA2: i1 < i2 ; ::_thesis: i1 <= i2 -' 1
then  i1 + 1 <= i2 by NAT_1:13;
then A3: (i1 + 1) - 1 <= i2 - 1 by XREAL_1:9;
 0 + 1 <= i2 by A2, NAT_1:13;
hence  i1 <= i2 -' 1 by A3, XREAL_1:233; ::_thesis: verum
end;
supposeA4: i1 + 1 <= i2 ; ::_thesis: i1 <= i2 -' 1
then A5: (i1 + 1) - 1 <= i2 - 1 by XREAL_1:9;
 0 + 1 <= i2 by A4, NAT_1:13;
hence  i1 <= i2 -' 1 by A5, XREAL_1:233; ::_thesis: verum
end;
end;
end;

theorem Th50: :: NAT_D:50
for i, i1, i2 being Nat st i >= i1 holds
i >= i1 -' i2
proof
let i, i1, i2 be Nat; ::_thesis: ( i >= i1 implies i >= i1 -' i2 )
assume A1: i >= i1 ; ::_thesis: i >= i1 -' i2
 i1 >= i1 -' i2 by Th35;
hence  i >= i1 -' i2 by A1, XXREAL_0:2; ::_thesis: verum
end;

theorem :: NAT_D:51
for i, i1 being Nat st 1 <= i & 1 <= i1 -' i holds
i1 -' i < i1
proof
let i, i1 be Nat; ::_thesis: ( 1 <= i & 1 <= i1 -' i implies i1 -' i < i1 )
assume that
A1: 1 <= i and
A2: 1 <= i1 -' i ; ::_thesis: i1 -' i < i1
i1 - i = ((i1 -' i) + i) - i by A2, Th43
.= i1 -' i ;
hence  i1 -' i < i1 by A1, XREAL_1:231; ::_thesis: verum
end;

theorem Th52: :: NAT_D:52
for i, k, j being Nat st i -' k <= j holds
i <= j + k
proof
let i, k, j be Nat; ::_thesis: ( i -' k <= j implies i <= j + k )
assume A1: i -' k <= j ; ::_thesis: i <= j + k
percases ( i >= k or i <= k ) ;
supposeA2: i >= k ; ::_thesis: i <= j + k
 (i -' k) + k <= j + k by A1, XREAL_1:6;
hence  i <= j + k by A2, XREAL_1:235; ::_thesis: verum
end;
supposeA3: i <= k ; ::_thesis: i <= j + k
 k <= j + k by NAT_1:11;
hence  i <= j + k by A3, XXREAL_0:2; ::_thesis: verum
end;
end;
end;

theorem :: NAT_D:53
for i, j, k being Nat st i <= j + k holds
i -' k <= j
proof
let i, j, k be Nat; ::_thesis: ( i <= j + k implies i -' k <= j )
assume  i <= j + k ; ::_thesis: i -' k <= j
then  i -' k <= (j + k) -' k by Th42;
hence  i -' k <= j by Th34; ::_thesis: verum
end;

theorem :: NAT_D:54
for i, j, k being Nat st i <= j -' k & k <= j holds
i + k <= j
proof
let i, j, k be Nat; ::_thesis: ( i <= j -' k & k <= j implies i + k <= j )
assume that
A1: i <= j -' k and
A2: j >= k ; ::_thesis: i + k <= j
 i + k <= (j -' k) + k by A1, XREAL_1:6;
hence  i + k <= j by A2, XREAL_1:235; ::_thesis: verum
end;

theorem :: NAT_D:55
for j, k, i being Nat st j + k <= i holds
k <= i -' j
proof
let j, k, i be Nat; ::_thesis: ( j + k <= i implies k <= i -' j )
assume A1: j + k <= i ; ::_thesis: k <= i -' j
percases ( j + k = i or j + k < i ) by A1, XXREAL_0:1;
suppose j + k = i ; ::_thesis: k <= i -' j
hence  k <= i -' j by Th34; ::_thesis: verum
end;
suppose j + k < i ; ::_thesis: k <= i -' j
hence  k <= i -' j by Th52; ::_thesis: verum
end;
end;
end;

theorem :: NAT_D:56
for k, i, j being Nat st k <= i & i < j holds
i -' k < j -' k
proof
let k, i, j be Nat; ::_thesis: ( k <= i & i < j implies i -' k < j -' k )
assume that
A1: k <= i and
A2: i < j ; ::_thesis: i -' k < j -' k
 (i -' k) + k = i by A1, XREAL_1:235;
then  (i -' k) + k < (j -' k) + k by A1, A2, XREAL_1:235, XXREAL_0:2;
hence  i -' k < j -' k by XREAL_1:6; ::_thesis: verum
end;

theorem :: NAT_D:57
for i, j, k being Nat st i < j & k < j holds
i -' k < j -' k
proof
let i, j, k be Nat; ::_thesis: ( i < j & k < j implies i -' k < j -' k )
assume that
A1: i < j and
A2: k < j ; ::_thesis: i -' k < j -' k
percases ( k <= i or k > i ) ;
suppose k <= i ; ::_thesis: i -' k < j -' k
then A3: i -' k = i - k by XREAL_1:233;
 j -' k = j - k by A2, XREAL_1:233;
hence  i -' k < j -' k by A1, A3, XREAL_1:9; ::_thesis: verum
end;
suppose k > i ; ::_thesis: i -' k < j -' k
then  i - k < 0 by XREAL_1:49;
then A4: i -' k = 0 by XREAL_0:def_2;
 j -' k <> 0 by A2, Th36;
hence  i -' k < j -' k by A4; ::_thesis: verum
end;
end;
end;

theorem :: NAT_D:58
for i, j being Nat st i <= j holds
j -' (j -' i) = i
proof
let i, j be Nat; ::_thesis: ( i <= j implies j -' (j -' i) = i )
assume A1: i <= j ; ::_thesis: j -' (j -' i) = i
(j -' (j -' i)) + (j -' i) = j by Th50, XREAL_1:235
.= i + (j -' i) by A1, XREAL_1:235 ;
hence  j -' (j -' i) = i ; ::_thesis: verum
end;

theorem :: NAT_D:59
for n, k being Nat st n < k holds
(k -' (n + 1)) + 1 = k -' n
proof
let n, k be Nat; ::_thesis: ( n < k implies (k -' (n + 1)) + 1 = k -' n )
assume A1: n < k ; ::_thesis: (k -' (n + 1)) + 1 = k -' n
A2: k -' n = k - n by A1, XREAL_1:233;
 n + 1 <= k by A1, NAT_1:13;
then  k -' (n + 1) = k - (n + 1) by XREAL_1:233;
hence  (k -' (n + 1)) + 1 = k -' n by A2; ::_thesis: verum
end;

theorem :: NAT_D:60
for A being finite set holds
( A is trivial iff card A < 2 )
proof
let A be finite set ; ::_thesis: ( A is trivial iff card A < 2 )
hereby  ::_thesis: ( card A < 2 implies A is trivial )
assume A1: A is trivial ; ::_thesis: card A < 2
percases ( A is empty or not A is empty ) ;
suppose A is empty ; ::_thesis: card A < 2
hence  card A < 2 ; ::_thesis: verum
end;
suppose not A is empty ; ::_thesis: card A < 2
then  ex x being set st A = {x} by A1, ZFMISC_1:131;
then  card A = 1 by CARD_1:30;
hence  card A < 2 ; ::_thesis: verum
end;
end;
end;
assume A2: card A < 2 ; ::_thesis: A is trivial
percases ( card A = 0 or card A = 1 ) by A2, NAT_1:23;
suppose card A = 0 ; ::_thesis: A is trivial
hence  A is trivial ; ::_thesis: verum
end;
suppose card A = 1 ; ::_thesis: A is trivial
then  A is 1 -element by CARD_1:def_7;
hence  A is trivial ; ::_thesis: verum
end;
end;
end;

theorem Th61: :: NAT_D:61
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
let n, a, k be Integer; ::_thesis: ( ( n <> 0 implies (a + (n * k)) div n = (a div n) + k ) & (a + (n * k)) mod n = a mod n )
hereby  ::_thesis: (a + (n * k)) mod n = a mod n
assume A2: n <> 0 ; ::_thesis: (a + (n * k)) div n = (a div n) + k
thus (a + (n * k)) div n = [\((a + (n * k)) / n)/] by INT_1:def_9
.= [\((a + (n * k)) * (n "))/] by XCMPLX_0:def_9
.= [\((a * (n ")) + ((n * (n ")) * k))/]
.= [\((a * (n ")) + (1 * k))/] by A2, XCMPLX_0:def_7
.= [\(a * (n "))/] + k by INT_1:28
.= [\(a / n)/] + k by XCMPLX_0:def_9
.= (a div n) + k by INT_1:def_9 ; ::_thesis: verum
end;
percases ( n <> 0 or n = 0 ) ;
supposeA3: n <> 0 ; ::_thesis: (a + (n * k)) mod n = a mod n
hence (a + (n * k)) mod n = (a + (n * k)) - (((a div n) + k) * n) by A1, INT_1:def_10
.= a - ((a div n) * n)
.= a mod n by A3, INT_1:def_10 ;
::_thesis: verum
end;
suppose n = 0 ; ::_thesis: (a + (n * k)) mod n = a mod n
hence  (a + (n * k)) mod n = a mod n ; ::_thesis: verum
end;
end;
end;

theorem Th62: :: NAT_D:62
for n being Nat st n > 0 holds
for a being Integer holds
( a mod n >= 0 & a mod n < n )
proof
let n be Nat; ::_thesis: ( n > 0 implies for a being Integer holds
( a mod n >= 0 & a mod n < n ) )
assume A1: n > 0 ; ::_thesis: for a being Integer holds
( a mod n >= 0 & a mod n < n )
let a be Integer; ::_thesis: ( a mod n >= 0 & a mod n < n )
now__::_thesis:_(_0_<=_a_mod_n_&_not_a_mod_n_>=_n_)
 a div n = [\(a / n)/] by INT_1:def_9;
then  a div n <= a / n by INT_1:def_6;
then  (a div n) * n <= (a / n) * n by XREAL_1:64;
then  (a div n) * n <= (a * (n ")) * n by XCMPLX_0:def_9;
then  (a div n) * n <= a * ((n ") * n) ;
then  (a div n) * n <= a * 1 by A1, XCMPLX_0:def_7;
then  ((a div n) * n) - ((a div n) * n) <= a - ((a div n) * n) by XREAL_1:9;
hence  0 <= a mod n by INT_1:def_10; ::_thesis: not a mod n >= n
assume  a mod n >= n ; ::_thesis: contradiction
then  a - ((a div n) * n) >= n by A1, INT_1:def_10;
then  (a + (- ((a div n) * n))) + ((a div n) * n) >= n + ((a div n) * n) by XREAL_1:6;
then  a - n >= (n + ((a div n) * n)) - n by XREAL_1:9;
then  (a - n) * (n ") >= ((a div n) * n) * (n ") by XREAL_1:64;
then  (a - n) * (n ") >= (a div n) * (n * (n ")) ;
then  (a * (n ")) - (n * (n ")) >= (a div n) * 1 by A1, XCMPLX_0:def_7;
then  (a * (n ")) - 1 >= a div n by A1, XCMPLX_0:def_7;
then A2: (a / n) - 1 >= a div n by XCMPLX_0:def_9;
 a div n = [\(a / n)/] by INT_1:def_9;
hence  contradiction by A2, INT_1:def_6; ::_thesis: verum
end;
hence  ( a mod n >= 0 & a mod n < n ) ; ::_thesis: verum
end;

theorem Th63: :: NAT_D:63
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
let n, a be Integer; ::_thesis: ( ( 0 <= a & a < n implies a mod n = a ) & ( 0 > a & a >= - n implies a mod n = n + a ) )
percases ( n = 0 or n <> 0 ) ;
suppose n = 0 ; ::_thesis: ( ( 0 <= a & a < n implies a mod n = a ) & ( 0 > a & a >= - n implies a mod n = n + a ) )
hence  ( ( 0 <= a & a < n implies a mod n = a ) & ( 0 > a & a >= - n implies a mod n = n + a ) ) ; ::_thesis: verum
end;
supposeA1: n <> 0 ; ::_thesis: ( ( 0 <= a & a < n implies a mod n = a ) & ( 0 > a & a >= - n implies a mod n = n + a ) )
hereby  ::_thesis: ( 0 > a & a >= - n implies a mod n = n + a )
assume that
A2: 0 <= a and
A3: a < n ; ::_thesis: a mod n = a
reconsider aa = a as Element of NAT by A2, INT_1:3;
reconsider nn = n as Element of NAT by A2, A3, INT_1:3;
consider t being Nat such that
A4: aa = (nn * t) + (aa mod nn) and
 aa mod nn < nn by A1, Def2;
 t = 0
proof
assume  t <> 0 ; ::_thesis: contradiction
then  t >= 1 + 0 by INT_1:7;
then A5: t * n >= 1 * n by A2, A3, XREAL_1:64;
 (nn * t) + (aa mod nn) >= nn * t by NAT_1:11;
hence  contradiction by A3, A4, A5, XXREAL_0:2; ::_thesis: verum
end;
hence  a mod n = a by A4; ::_thesis: verum
end;
assume that
A6: 0 > a and
A7: a >= - n ; ::_thesis: a mod n = n + a
A8: n >= 0 by A6, A7;
A9: (a / n) - 1 < - 1
proof
assume  (a / n) - 1 >= - 1 ; ::_thesis: contradiction
then  ((a / n) - 1) + 1 >= (- 1) + 1 by XREAL_1:6;
then  a * (n ") >= 0 by XCMPLX_0:def_9;
then  (a * (n ")) * n >= 0 * n by A8;
then  a * ((n ") * n) >= 0 ;
then  a * 1 >= 0 by A1, XCMPLX_0:def_7;
hence  contradiction by A6; ::_thesis: verum
end;
 a * (n ") >= (- n) * (n ") by A7, A8, XREAL_1:64;
then  a / n >= - (n * (n ")) by XCMPLX_0:def_9;
then  - 1 <= a / n by A1, XCMPLX_0:def_7;
then  [\(a / n)/] = - 1 by A9, INT_1:def_6;
then A10: a div n = - 1 by INT_1:def_9;
 a mod n = a - ((a div n) * n) by A1, INT_1:def_10;
hence  a mod n = n + a by A10; ::_thesis: verum
end;
end;
end;

theorem Th64: :: NAT_D:64
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
let n, a, b be Integer; ::_thesis: ( ( 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 ) )
hereby  ::_thesis: ( a,b are_congruent_mod n implies a mod n = b mod n )
assume A1: n <> 0 ; ::_thesis: ( a mod n = b mod n implies a,b are_congruent_mod n )
assume  a mod n = b mod n ; ::_thesis: a,b are_congruent_mod n
then  a - ((a div n) * n) = b mod n by A1, INT_1:def_10;
then  a - ((a div n) * n) = b - ((b div n) * n) by A1, INT_1:def_10;
then  a - b = ((- (b div n)) + (a div n)) * n ;
then  n divides a - b by INT_1:def_3;
hence  a,b are_congruent_mod n by INT_2:15; ::_thesis: verum
end;
assume  a,b are_congruent_mod n ; ::_thesis: a mod n = b mod n
then  n divides a - b by INT_2:15;
then consider k being Integer such that
A2: n * k = a - b by INT_1:def_3;
 a = (n * k) + b by A2;
hence  a mod n = b mod n by Th61; ::_thesis: verum
end;

theorem :: NAT_D:65
for n being Nat
for a being Integer holds (a mod n) mod n = a mod n
proof
let n be Nat; ::_thesis: for a being Integer holds (a mod n) mod n = a mod n
let a be Integer; ::_thesis: (a mod n) mod n = a mod n
percases ( n = 0 or n <> 0 ) ;
supposeA1: n = 0 ; ::_thesis: (a mod n) mod n = a mod n
hence (a mod n) mod n = 0 by INT_1:def_10
.= a mod n by A1, INT_1:def_10 ;
::_thesis: verum
end;
suppose n <> 0 ; ::_thesis: (a mod n) mod n = a mod n
then  ( a mod n >= 0 & a mod n < n ) by Th62;
hence  (a mod n) mod n = a mod n by Th63; ::_thesis: verum
end;
end;
end;

theorem :: NAT_D:66
for n, a, b being Integer holds (a + b) mod n = ((a mod n) + (b mod n)) mod n
proof
let n, a, b be Integer; ::_thesis: (a + b) mod n = ((a mod n) + (b mod n)) mod n
percases ( n = 0 or n <> 0 ) ;
supposeA1: n = 0 ; ::_thesis: (a + b) mod n = ((a mod n) + (b mod n)) mod n
hence (a + b) mod n = 0 by INT_1:def_10
.= ((a mod n) + (b mod n)) mod n by A1, INT_1:def_10 ;
::_thesis: verum
end;
suppose n <> 0 ; ::_thesis: (a + b) mod n = ((a mod n) + (b mod n)) mod n
then  ( (a mod n) + ((a div n) * n) = (a - ((a div n) * n)) + ((a div n) * n) & (b mod n) + ((b div n) * n) = (b - ((b div n) * n)) + ((b div n) * n) ) by INT_1:def_10;
then  (a + b) - ((a mod n) + (b mod n)) = ((a div n) + (b div n)) * n ;
then  n divides (a + b) - ((a mod n) + (b mod n)) by INT_1:def_3;
then  a + b,(a mod n) + (b mod n) are_congruent_mod n by INT_2:15;
hence  (a + b) mod n = ((a mod n) + (b mod n)) mod n by Th64; ::_thesis: verum
end;
end;
end;

theorem :: NAT_D:67
for n, a, b being Integer holds (a * b) mod n = ((a mod n) * (b mod n)) mod n
proof
let n, a, b be Integer; ::_thesis: (a * b) mod n = ((a mod n) * (b mod n)) mod n
percases ( n = 0 or n <> 0 ) ;
supposeA1: n = 0 ; ::_thesis: (a * b) mod n = ((a mod n) * (b mod n)) mod n
hence (a * b) mod n = 0 by INT_1:def_10
.= ((a mod n) * (b mod n)) mod n by A1, INT_1:def_10 ;
::_thesis: verum
end;
suppose n <> 0 ; ::_thesis: (a * b) mod n = ((a mod n) * (b mod n)) mod n
then  ( (a mod n) + ((a div n) * n) = (a - ((a div n) * n)) + ((a div n) * n) & (b mod n) + ((b div n) * n) = (b - ((b div n) * n)) + ((b div n) * n) ) by INT_1:def_10;
then  (a * b) - ((a mod n) * (b mod n)) = (((a mod n) * (b div n)) + (((a div n) * (b mod n)) + (((a div n) * n) * (b div n)))) * n ;
then  n divides (a * b) - ((a mod n) * (b mod n)) by INT_1:def_3;
then  a * b,(a mod n) * (b mod n) are_congruent_mod n by INT_2:15;
hence  (a * b) mod n = ((a mod n) * (b mod n)) mod n by Th64; ::_thesis: verum
end;
end;
end;

theorem :: NAT_D:68
for a, b being Integer ex s, t being Integer st a gcd b = (s * a) + (t * b)
proof
let a, b be Integer; ::_thesis: ex s, t being Integer st a gcd b = (s * a) + (t * b)
A1: for a, b being Integer st a > 0 & b > 0 holds
ex s, t being Integer st a gcd b = (s * a) + (t * b)
proof
let a, b be Integer; ::_thesis: ( a > 0 & b > 0 implies ex s, t being Integer st a gcd b = (s * a) + (t * b) )
assume that
A2: a > 0 and
A3: b > 0 ; ::_thesis: ex s, t being Integer st a gcd b = (s * a) + (t * b)
reconsider a = a, b = b as Element of NAT by A2, A3, INT_1:3;
set M =  {  z where z is Element of NAT : ex s, t being Integer st z = (s * a) + (t * b)  }  ;
defpred S1[ Nat] means ( $1 in  {  z where z is Element of NAT : ex s, t being Integer st z = (s * a) + (t * b)  }  & $1 <> 0 );
 a = (1 * a) + (0 * b) ;
then A4: a in  {  z where z is Element of NAT : ex s, t being Integer st z = (s * a) + (t * b)  }  ;
then A5: ex k being Nat st S1[k] by A2;
consider g being Nat such that
A6: ( S1[g] & ( for n being Nat st S1[n] holds
g <= n ) ) from NAT_1:sch_5(A5);
set G =  {  zz where zz is Element of NAT : ex s being Element of NAT st zz = s * g  }  ;
 ex z being Element of NAT st
( z = g & ex s, t being Integer st z = (s * a) + (t * b) ) by A6;
then consider s, t being Integer such that
A7: g = (s * a) + (t * b) ;
A8: for x being set st x in  {  z where z is Element of NAT : ex s, t being Integer st z = (s * a) + (t * b)  }  holds
x in  {  zz where zz is Element of NAT : ex s being Element of NAT st zz = s * g  }
proof
let x be set ; ::_thesis: ( x in  {  z where z is Element of NAT : ex s, t being Integer st z = (s * a) + (t * b)  }  implies x in  {  zz where zz is Element of NAT : ex s being Element of NAT st zz = s * g  }  )
assume  x in  {  z where z is Element of NAT : ex s, t being Integer st z = (s * a) + (t * b)  }  ; ::_thesis: x in  {  zz where zz is Element of NAT : ex s being Element of NAT st zz = s * g  }
then consider x9 being Element of NAT  such that
A9: x9 = x and
A10: ex u, v being Integer st x9 = (u * a) + (v * b) ;
consider u, v being Integer such that
A11: x = (u * a) + (v * b) by A9, A10;
consider r being Nat such that
A12: x9 = (g * (x9 div g)) + r and
A13: r < g by A6, Def1;
A14: r in NAT by ORDINAL1:def_12;
r = x9 - (g * (x9 div g)) by A12
.= (a * (u + (- (s * (x9 div g))))) + (b * (v + (- (t * (x9 div g))))) by A7, A9, A11 ;
then  r in  {  z where z is Element of NAT : ex s, t being Integer st z = (s * a) + (t * b)  }  by A14;
then  r = 0 by A6, A13;
hence  x in  {  zz where zz is Element of NAT : ex s being Element of NAT st zz = s * g  }  by A9, A12; ::_thesis: verum
end;
 for x being set st x in  {  zz where zz is Element of NAT : ex s being Element of NAT st zz = s * g  }  holds
x in  {  z where z is Element of NAT : ex s, t being Integer st z = (s * a) + (t * b)  }
proof
let x be set ; ::_thesis: ( x in  {  zz where zz is Element of NAT : ex s being Element of NAT st zz = s * g  }  implies x in  {  z where z is Element of NAT : ex s, t being Integer st z = (s * a) + (t * b)  }  )
assume  x in  {  zz where zz is Element of NAT : ex s being Element of NAT st zz = s * g  }  ; ::_thesis: x in  {  z where z is Element of NAT : ex s, t being Integer st z = (s * a) + (t * b)  }
then A15: ex x9 being Element of NAT st
( x9 = x & ex u being Element of NAT st x9 = u * g ) ;
then consider u being Integer such that
A16: x = u * g ;
 x = ((u * s) * a) + ((u * t) * b) by A7, A16;
hence  x in  {  z where z is Element of NAT : ex s, t being Integer st z = (s * a) + (t * b)  }  by A15; ::_thesis: verum
end;
then A17:  {  zz where zz is Element of NAT : ex s being Element of NAT st zz = s * g  }  =  {  z where z is Element of NAT : ex s, t being Integer st z = (s * a) + (t * b)  }  by A8, TARSKI:1;
A18: abs b = b by ABSVALUE:def_1;
A19: abs a = a by ABSVALUE:def_1;
A20: for m being Nat st m divides abs a & m divides abs b holds
m divides g
proof
 ex g9 being Element of NAT st
( g9 = g & ex s, t being Integer st g9 = (s * a) + (t * b) ) by A6;
then consider s, t being Integer such that
A21: g = (s * a) + (t * b) ;
let m be Nat; ::_thesis: ( m divides abs a & m divides abs b implies m divides g )
assume that
A22: m divides abs a and
A23: m divides abs b ; ::_thesis: m divides g
consider u being Nat such that
A24: a = m * u by A19, A22, Def3;
consider v being Nat such that
A25: b = m * v by A18, A23, Def3;
A26: g = m * ((s * u) + (t * v)) by A24, A25, A21;
then  (s * u) + (t * v) >= 0 by A6;
then  (s * u) + (t * v) is Element of NAT by INT_1:3;
hence  m divides g by A26, Def3; ::_thesis: verum
end;
 b = (0 * a) + (1 * b) ;
then  b in  {  z where z is Element of NAT : ex s, t being Integer st z = (s * a) + (t * b)  }  ;
then  ex b9 being Element of NAT st
( b9 = b & ex t being Element of NAT st b9 = t * g ) by A17;
then A27: g divides abs b by A18, Def3;
 ex a9 being Element of NAT st
( a9 = a & ex s being Element of NAT st a9 = s * g ) by A4, A17;
then  g divides abs a by A19, Def3;
then g = (abs a) gcd (abs b) by A27, A20, Def5
.= a gcd b by INT_2:34 ;
hence  ex s, t being Integer st a gcd b = (s * a) + (t * b) by A7; ::_thesis: verum
end;
now__::_thesis:_(_(_(_a_=_0_or_b_=_0_)_&_ex_s,_t_being_Integer_st_a_gcd_b_=_(s_*_a)_+_(t_*_b)_)_or_(_a_<>_0_&_b_<>_0_&_ex_s,_t_being_Integer_st_a_gcd_b_=_(s_*_a)_+_(t_*_b)_)_)
percases ( a = 0 or b = 0 or ( a <> 0 & b <> 0 ) ) ;
caseA28: ( a = 0 or b = 0 ) ; ::_thesis: ex s, t being Integer st a gcd b = (s * a) + (t * b)
A29: for a, b being Integer st a = 0 holds
a gcd b = abs b
proof
let a, b be Integer; ::_thesis: ( a = 0 implies a gcd b = abs b )
assume  a = 0 ; ::_thesis: a gcd b = abs b
then  abs a = 0 by ABSVALUE:def_1;
then A30: abs b divides abs a by Th6;
 ( a gcd b = (abs a) gcd (abs b) & ( for m being Nat st m divides abs a & m divides abs b holds
m divides abs b ) ) by INT_2:34;
hence  a gcd b = abs b by A30, Def5; ::_thesis: verum
end;
now__::_thesis:_(_(_a_=_0_&_ex_s,_t_being_Integer_st_a_gcd_b_=_(s_*_a)_+_(t_*_b)_)_or_(_b_=_0_&_ex_s,_t_being_Integer_st_a_gcd_b_=_(s_*_a)_+_(t_*_b)_)_)
percases ( a = 0 or b = 0 ) by A28;
case a = 0 ; ::_thesis: ex s, t being Integer st a gcd b = (s * a) + (t * b)
then A31: a gcd b = abs b by A29;
now__::_thesis:_(_(_b_>=_0_&_a_gcd_b_=_(0_*_a)_+_(1_*_b)_)_or_(_b_<_0_&_a_gcd_b_=_(0_*_a)_+_((-_1)_*_b)_)_)
percases ( b >= 0 or b < 0 ) ;
case b >= 0 ; ::_thesis: a gcd b = (0 * a) + (1 * b)
hence  a gcd b = (0 * a) + (1 * b) by A31, ABSVALUE:def_1; ::_thesis: verum
end;
case b < 0 ; ::_thesis: a gcd b = (0 * a) + ((- 1) * b)
hence a gcd b = - (b * 1) by A31, ABSVALUE:def_1
.= (0 * a) + ((- 1) * b) ;
::_thesis: verum
end;
end;
end;
hence  ex s, t being Integer st a gcd b = (s * a) + (t * b) ; ::_thesis: verum
end;
case b = 0 ; ::_thesis: ex s, t being Integer st a gcd b = (s * a) + (t * b)
then A32: a gcd b = abs a by A29;
now__::_thesis:_(_(_a_>=_0_&_a_gcd_b_=_(1_*_a)_+_(0_*_b)_)_or_(_a_<_0_&_a_gcd_b_=_(0_*_b)_+_((-_1)_*_a)_)_)
percases ( a >= 0 or a < 0 ) ;
case a >= 0 ; ::_thesis: a gcd b = (1 * a) + (0 * b)
hence  a gcd b = (1 * a) + (0 * b) by A32, ABSVALUE:def_1; ::_thesis: verum
end;
case a < 0 ; ::_thesis: a gcd b = (0 * b) + ((- 1) * a)
hence a gcd b = - (a * 1) by A32, ABSVALUE:def_1
.= (0 * b) + ((- 1) * a) ;
::_thesis: verum
end;
end;
end;
hence  ex s, t being Integer st a gcd b = (s * a) + (t * b) ; ::_thesis: verum
end;
end;
end;
hence  ex s, t being Integer st a gcd b = (s * a) + (t * b) ; ::_thesis: verum
end;
caseA33: ( a <> 0 & b <> 0 ) ; ::_thesis: ex s, t being Integer st a gcd b = (s * a) + (t * b)
now__::_thesis:_(_(_a_>=_0_&_b_>=_0_&_ex_s,_t_being_Integer_st_a_gcd_b_=_(s_*_a)_+_(t_*_b)_)_or_(_a_<_0_&_b_>=_0_&_ex_s,_t_being_Integer_st_a_gcd_b_=_(s_*_a)_+_(t_*_b)_)_or_(_a_>=_0_&_b_<_0_&_ex_s,_t_being_Integer_st_a_gcd_b_=_(s_*_a)_+_(t_*_b)_)_or_(_a_<_0_&_b_<_0_&_ex_s,_t_being_Integer_st_a_gcd_b_=_(s_*_a)_+_(t_*_b)_)_)
percases ( ( a >= 0 & b >= 0 ) or ( a < 0 & b >= 0 ) or ( a >= 0 & b < 0 ) or ( a < 0 & b < 0 ) ) ;
case ( a >= 0 & b >= 0 ) ; ::_thesis: ex s, t being Integer st a gcd b = (s * a) + (t * b)
hence  ex s, t being Integer st a gcd b = (s * a) + (t * b) by A1, A33; ::_thesis: verum
end;
caseA34: ( a < 0 & b >= 0 ) ; ::_thesis: ex s, t being Integer st a gcd b = (s * a) + (t * b)
then  - a > 0 by XREAL_1:58;
then consider s, t being Integer such that
A35: (- a) gcd b = (s * (- a)) + (t * b) by A1, A33, A34;
A36: a gcd b = (abs a) gcd (abs b) by INT_2:34
.= (abs (- a)) gcd (abs b) by COMPLEX1:52
.= (- a) gcd b by INT_2:34 ;
 (s * (- a)) + (t * b) = ((- s) * a) + (t * b) ;
hence  ex s, t being Integer st a gcd b = (s * a) + (t * b) by A35, A36; ::_thesis: verum
end;
caseA37: ( a >= 0 & b < 0 ) ; ::_thesis: ex s, t being Integer st a gcd b = (s * a) + (t * b)
then  - b > 0 by XREAL_1:58;
then consider s, t being Integer such that
A38: a gcd (- b) = (s * a) + (t * (- b)) by A1, A33, A37;
A39: a gcd b = (abs a) gcd (abs b) by INT_2:34
.= (abs a) gcd (abs (- b)) by COMPLEX1:52
.= a gcd (- b) by INT_2:34 ;
 (s * a) + (t * (- b)) = (s * a) + ((- t) * b) ;
hence  ex s, t being Integer st a gcd b = (s * a) + (t * b) by A38, A39; ::_thesis: verum
end;
case ( a < 0 & b < 0 ) ; ::_thesis: ex s, t being Integer st a gcd b = (s * a) + (t * b)
then  ( - a > 0 & - b > 0 ) by XREAL_1:58;
then consider s, t being Integer such that
A40: (- a) gcd (- b) = (s * (- a)) + (t * (- b)) by A1;
A41: a gcd b = (abs a) gcd (abs b) by INT_2:34
.= (abs a) gcd (abs (- b)) by COMPLEX1:52
.= (abs (- a)) gcd (abs (- b)) by COMPLEX1:52
.= (- a) gcd (- b) by INT_2:34 ;
 (s * (- a)) + (t * (- b)) = ((- s) * a) + ((- t) * b) ;
hence  ex s, t being Integer st a gcd b = (s * a) + (t * b) by A40, A41; ::_thesis: verum
end;
end;
end;
hence  ex s, t being Integer st a gcd b = (s * a) + (t * b) ; ::_thesis: verum
end;
end;
end;
hence  ex s, t being Integer st a gcd b = (s * a) + (t * b) ; ::_thesis: verum
end;

theorem :: NAT_D:69
for n, k being Nat st n mod k = k - 1 holds
(n + 1) mod k = 0
proof
let n, k be Nat; ::_thesis: ( n mod k = k - 1 implies (n + 1) mod k = 0 )
percases ( k <> 0 or k = 0 ) ;
suppose k <> 0 ; ::_thesis: ( n mod k = k - 1 implies (n + 1) mod k = 0 )
then  k >= 1 by NAT_1:14;
then reconsider K = k - 1 as Element of NAT by INT_1:3, XREAL_1:48;
A1: K + 1 = k - 0 ;
assume  n mod k = k - 1 ; ::_thesis: (n + 1) mod k = 0
then  (n + 1) mod k = k mod k by A1, Th22;
hence  (n + 1) mod k = 0 by Th25; ::_thesis: verum
end;
suppose k = 0 ; ::_thesis: ( n mod k = k - 1 implies (n + 1) mod k = 0 )
hence  ( n mod k = k - 1 implies (n + 1) mod k = 0 ) ; ::_thesis: verum
end;
end;
end;

theorem :: NAT_D:70
for n, k being Nat st n mod k < k - 1 holds
(n + 1) mod k = (n mod k) + 1
proof
let n, k be Nat; ::_thesis: ( n mod k < k - 1 implies (n + 1) mod k = (n mod k) + 1 )
assume  n mod k < k - 1 ; ::_thesis: (n + 1) mod k = (n mod k) + 1
then A1: (n mod k) + 1 < k by XREAL_1:20;
 (n + 1) mod k = ((n mod k) + 1) mod k by Th22;
hence  (n + 1) mod k = (n mod k) + 1 by A1, Th24; ::_thesis: verum
end;