Metamath Proof Explorer

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 = ; ; ; 2 5 0 3
Assertion 2503prm 
|- N e. Prime

Proof

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