Theorem 139prmALT 47584

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

Assertion

Ref	Expression
139prmALT	⊢ ;;139 ∈ ℙ

Proof of Theorem 139prmALT

Step	Hyp	Ref	Expression
1		1nn0 12418	. . . 4 ⊢ 1 ∈ ℕ0
2		3nn0 12420	. . . 4 ⊢ 3 ∈ ℕ0
3	1, 2	deccl 12624	. . 3 ⊢ ;13 ∈ ℕ0
4		9nn 12244	. . 3 ⊢ 9 ∈ ℕ
5	3, 4	decnncl 12629	. 2 ⊢ ;;139 ∈ ℕ
6		8nn0 12425	. . 3 ⊢ 8 ∈ ℕ0
7		4nn0 12421	. . 3 ⊢ 4 ∈ ℕ0
8		9nn0 12426	. . 3 ⊢ 9 ∈ ℕ0
9		1lt8 12339	. . 3 ⊢ 1 < 8
10		3lt10 12746	. . 3 ⊢ 3 < ;10
11		9lt10 12740	. . 3 ⊢ 9 < ;10
12	1, 6, 2, 7, 8, 1, 9, 10, 11	3decltc 12642	. 2 ⊢ ;;139 < ;;841
13		3nn 12225	. . . 4 ⊢ 3 ∈ ℕ
14	1, 13	decnncl 12629	. . 3 ⊢ ;13 ∈ ℕ
15		1lt10 12748	. . 3 ⊢ 1 < ;10
16	14, 8, 1, 15	declti 12647	. 2 ⊢ 1 < ;;139
17		4t2e8 12309	. . 3 ⊢ (4 · 2) = 8
18		df-9 12216	. . 3 ⊢ 9 = (8 + 1)
19	3, 7, 17, 18	dec2dvds 16993	. 2 ⊢ ¬ 2 ∥ ;;139
20		3ndvds4 47583	. . . 4 ⊢ ¬ 3 ∥ 4
21	1, 2	3dvdsdec 16261	. . . . 5 ⊢ (3 ∥ ;13 ↔ 3 ∥ (1 + 3))
22		3cn 12227	. . . . . . 7 ⊢ 3 ∈ ℂ
23		ax-1cn 11086	. . . . . . 7 ⊢ 1 ∈ ℂ
24		3p1e4 12286	. . . . . . 7 ⊢ (3 + 1) = 4
25	22, 23, 24	addcomli 11326	. . . . . 6 ⊢ (1 + 3) = 4
26	25	breq2i 5103	. . . . 5 ⊢ (3 ∥ (1 + 3) ↔ 3 ∥ 4)
27	21, 26	bitri 275	. . . 4 ⊢ (3 ∥ ;13 ↔ 3 ∥ 4)
28	20, 27	mtbir 323	. . 3 ⊢ ¬ 3 ∥ ;13
29	1, 2, 8	3dvds2dec 16262	. . . 4 ⊢ (3 ∥ ;;139 ↔ 3 ∥ ((1 + 3) + 9))
30	25	oveq1i 7363	. . . . . 6 ⊢ ((1 + 3) + 9) = (4 + 9)
31		9cn 12246	. . . . . . 7 ⊢ 9 ∈ ℂ
32		4cn 12231	. . . . . . 7 ⊢ 4 ∈ ℂ
33		9p4e13 12698	. . . . . . 7 ⊢ (9 + 4) = ;13
34	31, 32, 33	addcomli 11326	. . . . . 6 ⊢ (4 + 9) = ;13
35	30, 34	eqtri 2752	. . . . 5 ⊢ ((1 + 3) + 9) = ;13
36	35	breq2i 5103	. . . 4 ⊢ (3 ∥ ((1 + 3) + 9) ↔ 3 ∥ ;13)
37	29, 36	bitri 275	. . 3 ⊢ (3 ∥ ;;139 ↔ 3 ∥ ;13)
38	28, 37	mtbir 323	. 2 ⊢ ¬ 3 ∥ ;;139
39		4nn 12229	. . 3 ⊢ 4 ∈ ℕ
40		4lt5 12318	. . 3 ⊢ 4 < 5
41		5p4e9 12299	. . 3 ⊢ (5 + 4) = 9
42	3, 39, 40, 41	dec5dvds2 16995	. 2 ⊢ ¬ 5 ∥ ;;139
43		7nn 12238	. . 3 ⊢ 7 ∈ ℕ
44	1, 8	deccl 12624	. . 3 ⊢ ;19 ∈ ℕ0
45		6nn 12235	. . 3 ⊢ 6 ∈ ℕ
46		0nn0 12417	. . . 4 ⊢ 0 ∈ ℕ0
47		6nn0 12423	. . . 4 ⊢ 6 ∈ ℕ0
48		eqid 2729	. . . 4 ⊢ ;19 = ;19
49	47	dec0h 12631	. . . 4 ⊢ 6 = ;06
50		7nn0 12424	. . . 4 ⊢ 7 ∈ ℕ0
51		7cn 12240	. . . . . . 7 ⊢ 7 ∈ ℂ
52	51	mulridi 11138	. . . . . 6 ⊢ (7 · 1) = 7
53		6cn 12237	. . . . . . 7 ⊢ 6 ∈ ℂ
54	53	addlidi 11322	. . . . . 6 ⊢ (0 + 6) = 6
55	52, 54	oveq12i 7365	. . . . 5 ⊢ ((7 · 1) + (0 + 6)) = (7 + 6)
56		7p6e13 12687	. . . . 5 ⊢ (7 + 6) = ;13
57	55, 56	eqtri 2752	. . . 4 ⊢ ((7 · 1) + (0 + 6)) = ;13
58		9t7e63 12736	. . . . . 6 ⊢ (9 · 7) = ;63
59	31, 51, 58	mulcomli 11143	. . . . 5 ⊢ (7 · 9) = ;63
60		6p3e9 12301	. . . . . 6 ⊢ (6 + 3) = 9
61	53, 22, 60	addcomli 11326	. . . . 5 ⊢ (3 + 6) = 9
62	47, 2, 47, 59, 61	decaddi 12669	. . . 4 ⊢ ((7 · 9) + 6) = ;69
63	1, 8, 46, 47, 48, 49, 50, 8, 47, 57, 62	decma2c 12662	. . 3 ⊢ ((7 · ;19) + 6) = ;;139
64		6lt7 12327	. . 3 ⊢ 6 < 7
65	43, 44, 45, 63, 64	ndvdsi 16341	. 2 ⊢ ¬ 7 ∥ ;;139
66		1nn 12157	. . . 4 ⊢ 1 ∈ ℕ
67	1, 66	decnncl 12629	. . 3 ⊢ ;11 ∈ ℕ
68		2nn0 12419	. . . 4 ⊢ 2 ∈ ℕ0
69	1, 68	deccl 12624	. . 3 ⊢ ;12 ∈ ℕ0
70		eqid 2729	. . . 4 ⊢ ;12 = ;12
71	50	dec0h 12631	. . . 4 ⊢ 7 = ;07
72	1, 1	deccl 12624	. . . 4 ⊢ ;11 ∈ ℕ0
73		2cn 12221	. . . . . . 7 ⊢ 2 ∈ ℂ
74	73	addlidi 11322	. . . . . 6 ⊢ (0 + 2) = 2
75	74	oveq2i 7364	. . . . 5 ⊢ ((;11 · 1) + (0 + 2)) = ((;11 · 1) + 2)
76	67	nncni 12156	. . . . . . 7 ⊢ ;11 ∈ ℂ
77	76	mulridi 11138	. . . . . 6 ⊢ (;11 · 1) = ;11
78		1p2e3 12284	. . . . . 6 ⊢ (1 + 2) = 3
79	1, 1, 68, 77, 78	decaddi 12669	. . . . 5 ⊢ ((;11 · 1) + 2) = ;13
80	75, 79	eqtri 2752	. . . 4 ⊢ ((;11 · 1) + (0 + 2)) = ;13
81		eqid 2729	. . . . 5 ⊢ ;11 = ;11
82	73	mullidi 11139	. . . . . . 7 ⊢ (1 · 2) = 2
83		00id 11309	. . . . . . 7 ⊢ (0 + 0) = 0
84	82, 83	oveq12i 7365	. . . . . 6 ⊢ ((1 · 2) + (0 + 0)) = (2 + 0)
85	73	addridi 11321	. . . . . 6 ⊢ (2 + 0) = 2
86	84, 85	eqtri 2752	. . . . 5 ⊢ ((1 · 2) + (0 + 0)) = 2
87	82	oveq1i 7363	. . . . . 6 ⊢ ((1 · 2) + 7) = (2 + 7)
88		7p2e9 12302	. . . . . . 7 ⊢ (7 + 2) = 9
89	51, 73, 88	addcomli 11326	. . . . . 6 ⊢ (2 + 7) = 9
90	8	dec0h 12631	. . . . . 6 ⊢ 9 = ;09
91	87, 89, 90	3eqtri 2756	. . . . 5 ⊢ ((1 · 2) + 7) = ;09
92	1, 1, 46, 50, 81, 71, 68, 8, 46, 86, 91	decmac 12661	. . . 4 ⊢ ((;11 · 2) + 7) = ;29
93	1, 68, 46, 50, 70, 71, 72, 8, 68, 80, 92	decma2c 12662	. . 3 ⊢ ((;11 · ;12) + 7) = ;;139
94		7lt10 12742	. . . 4 ⊢ 7 < ;10
95	66, 1, 50, 94	declti 12647	. . 3 ⊢ 7 < ;11
96	67, 69, 43, 93, 95	ndvdsi 16341	. 2 ⊢ ¬ ;11 ∥ ;;139
97	1, 46	deccl 12624	. . 3 ⊢ ;10 ∈ ℕ0
98		eqid 2729	. . . 4 ⊢ ;10 = ;10
99	3	nn0cni 12414	. . . . . . 7 ⊢ ;13 ∈ ℂ
100	99	mulridi 11138	. . . . . 6 ⊢ (;13 · 1) = ;13
101	100, 83	oveq12i 7365	. . . . 5 ⊢ ((;13 · 1) + (0 + 0)) = (;13 + 0)
102	99	addridi 11321	. . . . 5 ⊢ (;13 + 0) = ;13
103	101, 102	eqtri 2752	. . . 4 ⊢ ((;13 · 1) + (0 + 0)) = ;13
104	99	mul01i 11324	. . . . . 6 ⊢ (;13 · 0) = 0
105	104	oveq1i 7363	. . . . 5 ⊢ ((;13 · 0) + 9) = (0 + 9)
106	31	addlidi 11322	. . . . 5 ⊢ (0 + 9) = 9
107	105, 106, 90	3eqtri 2756	. . . 4 ⊢ ((;13 · 0) + 9) = ;09
108	1, 46, 46, 8, 98, 90, 3, 8, 46, 103, 107	decma2c 12662	. . 3 ⊢ ((;13 · ;10) + 9) = ;;139
109	66, 2, 8, 11	declti 12647	. . 3 ⊢ 9 < ;13
110	14, 97, 4, 108, 109	ndvdsi 16341	. 2 ⊢ ¬ ;13 ∥ ;;139
111	1, 43	decnncl 12629	. . 3 ⊢ ;17 ∈ ℕ
112		eqid 2729	. . . 4 ⊢ ;17 = ;17
113	2	dec0h 12631	. . . 4 ⊢ 3 = ;03
114		5nn0 12422	. . . 4 ⊢ 5 ∈ ℕ0
115		8cn 12243	. . . . . . 7 ⊢ 8 ∈ ℂ
116	115	mullidi 11139	. . . . . 6 ⊢ (1 · 8) = 8
117		5cn 12234	. . . . . . 7 ⊢ 5 ∈ ℂ
118	117	addlidi 11322	. . . . . 6 ⊢ (0 + 5) = 5
119	116, 118	oveq12i 7365	. . . . 5 ⊢ ((1 · 8) + (0 + 5)) = (8 + 5)
120		8p5e13 12692	. . . . 5 ⊢ (8 + 5) = ;13
121	119, 120	eqtri 2752	. . . 4 ⊢ ((1 · 8) + (0 + 5)) = ;13
122		8t7e56 12729	. . . . . 6 ⊢ (8 · 7) = ;56
123	115, 51, 122	mulcomli 11143	. . . . 5 ⊢ (7 · 8) = ;56
124	114, 47, 2, 123, 60	decaddi 12669	. . . 4 ⊢ ((7 · 8) + 3) = ;59
125	1, 50, 46, 2, 112, 113, 6, 8, 114, 121, 124	decmac 12661	. . 3 ⊢ ((;17 · 8) + 3) = ;;139
126	66, 50, 2, 10	declti 12647	. . 3 ⊢ 3 < ;17
127	111, 6, 13, 125, 126	ndvdsi 16341	. 2 ⊢ ¬ ;17 ∥ ;;139
128	1, 4	decnncl 12629	. . 3 ⊢ ;19 ∈ ℕ
129	51	mullidi 11139	. . . . . 6 ⊢ (1 · 7) = 7
130	129, 54	oveq12i 7365	. . . . 5 ⊢ ((1 · 7) + (0 + 6)) = (7 + 6)
131	130, 56	eqtri 2752	. . . 4 ⊢ ((1 · 7) + (0 + 6)) = ;13
132	47, 2, 47, 58, 61	decaddi 12669	. . . 4 ⊢ ((9 · 7) + 6) = ;69
133	1, 8, 46, 47, 48, 49, 50, 8, 47, 131, 132	decmac 12661	. . 3 ⊢ ((;19 · 7) + 6) = ;;139
134		6lt10 12743	. . . 4 ⊢ 6 < ;10
135	66, 8, 47, 134	declti 12647	. . 3 ⊢ 6 < ;19
136	128, 50, 45, 133, 135	ndvdsi 16341	. 2 ⊢ ¬ ;19 ∥ ;;139
137	68, 13	decnncl 12629	. . 3 ⊢ ;23 ∈ ℕ
138		eqid 2729	. . . 4 ⊢ ;23 = ;23
139		2p1e3 12283	. . . . 5 ⊢ (2 + 1) = 3
140		6t2e12 12713	. . . . . 6 ⊢ (6 · 2) = ;12
141	53, 73, 140	mulcomli 11143	. . . . 5 ⊢ (2 · 6) = ;12
142	1, 68, 139, 141	decsuc 12640	. . . 4 ⊢ ((2 · 6) + 1) = ;13
143		8p1e9 12291	. . . . 5 ⊢ (8 + 1) = 9
144		6t3e18 12714	. . . . . 6 ⊢ (6 · 3) = ;18
145	53, 22, 144	mulcomli 11143	. . . . 5 ⊢ (3 · 6) = ;18
146	1, 6, 143, 145	decsuc 12640	. . . 4 ⊢ ((3 · 6) + 1) = ;19
147	68, 2, 1, 138, 47, 8, 1, 142, 146	decrmac 12667	. . 3 ⊢ ((;23 · 6) + 1) = ;;139
148		2nn 12219	. . . 4 ⊢ 2 ∈ ℕ
149	148, 2, 1, 15	declti 12647	. . 3 ⊢ 1 < ;23
150	137, 47, 66, 147, 149	ndvdsi 16341	. 2 ⊢ ¬ ;23 ∥ ;;139
151	5, 12, 16, 19, 38, 42, 65, 96, 110, 127, 136, 150	prmlem2 17049	1 ⊢ ;;139 ∈ ℙ

Syntax hints:   ∈ wcel 2109   class class class wbr 5095  (class class class)co 7353  0cc0 11028  1c1 11029   + caddc 11031   · cmul 11033  2c2 12201  3c3 12202  4c4 12203  5c5 12204  6c6 12205  7c7 12206  8c8 12207  9c9 12208  ;cdc 12609   ∥ cdvds 16181  ℙcprime 16600

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5238  ax-nul 5248  ax-pow 5307  ax-pr 5374  ax-un 7675  ax-cnex 11084  ax-resscn 11085  ax-1cn 11086  ax-icn 11087  ax-addcl 11088  ax-addrcl 11089  ax-mulcl 11090  ax-mulrcl 11091  ax-mulcom 11092  ax-addass 11093  ax-mulass 11094  ax-distr 11095  ax-i2m1 11096  ax-1ne0 11097  ax-1rid 11098  ax-rnegex 11099  ax-rrecex 11100  ax-cnre 11101  ax-pre-lttri 11102  ax-pre-lttrn 11103  ax-pre-ltadd 11104  ax-pre-mulgt0 11105  ax-pre-sup 11106

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-rmo 3345  df-reu 3346  df-rab 3397  df-v 3440  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-pss 3925  df-nul 4287  df-if 4479  df-pw 4555  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-iun 4946  df-br 5096  df-opab 5158  df-mpt 5177  df-tr 5203  df-id 5518  df-eprel 5523  df-po 5531  df-so 5532  df-fr 5576  df-we 5578  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-rn 5634  df-res 5635  df-ima 5636  df-pred 6253  df-ord 6314  df-on 6315  df-lim 6316  df-suc 6317  df-iota 6442  df-fun 6488  df-fn 6489  df-f 6490  df-f1 6491  df-fo 6492  df-f1o 6493  df-fv 6494  df-riota 7310  df-ov 7356  df-oprab 7357  df-mpo 7358  df-om 7807  df-1st 7931  df-2nd 7932  df-frecs 8221  df-wrecs 8252  df-recs 8301  df-rdg 8339  df-1o 8395  df-2o 8396  df-er 8632  df-en 8880  df-dom 8881  df-sdom 8882  df-fin 8883  df-sup 9351  df-inf 9352  df-pnf 11170  df-mnf 11171  df-xr 11172  df-ltxr 11173  df-le 11174  df-sub 11367  df-neg 11368  df-div 11796  df-nn 12147  df-2 12209  df-3 12210  df-4 12211  df-5 12212  df-6 12213  df-7 12214  df-8 12215  df-9 12216  df-n0 12403  df-z 12490  df-dec 12610  df-uz 12754  df-rp 12912  df-fz 13429  df-seq 13927  df-exp 13987  df-cj 15024  df-re 15025  df-im 15026  df-sqrt 15160  df-abs 15161  df-dvds 16182  df-prm 16601

This theorem is referenced by: (None)