:: 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 b₁ being Element of K37(omega) holds
( b₁ = EvenNAT iff b₁ = { 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 b₁ being Element of K37(omega) holds
( b₁ = OddNAT iff b₁ = { 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;

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

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

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