This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 = 4001
Assertion 4001prm ⊢ N ∈ ℙ

Proof

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