begin
Lm1:
for n, x, y being Nat st n > 1 & x >= 1 & 1 = (((x * y) * n) + x) + y holds
( x = 1 & y = 0 )
Lm2:
for n being Nat holds 2 |^ (2 |^ n) > 1
Lm3:
for n being Nat st n <> 0 holds
n - 1 >= 0
Lm4:
for n being Nat st n <> 0 holds
(n -' 1) + 1 = (n + 1) -' 1
Lm5:
for k, n being Nat holds (k * (2 |^ (n + 1))) div 2 = k * (2 |^ n)
Lm6:
for k, n, m being Nat st k <= n holds
m |^ k divides m |^ n
Lm7:
2 |^ 8 = 256
theorem Th25:
for
m,
n being
Nat st
m > 1 &
n > 0 holds
m |^ n > 1
Lm8:
for n being Nat holds (2 |^ (2 |^ n)) ^2 = 2 |^ (2 |^ (n + 1))
theorem Th30:
for
k,
n,
m being
Nat st
k > 1 &
k |^ n = k |^ m holds
n = m
Lm9:
for k, n, x being Nat st k > n & x > 1 holds
x |^ k > x |^ n
Lm10:
for m, n being Nat st 2 |^ m divides 2 |^ n holds
m <= n
Lm11:
for n, m being Nat st n > 1 & m > 1 & m,1 are_congruent_mod n holds
m mod n = 1
theorem
for
n being
Nat st
n <> 0 holds
- n < n ;
begin
begin
begin
Lm12:
for n being Nat holds Fermat n > 1
Lm13:
for n being Nat holds ((Fermat n) -' 1) mod 2 = 0
Lm14:
for n being Nat holds (Fermat n) -' 1 > 0
Lm15:
for n being Nat holds (Fermat n) mod (2 |^ (2 |^ n)) = 1
Lm16:
for n being Nat holds Fermat n is odd
begin
Lm17:
3 |^ 2 = 9
Lm18:
3 |^ 4 = 81
Lm19:
3 |^ 8 = 6561
Lm20:
3 |^ 16 = 6561 * 6561
Lm21:
for i being Nat holds Fermat 1 divides (3 |^ ((4 * i) + 2)) + 1
Lm22:
for n being Nat st n = 1 holds
3 |^ (((Fermat n) -' 1) div 2), - 1 are_congruent_mod Fermat n
Lm23:
for n being Nat holds Fermat 2 divides (3 |^ ((16 * n) + 8)) + 1
Lm24:
(3 |^ 1) mod (Fermat 3) = 3
Lm25:
(3 |^ 2) mod (Fermat 3) = 9
Lm26:
(3 |^ 4) mod (Fermat 3) = 81
Lm27:
(3 |^ 8) mod (Fermat 3) = 136
Lm28:
(3 |^ 16) mod (Fermat 3) = 83 * 3
Lm29:
(3 |^ 32) mod (Fermat 3) = 64
Lm30:
(3 |^ 64) mod (Fermat 3) = 241
Lm31:
(3 |^ 128) mod (Fermat 3) = 256
Lm32:
(3 |^ 1) mod (Fermat 4) = 3
Lm33:
(3 |^ 2) mod (Fermat 4) = 9
Lm34:
(3 |^ 4) mod (Fermat 4) = 81
Lm35:
(3 |^ 8) mod (Fermat 4) = 6561
Lm36:
(3 |^ 16) mod (Fermat 4) = (164 * 332) + 1
Lm37:
(3 |^ 32) mod (Fermat 4) = 123 * 503
Lm38:
(3 |^ 64) mod (Fermat 4) = (14 * 1367) + 1
Lm39:
(3 |^ 128) mod (Fermat 4) = 52 * 289
Lm40:
(3 |^ 256) mod (Fermat 4) = 282
Lm41:
(3 |^ (256 * 2)) mod (Fermat 4) = 71 * 197
Lm42:
(3 |^ (256 * 4)) mod (Fermat 4) = 32 * 257
Lm43:
(3 |^ (256 * 8)) mod (Fermat 4) = 81 * 809
Lm44:
(3 |^ (256 * 16)) mod (Fermat 4) = 64
Lm45:
(3 |^ (256 * 32)) mod (Fermat 4) = 256 * 16
Lm46:
(3 |^ (256 * 64)) mod (Fermat 4) = 673 * 97
Lm47:
(3 |^ (256 * 128)) mod (Fermat 4) = 256 * 256
Lm48:
Fermat 3 divides (3 |^ ((32 * 0) + 128)) + 1
Lm49:
Fermat 4 divides (3 |^ ((64 * 0) + (256 * 128))) + 1