Theorem 139prmALT 47600

Description: 139 is a prime number. In contrast to 139prm 17054, the proof of this theorem uses 3dvds2dec 16263 for checking the divisibility by 3. Although the proof using 3dvds2dec 16263 is longer (regarding size: 1849 characters compared with 1809 for 139prm 17054), the number of essential steps is smaller (301 compared with 327 for 139prm 17054). (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 12419	. . . 4 ⊢ 1 ∈ ℕ0
2		3nn0 12421	. . . 4 ⊢ 3 ∈ ℕ0
3	1, 2	deccl 12625	. . 3 ⊢ ;13 ∈ ℕ0
4		9nn 12245	. . 3 ⊢ 9 ∈ ℕ
5	3, 4	decnncl 12630	. 2 ⊢ ;;139 ∈ ℕ
6		8nn0 12426	. . 3 ⊢ 8 ∈ ℕ0
7		4nn0 12422	. . 3 ⊢ 4 ∈ ℕ0
8		9nn0 12427	. . 3 ⊢ 9 ∈ ℕ0
9		1lt8 12340	. . 3 ⊢ 1 < 8
10		3lt10 12747	. . 3 ⊢ 3 < ;10
11		9lt10 12741	. . 3 ⊢ 9 < ;10
12	1, 6, 2, 7, 8, 1, 9, 10, 11	3decltc 12643	. 2 ⊢ ;;139 < ;;841
13		3nn 12226	. . . 4 ⊢ 3 ∈ ℕ
14	1, 13	decnncl 12630	. . 3 ⊢ ;13 ∈ ℕ
15		1lt10 12749	. . 3 ⊢ 1 < ;10
16	14, 8, 1, 15	declti 12648	. 2 ⊢ 1 < ;;139
17		4t2e8 12310	. . 3 ⊢ (4 · 2) = 8
18		df-9 12217	. . 3 ⊢ 9 = (8 + 1)
19	3, 7, 17, 18	dec2dvds 16994	. 2 ⊢ ¬ 2 ∥ ;;139
20		3ndvds4 47599	. . . 4 ⊢ ¬ 3 ∥ 4
21	1, 2	3dvdsdec 16262	. . . . 5 ⊢ (3 ∥ ;13 ↔ 3 ∥ (1 + 3))
22		3cn 12228	. . . . . . 7 ⊢ 3 ∈ ℂ
23		ax-1cn 11086	. . . . . . 7 ⊢ 1 ∈ ℂ
24		3p1e4 12287	. . . . . . 7 ⊢ (3 + 1) = 4
25	22, 23, 24	addcomli 11327	. . . . . 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 16263	. . . 4 ⊢ (3 ∥ ;;139 ↔ 3 ∥ ((1 + 3) + 9))
30	25	oveq1i 7363	. . . . . 6 ⊢ ((1 + 3) + 9) = (4 + 9)
31		9cn 12247	. . . . . . 7 ⊢ 9 ∈ ℂ
32		4cn 12232	. . . . . . 7 ⊢ 4 ∈ ℂ
33		9p4e13 12699	. . . . . . 7 ⊢ (9 + 4) = ;13
34	31, 32, 33	addcomli 11327	. . . . . 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 12230	. . 3 ⊢ 4 ∈ ℕ
40		4lt5 12319	. . 3 ⊢ 4 < 5
41		5p4e9 12300	. . 3 ⊢ (5 + 4) = 9
42	3, 39, 40, 41	dec5dvds2 16996	. 2 ⊢ ¬ 5 ∥ ;;139
43		7nn 12239	. . 3 ⊢ 7 ∈ ℕ
44	1, 8	deccl 12625	. . 3 ⊢ ;19 ∈ ℕ0
45		6nn 12236	. . 3 ⊢ 6 ∈ ℕ
46		0nn0 12418	. . . 4 ⊢ 0 ∈ ℕ0
47		6nn0 12424	. . . 4 ⊢ 6 ∈ ℕ0
48		eqid 2729	. . . 4 ⊢ ;19 = ;19
49	47	dec0h 12632	. . . 4 ⊢ 6 = ;06
50		7nn0 12425	. . . 4 ⊢ 7 ∈ ℕ0
51		7cn 12241	. . . . . . 7 ⊢ 7 ∈ ℂ
52	51	mulridi 11138	. . . . . 6 ⊢ (7 · 1) = 7
53		6cn 12238	. . . . . . 7 ⊢ 6 ∈ ℂ
54	53	addlidi 11323	. . . . . 6 ⊢ (0 + 6) = 6
55	52, 54	oveq12i 7365	. . . . 5 ⊢ ((7 · 1) + (0 + 6)) = (7 + 6)
56		7p6e13 12688	. . . . 5 ⊢ (7 + 6) = ;13
57	55, 56	eqtri 2752	. . . 4 ⊢ ((7 · 1) + (0 + 6)) = ;13
58		9t7e63 12737	. . . . . 6 ⊢ (9 · 7) = ;63
59	31, 51, 58	mulcomli 11143	. . . . 5 ⊢ (7 · 9) = ;63
60		6p3e9 12302	. . . . . 6 ⊢ (6 + 3) = 9
61	53, 22, 60	addcomli 11327	. . . . 5 ⊢ (3 + 6) = 9
62	47, 2, 47, 59, 61	decaddi 12670	. . . 4 ⊢ ((7 · 9) + 6) = ;69
63	1, 8, 46, 47, 48, 49, 50, 8, 47, 57, 62	decma2c 12663	. . 3 ⊢ ((7 · ;19) + 6) = ;;139
64		6lt7 12328	. . 3 ⊢ 6 < 7
65	43, 44, 45, 63, 64	ndvdsi 16342	. 2 ⊢ ¬ 7 ∥ ;;139
66		1nn 12158	. . . 4 ⊢ 1 ∈ ℕ
67	1, 66	decnncl 12630	. . 3 ⊢ ;11 ∈ ℕ
68		2nn0 12420	. . . 4 ⊢ 2 ∈ ℕ0
69	1, 68	deccl 12625	. . 3 ⊢ ;12 ∈ ℕ0
70		eqid 2729	. . . 4 ⊢ ;12 = ;12
71	50	dec0h 12632	. . . 4 ⊢ 7 = ;07
72	1, 1	deccl 12625	. . . 4 ⊢ ;11 ∈ ℕ0
73		2cn 12222	. . . . . . 7 ⊢ 2 ∈ ℂ
74	73	addlidi 11323	. . . . . 6 ⊢ (0 + 2) = 2
75	74	oveq2i 7364	. . . . 5 ⊢ ((;11 · 1) + (0 + 2)) = ((;11 · 1) + 2)
76	67	nncni 12157	. . . . . . 7 ⊢ ;11 ∈ ℂ
77	76	mulridi 11138	. . . . . 6 ⊢ (;11 · 1) = ;11
78		1p2e3 12285	. . . . . 6 ⊢ (1 + 2) = 3
79	1, 1, 68, 77, 78	decaddi 12670	. . . . 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 11310	. . . . . . 7 ⊢ (0 + 0) = 0
84	82, 83	oveq12i 7365	. . . . . 6 ⊢ ((1 · 2) + (0 + 0)) = (2 + 0)
85	73	addridi 11322	. . . . . 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 12303	. . . . . . 7 ⊢ (7 + 2) = 9
89	51, 73, 88	addcomli 11327	. . . . . 6 ⊢ (2 + 7) = 9
90	8	dec0h 12632	. . . . . 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 12662	. . . 4 ⊢ ((;11 · 2) + 7) = ;29
93	1, 68, 46, 50, 70, 71, 72, 8, 68, 80, 92	decma2c 12663	. . 3 ⊢ ((;11 · ;12) + 7) = ;;139
94		7lt10 12743	. . . 4 ⊢ 7 < ;10
95	66, 1, 50, 94	declti 12648	. . 3 ⊢ 7 < ;11
96	67, 69, 43, 93, 95	ndvdsi 16342	. 2 ⊢ ¬ ;11 ∥ ;;139
97	1, 46	deccl 12625	. . 3 ⊢ ;10 ∈ ℕ0
98		eqid 2729	. . . 4 ⊢ ;10 = ;10
99	3	nn0cni 12415	. . . . . . 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 11322	. . . . 5 ⊢ (;13 + 0) = ;13
103	101, 102	eqtri 2752	. . . 4 ⊢ ((;13 · 1) + (0 + 0)) = ;13
104	99	mul01i 11325	. . . . . 6 ⊢ (;13 · 0) = 0
105	104	oveq1i 7363	. . . . 5 ⊢ ((;13 · 0) + 9) = (0 + 9)
106	31	addlidi 11323	. . . . 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 12663	. . 3 ⊢ ((;13 · ;10) + 9) = ;;139
109	66, 2, 8, 11	declti 12648	. . 3 ⊢ 9 < ;13
110	14, 97, 4, 108, 109	ndvdsi 16342	. 2 ⊢ ¬ ;13 ∥ ;;139
111	1, 43	decnncl 12630	. . 3 ⊢ ;17 ∈ ℕ
112		eqid 2729	. . . 4 ⊢ ;17 = ;17
113	2	dec0h 12632	. . . 4 ⊢ 3 = ;03
114		5nn0 12423	. . . 4 ⊢ 5 ∈ ℕ0
115		8cn 12244	. . . . . . 7 ⊢ 8 ∈ ℂ
116	115	mullidi 11139	. . . . . 6 ⊢ (1 · 8) = 8
117		5cn 12235	. . . . . . 7 ⊢ 5 ∈ ℂ
118	117	addlidi 11323	. . . . . 6 ⊢ (0 + 5) = 5
119	116, 118	oveq12i 7365	. . . . 5 ⊢ ((1 · 8) + (0 + 5)) = (8 + 5)
120		8p5e13 12693	. . . . 5 ⊢ (8 + 5) = ;13
121	119, 120	eqtri 2752	. . . 4 ⊢ ((1 · 8) + (0 + 5)) = ;13
122		8t7e56 12730	. . . . . 6 ⊢ (8 · 7) = ;56
123	115, 51, 122	mulcomli 11143	. . . . 5 ⊢ (7 · 8) = ;56
124	114, 47, 2, 123, 60	decaddi 12670	. . . 4 ⊢ ((7 · 8) + 3) = ;59
125	1, 50, 46, 2, 112, 113, 6, 8, 114, 121, 124	decmac 12662	. . 3 ⊢ ((;17 · 8) + 3) = ;;139
126	66, 50, 2, 10	declti 12648	. . 3 ⊢ 3 < ;17
127	111, 6, 13, 125, 126	ndvdsi 16342	. 2 ⊢ ¬ ;17 ∥ ;;139
128	1, 4	decnncl 12630	. . 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 12670	. . . 4 ⊢ ((9 · 7) + 6) = ;69
133	1, 8, 46, 47, 48, 49, 50, 8, 47, 131, 132	decmac 12662	. . 3 ⊢ ((;19 · 7) + 6) = ;;139
134		6lt10 12744	. . . 4 ⊢ 6 < ;10
135	66, 8, 47, 134	declti 12648	. . 3 ⊢ 6 < ;19
136	128, 50, 45, 133, 135	ndvdsi 16342	. 2 ⊢ ¬ ;19 ∥ ;;139
137	68, 13	decnncl 12630	. . 3 ⊢ ;23 ∈ ℕ
138		eqid 2729	. . . 4 ⊢ ;23 = ;23
139		2p1e3 12284	. . . . 5 ⊢ (2 + 1) = 3
140		6t2e12 12714	. . . . . 6 ⊢ (6 · 2) = ;12
141	53, 73, 140	mulcomli 11143	. . . . 5 ⊢ (2 · 6) = ;12
142	1, 68, 139, 141	decsuc 12641	. . . 4 ⊢ ((2 · 6) + 1) = ;13
143		8p1e9 12292	. . . . 5 ⊢ (8 + 1) = 9
144		6t3e18 12715	. . . . . 6 ⊢ (6 · 3) = ;18
145	53, 22, 144	mulcomli 11143	. . . . 5 ⊢ (3 · 6) = ;18
146	1, 6, 143, 145	decsuc 12641	. . . 4 ⊢ ((3 · 6) + 1) = ;19
147	68, 2, 1, 138, 47, 8, 1, 142, 146	decrmac 12668	. . 3 ⊢ ((;23 · 6) + 1) = ;;139
148		2nn 12220	. . . 4 ⊢ 2 ∈ ℕ
149	148, 2, 1, 15	declti 12648	. . 3 ⊢ 1 < ;23
150	137, 47, 66, 147, 149	ndvdsi 16342	. 2 ⊢ ¬ ;23 ∥ ;;139
151	5, 12, 16, 19, 38, 42, 65, 96, 110, 127, 136, 150	prmlem2 17050	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 12202  3c3 12203  4c4 12204  5c5 12205  6c6 12206  7c7 12207  8c8 12208  9c9 12209  ;cdc 12610   ∥ cdvds 16182  ℙcprime 16601

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 11368  df-neg 11369  df-div 11797  df-nn 12148  df-2 12210  df-3 12211  df-4 12212  df-5 12213  df-6 12214  df-7 12215  df-8 12216  df-9 12217  df-n0 12404  df-z 12491  df-dec 12611  df-uz 12755  df-rp 12913  df-fz 13430  df-seq 13928  df-exp 13988  df-cj 15025  df-re 15026  df-im 15027  df-sqrt 15161  df-abs 15162  df-dvds 16183  df-prm 16602

This theorem is referenced by: (None)