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	⊢ 𝑁 = ; ; ; 1 2 5 9
Assertion	1259prm	⊢ 𝑁 ∈ ℙ

Proof

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