:: More on Divisibility Criteria for Selected Primes
:: by Adam Naumowicz and Rados{\l}aw Piliszek
::
:: Received May 19, 2013
:: Copyright (c) 2013-2021 Association of Mizar Users


theorem Th1: :: NUMERAL2:1
for f being non empty XFinSequence holds f | 1 = <%(f . 0)%>
proof end;

theorem Th2: :: NUMERAL2:2
for f being non empty XFinSequence holds f = <%(f . 0)%> ^ (f /^ 1)
proof end;

theorem Th3: :: NUMERAL2:3
for f being XFinSequence holds mid (f,2,(len f)) = f /^ 1
proof end;

theorem Th4: :: NUMERAL2:4
for X, Y being finite natural-membered set st X misses Y holds
dom ((Sgm0 X) ^ (Sgm0 Y)) = dom (Sgm0 (X \/ Y))
proof end;

theorem Th5: :: NUMERAL2:5
for X, Y being finite natural-membered set holds rng ((Sgm0 X) ^ (Sgm0 Y)) = rng (Sgm0 (X \/ Y))
proof end;

theorem Th6: :: NUMERAL2:6
for F being XFinSequence
for X being set holds dom (SubXFinS (F,X)) = dom (Sgm0 (X /\ (dom F)))
proof end;

definition
redefine func EvenNAT equals :: NUMERAL2:def 1
{ n where n is Nat : n is even } ;
compatibility
for b1 being Element of K37(omega) holds
( b1 = EvenNAT iff b1 = { n where n is Nat : n is even } )
proof end;
end;

:: deftheorem defines EvenNAT NUMERAL2:def 1 :
EvenNAT = { n where n is Nat : n is even } ;

definition
redefine func OddNAT equals :: NUMERAL2:def 2
{ n where n is Nat : n is odd } ;
compatibility
for b1 being Element of K37(omega) holds
( b1 = OddNAT iff b1 = { n where n is Nat : n is odd } )
proof end;
end;

:: deftheorem defines OddNAT NUMERAL2:def 2 :
OddNAT = { n where n is Nat : n is odd } ;

theorem Th7: :: NUMERAL2:7
EvenNAT misses OddNAT
proof end;

theorem Th8: :: NUMERAL2:8
EvenNAT \/ OddNAT = NAT
proof end;

registration
let F be Sequence;
let P be Permutation of (dom F);
cluster P (#) F -> Sequence-like ;
correctness
coherence
F * P is Sequence-like
;
proof end;
end;

theorem Th9: :: NUMERAL2:9
for F being XFinSequence
for X, Y being set st X misses Y holds
ex P being Permutation of (dom (SubXFinS (F,(X \/ Y)))) st (SubXFinS (F,(X \/ Y))) * P = (SubXFinS (F,X)) ^ (SubXFinS (F,Y))
proof end;

theorem Th10: :: NUMERAL2:10
for cF being complex-valued XFinSequence
for B1, B2 being set st B1 misses B2 holds
Sum (SubXFinS (cF,(B1 \/ B2))) = (Sum (SubXFinS (cF,B1))) + (Sum (SubXFinS (cF,B2)))
proof end;

theorem Th11: :: NUMERAL2:11
for F being XFinSequence holds F = SubXFinS (F,NAT)
proof end;

theorem Th12: :: NUMERAL2:12
for N, i being Nat st i in dom (Sgm0 (N /\ EvenNAT)) holds
(Sgm0 (N /\ EvenNAT)) . i = 2 * i
proof end;

theorem Th13: :: NUMERAL2:13
for N, i being Nat st i in dom (Sgm0 (N /\ OddNAT)) holds
(Sgm0 (N /\ OddNAT)) . i = (2 * i) + 1
proof end;

theorem Th14: :: NUMERAL2:14
for i, j being Integer holds (i mod j) mod j = i mod j
proof end;

theorem :: NUMERAL2:15
for i, j, k, l being Integer st i mod l = j mod l holds
(k + i) mod l = (k + j) mod l
proof end;

theorem Th16: :: NUMERAL2:16
for d being XFinSequence of INT
for n being Integer st ( for i being Nat st i in dom d holds
n divides d . i ) holds
n divides Sum d
proof end;

theorem :: NUMERAL2:17
for d, e being XFinSequence of INT
for n being Integer st dom d = dom e & ( for i being Nat st i in dom d holds
e . i = (d . i) mod n ) holds
(Sum d) mod n = (Sum e) mod n
proof end;

theorem Th18: :: NUMERAL2:18
for f, g being XFinSequence of NAT
for i being Integer st dom f = dom g & ( for n being object st n in dom f holds
f . n = i * (g . n) ) holds
Sum f = i * (Sum g)
proof end;

theorem Th19: :: NUMERAL2:19
for n, b being Nat st b > 1 holds
n = (b * (value ((mid ((digits (n,b)),2,(len (digits (n,b))))),b))) + ((digits (n,b)) . 0)
proof end;

theorem Th20: :: NUMERAL2:20
for n, k being Nat st k = (10 |^ (2 * n)) - 1 holds
11 divides k
proof end;

theorem Th21: :: NUMERAL2:21
for n, k being Nat st k = (10 |^ ((2 * n) + 1)) + 1 holds
11 divides k
proof end;

theorem Th22: :: NUMERAL2:22
7,10 are_coprime
proof end;

theorem Th23: :: NUMERAL2:23
29 is prime
proof end;

theorem Th24: :: NUMERAL2:24
31 is prime
proof end;

theorem Th25: :: NUMERAL2:25
41 is prime
proof end;

theorem Th26: :: NUMERAL2:26
47 is prime
proof end;

theorem Th27: :: NUMERAL2:27
53 is prime
proof end;

theorem Th28: :: NUMERAL2:28
59 is prime
proof end;

theorem Th29: :: NUMERAL2:29
61 is prime
proof end;

theorem Th30: :: NUMERAL2:30
67 is prime
proof end;

theorem Th31: :: NUMERAL2:31
71 is prime
proof end;

theorem Th32: :: NUMERAL2:32
73 is prime
proof end;

theorem Th33: :: NUMERAL2:33
79 is prime
proof end;

theorem Th34: :: NUMERAL2:34
89 is prime
proof end;

theorem Th35: :: NUMERAL2:35
97 is prime
proof end;

theorem Th36: :: NUMERAL2:36
101 is prime
proof end;

theorem Th37: :: NUMERAL2:37
for p being prime Nat
for n, f, b being Nat st ex k being Nat st (b * f) + 1 = p * k & b > 1 & p,b are_coprime holds
( p divides n iff p divides (value ((mid ((digits (n,b)),2,(len (digits (n,b))))),b)) - (f * ((digits (n,b)) . 0)) )
proof end;

theorem Th38: :: NUMERAL2:38
for p being prime Nat
for n, f, b being Nat st ex k being Nat st (b * f) - 1 = p * k & b > 1 & p,b are_coprime holds
( p divides n iff p divides (value ((mid ((digits (n,b)),2,(len (digits (n,b))))),b)) + (f * ((digits (n,b)) . 0)) )
proof end;

:: WP: Divisibility rule#Divisibility by 7
theorem Th39: :: NUMERAL2:39
for n being Nat holds
( 7 divides n iff 7 divides (value ((mid ((digits (n,10)),2,(len (digits (n,10))))),10)) - (2 * ((digits (n,10)) . 0)) )
proof end;

theorem :: NUMERAL2:40
for n being Nat holds
( 7 divides n iff 7 divides (value (((digits (n,10)) /^ 1),10)) - (2 * ((digits (n,10)) . 0)) )
proof end;

theorem Th41: :: NUMERAL2:41
for n being Nat holds
( 11 divides n iff 11 divides (value ((mid ((digits (n,10)),2,(len (digits (n,10))))),10)) - ((digits (n,10)) . 0) )
proof end;

theorem :: NUMERAL2:42
for n being Nat holds
( 11 divides n iff 11 divides (value (((digits (n,10)) /^ 1),10)) - ((digits (n,10)) . 0) )
proof end;

:: WP: Divisibility rule#Divisibility by 11
theorem :: NUMERAL2:43
for n being Nat holds
( 11 divides n iff 11 divides (Sum (SubXFinS ((digits (n,10)),EvenNAT))) - (Sum (SubXFinS ((digits (n,10)),OddNAT))) )
proof end;

:: WP: Divisibility rule#Divisibility by 13
theorem Th44: :: NUMERAL2:44
for n being Nat holds
( 13 divides n iff 13 divides (value ((mid ((digits (n,10)),2,(len (digits (n,10))))),10)) + (4 * ((digits (n,10)) . 0)) )
proof end;

theorem :: NUMERAL2:45
for n being Nat holds
( 13 divides n iff 13 divides (value (((digits (n,10)) /^ 1),10)) + (4 * ((digits (n,10)) . 0)) )
proof end;

theorem Th46: :: NUMERAL2:46
for n being Nat holds
( 17 divides n iff 17 divides (value ((mid ((digits (n,10)),2,(len (digits (n,10))))),10)) - (5 * ((digits (n,10)) . 0)) )
proof end;

theorem :: NUMERAL2:47
for n being Nat holds
( 17 divides n iff 17 divides (value (((digits (n,10)) /^ 1),10)) - (5 * ((digits (n,10)) . 0)) )
proof end;

theorem Th48: :: NUMERAL2:48
for n being Nat holds
( 19 divides n iff 19 divides (value ((mid ((digits (n,10)),2,(len (digits (n,10))))),10)) + (2 * ((digits (n,10)) . 0)) )
proof end;

theorem :: NUMERAL2:49
for n being Nat holds
( 19 divides n iff 19 divides (value (((digits (n,10)) /^ 1),10)) + (2 * ((digits (n,10)) . 0)) )
proof end;

theorem Th50: :: NUMERAL2:50
for n being Nat holds
( 23 divides n iff 23 divides (value ((mid ((digits (n,10)),2,(len (digits (n,10))))),10)) + (7 * ((digits (n,10)) . 0)) )
proof end;

theorem :: NUMERAL2:51
for n being Nat holds
( 23 divides n iff 23 divides (value (((digits (n,10)) /^ 1),10)) + (7 * ((digits (n,10)) . 0)) )
proof end;

theorem Th52: :: NUMERAL2:52
for n being Nat holds
( 29 divides n iff 29 divides (value ((mid ((digits (n,10)),2,(len (digits (n,10))))),10)) + (3 * ((digits (n,10)) . 0)) )
proof end;

theorem :: NUMERAL2:53
for n being Nat holds
( 29 divides n iff 29 divides (value (((digits (n,10)) /^ 1),10)) + (3 * ((digits (n,10)) . 0)) )
proof end;

theorem Th54: :: NUMERAL2:54
for n being Nat holds
( 31 divides n iff 31 divides (value ((mid ((digits (n,10)),2,(len (digits (n,10))))),10)) - (3 * ((digits (n,10)) . 0)) )
proof end;

theorem :: NUMERAL2:55
for n being Nat holds
( 31 divides n iff 31 divides (value (((digits (n,10)) /^ 1),10)) - (3 * ((digits (n,10)) . 0)) )
proof end;

theorem Th56: :: NUMERAL2:56
for n being Nat holds
( 37 divides n iff 37 divides (value ((mid ((digits (n,10)),2,(len (digits (n,10))))),10)) - (11 * ((digits (n,10)) . 0)) )
proof end;

theorem :: NUMERAL2:57
for n being Nat holds
( 37 divides n iff 37 divides (value (((digits (n,10)) /^ 1),10)) - (11 * ((digits (n,10)) . 0)) )
proof end;

theorem Th58: :: NUMERAL2:58
for n being Nat holds
( 41 divides n iff 41 divides (value ((mid ((digits (n,10)),2,(len (digits (n,10))))),10)) - (4 * ((digits (n,10)) . 0)) )
proof end;

theorem :: NUMERAL2:59
for n being Nat holds
( 41 divides n iff 41 divides (value (((digits (n,10)) /^ 1),10)) - (4 * ((digits (n,10)) . 0)) )
proof end;

theorem Th60: :: NUMERAL2:60
for n being Nat holds
( 43 divides n iff 43 divides (value ((mid ((digits (n,10)),2,(len (digits (n,10))))),10)) + (13 * ((digits (n,10)) . 0)) )
proof end;

theorem :: NUMERAL2:61
for n being Nat holds
( 43 divides n iff 43 divides (value (((digits (n,10)) /^ 1),10)) + (13 * ((digits (n,10)) . 0)) )
proof end;

theorem Th62: :: NUMERAL2:62
for n being Nat holds
( 47 divides n iff 47 divides (value ((mid ((digits (n,10)),2,(len (digits (n,10))))),10)) - (14 * ((digits (n,10)) . 0)) )
proof end;

theorem :: NUMERAL2:63
for n being Nat holds
( 47 divides n iff 47 divides (value (((digits (n,10)) /^ 1),10)) - (14 * ((digits (n,10)) . 0)) )
proof end;

theorem Th64: :: NUMERAL2:64
for n being Nat holds
( 53 divides n iff 53 divides (value ((mid ((digits (n,10)),2,(len (digits (n,10))))),10)) + (16 * ((digits (n,10)) . 0)) )
proof end;

theorem :: NUMERAL2:65
for n being Nat holds
( 53 divides n iff 53 divides (value (((digits (n,10)) /^ 1),10)) + (16 * ((digits (n,10)) . 0)) )
proof end;

theorem Th66: :: NUMERAL2:66
for n being Nat holds
( 59 divides n iff 59 divides (value ((mid ((digits (n,10)),2,(len (digits (n,10))))),10)) + (6 * ((digits (n,10)) . 0)) )
proof end;

theorem :: NUMERAL2:67
for n being Nat holds
( 59 divides n iff 59 divides (value (((digits (n,10)) /^ 1),10)) + (6 * ((digits (n,10)) . 0)) )
proof end;

theorem Th68: :: NUMERAL2:68
for n being Nat holds
( 61 divides n iff 61 divides (value ((mid ((digits (n,10)),2,(len (digits (n,10))))),10)) - (6 * ((digits (n,10)) . 0)) )
proof end;

theorem :: NUMERAL2:69
for n being Nat holds
( 61 divides n iff 61 divides (value (((digits (n,10)) /^ 1),10)) - (6 * ((digits (n,10)) . 0)) )
proof end;

theorem Th70: :: NUMERAL2:70
for n being Nat holds
( 67 divides n iff 67 divides (value ((mid ((digits (n,10)),2,(len (digits (n,10))))),10)) - (20 * ((digits (n,10)) . 0)) )
proof end;

theorem :: NUMERAL2:71
for n being Nat holds
( 67 divides n iff 67 divides (value (((digits (n,10)) /^ 1),10)) - (20 * ((digits (n,10)) . 0)) )
proof end;

theorem Th72: :: NUMERAL2:72
for n being Nat holds
( 71 divides n iff 71 divides (value ((mid ((digits (n,10)),2,(len (digits (n,10))))),10)) - (7 * ((digits (n,10)) . 0)) )
proof end;

theorem :: NUMERAL2:73
for n being Nat holds
( 71 divides n iff 71 divides (value (((digits (n,10)) /^ 1),10)) - (7 * ((digits (n,10)) . 0)) )
proof end;

theorem Th74: :: NUMERAL2:74
for n being Nat holds
( 73 divides n iff 73 divides (value ((mid ((digits (n,10)),2,(len (digits (n,10))))),10)) + (22 * ((digits (n,10)) . 0)) )
proof end;

theorem :: NUMERAL2:75
for n being Nat holds
( 73 divides n iff 73 divides (value (((digits (n,10)) /^ 1),10)) + (22 * ((digits (n,10)) . 0)) )
proof end;

theorem Th76: :: NUMERAL2:76
for n being Nat holds
( 79 divides n iff 79 divides (value ((mid ((digits (n,10)),2,(len (digits (n,10))))),10)) + (8 * ((digits (n,10)) . 0)) )
proof end;

theorem :: NUMERAL2:77
for n being Nat holds
( 79 divides n iff 79 divides (value (((digits (n,10)) /^ 1),10)) + (8 * ((digits (n,10)) . 0)) )
proof end;

theorem Th78: :: NUMERAL2:78
for n being Nat holds
( 83 divides n iff 83 divides (value ((mid ((digits (n,10)),2,(len (digits (n,10))))),10)) + (25 * ((digits (n,10)) . 0)) )
proof end;

theorem :: NUMERAL2:79
for n being Nat holds
( 83 divides n iff 83 divides (value (((digits (n,10)) /^ 1),10)) + (25 * ((digits (n,10)) . 0)) )
proof end;

theorem Th80: :: NUMERAL2:80
for n being Nat holds
( 89 divides n iff 89 divides (value ((mid ((digits (n,10)),2,(len (digits (n,10))))),10)) + (9 * ((digits (n,10)) . 0)) )
proof end;

theorem :: NUMERAL2:81
for n being Nat holds
( 89 divides n iff 89 divides (value (((digits (n,10)) /^ 1),10)) + (9 * ((digits (n,10)) . 0)) )
proof end;

theorem Th82: :: NUMERAL2:82
for n being Nat holds
( 97 divides n iff 97 divides (value ((mid ((digits (n,10)),2,(len (digits (n,10))))),10)) - (29 * ((digits (n,10)) . 0)) )
proof end;

theorem :: NUMERAL2:83
for n being Nat holds
( 97 divides n iff 97 divides (value (((digits (n,10)) /^ 1),10)) - (29 * ((digits (n,10)) . 0)) )
proof end;

theorem Th84: :: NUMERAL2:84
for n being Nat holds
( 101 divides n iff 101 divides (value ((mid ((digits (n,10)),2,(len (digits (n,10))))),10)) - (10 * ((digits (n,10)) . 0)) )
proof end;

theorem :: NUMERAL2:85
for n being Nat holds
( 101 divides n iff 101 divides (value (((digits (n,10)) /^ 1),10)) - (10 * ((digits (n,10)) . 0)) )
proof end;