Metamath Proof Explorer

Theorem 2503prm

Description: 2503 is a prime number. (Contributed by Mario Carneiro, 3-Mar-2014) (Proof shortened by Mario Carneiro, 20-Apr-2015)

Ref Expression
Hypothesis 2503prm.1 ⊢ 𝑁 = 2 5 0 3
Assertion 2503prm 𝑁 ∈ ℙ

Proof

Step Hyp Ref Expression
1 2503prm.1 ⊢ 𝑁 = 2 5 0 3
2 139prm ⊢ 1 3 9 ∈ ℙ
3 1nn0 ⊢ 1 ∈ ℕ0
4 8nn ⊢ 8 ∈ ℕ
5 3 4 decnncl ⊢ 1 8 ∈ ℕ
6 2nn0 ⊢ 2 ∈ ℕ0
7 5nn0 ⊢ 5 ∈ ℕ0
8 6 7 deccl ⊢ 2 5 ∈ ℕ0
9 0nn0 ⊢ 0 ∈ ℕ0
10 8 9 deccl ⊢ 2 5 0 ∈ ℕ0
11 2p1e3 ⊢ ( 2 + 1 ) = 3
12 eqid ⊢ 2 5 0 2 = 2 5 0 2
13 10 6 11 12 decsuc ⊢ ( 2 5 0 2 + 1 ) = 2 5 0 3
14 1 13 eqtr4i ⊢ 𝑁 = ( 2 5 0 2 + 1 )
15 14 oveq1i ⊢ ( 𝑁 − 1 ) = ( ( 2 5 0 2 + 1 ) − 1 )
16 8nn0 ⊢ 8 ∈ ℕ0
17 3 16 deccl ⊢ 1 8 ∈ ℕ0
18 3nn0 ⊢ 3 ∈ ℕ0
19 3 18 deccl ⊢ 1 3 ∈ ℕ0
20 9nn0 ⊢ 9 ∈ ℕ0
21 eqid ⊢ 1 3 9 = 1 3 9
22 6nn0 ⊢ 6 ∈ ℕ0
23 3 22 deccl ⊢ 1 6 ∈ ℕ0
24 eqid ⊢ 1 3 = 1 3
25 eqid ⊢ 1 6 = 1 6
26 7nn0 ⊢ 7 ∈ ℕ0
27 eqid ⊢ 1 8 = 1 8
28 6cn ⊢ 6 ∈ ℂ
29 ax-1cn ⊢ 1 ∈ ℂ
30 6p1e7 ⊢ ( 6 + 1 ) = 7
31 28 29 30 addcomli ⊢ ( 1 + 6 ) = 7
32 26 dec0h ⊢ 7 = 0 7
33 31 32 eqtri ⊢ ( 1 + 6 ) = 0 7
34 29 mulid1i ⊢ ( 1 · 1 ) = 1
35 29 addid2i ⊢ ( 0 + 1 ) = 1
36 34 35 oveq12i ⊢ ( ( 1 · 1 ) + ( 0 + 1 ) ) = ( 1 + 1 )
37 1p1e2 ⊢ ( 1 + 1 ) = 2
38 36 37 eqtri ⊢ ( ( 1 · 1 ) + ( 0 + 1 ) ) = 2
39 8cn ⊢ 8 ∈ ℂ
40 39 mulid1i ⊢ ( 8 · 1 ) = 8
41 40 oveq1i ⊢ ( ( 8 · 1 ) + 7 ) = ( 8 + 7 )
42 8p7e15 ⊢ ( 8 + 7 ) = 1 5
43 41 42 eqtri ⊢ ( ( 8 · 1 ) + 7 ) = 1 5
44 3 16 9 26 27 33 3 7 3 38 43 decmac ⊢ ( ( 1 8 · 1 ) + ( 1 + 6 ) ) = 2 5
45 22 dec0h ⊢ 6 = 0 6
46 3cn ⊢ 3 ∈ ℂ
47 46 mulid2i ⊢ ( 1 · 3 ) = 3
48 46 addid2i ⊢ ( 0 + 3 ) = 3
49 47 48 oveq12i ⊢ ( ( 1 · 3 ) + ( 0 + 3 ) ) = ( 3 + 3 )
50 3p3e6 ⊢ ( 3 + 3 ) = 6
51 49 50 eqtri ⊢ ( ( 1 · 3 ) + ( 0 + 3 ) ) = 6
52 4nn0 ⊢ 4 ∈ ℕ0
53 8t3e24 ⊢ ( 8 · 3 ) = 2 4
54 4cn ⊢ 4 ∈ ℂ
55 6p4e10 ⊢ ( 6 + 4 ) = 1 0
56 28 54 55 addcomli ⊢ ( 4 + 6 ) = 1 0
57 6 52 22 53 11 56 decaddci2 ⊢ ( ( 8 · 3 ) + 6 ) = 3 0
58 3 16 9 22 27 45 18 9 18 51 57 decmac ⊢ ( ( 1 8 · 3 ) + 6 ) = 6 0
59 3 18 3 22 24 25 17 9 22 44 58 decma2c ⊢ ( ( 1 8 · 1 3 ) + 1 6 ) = 2 5 0
60 9cn ⊢ 9 ∈ ℂ
61 60 mulid2i ⊢ ( 1 · 9 ) = 9
62 61 oveq1i ⊢ ( ( 1 · 9 ) + 7 ) = ( 9 + 7 )
63 9p7e16 ⊢ ( 9 + 7 ) = 1 6
64 62 63 eqtri ⊢ ( ( 1 · 9 ) + 7 ) = 1 6
65 9t8e72 ⊢ ( 9 · 8 ) = 7 2
66 60 39 65 mulcomli ⊢ ( 8 · 9 ) = 7 2
67 20 3 16 27 6 26 64 66 decmul1c ⊢ ( 1 8 · 9 ) = 1 6 2
68 17 19 20 21 6 23 59 67 decmul2c ⊢ ( 1 8 · 1 3 9 ) = 2 5 0 2
69 10 6 deccl ⊢ 2 5 0 2 ∈ ℕ0
70 69 nn0cni ⊢ 2 5 0 2 ∈ ℂ
71 70 29 pncan3oi ⊢ ( ( 2 5 0 2 + 1 ) − 1 ) = 2 5 0 2
72 68 71 eqtr4i ⊢ ( 1 8 · 1 3 9 ) = ( ( 2 5 0 2 + 1 ) − 1 )
73 15 72 eqtr4i ⊢ ( 𝑁 − 1 ) = ( 1 8 · 1 3 9 )
74 10 18 deccl ⊢ 2 5 0 3 ∈ ℕ0
75 1 74 eqeltri ⊢ 𝑁 ∈ ℕ0
76 75 nn0cni ⊢ 𝑁 ∈ ℂ
77 npcan ⊢ ( ( 𝑁 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝑁 − 1 ) + 1 ) = 𝑁 )
78 76 29 77 mp2an ⊢ ( ( 𝑁 − 1 ) + 1 ) = 𝑁
79 78 eqcomi ⊢ 𝑁 = ( ( 𝑁 − 1 ) + 1 )
80 1nn ⊢ 1 ∈ ℕ
81 2nn ⊢ 2 ∈ ℕ
82 19 20 deccl ⊢ 1 3 9 ∈ ℕ0
83 82 numexp1 ⊢ ( 1 3 9 ↑ 1 ) = 1 3 9
84 83 oveq2i ⊢ ( 1 8 · ( 1 3 9 ↑ 1 ) ) = ( 1 8 · 1 3 9 )
85 73 84 eqtr4i ⊢ ( 𝑁 − 1 ) = ( 1 8 · ( 1 3 9 ↑ 1 ) )
86 8lt10 ⊢ 8 < 1 0
87 1lt10 ⊢ 1 < 1 0
88 80 18 3 87 declti ⊢ 1 < 1 3
89 3 19 16 20 86 88 decltc ⊢ 1 8 < 1 3 9
90 89 83 breqtrri ⊢ 1 8 < ( 1 3 9 ↑ 1 )
91 1 2503lem2 ⊢ ( ( 2 ↑ ( 𝑁 − 1 ) ) mod 𝑁 ) = ( 1 mod 𝑁 )
92 1 2503lem3 ⊢ ( ( ( 2 ↑ 1 8 ) − 1 ) gcd 𝑁 ) = 1
93 2 5 73 79 5 80 81 85 90 91 92 pockthi ⊢ 𝑁 ∈ ℙ