Theorem 139prmALT 43844

Description: 139 is a prime number. In contrast to 139prm 16440, the proof of this theorem uses 3dvds2dec 15667 for checking the divisibility by 3. Although the proof using 3dvds2dec 15667 is longer (regarding size: 1849 characters compared with 1809 for 139prm 16440), the number of essential steps is smaller (301 compared with 327 for 139prm 16440). (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 11900	. . . 4 ⊢ 1 ∈ ℕ0
2		3nn0 11902	. . . 4 ⊢ 3 ∈ ℕ0
3	1, 2	deccl 12100	. . 3 ⊢ ;13 ∈ ℕ0
4		9nn 11722	. . 3 ⊢ 9 ∈ ℕ
5	3, 4	decnncl 12105	. 2 ⊢ ;;139 ∈ ℕ
6		8nn0 11907	. . 3 ⊢ 8 ∈ ℕ0
7		4nn0 11903	. . 3 ⊢ 4 ∈ ℕ0
8		9nn0 11908	. . 3 ⊢ 9 ∈ ℕ0
9		1lt8 11822	. . 3 ⊢ 1 < 8
10		3lt10 12222	. . 3 ⊢ 3 < ;10
11		9lt10 12216	. . 3 ⊢ 9 < ;10
12	1, 6, 2, 7, 8, 1, 9, 10, 11	3decltc 12118	. 2 ⊢ ;;139 < ;;841
13		3nn 11703	. . . 4 ⊢ 3 ∈ ℕ
14	1, 13	decnncl 12105	. . 3 ⊢ ;13 ∈ ℕ
15		1lt10 12224	. . 3 ⊢ 1 < ;10
16	14, 8, 1, 15	declti 12123	. 2 ⊢ 1 < ;;139
17		4t2e8 11792	. . 3 ⊢ (4 · 2) = 8
18		df-9 11694	. . 3 ⊢ 9 = (8 + 1)
19	3, 7, 17, 18	dec2dvds 16382	. 2 ⊢ ¬ 2 ∥ ;;139
20		3ndvds4 43843	. . . 4 ⊢ ¬ 3 ∥ 4
21	1, 2	3dvdsdec 15666	. . . . 5 ⊢ (3 ∥ ;13 ↔ 3 ∥ (1 + 3))
22		3cn 11705	. . . . . . 7 ⊢ 3 ∈ ℂ
23		ax-1cn 10581	. . . . . . 7 ⊢ 1 ∈ ℂ
24		3p1e4 11769	. . . . . . 7 ⊢ (3 + 1) = 4
25	22, 23, 24	addcomli 10818	. . . . . 6 ⊢ (1 + 3) = 4
26	25	breq2i 5060	. . . . 5 ⊢ (3 ∥ (1 + 3) ↔ 3 ∥ 4)
27	21, 26	bitri 277	. . . 4 ⊢ (3 ∥ ;13 ↔ 3 ∥ 4)
28	20, 27	mtbir 325	. . 3 ⊢ ¬ 3 ∥ ;13
29	1, 2, 8	3dvds2dec 15667	. . . 4 ⊢ (3 ∥ ;;139 ↔ 3 ∥ ((1 + 3) + 9))
30	25	oveq1i 7152	. . . . . 6 ⊢ ((1 + 3) + 9) = (4 + 9)
31		9cn 11724	. . . . . . 7 ⊢ 9 ∈ ℂ
32		4cn 11709	. . . . . . 7 ⊢ 4 ∈ ℂ
33		9p4e13 12174	. . . . . . 7 ⊢ (9 + 4) = ;13
34	31, 32, 33	addcomli 10818	. . . . . 6 ⊢ (4 + 9) = ;13
35	30, 34	eqtri 2844	. . . . 5 ⊢ ((1 + 3) + 9) = ;13
36	35	breq2i 5060	. . . 4 ⊢ (3 ∥ ((1 + 3) + 9) ↔ 3 ∥ ;13)
37	29, 36	bitri 277	. . 3 ⊢ (3 ∥ ;;139 ↔ 3 ∥ ;13)
38	28, 37	mtbir 325	. 2 ⊢ ¬ 3 ∥ ;;139
39		4nn 11707	. . 3 ⊢ 4 ∈ ℕ
40		4lt5 11801	. . 3 ⊢ 4 < 5
41		5p4e9 11782	. . 3 ⊢ (5 + 4) = 9
42	3, 39, 40, 41	dec5dvds2 16384	. 2 ⊢ ¬ 5 ∥ ;;139
43		7nn 11716	. . 3 ⊢ 7 ∈ ℕ
44	1, 8	deccl 12100	. . 3 ⊢ ;19 ∈ ℕ0
45		6nn 11713	. . 3 ⊢ 6 ∈ ℕ
46		0nn0 11899	. . . 4 ⊢ 0 ∈ ℕ0
47		6nn0 11905	. . . 4 ⊢ 6 ∈ ℕ0
48		eqid 2821	. . . 4 ⊢ ;19 = ;19
49	47	dec0h 12107	. . . 4 ⊢ 6 = ;06
50		7nn0 11906	. . . 4 ⊢ 7 ∈ ℕ0
51		7cn 11718	. . . . . . 7 ⊢ 7 ∈ ℂ
52	51	mulid1i 10631	. . . . . 6 ⊢ (7 · 1) = 7
53		6cn 11715	. . . . . . 7 ⊢ 6 ∈ ℂ
54	53	addid2i 10814	. . . . . 6 ⊢ (0 + 6) = 6
55	52, 54	oveq12i 7154	. . . . 5 ⊢ ((7 · 1) + (0 + 6)) = (7 + 6)
56		7p6e13 12163	. . . . 5 ⊢ (7 + 6) = ;13
57	55, 56	eqtri 2844	. . . 4 ⊢ ((7 · 1) + (0 + 6)) = ;13
58		9t7e63 12212	. . . . . 6 ⊢ (9 · 7) = ;63
59	31, 51, 58	mulcomli 10636	. . . . 5 ⊢ (7 · 9) = ;63
60		6p3e9 11784	. . . . . 6 ⊢ (6 + 3) = 9
61	53, 22, 60	addcomli 10818	. . . . 5 ⊢ (3 + 6) = 9
62	47, 2, 47, 59, 61	decaddi 12145	. . . 4 ⊢ ((7 · 9) + 6) = ;69
63	1, 8, 46, 47, 48, 49, 50, 8, 47, 57, 62	decma2c 12138	. . 3 ⊢ ((7 · ;19) + 6) = ;;139
64		6lt7 11810	. . 3 ⊢ 6 < 7
65	43, 44, 45, 63, 64	ndvdsi 15746	. 2 ⊢ ¬ 7 ∥ ;;139
66		1nn 11635	. . . 4 ⊢ 1 ∈ ℕ
67	1, 66	decnncl 12105	. . 3 ⊢ ;11 ∈ ℕ
68		2nn0 11901	. . . 4 ⊢ 2 ∈ ℕ0
69	1, 68	deccl 12100	. . 3 ⊢ ;12 ∈ ℕ0
70		eqid 2821	. . . 4 ⊢ ;12 = ;12
71	50	dec0h 12107	. . . 4 ⊢ 7 = ;07
72	1, 1	deccl 12100	. . . 4 ⊢ ;11 ∈ ℕ0
73		2cn 11699	. . . . . . 7 ⊢ 2 ∈ ℂ
74	73	addid2i 10814	. . . . . 6 ⊢ (0 + 2) = 2
75	74	oveq2i 7153	. . . . 5 ⊢ ((;11 · 1) + (0 + 2)) = ((;11 · 1) + 2)
76	67	nncni 11634	. . . . . . 7 ⊢ ;11 ∈ ℂ
77	76	mulid1i 10631	. . . . . 6 ⊢ (;11 · 1) = ;11
78		1p2e3 11767	. . . . . 6 ⊢ (1 + 2) = 3
79	1, 1, 68, 77, 78	decaddi 12145	. . . . 5 ⊢ ((;11 · 1) + 2) = ;13
80	75, 79	eqtri 2844	. . . 4 ⊢ ((;11 · 1) + (0 + 2)) = ;13
81		eqid 2821	. . . . 5 ⊢ ;11 = ;11
82	73	mulid2i 10632	. . . . . . 7 ⊢ (1 · 2) = 2
83		00id 10801	. . . . . . 7 ⊢ (0 + 0) = 0
84	82, 83	oveq12i 7154	. . . . . 6 ⊢ ((1 · 2) + (0 + 0)) = (2 + 0)
85	73	addid1i 10813	. . . . . 6 ⊢ (2 + 0) = 2
86	84, 85	eqtri 2844	. . . . 5 ⊢ ((1 · 2) + (0 + 0)) = 2
87	82	oveq1i 7152	. . . . . 6 ⊢ ((1 · 2) + 7) = (2 + 7)
88		7p2e9 11785	. . . . . . 7 ⊢ (7 + 2) = 9
89	51, 73, 88	addcomli 10818	. . . . . 6 ⊢ (2 + 7) = 9
90	8	dec0h 12107	. . . . . 6 ⊢ 9 = ;09
91	87, 89, 90	3eqtri 2848	. . . . 5 ⊢ ((1 · 2) + 7) = ;09
92	1, 1, 46, 50, 81, 71, 68, 8, 46, 86, 91	decmac 12137	. . . 4 ⊢ ((;11 · 2) + 7) = ;29
93	1, 68, 46, 50, 70, 71, 72, 8, 68, 80, 92	decma2c 12138	. . 3 ⊢ ((;11 · ;12) + 7) = ;;139
94		7lt10 12218	. . . 4 ⊢ 7 < ;10
95	66, 1, 50, 94	declti 12123	. . 3 ⊢ 7 < ;11
96	67, 69, 43, 93, 95	ndvdsi 15746	. 2 ⊢ ¬ ;11 ∥ ;;139
97	1, 46	deccl 12100	. . 3 ⊢ ;10 ∈ ℕ0
98		eqid 2821	. . . 4 ⊢ ;10 = ;10
99	3	nn0cni 11896	. . . . . . 7 ⊢ ;13 ∈ ℂ
100	99	mulid1i 10631	. . . . . 6 ⊢ (;13 · 1) = ;13
101	100, 83	oveq12i 7154	. . . . 5 ⊢ ((;13 · 1) + (0 + 0)) = (;13 + 0)
102	99	addid1i 10813	. . . . 5 ⊢ (;13 + 0) = ;13
103	101, 102	eqtri 2844	. . . 4 ⊢ ((;13 · 1) + (0 + 0)) = ;13
104	99	mul01i 10816	. . . . . 6 ⊢ (;13 · 0) = 0
105	104	oveq1i 7152	. . . . 5 ⊢ ((;13 · 0) + 9) = (0 + 9)
106	31	addid2i 10814	. . . . 5 ⊢ (0 + 9) = 9
107	105, 106, 90	3eqtri 2848	. . . 4 ⊢ ((;13 · 0) + 9) = ;09
108	1, 46, 46, 8, 98, 90, 3, 8, 46, 103, 107	decma2c 12138	. . 3 ⊢ ((;13 · ;10) + 9) = ;;139
109	66, 2, 8, 11	declti 12123	. . 3 ⊢ 9 < ;13
110	14, 97, 4, 108, 109	ndvdsi 15746	. 2 ⊢ ¬ ;13 ∥ ;;139
111	1, 43	decnncl 12105	. . 3 ⊢ ;17 ∈ ℕ
112		eqid 2821	. . . 4 ⊢ ;17 = ;17
113	2	dec0h 12107	. . . 4 ⊢ 3 = ;03
114		5nn0 11904	. . . 4 ⊢ 5 ∈ ℕ0
115		8cn 11721	. . . . . . 7 ⊢ 8 ∈ ℂ
116	115	mulid2i 10632	. . . . . 6 ⊢ (1 · 8) = 8
117		5cn 11712	. . . . . . 7 ⊢ 5 ∈ ℂ
118	117	addid2i 10814	. . . . . 6 ⊢ (0 + 5) = 5
119	116, 118	oveq12i 7154	. . . . 5 ⊢ ((1 · 8) + (0 + 5)) = (8 + 5)
120		8p5e13 12168	. . . . 5 ⊢ (8 + 5) = ;13
121	119, 120	eqtri 2844	. . . 4 ⊢ ((1 · 8) + (0 + 5)) = ;13
122		8t7e56 12205	. . . . . 6 ⊢ (8 · 7) = ;56
123	115, 51, 122	mulcomli 10636	. . . . 5 ⊢ (7 · 8) = ;56
124	114, 47, 2, 123, 60	decaddi 12145	. . . 4 ⊢ ((7 · 8) + 3) = ;59
125	1, 50, 46, 2, 112, 113, 6, 8, 114, 121, 124	decmac 12137	. . 3 ⊢ ((;17 · 8) + 3) = ;;139
126	66, 50, 2, 10	declti 12123	. . 3 ⊢ 3 < ;17
127	111, 6, 13, 125, 126	ndvdsi 15746	. 2 ⊢ ¬ ;17 ∥ ;;139
128	1, 4	decnncl 12105	. . 3 ⊢ ;19 ∈ ℕ
129	51	mulid2i 10632	. . . . . 6 ⊢ (1 · 7) = 7
130	129, 54	oveq12i 7154	. . . . 5 ⊢ ((1 · 7) + (0 + 6)) = (7 + 6)
131	130, 56	eqtri 2844	. . . 4 ⊢ ((1 · 7) + (0 + 6)) = ;13
132	47, 2, 47, 58, 61	decaddi 12145	. . . 4 ⊢ ((9 · 7) + 6) = ;69
133	1, 8, 46, 47, 48, 49, 50, 8, 47, 131, 132	decmac 12137	. . 3 ⊢ ((;19 · 7) + 6) = ;;139
134		6lt10 12219	. . . 4 ⊢ 6 < ;10
135	66, 8, 47, 134	declti 12123	. . 3 ⊢ 6 < ;19
136	128, 50, 45, 133, 135	ndvdsi 15746	. 2 ⊢ ¬ ;19 ∥ ;;139
137	68, 13	decnncl 12105	. . 3 ⊢ ;23 ∈ ℕ
138		eqid 2821	. . . 4 ⊢ ;23 = ;23
139		2p1e3 11766	. . . . 5 ⊢ (2 + 1) = 3
140		6t2e12 12189	. . . . . 6 ⊢ (6 · 2) = ;12
141	53, 73, 140	mulcomli 10636	. . . . 5 ⊢ (2 · 6) = ;12
142	1, 68, 139, 141	decsuc 12116	. . . 4 ⊢ ((2 · 6) + 1) = ;13
143		8p1e9 11774	. . . . 5 ⊢ (8 + 1) = 9
144		6t3e18 12190	. . . . . 6 ⊢ (6 · 3) = ;18
145	53, 22, 144	mulcomli 10636	. . . . 5 ⊢ (3 · 6) = ;18
146	1, 6, 143, 145	decsuc 12116	. . . 4 ⊢ ((3 · 6) + 1) = ;19
147	68, 2, 1, 138, 47, 8, 1, 142, 146	decrmac 12143	. . 3 ⊢ ((;23 · 6) + 1) = ;;139
148		2nn 11697	. . . 4 ⊢ 2 ∈ ℕ
149	148, 2, 1, 15	declti 12123	. . 3 ⊢ 1 < ;23
150	137, 47, 66, 147, 149	ndvdsi 15746	. 2 ⊢ ¬ ;23 ∥ ;;139
151	5, 12, 16, 19, 38, 42, 65, 96, 110, 127, 136, 150	prmlem2 16436	1 ⊢ ;;139 ∈ ℙ

Syntax hints:   ∈ wcel 2114   class class class wbr 5052  (class class class)co 7142  0cc0 10523  1c1 10524   + caddc 10526   · cmul 10528  2c2 11679  3c3 11680  4c4 11681  5c5 11682  6c6 11683  7c7 11684  8c8 11685  9c9 11686  ;cdc 12085   ∥ cdvds 15592  ℙcprime 15998

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5189  ax-nul 5196  ax-pow 5252  ax-pr 5316  ax-un 7447  ax-cnex 10579  ax-resscn 10580  ax-1cn 10581  ax-icn 10582  ax-addcl 10583  ax-addrcl 10584  ax-mulcl 10585  ax-mulrcl 10586  ax-mulcom 10587  ax-addass 10588  ax-mulass 10589  ax-distr 10590  ax-i2m1 10591  ax-1ne0 10592  ax-1rid 10593  ax-rnegex 10594  ax-rrecex 10595  ax-cnre 10596  ax-pre-lttri 10597  ax-pre-lttrn 10598  ax-pre-ltadd 10599  ax-pre-mulgt0 10600  ax-pre-sup 10601

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-nel 3124  df-ral 3143  df-rex 3144  df-reu 3145  df-rmo 3146  df-rab 3147  df-v 3488  df-sbc 3764  df-csb 3872  df-dif 3927  df-un 3929  df-in 3931  df-ss 3940  df-pss 3942  df-nul 4280  df-if 4454  df-pw 4527  df-sn 4554  df-pr 4556  df-tp 4558  df-op 4560  df-uni 4825  df-iun 4907  df-br 5053  df-opab 5115  df-mpt 5133  df-tr 5159  df-id 5446  df-eprel 5451  df-po 5460  df-so 5461  df-fr 5500  df-we 5502  df-xp 5547  df-rel 5548  df-cnv 5549  df-co 5550  df-dm 5551  df-rn 5552  df-res 5553  df-ima 5554  df-pred 6134  df-ord 6180  df-on 6181  df-lim 6182  df-suc 6183  df-iota 6300  df-fun 6343  df-fn 6344  df-f 6345  df-f1 6346  df-fo 6347  df-f1o 6348  df-fv 6349  df-riota 7100  df-ov 7145  df-oprab 7146  df-mpo 7147  df-om 7567  df-1st 7675  df-2nd 7676  df-wrecs 7933  df-recs 7994  df-rdg 8032  df-1o 8088  df-2o 8089  df-er 8275  df-en 8496  df-dom 8497  df-sdom 8498  df-fin 8499  df-sup 8892  df-inf 8893  df-pnf 10663  df-mnf 10664  df-xr 10665  df-ltxr 10666  df-le 10667  df-sub 10858  df-neg 10859  df-div 11284  df-nn 11625  df-2 11687  df-3 11688  df-4 11689  df-5 11690  df-6 11691  df-7 11692  df-8 11693  df-9 11694  df-n0 11885  df-z 11969  df-dec 12086  df-uz 12231  df-rp 12377  df-fz 12883  df-seq 13360  df-exp 13420  df-cj 14443  df-re 14444  df-im 14445  df-sqrt 14579  df-abs 14580  df-dvds 15593  df-prm 15999

This theorem is referenced by: (None)