:: Fermat's Little Theorem via Divisibility of {N}ewton's Binomial :: by Rafa{\l} Ziobro :: :: Received June 30, 2015 :: Copyright (c) 2015-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 ABIAN, NUMBERS, NAT_1, INT_1, FINSEQ_1, ARYTM_3, XXREAL_0, CARD_1, ARYTM_1, INT_2, COMPLEX1, RELAT_1, REAL_1, XCMPLX_0, XREAL_0, ORDINAL1, ORDINAL4, NEWTON, POWER, PREPOWER, FUNCT_1, CARD_3, SUBSET_1, TARSKI, RFINSEQ, XBOOLE_0, REALSET1, PARTFUN1; notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, XCMPLX_0, XREAL_0, NUMBERS, XXREAL_0, ABIAN, POWER, INT_1, INT_2, NEWTON, ABSVALUE, PREPOWER, RELAT_1, FUNCT_1, RECDEF_1, PARTFUN1, RFINSEQ, RVSUM_1, FINSEQ_1, IRRAT_1; constructors ABIAN, SQUARE_1, NAT_D, NEWTON, POWER, PREPOWER, RFINSEQ, WSIERP_1, RECDEF_1, RELSET_1; registrations ABIAN, ORDINAL1, XXREAL_0, XREAL_0, NAT_1, INT_1, NEWTON, XCMPLX_0, WSIERP_1, POWER, NEWTON01, NAT_6, FUNCT_1, NUMBERS, FINSEQ_1, XBOOLE_0, VALUED_0, CARD_1, RVSUM_1, RELAT_1, NAT_3, INT_6, LAGRA4SQ; requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM; begin :: Divisibility of Newton's Binomial reserve a,b,c,d,m,x,n,j,k,l for Nat, t,u,v,z for Integer, f,F for FinSequence of NAT; reserve p,q,r,s for real number; registration let a be Complex; reduce 1*a|^0 to 1; end; registration let n be non zero Nat; reduce 0|^n to 0; end; registration let a be Nat; reduce |.a.| to a; end; registration let a be Nat; reduce a gcd 0 to a; end; registration let t,z; reduce (t mod z) mod z to t mod z; end; registration let t; reduce 0 mod t to 0; end; registration let u,z; reduce (0 + u*z) mod z to 0; end; registration let r be non zero Real; let n be even natural number; cluster r |^ n -> positive; end; :: some remarks on divisibility of the differences of like powers theorem :: NEWTON02:1 t gcd z = -t gcd z; ::see also NAT_3:1 theorem :: NEWTON02:2 t divides z & u divides v implies t*u divides z*v; theorem :: NEWTON02:3 t divides z iff t gcd z = |.t.|; theorem :: NEWTON02:4 t*u divides z*u iff |.u.|*(t gcd z) = |.u.|*|.t.|; theorem :: NEWTON02:5 (t+u*z) gcd z = t gcd z & (t-u*z) gcd z = t gcd z; theorem :: NEWTON02:6 n>0 implies t divides t|^n; theorem :: NEWTON02:7 a|^n gcd b|^n = (a gcd b)|^n; theorem :: NEWTON02:8 a > b & a,b are_coprime implies (a+b) gcd (a-b) <= 2; theorem :: NEWTON02:9 t gcd z is even iff t is even & z is even; theorem :: NEWTON02:10 t divides ((t+z)|^n - z|^n) & z divides ((t+z)|^n - t|^n); theorem :: NEWTON02:11 u divides (u+z)|^n iff u divides z|^n; theorem :: NEWTON02:12 t divides (t+z)|^n implies t divides (t+z)|^n + z|^n; theorem :: NEWTON02:13 (t+u) divides ((t+2*u)|^n - u|^n); theorem :: NEWTON02:14 l>0 & t divides z implies t divides z|^l; theorem :: NEWTON02:15 t divides z implies t|^n divides z|^n; theorem :: NEWTON02:16 n>0 & not t divides (t+z)|^n implies not t divides z; theorem :: NEWTON02:17 m>0 implies t*z divides (t+z)|^m - (t|^m + z|^m); theorem :: NEWTON02:18 t-z divides t|^m - z|^m; theorem :: NEWTON02:19 n>0 implies t*z divides (t-z)|^n - (t|^n + (-z)|^n); theorem :: NEWTON02:20 t*z divides (t+z)|^n - (t-z)|^n + ((-z)|^n - z|^n); theorem :: NEWTON02:21 n>0 implies t divides (t+z)|^n + (t|^n - z|^n); theorem :: NEWTON02:22 u divides t+z & u divides t-z implies u divides 2*t & u divides 2*z; theorem :: NEWTON02:23 t*z divides (t+z)|^(2*n) - (t-z)|^(2*n); theorem :: NEWTON02:24 n>0 implies t*z divides (t-z)|^(2*n) - (t|^(2*n) + z|^(2*n)); theorem :: NEWTON02:25 t*z divides (t-z)|^(2*n+1) - (t|^(2*n+1) - z|^(2*n+1)); theorem :: NEWTON02:26 k>0 & x divides a+k & x divides a-k implies x <= 2*k; :: gcd theorem :: NEWTON02:27 k>0 implies a gcd b <= a gcd b*k; theorem :: NEWTON02:28 n > 0 implies (a gcd b) gcd b|^n = a gcd b; theorem :: NEWTON02:29 t+z,t are_coprime iff t+z,z are_coprime; theorem :: NEWTON02:30 a,b are_coprime & a*b = c|^n implies ex k st k|^n = a; theorem :: NEWTON02:31 for a,b st a,b are_coprime & a + b > 2 holds a+b divides a|^n+b|^n iff not a+b divides a|^n-b|^n; theorem :: NEWTON02:32 a,b are_coprime & a + b > 2 & n is odd implies not a+b divides a|^n-b|^n; theorem :: NEWTON02:33 a,b are_coprime & a + b > 2 & n is even implies not a+b divides a|^n+b|^n; theorem :: NEWTON02:34 a,b are_coprime implies a*b,(a|^(n+1) + b|^(n+1)) are_coprime; theorem :: NEWTON02:35 a,b are_coprime implies a*b,(a|^(n+1) - b|^(n+1)) are_coprime; theorem :: NEWTON02:36 q>0 & n>0 implies ex r st q = r|^n; theorem :: NEWTON02:37 k>0 & a+b > k & a+b divides k*a implies not a,b are_coprime; theorem :: NEWTON02:38 k>1 implies not k divides (k+1)|^n; theorem :: NEWTON02:39 a>1 & b>0 & a gcd b = 1 implies not a divides (a+b)|^n; :: inequalities (see also SERIES_3) theorem :: NEWTON02:40 for c st c > 0 for r,s be non negative Real holds r < s iff r|^c < s|^c; theorem :: NEWTON02:41 for r,s be non negative Real holds r >= s implies r|^n >= s|^n; theorem :: NEWTON02:42 a>0 & n>0 implies ex r st a|^n + b|^n = r|^n; theorem :: NEWTON02:43 for a holds ex b st b|^(n+1) <= a & a < (b+1)|^(n+1); theorem :: NEWTON02:44 n>0 & a>b & a,b are_coprime implies (a|^n+b|^n) gcd (a|^n -b|^n) <= 2; theorem :: NEWTON02:45 a+b divides c & a,c are_coprime implies a,b are_coprime; theorem :: NEWTON02:46 t,z are_coprime & t,u are_coprime & t is even implies u + z is even & u - z is even & u*z is odd; theorem :: NEWTON02:47 a,b are_coprime & c is even & a|^n + b|^n = c|^n implies a+b is even & a-b is even; theorem :: NEWTON02:48 a is even & a,b are_coprime implies (a-b),(a+b) are_coprime; theorem :: NEWTON02:49 a,b are_coprime implies (a+b),(a*b) are_coprime; theorem :: NEWTON02:50 not 3 divides a*b implies 3 divides (a+b)*(a-b); theorem :: NEWTON02:51 3 divides (a+b)*(a-b)+a*b iff 3 divides a & 3 divides b; theorem :: NEWTON02:52 b|^2 = a*(a-b) implies 3 divides a & 3 divides b; theorem :: NEWTON02:53 a,b are_coprime implies not 3 divides (a+b)*(a-b)+ a*b; theorem :: NEWTON02:54 a > b & a + b >= 2|^(n+1) implies a > 2|^n; theorem :: NEWTON02:55 :: see SERIES_3:6 a<>b implies 2*a*b < a|^2 + b|^2; theorem :: NEWTON02:56 n>0 & a<>b implies 2*(a|^n)*(b|^n) < a|^(2*n) + b|^(2*n); theorem :: NEWTON02:57 b>0 implies ex n st b >= 2|^n & b < 2|^(n+1); :: division by 4 theorem :: NEWTON02:58 for a,b be odd Nat holds (4 divides a + b iff not 4 divides a - b); theorem :: NEWTON02:59 b+c gcd b = 1 & c is odd implies 2*b + c gcd c = 1; theorem :: NEWTON02:60 a + b = k*a + k*b & a*b > 0 implies k = 1; theorem :: NEWTON02:61 t*z = t+z implies t=z; theorem :: NEWTON02:62 (2*n+1)|^2 = 4*n*(n+1)+1; theorem :: NEWTON02:63 a is odd & b is odd implies 8 divides a|^2 - b|^2; theorem :: NEWTON02:64 for a,b be odd Nat holds 4 divides a - b implies 4 divides a|^n-b|^n; theorem :: NEWTON02:65 for a,b be odd Nat, m be even Nat holds 4 divides a|^(m) - b|^(m); theorem :: NEWTON02:66 t is even & not 4 divides t implies ex u st u = t/2 & u is odd; theorem :: NEWTON02:67 a is odd & 2|^n divides a*b implies 2|^n divides b; theorem :: NEWTON02:68 for a,b,m be odd Nat holds 4 divides a|^m + b|^m iff 4 divides a + b; theorem :: NEWTON02:69 for a,b,m be odd Nat holds 4 divides a-b iff not 4 divides a|^m + b|^m; theorem :: NEWTON02:70 a|^2 + b|^2 = c|^2 implies ex t st b|^2 = (2*a+t)*t; theorem :: NEWTON02:71 b|^2 = (2*a+t)*t implies ex c st a|^2 + b|^2 = c|^2; theorem :: NEWTON02:72 a is odd & b is odd & m is even implies a|^m + b|^m <> c|^m; theorem :: NEWTON02:73 t,z|^n are_coprime & n > 0 implies t,z are_coprime; theorem :: NEWTON02:74 a,b are_coprime implies (a+b)|^2 gcd (a|^2 + b|^2 - (n-2)*a*b) = a|^2 + b|^2 - (n-2)*a*b gcd n; theorem :: NEWTON02:75 a,b are_coprime implies (a+b),(a|^2 + b|^2 + a*b) are_coprime; theorem :: NEWTON02:76 a,b are_coprime implies (a-b)|^2 gcd (a|^2 + b|^2 + (n-2)*a*b) = a|^2 + b|^2 + (n-2)*a*b gcd n; theorem :: NEWTON02:77 a divides k*(a*n+1) iff a divides k; theorem :: NEWTON02:78 for n be positive Nat holds a divides k*(a|^n+1) iff a divides k; theorem :: NEWTON02:79 for a,b be positive Nat holds a mod b = b mod a implies a = b; theorem :: NEWTON02:80 k*(a*n+1) mod a = k mod a; theorem :: NEWTON02:81 for n be positive Nat holds k*(a|^n+1) mod a = k mod a; theorem :: NEWTON02:82 for n be positive Nat holds k*(a|^n+1)|^m mod a = k mod a; theorem :: NEWTON02:83 for n be positive Nat holds b*(a|^n+1)|^m + c*(a|^n+1)|^l mod a = b+c mod a; theorem :: NEWTON02:84 for a,n be positive Nat holds a divides b*(a|^n+1)|^m + c*(a|^n+1)|^l iff a divides b+c; theorem :: NEWTON02:85 |.t.| < a implies t mod a = |.t.| or t mod a = a -|.t.|; theorem :: NEWTON02:86 -t mod a = (u*a - (t mod a)) mod a; theorem :: NEWTON02:87 for n be odd Nat holds t|^n mod 3 = t mod 3; theorem :: NEWTON02:88 (t + (u mod z))mod z = (t+u) mod z; theorem :: NEWTON02:89 for n be odd Nat holds (a+b-c) mod 3 = (a|^n+b|^n-c|^n) mod 3; theorem :: NEWTON02:90 for k be positive Nat holds t mod k = k - 1 iff (t+1) mod k = 0; theorem :: NEWTON02:91 a|^2 + b|^2 = c|^2 implies 3 divides a*b*c; theorem :: NEWTON02:92 for a,n be non zero Nat holds t mod a = z mod a implies t|^n mod a = z|^n mod a; theorem :: NEWTON02:93 3 divides t-z implies 3 divides t|^n - z|^n; theorem :: NEWTON02:94 for n be odd Nat holds 3 divides (a+b-c) iff 3 divides (a|^n+b|^n-c|^n); theorem :: NEWTON02:95 (t+u-z)|^2,(t|^2+u|^2+z|^2) are_congruent_mod 2; theorem :: NEWTON02:96 (t+u-z)|^3,(t|^3+u|^3-z|^3) are_congruent_mod 3; theorem :: NEWTON02:97 6 divides a|^3 - a; theorem :: NEWTON02:98 for a,b,c be odd Nat holds 3 divides t|^a + t|^b + t|^c; theorem :: NEWTON02:99 2|^m - 1 divides 2|^(2*m+1) - 2 & 2|^m + 1 divides 2|^(2*m+1) - 2; theorem :: NEWTON02:100 (u + t + z) is even implies u*t*z is even; theorem :: NEWTON02:101 t|^n + u|^n = z|^n implies 2|^n divides (t*u*z)|^n; theorem :: NEWTON02:102 t|^n,t|^m are_congruent_mod t-1; begin :: Fermat's Little Theorem Revisited reserve a,b,c,d,m,x,n,k,l for Nat, t,z for Integer, f,F,G for FinSequence of REAL; reserve q,r,s for real number; reserve D for set; theorem :: NEWTON02:103 for f be FinSequence holds f is D-valued iff f is FinSequence of D; :: Seg vs Segm theorem :: NEWTON02:104 k+1 in Seg n iff k < n; theorem :: NEWTON02:105 :: AFINSEQ_1:Lm1 n+1 <= len f iff n+1 in dom f; theorem :: NEWTON02:106 k in Segm n iff k+1 in Seg n; theorem :: NEWTON02:107 n in dom f & 1 <= m & m <= n implies f.m = (f|n).m; theorem :: NEWTON02:108 f is FinSequence of D implies f|n is FinSequence of D & f/^n is FinSequence of D; theorem :: NEWTON02:109 n in dom f implies (f|n).1 = f.1; theorem :: NEWTON02:110 for f be FinSequence of REAL st n in dom f holds len(f|n) = n; registration let s; cluster <*s*> -> REAL-valued; end; registration let D; let f be D-valued FinSequence; let n; cluster (f|n) -> D-valued; end; registration let D; let f be FinSequence of D; let n; cluster (f/^n) -> D-valued; end; theorem :: NEWTON02:111 for f be FinSequence of COMPLEX holds k in dom (f|n) implies k in dom f; registration let n; cluster {}/^n -> empty; end; registration let f,n; cluster (f|n)/^n -> empty; end; registration let D; let f be D-valued FinSequence; let n; cluster (f/^n) -> D-valued; end; registration let f be FinSequence of NAT,n; cluster f.n -> natural; end; registration let f be FinSequence of NAT,n,k; cluster (f|n).k -> natural; cluster ((f|n)/^1).k -> natural; end; theorem :: NEWTON02:112 Sum(f^F) = Sum(f) + Sum(F); theorem :: NEWTON02:113 for f be FinSequence of REAL holds k in dom (f/^n) & n in dom f implies n+k in dom f; theorem :: NEWTON02:114 for k be positive Nat holds n+k in dom f implies k in dom (f/^n); theorem :: NEWTON02:115 for n be positive Nat st n+1 = len f holds Sum f = Sum((f|n)/^1) + f.1 + f.(n+1); theorem :: NEWTON02:116 n+1 = len f implies (f/^n) = <*f.(n+1)*>; theorem :: NEWTON02:117 ((f|n)/^1) is not empty implies len ((f|n)/^1) <= len f - 1; theorem :: NEWTON02:118 ((f|n)/^1) is not empty implies len ((f|n)/^1) < n; :: n choose k theorem :: NEWTON02:119 n is prime & k <> 0 & k <> n implies n divides (n choose k); :: factorial theorem :: NEWTON02:120 b >= 2 implies (b+1)! > 2|^b; theorem :: NEWTON02:121 b > 1 iff b! > 1; theorem :: NEWTON02:122 b >= 2 implies b! < b|^b; theorem :: NEWTON02:123 (b+1)! >= 2|^b; theorem :: NEWTON02:124 b! <= b|^b; theorem :: NEWTON02:125 b>0 & a,b! are_coprime implies a,b are_coprime; theorem :: NEWTON02:126 a,(a+b)! are_coprime implies a = 1 or (a = 0 & (b = 0 or b = 1)); theorem :: NEWTON02:127 for n st n in dom f & m in dom ((f|n)/^1) holds ((f|n)/^1).m = f.(m+1); :: Newton_Coeff registration let n; cluster Newton_Coeff n -> non empty; end; registration let n,m; cluster (Newton_Coeff n).m -> natural; end; registration let n; cluster Newton_Coeff n -> NAT-valued; end; registration let h be FinSequence of NAT; cluster Sum h -> natural; end; theorem :: NEWTON02:128 n > 0 implies n in dom (Newton_Coeff n); theorem :: NEWTON02:129 (Newton_Coeff n) is FinSequence of NAT; theorem :: NEWTON02:130 (Newton_Coeff n).(n+1) = 1; theorem :: NEWTON02:131 (Newton_Coeff k).1 = 1; theorem :: NEWTON02:132 for n be positive Nat holds Sum(Newton_Coeff n) = Sum(((Newton_Coeff n)|n)/^1) + (Newton_Coeff n).1 + (Newton_Coeff n).(n+1); theorem :: NEWTON02:133 for n be positive Nat holds Sum(Newton_Coeff n) = Sum(((Newton_Coeff n)|n)/^1) + 2; theorem :: NEWTON02:134 Sum(Newton_Coeff n) = Sum ((Newton_Coeff n)|n) + 1; theorem :: NEWTON02:135 len((Newton_Coeff n)|n) = n; theorem :: NEWTON02:136 m in dom (((Newton_Coeff n)|n)/^1) implies (((Newton_Coeff n)|n)/^1).m = (Newton_Coeff n).(m+1); theorem :: NEWTON02:137 n is prime implies n divides (((Newton_Coeff n)|n)/^1).k; theorem :: NEWTON02:138 for n be prime Nat holds n divides 2|^n - 2; registration let k be positive Nat; let n; cluster n|^k - n -> natural; end; theorem :: NEWTON02:139 for k,n be prime Nat holds n*k divides (2|^n - 2)*(2|^k -2); theorem :: NEWTON02:140 for n be odd Prime st n = 2*k + 1 holds n divides (2|^k - 1) iff not n divides (2|^k + 1); definition let n be natural number; func n\ -> FinSequence of REAL equals :: NEWTON02:def 1 (1,1) In_Power n; end; registration let n; identify n\ with Newton_Coeff n; identify Newton_Coeff n with n\; end; :: The use of this registration would make most of the above code unnecessary. I leave it as an illustration. :: In_Power theorem :: NEWTON02:141 n > 0 implies n in dom ((a,b) In_Power n); registration let a,b,n,m; cluster ((a,b) In_Power n).m -> natural; end; registration let a,b,n; cluster (a,b) In_Power n -> NAT-valued; end; theorem :: NEWTON02:142 (k+l) is prime & k > 0 & l > 0 implies (k+l) divides ((a,b) In_Power (k+l)).(k+1); theorem :: NEWTON02:143 a<>0 implies ((a,b) In_Power m).1 <> 0; theorem :: NEWTON02:144 for m be non zero Nat holds a = 0 iff ((a,b) In_Power m).1 = 0; theorem :: NEWTON02:145 ((a,b) In_Power m).1=0 implies m<>0; theorem :: NEWTON02:146 for m be positive Nat holds Sum (a,b) In_Power m = a|^m + b|^m + Sum ((((a,b) In_Power m)|m)/^1); theorem :: NEWTON02:147 Sum((a,b) In_Power (m+n)) = Sum((a,b) In_Power m)*Sum((a,b) In_Power n); theorem :: NEWTON02:148 l>0 implies ex x st ((a,b) In_Power (k+l)).(k+1) = a*x; theorem :: NEWTON02:149 m>0 implies ex k st ((a,b) In_Power m).1 = a*k; theorem :: NEWTON02:150 l>0 implies ex x st ((a,b) In_Power (k+l)).l = a*x; theorem :: NEWTON02:151 for n st n = ((a,b) In_Power (k+l)).(k+1) & l>0 holds a divides n; theorem :: NEWTON02:152 for n be prime Nat, a,b be positive Nat holds n*a*b divides (((a,b) In_Power n)|n/^1).k; theorem :: NEWTON02:153 for n be prime Nat, a,b be positive Nat holds n*a*b divides (a+b)|^n - (a|^n + b|^n); theorem :: NEWTON02:154 for n be prime Nat holds n*a divides (a+1)|^n - (a|^n + 1); theorem :: NEWTON02:155 for a,b be positive Nat holds 2*a*b divides (a+b)|^2 - (a|^2 + b|^2); theorem :: NEWTON02:156 for n be prime Nat holds n divides a|^n - a; theorem :: NEWTON02:157 for k be Nat st k+1 is prime & not k+1 divides a holds k+1 divides a|^k - 1; theorem :: NEWTON02:158 for n be prime Nat holds n divides a+b iff n divides a|^n + b|^n; theorem :: NEWTON02:159 163 divides (a+b) iff 163 divides a|^163 + b|^163; theorem :: NEWTON02:160 for n be prime Nat holds n divides a iff n divides a|^n; theorem :: NEWTON02:161 for n be prime Nat holds n divides a|^n + 1 iff n divides a+1; theorem :: NEWTON02:162 for n be prime Nat holds n divides a|^n + b|^n iff n divides (a+b)|^n; theorem :: NEWTON02:163 7 divides a|^7 + 1 iff 7 divides a+1; theorem :: NEWTON02:164 not 7 divides a implies 7 divides a|^6 - 1; theorem :: NEWTON02:165 for n be prime Nat, a,b be positive Nat holds n*a*b divides (a+b)|^(k*n) - (a|^n + b|^n)|^k; theorem :: NEWTON02:166 for n be prime Nat, a,b be positive Nat holds n*a*b divides (a+t)|^n - (a|^n + b|^n) implies n*a*b divides (a+b)|^n - (a+t)|^n; theorem :: NEWTON02:167 for n be prime Nat, a,b,c be positive Nat holds n*a*b divides c-b implies n*a*b divides (a|^n + b|^n) - (a+c)|^n; theorem :: NEWTON02:168 for p be prime Nat st p = 2*n+1 holds p divides a or p divides a|^n-1 or p divides a|^n+1; theorem :: NEWTON02:169 for p be prime Nat st not p divides a holds ex n st p divides a|^n - 1 & 0 < n & n < p; theorem :: NEWTON02:170 5 divides a|^3 - 1 iff 5 divides a - 1; theorem :: NEWTON02:171 for k st k+1 is prime holds k+1 divides a|^(n*k+1) - a; theorem :: NEWTON02:172 2 divides a|^(n+1) - a; theorem :: NEWTON02:173 3 divides a|^(2*n+1) - a; theorem :: NEWTON02:174 5 divides a|^(4*n+1) - a; theorem :: NEWTON02:175 7 divides a|^(6*n+1) - a; theorem :: NEWTON02:176 for k,l st k <> l & k+1 is odd prime & l+1 is odd prime holds 2*(k+1)*(l+1) divides a|^(k*l+1) - a; theorem :: NEWTON02:177 154 divides a|^61 - a; theorem :: NEWTON02:178 6 divides a|^(2*n+1) - a; theorem :: NEWTON02:179 30 divides a|^(4*n+1) - a; theorem :: NEWTON02:180 42 divides a|^(6*n+1) - a; theorem :: NEWTON02:181 for n be prime Nat holds n divides a|^(n+k) - a|^(k+1); theorem :: NEWTON02:182 for n st 2*n+1 is prime for k st 2*n > k & k > 1 holds not 2*n+1 divides a|^n - k & not 2*n+1 divides a|^n + k; theorem :: NEWTON02:183 not 5 divides a|^2 - 2 & not 5 divides a|^2 + 2 & not 5 divides a|^2 - 3 & not 5 divides a|^2 + 3; :: Pythagorean triples theorem :: NEWTON02:184 a|^2 + b|^2 = c|^2 implies 5 divides a or 5 divides b or 5 divides c; theorem :: NEWTON02:185 not 7 divides a|^3 - 2 & not 7 divides a|^3 + 2 & not 7 divides a|^3 - 3 & not 7 divides a|^3 + 3 & not 7 divides a|^3 - 4 & not 7 divides a|^3 + 4 & not 7 divides a|^3 - 5 & not 7 divides a|^3 + 5; theorem :: NEWTON02:186 2 divides 2|^n - 1 iff n = 0; theorem :: NEWTON02:187 2|^(k+l) divides 2|^(n+k) - 2|^k implies l = 0 or n = 0; theorem :: NEWTON02:188 3 divides b or 3 divides b-1 or 3 divides b+1; theorem :: NEWTON02:189 not 3 divides b implies not 3 divides b|^2 + c|^2; theorem :: NEWTON02:190 not 3 divides b|^2 + 1 & not 3 divides b|^2 - 2; theorem :: NEWTON02:191 not 3 divides b|^3 + b|^2 - b + 1; theorem :: NEWTON02:192 for a be positive Nat holds b,c are_coprime & a+1 divides b implies not a+1 divides c; theorem :: NEWTON02:193 b,c are_coprime implies not 3 divides b|^2 + c|^2; theorem :: NEWTON02:194 for p be prime Nat holds p divides a implies p divides a|^(n+1); theorem :: NEWTON02:195 b,c are_coprime & b|^2 + c|^2 = a|^2 implies not 3 divides a; theorem :: NEWTON02:196 for p be prime Nat holds p divides a + b implies p divides a|^(2*n+1) + b|^(2*n+1); theorem :: NEWTON02:197 for p be prime Nat holds not p divides a|^(2*n+1) + b|^(2*n+1) & p divides a|^2 - b|^2 implies p divides a - b; theorem :: NEWTON02:198 3 divides a*b or 3 divides a+b or 3 divides a-b; theorem :: NEWTON02:199 not 3 divides a & not 3 divides b implies 3 divides a|^(2*n+1) + b|^(2*n+1) or 3 divides a|^(2*n+1) - b|^(2*n+1); theorem :: NEWTON02:200 a|^3 + b|^3 = c|^3 implies 7 divides a or 7 divides b or 7 divides c;