# Metamath Proof Explorer

## Theorem 37prm

Description: 37 is a prime number. (Contributed by Mario Carneiro, 18-Feb-2014) (Proof shortened by Mario Carneiro, 20-Apr-2015)

Ref Expression
Assertion 37prm ${⊢}37\in ℙ$

### Proof

Step Hyp Ref Expression
1 3nn0 ${⊢}3\in {ℕ}_{0}$
2 7nn ${⊢}7\in ℕ$
3 1 2 decnncl ${⊢}37\in ℕ$
4 8nn0 ${⊢}8\in {ℕ}_{0}$
5 4nn0 ${⊢}4\in {ℕ}_{0}$
6 4 5 deccl ${⊢}84\in {ℕ}_{0}$
7 7nn0 ${⊢}7\in {ℕ}_{0}$
8 1nn0 ${⊢}1\in {ℕ}_{0}$
9 7lt10 ${⊢}7<10$
10 8nn ${⊢}8\in ℕ$
11 3lt10 ${⊢}3<10$
12 10 5 1 11 declti ${⊢}3<84$
13 1 6 7 8 9 12 decltc ${⊢}37<841$
14 3nn ${⊢}3\in ℕ$
15 1lt10 ${⊢}1<10$
16 14 7 8 15 declti ${⊢}1<37$
17 3t2e6 ${⊢}3\cdot 2=6$
18 df-7 ${⊢}7=6+1$
19 1 1 17 18 dec2dvds ${⊢}¬2\parallel 37$
20 2nn0 ${⊢}2\in {ℕ}_{0}$
21 8 20 deccl ${⊢}12\in {ℕ}_{0}$
22 1nn ${⊢}1\in ℕ$
23 6nn0 ${⊢}6\in {ℕ}_{0}$
24 6p1e7 ${⊢}6+1=7$
25 eqid ${⊢}12=12$
26 0nn0 ${⊢}0\in {ℕ}_{0}$
27 3cn ${⊢}3\in ℂ$
28 27 mulid1i ${⊢}3\cdot 1=3$
29 28 oveq1i ${⊢}3\cdot 1+0=3+0$
30 27 addid1i ${⊢}3+0=3$
31 29 30 eqtri ${⊢}3\cdot 1+0=3$
32 23 dec0h ${⊢}6=06$
33 17 32 eqtri ${⊢}3\cdot 2=06$
34 1 8 20 25 23 26 31 33 decmul2c ${⊢}3\cdot 12=36$
35 1 23 24 34 decsuc ${⊢}3\cdot 12+1=37$
36 1lt3 ${⊢}1<3$
37 14 21 22 35 36 ndvdsi ${⊢}¬3\parallel 37$
38 2nn ${⊢}2\in ℕ$
39 2lt5 ${⊢}2<5$
40 5p2e7 ${⊢}5+2=7$
41 1 38 39 40 dec5dvds2 ${⊢}¬5\parallel 37$
42 5nn0 ${⊢}5\in {ℕ}_{0}$
43 7t5e35 ${⊢}7\cdot 5=35$
44 1 42 20 43 40 decaddi ${⊢}7\cdot 5+2=37$
45 2lt7 ${⊢}2<7$
46 2 42 38 44 45 ndvdsi ${⊢}¬7\parallel 37$
47 8 22 decnncl ${⊢}11\in ℕ$
48 4nn ${⊢}4\in ℕ$
49 eqid ${⊢}11=11$
50 27 mulid2i ${⊢}1\cdot 3=3$
51 50 oveq1i ${⊢}1\cdot 3+4=3+4$
52 48 nncni ${⊢}4\in ℂ$
53 4p3e7 ${⊢}4+3=7$
54 52 27 53 addcomli ${⊢}3+4=7$
55 51 54 eqtri ${⊢}1\cdot 3+4=7$
56 8 8 5 49 1 50 55 decrmanc ${⊢}11\cdot 3+4=37$
57 4lt10 ${⊢}4<10$
58 22 8 5 57 declti ${⊢}4<11$
59 47 1 48 56 58 ndvdsi ${⊢}¬11\parallel 37$
60 8 14 decnncl ${⊢}13\in ℕ$
61 eqid ${⊢}13=13$
62 2cn ${⊢}2\in ℂ$
63 62 mulid2i ${⊢}1\cdot 2=2$
64 20 8 1 61 63 17 decmul1 ${⊢}13\cdot 2=26$
65 2p1e3 ${⊢}2+1=3$
66 20 23 8 8 64 49 65 24 decadd ${⊢}13\cdot 2+11=37$
67 8 8 14 36 declt ${⊢}11<13$
68 60 20 47 66 67 ndvdsi ${⊢}¬13\parallel 37$
69 8 2 decnncl ${⊢}17\in ℕ$
70 eqid ${⊢}17=17$
71 1 dec0h ${⊢}3=03$
72 0p1e1 ${⊢}0+1=1$
73 63 72 oveq12i ${⊢}1\cdot 2+0+1=2+1$
74 73 65 eqtri ${⊢}1\cdot 2+0+1=3$
75 7t2e14 ${⊢}7\cdot 2=14$
76 8 5 1 75 53 decaddi ${⊢}7\cdot 2+3=17$
77 8 7 26 1 70 71 20 7 8 74 76 decmac ${⊢}17\cdot 2+3=37$
78 22 7 1 11 declti ${⊢}3<17$
79 69 20 14 77 78 ndvdsi ${⊢}¬17\parallel 37$
80 9nn ${⊢}9\in ℕ$
81 8 80 decnncl ${⊢}19\in ℕ$
82 8 10 decnncl ${⊢}18\in ℕ$
83 9nn0 ${⊢}9\in {ℕ}_{0}$
84 81 nncni ${⊢}19\in ℂ$
85 84 mulid1i ${⊢}19\cdot 1=19$
86 eqid ${⊢}18=18$
87 1p1e2 ${⊢}1+1=2$
88 87 oveq1i ${⊢}1+1+1=2+1$
89 88 65 eqtri ${⊢}1+1+1=3$
90 9p8e17 ${⊢}9+8=17$
91 8 83 8 4 85 86 89 7 90 decaddc ${⊢}19\cdot 1+18=37$
92 8lt9 ${⊢}8<9$
93 8 4 80 92 declt ${⊢}18<19$
94 81 8 82 91 93 ndvdsi ${⊢}¬19\parallel 37$
95 20 14 decnncl ${⊢}23\in ℕ$
96 8 48 decnncl ${⊢}14\in ℕ$
97 95 nncni ${⊢}23\in ℂ$
98 97 mulid1i ${⊢}23\cdot 1=23$
99 eqid ${⊢}14=14$
100 20 1 8 5 98 99 65 54 decadd ${⊢}23\cdot 1+14=37$
101 1lt2 ${⊢}1<2$
102 8 20 5 1 57 101 decltc ${⊢}14<23$
103 95 8 96 100 102 ndvdsi ${⊢}¬23\parallel 37$
104 3 13 16 19 37 41 46 59 68 79 94 103 prmlem2 ${⊢}37\in ℙ$