:: Proth Numbers :: by Christoph Schwarzweller :: :: Received June 4, 2014 :: Copyright (c) 2014-2018 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, ORDINAL1, CARD_1, XXREAL_0, RELAT_1, ARYTM_3, NEWTON, INT_1, SUBSET_1, ARYTM_1, ABIAN, TARSKI, XBOOLE_0, INT_2, NAT_1, EC_PF_2, INT_7, INT_5, INT_3, PEPIN, SQUARE_1, ZFMISC_1, GRAPH_1, GROUP_1, ALGSTR_0, FUNCT_7, FUNCT_1, BINOP_2, XCMPLX_0, NAT_6; notations SUBSET_1, TARSKI, XBOOLE_0, ORDINAL1, STRUCT_0, NUMBERS, CARD_1, XCMPLX_0, XREAL_0, ALGSTR_0, GR_CY_1, INT_5, INT_1, ABIAN, SQUARE_1, GROUP_1, PEPIN, NAT_3, BINOP_1, MEMBERED, INT_2, INT_3, EC_PF_2, INT_7, NAT_D, XXREAL_0, NEWTON; constructors REAL_1, NAT_D, POWER, DOMAIN_1, ABIAN, PEPIN, NAT_3, NUMBERS, NAT_4, NEWTON, EC_PF_2, SUBSET_1, ALGSTR_0, INT_5, INT_7, XXREAL_0, GROUP_1, GR_CY_1, BINOP_2, RELSET_1, XTUPLE_0, BINOP_1, INT_3; registrations ORDINAL1, XCMPLX_0, XXREAL_0, XREAL_0, NAT_1, INT_1, MEMBERED, NEWTON, NAT_2, NAT_3, SQUARE_1, INT_7, ABIAN, STRUCT_0, RELSET_1, WSIERP_1; requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM; definitions NAT_1, NAT_2, NAT_D, INT_1, NEWTON, EC_PF_2, XREAL_0, XCMPLX_0, ALGSTR_0, INT_3, INT_7; equalities NEWTON, NAT_1, NAT_2, INT_1, INT_2, SQUARE_1; expansions NEWTON, NAT_1, NAT_2, INT_1, INT_2, EC_PF_2, TARSKI, MEMBERED, ABIAN, SQUARE_1, XCMPLX_0; theorems ABIAN, INT_1, INT_2, NAT_1, NAT_2, NEWTON, XREAL_1, XCMPLX_0, XCMPLX_1, XXREAL_0, NAT_4, ORDINAL1, PEPIN, SQUARE_1, EC_PF_2, INT_3, XBOOLE_0, NAT_D, INT_5, INT_7, GROUP_1, GR_CY_1, EULER_1, ALGSTR_0, TARSKI; schemes NAT_1; begin :: Preliminaries registration let n be positive natural number; cluster n - 1 -> natural; coherence proof n + 1 > 0 + 1 by XREAL_1:6; then n >= 1 by NAT_1:13; then n - 1 >= 1 - 1 by XREAL_1:9; then n - 1 in NAT by INT_1:3; hence thesis; end; end; registration let n be non trivial natural number; cluster n - 1 -> positive; coherence proof n - 1 >= 2 - 1 by NAT_2:29,XREAL_1:9; hence thesis; end; end; registration let n be natural number; reduce 1|^n to 1; reducibility; end; Lm1: for n being even natural number holds (-1)|^n = 1 proof let n be even natural number; defpred P[Nat] means \$1 is even implies (-1)|^(\$1) = 1; A1: now let k be Nat; assume A2: for n being Nat st n < k holds P[n]; per cases; suppose k is odd; hence P[k]; end; suppose A3: k is even; now per cases; case k = 0; hence P[k] by NEWTON:4; end; case A4: k > 0; 0 is even & 0+1=1; then k-2 in NAT by A3,A4,NAT_1:23,INT_1:5; then reconsider k2 = k-2 as Nat; A5: k2 + 2 = k; then A6: k2 is even by A3; (-1)|^k = (-1)|^(k2+2) .= ((-1)|^k2) * ((-1)|^2) by NEWTON:8 .= 1 * (-1)|^(1+1) by A2,A6,A5,NAT_1:16 .= (-1)|^1 * (-1) by NEWTON:6 .= (-1) * (-1); hence P[k]; end; end; hence P[k]; end; end; for k being Nat holds P[k] from NAT_1:sch 4(A1); hence thesis; end; registration let n be even natural number; reduce (-1)|^n to 1; reducibility by Lm1; end; Lm2: for n being odd natural number holds (-1)|^n = -1 proof let n be odd natural number; defpred P[Nat] means \$1 is odd implies (-1)|^(\$1) = -1; A1: now let k be Nat; assume A2: for n being Nat st n < k holds P[n]; per cases; suppose k is even; hence P[k]; end; suppose A3: k is odd; now per cases by NAT_1:23; case k = 0; hence P[k]; end; case k = 1; hence P[k]; end; case k >= 2; then k-2 in NAT by INT_1:5; then reconsider k2 = k-2 as Nat; A4: k2 + 2 = k; then A5: k2 is odd by A3; (-1)|^k = (-1)|^(k2+2) .= ((-1)|^k2) * ((-1)|^2) by NEWTON:8 .= (-1) * (-1)|^(1+1) by A2,A5,A4,NAT_1:16 .= (-1) * (-1)|^1 * (-1) by NEWTON:6 .= (-1) * (-1) * (-1); hence P[k]; end; end; hence P[k]; end; end; for k being Nat holds P[k] from NAT_1:sch 4(A1); hence thesis; end; registration let n be odd natural number; reduce (-1)|^n to -1; reducibility by Lm2; end; theorem Th1: for a being positive natural number, n,m being natural number st n >= m holds a|^n >= a|^m proof let a be positive natural number; let n,m be natural number; assume n >= m; then a|^m divides a|^n by NEWTON:89; hence thesis by INT_2:27; end; theorem Th2: for a being non trivial natural number, n,m being natural number st n > m holds a|^n > a|^m proof let a be non trivial natural number; let n,m be natural number; assume A1: n > m; then consider k being Nat such that A2: n = m + k by NAT_1:10; k <> 0 by A1,A2; then k + 1 > 0 + 1 by XREAL_1:6; then k >= 1 by NAT_1:13; then a|^k >= a|^1 by Th1; then A3: a|^k >= a; a >= 2 by NAT_2:29; then a|^k >= 1 + 1 by A3,XXREAL_0:2; then a|^k > 1 by NAT_1:13; then 1 * a|^m < a|^k * a|^m by XREAL_1:68; hence thesis by A2,NEWTON:8; end; theorem Th3: for n being non zero natural number ex k being natural number, l being odd natural number st n = l * 2|^k proof let n be non zero natural number; per cases; suppose n is odd; then reconsider l = n as odd natural number; take k = 0, l; thus l * 2|^k = l * 1 by NEWTON:4 .= n; end; suppose A1: n is even; defpred P[Nat] means 2|^(\$1) divides n; A2: now let m be Nat; A3: 2|^m > m by NEWTON:86; assume P[m]; then 2|^m <= n by INT_2:27; hence m <= n by A3,XXREAL_0:2; end; 2|^1 = 2; then A3: ex m being Nat st P[m] by A1; consider k being Nat such that A4: P[k] & for n being Nat st P[n] holds n <= k from NAT_1:sch 6(A2,A3); consider l being Integer such that A5: n = 2|^k * l by A4,INT_1:def 3; l >= 0 by A5; then A6: l in NAT by INT_1:3; now assume l is even; then consider u being Integer such that A7: l = 2 * u by INT_1:def 3; n = 2|^k * 2 * u by A5,A7 .= 2|^(k+1) * u by NEWTON:6; then 2|^(k+1) divides n; hence contradiction by A4,NAT_1:16; end; then reconsider l as odd natural number by A6; take k,l; thus thesis by A5; end; end; theorem Th4: for n being even natural number holds n div 2 = n/2 proof let n be even natural number; consider k being Nat such that A1: n = 2*k by ABIAN:def 2; thus thesis by A1,INT_1:25; end; theorem for n being odd natural number holds n div 2 = (n-1)/2 proof let n be odd natural number; consider k being Integer such that A1: n = 2*k+1 by ABIAN:1; A2: (n-1)/2 = k by A1; (n-1)+1 = n; then n-1 <= n by INT_1:6; then A3: k <= n/2 by A2,XREAL_1:72; (n/2) - (1/2) > (n/2) - 1 by XREAL_1:10; hence thesis by A1,A3,INT_1:def 6; end; registration let n be even integer number; cluster n/2 -> integer; coherence proof consider k being Integer such that A1: n = 2 * k by ABIAN:def 1,INT_1:def 3; thus thesis by A1; end; end; registration let n be even natural number; cluster n/2 -> natural; coherence proof consider k being Integer such that A1: n = 2 * k by ABIAN:def 1,INT_1:def 3; k >= 0 by A1; then k in NAT by INT_1:3; then reconsider k as natural number; n / 2 = k by A1; hence thesis; end; end; begin :: Congruences and Prime Numbers registration cluster prime -> non trivial for natural number; coherence; end; Lm3: for a being natural number, b being integer number st a divides b holds a gcd b = a proof let a be natural number, b be integer number; assume A1: a divides b; for m being Integer st m divides a & m divides b holds m divides a; hence thesis by A1,INT_2:def 2; end; theorem Th6: for p being prime natural number, a being integer number holds a gcd p <> 1 iff p divides a proof let p be prime natural number, a be integer number; hereby assume a gcd p <> 1; then a gcd p = p by INT_2:21,INT_2:def 4; hence p divides a by INT_2:21; end; assume A1: p divides a; p divides (a gcd p) by A1,INT_2:22; hence a gcd p <> 1 by INT_2:27,INT_2:def 4; end; theorem Th7: for i,j being integer number, p being prime natural number st p divides i * j holds p divides i or p divides j proof let i,j be integer number, p be prime natural number; assume A1: p divides i * j; assume not(p divides i); then i gcd p = 1 by Th6; hence thesis by A1,INT_2:25,INT_2:def 3; end; theorem Th8: for x,p being prime natural number, k being non zero natural number holds x divides (p|^k) iff x = p proof let x,p be prime natural number; let k be non zero natural number; A1: now assume A2: x divides (p|^k); defpred P[Nat] means x divides p|^(\$1) implies x = p; A3: P[1] proof assume x divides p|^1; then x divides p; then x = 1 or x = p by INT_2:def 4; hence x = p by NAT_2:def 1; end; A4: now let k be non zero Nat; assume A5: P[k]; now assume A6: x divides p|^(k+1); A7: p|^(k+1) = p * p|^k by NEWTON:6; per cases by INT_2:30; suppose x,p are_coprime; hence x = p by A5,A6,A7,INT_2:25; end; suppose x = p; hence x = p; end; end; hence P[k + 1]; end; A8: for k being non zero Nat holds P[k] from NAT_1:sch 10(A3,A4); thus x = p by A8,A2; end; now assume A9: x = p; reconsider k1 = k-1 as natural number; p * p|^k1 = p|^(k1+1) by NEWTON:6; hence x divides (p|^k) by A9; end; hence thesis by A1; end; theorem Th9: for x,y,n being integer number holds x,y are_congruent_mod n iff ex k being Integer st x = k * n + y proof let x,y,n be integer number; now assume x,y are_congruent_mod n; then consider k being integer Number such that A1: n * k = x - y; x = n * k + y by A1; hence ex k being Integer st x = k * n + y; end; hence thesis; end; theorem Th10: for i being integer number, j being non zero integer number holds i, i mod j are_congruent_mod j proof let i be integer number; let j be non zero integer number; i = (i div j) * j + (i mod j) by INT_1:59; hence i, i mod j are_congruent_mod j; end; theorem for x,y being integer number, n being positive integer number holds x,y are_congruent_mod n iff x mod n = y mod n proof let x,y be integer number, n being positive integer number; A1: now assume x,y are_congruent_mod n; then consider k being Integer such that A2: x = k * n + y by Th9; thus x mod n = y mod n by A2,EULER_1:12; end; now assume A3: x mod n = y mod n; A4: x,x mod n are_congruent_mod n by Th10; y mod n, y are_congruent_mod n by Th10,INT_1:14; hence x,y are_congruent_mod n by A3,A4,INT_1:15; end; hence thesis by A1; end; theorem Th12: for i,j being integer number, n being natural number st n < j & i,n are_congruent_mod j holds i mod j = n proof let i,j be integer number, n be natural number; assume A1: n < j & i,n are_congruent_mod j; then consider x being Integer such that A2: j * x = i - n; A3: i = (i div j) * j + (i mod j) by A1,INT_1:59; A4: j in NAT by A1,INT_1:3; per cases; suppose n = 0; hence i mod j = n by A4,A1,INT_1:62; end; suppose A5: n <> 0; A6: i/j = (j*x+n) * j" by A2,XCMPLX_0:def 9 .= x * (j * j") + n * j" .= x * 1 + n * j" by A1,XCMPLX_0:def 7; then A7: x <= i/j by A5,A1,XREAL_1:29; A8: i/j - 1 = x + (n*j" - 1) by A6; A9: n/j < j/j by A1,XREAL_1:74; j/j = j*j" by XCMPLX_0:def 9 .= 1 by A1,XCMPLX_0:def 7; then n*j" < 1 by A9,XCMPLX_0:def 9; then n*j" - 1 < 1 - 1 by XREAL_1:9; then i/j - 1 < x by A8,XREAL_1:30; then i div j = x by A7,INT_1:def 6; hence i mod j = n by A2,A3; end; end; theorem Th13: for n being non zero natural number, x being integer number holds x,0 are_congruent_mod n or ... or x,(n-1) are_congruent_mod n proof let n be non zero natural number, x be integer number; x mod n in NAT by INT_1:3,INT_1:57; then reconsider j = x mod n as Nat; (x mod n) + 1 <= n by INT_1:7,INT_1:58; then A1: (x mod n) + 1 - 1 <= n - 1 by XREAL_1:9; take j; thus thesis by Th10,A1; end; theorem Th14: for n being non zero natural number, x being integer number, k,l being natural number st k < n & l < n & x,k are_congruent_mod n & x,l are_congruent_mod n holds k = l proof let n be non zero natural number, x be integer number, k,l be natural number; assume A1: k < n & l < n & x,k are_congruent_mod n & x,l are_congruent_mod n; hence k = x mod n by Th12 .= l by A1,Th12; end; theorem Th15: for x being integer number holds x|^2, 0 are_congruent_mod 3 or x|^2, 1 are_congruent_mod 3 proof let x be integer number; x,0 are_congruent_mod 3 or ... or x,(3-1) are_congruent_mod 3 by Th13; then A1: x,0 are_congruent_mod 3 or ... or x,2 are_congruent_mod 3; per cases by A1; suppose x,0 are_congruent_mod 3; then x*x, 0*0 are_congruent_mod 3 by INT_1:18; hence thesis by NEWTON:81; end; suppose x,1 are_congruent_mod 3; then x*x, 1*1 are_congruent_mod 3 by INT_1:18; hence thesis by NEWTON:81; end; suppose x,2 are_congruent_mod 3; then x*x, 2*2 are_congruent_mod 3 by INT_1:18; then 4, x*x are_congruent_mod 3 by INT_1:14; then (4-3),x*x are_congruent_mod 3 by INT_1:22; then x*x, (4-3) are_congruent_mod 3 by INT_1:14; hence thesis by NEWTON:81; end; end; theorem Th16: for p being prime natural number, x,y being Element of Z/Z*(p), i,j being integer number st x = i & y = j holds x * y = (i * j) mod p proof let p be prime natural number, x,y be Element of Z/Z*(p), i,j be integer number; assume A1: x = i & y = j; A2: INT.Ring(p) = doubleLoopStr(#Segm(p),addint(p), multint(p),In (1,Segm(p)),In (0,Segm(p))#) by INT_3:def 12; A3: Z/Z*(p) = multMagma(#Segm0(p),multint0(p)#) by INT_7:def 4; then x in Segm0(p); then x in Segm(p)\{0} by INT_2:def 4,INT_7:def 2; then reconsider xx = x as Element of Segm(p) by XBOOLE_0:def 5; y in Segm0(p) by A3; then y in Segm(p)\{0} by INT_2:def 4,INT_7:def 2; then reconsider yy = y as Element of Segm(p) by XBOOLE_0:def 5; reconsider x1 = xx, y1= yy as Element of INT.Ring(p) by A2; A4: x * y = x1 * y1 by INT_7:20; x1 * y1 = (multint(p)).(xx,yy) by A2,ALGSTR_0:def 18; hence thesis by A4,A1,INT_3:def 10; end; theorem Th17: for p being prime natural number, x being Element of Z/Z*(p), i being integer number, n being natural number st x = i holds x |^ n = (i |^ n) mod p proof let p be prime natural number, x be Element of Z/Z*(p), i be integer number, n be natural number; assume A1: x = i; A2: Z/Z*(p) = multMagma(#Segm0(p),multint0(p)#) by INT_7:def 4; Segm0(p) = Segm(p) \ {0} by INT_2:def 4,INT_7:def 2; then A3: i in Segm(p) by A2,A1,XBOOLE_0:def 5; reconsider i as Element of NAT by A1,A2,INT_1:3; defpred P[Nat] means x |^ (\$1) = (i |^ (\$1)) mod p; A4: x|^0 = 1_(Z/Z*(p)) by GROUP_1:25; 1 < p by INT_2:def 4; then A5: 1 div p <= 1-1 by INT_1:56,INT_1:52; A6: 1 div p = 0 by A5; i|^0 = 1 by NEWTON:4; then (i |^ 0) mod p = 1 - (1 div p) * p by INT_1:def 10; then A7: P[0] by A4,A6,INT_7:21; A8: now let k be Nat; assume A9: P[k]; x |^ (k+1) = x|^k * x by GROUP_1:34 .= ((i |^ k mod p) * i) mod p by A1,A9,Th16 .= ((i |^ k mod p) * (i mod p)) mod p by A3,NAT_D:24,NAT_1:44 .= (i |^ k * i) mod p by NAT_D:67 .= (i |^ (k+1)) mod p by NEWTON:6; hence P[k+1]; end; A10: for k being Nat holds P[k] from NAT_1:sch 2(A7,A8); thus thesis by A10; end; theorem Th18: for p being prime natural number, x being integer number holds x|^2, 1 are_congruent_mod p iff (x, 1 are_congruent_mod p or x, -1 are_congruent_mod p) proof let p be prime natural number, x be integer number; A1: now assume x|^2, 1 are_congruent_mod p; then p divides (x^2 - 1^2) by NEWTON:81; then A2: p divides (x+1) * (x-1); now per cases by A2,Th7; case p divides x+1; then consider l being Integer such that A3: p * l = x + 1; thus x,-1 are_congruent_mod p by A3; end; case p divides x-1; then consider l being Integer such that A4: p * l = x - 1; thus x,1 are_congruent_mod p by A4; end; end; hence x,1 are_congruent_mod p or x,-1 are_congruent_mod p; end; now assume A5: x,1 are_congruent_mod p or x,-1 are_congruent_mod p; now per cases by A5; case x,1 are_congruent_mod p; then x*x,1*1 are_congruent_mod p by INT_1:18; hence x|^2, 1 are_congruent_mod p by NEWTON:81; end; case x,-1 are_congruent_mod p; then x*x,(-1)*(-1) are_congruent_mod p by INT_1:18; hence x|^2, 1 are_congruent_mod p by NEWTON:81; end; end; hence x|^2, 1 are_congruent_mod p; end; hence thesis by A1; end; theorem Th19: for n being natural number holds -1,1 are_congruent_mod n iff (n = 2 or n = 1) proof let n be natural number; hereby assume -1,1 are_congruent_mod n; then consider k being Integer such that A1: n * k = -2; k < 0 & n <> 0 by A1; then A2: k <= -1 by INT_1:8; now assume A3: n <> 2; now assume n <> 1; then not(n=0 or ... or n = 2) by A1,A3; then not(n <= 2); then n >= 2+1 by NAT_1:13; then n >= 3 & k < 0 by A1; then A4: n * k <= 3 * k by XREAL_1:65; 3 * k <= 3 * (-1) by A2,XREAL_1:64; hence contradiction by A1,A4,XXREAL_0:2; end; hence n = 1; end; hence n = 2 or n = 1; end; assume A5: n = 2 or n = 1; per cases by A5; suppose n = 2; then n * (-1) = -2; hence -1,1 are_congruent_mod n; end; suppose n = 1; hence -1,1 are_congruent_mod n by INT_1:13; end; end; theorem Th20: for i being integer Number holds -1,1 are_congruent_mod i iff (i = 2 or i = 1 or i = -2 or i = -1) proof let n be integer Number; hereby assume A1: -1,1 are_congruent_mod n; then consider k being Integer such that A2: n * k = -2; now per cases; case n >= 0; then n in NAT by INT_1:3; then reconsider m = n as natural number; m = 1 or m = 2 by A1,Th19; hence n = 2 or n = 1 or n = -2 or n = -1; end; case A3: n < 0; then A4: k > 0 by A2; then A5: k >= 0 + 1 by INT_1:7; now assume A6: n <> -2; now assume A7: n <> -1; n <= -1 by A3,INT_1:8; then n < -1 by A7,XXREAL_0:1; then n + 1 <= -1 by INT_1:7; then n + 1 - 1 <= -1 - 1 by XREAL_1:9; then n < -2 by A6,XXREAL_0:1; then n + 1 <= -2 by INT_1:7; then n + 1 - 1 <= -2 - 1 by XREAL_1:9; then A8: n * k <= (-3) * k by A4,XREAL_1:64; (-3) * k <= (-3) * 1 by A5,XREAL_1:65; hence contradiction by A2,A8,XXREAL_0:2; end; hence n = -1; end; hence n = 2 or n = 1 or n = -2 or n = -1; end; end; hence n = 2 or n = 1 or n = -2 or n = -1; end; assume A9: n = 2 or n = 1 or n = -2 or n = -1; per cases by A9; suppose n = 2; then n * (-1) = -2; hence -1,1 are_congruent_mod n; end; suppose n = 1; hence -1,1 are_congruent_mod n by INT_1:13; end; suppose n = -2; hence -1,1 are_congruent_mod n; end; suppose n = -1; then n * (-1) = 1; hence -1,1 are_congruent_mod n by INT_1:20,INT_1:13; end; end; begin :: n_greater definition let n,x be natural number; attr x is n_greater means :Def1: x > n; end; notation let n,x be natural number; antonym x is n_smaller for x is n_or_greater; antonym x is n_or_smaller for x is n_greater; end; registration let n be natural number; cluster n_greater odd for natural number; existence proof per cases; suppose n is even; then consider k being Nat such that A1: n = 2 * k; take n + 1; n+1 > n+0 by XREAL_1:6; hence n+1 is n_greater; thus n+1 is odd by A1; end; suppose n is odd; then consider k being Integer such that A2: n = 2 * k + 1 by ABIAN:1; take n + 2; n+1 > n+0 by XREAL_1:6; hence n+2 is n_greater by XREAL_1:6; thus n+2 is odd by A2; end; end; cluster n_greater even for natural number; existence proof per cases; suppose n is odd; then consider k being Integer such that A3: n = 2 * k + 1 by ABIAN:1; take n + 1; n+1 > n+0 by XREAL_1:6; hence n+1 is n_greater; thus n+1 is even by A3; end; suppose n is even; then consider k being Nat such that A4: n = 2 * k; take n + 2; n+1 > n+0 by XREAL_1:6; hence n+2 is n_greater by XREAL_1:6; thus n+2 is even by A4; end; end; end; registration let n be natural number; cluster n_greater -> n_or_greater for natural number; coherence; end; registration let n be natural number; cluster (n+1)_or_greater -> n_or_greater for natural number; coherence proof let x be natural number; assume A1: x is (n+1)_or_greater; n+1 >= n+0 by XREAL_1:6; hence x is n_or_greater by A1,XXREAL_0:2; end; cluster (n+1)_greater -> n_greater for natural number; coherence proof let x be natural number; assume A2: x is (n+1)_greater; n+1 > n+0 by XREAL_1:6; hence x is n_greater by A2,XXREAL_0:2; end; cluster n_greater -> (n+1)_or_greater for natural number; coherence by NAT_1:13; end; registration let m be non trivial natural number; cluster m_or_greater-> non trivial for natural number; coherence proof let n be natural number; assume A1: n is m_or_greater; m >= 2 by NAT_2:29; hence thesis by A1,XXREAL_0:2; end; end; registration let a be positive natural number; let m be natural number; let n be m_or_greater natural number; cluster a|^n -> (a|^m)_or_greater; coherence by Th1,EC_PF_2:def 1; end; registration let a be non trivial natural number; let m be natural number; let n be m_greater natural number; cluster a|^n -> (a|^m)_greater; coherence by Def1,Th2; end; registration cluster 2_or_greater -> non trivial for natural number; coherence; cluster non trivial -> 2_or_greater for natural number; coherence proof let n be natural number; assume A1: n is non trivial; n <= 1 implies n = 0 or ... or n = 1; then n >= 1 + 1 by A1,NAT_1:13; hence thesis; end; cluster non trivial odd -> 2_greater for natural number; coherence proof let n be natural number; assume A2: n is non trivial odd; n <= 2 implies n = 0 or ... or n = 2; hence thesis by A2; end; end; registration let n be 2_greater natural number; cluster n - 1 -> non trivial; coherence proof n - 1 > 2 - 1 by Def1,XREAL_1:9; hence thesis by NAT_2:def 1; end; end; registration let n be 2_or_greater natural number; cluster n - 2 -> natural; coherence proof n - 2 >= 2 - 2 by EC_PF_2:def 1,XREAL_1:9; then n-2 in NAT by INT_1:3; hence thesis; end; end; registration let m be non zero natural number; let n be m_or_greater natural number; cluster n - 1 -> natural; coherence proof n >= m by EC_PF_2:def 1; then reconsider nn = n - 1 as Element of NAT by INT_1:3; n - 1 >= m-1 by EC_PF_2:def 1,XREAL_1:9; then n-1 in NAT by INT_1:3; hence thesis; end; end; registration cluster 2_greater -> odd for prime natural number; coherence by INT_2:def 4; end; registration let n be natural number; cluster n_greater prime for natural number; existence proof now assume A1: not(ex p being natural number st p is n_greater prime); A2: now let p be prime natural number; not(p is n_greater) by A1; hence p < n+1 by NAT_1:13; end; A3: now let p be set; assume A4: p in SetPrimes; then reconsider p1 = p as Element of NAT; A5: p1 is prime by A4,NEWTON:def 6; then p1 < n+1 by A2; hence p in SetPrimenumber(n+1) by A5,NEWTON:def 7; end; now let p be set; assume A6: p in SetPrimenumber(n+1); reconsider n1 = n + 1 as Nat; SetPrimenumber(n1) c= SetPrimes by NEWTON:68; hence p in SetPrimes by A6; end; then SetPrimes = SetPrimenumber(n+1) by A3; hence contradiction; end; hence thesis; end; end; begin :: Pocklington's theorem revisited definition let n be natural number; mode Divisor of n -> natural number means :Def2: it divides n; existence; end; registration let n be non trivial natural number; cluster non trivial for Divisor of n; existence proof reconsider m = n as Divisor of n by Def2; take m; thus thesis; end; end; registration let n be non zero natural number; cluster -> non zero for Divisor of n; coherence proof let x be Divisor of n; consider k being Integer such that A1: x * k = n by Def2,INT_1:def 3; thus thesis by A1; end; end; registration let n be positive natural number; cluster -> positive for Divisor of n; coherence; end; registration let n be non zero natural number; cluster -> n_or_smaller for Divisor of n; coherence proof let x be Divisor of n; consider k being Integer such that A1: x * k = n by Def2,INT_1:def 3; k >= 0 by A1; then reconsider k as Element of NAT by INT_1:3; k <> 0 by A1; hence thesis by A1,NAT_1:24; end; end; registration let n be non trivial natural number; cluster prime for Divisor of n; existence proof consider p being Element of NAT such that A1: p is prime & p divides n by NAT_2:29,INT_2:31; reconsider p as natural number; take p; thus thesis by A1,Def2; end; end; registration let n be natural number; let q be Divisor of n; cluster n / q -> natural; coherence proof per cases; suppose n = 0; hence thesis; end; suppose A1: n <> 0; consider k being Integer such that A2: q * k = n by Def2,INT_1:def 3; 0 <= k by A2,A1; then A3: k in NAT by INT_1:3; n/q = (q * k) * q" by A2,XCMPLX_0:def 9 .= k * (q * q") .= k * 1 by A1,XCMPLX_0:def 7; hence thesis by A3; end; end; end; registration let n be natural number; let s be Divisor of n; let q be Divisor of s; cluster n / q -> natural; coherence proof per cases; suppose n = 0; hence thesis; end; suppose A1: n <> 0; consider k being Integer such that A2: s * k = n by Def2,INT_1:def 3; consider l being Integer such that A3: q * l = s by Def2,INT_1:def 3; 0 <= k by A2,A1; then A4: k in NAT by INT_1:3; 0 <= l by A3,A1; then A5: l in NAT by INT_1:3; n/q = ((q * l) * k) * q" by A3,A2,XCMPLX_0:def 9 .= l * k * (q * q") .= l * k * 1 by A1,XCMPLX_0:def 7; hence thesis by A4,A5; end; end; end; ::\$N Pocklington's theorem theorem Th21: for n being 2_greater natural number, s being non trivial Divisor of n - 1 st s > sqrt(n) & ex a being natural number st a|^(n-1),1 are_congruent_mod n & for q being prime Divisor of s holds a|^((n-1)/q) - 1 gcd n = 1 holds n is prime proof let n be 2_greater natural number; let s be non trivial Divisor of n - 1; assume A1: s > sqrt(n) & ex a being natural number st a|^(n-1),1 are_congruent_mod n & for q being prime Divisor of s holds a|^((n-1)/q) - 1 gcd n = 1; reconsider m = n as Element of NAT by ORDINAL1:def 12; reconsider f = s as Element of NAT by ORDINAL1:def 12; m > 1+1 by Def1; then A2: m >= 1 by NAT_1:13; consider c being Integer such that A3: m-1 = f * c by Def2,INT_1:def 3; A4: sqrt n >= 0 by SQUARE_1:def 2; A5: now assume s <= c; then c >= sqrt(n) by A1,XXREAL_0:2; then s * c >= (sqrt(n))^2 by A4,A1,XREAL_1:66; then s * c >= n by SQUARE_1:def 2; then n - 1 - n >= n - n by A3,XREAL_1:9; then -1 >= 0; hence contradiction; end; c > 0 by A3; then reconsider c as Element of NAT by INT_1:3; A6: m-1 = f*c & f > c & c > 0 by A3,A5; now let p be Element of NAT; assume A7: p divides f & p is prime; reconsider q = p as natural number; reconsider q as Divisor of s by A7,Def2; reconsider q as prime Divisor of s by A7; consider b being natural number such that A8: b|^(n-1),1 are_congruent_mod n & for q being prime Divisor of s holds b|^((n-1)/q) - 1 gcd n = 1 by A1; reconsider a = b as Element of NAT by ORDINAL1:def 12; consider k1 being Integer such that A9: q * k1 = s by Def2,INT_1:def 3; consider k2 being Integer such that A10: s * k2 = n-1 by Def2,INT_1:def 3; consider l1 being Integer such that A11: p * l1 = f by A7; A12: k2 = c by A3,A10,XCMPLX_1:5; A13: (m-1)/p = (p * l1 * c) * p" by A3,A11,XCMPLX_0:def 9 .= (l1 * c) * ( p * p") .= (l1 * c) * 1 by A7,XCMPLX_0:def 7; A14: n-1 >= 2-1 by Def1,XREAL_1:9; now assume a = 0; then a |^ (n-1) = 0 by A14,NEWTON:11; then n = 1 or n = -1 by A8,INT_2:13; hence contradiction by Def1; end; then a|^((m-'1) div p) + 1 > 0 + 1 by XREAL_1:6; then A15: a|^((m-'1) div p) >= 1 by NAT_1:13; (n-1)/q = ((q*k1)*k2) * q" by A9,A10,XCMPLX_0:def 9 .= (k1 * k2) * (q * q") .= k1 * k2 * 1 by XCMPLX_0:def 7 .= (m-1)/p by A9,A11,A12,A13,XCMPLX_1:5 .= [/ (m-1)/p \] by A13,INT_1:30 .= [\ (m-1)/p /] by A13,INT_1:34 .= (m-'1) div p by A2,XREAL_1:233; then a|^((m-'1) div p)-'1 = b|^((n-1)/q) - 1 by A15,XREAL_1:233; then A16: (a|^((m-'1) div p)-'1) gcd m = 1 by A8; consider x being Integer such that A17: n * x = a|^(n-1) - 1 by A8; A18: a|^(n-1) / n = (n*x+1) * n" by A17,XCMPLX_0:def 9 .= n"*n*x + 1 *n" .= 1 * x + n" by XCMPLX_0:def 7; A19: x <= a|^(n-1)/n by A18,XREAL_1:29; A20: a|^(n-1)/n - 1 = x + (n" - 1) by A18; 2 < n by Def1; then 2 - 1 < n - 0 by XREAL_1:15; then n" < 1" by XREAL_1:88; then n" - 1 < 0 by XREAL_1:49; then a|^(n-1)/n - 1 < x by A20,XREAL_1:30; then a|^(n-1) div n = x by A19,INT_1:def 6; then A21: a|^(n-1) mod n = a|^(n-1) - n * x by INT_1:def 10 .= 1 by A17; a|^(m-'1) mod m = 1 by A21,A2,XREAL_1:233; hence ex a being Element of NAT st a|^(m-'1) mod m = 1 & (a|^((m-'1) div p)-'1) gcd m = 1 by A16; end; hence thesis by A6,NAT_4:24; end; begin :: Euler's criterion notation let a be integer number, p be natural number; antonym a is_quadratic_non_residue_mod p for a is_quadratic_residue_mod p; end; theorem Th22: for p being positive natural number, a being integer number holds a is_quadratic_residue_mod p iff ex x being integer number st x|^2, a are_congruent_mod p proof let p be positive natural number, a be integer number; thus a is_quadratic_residue_mod p implies ex x being integer number st x|^2, a are_congruent_mod p proof assume a is_quadratic_residue_mod p; then consider x being Integer such that A1: (x^2 - a) mod p = 0 by INT_5:def 2; A2: x^2 - a = ((x^2 - a) div p) * p + 0 by A1,INT_1:59; reconsider xx = x as integer number by TARSKI:1; take xx; xx^2 = xx|^2 by NEWTON:81; hence thesis by A2; end; assume ex x being integer number st x|^2, a are_congruent_mod p; then consider x being integer number such that A3: x|^2, a are_congruent_mod p; x^2 = x|^1 * x .= x|^(1+1) by NEWTON:6; then (x^2 - a) mod p = 0 by A3,INT_1:62; hence a is_quadratic_residue_mod p by INT_5:def 2; end; theorem Th23: 2 is_quadratic_non_residue_mod 3 proof now assume ex x being integer number st x|^2, 2 are_congruent_mod 3; then consider x being integer number such that A1: x|^2,2 are_congruent_mod 3; now per cases by Th15; case x|^2, 0 are_congruent_mod 3; hence contradiction by A1,Th14; end; case x|^2, 1 are_congruent_mod 3; hence contradiction by A1,Th14; end; end; hence contradiction; end; hence thesis by Th22; end; ::\$N Legendre symbol definition let p be natural number; let a be integer number; func LegendreSymbol(a,p) -> integer Number equals :Def3: 1 if a gcd p = 1 & a is_quadratic_residue_mod p & p <> 1, 0 if p divides a, -1 if a gcd p = 1 & a is_quadratic_non_residue_mod p & p <> 1; coherence; consistency by Lm3; end; definition let p be prime natural number; let a be integer number; redefine func LegendreSymbol(a,p) equals :Def4: 1 if a gcd p = 1 & a is_quadratic_residue_mod p, 0 if p divides a, -1 if a gcd p = 1 & a is_quadratic_non_residue_mod p; consistency proof A1: a gcd p = 1 & a is_quadratic_residue_mod p & p divides a implies for z being integer number holds z = 1 iff z = 0 proof assume A2: a gcd p = 1 & a is_quadratic_residue_mod p & p divides a; then a gcd p = p by Lm3; hence thesis by A2,INT_2:def 4; end; a gcd p = 1 & a is_quadratic_non_residue_mod p & p divides a implies for z being integer number holds z = -1 iff z = 0 proof assume A3: a gcd p = 1 & a is_quadratic_non_residue_mod p & p divides a; then a gcd p = p by Lm3; hence thesis by A3,INT_2:def 4; end; hence thesis by A1; end; compatibility proof p <> 1 by INT_2:def 4; hence thesis by Def3; end; end; notation let p be natural number; let a be integer number; synonym Leg(a,p) for LegendreSymbol(a,p); end; theorem Th24: for p be prime natural number, a be integer number holds Leg(a,p) = 1 or Leg(a,p) = 0 or Leg(a,p) = -1 proof let p be prime natural number; let a be integer number; assume A1: Leg(a,p) <> 1 & Leg(a,p) <> 0; a gcd p = 1 proof a gcd p = 1 or a gcd p = p by INT_2:def 4,INT_2:21; hence thesis by A1,Def4,INT_2:21; end; hence Leg(a,p) = -1 by A1,Def4; end; theorem Th25: for p being prime natural number, a being integer number holds (Leg(a,p) = 1 iff a gcd p = 1 & a is_quadratic_residue_mod p) & (Leg(a,p) = 0 iff p divides a) & (Leg(a,p) = -1 iff a gcd p = 1 & a is_quadratic_non_residue_mod p) proof let p be prime natural number, a be integer number; A1:now assume A2: Leg(a,p) = 0; now assume not p divides a; then a gcd p = 1 by Th6; hence contradiction by A2,Def4; end; hence p divides a; end; now assume A3: Leg(a,p) = 1; then a gcd p = 1 by Th6,Def4; hence a gcd p = 1 & a is_quadratic_residue_mod p by A3,Def4; end; hence Leg(a,p) = 1 iff a gcd p = 1 & a is_quadratic_residue_mod p by Def4; now assume A4: Leg(a,p) = -1; then a gcd p = 1 by Th6,Def4; hence a gcd p = 1 & a is_quadratic_non_residue_mod p by A4,Def4; end; hence thesis by A1,Def4; end; theorem for p being natural number holds Leg(p,p) = 0 by Def3; theorem for a being integer number holds Leg(a,2) = a mod 2 proof let a be integer number; per cases; suppose A1: a is even; then a mod 2 = 0 by INT_1:62; hence thesis by A1,Def3; end; suppose A2: a is odd; reconsider amod2 = a mod 2 as Element of NAT by INT_1:3,INT_1:57; A3: amod2 = 0 or amod2 = 1 by NAT_1:23,INT_1:58; a - 1 = (a div 2) * 2 + 1 - 1 by A3,A2,INT_1:62,INT_1:59; then A4: 1,a are_congruent_mod 2 by INT_1:def 5,INT_1:14; a gcd 2 <= 2 by INT_2:27,INT_2:21; then A5: a gcd 2 = 0 or ... or a gcd 2 = 2; 1|^(1+1) = 1; hence thesis by A4,INT_2:5,A5,INT_2:21,A3,A2,INT_1:62,Def3,Th22; end; end; Lm4: for a be integer number, p be prime natural number holds Lege(a,p) = Leg(a,p) proof let a be integer number, p be prime natural number; per cases by Th24; suppose A1: Leg(a,p) = 1; then not(p divides a) by Th25; then a mod p <> 0 by INT_1:62; hence thesis by A1,INT_5:def 3,Th25; end; suppose A2: Leg(a,p) = 0; then A3: p divides a by Th25; p divides (-a) by A2,Th25,INT_2:10; then A4: (0^2 - a) mod p = 0 by INT_1:62; a mod p = 0 by A3,INT_1:62; hence thesis by A2,A4,INT_5:def 3,INT_5:def 2; end; suppose Leg(a,p) = -1; hence thesis by Th25,INT_5:def 3; end; end; theorem Th28: for p being 2_greater prime natural number, a,b being integer number st a gcd p = 1 & b gcd p = 1 & a,b are_congruent_mod p holds Leg(a,p) = Leg(b,p) proof let p be 2_greater prime natural number, a,b be integer number; assume A1: a gcd p = 1 & b gcd p = 1 & a,b are_congruent_mod p; thus Leg(a,p) = Lege(a,p) by Lm4 .= Lege(b,p) by Def1,A1,INT_5:29 .= Leg(b,p) by Lm4; end; theorem for p being 2_greater prime natural number, a,b being integer number st a gcd p = 1 & b gcd p = 1 holds Leg(a*b,p) = Leg(a,p) * Leg(b,p) proof let p be 2_greater prime natural number, a,b be integer number; assume A1: a gcd p = 1 & b gcd p = 1; thus Leg(a*b,p) = Lege(a*b,p) by Lm4 .= Lege(a,p) * Lege(b,p) by A1,Def1,INT_5:30 .= Leg(a,p) * Lege(b,p) by Lm4 .= Leg(a,p) * Leg(b,p) by Lm4; end; theorem Th30: for p,q being 2_greater prime natural number st p <> q holds Leg(p,q) * Leg(q,p) = (-1)|^( ((p-1)/2) * ((q-1)/2) ) proof let p,q be 2_greater prime natural number; assume A1: p <> q; A2: p > 2 & q > 2 by Def1; p - 1 > 2 - 1 by Def1,XREAL_1:9; then p -' 1 = p - 1 by NAT_D:39; then A3: (p-'1) div 2 = (p-1)/2 by Th4; q - 1 > 2 - 1 by Def1,XREAL_1:9; then q -' 1 = q - 1 by NAT_D:39; then A4: (-1)|^(((p-'1) div 2)*((q-'1) div 2)) = (-1)|^( ((p-1)/2) * ((q-1)/2) ) by A3,Th4; thus Leg(p,q) * Leg(q,p) = Leg(p,q) * Lege(q,p) by Lm4 .= Lege(p,q) * Lege(q,p) by Lm4 .= (-1)|^( ((p-1)/2) * ((q-1)/2) ) by A1,A2,A4,INT_5:49; end; ::\$N Euler's criterion theorem Th31: for p being 2_greater prime natural number, a being integer number st a gcd p = 1 holds a|^((p-1)/2), LegendreSymbol(a,p) are_congruent_mod p proof let p be 2_greater prime natural number, a be integer number; p - 1 > 2 - 1 by Def1,XREAL_1:9; then A1: p -' 1 = p - 1 by NAT_D:39; assume a gcd p = 1; then Lege (a,p),a|^((p-'1) div 2) are_congruent_mod p by Def1,INT_5:28; then A2: Lege (a,p),a|^((p-1)/2) are_congruent_mod p by A1,Th4; Leg(a,p) = Lege(a,p) by Lm4; hence thesis by A2,INT_1:14; end; begin :: Proth Numbers ::\$N Proth numbers definition let p be natural number; attr p is Proth means :Def5: ex k being odd natural number, n being positive natural number st 2|^n > k & p = k * (2|^n) + 1; end; Lm5: 1 is odd proof 1 = 2 * 0 + 1; hence thesis; end; Lm6: 3 is Proth proof reconsider e = 1 as odd natural number by Lm5; take e,1; thus thesis; end; Lm7: 9 is Proth proof A1: 2|^2 = 2|^(1+1) .= 2|^1 * 2 by NEWTON:6 .= 2 * 2; A2: 2|^3 = 2|^(2+1) .= 4 * 2 by A1,NEWTON:6; reconsider e = 1 as odd natural number by Lm5; take e,3; thus thesis by A2; end; registration cluster Proth prime for natural number; existence by Lm6,PEPIN:41; cluster Proth non prime for natural number; existence proof 3 * 3 = 9; then 3 divides 9; then 9 is non prime; hence thesis by Lm7; end; end; registration cluster Proth -> non trivial odd for natural number; coherence proof let p be natural number; assume A1: p is Proth; then consider k being odd natural number, n being positive natural number such that A2: 2|^n > k & p = k * 2|^n + 1; thus p is non trivial by A1,NAT_2:def 1; reconsider n1 = n - 1 as Element of NAT by INT_1:3; 2 * 2|^n1 = 2|^(1+n1) by NEWTON:6 .= 2|^n; hence thesis by A2; end; end; theorem 3 is Proth by Lm6; theorem 5 is Proth proof A1: 2|^2 = 2|^(1+1) .= 2|^1 * 2 by NEWTON:6 .= 2 * 2; reconsider e = 1 as odd natural number by Lm5; take e,2; thus thesis by A1; end; theorem 9 is Proth by Lm7; theorem 13 is Proth proof A1: 2|^2 = 2|^(1+1) .= 2|^1 * 2 by NEWTON:6 .= 2 * 2; 3 = 2 * 1 + 1; then reconsider e = 3 as odd natural number; take e,2; thus thesis by A1; end; theorem 17 is Proth proof A1: 2|^2 = 2|^(1+1) .= 2|^1 * 2 by NEWTON:6 .= 2 * 2; A2: 2|^3 = 2|^(2+1) .= 2|^2 * 2 by NEWTON:6 .= 8 by A1; A3: 2|^4 = 2|^(3+1) .= 2|^3 * 2 by NEWTON:6 .= 16 by A2; reconsider e = 1 as odd natural number by Lm5; take e,4; thus thesis by A3; end; theorem Th37: 641 is Proth proof A1: 2|^2 = 2|^(1+1) .= 2|^1 * 2 by NEWTON:6 .= 2 * 2; then 2|^(2+2) = 4 * 4 by NEWTON:8; then A2: 2|^(4+2) = 16 * 4 by A1,NEWTON:8; A3: 2|^(6+1) = 2|^6 * 2|^1 by NEWTON:8 .= 64 * 2 by A2; A4: 5 = 2 * 2 + 1; 641 = 5 * 2|^7 + 1 by A3; hence thesis by A3,A4; end; theorem 11777 is Proth proof A1: 2|^2 = 2|^(1+1) .= 2|^1 * 2 by NEWTON:6 .= 2 * 2; A2: 2|^(2+2) = 4 * 4 by A1,NEWTON:8; A3: 2|^(4+4) = 16 * 16 by A2,NEWTON:8; A4: 2|^(8+1) = 2|^8 * 2|^1 by NEWTON:8 .= 256 * 2 by A3; A5: 23 = 2 * 11 + 1; 11777 = 23 * 2|^9 + 1 by A4; hence thesis by A4,A5; end; theorem 13313 is Proth proof A1: 2|^2 = 2|^(1+1) .= 2|^1 * 2 by NEWTON:6 .= 2 * 2; then 2|^(2+2) = 4 * 4 by NEWTON:8; then 2|^(4+4) = 16 * 16 by NEWTON:8; then A2: 2|^(8+2) = 256 * 4 by A1,NEWTON:8; A3: 13 = 2 * 6 + 1; 13313 = 13 * 2|^10 + 1 by A2; hence thesis by A2,A3; end; ::\$N Proth's theorem theorem Th40: :: Proth for n being Proth natural number holds n is prime iff ex a being natural number st a|^((n-1)/2), -1 are_congruent_mod n proof let n be Proth natural number; consider k being odd natural number, l being positive natural number such that A1: 2|^l > k & n = k * (2|^l) + 1 by Def5; set s = 2|^l; A2: l + 1 >= 1 + 1 by NAT_1:14,XREAL_1:6; 2|^l >= l + 1 by NEWTON:85; then 2|^l <>0 & 2|^l <> 1 by A2,XXREAL_0:2; then reconsider s as non trivial natural number by NAT_2:def 1; reconsider s as non trivial Divisor of n-1 by A1,INT_1:def 3,Def2; A3: now assume ex a being natural number st a |^ ((n-1) / 2), -1 are_congruent_mod n; then consider a being natural number such that A4: a |^ ((n-1) / 2), -1 are_congruent_mod n; A5: (a |^ ((n-1) / 2)) * (a |^ ((n-1) / 2)) = a |^ ( ((n-1) / 2) + ((n-1) / 2) ) by NEWTON:8 .= a|^(n-1); A6: (-1) * (-1) = 1; A7: l >= 1 by NAT_1:14; (2|^l - 1) + 1 > k by A1; then A8: k <= 2|^l - 1 by NAT_1:13; then k * 2|^ l <= (2|^l - 1) * 2|^l by XREAL_1:64; then A9: n <= (2|^l - 1) * 2|^l + 1 by A1,XREAL_1:6; (2|^l - 1) * 2|^l + 1 = (2|^l) * (2|^l) - 2|^l + 1 .= 2|^(l+l) - 2|^l + 1 by NEWTON:8; then A10: n < 2|^(l+l) - 2|^l + 1 + 1 by A9,NAT_1:13; A11: s > sqrt(n) proof per cases; suppose l >= 2; then A12: 2|^l >= 2|^2 by Th1; 2|^(1+1) = 2|^1 * 2 by NEWTON:6 .= 2 * 2; then 2|^l > 2 by A12,XXREAL_0:2; then 2 - 2|^l < 2|^l - 2|^l by XREAL_1:9; then 2|^(l+l) + (-2|^l + 2) < 2|^(l+l) + 0 by XREAL_1:6; then A13: n < 2|^(2*l) by A10,XXREAL_0:2; (2|^l)^2 = 2|^(l+l) by NEWTON:8; then sqrt(2|^(2*l)) = 2|^l by SQUARE_1:def 2; hence thesis by A13,SQUARE_1:27; end; suppose l < 2; then l < 1 + 1; then A14: l <= 1 by NAT_1:13; then A15: l = 1 by A7,XXREAL_0:1; then A16: s = sqrt 4 by SQUARE_1:20; A17: n = k*2|^1 + 1 by A14,A1,A7,XXREAL_0:1 .= k*2 + 1; A18: k <= 2 - 1 by A8,A15; k >= 1 by NAT_1:14; then k = 1 by A18,XXREAL_0:1; hence thesis by A17,A16,SQUARE_1:27; end; end; now let q be prime Divisor of s; A19: a|^((n-1)/q), -1 are_congruent_mod n by A4,Th8,INT_2:28,Def2; 1 * (a|^((n-1)/q) - 1) = a|^((n-1)/q) - 1; then A20: 1 divides a|^((n-1)/q) - 1; 1 * n = n; then A21: 1 divides n; now let m be Integer; assume A22: m divides a|^((n-1)/q) - 1 & m divides n; then A23: a|^((n-1)/q), 1 are_congruent_mod m; consider j being Integer such that A24: m * j = n by A22; a|^((n-1)/q), -1 are_congruent_mod m by A19,A24,INT_1:20; then a|^((n-1)/q) - a|^((n-1)/q), (-1)- 1 are_congruent_mod m by A23,INT_1:17; then 0+1,(-2)+1 are_congruent_mod m; then A25: m = 2 or m = 1 or m = -2 or m = -1 by Th20,INT_1:14; A26: now assume (-2) divides n; then consider g being Integer such that A27: n = (-2) * g; n = 2 * (-g) by A27; hence contradiction; end; 1 * 1 = 1 & (-1) * (-1) = 1; hence m divides 1 by A26,A22,A25; end; hence a|^((n-1)/q) - 1 gcd n = 1 by A20,A21,INT_2:def 2; end; hence n is prime by A4,A5,INT_1:18,A6,A11,Th21; end; now assume n is prime; then reconsider m = n as prime Proth natural number; Z/Z*(m) is cyclic by INT_7:31; then consider g being Element of Z/Z*(m) such that A28: ord(g) = card(Z/Z*(m)) by GR_CY_1:19; A29: ord g = m-1 by A28,INT_7:23; Z/Z*(m) = multMagma(#Segm0(m),multint0(m)#) by INT_7:def 4; then reconsider g1 = g as natural number; A30: not(g is being_of_order_0) by A28,GROUP_1:def 11; A31: (g1 |^ (m-1)) mod m = g |^ (m-1) by Th17 .= 1_(Z/Z*(m)) by A29,A30,GROUP_1:def 11 .= 1 by INT_7:21; A32: g1 |^ (m-1), 1 are_congruent_mod m by Th10,A31; A33: (g1 |^ ((m-1) / 2)) |^ (1+1) = (g1 |^ ((m-1) / 2)) |^ 1 * (g1 |^ ((m-1) / 2)) by NEWTON:6 .= (g1 |^ ((m-1) / 2)) * (g1 |^ ((m-1) / 2)) .= g1 |^ (((m-1) / 2) + ((m-1) / 2)) by NEWTON:8 .= g1 |^ (m-1); now assume A34: g1 |^ ((m-1) / 2), 1 are_congruent_mod n; A35: 1_(Z/Z*(m)) = 1 by INT_7:21 .= (g1 |^ ((m-1) / 2)) mod m by A34,INT_2:def 4,Th12 .= g |^ ((m-1) / 2) by Th17; A36: m-1 <> 0; (m-1) * 2 >= (m-1) * 1 & 0<2 by XREAL_1:64; then A37: (m-1) / 2 <= m-1 by XREAL_1:79; m-1 <= (m-1)/2 by A29,A30,A35,GROUP_1:def 11; then m-1 = (m-1)/2 by A37,XXREAL_0:1; hence contradiction by A36; end; hence ex a being natural number st a |^ ((n-1) / 2), -1 are_congruent_mod n by A33,A32,Th18; end; hence thesis by A3; end; theorem Th41: :: Proth for l being 2_or_greater natural number, k being positive natural number st not(3 divides k) & k <= 2|^l - 1 holds k * 2|^l + 1 is prime iff 3|^(k*2|^(l-1)), -1 are_congruent_mod k* 2|^l + 1 proof let l be 2_or_greater natural number, k be positive natural number; assume A1: not 3 divides k & k <= 2|^l - 1; set s = 2|^l, a = 3, n = k*2|^l + 1; k >= 1 by NAT_1:14; then k * 2|^l >= 1 * 2|^l by XREAL_1:66; then A2: n >= 2|^l + 1 by XREAL_1:7; A3: (2|^l)/2 = 2|^((l-1)+1) * 2" .= (2|^(l-1) * 2) * 2" by NEWTON:6 .= 2|^(l-1) * 1; A4: 2 * (k * 2|^(l-1)) = k * (2 * 2|^(l-1)) .= k * 2|^((l-1)+1) by NEWTON:6; A5: l >= 1 by NAT_1:14; A6: l + 1 >= 1 + 1 by NAT_1:14,XREAL_1:6; A7: 2|^l >= l + 1 by NEWTON:85; then 2|^l >= 1 + 1 by A6,XXREAL_0:2; then 2|^l + 1 >= 2 + 1 by XREAL_1:7; then n >= 2 + 1 by A2,XXREAL_0:2; then n > 2 by NAT_1:13; then reconsider n as 2_greater odd natural number by A4,Def1; 2 * (k * 2|^(l-1)) = k * (2 * 2|^(l-1)) .= k * 2|^((l-1)+1) by NEWTON:6; then reconsider k2 = (k*2|^l)/2 as natural number; A8: 3|^((n-1)/2) = 3|^(k*2|^(l-1)) by A3; A9:now assume A10: 3|^(k*2|^(l-1)), -1 are_congruent_mod k* 2|^l + 1; reconsider s as Divisor of n-1 by INT_2:2,Def2; s <> 0 & s <> 1 by A7,A6,XXREAL_0:2; then reconsider s as non trivial Divisor of n-1 by NAT_2:def 1; A11: (3|^(k*2|^(l-1))) * (3|^(k*2|^(l-1))),(-1)*(-1) are_congruent_mod n by A10,INT_1:18; A12: (3|^(k*2|^(l-1))) * (3|^(k*2|^(l-1))) = 3|^(k*2|^(l-1)+k*2|^(l-1)) by NEWTON:8 .= 3|^(k*(2|^(l-1)*2)) .= 3|^(k*(2|^(l-1+1))) by NEWTON:6 .= 3|^(k*2|^l); A13: k * 2|^ l <= (2|^l - 1) * 2|^l by A1,XREAL_1:64; A14: (2|^l - 1) * 2|^l + 1 = (2|^l) * (2|^l) - 2|^l + 1 .= 2|^(l+l) - 2|^l + 1 by NEWTON:8; then n <= 2|^(l+l) - 2|^l + 1 by A13,XREAL_1:6; then A15: n < 2|^(l+l) - 2|^l + 1 + 1 by A14,NAT_1:13; A16: s > sqrt(n) proof per cases; suppose l >= 2; then A17: 2|^l >= 2|^2 by Th1; 2|^(1+1) = 2|^1 * 2 by NEWTON:6 .= 2 * 2; then 2|^l > 2 by A17,XXREAL_0:2; then 2 - 2|^l < 2|^l - 2|^l by XREAL_1:9; then 2|^(l+l) + (-2|^l + 2) < 2|^(l+l) + 0 by XREAL_1:6; then A18: n < 2|^(2*l) by A15,XXREAL_0:2; (2|^l)^2 = 2|^(l+l) by NEWTON:8; then sqrt(2|^(2*l)) = 2|^l by SQUARE_1:def 2; hence thesis by A18,SQUARE_1:27; end; suppose l < 2; then l < 1 + 1; then l <= 1 by NAT_1:13; then A19: l = 1 by A5,XXREAL_0:1; then A20: n = k*2 + 1; A21: k <= 2 - 1 by A1,A19; k >= 1 by NAT_1:14; then k = 1 by A21,XXREAL_0:1; hence thesis by A20,SQUARE_1:27,SQUARE_1:20; end; end; now let q be prime Divisor of s; A22: a|^((n-1)/q), -1 are_congruent_mod n by A8,A10,Th8,INT_2:28,Def2; 1 * (a|^((n-1)/q) - 1) = a|^((n-1)/q) - 1; then A23: 1 divides a|^((n-1)/q) - 1; 1 * n = n; then A24: 1 divides n; now let m be Integer; assume A25: m divides a|^((n-1)/q) - 1 & m divides n; then A26: a|^((n-1)/q), 1 are_congruent_mod m; consider j being Integer such that A27: m * j = n by A25; a|^((n-1)/q), -1 are_congruent_mod m by A22,A27,INT_1:20; then a|^((n-1)/q) - a|^((n-1)/q), (-1)- 1 are_congruent_mod m by A26,INT_1:17; then 0+1,(-2)+1 are_congruent_mod m; then m = 2 or m = 1 or m = -2 or m = -1 by Th20,INT_1:14; hence m divides 1 by A25,INT_2:10,ABIAN:def 1; end; hence a|^((n-1)/q) - 1 gcd n = 1 by A23,A24,INT_2:def 2; end; hence k * 2|^l + 1 is prime by A12,A11,A16,Th21; end; now assume n is prime; then reconsider n as 2_greater prime natural number; reconsider two = 2 as prime natural number by INT_2:28; reconsider three = 3 as 2_greater prime natural number by Def1,PEPIN:41; A28: 2|^l + 1 >= 2|^2 + 1 by XREAL_1:6,EC_PF_2:def 1; 2|^2 = 2|^(1+1) .= 2|^1 * 2 by NEWTON:6 .= 2 * 2; then A29: 3 <> n by A28,A2,XXREAL_0:2; A30: not(n,0 are_congruent_mod 3) by A29,INT_2:def 4; A31: now assume A32: n,1 are_congruent_mod 3; not (three divides 2|^l) by Th8,INT_2:28; then 3 gcd (2|^l) = 1 by Th6; hence contradiction by A1,INT_2:25,A32,INT_2:def 3; end; n,0 are_congruent_mod 3 or ... or n,(3-1) are_congruent_mod 3 by Th13; then A33: n,0 are_congruent_mod 3 or ... or n,2 are_congruent_mod 3; A34: 2,2+1 are_coprime by PEPIN:1; not(three divides n) by A29,INT_2:def 4; then A35: n gcd 3 = 1 by Th6; A36: ((3-1)/2) * ((n-1)/2) = 1 * ((n-1)/2); (n-1)/2 = (k * 2|^((l-1)+1))/2 .= (k * (2|^(l-1) * 2))/2 by NEWTON:6 .= k * 2|^(l-2+1) .= k * (2|^(l-2) * 2) by NEWTON:6 .= 2 * k * 2|^(l-2); then A37: (-1)|^((n-1)/2) = 1; Leg(three,n) * Leg(n,three) = 1 by A36,A37,A29,Th30; then Leg(three,n) = 1 & Leg(n,three) = 1 or Leg(three,n) = - 1 & Leg(n,three) = - 1 by INT_1:9; then Leg(3,n) = Leg(two,three) by A35,A33,A30,A31,A34,Th28 .= -1 by Th23,A34,Def4; hence 3|^(k*2|^(l-1)), -1 are_congruent_mod k* 2|^l + 1 by A8,A35,Th31; end; hence thesis by A9; end; theorem 641 is prime proof 641 = 2 * 320 + 1; then reconsider n = 641 as odd natural number; A1: 256 + 64 = 320; A2: 3 * 3 = 3|^1 * 3 .= 3|^1 * 3|^1 .= 3|^(1+1) by NEWTON:8; A3: 3|^2 * 3|^2 = 3|^(2+2) by NEWTON:8; A4: 3|^4 * 3|^4 = 3|^(4+4) by NEWTON:8; 6561 = 10 * 641 + 151; then 3|^8, 151 are_congruent_mod 641 by A4,A3,A2; then (3|^8) * (3|^8), 151 * 151 are_congruent_mod 641 by INT_1:18; then A5: 3|^(8+8), 22801 are_congruent_mod 641 by NEWTON:8; 22801 = 35 * 641 + 366; then 22801, 366 are_congruent_mod 641; then 3|^16, 366 are_congruent_mod 641 by A5,INT_1:15; then A6: (3|^16) * (3|^16), 366 * 366 are_congruent_mod 641 by INT_1:18; A7: 183,183 are_congruent_mod 641 by INT_1:11; 732,91 are_congruent_mod 641; then 732 * 183, 91 * 183 are_congruent_mod 641 by A7,INT_1:18; then (3|^16) * (3|^16),91 * 183 are_congruent_mod 641 by A6,INT_1:15; then A8: 3|^(16+16),91 * 183 are_congruent_mod 641 by NEWTON:8; 16653 = 26 * 641 + (-13); then 16653,-13 are_congruent_mod 641; then 3|^32, -13 are_congruent_mod 641 by A8,INT_1:15; then (3|^32) * (3|^32), (-13) * (-13) are_congruent_mod 641 by INT_1:18; then A9: 3 |^ (32+32), 169 are_congruent_mod 641 by NEWTON:8; then A10: (3|^64) * (3|^64), 169 * 169 are_congruent_mod 641 by INT_1:18; 28561 = 44 * 641 + 357; then 28561,357 are_congruent_mod 641; then (3|^64) * (3|^64), 357 are_congruent_mod 641 by A10,INT_1:15; then 3|^(64+64), 357 are_congruent_mod 641 by NEWTON:8; then A11: (3|^128) * (3|^128), 357 * 357 are_congruent_mod 641 by INT_1:18; A12: 119,119 are_congruent_mod 641 by INT_1:11; 1071,430 are_congruent_mod 641; then 1071 * 119, 430 * 119 are_congruent_mod 641 by A12,INT_1:18; then (3|^128) * (3|^128),430 * 119 are_congruent_mod 641 by A11,INT_1:15; then A13: 3|^(128+128),3010 * 17 are_congruent_mod 641 by NEWTON:8; A14: 17,17 are_congruent_mod 641 by INT_1:11; 3010 = 4 * 641 + 446; then 3010,446 are_congruent_mod 641; then 3010*17,446*17 are_congruent_mod 641 by A14,INT_1:18; then A15: 3|^(128+128),446*17 are_congruent_mod 641 by A13,INT_1:15; 7582 = 12 * 641 + (-110); then 7582,-110 are_congruent_mod 641; then 3 |^ 256, -110 are_congruent_mod 641 by A15,INT_1:15; then (3 |^ 256) * (3|^64), (-110) * 169 are_congruent_mod 641 by A9,INT_1:18; then A16: 3 |^ 320, -18590 are_congruent_mod 641 by A1,NEWTON:8; A17: -18590 = (-30) * 641 + 640; A18: 640,-1 are_congruent_mod 641; -18590,640 are_congruent_mod 641 by A17; then -18590,-1 are_congruent_mod 641 by A18,INT_1:15; then ex a being natural number st a|^((n-1)/2),-1 are_congruent_mod n by A16,INT_1: 15; hence thesis by Th40,Th37; end; begin :: Fermat Numbers registration let l be natural number; cluster Fermat l -> Proth; coherence proof reconsider p = Fermat l as natural number; set k = 1, n = 2|^l; A3: 2|^n > n by NEWTON:86; n + 1 > 0 + 1 by XREAL_1:6; then n >= 1 by NAT_1:13; then A1: 2|^n > k by A3,XXREAL_0:2; A2: 2 * 0 + 1 = 1; p = k * (2|^n) + 1 by PEPIN:def 3; hence thesis by A1,A2; end; end; ::\$N Pepin's theorem theorem :: Pepin for l being non zero natural number holds Fermat l is prime iff 3|^((Fermat l - 1)/2), -1 are_congruent_mod Fermat l proof let l be non zero natural number; set k = 1; A1: 2|^2 = 2|^(1+1) .= 2|^1 * 2 by NEWTON:6 .= 2 * 2; l + 1 >= 0 + 1 by XREAL_1:6; then l >= 1 by NAT_1:13; then 2|^l >= 2|^1 by Th1; then 2|^l >= 2; then reconsider l1 = 2|^l as 2_or_greater natural number by EC_PF_2:def 1; A2: not(3 divides k) by INT_2:27; 2|^l1 - 1 >= 4 - 1 by A1,XREAL_1:9,EC_PF_2:def 1; then A3: 1 <= 2|^l1 - 1 by XXREAL_0:2; A4: k * 2|^l1 + 1 = Fermat l by PEPIN:def 3; (Fermat l - 1)/2 = (2 |^ (2 |^ l) + 1 - 1) / 2 by PEPIN:def 3 .= 2|^(l1-1+1) / 2 .= (2|^(l1 - 1) *2) / 2 by NEWTON:6 .= k * 2|^(l1-1); hence thesis by A2,A3,A4,Th41; end; theorem Fermat 5 is non prime proof A1: 2|^7 * 2|^7 = 2|^(7+7) by NEWTON:8; A2: 5 * 5 = 5|^1 * 5 .= 5|^1 * 5|^1 .= 5|^(1+1) by NEWTON:8; A3: 5|^2 * 5|^2 = 5|^(2+2) by NEWTON:8; A4: 2|^14 * 2|^14 = 2|^(14+14) by NEWTON:8; A5: 2|^4 * 2|^28 = 2|^(4+28) by NEWTON:8; A6: 2|^2 = 2|^(1+1) .= 2|^1 * 2 by NEWTON:6 .= 2 * 2; A7: 2|^3 = 2|^(2+1) .= 2|^2 * 2 by NEWTON:6 .= 8 by A6; A8: 2|^4 = 2|^(3+1) .= 2|^3 * 2 by NEWTON:6 .= 16 by A7; A9: 2|^(3+4) = 8 * 16 by A8,A7,NEWTON:8; 5 * 2|^7, -1 are_congruent_mod 641 by A9; then (5 * 2|^7) * (5 * 2|^7), (-1)*(-1) are_congruent_mod 641 by INT_1:18; then A10: (5|^2*2|^14)*(5|^2*2|^14), 1*1 are_congruent_mod 641 by A1,A2,INT_1: 18; (5|^4 + 2|^4) - 2|^4, 0 - 2|^4 are_congruent_mod 641 by A2,A3,A8; then A11: -2|^4, 5|^4 are_congruent_mod 641 by INT_1:14; 2|^28, 2|^28 are_congruent_mod 641 by INT_1:11; then (-2|^4) * 2|^28, 5|^4 * 2|^28 are_congruent_mod 641 by A11,INT_1:18; then A12: -2|^32, 1 are_congruent_mod 641 by A3,A4,A5,A10,INT_1:15; -1, -1 are_congruent_mod 641 by INT_1:11; then A13: (-1) * (-2|^32), (-1) * 1 are_congruent_mod 641 by A12,INT_1:18; A14: 5 * 2|^7 + 1 = 641 by A9; 2|^(4+1) = 16 * 2 by A8,NEWTON:6; then A15: Fermat 5 = 2|^32 + 1 by PEPIN:def 3; 5 * 2|^7 < 2|^3 * 2|^7 by A7,XREAL_1:68; then A16: 5 * 2|^7 < 2|^(3+7) by NEWTON:8; 2 is non trivial; then 2|^10 < 2|^32 by Th2; then 5* 2|^7 < 2|^32 by A16,XXREAL_0:2; then 641 < 2|^32 + 1 by A14,XREAL_1:6; hence thesis by A15,A13; end; begin :: Cullen numbers ::\$N Cullen numbers definition let n be natural number; func CullenNumber n -> natural number equals n * 2|^n + 1; coherence; end; registration let n be non zero natural number; cluster CullenNumber n -> Proth; coherence proof consider k being natural number, l being odd natural number such that A1: n = l * 2|^k by Th3; A2: n * 2|^n + 1 = l* (2|^k * 2|^n) + 1 by A1 .= l * 2|^(k+n) + 1 by NEWTON:8; 2|^k + 1 > 0 + 1 by XREAL_1:6; then 2|^k >= 1 by NAT_1:13; then A3: 2|^k * l >= 1 * l by XREAL_1:64; A4: 2|^(k+n) > k+n by NEWTON:86; k + n >= n by NAT_1:11; then k + n >= l by A1,A3,XXREAL_0:2; then 2|^(k+n) > l by A4,XXREAL_0:2; hence thesis by A2; end; end;