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 \mathbb{P}$$

Proof

Step	Hyp	Ref	Expression
1		4001prm.1	$$⊢N=4001$$
2		5prm	$$⊢5\in \mathbb{P}$$
3		8nn	$$⊢8\in \mathbb{N}$$
4	3	decnncl2	$$⊢80\in \mathbb{N}$$
5	4	decnncl2	$$⊢800\in \mathbb{N}$$
6		4nn0	$$⊢4\in {\mathbb{N}}_0$$
7		0nn0	$$⊢0\in {\mathbb{N}}_0$$
8	6 7	deccl	$$⊢40\in {\mathbb{N}}_0$$
9	8 7	deccl	$$⊢400\in {\mathbb{N}}_0$$
10	9 7	deccl	$$⊢4000\in {\mathbb{N}}_0$$
11	10	nn0cni	$$⊢4000\in ℂ$$
12		ax-1cn	$$⊢1\in ℂ$$
13	12	addlidi	$$⊢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 {\mathbb{N}}_0$$
19		8nn0	$$⊢8\in {\mathbb{N}}_0$$
20	19 7	deccl	$$⊢80\in {\mathbb{N}}_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 {\mathbb{N}}_0$$
30	9 29	deccl	$$⊢4001\in {\mathbb{N}}_0$$
31	1 30	eqeltri	$$⊢N\in {\mathbb{N}}_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 {\mathbb{N}}_0$$
37		2nn	$$⊢2\in \mathbb{N}$$
38	36 37	decnncl	$$⊢32\in \mathbb{N}$$
39		3nn	$$⊢3\in \mathbb{N}$$
40		2nn0	$$⊢2\in {\mathbb{N}}_0$$
41	36 40	deccl	$$⊢32\in {\mathbb{N}}_0$$
42	29 40	deccl	$$⊢12\in {\mathbb{N}}_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	addlidi	$$⊢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 {\mathbb{N}}_0$$
55	29 54	deccl	$$⊢16\in {\mathbb{N}}_0$$
56		eqid	$$⊢12=12$$
57		eqid	$$⊢16=16$$
58		7nn0	$$⊢7\in {\mathbb{N}}_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 {\mathbb{N}}_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	$$⊢325^3=4000$$
95	17 94	eqtr4i	$$⊢N-1=325^3$$
96		2lt10	$$⊢2<10$$
97		1nn	$$⊢1\in \mathbb{N}$$
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)\gcd N=1$$
104	2 5 28 35 38 39 37 95 101 102 103	pockthi	$$⊢N\in \mathbb{P}$$