Theorem 1259prm

Description: 1259 is a prime number. (Contributed by Mario Carneiro, 22-Feb-2014) (Proof shortened by Mario Carneiro, 20-Apr-2015)

	Ref	Expression
Hypothesis	1259prm.1	$$⊢N=1259$$
Assertion	1259prm	$$⊢N\in \mathbb{P}$$

Proof

Step	Hyp	Ref	Expression
1		1259prm.1	$$⊢N=1259$$
2		37prm	$$⊢37\in \mathbb{P}$$
3		3nn0	$$⊢3\in {\mathbb{N}}_0$$
4		4nn	$$⊢4\in \mathbb{N}$$
5	3 4	decnncl	$$⊢34\in \mathbb{N}$$
6		1nn0	$$⊢1\in {\mathbb{N}}_0$$
7		2nn0	$$⊢2\in {\mathbb{N}}_0$$
8	6 7	deccl	$$⊢12\in {\mathbb{N}}_0$$
9		5nn0	$$⊢5\in {\mathbb{N}}_0$$
10	8 9	deccl	$$⊢125\in {\mathbb{N}}_0$$
11		8nn0	$$⊢8\in {\mathbb{N}}_0$$
12	10 11	deccl	$$⊢1258\in {\mathbb{N}}_0$$
13	12	nn0cni	$$⊢1258\in ℂ$$
14		ax-1cn	$$⊢1\in ℂ$$
15		eqid	$$⊢1258=1258$$
16		8p1e9	$$⊢8+1=9$$
17	10 11 6 15 16	decaddi	$$⊢1258+1=1259$$
18	1 17	eqtr4i	$$⊢N=1258+1$$
19	13 14 18	mvrraddi	$$⊢N-1=1258$$
20		4nn0	$$⊢4\in {\mathbb{N}}_0$$
21	3 20	deccl	$$⊢34\in {\mathbb{N}}_0$$
22		7nn0	$$⊢7\in {\mathbb{N}}_0$$
23		eqid	$$⊢37=37$$
24	7 3	deccl	$$⊢23\in {\mathbb{N}}_0$$
25		eqid	$$⊢34=34$$
26		eqid	$$⊢23=23$$
27		3t3e9	$$⊢3\cdot 3=9$$
28		2p1e3	$$⊢2+1=3$$
29	27 28	oveq12i	$$⊢3\cdot 3+2+1=9+3$$
30		9p3e12	$$⊢9+3=12$$
31	29 30	eqtri	$$⊢3\cdot 3+2+1=12$$
32		4t3e12	$$⊢4\cdot 3=12$$
33		3cn	$$⊢3\in ℂ$$
34		2cn	$$⊢2\in ℂ$$
35		3p2e5	$$⊢3+2=5$$
36	33 34 35	addcomli	$$⊢2+3=5$$
37	6 7 3 32 36	decaddi	$$⊢4\cdot 3+3=15$$
38	3 20 7 3 25 26 3 9 6 31 37	decmac	$$⊢34\cdot 3+23=125$$
39		7cn	$$⊢7\in ℂ$$
40		7t3e21	$$⊢7\cdot 3=21$$
41	39 33 40	mulcomli	$$⊢3\cdot 7=21$$
42		1p2e3	$$⊢1+2=3$$
43	7 6 7 41 42	decaddi	$$⊢3\cdot 7+2=23$$
44		4cn	$$⊢4\in ℂ$$
45		7t4e28	$$⊢7\cdot 4=28$$
46	39 44 45	mulcomli	$$⊢4\cdot 7=28$$
47	22 3 20 25 11 7 43 46	decmul1c	$$⊢34\cdot 7=238$$
48	21 3 22 23 11 24 38 47	decmul2c	$$⊢34\cdot 37=1258$$
49	19 48	eqtr4i	$$⊢N-1=34\cdot 37$$
50		9nn0	$$⊢9\in {\mathbb{N}}_0$$
51	10 50	deccl	$$⊢1259\in {\mathbb{N}}_0$$
52	1 51	eqeltri	$$⊢N\in {\mathbb{N}}_0$$
53	52	nn0cni	$$⊢N\in ℂ$$
54		npcan	$$⊢\left(N\in ℂ\wedge 1\in ℂ\right)\to N-1+1=N$$
55	53 14 54	mp2an	$$⊢N-1+1=N$$
56	55	eqcomi	$$⊢N=N-1+1$$
57		1nn	$$⊢1\in \mathbb{N}$$
58		2nn	$$⊢2\in \mathbb{N}$$
59	3 22	deccl	$$⊢37\in {\mathbb{N}}_0$$
60	59	numexp1	$$⊢{37}^1=37$$
61	60	oveq2i	$$⊢34{37}^1=34\cdot 37$$
62	49 61	eqtr4i	$$⊢N-1=34{37}^1$$
63		7nn	$$⊢7\in \mathbb{N}$$
64		4lt7	$$⊢4<7$$
65	3 20 63 64	declt	$$⊢34<37$$
66	65 60	breqtrri	$$⊢34<{37}^1$$
67	1	1259lem4	$$⊢2^{N-1}\mathrm{mod}N=1\mathrm{mod}N$$
68	1	1259lem5	$$⊢\left(2^{34}-1\right)\gcd N=1$$
69	2 5 49 56 5 57 58 62 66 67 68	pockthi	$$⊢N\in \mathbb{P}$$