Metamath Proof Explorer


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

Proof

Step Hyp Ref Expression
1 1259prm.1 N=1259
2 37prm 37
3 3nn0 30
4 4nn 4
5 3 4 decnncl 34
6 1nn0 10
7 2nn0 20
8 6 7 deccl 120
9 5nn0 50
10 8 9 deccl 1250
11 8nn0 80
12 10 11 deccl 12580
13 12 nn0cni 1258
14 ax-1cn 1
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 N1=1258
20 4nn0 40
21 3 20 deccl 340
22 7nn0 70
23 eqid 37=37
24 7 3 deccl 230
25 eqid 34=34
26 eqid 23=23
27 3t3e9 33=9
28 2p1e3 2+1=3
29 27 28 oveq12i 33+2+1=9+3
30 9p3e12 9+3=12
31 29 30 eqtri 33+2+1=12
32 4t3e12 43=12
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 43+3=15
38 3 20 7 3 25 26 3 9 6 31 37 decmac 343+23=125
39 7cn 7
40 7t3e21 73=21
41 39 33 40 mulcomli 37=21
42 1p2e3 1+2=3
43 7 6 7 41 42 decaddi 37+2=23
44 4cn 4
45 7t4e28 74=28
46 39 44 45 mulcomli 47=28
47 22 3 20 25 11 7 43 46 decmul1c 347=238
48 21 3 22 23 11 24 38 47 decmul2c 3437=1258
49 19 48 eqtr4i N1=3437
50 9nn0 90
51 10 50 deccl 12590
52 1 51 eqeltri N0
53 52 nn0cni N
54 npcan N1N-1+1=N
55 53 14 54 mp2an N-1+1=N
56 55 eqcomi N=N-1+1
57 1nn 1
58 2nn 2
59 3 22 deccl 370
60 59 numexp1 371=37
61 60 oveq2i 34371=3437
62 49 61 eqtr4i N1=34371
63 7nn 7
64 4lt7 4<7
65 3 20 63 64 declt 34<37
66 65 60 breqtrri 34<371
67 1 1259lem4 2N1modN=1modN
68 1 1259lem5 2341gcdN=1
69 2 5 49 56 5 57 58 62 66 67 68 pockthi N