:: 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;