:: by Adam Naumowicz and Rados{\l}aw Piliszek

::

:: Received May 19, 2013

:: Copyright (c) 2013-2018 Association of Mizar Users

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))

dom ((Sgm0 X) ^ (Sgm0 Y)) = dom (Sgm0 (X \/ Y))

proof end;

definition

compatibility

for b_{1} being Element of K37(omega) holds

( b_{1} = EvenNAT iff b_{1} = { n where n is Nat : n is even } )

end;
for b

( b

proof end;

definition

compatibility

for b_{1} being Element of K37(omega) holds

( b_{1} = OddNAT iff b_{1} = { n where n is Nat : n is odd } )

end;
for b

( b

proof end;

registration

let F be Sequence;

let P be Permutation of (dom F);

correctness

coherence

F * P is Sequence-like ;

end;
let P be Permutation of (dom F);

correctness

coherence

F * P is Sequence-like ;

proof 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))

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)))

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

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

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)

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)

n = (b * (value ((mid ((digits (n,b)),2,(len (digits (n,b))))),b))) + ((digits (n,b)) . 0)

proof end;

Lm1: for n being Element of NAT st 1 < n & n < 5 & n is prime & not n = 2 holds

n = 3

proof end;

Lm2: ( not 6 is prime & not 8 is prime & not 9 is prime & not 10 is prime & not 12 is prime & not 14 is prime & not 15 is prime & not 16 is prime & not 18 is prime & not 20 is prime & not 21 is prime & not 22 is prime & not 24 is prime & not 25 is prime & not 26 is prime & not 27 is prime & not 28 is prime )

proof end;

Lm3: for n being Element of NAT st 1 < n & n < 29 & n is prime & not n = 2 & not n = 3 & not n = 5 & not n = 7 & not n = 11 & not n = 13 & not n = 17 & not n = 19 holds

n = 23

proof end;

Lm4: for k being Element of NAT st k < 841 holds

for n being Element of NAT st 1 < n & n * n <= k & n is prime & not n = 2 & not n = 3 & not n = 5 & not n = 7 & not n = 11 & not n = 13 & not n = 17 & not n = 19 holds

n = 23

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)) )

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)) )

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)) )

( 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)) )

( 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) )

( 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) )

( 11 divides n iff 11 divides (value (((digits (n,10)) /^ 1),10)) - ((digits (n,10)) . 0) )

proof end;

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))) )

( 11 divides n iff 11 divides (Sum (SubXFinS ((digits (n,10)),EvenNAT))) - (Sum (SubXFinS ((digits (n,10)),OddNAT))) )

proof end;

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)) )

( 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)) )

( 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)) )

( 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)) )

( 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)) )

( 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)) )

( 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)) )

( 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)) )

( 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)) )

( 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)) )

( 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)) )

( 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)) )

( 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)) )

( 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)) )

( 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)) )

( 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)) )

( 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)) )

( 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)) )

( 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)) )

( 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)) )

( 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)) )

( 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)) )

( 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)) )

( 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)) )

( 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)) )

( 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)) )

( 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)) )

( 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)) )

( 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)) )

( 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)) )

( 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)) )

( 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)) )

( 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)) )

( 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)) )

( 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)) )

( 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)) )

( 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)) )

( 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)) )

( 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)) )

( 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)) )

( 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)) )

( 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)) )

( 101 divides n iff 101 divides (value (((digits (n,10)) /^ 1),10)) - (10 * ((digits (n,10)) . 0)) )

proof end;