Theorem 139prm

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

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

Proof

Step	Hyp	Ref	Expression
1		1nn0	$$⊢1\in {\mathbb{N}}_0$$
2		3nn0	$$⊢3\in {\mathbb{N}}_0$$
3	1 2	deccl	$$⊢13\in {\mathbb{N}}_0$$
4		9nn	$$⊢9\in \mathbb{N}$$
5	3 4	decnncl	$$⊢139\in \mathbb{N}$$
6		8nn0	$$⊢8\in {\mathbb{N}}_0$$
7		4nn0	$$⊢4\in {\mathbb{N}}_0$$
8		9nn0	$$⊢9\in {\mathbb{N}}_0$$
9		1lt8	$$⊢1<8$$
10		3lt10	$$⊢3<10$$
11		9lt10	$$⊢9<10$$
12	1 6 2 7 8 1 9 10 11	3decltc	$$⊢139<841$$
13		3nn	$$⊢3\in \mathbb{N}$$
14	1 13	decnncl	$$⊢13\in \mathbb{N}$$
15		1lt10	$$⊢1<10$$
16	14 8 1 15	declti	$$⊢1<139$$
17		4t2e8	$$⊢4\cdot 2=8$$
18		df-9	$$⊢9=8+1$$
19	3 7 17 18	dec2dvds	$$⊢\neg 2\parallel 139$$
20		6nn0	$$⊢6\in {\mathbb{N}}_0$$
21	7 20	deccl	$$⊢46\in {\mathbb{N}}_0$$
22		1nn	$$⊢1\in \mathbb{N}$$
23		0nn0	$$⊢0\in {\mathbb{N}}_0$$
24		eqid	$$⊢46=46$$
25	1	dec0h	$$⊢1=01$$
26		ax-1cn	$$⊢1\in ℂ$$
27	26	addlidi	$$⊢0+1=1$$
28	27	oveq2i	$$⊢3\cdot 4+0+1=3\cdot 4+1$$
29		2nn0	$$⊢2\in {\mathbb{N}}_0$$
30		2p1e3	$$⊢2+1=3$$
31	7	nn0cni	$$⊢4\in ℂ$$
32		3cn	$$⊢3\in ℂ$$
33		4t3e12	$$⊢4\cdot 3=12$$
34	31 32 33	mulcomli	$$⊢3\cdot 4=12$$
35	1 29 30 34	decsuc	$$⊢3\cdot 4+1=13$$
36	28 35	eqtri	$$⊢3\cdot 4+0+1=13$$
37		8p1e9	$$⊢8+1=9$$
38	20	nn0cni	$$⊢6\in ℂ$$
39		6t3e18	$$⊢6\cdot 3=18$$
40	38 32 39	mulcomli	$$⊢3\cdot 6=18$$
41	1 6 37 40	decsuc	$$⊢3\cdot 6+1=19$$
42	7 20 23 1 24 25 2 8 1 36 41	decma2c	$$⊢3\cdot 46+1=139$$
43		1lt3	$$⊢1<3$$
44	13 21 22 42 43	ndvdsi	$$⊢\neg 3\parallel 139$$
45		4nn	$$⊢4\in \mathbb{N}$$
46		4lt5	$$⊢4<5$$
47		5p4e9	$$⊢5+4=9$$
48	3 45 46 47	dec5dvds2	$$⊢\neg 5\parallel 139$$
49		7nn	$$⊢7\in \mathbb{N}$$
50	1 8	deccl	$$⊢19\in {\mathbb{N}}_0$$
51		6nn	$$⊢6\in \mathbb{N}$$
52		eqid	$$⊢19=19$$
53	20	dec0h	$$⊢6=06$$
54		7nn0	$$⊢7\in {\mathbb{N}}_0$$
55		7cn	$$⊢7\in ℂ$$
56	55	mulridi	$$⊢7\cdot 1=7$$
57	38	addlidi	$$⊢0+6=6$$
58	56 57	oveq12i	$$⊢7\cdot 1+0+6=7+6$$
59		7p6e13	$$⊢7+6=13$$
60	58 59	eqtri	$$⊢7\cdot 1+0+6=13$$
61		9cn	$$⊢9\in ℂ$$
62		9t7e63	$$⊢9\cdot 7=63$$
63	61 55 62	mulcomli	$$⊢7\cdot 9=63$$
64		6p3e9	$$⊢6+3=9$$
65	38 32 64	addcomli	$$⊢3+6=9$$
66	20 2 20 63 65	decaddi	$$⊢7\cdot 9+6=69$$
67	1 8 23 20 52 53 54 8 20 60 66	decma2c	$$⊢7\cdot 19+6=139$$
68		6lt7	$$⊢6<7$$
69	49 50 51 67 68	ndvdsi	$$⊢\neg 7\parallel 139$$
70	1 22	decnncl	$$⊢11\in \mathbb{N}$$
71	1 29	deccl	$$⊢12\in {\mathbb{N}}_0$$
72		eqid	$$⊢12=12$$
73	54	dec0h	$$⊢7=07$$
74	1 1	deccl	$$⊢11\in {\mathbb{N}}_0$$
75		2cn	$$⊢2\in ℂ$$
76	75	addlidi	$$⊢0+2=2$$
77	76	oveq2i	$$⊢11\cdot 1+0+2=11\cdot 1+2$$
78	70	nncni	$$⊢11\in ℂ$$
79	78	mulridi	$$⊢11\cdot 1=11$$
80		1p2e3	$$⊢1+2=3$$
81	1 1 29 79 80	decaddi	$$⊢11\cdot 1+2=13$$
82	77 81	eqtri	$$⊢11\cdot 1+0+2=13$$
83		eqid	$$⊢11=11$$
84	75	mullidi	$$⊢1\cdot 2=2$$
85		00id	$$⊢0+0=0$$
86	84 85	oveq12i	$$⊢1\cdot 2+0+0=2+0$$
87	75	addridi	$$⊢2+0=2$$
88	86 87	eqtri	$$⊢1\cdot 2+0+0=2$$
89	84	oveq1i	$$⊢1\cdot 2+7=2+7$$
90		7p2e9	$$⊢7+2=9$$
91	55 75 90	addcomli	$$⊢2+7=9$$
92	8	dec0h	$$⊢9=09$$
93	89 91 92	3eqtri	$$⊢1\cdot 2+7=09$$
94	1 1 23 54 83 73 29 8 23 88 93	decmac	$$⊢11\cdot 2+7=29$$
95	1 29 23 54 72 73 74 8 29 82 94	decma2c	$$⊢11\cdot 12+7=139$$
96		7lt10	$$⊢7<10$$
97	22 1 54 96	declti	$$⊢7<11$$
98	70 71 49 95 97	ndvdsi	$$⊢\neg 11\parallel 139$$
99		10nn0	$$⊢10\in {\mathbb{N}}_0$$
100		eqid	$$⊢10=10$$
101		eqid	$$⊢13=13$$
102	23	dec0h	$$⊢0=00$$
103	85 102	eqtri	$$⊢0+0=00$$
104	26	mulridi	$$⊢1\cdot 1=1$$
105	104 85	oveq12i	$$⊢1\cdot 1+0+0=1+0$$
106	26	addridi	$$⊢1+0=1$$
107	105 106	eqtri	$$⊢1\cdot 1+0+0=1$$
108	32	mulridi	$$⊢3\cdot 1=3$$
109	108	oveq1i	$$⊢3\cdot 1+0=3+0$$
110	32	addridi	$$⊢3+0=3$$
111	2	dec0h	$$⊢3=03$$
112	109 110 111	3eqtri	$$⊢3\cdot 1+0=03$$
113	1 2 23 23 101 103 1 2 23 107 112	decmac	$$⊢13\cdot 1+0+0=13$$
114	3	nn0cni	$$⊢13\in ℂ$$
115	114	mul01i	$$⊢13\cdot 0=0$$
116	115	oveq1i	$$⊢13\cdot 0+9=0+9$$
117	61	addlidi	$$⊢0+9=9$$
118	116 117 92	3eqtri	$$⊢13\cdot 0+9=09$$
119	1 23 23 8 100 92 3 8 23 113 118	decma2c	$$⊢13\cdot 10+9=139$$
120	22 2 8 11	declti	$$⊢9<13$$
121	14 99 4 119 120	ndvdsi	$$⊢\neg 13\parallel 139$$
122	1 49	decnncl	$$⊢17\in \mathbb{N}$$
123		eqid	$$⊢17=17$$
124		5nn0	$$⊢5\in {\mathbb{N}}_0$$
125		8cn	$$⊢8\in ℂ$$
126	125	mullidi	$$⊢1\cdot 8=8$$
127		5cn	$$⊢5\in ℂ$$
128	127	addlidi	$$⊢0+5=5$$
129	126 128	oveq12i	$$⊢1\cdot 8+0+5=8+5$$
130		8p5e13	$$⊢8+5=13$$
131	129 130	eqtri	$$⊢1\cdot 8+0+5=13$$
132		8t7e56	$$⊢8\cdot 7=56$$
133	125 55 132	mulcomli	$$⊢7\cdot 8=56$$
134	124 20 2 133 64	decaddi	$$⊢7\cdot 8+3=59$$
135	1 54 23 2 123 111 6 8 124 131 134	decmac	$$⊢17\cdot 8+3=139$$
136	22 54 2 10	declti	$$⊢3<17$$
137	122 6 13 135 136	ndvdsi	$$⊢\neg 17\parallel 139$$
138	1 4	decnncl	$$⊢19\in \mathbb{N}$$
139	55	mullidi	$$⊢1\cdot 7=7$$
140	139 57	oveq12i	$$⊢1\cdot 7+0+6=7+6$$
141	140 59	eqtri	$$⊢1\cdot 7+0+6=13$$
142	20 2 20 62 65	decaddi	$$⊢9\cdot 7+6=69$$
143	1 8 23 20 52 53 54 8 20 141 142	decmac	$$⊢19\cdot 7+6=139$$
144		6lt10	$$⊢6<10$$
145	22 8 20 144	declti	$$⊢6<19$$
146	138 54 51 143 145	ndvdsi	$$⊢\neg 19\parallel 139$$
147	29 13	decnncl	$$⊢23\in \mathbb{N}$$
148		eqid	$$⊢23=23$$
149		6t2e12	$$⊢6\cdot 2=12$$
150	38 75 149	mulcomli	$$⊢2\cdot 6=12$$
151	1 29 30 150	decsuc	$$⊢2\cdot 6+1=13$$
152	29 2 1 148 20 8 1 151 41	decrmac	$$⊢23\cdot 6+1=139$$
153		2nn	$$⊢2\in \mathbb{N}$$
154	153 2 1 15	declti	$$⊢1<23$$
155	147 20 22 152 154	ndvdsi	$$⊢\neg 23\parallel 139$$
156	5 12 16 19 44 48 69 98 121 137 146 155	prmlem2	$$⊢139\in \mathbb{P}$$