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