:: NAT_2 semantic presentation

begin


scheme :: NAT_2:sch 1
NonUniqPiFinRecExD{ F1() ->  non empty set , F2() ->  Element of F1(), F3() ->  Nat, P1[ set , set , set ] } :
 ex p being FinSequence of F1() st
( len p = F3() & ( p /. 1 = F2() or F3() = 0 ) & ( for n being Nat st 1 <= n & n < F3() holds
P1[n,p /. n,p /. (n + 1)] ) )
provided
A1: for n being Nat st 1 <= n & n < F3() holds
for x being Element of F1() ex y being Element of F1() st P1[n,x,y]
proof
A2: for n being Element of NAT st 1 <= n & n < F3() holds
for x being Element of F1() ex y being Element of F1() st P1[n,x,y] by A1;
consider p being FinSequence of F1() such that
A3: len p = F3() and
A4: ( p . 1 = F2() or F3() = 0 ) and
A5: for n being Element of NAT st 1 <= n & n < F3() holds
P1[n,p . n,p . (n + 1)] from RECDEF_1:sch_4(A2);
take  p ; ::_thesis: ( len p = F3() & ( p /. 1 = F2() or F3() = 0 ) & ( for n being Nat st 1 <= n & n < F3() holds
P1[n,p /. n,p /. (n + 1)] ) )
thus  len p = F3() by A3; ::_thesis: ( ( p /. 1 = F2() or F3() = 0 ) & ( for n being Nat st 1 <= n & n < F3() holds
P1[n,p /. n,p /. (n + 1)] ) )
now__::_thesis:_(_F3()_<>_0_implies_p_/._1_=_F2()_)
assume  F3() <> 0 ; ::_thesis: p /. 1 = F2()
then  F3() >= 0 + 1 by NAT_1:13;
hence  p /. 1 = F2() by A3, A4, FINSEQ_4:15; ::_thesis: verum
end;
hence  ( p /. 1 = F2() or F3() = 0 ) ; ::_thesis: for n being Nat st 1 <= n & n < F3() holds
P1[n,p /. n,p /. (n + 1)]
let n be Nat; ::_thesis: ( 1 <= n & n < F3() implies P1[n,p /. n,p /. (n + 1)] )
assume that
A6: 1 <= n and
A7: n < F3() ; ::_thesis: P1[n,p /. n,p /. (n + 1)]
 n + 1 <= F3() by A7, NAT_1:13;
then A8: p . (n + 1) = p /. (n + 1) by A3, FINSEQ_4:15, NAT_1:11;
 ( n in NAT & p . n = p /. n ) by A3, A6, A7, FINSEQ_4:15, ORDINAL1:def_12;
hence  P1[n,p /. n,p /. (n + 1)] by A5, A6, A7, A8; ::_thesis: verum
end;

theorem :: NAT_2:1
for x, y being real number st x >= 0 & y > 0 holds
x / ([\(x / y)/] + 1) < y
proof
let x, y be real number ; ::_thesis: ( x >= 0 & y > 0 implies x / ([\(x / y)/] + 1) < y )
assume that
A1: x >= 0 and
A2: y > 0 ; ::_thesis: x / ([\(x / y)/] + 1) < y
 (x / y) * y < ([\(x / y)/] + 1) * y by A2, INT_1:29, XREAL_1:68;
then A3: x < ([\(x / y)/] + 1) * y by A2, XCMPLX_1:87;
 [\(x / y)/] >= 0 by A1, A2, INT_1:53;
hence  x / ([\(x / y)/] + 1) < y by A3, XREAL_1:83; ::_thesis: verum
end;

begin

theorem Th2: :: NAT_2:2
for n being Nat holds 0 div n = 0
proof
let n be Nat; ::_thesis: 0 div n = 0
now__::_thesis:_0_div_n_=_0
percases ( ex t being Nat st
( 0 = (n * (0 div n)) + t & t < n ) or ( 0 div n = 0 & n = 0 ) ) by NAT_D:def_1;
supposeA1: ex t being Nat st
( 0 = (n * (0 div n)) + t & t < n ) ; ::_thesis: 0 div n = 0
then  n * (0 div n) = 0 ;
hence  0 div n = 0 by A1, XCMPLX_1:6; ::_thesis: verum
end;
suppose ( 0 div n = 0 & n = 0 ) ; ::_thesis: 0 div n = 0
hence  0 div n = 0 ; ::_thesis: verum
end;
end;
end;
hence  0 div n = 0 ; ::_thesis: verum
end;

theorem :: NAT_2:3
for n being non empty Nat holds n div n = 1
proof
let n be non empty Nat; ::_thesis: n div n = 1
 (n * 1) div n = 1 by NAT_D:18;
hence  n div n = 1 ; ::_thesis: verum
end;

theorem :: NAT_2:4
for n being Nat holds n div 1 = n
proof
let n be Nat; ::_thesis: n div 1 = n
 n = (1 * n) + 0 ;
hence  n div 1 = n by NAT_D:def_1; ::_thesis: verum
end;

theorem :: NAT_2:5
for i, j, k, l being Nat st i <= j & k <= j & i = (j -' k) + l holds
k = (j -' i) + l
proof
let i, j, k, l be Nat; ::_thesis: ( i <= j & k <= j & i = (j -' k) + l implies k = (j -' i) + l )
assume that
A1: i <= j and
A2: ( k <= j & i = (j -' k) + l ) ; ::_thesis: k = (j -' i) + l
 i - l = j - k by A2, XREAL_1:233;
hence k = (j - i) + l
.= (j -' i) + l by A1, XREAL_1:233 ;
::_thesis: verum
end;

theorem :: NAT_2:6
for i, n being Nat st i in Seg n holds
(n -' i) + 1 in Seg n
proof
let i, n be Nat; ::_thesis: ( i in Seg n implies (n -' i) + 1 in Seg n )
A1: 1 <= (n -' i) + 1 by NAT_1:11;
assume A2: i in Seg n ; ::_thesis: (n -' i) + 1 in Seg n
then  1 <= i by FINSEQ_1:1;
then  n - i <= n - 1 by XREAL_1:13;
then A3: (n - i) + 1 <= n by XREAL_1:19;
 i <= n by A2, FINSEQ_1:1;
then  (n -' i) + 1 <= n by A3, XREAL_1:233;
hence  (n -' i) + 1 in Seg n by A1, FINSEQ_1:1; ::_thesis: verum
end;

theorem :: NAT_2:7
for j, i being Nat st j < i holds
(i -' (j + 1)) + 1 = i -' j
proof
let j, i be Nat; ::_thesis: ( j < i implies (i -' (j + 1)) + 1 = i -' j )
assume A1: j < i ; ::_thesis: (i -' (j + 1)) + 1 = i -' j
then  j + 1 <= i by NAT_1:13;
hence (i -' (j + 1)) + 1 = (i - (j + 1)) + 1 by XREAL_1:233
.= i - j
.= i -' j by A1, XREAL_1:233 ;
::_thesis: verum
end;

theorem Th8: :: NAT_2:8
for i, j being Nat st i >= j holds
j -' i = 0
proof
let i, j be Nat; ::_thesis: ( i >= j implies j -' i = 0 )
assume A1: i >= j ; ::_thesis: j -' i = 0
percases ( i = j or i > j ) by A1, XXREAL_0:1;
suppose i = j ; ::_thesis: j -' i = 0
hence  j -' i = 0 by XREAL_1:232; ::_thesis: verum
end;
suppose i > j ; ::_thesis: j -' i = 0
then  j - i < 0 by XREAL_1:49;
hence  j -' i = 0 by XREAL_0:def_2; ::_thesis: verum
end;
end;
end;

theorem Th9: :: NAT_2:9
for i, j being non empty Nat holds i -' j < i
proof
let i, j be non empty Nat; ::_thesis: i -' j < i
percases ( j <= i or j > i ) ;
supposeA1: j <= i ; ::_thesis: i -' j < i
 i - j < i - 0 by XREAL_1:15;
hence  i -' j < i by A1, XREAL_1:233; ::_thesis: verum
end;
suppose j > i ; ::_thesis: i -' j < i
hence  i -' j < i by Th8; ::_thesis: verum
end;
end;
end;

theorem Th10: :: NAT_2:10
for k, n being Nat st k <= n holds
2 to_power n = (2 to_power k) * (2 to_power (n -' k))
proof
let k, n be Nat; ::_thesis: ( k <= n implies 2 to_power n = (2 to_power k) * (2 to_power (n -' k)) )
assume  k <= n ; ::_thesis: 2 to_power n = (2 to_power k) * (2 to_power (n -' k))
then  n = k + (n -' k) by XREAL_1:235;
hence  2 to_power n = (2 to_power k) * (2 to_power (n -' k)) by POWER:27; ::_thesis: verum
end;

theorem :: NAT_2:11
for k, n being Nat st k <= n holds
2 to_power k divides 2 to_power n
proof
let k, n be Nat; ::_thesis: ( k <= n implies 2 to_power k divides 2 to_power n )
assume  k <= n ; ::_thesis: 2 to_power k divides 2 to_power n
then  2 to_power n = (2 to_power k) * (2 to_power (n -' k)) by Th10;
hence  2 to_power k divides 2 to_power n by NAT_D:def_3; ::_thesis: verum
end;

theorem Th12: :: NAT_2:12
for k, n being Nat st k > 0 & n div k = 0 holds
n < k
proof
let k, n be Nat; ::_thesis: ( k > 0 & n div k = 0 implies n < k )
assume that
A1: k > 0 and
A2: n div k = 0 ; ::_thesis: n < k
 ex t being Nat st
( n = (k * (n div k)) + t & t < k ) by A1, NAT_D:def_1;
hence  n < k by A2; ::_thesis: verum
end;

theorem :: NAT_2:13
for k, n being Nat st k > 0 & k <= n holds
n div k >= 1
proof
let k, n be Nat; ::_thesis: ( k > 0 & k <= n implies n div k >= 1 )
assume  ( k > 0 & k <= n ) ; ::_thesis: n div k >= 1
then  n div k <> 0 by Th12;
then  n div k >= 0 + 1 by NAT_1:13;
hence  n div k >= 1 ; ::_thesis: verum
end;

theorem :: NAT_2:14
for k, n being Nat st k <> 0 holds
(n + k) div k = (n div k) + 1
proof
let k, n be Nat; ::_thesis: ( k <> 0 implies (n + k) div k = (n div k) + 1 )
assume  k <> 0 ; ::_thesis: (n + k) div k = (n div k) + 1
then consider t being Nat such that
A1: n = (k * (n div k)) + t and
A2: t < k by NAT_D:def_1;
 n + k = (k * ((n div k) + 1)) + t by A1;
hence  (n + k) div k = (n div k) + 1 by A2, NAT_D:def_1; ::_thesis: verum
end;

theorem :: NAT_2:15
for k, n, i being Nat st k divides n & 1 <= n & 1 <= i & i <= k holds
(n -' i) div k = (n div k) - 1
proof
let k, n, i be Nat; ::_thesis: ( k divides n & 1 <= n & 1 <= i & i <= k implies (n -' i) div k = (n div k) - 1 )
assume that
A1: k divides n and
A2: 1 <= n and
A3: 1 <= i and
A4: i <= k ; ::_thesis: (n -' i) div k = (n div k) - 1
A5: k -' i < k by A3, A4, Th9;
A6: k <= n by A1, A2, NAT_D:7;
then  i + k <= k + n by A4, XREAL_1:7;
then A7: i <= n by XREAL_1:6;
 n div k > 0
proof
assume  not n div k > 0 ; ::_thesis: contradiction
then  n div k = 0 ;
hence  contradiction by A3, A4, A6, Th12; ::_thesis: verum
end;
then  n div k >= 0 + 1 by NAT_1:13;
then A8: (n div k) -' 1 = (n div k) - 1 by XREAL_1:233;
 n = k * (n div k) by A1, NAT_D:3;
then n -' i = (((k * (n div k)) - (k * 1)) + k) - i by A7, XREAL_1:233
.= (k * ((n div k) -' 1)) + (k - i) by A8
.= (k * ((n div k) -' 1)) + (k -' i) by A4, XREAL_1:233 ;
hence  (n -' i) div k = (n div k) - 1 by A8, A5, NAT_D:def_1; ::_thesis: verum
end;

theorem :: NAT_2:16
for k, n being Nat st k <= n holds
(2 to_power n) div (2 to_power k) = 2 to_power (n -' k)
proof
let k, n be Nat; ::_thesis: ( k <= n implies (2 to_power n) div (2 to_power k) = 2 to_power (n -' k) )
assume  k <= n ; ::_thesis: (2 to_power n) div (2 to_power k) = 2 to_power (n -' k)
then  ( 2 to_power k > 0 & 2 to_power n = (2 to_power k) * (2 to_power (n -' k)) ) by Th10, POWER:34;
hence  (2 to_power n) div (2 to_power k) = 2 to_power (n -' k) by NAT_D:18; ::_thesis: verum
end;

theorem :: NAT_2:17
for n being Nat st n > 0 holds
(2 to_power n) mod 2 = 0
proof
let n be Nat; ::_thesis: ( n > 0 implies (2 to_power n) mod 2 = 0 )
assume  n > 0 ; ::_thesis: (2 to_power n) mod 2 = 0
then A1: n >= 0 + 1 by NAT_1:13;
2 to_power n = 2 to_power ((n - 1) + 1)
.= 2 to_power ((n -' 1) + 1) by A1, XREAL_1:233
.= (2 to_power (n -' 1)) * (2 to_power 1) by POWER:27
.= (2 to_power (n -' 1)) * 2 by POWER:25 ;
hence  (2 to_power n) mod 2 = 0 by NAT_D:13; ::_thesis: verum
end;

theorem :: NAT_2:18
for n being Nat st n > 0 holds
( n mod 2 = 0 iff (n -' 1) mod 2 = 1 )
proof
let n be Nat; ::_thesis: ( n > 0 implies ( n mod 2 = 0 iff (n -' 1) mod 2 = 1 ) )
assume A1: n > 0 ; ::_thesis: ( n mod 2 = 0 iff (n -' 1) mod 2 = 1 )
thus  ( n mod 2 = 0 implies (n -' 1) mod 2 = 1 ) ::_thesis: ( (n -' 1) mod 2 = 1 implies n mod 2 = 0 )
proof
consider t being Nat such that
A2: n = (2 * t) + (n mod 2) and
 n mod 2 < 2 by NAT_D:def_2;
assume A3: n mod 2 = 0 ; ::_thesis: (n -' 1) mod 2 = 1
then  t > 0 by A1, A2;
then A4: t >= 0 + 1 by NAT_1:13;
 n >= 0 + 1 by A1, NAT_1:13;
then n -' 1 = (2 * ((t - 1) + 1)) - 1 by A3, A2, XREAL_1:233
.= (2 * (t - 1)) + ((1 + 1) - 1)
.= (2 * (t -' 1)) + 1 by A4, XREAL_1:233 ;
hence  (n -' 1) mod 2 = 1 by NAT_D:def_2; ::_thesis: verum
end;
assume  (n -' 1) mod 2 = 1 ; ::_thesis: n mod 2 = 0
then consider t being Nat such that
A5: n -' 1 = (2 * t) + 1 and
 1 < 2 by NAT_D:def_2;
 n >= 0 + 1 by A1, NAT_1:13;
then n = ((2 * t) + 1) + 1 by A5, XREAL_1:235
.= (2 * (t + 1)) + 0 ;
hence  n mod 2 = 0 by NAT_D:def_2; ::_thesis: verum
end;

theorem :: NAT_2:19
for n being non empty Nat st n <> 1 holds
n > 1
proof
let n be non empty Nat; ::_thesis: ( n <> 1 implies n > 1 )
A1: n >= 1 by NAT_1:14;
assume  n <> 1 ; ::_thesis: n > 1
hence  n > 1 by A1, XXREAL_0:1; ::_thesis: verum
end;

theorem :: NAT_2:20
for n, k being Nat st n <= k & k < n + n holds
k div n = 1
proof
let n, k be Nat; ::_thesis: ( n <= k & k < n + n implies k div n = 1 )
assume that
A1: n <= k and
A2: k < n + n ; ::_thesis: k div n = 1
A3: k = n + (k - n)
.= (n * 1) + (k -' n) by A1, XREAL_1:233 ;
 k - n < (n + n) - n by A2, XREAL_1:9;
hence  k div n = 1 by A3, NAT_D:def_1; ::_thesis: verum
end;

theorem Th21: :: NAT_2:21
for n being Nat holds
( n is even iff n mod 2 = 0 )
proof
let n be Nat; ::_thesis: ( n is even iff n mod 2 = 0 )
A1: n in NAT by ORDINAL1:def_12;
thus  ( n is even implies n mod 2 = 0 ) ::_thesis: ( n mod 2 = 0 implies n is even )
proof
assume  n is even ; ::_thesis: n mod 2 = 0
then consider k being Element of NAT  such that
A2: n = 2 * k by A1, ABIAN:def_2;
 n = (2 * k) + 0 by A2;
hence  n mod 2 = 0 by NAT_D:def_2; ::_thesis: verum
end;
assume  n mod 2 = 0 ; ::_thesis: n is even
then  ex k being Nat st
( n = (2 * k) + 0 & 0 < 2 ) by NAT_D:def_2;
hence  n is even ; ::_thesis: verum
end;

theorem :: NAT_2:22
for n being Nat holds
( n is odd iff n mod 2 = 1 )
proof
let n be Nat; ::_thesis: ( n is odd iff n mod 2 = 1 )
 ( n is odd iff not n mod 2 = 0 ) by Th21;
hence  ( n is odd iff n mod 2 = 1 ) by NAT_D:12; ::_thesis: verum
end;

theorem :: NAT_2:23
for t, k, n being Nat st 1 <= t & k <= n & 2 * t divides k holds
( n div t is even iff (n -' k) div t is even )
proof
let t, k, n be Nat; ::_thesis: ( 1 <= t & k <= n & 2 * t divides k implies ( n div t is even iff (n -' k) div t is even ) )
assume that
A1: 1 <= t and
A2: k <= n and
A3: 2 * t divides k ; ::_thesis: ( n div t is even iff (n -' k) div t is even )
consider r being Nat such that
A4: k = (2 * t) * r by A3, NAT_D:def_3;
thus  ( n div t is even implies (n -' k) div t is even ) ::_thesis: ( (n -' k) div t is even implies n div t is even )
proof
assume  n div t is even ; ::_thesis: (n -' k) div t is even
then consider p being Element of NAT  such that
A5: n div t = 2 * p by ABIAN:def_2;
consider q being Nat such that
A6: n = (t * (2 * p)) + q and
A7: q < t by A1, A5, NAT_D:def_1;
 1 * t < 2 * t by A1, XREAL_1:68;
then  t + q < (2 * t) + t by A7, XREAL_1:8;
then  q < 2 * t by XREAL_1:6;
then  q / (2 * t) < 1 by XREAL_1:189;
then A8: p + (q / (2 * t)) < p + 1 by XREAL_1:6;
consider r being Nat such that
A9: k = (2 * t) * r by A3, NAT_D:def_3;
A10: 2 * t <> 0 by A1;
then  (2 * t) * r <= ((2 * t) * p) + ((q / (2 * t)) * (2 * t)) by A2, A6, A9, XCMPLX_1:87;
then  (2 * t) * r <= (2 * t) * (p + (q / (2 * t))) ;
then  r <= p + (q / (2 * t)) by A10, XREAL_1:68;
then  (p + (q / (2 * t))) + r < (p + 1) + (p + (q / (2 * t))) by A8, XREAL_1:8;
then  r < p + 1 by XREAL_1:6;
then A11: r <= p by NAT_1:13;
n -' k = ((t * (2 * p)) + q) - ((2 * t) * r) by A2, A6, A9, XREAL_1:233
.= (t * (2 * (p - r))) + q
.= (t * (2 * (p -' r))) + q by A11, XREAL_1:233 ;
hence  (n -' k) div t is even by A7, NAT_D:def_1; ::_thesis: verum
end;
assume  (n -' k) div t is even ; ::_thesis: n div t is even
then consider p being Element of NAT  such that
A12: (n -' k) div t = 2 * p by ABIAN:def_2;
consider q being Nat such that
A13: n -' k = (t * (2 * p)) + q and
A14: q < t by A1, A12, NAT_D:def_1;
 n - k = (t * (2 * p)) + q by A2, A13, XREAL_1:233;
then  n = (t * (2 * (p + r))) + q by A4;
hence  n div t is even by A14, NAT_D:def_1; ::_thesis: verum
end;

theorem Th24: :: NAT_2:24
for n, m, k being Nat st n <= m holds
n div k <= m div k
proof
let n, m, k be Nat; ::_thesis: ( n <= m implies n div k <= m div k )
assume that
A1: n <= m and
A2: n div k > m div k ; ::_thesis: contradiction
set r = (n div k) -' (m div k);
A3: (n div k) -' (m div k) = (n div k) - (m div k) by A2, XREAL_1:233;
then  (n div k) -' (m div k) > (m div k) - (m div k) by A2, XREAL_1:9;
then  (n div k) -' (m div k) >= 0 + 1 by NAT_1:13;
then  k * ((n div k) -' (m div k)) >= k * 1 by XREAL_1:64;
then A4: (k * ((n div k) -' (m div k))) + (k * (m div k)) >= k + (k * (m div k)) by XREAL_1:6;
percases ( k <> 0 or k = 0 ) ;
supposeA5: k <> 0 ; ::_thesis: contradiction
then  ex t2 being Nat st
( m = (k * (m div k)) + t2 & t2 < k ) by NAT_D:def_1;
then  m < k + (k * (m div k)) by XREAL_1:6;
then  m - (k * (n div k)) < (k + (k * (m div k))) - (k + (k * (m div k))) by A3, A4, XREAL_1:14;
then A6: m - (k * (n div k)) < 0 ;
 ex t1 being Nat st
( n = (k * (n div k)) + t1 & t1 < k ) by A5, NAT_D:def_1;
then  k * (n div k) <= n by NAT_1:11;
then  m - n < (k * (n div k)) - (k * (n div k)) by A6, XREAL_1:13;
then  m < 0 + n by XREAL_1:19;
hence  contradiction by A1; ::_thesis: verum
end;
suppose k = 0 ; ::_thesis: contradiction
hence  contradiction by A2, NAT_D:def_1; ::_thesis: verum
end;
end;
end;

theorem :: NAT_2:25
for k, n being Nat st k <= 2 * n holds
(k + 1) div 2 <= n
proof
let k, n be Nat; ::_thesis: ( k <= 2 * n implies (k + 1) div 2 <= n )
assume  k <= 2 * n ; ::_thesis: (k + 1) div 2 <= n
then  k + 1 <= (2 * n) + 1 by XREAL_1:6;
then  (k + 1) div 2 <= ((2 * n) + 1) div 2 by Th24;
hence  (k + 1) div 2 <= n by NAT_D:def_1; ::_thesis: verum
end;

theorem :: NAT_2:26
for n being Nat st n is even holds
n div 2 = (n + 1) div 2
proof
let n be Nat; ::_thesis: ( n is even implies n div 2 = (n + 1) div 2 )
assume A1: n is even ; ::_thesis: n div 2 = (n + 1) div 2
n = (2 * (n div 2)) + (n mod 2) by NAT_D:2
.= (2 * (n div 2)) + 0 by A1, Th21 ;
hence  n div 2 = (n + 1) div 2 by NAT_D:def_1; ::_thesis: verum
end;

theorem :: NAT_2:27
for n, k, i being Nat holds (n div k) div i = n div (k * i)
proof
let n, k, i be Nat; ::_thesis: (n div k) div i = n div (k * i)
now__::_thesis:_(n_div_k)_div_i_=_n_div_(k_*_i)
percases ( i = 0 or i <> 0 ) ;
supposeA1: i = 0 ; ::_thesis: (n div k) div i = n div (k * i)
hence (n div k) div i = 0 by NAT_D:def_1
.= n div (k * i) by A1, NAT_D:def_1 ;
::_thesis: verum
end;
supposeA2: i <> 0 ; ::_thesis: (n div k) div i = n div (k * i)
now__::_thesis:_(n_div_k)_div_i_=_n_div_(k_*_i)
percases ( k = 0 or k <> 0 ) ;
supposeA3: k = 0 ; ::_thesis: (n div k) div i = n div (k * i)
then  n div k = 0 by NAT_D:def_1;
hence  (n div k) div i = n div (k * i) by A3, Th2; ::_thesis: verum
end;
supposeA4: k <> 0 ; ::_thesis: (n div k) div i = n div (k * i)
consider t2 being Nat such that
A5: n div k = (i * ((n div k) div i)) + t2 and
A6: t2 < i by A2, NAT_D:def_1;
 t2 + 1 <= i by A6, NAT_1:13;
then A7: k * (t2 + 1) <= k * i by XREAL_1:64;
consider t1 being Nat such that
A8: n = (k * (n div k)) + t1 and
A9: t1 < k by A4, NAT_D:def_1;
 (k * t2) + t1 < (k * t2) + (k * 1) by A9, XREAL_1:6;
then  ((k * t2) + t1) - (k * i) < (k * (t2 + 1)) - (k * (t2 + 1)) by A7, XREAL_1:14;
then A10: (k * t2) + t1 < 0 + (k * i) by XREAL_1:19;
 n = ((k * i) * ((n div k) div i)) + ((k * t2) + t1) by A8, A5;
hence  (n div k) div i = n div (k * i) by A10, NAT_D:def_1; ::_thesis: verum
end;
end;
end;
hence  (n div k) div i = n div (k * i) ; ::_thesis: verum
end;
end;
end;
hence  (n div k) div i = n div (k * i) ; ::_thesis: verum
end;

definition
let n be Nat;
redefine attr n is trivial  means :Def1: :: NAT_2:def 1
( n = 0 or n = 1 );
compatibility
 ( n is trivial iff ( n = 0 or n = 1 ) )
proof
thus  ( not n is trivial or n = 0 or n = 1 ) ::_thesis: ( ( n = 0 or n = 1 ) implies n is trivial )
proof
assume A1: n is trivial ; ::_thesis: ( n = 0 or n = 1 )
assume that
A2: n <> 0 and
A3: n <> 1 ; ::_thesis: contradiction
A4: n > 1 + 0 by A2, A3, NAT_1:25;
reconsider n = n as Nat ;
consider x being set  such that
A5: n = {x} by A1, A2, ZFMISC_1:131;
A6: n =  {  k where k is Element of NAT : k < n  }  by AXIOMS:4;
then A7: 1 in n by A4;
 0 in n by A2, A6;
then  0 = x by A5, TARSKI:def_1;
hence  contradiction by A7, A5, TARSKI:def_1; ::_thesis: verum
end;
assume  ( n = 0 or n = 1 ) ; ::_thesis: n is trivial
hence  n is trivial by CARD_1:49; ::_thesis: verum
end;
end;

:: deftheorem Def1 defines trivial NAT_2:def_1_:_
 for n being Nat holds
( n is trivial iff ( n = 0 or n = 1 ) );

registration
cluster ext-real non negative non trivial ordinal natural V14() real integer for set ;
existence
 not for b1 being Nat holds b1 is trivial
proof
take  2 ; ::_thesis: not 2 is trivial
thus  not 2 is trivial by Def1; ::_thesis: verum
end;
end;

theorem :: NAT_2:28
for k being Nat holds
( not k is trivial iff ( not k is empty & k <> 1 ) ) by Def1;

theorem :: NAT_2:29
for k being non trivial Nat holds k >= 2
proof
let k be non trivial Nat; ::_thesis: k >= 2
 k >= 1 by NAT_1:14;
then  ( k > 1 or k = 1 ) by XXREAL_0:1;
then  k >= 1 + 1 by Def1, NAT_1:13;
hence  k >= 2 ; ::_thesis: verum
end;

scheme :: NAT_2:sch 2
Indfrom2{ P1[ set ] } :
 for k being non trivial Nat holds P1[k]
provided
A1: P1[2] and
A2: for k being non trivial Nat st P1[k] holds
P1[k + 1]
proof
defpred S1[ non empty Nat] means ( not $1 is trivial implies P1[$1] );
A3: now__::_thesis:_for_k_being_non_empty_Nat_st_S1[k]_holds_
S1[k_+_1]
let k be non empty Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A4: S1[k] ; ::_thesis: S1[k + 1]
now__::_thesis:_(_not_k_+_1_is_trivial_implies_S1[k_+_1]_)
assume  not k + 1 is trivial ; ::_thesis: S1[k + 1]
percases ( k = 1 or k <> 1 ) ;
suppose k = 1 ; ::_thesis: S1[k + 1]
hence  S1[k + 1] by A1; ::_thesis: verum
end;
suppose k <> 1 ; ::_thesis: S1[k + 1]
then  not k is trivial by Def1;
hence  S1[k + 1] by A2, A4; ::_thesis: verum
end;
end;
end;
hence  S1[k + 1] ; ::_thesis: verum
end;
A5: S1[1] by Def1;
 for k being non empty Nat holds S1[k] from NAT_1:sch_10(A5, A3);
hence  for k being non trivial Nat holds P1[k] ; ::_thesis: verum
end;

begin

theorem :: NAT_2:30
for i, j, k being Nat holds (i -' j) -' k = i -' (j + k)
proof
let i, j, k be Nat; ::_thesis: (i -' j) -' k = i -' (j + k)
percases ( i <= j or ( j <= i & i - j <= k ) or ( j <= i & k <= i - j ) ) ;
supposeA1: i <= j ; ::_thesis: (i -' j) -' k = i -' (j + k)
hence (i -' j) -' k = 0 -' k by Th8
.= 0 by Th8
.= i -' (j + k) by A1, Th8, NAT_1:12 ;
::_thesis: verum
end;
supposeA2: ( j <= i & i - j <= k ) ; ::_thesis: (i -' j) -' k = i -' (j + k)
then A3: i <= j + k by XREAL_1:20;
 i -' j = i - j by A2, XREAL_1:233;
hence (i -' j) -' k = 0 by A2, Th8
.= i -' (j + k) by A3, Th8 ;
::_thesis: verum
end;
supposeA4: ( j <= i & k <= i - j ) ; ::_thesis: (i -' j) -' k = i -' (j + k)
then A5: k + j <= i by XREAL_1:19;
 i -' j = i - j by A4, XREAL_1:233;
hence (i -' j) -' k = (i - j) - k by A4, XREAL_1:233
.= i - (j + k)
.= i -' (j + k) by A5, XREAL_1:233 ;
::_thesis: verum
end;
end;
end;