:: Natural Numbers :: by Robert Milewski :: :: Received February 23, 1998 :: Copyright (c) 1998-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, NAT_1, XBOOLE_0, SUBSET_1, FINSEQ_1, PARTFUN1, CARD_1, XXREAL_0, ARYTM_3, FUNCT_1, INT_1, RELAT_1, ARYTM_1, POWER, ABIAN, ZFMISC_1, REAL_1, XCMPLX_0; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, XCMPLX_0, XREAL_0, NUMBERS, INT_1, NAT_1, NAT_D, POWER, ABIAN, FUNCT_1, PARTFUN1, FINSEQ_1, XXREAL_0; constructors XXREAL_0, REAL_1, NAT_1, NAT_D, MEMBERED, SERIES_1, BINARITH, ABIAN; registrations RELSET_1, XXREAL_0, XREAL_0, NAT_1, INT_1, ABIAN, SERIES_1, XBOOLE_0, ZFMISC_1, ORDINAL1; requirements REAL, NUMERALS, SUBSET, ARITHM; begin :: Preliminaries reserve i, j, k, l, m, n, t for Nat; scheme :: NAT_2:sch 1 NonUniqPiFinRecExD{D() -> non empty set, A() -> Element of D(), N() -> Nat, P[set,set,set]}: ex p be FinSequence of D() st len p = N() & (p/.1 = A() or N() = 0) & for n be Nat st 1 <= n & n < N() holds P[n,p/.n,p/.(n+1)] provided for n be Nat st 1 <= n & n < N() for x be Element of D() ex y be Element of D() st P[n,x,y]; theorem :: NAT_2:1 for x,y be Real st x >= 0 & y > 0 holds x / ( [\ x / y /] + 1 ) < y; begin :: Division and Rest of Division theorem :: NAT_2:2 0 div n = 0; theorem :: NAT_2:3 for n be non zero Nat holds n div n = 1; theorem :: NAT_2:4 n div 1 = n; theorem :: NAT_2:5 i <= j & k <= j & i = j -' k + l implies k = j -' i + l; theorem :: NAT_2:6 i in Seg n implies n -' i + 1 in Seg n; theorem :: NAT_2:7 j < i implies i -' (j + 1) + 1 = i -' j; theorem :: NAT_2:8 i >= j implies j -' i = 0; theorem :: NAT_2:9 for i,j be non zero Nat holds i -' j < i; theorem :: NAT_2:10 k <= n implies 2 to_power n = (2 to_power k) * (2 to_power (n-'k )); theorem :: NAT_2:11 k <= n implies 2 to_power k divides 2 to_power n; theorem :: NAT_2:12 k > 0 & n div k = 0 implies n < k; theorem :: NAT_2:13 k > 0 & k <= n implies n div k >= 1; theorem :: NAT_2:14 k <> 0 implies (n+k) div k = (n div k) + 1; theorem :: NAT_2:15 k divides n & 1 <= n & 1 <= i & i <= k implies (n -' i) div k = (n div k) - 1 ; theorem :: NAT_2:16 k <= n implies (2 to_power n) div (2 to_power k) = 2 to_power (n -' k); theorem :: NAT_2:17 n > 0 implies 2 to_power n mod 2 = 0; theorem :: NAT_2:18 n > 0 implies (n mod 2 = 0 iff (n -' 1) mod 2 = 1); theorem :: NAT_2:19 for n be non zero Nat st n <> 1 holds n > 1; theorem :: NAT_2:20 n <= k & k < n + n implies k div n = 1; theorem :: NAT_2:21 n is even iff n mod 2 = 0; theorem :: NAT_2:22 n is odd iff n mod 2 = 1; theorem :: NAT_2:23 1 <= t & k <= n & 2*t divides k implies (n div t is even iff (n-'k) div t is even); theorem :: NAT_2:24 n <= m implies n div k <= m div k; theorem :: NAT_2:25 k <= 2 * n implies (k+1) div 2 <= n; theorem :: NAT_2:26 n is even implies n div 2 = (n + 1) div 2; theorem :: NAT_2:27 (n div k) div i = n div (k*i); definition let n be Nat; redefine attr n is trivial means :: NAT_2:def 1 n = 0 or n = 1; end; registration cluster non trivial for Nat; end; theorem :: NAT_2:28 k is non trivial iff k is non empty & k <> 1; theorem :: NAT_2:29 for k be non trivial Nat holds k >= 2; scheme :: NAT_2:sch 2 Indfrom2 { P[set] } : for k be non trivial Nat holds P[k] provided P[2] and for k be non trivial Nat st P[k] holds P[k + 1]; begin :: Addenda :: from POLYNOM1, 2007.03.18, A.T. theorem :: NAT_2:30 i-'j-'k = i-'(j+k);