Theorem 139prmALT 48074

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 48073	. . . 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 5080	. . . . 5 ⊢ (3 ∥ (1 + 3) ↔ 3 ∥ 4)
27	21, 26	bitri 276	. . . 4 ⊢ (3 ∥ ;13 ↔ 3 ∥ 4)
28	20, 27	mtbir 324	. . 3 ⊢ ¬ 3 ∥ ;13
29	1, 2, 8	3dvds2dec 16293	. . . 4 ⊢ (3 ∥ ;;139 ↔ 3 ∥ ((1 + 3) + 9))
30	25	oveq1i 7366	. . . . . 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 2762	. . . . 5 ⊢ ((1 + 3) + 9) = ;13
36	35	breq2i 5080	. . . 4 ⊢ (3 ∥ ((1 + 3) + 9) ↔ 3 ∥ ;13)
37	29, 36	bitri 276	. . 3 ⊢ (3 ∥ ;;139 ↔ 3 ∥ ;13)
38	28, 37	mtbir 324	. 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 2739	. . . 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 7368	. . . . 5 ⊢ ((7 · 1) + (0 + 6)) = (7 + 6)
56		7p6e13 12713	. . . . 5 ⊢ (7 + 6) = ;13
57	55, 56	eqtri 2762	. . . 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 2739	. . . 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 7367	. . . . 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 2762	. . . 4 ⊢ ((;11 · 1) + (0 + 2)) = ;13
81		eqid 2739	. . . . 5 ⊢ ;11 = ;11
82	73	mullidi 11141	. . . . . . 7 ⊢ (1 · 2) = 2
83		00id 11312	. . . . . . 7 ⊢ (0 + 0) = 0
84	82, 83	oveq12i 7368	. . . . . 6 ⊢ ((1 · 2) + (0 + 0)) = (2 + 0)
85	73	addridi 11324	. . . . . 6 ⊢ (2 + 0) = 2
86	84, 85	eqtri 2762	. . . . 5 ⊢ ((1 · 2) + (0 + 0)) = 2
87	82	oveq1i 7366	. . . . . 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 2766	. . . . 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 2739	. . . 4 ⊢ ;10 = ;10
99	3	nn0cni 12440	. . . . . . 7 ⊢ ;13 ∈ ℂ
100	99	mulridi 11140	. . . . . 6 ⊢ (;13 · 1) = ;13
101	100, 83	oveq12i 7368	. . . . 5 ⊢ ((;13 · 1) + (0 + 0)) = (;13 + 0)
102	99	addridi 11324	. . . . 5 ⊢ (;13 + 0) = ;13
103	101, 102	eqtri 2762	. . . 4 ⊢ ((;13 · 1) + (0 + 0)) = ;13
104	99	mul01i 11327	. . . . . 6 ⊢ (;13 · 0) = 0
105	104	oveq1i 7366	. . . . 5 ⊢ ((;13 · 0) + 9) = (0 + 9)
106	31	addlidi 11325	. . . . 5 ⊢ (0 + 9) = 9
107	105, 106, 90	3eqtri 2766	. . . 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 2739	. . . 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 7368	. . . . 5 ⊢ ((1 · 8) + (0 + 5)) = (8 + 5)
120		8p5e13 12718	. . . . 5 ⊢ (8 + 5) = ;13
121	119, 120	eqtri 2762	. . . 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 7368	. . . . 5 ⊢ ((1 · 7) + (0 + 6)) = (7 + 6)
131	130, 56	eqtri 2762	. . . 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 2739	. . . 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 2119   class class class wbr 5072  (class class class)co 7356  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 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-sep 5218  ax-nul 5228  ax-pow 5294  ax-pr 5362  ax-un 7678  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 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ne 2935  df-nel 3039  df-ral 3054  df-rex 3064  df-rmo 3344  df-reu 3345  df-rab 3392  df-v 3433  df-sbc 3724  df-csb 3832  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3903  df-nul 4262  df-if 4455  df-pw 4531  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-iun 4923  df-br 5073  df-opab 5135  df-mpt 5154  df-tr 5180  df-id 5513  df-eprel 5518  df-po 5526  df-so 5527  df-fr 5571  df-we 5573  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-rn 5629  df-res 5630  df-ima 5631  df-pred 6252  df-ord 6313  df-on 6314  df-lim 6315  df-suc 6316  df-iota 6441  df-fun 6487  df-fn 6488  df-f 6489  df-f1 6490  df-fo 6491  df-f1o 6492  df-fv 6493  df-riota 7313  df-ov 7359  df-oprab 7360  df-mpo 7361  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 8633  df-en 8884  df-dom 8885  df-sdom 8886  df-fin 8887  df-sup 9345  df-inf 9346  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)