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	$$⊢N=2503$$
Assertion	2503prm	$$⊢N\in \mathbb{P}$$

Proof

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