Metamath Proof Explorer

Theorem 4001prm

Description: 4001 is a prime number. (Contributed by Mario Carneiro, 3-Mar-2014) (Proof shortened by Mario Carneiro, 20-Apr-2015) (Proof shortened by AV, 16-Sep-2021)

Ref Expression
Hypothesis 4001prm.1 
|- N = ; ; ; 4 0 0 1
Assertion 4001prm 
|- N e. Prime

Proof

Step Hyp Ref Expression
1 4001prm.1 
 |-  N = ; ; ; 4 0 0 1
2 5prm 
 |-  5 e. Prime
3 8nn 
 |-  8 e. NN
4 3 decnncl2 
 |-  ; 8 0 e. NN
5 4 decnncl2 
 |-  ; ; 8 0 0 e. NN
6 4nn0 
 |-  4 e. NN0
7 0nn0 
 |-  0 e. NN0
8 6 7 deccl 
 |-  ; 4 0 e. NN0
9 8 7 deccl 
 |-  ; ; 4 0 0 e. NN0
10 9 7 deccl 
 |-  ; ; ; 4 0 0 0 e. NN0
11 10 nn0cni 
 |-  ; ; ; 4 0 0 0 e. CC
12 ax-1cn 
 |-  1 e. CC
13 12 addlidi 
 |-  ( 0 + 1 ) = 1
14 eqid 
 |-  ; ; ; 4 0 0 0 = ; ; ; 4 0 0 0
15 9 7 13 14 decsuc 
 |-  ( ; ; ; 4 0 0 0 + 1 ) = ; ; ; 4 0 0 1
16 1 15 eqtr4i 
 |-  N = ( ; ; ; 4 0 0 0 + 1 )
17 11 12 16 mvrraddi 
 |-  ( N - 1 ) = ; ; ; 4 0 0 0
18 5nn0 
 |-  5 e. NN0
19 8nn0 
 |-  8 e. NN0
20 19 7 deccl 
 |-  ; 8 0 e. NN0
21 eqid 
 |-  ; ; 8 0 0 = ; ; 8 0 0
22 eqid 
 |-  ; 8 0 = ; 8 0
23 8t5e40 
 |-  ( 8 x. 5 ) = ; 4 0
24 5cn 
 |-  5 e. CC
25 24 mul02i 
 |-  ( 0 x. 5 ) = 0
26 18 19 7 22 23 25 decmul1 
 |-  ( ; 8 0 x. 5 ) = ; ; 4 0 0
27 18 20 7 21 26 25 decmul1 
 |-  ( ; ; 8 0 0 x. 5 ) = ; ; ; 4 0 0 0
28 17 27 eqtr4i 
 |-  ( N - 1 ) = ( ; ; 8 0 0 x. 5 )
29 1nn0 
 |-  1 e. NN0
30 9 29 deccl 
 |-  ; ; ; 4 0 0 1 e. NN0
31 1 30 eqeltri 
 |-  N e. NN0
32 31 nn0cni 
 |-  N e. CC
33 npcan 
 |-  ( ( N e. CC /\ 1 e. CC ) -> ( ( N - 1 ) + 1 ) = N )
34 32 12 33 mp2an 
 |-  ( ( N - 1 ) + 1 ) = N
35 34 eqcomi 
 |-  N = ( ( N - 1 ) + 1 )
36 3nn0 
 |-  3 e. NN0
37 2nn 
 |-  2 e. NN
38 36 37 decnncl 
 |-  ; 3 2 e. NN
39 3nn 
 |-  3 e. NN
40 2nn0 
 |-  2 e. NN0
41 36 40 deccl 
 |-  ; 3 2 e. NN0
42 29 40 deccl 
 |-  ; 1 2 e. NN0
43 2p1e3 
 |-  ( 2 + 1 ) = 3
44 24 sqvali 
 |-  ( 5 ^ 2 ) = ( 5 x. 5 )
45 5t5e25 
 |-  ( 5 x. 5 ) = ; 2 5
46 44 45 eqtri 
 |-  ( 5 ^ 2 ) = ; 2 5
47 2cn 
 |-  2 e. CC
48 5t2e10 
 |-  ( 5 x. 2 ) = ; 1 0
49 24 47 48 mulcomli 
 |-  ( 2 x. 5 ) = ; 1 0
50 47 addlidi 
 |-  ( 0 + 2 ) = 2
51 29 7 40 49 50 decaddi 
 |-  ( ( 2 x. 5 ) + 2 ) = ; 1 2
52 18 40 18 46 18 40 51 45 decmul1c 
 |-  ( ( 5 ^ 2 ) x. 5 ) = ; ; 1 2 5
53 18 40 43 52 numexpp1 
 |-  ( 5 ^ 3 ) = ; ; 1 2 5
54 6nn0 
 |-  6 e. NN0
55 29 54 deccl 
 |-  ; 1 6 e. NN0
56 eqid 
 |-  ; 1 2 = ; 1 2
57 eqid 
 |-  ; 1 6 = ; 1 6
58 7nn0 
 |-  7 e. NN0
59 7cn 
 |-  7 e. CC
60 7p1e8 
 |-  ( 7 + 1 ) = 8
61 59 12 60 addcomli 
 |-  ( 1 + 7 ) = 8
62 61 19 eqeltri 
 |-  ( 1 + 7 ) e. NN0
63 eqid 
 |-  ; 3 2 = ; 3 2
64 3t1e3 
 |-  ( 3 x. 1 ) = 3
65 64 oveq1i 
 |-  ( ( 3 x. 1 ) + 1 ) = ( 3 + 1 )
66 3p1e4 
 |-  ( 3 + 1 ) = 4
67 65 66 eqtri 
 |-  ( ( 3 x. 1 ) + 1 ) = 4
68 2t1e2 
 |-  ( 2 x. 1 ) = 2
69 68 61 oveq12i 
 |-  ( ( 2 x. 1 ) + ( 1 + 7 ) ) = ( 2 + 8 )
70 8cn 
 |-  8 e. CC
71 8p2e10 
 |-  ( 8 + 2 ) = ; 1 0
72 70 47 71 addcomli 
 |-  ( 2 + 8 ) = ; 1 0
73 69 72 eqtri 
 |-  ( ( 2 x. 1 ) + ( 1 + 7 ) ) = ; 1 0
74 36 40 62 63 29 7 29 67 73 decrmac 
 |-  ( ( ; 3 2 x. 1 ) + ( 1 + 7 ) ) = ; 4 0
75 3t2e6 
 |-  ( 3 x. 2 ) = 6
76 75 oveq1i 
 |-  ( ( 3 x. 2 ) + 1 ) = ( 6 + 1 )
77 6p1e7 
 |-  ( 6 + 1 ) = 7
78 76 77 eqtri 
 |-  ( ( 3 x. 2 ) + 1 ) = 7
79 2t2e4 
 |-  ( 2 x. 2 ) = 4
80 79 oveq1i 
 |-  ( ( 2 x. 2 ) + 6 ) = ( 4 + 6 )
81 6cn 
 |-  6 e. CC
82 4cn 
 |-  4 e. CC
83 6p4e10 
 |-  ( 6 + 4 ) = ; 1 0
84 81 82 83 addcomli 
 |-  ( 4 + 6 ) = ; 1 0
85 80 84 eqtri 
 |-  ( ( 2 x. 2 ) + 6 ) = ; 1 0
86 36 40 54 63 40 7 29 78 85 decrmac 
 |-  ( ( ; 3 2 x. 2 ) + 6 ) = ; 7 0
87 29 40 29 54 56 57 41 7 58 74 86 decma2c 
 |-  ( ( ; 3 2 x. ; 1 2 ) + ; 1 6 ) = ; ; 4 0 0
88 5p1e6 
 |-  ( 5 + 1 ) = 6
89 3cn 
 |-  3 e. CC
90 5t3e15 
 |-  ( 5 x. 3 ) = ; 1 5
91 24 89 90 mulcomli 
 |-  ( 3 x. 5 ) = ; 1 5
92 29 18 88 91 decsuc 
 |-  ( ( 3 x. 5 ) + 1 ) = ; 1 6
93 18 36 40 63 7 29 92 49 decmul1c 
 |-  ( ; 3 2 x. 5 ) = ; ; 1 6 0
94 41 42 18 53 7 55 87 93 decmul2c 
 |-  ( ; 3 2 x. ( 5 ^ 3 ) ) = ; ; ; 4 0 0 0
95 17 94 eqtr4i 
 |-  ( N - 1 ) = ( ; 3 2 x. ( 5 ^ 3 ) )
96 2lt10 
 |-  2 < ; 1 0
97 1nn 
 |-  1 e. NN
98 3lt10 
 |-  3 < ; 1 0
99 97 40 36 98 declti 
 |-  3 < ; 1 2
100 36 42 40 18 96 99 decltc 
 |-  ; 3 2 < ; ; 1 2 5
101 100 53 breqtrri 
 |-  ; 3 2 < ( 5 ^ 3 )
102 1 4001lem3 
 |-  ( ( 2 ^ ( N - 1 ) ) mod N ) = ( 1 mod N )
103 1 4001lem4 
 |-  ( ( ( 2 ^ ; ; 8 0 0 ) - 1 ) gcd N ) = 1
104 2 5 28 35 38 39 37 95 101 102 103 pockthi 
 |-  N e. Prime