Theorem 139prmALT

Description: 139 is a prime number. In contrast to 139prm , the proof of this theorem uses 3dvds2dec for checking the divisibility by 3. Although the proof using 3dvds2dec is longer (regarding size: 1849 characters compared with 1809 for 139prm ), the number of essential steps is smaller (301 compared with 327 for 139prm ). (Contributed by Mario Carneiro, 19-Feb-2014) (Revised by AV, 18-Aug-2021) (New usage is discouraged.) (Proof modification is discouraged.)

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