Proof of Theorem 2503prm
Step | Hyp | Ref
| Expression |
1 | | 139prm 16753 |
. 2
⊢ ;;139 ∈ ℙ |
2 | | 1nn0 12179 |
. . 3
⊢ 1 ∈
ℕ0 |
3 | | 8nn 11998 |
. . 3
⊢ 8 ∈
ℕ |
4 | 2, 3 | decnncl 12386 |
. 2
⊢ ;18 ∈ ℕ |
5 | | 2503prm.1 |
. . . . 5
⊢ 𝑁 = ;;;2503 |
6 | | 2nn0 12180 |
. . . . . . . 8
⊢ 2 ∈
ℕ0 |
7 | | 5nn0 12183 |
. . . . . . . 8
⊢ 5 ∈
ℕ0 |
8 | 6, 7 | deccl 12381 |
. . . . . . 7
⊢ ;25 ∈
ℕ0 |
9 | | 0nn0 12178 |
. . . . . . 7
⊢ 0 ∈
ℕ0 |
10 | 8, 9 | deccl 12381 |
. . . . . 6
⊢ ;;250 ∈ ℕ0 |
11 | | 2p1e3 12045 |
. . . . . 6
⊢ (2 + 1) =
3 |
12 | | eqid 2738 |
. . . . . 6
⊢ ;;;2502 =
;;;2502 |
13 | 10, 6, 11, 12 | decsuc 12397 |
. . . . 5
⊢ (;;;2502 +
1) = ;;;2503 |
14 | 5, 13 | eqtr4i 2769 |
. . . 4
⊢ 𝑁 = (;;;2502 + 1) |
15 | 14 | oveq1i 7265 |
. . 3
⊢ (𝑁 − 1) = ((;;;2502 +
1) − 1) |
16 | | 8nn0 12186 |
. . . . . 6
⊢ 8 ∈
ℕ0 |
17 | 2, 16 | deccl 12381 |
. . . . 5
⊢ ;18 ∈
ℕ0 |
18 | | 3nn0 12181 |
. . . . . 6
⊢ 3 ∈
ℕ0 |
19 | 2, 18 | deccl 12381 |
. . . . 5
⊢ ;13 ∈
ℕ0 |
20 | | 9nn0 12187 |
. . . . 5
⊢ 9 ∈
ℕ0 |
21 | | eqid 2738 |
. . . . 5
⊢ ;;139 = ;;139 |
22 | | 6nn0 12184 |
. . . . . 6
⊢ 6 ∈
ℕ0 |
23 | 2, 22 | deccl 12381 |
. . . . 5
⊢ ;16 ∈
ℕ0 |
24 | | eqid 2738 |
. . . . . 6
⊢ ;13 = ;13 |
25 | | eqid 2738 |
. . . . . 6
⊢ ;16 = ;16 |
26 | | 7nn0 12185 |
. . . . . . 7
⊢ 7 ∈
ℕ0 |
27 | | eqid 2738 |
. . . . . . 7
⊢ ;18 = ;18 |
28 | | 6cn 11994 |
. . . . . . . . 9
⊢ 6 ∈
ℂ |
29 | | ax-1cn 10860 |
. . . . . . . . 9
⊢ 1 ∈
ℂ |
30 | | 6p1e7 12051 |
. . . . . . . . 9
⊢ (6 + 1) =
7 |
31 | 28, 29, 30 | addcomli 11097 |
. . . . . . . 8
⊢ (1 + 6) =
7 |
32 | 26 | dec0h 12388 |
. . . . . . . 8
⊢ 7 = ;07 |
33 | 31, 32 | eqtri 2766 |
. . . . . . 7
⊢ (1 + 6) =
;07 |
34 | 29 | mulid1i 10910 |
. . . . . . . . 9
⊢ (1
· 1) = 1 |
35 | 29 | addid2i 11093 |
. . . . . . . . 9
⊢ (0 + 1) =
1 |
36 | 34, 35 | oveq12i 7267 |
. . . . . . . 8
⊢ ((1
· 1) + (0 + 1)) = (1 + 1) |
37 | | 1p1e2 12028 |
. . . . . . . 8
⊢ (1 + 1) =
2 |
38 | 36, 37 | eqtri 2766 |
. . . . . . 7
⊢ ((1
· 1) + (0 + 1)) = 2 |
39 | | 8cn 12000 |
. . . . . . . . . 10
⊢ 8 ∈
ℂ |
40 | 39 | mulid1i 10910 |
. . . . . . . . 9
⊢ (8
· 1) = 8 |
41 | 40 | oveq1i 7265 |
. . . . . . . 8
⊢ ((8
· 1) + 7) = (8 + 7) |
42 | | 8p7e15 12451 |
. . . . . . . 8
⊢ (8 + 7) =
;15 |
43 | 41, 42 | eqtri 2766 |
. . . . . . 7
⊢ ((8
· 1) + 7) = ;15 |
44 | 2, 16, 9, 26, 27, 33, 2, 7, 2,
38, 43 | decmac 12418 |
. . . . . 6
⊢ ((;18 · 1) + (1 + 6)) = ;25 |
45 | 22 | dec0h 12388 |
. . . . . . 7
⊢ 6 = ;06 |
46 | | 3cn 11984 |
. . . . . . . . . 10
⊢ 3 ∈
ℂ |
47 | 46 | mulid2i 10911 |
. . . . . . . . 9
⊢ (1
· 3) = 3 |
48 | 46 | addid2i 11093 |
. . . . . . . . 9
⊢ (0 + 3) =
3 |
49 | 47, 48 | oveq12i 7267 |
. . . . . . . 8
⊢ ((1
· 3) + (0 + 3)) = (3 + 3) |
50 | | 3p3e6 12055 |
. . . . . . . 8
⊢ (3 + 3) =
6 |
51 | 49, 50 | eqtri 2766 |
. . . . . . 7
⊢ ((1
· 3) + (0 + 3)) = 6 |
52 | | 4nn0 12182 |
. . . . . . . 8
⊢ 4 ∈
ℕ0 |
53 | | 8t3e24 12482 |
. . . . . . . 8
⊢ (8
· 3) = ;24 |
54 | | 4cn 11988 |
. . . . . . . . 9
⊢ 4 ∈
ℂ |
55 | | 6p4e10 12438 |
. . . . . . . . 9
⊢ (6 + 4) =
;10 |
56 | 28, 54, 55 | addcomli 11097 |
. . . . . . . 8
⊢ (4 + 6) =
;10 |
57 | 6, 52, 22, 53, 11, 56 | decaddci2 12428 |
. . . . . . 7
⊢ ((8
· 3) + 6) = ;30 |
58 | 2, 16, 9, 22, 27, 45, 18, 9, 18, 51, 57 | decmac 12418 |
. . . . . 6
⊢ ((;18 · 3) + 6) = ;60 |
59 | 2, 18, 2, 22, 24, 25, 17, 9, 22, 44, 58 | decma2c 12419 |
. . . . 5
⊢ ((;18 · ;13) + ;16) = ;;250 |
60 | | 9cn 12003 |
. . . . . . . . 9
⊢ 9 ∈
ℂ |
61 | 60 | mulid2i 10911 |
. . . . . . . 8
⊢ (1
· 9) = 9 |
62 | 61 | oveq1i 7265 |
. . . . . . 7
⊢ ((1
· 9) + 7) = (9 + 7) |
63 | | 9p7e16 12458 |
. . . . . . 7
⊢ (9 + 7) =
;16 |
64 | 62, 63 | eqtri 2766 |
. . . . . 6
⊢ ((1
· 9) + 7) = ;16 |
65 | | 9t8e72 12494 |
. . . . . . 7
⊢ (9
· 8) = ;72 |
66 | 60, 39, 65 | mulcomli 10915 |
. . . . . 6
⊢ (8
· 9) = ;72 |
67 | 20, 2, 16, 27, 6, 26, 64, 66 | decmul1c 12431 |
. . . . 5
⊢ (;18 · 9) = ;;162 |
68 | 17, 19, 20, 21, 6, 23, 59, 67 | decmul2c 12432 |
. . . 4
⊢ (;18 · ;;139) =
;;;2502 |
69 | 10, 6 | deccl 12381 |
. . . . . 6
⊢ ;;;2502
∈ ℕ0 |
70 | 69 | nn0cni 12175 |
. . . . 5
⊢ ;;;2502
∈ ℂ |
71 | 70, 29 | pncan3oi 11167 |
. . . 4
⊢ ((;;;2502 +
1) − 1) = ;;;2502 |
72 | 68, 71 | eqtr4i 2769 |
. . 3
⊢ (;18 · ;;139) =
((;;;2502 +
1) − 1) |
73 | 15, 72 | eqtr4i 2769 |
. 2
⊢ (𝑁 − 1) = (;18 · ;;139) |
74 | 10, 18 | deccl 12381 |
. . . . . 6
⊢ ;;;2503
∈ ℕ0 |
75 | 5, 74 | eqeltri 2835 |
. . . . 5
⊢ 𝑁 ∈
ℕ0 |
76 | 75 | nn0cni 12175 |
. . . 4
⊢ 𝑁 ∈ ℂ |
77 | | npcan 11160 |
. . . 4
⊢ ((𝑁 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑁 −
1) + 1) = 𝑁) |
78 | 76, 29, 77 | mp2an 688 |
. . 3
⊢ ((𝑁 − 1) + 1) = 𝑁 |
79 | 78 | eqcomi 2747 |
. 2
⊢ 𝑁 = ((𝑁 − 1) + 1) |
80 | | 1nn 11914 |
. 2
⊢ 1 ∈
ℕ |
81 | | 2nn 11976 |
. 2
⊢ 2 ∈
ℕ |
82 | 19, 20 | deccl 12381 |
. . . . 5
⊢ ;;139 ∈ ℕ0 |
83 | 82 | numexp1 16706 |
. . . 4
⊢ (;;139↑1) = ;;139 |
84 | 83 | oveq2i 7266 |
. . 3
⊢ (;18 · (;;139↑1)) = (;18 · ;;139) |
85 | 73, 84 | eqtr4i 2769 |
. 2
⊢ (𝑁 − 1) = (;18 · (;;139↑1)) |
86 | | 8lt10 12498 |
. . . 4
⊢ 8 <
;10 |
87 | | 1lt10 12505 |
. . . . 5
⊢ 1 <
;10 |
88 | 80, 18, 2, 87 | declti 12404 |
. . . 4
⊢ 1 <
;13 |
89 | 2, 19, 16, 20, 86, 88 | decltc 12395 |
. . 3
⊢ ;18 < ;;139 |
90 | 89, 83 | breqtrri 5097 |
. 2
⊢ ;18 < (;;139↑1) |
91 | 5 | 2503lem2 16767 |
. 2
⊢
((2↑(𝑁 −
1)) mod 𝑁) = (1 mod 𝑁) |
92 | 5 | 2503lem3 16768 |
. 2
⊢
(((2↑;18) − 1)
gcd 𝑁) = 1 |
93 | 1, 4, 73, 79, 4, 80, 81, 85, 90, 91, 92 | pockthi 16536 |
1
⊢ 𝑁 ∈ ℙ |