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 = ; ; ; 1 2 5 9
Assertion 1259prm 
|- N e. Prime

Proof

Step Hyp Ref Expression
1 1259prm.1 
 |-  N = ; ; ; 1 2 5 9
2 37prm 
 |-  ; 3 7 e. Prime
3 3nn0 
 |-  3 e. NN0
4 4nn 
 |-  4 e. NN
5 3 4 decnncl 
 |-  ; 3 4 e. NN
6 1nn0 
 |-  1 e. NN0
7 2nn0 
 |-  2 e. NN0
8 6 7 deccl 
 |-  ; 1 2 e. NN0
9 5nn0 
 |-  5 e. NN0
10 8 9 deccl 
 |-  ; ; 1 2 5 e. NN0
11 8nn0 
 |-  8 e. NN0
12 10 11 deccl 
 |-  ; ; ; 1 2 5 8 e. NN0
13 12 nn0cni 
 |-  ; ; ; 1 2 5 8 e. CC
14 ax-1cn 
 |-  1 e. CC
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 
 |-  N = ( ; ; ; 1 2 5 8 + 1 )
19 13 14 18 mvrraddi 
 |-  ( N - 1 ) = ; ; ; 1 2 5 8
20 4nn0 
 |-  4 e. NN0
21 3 20 deccl 
 |-  ; 3 4 e. NN0
22 7nn0 
 |-  7 e. NN0
23 eqid 
 |-  ; 3 7 = ; 3 7
24 7 3 deccl 
 |-  ; 2 3 e. NN0
25 eqid 
 |-  ; 3 4 = ; 3 4
26 eqid 
 |-  ; 2 3 = ; 2 3
27 3t3e9 
 |-  ( 3 x. 3 ) = 9
28 2p1e3 
 |-  ( 2 + 1 ) = 3
29 27 28 oveq12i 
 |-  ( ( 3 x. 3 ) + ( 2 + 1 ) ) = ( 9 + 3 )
30 9p3e12 
 |-  ( 9 + 3 ) = ; 1 2
31 29 30 eqtri 
 |-  ( ( 3 x. 3 ) + ( 2 + 1 ) ) = ; 1 2
32 4t3e12 
 |-  ( 4 x. 3 ) = ; 1 2
33 3cn 
 |-  3 e. CC
34 2cn 
 |-  2 e. CC
35 3p2e5 
 |-  ( 3 + 2 ) = 5
36 33 34 35 addcomli 
 |-  ( 2 + 3 ) = 5
37 6 7 3 32 36 decaddi 
 |-  ( ( 4 x. 3 ) + 3 ) = ; 1 5
38 3 20 7 3 25 26 3 9 6 31 37 decmac 
 |-  ( ( ; 3 4 x. 3 ) + ; 2 3 ) = ; ; 1 2 5
39 7cn 
 |-  7 e. CC
40 7t3e21 
 |-  ( 7 x. 3 ) = ; 2 1
41 39 33 40 mulcomli 
 |-  ( 3 x. 7 ) = ; 2 1
42 1p2e3 
 |-  ( 1 + 2 ) = 3
43 7 6 7 41 42 decaddi 
 |-  ( ( 3 x. 7 ) + 2 ) = ; 2 3
44 4cn 
 |-  4 e. CC
45 7t4e28 
 |-  ( 7 x. 4 ) = ; 2 8
46 39 44 45 mulcomli 
 |-  ( 4 x. 7 ) = ; 2 8
47 22 3 20 25 11 7 43 46 decmul1c 
 |-  ( ; 3 4 x. 7 ) = ; ; 2 3 8
48 21 3 22 23 11 24 38 47 decmul2c 
 |-  ( ; 3 4 x. ; 3 7 ) = ; ; ; 1 2 5 8
49 19 48 eqtr4i 
 |-  ( N - 1 ) = ( ; 3 4 x. ; 3 7 )
50 9nn0 
 |-  9 e. NN0
51 10 50 deccl 
 |-  ; ; ; 1 2 5 9 e. NN0
52 1 51 eqeltri 
 |-  N e. NN0
53 52 nn0cni 
 |-  N e. CC
54 npcan 
 |-  ( ( N e. CC /\ 1 e. CC ) -> ( ( N - 1 ) + 1 ) = N )
55 53 14 54 mp2an 
 |-  ( ( N - 1 ) + 1 ) = N
56 55 eqcomi 
 |-  N = ( ( N - 1 ) + 1 )
57 1nn 
 |-  1 e. NN
58 2nn 
 |-  2 e. NN
59 3 22 deccl 
 |-  ; 3 7 e. NN0
60 59 numexp1 
 |-  ( ; 3 7 ^ 1 ) = ; 3 7
61 60 oveq2i 
 |-  ( ; 3 4 x. ( ; 3 7 ^ 1 ) ) = ( ; 3 4 x. ; 3 7 )
62 49 61 eqtr4i 
 |-  ( N - 1 ) = ( ; 3 4 x. ( ; 3 7 ^ 1 ) )
63 7nn 
 |-  7 e. NN
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 ^ ( N - 1 ) ) mod N ) = ( 1 mod N )
68 1 1259lem5 
 |-  ( ( ( 2 ^ ; 3 4 ) - 1 ) gcd N ) = 1
69 2 5 49 56 5 57 58 62 66 67 68 pockthi 
 |-  N e. Prime