Proof of Theorem 1259prm
Step | Hyp | Ref
| Expression |
1 | | 37prm 15666 |
. 2
⊢ ;37 ∈ ℙ |
2 | | 3nn0 11187 |
. . 3
⊢ 3 ∈
ℕ0 |
3 | | 4nn 11064 |
. . 3
⊢ 4 ∈
ℕ |
4 | 2, 3 | decnncl 11394 |
. 2
⊢ ;34 ∈ ℕ |
5 | | 1259prm.1 |
. . . . . 6
⊢ 𝑁 = ;;;1259 |
6 | | 1nn0 11185 |
. . . . . . . . 9
⊢ 1 ∈
ℕ0 |
7 | | 2nn0 11186 |
. . . . . . . . 9
⊢ 2 ∈
ℕ0 |
8 | 6, 7 | deccl 11388 |
. . . . . . . 8
⊢ ;12 ∈
ℕ0 |
9 | | 5nn0 11189 |
. . . . . . . 8
⊢ 5 ∈
ℕ0 |
10 | 8, 9 | deccl 11388 |
. . . . . . 7
⊢ ;;125 ∈ ℕ0 |
11 | | 8nn0 11192 |
. . . . . . 7
⊢ 8 ∈
ℕ0 |
12 | | eqid 2610 |
. . . . . . 7
⊢ ;;;1258 =
;;;1258 |
13 | | 8p1e9 11035 |
. . . . . . 7
⊢ (8 + 1) =
9 |
14 | 10, 11, 6, 12, 13 | decaddi 11455 |
. . . . . 6
⊢ (;;;1258 +
1) = ;;;1259 |
15 | 5, 14 | eqtr4i 2635 |
. . . . 5
⊢ 𝑁 = (;;;1258 + 1) |
16 | 15 | oveq1i 6559 |
. . . 4
⊢ (𝑁 − 1) = ((;;;1258 +
1) − 1) |
17 | 10, 11 | deccl 11388 |
. . . . . 6
⊢ ;;;1258
∈ ℕ0 |
18 | 17 | nn0cni 11181 |
. . . . 5
⊢ ;;;1258
∈ ℂ |
19 | | ax-1cn 9873 |
. . . . 5
⊢ 1 ∈
ℂ |
20 | 18, 19 | pncan3oi 10176 |
. . . 4
⊢ ((;;;1258 +
1) − 1) = ;;;1258 |
21 | 16, 20 | eqtri 2632 |
. . 3
⊢ (𝑁 − 1) = ;;;1258 |
22 | | 4nn0 11188 |
. . . . 5
⊢ 4 ∈
ℕ0 |
23 | 2, 22 | deccl 11388 |
. . . 4
⊢ ;34 ∈
ℕ0 |
24 | | 7nn0 11191 |
. . . 4
⊢ 7 ∈
ℕ0 |
25 | | eqid 2610 |
. . . 4
⊢ ;37 = ;37 |
26 | 7, 2 | deccl 11388 |
. . . 4
⊢ ;23 ∈
ℕ0 |
27 | | eqid 2610 |
. . . . 5
⊢ ;34 = ;34 |
28 | | eqid 2610 |
. . . . 5
⊢ ;23 = ;23 |
29 | | 3t3e9 11057 |
. . . . . . 7
⊢ (3
· 3) = 9 |
30 | | 2p1e3 11028 |
. . . . . . 7
⊢ (2 + 1) =
3 |
31 | 29, 30 | oveq12i 6561 |
. . . . . 6
⊢ ((3
· 3) + (2 + 1)) = (9 + 3) |
32 | | 9p3e12 11497 |
. . . . . 6
⊢ (9 + 3) =
;12 |
33 | 31, 32 | eqtri 2632 |
. . . . 5
⊢ ((3
· 3) + (2 + 1)) = ;12 |
34 | | 4t3e12 11508 |
. . . . . 6
⊢ (4
· 3) = ;12 |
35 | | 3cn 10972 |
. . . . . . 7
⊢ 3 ∈
ℂ |
36 | | 2cn 10968 |
. . . . . . 7
⊢ 2 ∈
ℂ |
37 | | 3p2e5 11037 |
. . . . . . 7
⊢ (3 + 2) =
5 |
38 | 35, 36, 37 | addcomli 10107 |
. . . . . 6
⊢ (2 + 3) =
5 |
39 | 6, 7, 2, 34, 38 | decaddi 11455 |
. . . . 5
⊢ ((4
· 3) + 3) = ;15 |
40 | 2, 22, 7, 2, 27, 28, 2, 9, 6,
33, 39 | decmac 11442 |
. . . 4
⊢ ((;34 · 3) + ;23) = ;;125 |
41 | | 7cn 10981 |
. . . . . . 7
⊢ 7 ∈
ℂ |
42 | | 7t3e21 11525 |
. . . . . . 7
⊢ (7
· 3) = ;21 |
43 | 41, 35, 42 | mulcomli 9926 |
. . . . . 6
⊢ (3
· 7) = ;21 |
44 | | 1p2e3 11029 |
. . . . . 6
⊢ (1 + 2) =
3 |
45 | 7, 6, 7, 43, 44 | decaddi 11455 |
. . . . 5
⊢ ((3
· 7) + 2) = ;23 |
46 | | 4cn 10975 |
. . . . . 6
⊢ 4 ∈
ℂ |
47 | | 7t4e28 11526 |
. . . . . 6
⊢ (7
· 4) = ;28 |
48 | 41, 46, 47 | mulcomli 9926 |
. . . . 5
⊢ (4
· 7) = ;28 |
49 | 24, 2, 22, 27, 11, 7, 45, 48 | decmul1c 11463 |
. . . 4
⊢ (;34 · 7) = ;;238 |
50 | 23, 2, 24, 25, 11, 26, 40, 49 | decmul2c 11465 |
. . 3
⊢ (;34 · ;37) = ;;;1258 |
51 | 21, 50 | eqtr4i 2635 |
. 2
⊢ (𝑁 − 1) = (;34 · ;37) |
52 | | 9nn0 11193 |
. . . . . . 7
⊢ 9 ∈
ℕ0 |
53 | 10, 52 | deccl 11388 |
. . . . . 6
⊢ ;;;1259
∈ ℕ0 |
54 | 5, 53 | eqeltri 2684 |
. . . . 5
⊢ 𝑁 ∈
ℕ0 |
55 | 54 | nn0cni 11181 |
. . . 4
⊢ 𝑁 ∈ ℂ |
56 | | npcan 10169 |
. . . 4
⊢ ((𝑁 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑁 −
1) + 1) = 𝑁) |
57 | 55, 19, 56 | mp2an 704 |
. . 3
⊢ ((𝑁 − 1) + 1) = 𝑁 |
58 | 57 | eqcomi 2619 |
. 2
⊢ 𝑁 = ((𝑁 − 1) + 1) |
59 | | 1nn 10908 |
. 2
⊢ 1 ∈
ℕ |
60 | | 2nn 11062 |
. 2
⊢ 2 ∈
ℕ |
61 | 2, 24 | deccl 11388 |
. . . . 5
⊢ ;37 ∈
ℕ0 |
62 | 61 | numexp1 15619 |
. . . 4
⊢ (;37↑1) = ;37 |
63 | 62 | oveq2i 6560 |
. . 3
⊢ (;34 · (;37↑1)) = (;34 · ;37) |
64 | 51, 63 | eqtr4i 2635 |
. 2
⊢ (𝑁 − 1) = (;34 · (;37↑1)) |
65 | | 7nn 11067 |
. . . 4
⊢ 7 ∈
ℕ |
66 | | 4lt7 11088 |
. . . 4
⊢ 4 <
7 |
67 | 2, 22, 65, 66 | declt 11406 |
. . 3
⊢ ;34 < ;37 |
68 | 67, 62 | breqtrri 4610 |
. 2
⊢ ;34 < (;37↑1) |
69 | 5 | 1259lem4 15679 |
. 2
⊢
((2↑(𝑁 −
1)) mod 𝑁) = (1 mod 𝑁) |
70 | 5 | 1259lem5 15680 |
. 2
⊢
(((2↑;34) − 1)
gcd 𝑁) = 1 |
71 | 1, 4, 51, 58, 4, 59, 60, 64, 68, 69, 70 | pockthi 15449 |
1
⊢ 𝑁 ∈ ℙ |