Theorem 43prm

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

	Ref	Expression
Assertion	43prm	$$⊢43\in \mathbb{P}$$

Proof

Step	Hyp	Ref	Expression
1		4nn0	$$⊢4\in {\mathbb{N}}_0$$
2		3nn	$$⊢3\in \mathbb{N}$$
3	1 2	decnncl	$$⊢43\in \mathbb{N}$$
4		8nn0	$$⊢8\in {\mathbb{N}}_0$$
5	4 1	deccl	$$⊢84\in {\mathbb{N}}_0$$
6		3nn0	$$⊢3\in {\mathbb{N}}_0$$
7		1nn0	$$⊢1\in {\mathbb{N}}_0$$
8		3lt10	$$⊢3<10$$
9		8nn	$$⊢8\in \mathbb{N}$$
10		4lt10	$$⊢4<10$$
11	9 1 1 10	declti	$$⊢4<84$$
12	1 5 6 7 8 11	decltc	$$⊢43<841$$
13		4nn	$$⊢4\in \mathbb{N}$$
14		1lt10	$$⊢1<10$$
15	13 6 7 14	declti	$$⊢1<43$$
16		2cn	$$⊢2\in ℂ$$
17	16	mulid2i	$$⊢1\cdot 2=2$$
18		df-3	$$⊢3=2+1$$
19	1 7 17 18	dec2dvds	$$⊢\neg 2\parallel 43$$
20	7 1	deccl	$$⊢14\in {\mathbb{N}}_0$$
21		1nn	$$⊢1\in \mathbb{N}$$
22		0nn0	$$⊢0\in {\mathbb{N}}_0$$
23		eqid	$$⊢14=14$$
24	7	dec0h	$$⊢1=01$$
25		3cn	$$⊢3\in ℂ$$
26	25	mulid1i	$$⊢3\cdot 1=3$$
27		ax-1cn	$$⊢1\in ℂ$$
28	27	addid2i	$$⊢0+1=1$$
29	26 28	oveq12i	$$⊢3\cdot 1+0+1=3+1$$
30		3p1e4	$$⊢3+1=4$$
31	29 30	eqtri	$$⊢3\cdot 1+0+1=4$$
32		2nn0	$$⊢2\in {\mathbb{N}}_0$$
33		2p1e3	$$⊢2+1=3$$
34		4cn	$$⊢4\in ℂ$$
35		4t3e12	$$⊢4\cdot 3=12$$
36	34 25 35	mulcomli	$$⊢3\cdot 4=12$$
37	7 32 33 36	decsuc	$$⊢3\cdot 4+1=13$$
38	7 1 22 7 23 24 6 6 7 31 37	decma2c	$$⊢3\cdot 14+1=43$$
39		1lt3	$$⊢1<3$$
40	2 20 21 38 39	ndvdsi	$$⊢\neg 3\parallel 43$$
41		3lt5	$$⊢3<5$$
42	1 2 41	dec5dvds	$$⊢\neg 5\parallel 43$$
43		7nn	$$⊢7\in \mathbb{N}$$
44		6nn0	$$⊢6\in {\mathbb{N}}_0$$
45		7t6e42	$$⊢7\cdot 6=42$$
46	1 32 33 45	decsuc	$$⊢7\cdot 6+1=43$$
47		1lt7	$$⊢1<7$$
48	43 44 21 46 47	ndvdsi	$$⊢\neg 7\parallel 43$$
49	7 21	decnncl	$$⊢11\in \mathbb{N}$$
50	21	decnncl2	$$⊢10\in \mathbb{N}$$
51		eqid	$$⊢11=11$$
52		eqid	$$⊢10=10$$
53	25	mulid2i	$$⊢1\cdot 3=3$$
54	27	addid1i	$$⊢1+0=1$$
55	53 54	oveq12i	$$⊢1\cdot 3+1+0=3+1$$
56	55 30	eqtri	$$⊢1\cdot 3+1+0=4$$
57	53	oveq1i	$$⊢1\cdot 3+0=3+0$$
58	25	addid1i	$$⊢3+0=3$$
59	6	dec0h	$$⊢3=03$$
60	57 58 59	3eqtri	$$⊢1\cdot 3+0=03$$
61	7 7 7 22 51 52 6 6 22 56 60	decmac	$$⊢11\cdot 3+10=43$$
62		0lt1	$$⊢0<1$$
63	7 22 21 62	declt	$$⊢10<11$$
64	49 6 50 61 63	ndvdsi	$$⊢\neg 11\parallel 43$$
65	7 2	decnncl	$$⊢13\in \mathbb{N}$$
66		eqid	$$⊢13=13$$
67	1	dec0h	$$⊢4=04$$
68	53 28	oveq12i	$$⊢1\cdot 3+0+1=3+1$$
69	68 30	eqtri	$$⊢1\cdot 3+0+1=4$$
70		3t3e9	$$⊢3\cdot 3=9$$
71	70	oveq1i	$$⊢3\cdot 3+4=9+4$$
72		9p4e13	$$⊢9+4=13$$
73	71 72	eqtri	$$⊢3\cdot 3+4=13$$
74	7 6 22 1 66 67 6 6 7 69 73	decmac	$$⊢13\cdot 3+4=43$$
75	21 6 1 10	declti	$$⊢4<13$$
76	65 6 13 74 75	ndvdsi	$$⊢\neg 13\parallel 43$$
77	7 43	decnncl	$$⊢17\in \mathbb{N}$$
78		9nn	$$⊢9\in \mathbb{N}$$
79	43	nnnn0i	$$⊢7\in {\mathbb{N}}_0$$
80	78	nnnn0i	$$⊢9\in {\mathbb{N}}_0$$
81		eqid	$$⊢17=17$$
82	80	dec0h	$$⊢9=09$$
83	16	addid2i	$$⊢0+2=2$$
84	17 83	oveq12i	$$⊢1\cdot 2+0+2=2+2$$
85		2p2e4	$$⊢2+2=4$$
86	84 85	eqtri	$$⊢1\cdot 2+0+2=4$$
87		7t2e14	$$⊢7\cdot 2=14$$
88		1p1e2	$$⊢1+1=2$$
89	78	nncni	$$⊢9\in ℂ$$
90	89 34 72	addcomli	$$⊢4+9=13$$
91	7 1 80 87 88 6 90	decaddci	$$⊢7\cdot 2+9=23$$
92	7 79 22 80 81 82 32 6 32 86 91	decmac	$$⊢17\cdot 2+9=43$$
93		9lt10	$$⊢9<10$$
94	21 79 80 93	declti	$$⊢9<17$$
95	77 32 78 92 94	ndvdsi	$$⊢\neg 17\parallel 43$$
96	7 78	decnncl	$$⊢19\in \mathbb{N}$$
97		5nn	$$⊢5\in \mathbb{N}$$
98	97	nnnn0i	$$⊢5\in {\mathbb{N}}_0$$
99		eqid	$$⊢19=19$$
100	98	dec0h	$$⊢5=05$$
101		9t2e18	$$⊢9\cdot 2=18$$
102		8p5e13	$$⊢8+5=13$$
103	7 4 98 101 88 6 102	decaddci	$$⊢9\cdot 2+5=23$$
104	7 80 22 98 99 100 32 6 32 86 103	decmac	$$⊢19\cdot 2+5=43$$
105		5lt10	$$⊢5<10$$
106	21 80 98 105	declti	$$⊢5<19$$
107	96 32 97 104 106	ndvdsi	$$⊢\neg 19\parallel 43$$
108	32 2	decnncl	$$⊢23\in \mathbb{N}$$
109		2nn	$$⊢2\in \mathbb{N}$$
110	109	decnncl2	$$⊢20\in \mathbb{N}$$
111	108	nncni	$$⊢23\in ℂ$$
112	111	mulid1i	$$⊢23\cdot 1=23$$
113		eqid	$$⊢20=20$$
114	32 6 32 22 112 113 85 58	decadd	$$⊢23\cdot 1+20=43$$
115		3pos	$$⊢0<3$$
116	32 22 2 115	declt	$$⊢20<23$$
117	108 7 110 114 116	ndvdsi	$$⊢\neg 23\parallel 43$$
118	3 12 15 19 40 42 48 64 76 95 107 117	prmlem2	$$⊢43\in \mathbb{P}$$