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 \mathbb{P}$$

Proof

Step	Hyp	Ref	Expression
1		3nn0	$$⊢3\in {\mathbb{N}}_0$$
2		7nn	$$⊢7\in \mathbb{N}$$
3	1 2	decnncl	$$⊢37\in \mathbb{N}$$
4		8nn0	$$⊢8\in {\mathbb{N}}_0$$
5		4nn0	$$⊢4\in {\mathbb{N}}_0$$
6	4 5	deccl	$$⊢84\in {\mathbb{N}}_0$$
7		7nn0	$$⊢7\in {\mathbb{N}}_0$$
8		1nn0	$$⊢1\in {\mathbb{N}}_0$$
9		7lt10	$$⊢7<10$$
10		8nn	$$⊢8\in \mathbb{N}$$
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 \mathbb{N}$$
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	$$⊢\neg 2\parallel 37$$
20		2nn0	$$⊢2\in {\mathbb{N}}_0$$
21	8 20	deccl	$$⊢12\in {\mathbb{N}}_0$$
22		1nn	$$⊢1\in \mathbb{N}$$
23		6nn0	$$⊢6\in {\mathbb{N}}_0$$
24		6p1e7	$$⊢6+1=7$$
25		eqid	$$⊢12=12$$
26		0nn0	$$⊢0\in {\mathbb{N}}_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	$$⊢\neg 3\parallel 37$$
38		2nn	$$⊢2\in \mathbb{N}$$
39		2lt5	$$⊢2<5$$
40		5p2e7	$$⊢5+2=7$$
41	1 38 39 40	dec5dvds2	$$⊢\neg 5\parallel 37$$
42		5nn0	$$⊢5\in {\mathbb{N}}_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	$$⊢\neg 7\parallel 37$$
47	8 22	decnncl	$$⊢11\in \mathbb{N}$$
48		4nn	$$⊢4\in \mathbb{N}$$
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	$$⊢\neg 11\parallel 37$$
60	8 14	decnncl	$$⊢13\in \mathbb{N}$$
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	$$⊢\neg 13\parallel 37$$
69	8 2	decnncl	$$⊢17\in \mathbb{N}$$
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	$$⊢\neg 17\parallel 37$$
80		9nn	$$⊢9\in \mathbb{N}$$
81	8 80	decnncl	$$⊢19\in \mathbb{N}$$
82	8 10	decnncl	$$⊢18\in \mathbb{N}$$
83		9nn0	$$⊢9\in {\mathbb{N}}_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	$$⊢\neg 19\parallel 37$$
95	20 14	decnncl	$$⊢23\in \mathbb{N}$$
96	8 48	decnncl	$$⊢14\in \mathbb{N}$$
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	$$⊢\neg 23\parallel 37$$
104	3 13 16 19 37 41 46 59 68 79 94 103	prmlem2	$$⊢37\in \mathbb{P}$$