:: Elementary Number Theory Problems. {P}art {II} :: by Artur Korni{\l}owicz and Dariusz Surowik :: :: Received March 30, 2021 :: Copyright (c) 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, FINSEQ_1, RELAT_1, FUNCT_1, XXREAL_0, XBOOLE_0, SUBSET_1, ARYTM_3, TARSKI, XCMPLX_0, CARD_3, CARD_1, ARYTM_1, INT_2, INT_1, FINSET_1, SQUARE_1, NEWTON, FINSEQ_3, ABIAN, PBOOLE, NAT_LAT, NUMBER02; notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, CARD_1, NUMBERS, XCMPLX_0, XREAL_0, REAL_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, MEMBERED, VALUED_0, FINSET_1, FINSEQ_1, FINSEQ_2, FINSEQ_3, FUNCOP_1, INT_1, INT_2, NAT_1, NAT_D, VALUED_1, PBOOLE, ABIAN, NAT_LAT, RVSUM_1, SQUARE_1, XXREAL_0, NEWTON, WSIERP_1, NEWTON02; constructors PARTFUN1, WELLORD2, REAL_1, SQUARE_1, NAT_1, NAT_D, BINOP_2, FINSOP_1, RVSUM_1, FUNCOP_1, RELSET_1, FINSEQOP, NEWTON, WSIERP_1, RECDEF_1, NEWTON02, ABIAN, NAT_LAT; registrations ORDINAL1, RELSET_1, FINSET_1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, NAT_1, INT_1, MEMBERED, FINSEQ_1, FINSEQ_2, RVSUM_1, VALUED_0, CARD_1, SQUARE_1, PEPIN, NEWTON, NEWTON02, NEWTON03, FOMODEL0, NAT_2, ABIAN, NAT_6, RAT_1, NUMPOLY1, NEWTON01, INT_2, JORDAN1D, NAT_LAT; requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM; begin :: Preliminaries registration let D be non empty set; let f be D-valued FinSequence; let i be Nat; cluster Del(f,i) -> D-valued; end; reserve a,b,i,k,m,n for Nat; reserve s,z for non zero Nat; reserve c for Complex; theorem :: NUMBER02:1 c|^5 = c*c*c*c*c; theorem :: NUMBER02:2 c|^6 = c*c*c*c*c*c; theorem :: NUMBER02:3 c|^7 = c*c*c*c*c*c*c; theorem :: NUMBER02:4 c|^8 = c*c*c*c*c*c*c*c; theorem :: NUMBER02:5 c|^9 = c*c*c*c*c*c*c*c*c; theorem :: NUMBER02:6 c|^10 = c*c*c*c*c*c*c*c*c*c; theorem :: NUMBER02:7 a = n-1 & k < n implies k = 0 or ... or k = a; theorem :: NUMBER02:8 -1 div 3 = -1; theorem :: NUMBER02:9 -1 mod 3 = 2; theorem :: NUMBER02:10 not 30 is prime; begin theorem :: NUMBER02:11 n < 31 & n is prime implies n = 2 or n = 3 or n = 5 or n = 7 or n = 11 or n = 13 or n = 17 or n = 19 or n = 23 or n = 29; theorem :: NUMBER02:12 k < 961 & n*n <= k & n is prime implies n = 2 or n = 3 or n = 5 or n = 7 or n = 11 or n = 13 or n = 17 or n = 19 or n = 23 or n = 29; theorem :: NUMBER02:13 113 is prime; theorem :: NUMBER02:14 337 is prime; theorem :: NUMBER02:15 881 is prime; theorem :: NUMBER02:16 k < a implies (a*b+k) mod a = k; theorem :: NUMBER02:17 a divides a|^s + a|^z; theorem :: NUMBER02:18 a divides a|^s - a|^z; theorem :: NUMBER02:19 a divides a|^s * a|^z; registration let p,q be prime Nat; cluster p*q -> non prime; end; theorem :: NUMBER02:20 11 divides 2|^341-2; theorem :: NUMBER02:21 31 divides 2|^341-2; theorem :: NUMBER02:22 ex k st n = z*k+0 or ... or n = z*k+(z-1); theorem :: NUMBER02:23 ex k st n = 3*k or n = 3*k+1 or n = 3*k+2; theorem :: NUMBER02:24 ex k st n = 4*k or n = 4*k+1 or n = 4*k+2 or n = 4*k+3; theorem :: NUMBER02:25 ex k st n = 5*k or n = 5*k+1 or n = 5*k+2 or n = 5*k+3 or n = 5*k+4; theorem :: NUMBER02:26 ex k st n = 6*k or n = 6*k+1 or n = 6*k+2 or n = 6*k+3 or n = 6*k+4 or n = 6*k+5; theorem :: NUMBER02:27 ex k st n = 7*k or n = 7*k+1 or n = 7*k+2 or n = 7*k+3 or n = 7*k+4 or n = 7*k+5 or n = 7*k+6; theorem :: NUMBER02:28 ex k st n = 8*k or n = 8*k+1 or n = 8*k+2 or n = 8*k+3 or n = 8*k+4 or n = 8*k+5 or n = 8*k+6 or n = 8*k+7; theorem :: NUMBER02:29 ex k st n = 9*k or n = 9*k+1 or n = 9*k+2 or n = 9*k+3 or n = 9*k+4 or n = 9*k+5 or n = 9*k+6 or n = 9*k+7 or n = 9*k+8; theorem :: NUMBER02:30 ex k st n = 10*k or n = 10*k+1 or n = 10*k+2 or n = 10*k+3 or n = 10*k+4 or n = 10*k+5 or n = 10*k+6 or n = 10*k+7 or n = 10*k+8 or n = 10*k+9; theorem :: NUMBER02:31 not 3 divides n iff ex k st n = 3*k+1 or n = 3*k+2; theorem :: NUMBER02:32 not 4 divides n iff ex k st n = 4*k+1 or n = 4*k+2 or n = 4*k+3; theorem :: NUMBER02:33 not 5 divides n iff ex k st n = 5*k+1 or n = 5*k+2 or n = 5*k+3 or n = 5*k+4; theorem :: NUMBER02:34 not 6 divides n iff ex k st n = 6*k+1 or n = 6*k+2 or n = 6*k+3 or n = 6*k+4 or n = 6*k+5; theorem :: NUMBER02:35 not 7 divides n iff ex k st n = 7*k+1 or n = 7*k+2 or n = 7*k+3 or n = 7*k+4 or n = 7*k+5 or n = 7*k+6; theorem :: NUMBER02:36 not 8 divides n iff ex k st n = 8*k+1 or n = 8*k+2 or n = 8*k+3 or n = 8*k+4 or n = 8*k+5 or n = 8*k+6 or n = 8*k+7; theorem :: NUMBER02:37 not 9 divides n iff ex k st n = 9*k+1 or n = 9*k+2 or n = 9*k+3 or n = 9*k+4 or n = 9*k+5 or n = 9*k+6 or n = 9*k+7 or n = 9*k+8; theorem :: NUMBER02:38 not 10 divides n iff ex k st n = 10*k+1 or n = 10*k+2 or n = 10*k+3 or n = 10*k+4 or n = 10*k+5 or n = 10*k+6 or n = 10*k+7 or n = 10*k+8 or n = 10*k+9; theorem :: NUMBER02:39 2|^(2|^z) mod 3 = 1; definition let n be Integer; attr n is composite means :: NUMBER02:def 1 2 <= n & n is non prime; end; registration cluster composite for Integer; cluster composite for Nat; cluster composite -> positive for Integer; cluster prime -> non composite for Integer; cluster composite -> non prime for Integer; end; registration let m,n be composite Nat; cluster m*n -> composite; end; theorem :: NUMBER02:40 n is composite implies 4 <= n; begin :: Main problems theorem :: NUMBER02:41 1 <= i <= len ((a,b) In_Power n) - m implies a|^m divides ((a,b) In_Power n).i; ::Problem 14 theorem :: NUMBER02:42 n^2 divides (n+1)|^n - 1; :: Problem 15 theorem :: NUMBER02:43 (2|^n-1)^2 divides 2|^((2|^n-1)*n) - 1; :: Problem 29 theorem :: NUMBER02:44 not 6 divides 2|^6-2 & 6 divides 3|^6-3 & not ex n being Nat st n < 6 & not n divides 2|^n-2 & n divides 3|^n-3; :: Problem 30 theorem :: NUMBER02:45 for a being non zero Nat ex n being non prime Nat st n divides a|^n-a; theorem :: NUMBER02:46 not 7 divides a implies ex k st a^2 = 7*k+1 or a^2 = 7*k+2 or a^2 = 7*k+4; theorem :: NUMBER02:47 ex k st a^2 = 7*k or a^2 = 7*k+1 or a^2 = 7*k+2 or a^2 = 7*k+4; theorem :: NUMBER02:48 not 7 divides a implies a^2 mod 7 = 1 or a^2 mod 7 = 2 or a^2 mod 7 = 4; theorem :: NUMBER02:49 a^2 mod 7 = 0 or a^2 mod 7 = 1 or a^2 mod 7 = 2 or a^2 mod 7 = 4; theorem :: NUMBER02:50 (ex k st a = 7*k+1 or a = 7*k+2 or a = 7*k+4) & (ex k st b = 7*k+1 or b = 7*k+2 or b = 7*k+4) implies ex k st a+b = 7*k+1 or ... or a+b = 7*k+6; theorem :: NUMBER02:51 (a mod 7 = 1 or a mod 7 = 2 or a mod 7 = 4) & (b mod 7 = 1 or b mod 7 = 2 or b mod 7 = 4) implies a+b mod 7 = 1 or ... or a+b mod 7 = 6; :: Problem 34 theorem :: NUMBER02:52 7 divides a^2+b^2 implies 7 divides a & 7 divides b; :: Problem 78 theorem :: NUMBER02:53 13^2+1 = 7^2 + 11^2 & 17^2+1 = 11^2 + 13^2 & 23^2+1 = 13^2 + 19^2 & 31^2+1 = 11^2 + 29^2; :: Problem 83 theorem :: NUMBER02:54 2 = 1|^4+1|^4 & 17 = 1|^4+2|^4 & 97 = 2|^4+3|^4 & 257 = 1|^4+4|^4 & 641 = 2|^4+5|^4; theorem :: NUMBER02:55 0|^4+(0+1)|^4 is non composite; theorem :: NUMBER02:56 1|^4+(1+1)|^4 is non composite; theorem :: NUMBER02:57 2|^4+(2+1)|^4 is non composite; theorem :: NUMBER02:58 3|^4+(3+1)|^4 is non composite; theorem :: NUMBER02:59 4|^4+(4+1)|^4 is non composite; :: Problem 97 theorem :: NUMBER02:60 5|^4+(5+1)|^4 is composite & not ex n being Nat st n < 5 & n|^4+(n+1)|^4 is composite; theorem :: NUMBER02:61 1 <= a implies 2|^(2|^n) + (6*a-1) > 6; theorem :: NUMBER02:62 3 divides 2|^(2|^z) + (6*a-1); theorem :: NUMBER02:63 1 <= a implies 2|^(2|^z) + (6*a-1) is non prime; theorem :: NUMBER02:64 1 <= a implies 2|^(2|^z) + (6*a-1) is composite; :: Problem 116 theorem :: NUMBER02:65 for z being non zero Nat holds {k where k is Nat: k is odd & 2|^(2|^z)+k is composite} is infinite;