Metamath Proof Explorer

Theorem 4001prm

Description: 4001 is a prime number. (Contributed by Mario Carneiro, 3-Mar-2014) (Proof shortened by Mario Carneiro, 20-Apr-2015) (Proof shortened by AV, 16-Sep-2021)

Ref Expression
Hypothesis 4001prm.1 ⊢ 𝑁 = 4 0 0 1
Assertion 4001prm 𝑁 ∈ ℙ

Proof

Step Hyp Ref Expression
1 4001prm.1 ⊢ 𝑁 = 4 0 0 1
2 5prm ⊢ 5 ∈ ℙ
3 8nn ⊢ 8 ∈ ℕ
4 3 decnncl2 ⊢ 8 0 ∈ ℕ
5 4 decnncl2 ⊢ 8 0 0 ∈ ℕ
6 4nn0 ⊢ 4 ∈ ℕ0
7 0nn0 ⊢ 0 ∈ ℕ0
8 6 7 deccl ⊢ 4 0 ∈ ℕ0
9 8 7 deccl ⊢ 4 0 0 ∈ ℕ0
10 9 7 deccl ⊢ 4 0 0 0 ∈ ℕ0
11 10 nn0cni ⊢ 4 0 0 0 ∈ ℂ
12 ax-1cn ⊢ 1 ∈ ℂ
13 12 addlidi ⊢ ( 0 + 1 ) = 1
14 eqid ⊢ 4 0 0 0 = 4 0 0 0
15 9 7 13 14 decsuc ⊢ ( 4 0 0 0 + 1 ) = 4 0 0 1
16 1 15 eqtr4i ⊢ 𝑁 = ( 4 0 0 0 + 1 )
17 11 12 16 mvrraddi ⊢ ( 𝑁 − 1 ) = 4 0 0 0
18 5nn0 ⊢ 5 ∈ ℕ0
19 8nn0 ⊢ 8 ∈ ℕ0
20 19 7 deccl ⊢ 8 0 ∈ ℕ0
21 eqid ⊢ 8 0 0 = 8 0 0
22 eqid ⊢ 8 0 = 8 0
23 8t5e40 ⊢ ( 8 · 5 ) = 4 0
24 5cn ⊢ 5 ∈ ℂ
25 24 mul02i ⊢ ( 0 · 5 ) = 0
26 18 19 7 22 23 25 decmul1 ⊢ ( 8 0 · 5 ) = 4 0 0
27 18 20 7 21 26 25 decmul1 ⊢ ( 8 0 0 · 5 ) = 4 0 0 0
28 17 27 eqtr4i ⊢ ( 𝑁 − 1 ) = ( 8 0 0 · 5 )
29 1nn0 ⊢ 1 ∈ ℕ0
30 9 29 deccl ⊢ 4 0 0 1 ∈ ℕ0
31 1 30 eqeltri ⊢ 𝑁 ∈ ℕ0
32 31 nn0cni ⊢ 𝑁 ∈ ℂ
33 npcan ⊢ ( ( 𝑁 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝑁 − 1 ) + 1 ) = 𝑁 )
34 32 12 33 mp2an ⊢ ( ( 𝑁 − 1 ) + 1 ) = 𝑁
35 34 eqcomi ⊢ 𝑁 = ( ( 𝑁 − 1 ) + 1 )
36 3nn0 ⊢ 3 ∈ ℕ0
37 2nn ⊢ 2 ∈ ℕ
38 36 37 decnncl ⊢ 3 2 ∈ ℕ
39 3nn ⊢ 3 ∈ ℕ
40 2nn0 ⊢ 2 ∈ ℕ0
41 36 40 deccl ⊢ 3 2 ∈ ℕ0
42 29 40 deccl ⊢ 1 2 ∈ ℕ0
43 2p1e3 ⊢ ( 2 + 1 ) = 3
44 24 sqvali ⊢ ( 5 ↑ 2 ) = ( 5 · 5 )
45 5t5e25 ⊢ ( 5 · 5 ) = 2 5
46 44 45 eqtri ⊢ ( 5 ↑ 2 ) = 2 5
47 2cn ⊢ 2 ∈ ℂ
48 5t2e10 ⊢ ( 5 · 2 ) = 1 0
49 24 47 48 mulcomli ⊢ ( 2 · 5 ) = 1 0
50 47 addlidi ⊢ ( 0 + 2 ) = 2
51 29 7 40 49 50 decaddi ⊢ ( ( 2 · 5 ) + 2 ) = 1 2
52 18 40 18 46 18 40 51 45 decmul1c ⊢ ( ( 5 ↑ 2 ) · 5 ) = 1 2 5
53 18 40 43 52 numexpp1 ⊢ ( 5 ↑ 3 ) = 1 2 5
54 6nn0 ⊢ 6 ∈ ℕ0
55 29 54 deccl ⊢ 1 6 ∈ ℕ0
56 eqid ⊢ 1 2 = 1 2
57 eqid ⊢ 1 6 = 1 6
58 7nn0 ⊢ 7 ∈ ℕ0
59 7cn ⊢ 7 ∈ ℂ
60 7p1e8 ⊢ ( 7 + 1 ) = 8
61 59 12 60 addcomli ⊢ ( 1 + 7 ) = 8
62 61 19 eqeltri ⊢ ( 1 + 7 ) ∈ ℕ0
63 eqid ⊢ 3 2 = 3 2
64 3t1e3 ⊢ ( 3 · 1 ) = 3
65 64 oveq1i ⊢ ( ( 3 · 1 ) + 1 ) = ( 3 + 1 )
66 3p1e4 ⊢ ( 3 + 1 ) = 4
67 65 66 eqtri ⊢ ( ( 3 · 1 ) + 1 ) = 4
68 2t1e2 ⊢ ( 2 · 1 ) = 2
69 68 61 oveq12i ⊢ ( ( 2 · 1 ) + ( 1 + 7 ) ) = ( 2 + 8 )
70 8cn ⊢ 8 ∈ ℂ
71 8p2e10 ⊢ ( 8 + 2 ) = 1 0
72 70 47 71 addcomli ⊢ ( 2 + 8 ) = 1 0
73 69 72 eqtri ⊢ ( ( 2 · 1 ) + ( 1 + 7 ) ) = 1 0
74 36 40 62 63 29 7 29 67 73 decrmac ⊢ ( ( 3 2 · 1 ) + ( 1 + 7 ) ) = 4 0
75 3t2e6 ⊢ ( 3 · 2 ) = 6
76 75 oveq1i ⊢ ( ( 3 · 2 ) + 1 ) = ( 6 + 1 )
77 6p1e7 ⊢ ( 6 + 1 ) = 7
78 76 77 eqtri ⊢ ( ( 3 · 2 ) + 1 ) = 7
79 2t2e4 ⊢ ( 2 · 2 ) = 4
80 79 oveq1i ⊢ ( ( 2 · 2 ) + 6 ) = ( 4 + 6 )
81 6cn ⊢ 6 ∈ ℂ
82 4cn ⊢ 4 ∈ ℂ
83 6p4e10 ⊢ ( 6 + 4 ) = 1 0
84 81 82 83 addcomli ⊢ ( 4 + 6 ) = 1 0
85 80 84 eqtri ⊢ ( ( 2 · 2 ) + 6 ) = 1 0
86 36 40 54 63 40 7 29 78 85 decrmac ⊢ ( ( 3 2 · 2 ) + 6 ) = 7 0
87 29 40 29 54 56 57 41 7 58 74 86 decma2c ⊢ ( ( 3 2 · 1 2 ) + 1 6 ) = 4 0 0
88 5p1e6 ⊢ ( 5 + 1 ) = 6
89 3cn ⊢ 3 ∈ ℂ
90 5t3e15 ⊢ ( 5 · 3 ) = 1 5
91 24 89 90 mulcomli ⊢ ( 3 · 5 ) = 1 5
92 29 18 88 91 decsuc ⊢ ( ( 3 · 5 ) + 1 ) = 1 6
93 18 36 40 63 7 29 92 49 decmul1c ⊢ ( 3 2 · 5 ) = 1 6 0
94 41 42 18 53 7 55 87 93 decmul2c ⊢ ( 3 2 · ( 5 ↑ 3 ) ) = 4 0 0 0
95 17 94 eqtr4i ⊢ ( 𝑁 − 1 ) = ( 3 2 · ( 5 ↑ 3 ) )
96 2lt10 ⊢ 2 < 1 0
97 1nn ⊢ 1 ∈ ℕ
98 3lt10 ⊢ 3 < 1 0
99 97 40 36 98 declti ⊢ 3 < 1 2
100 36 42 40 18 96 99 decltc ⊢ 3 2 < 1 2 5
101 100 53 breqtrri ⊢ 3 2 < ( 5 ↑ 3 )
102 1 4001lem3 ⊢ ( ( 2 ↑ ( 𝑁 − 1 ) ) mod 𝑁 ) = ( 1 mod 𝑁 )
103 1 4001lem4 ⊢ ( ( ( 2 ↑ 8 0 0 ) − 1 ) gcd 𝑁 ) = 1
104 2 5 28 35 38 39 37 95 101 102 103 pockthi ⊢ 𝑁 ∈ ℙ