Theorem 139prmALT 48071

Description: 139 is a prime number. In contrast to 139prm 17085, the proof of this theorem uses 3dvds2dec 16293 for checking the divisibility by 3. Although the proof using 3dvds2dec 16293 is longer (regarding size: 1849 characters compared with 1809 for 139prm 17085), the number of essential steps is smaller (301 compared with 327 for 139prm 17085). (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 12444	. . . 4 ⊢ 1 ∈ ℕ0
2		3nn0 12446	. . . 4 ⊢ 3 ∈ ℕ0
3	1, 2	deccl 12650	. . 3 ⊢ ;13 ∈ ℕ0
4		9nn 12270	. . 3 ⊢ 9 ∈ ℕ
5	3, 4	decnncl 12655	. 2 ⊢ ;;139 ∈ ℕ
6		8nn0 12451	. . 3 ⊢ 8 ∈ ℕ0
7		4nn0 12447	. . 3 ⊢ 4 ∈ ℕ0
8		9nn0 12452	. . 3 ⊢ 9 ∈ ℕ0
9		1lt8 12365	. . 3 ⊢ 1 < 8
10		3lt10 12772	. . 3 ⊢ 3 < ;10
11		9lt10 12766	. . 3 ⊢ 9 < ;10
12	1, 6, 2, 7, 8, 1, 9, 10, 11	3decltc 12668	. 2 ⊢ ;;139 < ;;841
13		3nn 12251	. . . 4 ⊢ 3 ∈ ℕ
14	1, 13	decnncl 12655	. . 3 ⊢ ;13 ∈ ℕ
15		1lt10 12774	. . 3 ⊢ 1 < ;10
16	14, 8, 1, 15	declti 12673	. 2 ⊢ 1 < ;;139
17		4t2e8 12335	. . 3 ⊢ (4 · 2) = 8
18		df-9 12242	. . 3 ⊢ 9 = (8 + 1)
19	3, 7, 17, 18	dec2dvds 17025	. 2 ⊢ ¬ 2 ∥ ;;139
20		3ndvds4 48070	. . . 4 ⊢ ¬ 3 ∥ 4
21	1, 2	3dvdsdec 16292	. . . . 5 ⊢ (3 ∥ ;13 ↔ 3 ∥ (1 + 3))
22		3cn 12253	. . . . . . 7 ⊢ 3 ∈ ℂ
23		ax-1cn 11087	. . . . . . 7 ⊢ 1 ∈ ℂ
24		3p1e4 12312	. . . . . . 7 ⊢ (3 + 1) = 4
25	22, 23, 24	addcomli 11329	. . . . . 6 ⊢ (1 + 3) = 4
26	25	breq2i 5094	. . . . 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 16293	. . . 4 ⊢ (3 ∥ ;;139 ↔ 3 ∥ ((1 + 3) + 9))
30	25	oveq1i 7370	. . . . . 6 ⊢ ((1 + 3) + 9) = (4 + 9)
31		9cn 12272	. . . . . . 7 ⊢ 9 ∈ ℂ
32		4cn 12257	. . . . . . 7 ⊢ 4 ∈ ℂ
33		9p4e13 12724	. . . . . . 7 ⊢ (9 + 4) = ;13
34	31, 32, 33	addcomli 11329	. . . . . 6 ⊢ (4 + 9) = ;13
35	30, 34	eqtri 2760	. . . . 5 ⊢ ((1 + 3) + 9) = ;13
36	35	breq2i 5094	. . . 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 12255	. . 3 ⊢ 4 ∈ ℕ
40		4lt5 12344	. . 3 ⊢ 4 < 5
41		5p4e9 12325	. . 3 ⊢ (5 + 4) = 9
42	3, 39, 40, 41	dec5dvds2 17027	. 2 ⊢ ¬ 5 ∥ ;;139
43		7nn 12264	. . 3 ⊢ 7 ∈ ℕ
44	1, 8	deccl 12650	. . 3 ⊢ ;19 ∈ ℕ0
45		6nn 12261	. . 3 ⊢ 6 ∈ ℕ
46		0nn0 12443	. . . 4 ⊢ 0 ∈ ℕ0
47		6nn0 12449	. . . 4 ⊢ 6 ∈ ℕ0
48		eqid 2737	. . . 4 ⊢ ;19 = ;19
49	47	dec0h 12657	. . . 4 ⊢ 6 = ;06
50		7nn0 12450	. . . 4 ⊢ 7 ∈ ℕ0
51		7cn 12266	. . . . . . 7 ⊢ 7 ∈ ℂ
52	51	mulridi 11140	. . . . . 6 ⊢ (7 · 1) = 7
53		6cn 12263	. . . . . . 7 ⊢ 6 ∈ ℂ
54	53	addlidi 11325	. . . . . 6 ⊢ (0 + 6) = 6
55	52, 54	oveq12i 7372	. . . . 5 ⊢ ((7 · 1) + (0 + 6)) = (7 + 6)
56		7p6e13 12713	. . . . 5 ⊢ (7 + 6) = ;13
57	55, 56	eqtri 2760	. . . 4 ⊢ ((7 · 1) + (0 + 6)) = ;13
58		9t7e63 12762	. . . . . 6 ⊢ (9 · 7) = ;63
59	31, 51, 58	mulcomli 11145	. . . . 5 ⊢ (7 · 9) = ;63
60		6p3e9 12327	. . . . . 6 ⊢ (6 + 3) = 9
61	53, 22, 60	addcomli 11329	. . . . 5 ⊢ (3 + 6) = 9
62	47, 2, 47, 59, 61	decaddi 12695	. . . 4 ⊢ ((7 · 9) + 6) = ;69
63	1, 8, 46, 47, 48, 49, 50, 8, 47, 57, 62	decma2c 12688	. . 3 ⊢ ((7 · ;19) + 6) = ;;139
64		6lt7 12353	. . 3 ⊢ 6 < 7
65	43, 44, 45, 63, 64	ndvdsi 16372	. 2 ⊢ ¬ 7 ∥ ;;139
66		1nn 12176	. . . 4 ⊢ 1 ∈ ℕ
67	1, 66	decnncl 12655	. . 3 ⊢ ;11 ∈ ℕ
68		2nn0 12445	. . . 4 ⊢ 2 ∈ ℕ0
69	1, 68	deccl 12650	. . 3 ⊢ ;12 ∈ ℕ0
70		eqid 2737	. . . 4 ⊢ ;12 = ;12
71	50	dec0h 12657	. . . 4 ⊢ 7 = ;07
72	1, 1	deccl 12650	. . . 4 ⊢ ;11 ∈ ℕ0
73		2cn 12247	. . . . . . 7 ⊢ 2 ∈ ℂ
74	73	addlidi 11325	. . . . . 6 ⊢ (0 + 2) = 2
75	74	oveq2i 7371	. . . . 5 ⊢ ((;11 · 1) + (0 + 2)) = ((;11 · 1) + 2)
76	67	nncni 12175	. . . . . . 7 ⊢ ;11 ∈ ℂ
77	76	mulridi 11140	. . . . . 6 ⊢ (;11 · 1) = ;11
78		1p2e3 12310	. . . . . 6 ⊢ (1 + 2) = 3
79	1, 1, 68, 77, 78	decaddi 12695	. . . . 5 ⊢ ((;11 · 1) + 2) = ;13
80	75, 79	eqtri 2760	. . . 4 ⊢ ((;11 · 1) + (0 + 2)) = ;13
81		eqid 2737	. . . . 5 ⊢ ;11 = ;11
82	73	mullidi 11141	. . . . . . 7 ⊢ (1 · 2) = 2
83		00id 11312	. . . . . . 7 ⊢ (0 + 0) = 0
84	82, 83	oveq12i 7372	. . . . . 6 ⊢ ((1 · 2) + (0 + 0)) = (2 + 0)
85	73	addridi 11324	. . . . . 6 ⊢ (2 + 0) = 2
86	84, 85	eqtri 2760	. . . . 5 ⊢ ((1 · 2) + (0 + 0)) = 2
87	82	oveq1i 7370	. . . . . 6 ⊢ ((1 · 2) + 7) = (2 + 7)
88		7p2e9 12328	. . . . . . 7 ⊢ (7 + 2) = 9
89	51, 73, 88	addcomli 11329	. . . . . 6 ⊢ (2 + 7) = 9
90	8	dec0h 12657	. . . . . 6 ⊢ 9 = ;09
91	87, 89, 90	3eqtri 2764	. . . . 5 ⊢ ((1 · 2) + 7) = ;09
92	1, 1, 46, 50, 81, 71, 68, 8, 46, 86, 91	decmac 12687	. . . 4 ⊢ ((;11 · 2) + 7) = ;29
93	1, 68, 46, 50, 70, 71, 72, 8, 68, 80, 92	decma2c 12688	. . 3 ⊢ ((;11 · ;12) + 7) = ;;139
94		7lt10 12768	. . . 4 ⊢ 7 < ;10
95	66, 1, 50, 94	declti 12673	. . 3 ⊢ 7 < ;11
96	67, 69, 43, 93, 95	ndvdsi 16372	. 2 ⊢ ¬ ;11 ∥ ;;139
97	1, 46	deccl 12650	. . 3 ⊢ ;10 ∈ ℕ0
98		eqid 2737	. . . 4 ⊢ ;10 = ;10
99	3	nn0cni 12440	. . . . . . 7 ⊢ ;13 ∈ ℂ
100	99	mulridi 11140	. . . . . 6 ⊢ (;13 · 1) = ;13
101	100, 83	oveq12i 7372	. . . . 5 ⊢ ((;13 · 1) + (0 + 0)) = (;13 + 0)
102	99	addridi 11324	. . . . 5 ⊢ (;13 + 0) = ;13
103	101, 102	eqtri 2760	. . . 4 ⊢ ((;13 · 1) + (0 + 0)) = ;13
104	99	mul01i 11327	. . . . . 6 ⊢ (;13 · 0) = 0
105	104	oveq1i 7370	. . . . 5 ⊢ ((;13 · 0) + 9) = (0 + 9)
106	31	addlidi 11325	. . . . 5 ⊢ (0 + 9) = 9
107	105, 106, 90	3eqtri 2764	. . . 4 ⊢ ((;13 · 0) + 9) = ;09
108	1, 46, 46, 8, 98, 90, 3, 8, 46, 103, 107	decma2c 12688	. . 3 ⊢ ((;13 · ;10) + 9) = ;;139
109	66, 2, 8, 11	declti 12673	. . 3 ⊢ 9 < ;13
110	14, 97, 4, 108, 109	ndvdsi 16372	. 2 ⊢ ¬ ;13 ∥ ;;139
111	1, 43	decnncl 12655	. . 3 ⊢ ;17 ∈ ℕ
112		eqid 2737	. . . 4 ⊢ ;17 = ;17
113	2	dec0h 12657	. . . 4 ⊢ 3 = ;03
114		5nn0 12448	. . . 4 ⊢ 5 ∈ ℕ0
115		8cn 12269	. . . . . . 7 ⊢ 8 ∈ ℂ
116	115	mullidi 11141	. . . . . 6 ⊢ (1 · 8) = 8
117		5cn 12260	. . . . . . 7 ⊢ 5 ∈ ℂ
118	117	addlidi 11325	. . . . . 6 ⊢ (0 + 5) = 5
119	116, 118	oveq12i 7372	. . . . 5 ⊢ ((1 · 8) + (0 + 5)) = (8 + 5)
120		8p5e13 12718	. . . . 5 ⊢ (8 + 5) = ;13
121	119, 120	eqtri 2760	. . . 4 ⊢ ((1 · 8) + (0 + 5)) = ;13
122		8t7e56 12755	. . . . . 6 ⊢ (8 · 7) = ;56
123	115, 51, 122	mulcomli 11145	. . . . 5 ⊢ (7 · 8) = ;56
124	114, 47, 2, 123, 60	decaddi 12695	. . . 4 ⊢ ((7 · 8) + 3) = ;59
125	1, 50, 46, 2, 112, 113, 6, 8, 114, 121, 124	decmac 12687	. . 3 ⊢ ((;17 · 8) + 3) = ;;139
126	66, 50, 2, 10	declti 12673	. . 3 ⊢ 3 < ;17
127	111, 6, 13, 125, 126	ndvdsi 16372	. 2 ⊢ ¬ ;17 ∥ ;;139
128	1, 4	decnncl 12655	. . 3 ⊢ ;19 ∈ ℕ
129	51	mullidi 11141	. . . . . 6 ⊢ (1 · 7) = 7
130	129, 54	oveq12i 7372	. . . . 5 ⊢ ((1 · 7) + (0 + 6)) = (7 + 6)
131	130, 56	eqtri 2760	. . . 4 ⊢ ((1 · 7) + (0 + 6)) = ;13
132	47, 2, 47, 58, 61	decaddi 12695	. . . 4 ⊢ ((9 · 7) + 6) = ;69
133	1, 8, 46, 47, 48, 49, 50, 8, 47, 131, 132	decmac 12687	. . 3 ⊢ ((;19 · 7) + 6) = ;;139
134		6lt10 12769	. . . 4 ⊢ 6 < ;10
135	66, 8, 47, 134	declti 12673	. . 3 ⊢ 6 < ;19
136	128, 50, 45, 133, 135	ndvdsi 16372	. 2 ⊢ ¬ ;19 ∥ ;;139
137	68, 13	decnncl 12655	. . 3 ⊢ ;23 ∈ ℕ
138		eqid 2737	. . . 4 ⊢ ;23 = ;23
139		2p1e3 12309	. . . . 5 ⊢ (2 + 1) = 3
140		6t2e12 12739	. . . . . 6 ⊢ (6 · 2) = ;12
141	53, 73, 140	mulcomli 11145	. . . . 5 ⊢ (2 · 6) = ;12
142	1, 68, 139, 141	decsuc 12666	. . . 4 ⊢ ((2 · 6) + 1) = ;13
143		8p1e9 12317	. . . . 5 ⊢ (8 + 1) = 9
144		6t3e18 12740	. . . . . 6 ⊢ (6 · 3) = ;18
145	53, 22, 144	mulcomli 11145	. . . . 5 ⊢ (3 · 6) = ;18
146	1, 6, 143, 145	decsuc 12666	. . . 4 ⊢ ((3 · 6) + 1) = ;19
147	68, 2, 1, 138, 47, 8, 1, 142, 146	decrmac 12693	. . 3 ⊢ ((;23 · 6) + 1) = ;;139
148		2nn 12245	. . . 4 ⊢ 2 ∈ ℕ
149	148, 2, 1, 15	declti 12673	. . 3 ⊢ 1 < ;23
150	137, 47, 66, 147, 149	ndvdsi 16372	. 2 ⊢ ¬ ;23 ∥ ;;139
151	5, 12, 16, 19, 38, 42, 65, 96, 110, 127, 136, 150	prmlem2 17081	1 ⊢ ;;139 ∈ ℙ

Syntax hints:   ∈ wcel 2114   class class class wbr 5086  (class class class)co 7360  0cc0 11029  1c1 11030   + caddc 11032   · cmul 11034  2c2 12227  3c3 12228  4c4 12229  5c5 12230  6c6 12231  7c7 12232  8c8 12233  9c9 12234  ;cdc 12635   ∥ cdvds 16212  ℙcprime 16631

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5231  ax-nul 5241  ax-pow 5302  ax-pr 5370  ax-un 7682  ax-cnex 11085  ax-resscn 11086  ax-1cn 11087  ax-icn 11088  ax-addcl 11089  ax-addrcl 11090  ax-mulcl 11091  ax-mulrcl 11092  ax-mulcom 11093  ax-addass 11094  ax-mulass 11095  ax-distr 11096  ax-i2m1 11097  ax-1ne0 11098  ax-1rid 11099  ax-rnegex 11100  ax-rrecex 11101  ax-cnre 11102  ax-pre-lttri 11103  ax-pre-lttrn 11104  ax-pre-ltadd 11105  ax-pre-mulgt0 11106  ax-pre-sup 11107

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-rmo 3343  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-iun 4936  df-br 5087  df-opab 5149  df-mpt 5168  df-tr 5194  df-id 5519  df-eprel 5524  df-po 5532  df-so 5533  df-fr 5577  df-we 5579  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-pred 6259  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-riota 7317  df-ov 7363  df-oprab 7364  df-mpo 7365  df-om 7811  df-1st 7935  df-2nd 7936  df-frecs 8224  df-wrecs 8255  df-recs 8304  df-rdg 8342  df-1o 8398  df-2o 8399  df-er 8636  df-en 8887  df-dom 8888  df-sdom 8889  df-fin 8890  df-sup 9348  df-inf 9349  df-pnf 11172  df-mnf 11173  df-xr 11174  df-ltxr 11175  df-le 11176  df-sub 11370  df-neg 11371  df-div 11799  df-nn 12166  df-2 12235  df-3 12236  df-4 12237  df-5 12238  df-6 12239  df-7 12240  df-8 12241  df-9 12242  df-n0 12429  df-z 12516  df-dec 12636  df-uz 12780  df-rp 12934  df-fz 13453  df-seq 13955  df-exp 14015  df-cj 15052  df-re 15053  df-im 15054  df-sqrt 15188  df-abs 15189  df-dvds 16213  df-prm 16632

This theorem is referenced by: (None)