# 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 ${⊢}{N}=4001$
Assertion 4001prm ${⊢}{N}\in ℙ$

### Proof

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