Theorem 139prmALT

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

	Ref	Expression
Assertion	139prmALT	|- ; ; 1 3 9 e. Prime

Proof

Step	Hyp	Ref	Expression
1		1nn0	|- 1 e. NN0
2		3nn0	|- 3 e. NN0
3	1 2	deccl	|- ; 1 3 e. NN0
4		9nn	|- 9 e. NN
5	3 4	decnncl	|- ; ; 1 3 9 e. NN
6		8nn0	|- 8 e. NN0
7		4nn0	|- 4 e. NN0
8		9nn0	|- 9 e. NN0
9		1lt8	|- 1 < 8
10		3lt10	|- 3 < ; 1 0
11		9lt10	|- 9 < ; 1 0
12	1 6 2 7 8 1 9 10 11	3decltc	|- ; ; 1 3 9 < ; ; 8 4 1
13		3nn	|- 3 e. NN
14	1 13	decnncl	|- ; 1 3 e. NN
15		1lt10	|- 1 < ; 1 0
16	14 8 1 15	declti	|- 1 < ; ; 1 3 9
17		4t2e8	|- ( 4 x. 2 ) = 8
18		df-9	|- 9 = ( 8 + 1 )
19	3 7 17 18	dec2dvds	|- -. 2 || ; ; 1 3 9
20		3ndvds4	|- -. 3 || 4
21	1 2	3dvdsdec	|- ( 3 || ; 1 3 <-> 3 || ( 1 + 3 ) )
22		3cn	|- 3 e. CC
23		ax-1cn	|- 1 e. CC
24		3p1e4	|- ( 3 + 1 ) = 4
25	22 23 24	addcomli	|- ( 1 + 3 ) = 4
26	25	breq2i	|- ( 3 || ( 1 + 3 ) <-> 3 || 4 )
27	21 26	bitri	|- ( 3 || ; 1 3 <-> 3 || 4 )
28	20 27	mtbir	|- -. 3 || ; 1 3
29	1 2 8	3dvds2dec	|- ( 3 || ; ; 1 3 9 <-> 3 || ( ( 1 + 3 ) + 9 ) )
30	25	oveq1i	|- ( ( 1 + 3 ) + 9 ) = ( 4 + 9 )
31		9cn	|- 9 e. CC
32		4cn	|- 4 e. CC
33		9p4e13	|- ( 9 + 4 ) = ; 1 3
34	31 32 33	addcomli	|- ( 4 + 9 ) = ; 1 3
35	30 34	eqtri	|- ( ( 1 + 3 ) + 9 ) = ; 1 3
36	35	breq2i	|- ( 3 || ( ( 1 + 3 ) + 9 ) <-> 3 || ; 1 3 )
37	29 36	bitri	|- ( 3 || ; ; 1 3 9 <-> 3 || ; 1 3 )
38	28 37	mtbir	|- -. 3 || ; ; 1 3 9
39		4nn	|- 4 e. NN
40		4lt5	|- 4 < 5
41		5p4e9	|- ( 5 + 4 ) = 9
42	3 39 40 41	dec5dvds2	|- -. 5 || ; ; 1 3 9
43		7nn	|- 7 e. NN
44	1 8	deccl	|- ; 1 9 e. NN0
45		6nn	|- 6 e. NN
46		0nn0	|- 0 e. NN0
47		6nn0	|- 6 e. NN0
48		eqid	|- ; 1 9 = ; 1 9
49	47	dec0h	|- 6 = ; 0 6
50		7nn0	|- 7 e. NN0
51		7cn	|- 7 e. CC
52	51	mulid1i	|- ( 7 x. 1 ) = 7
53		6cn	|- 6 e. CC
54	53	addid2i	|- ( 0 + 6 ) = 6
55	52 54	oveq12i	|- ( ( 7 x. 1 ) + ( 0 + 6 ) ) = ( 7 + 6 )
56		7p6e13	|- ( 7 + 6 ) = ; 1 3
57	55 56	eqtri	|- ( ( 7 x. 1 ) + ( 0 + 6 ) ) = ; 1 3
58		9t7e63	|- ( 9 x. 7 ) = ; 6 3
59	31 51 58	mulcomli	|- ( 7 x. 9 ) = ; 6 3
60		6p3e9	|- ( 6 + 3 ) = 9
61	53 22 60	addcomli	|- ( 3 + 6 ) = 9
62	47 2 47 59 61	decaddi	|- ( ( 7 x. 9 ) + 6 ) = ; 6 9
63	1 8 46 47 48 49 50 8 47 57 62	decma2c	|- ( ( 7 x. ; 1 9 ) + 6 ) = ; ; 1 3 9
64		6lt7	|- 6 < 7
65	43 44 45 63 64	ndvdsi	|- -. 7 || ; ; 1 3 9
66		1nn	|- 1 e. NN
67	1 66	decnncl	|- ; 1 1 e. NN
68		2nn0	|- 2 e. NN0
69	1 68	deccl	|- ; 1 2 e. NN0
70		eqid	|- ; 1 2 = ; 1 2
71	50	dec0h	|- 7 = ; 0 7
72	1 1	deccl	|- ; 1 1 e. NN0
73		2cn	|- 2 e. CC
74	73	addid2i	|- ( 0 + 2 ) = 2
75	74	oveq2i	|- ( ( ; 1 1 x. 1 ) + ( 0 + 2 ) ) = ( ( ; 1 1 x. 1 ) + 2 )
76	67	nncni	|- ; 1 1 e. CC
77	76	mulid1i	|- ( ; 1 1 x. 1 ) = ; 1 1
78		1p2e3	|- ( 1 + 2 ) = 3
79	1 1 68 77 78	decaddi	|- ( ( ; 1 1 x. 1 ) + 2 ) = ; 1 3
80	75 79	eqtri	|- ( ( ; 1 1 x. 1 ) + ( 0 + 2 ) ) = ; 1 3
81		eqid	|- ; 1 1 = ; 1 1
82	73	mulid2i	|- ( 1 x. 2 ) = 2
83		00id	|- ( 0 + 0 ) = 0
84	82 83	oveq12i	|- ( ( 1 x. 2 ) + ( 0 + 0 ) ) = ( 2 + 0 )
85	73	addid1i	|- ( 2 + 0 ) = 2
86	84 85	eqtri	|- ( ( 1 x. 2 ) + ( 0 + 0 ) ) = 2
87	82	oveq1i	|- ( ( 1 x. 2 ) + 7 ) = ( 2 + 7 )
88		7p2e9	|- ( 7 + 2 ) = 9
89	51 73 88	addcomli	|- ( 2 + 7 ) = 9
90	8	dec0h	|- 9 = ; 0 9
91	87 89 90	3eqtri	|- ( ( 1 x. 2 ) + 7 ) = ; 0 9
92	1 1 46 50 81 71 68 8 46 86 91	decmac	|- ( ( ; 1 1 x. 2 ) + 7 ) = ; 2 9
93	1 68 46 50 70 71 72 8 68 80 92	decma2c	|- ( ( ; 1 1 x. ; 1 2 ) + 7 ) = ; ; 1 3 9
94		7lt10	|- 7 < ; 1 0
95	66 1 50 94	declti	|- 7 < ; 1 1
96	67 69 43 93 95	ndvdsi	|- -. ; 1 1 || ; ; 1 3 9
97	1 46	deccl	|- ; 1 0 e. NN0
98		eqid	|- ; 1 0 = ; 1 0
99	3	nn0cni	|- ; 1 3 e. CC
100	99	mulid1i	|- ( ; 1 3 x. 1 ) = ; 1 3
101	100 83	oveq12i	|- ( ( ; 1 3 x. 1 ) + ( 0 + 0 ) ) = ( ; 1 3 + 0 )
102	99	addid1i	|- ( ; 1 3 + 0 ) = ; 1 3
103	101 102	eqtri	|- ( ( ; 1 3 x. 1 ) + ( 0 + 0 ) ) = ; 1 3
104	99	mul01i	|- ( ; 1 3 x. 0 ) = 0
105	104	oveq1i	|- ( ( ; 1 3 x. 0 ) + 9 ) = ( 0 + 9 )
106	31	addid2i	|- ( 0 + 9 ) = 9
107	105 106 90	3eqtri	|- ( ( ; 1 3 x. 0 ) + 9 ) = ; 0 9
108	1 46 46 8 98 90 3 8 46 103 107	decma2c	|- ( ( ; 1 3 x. ; 1 0 ) + 9 ) = ; ; 1 3 9
109	66 2 8 11	declti	|- 9 < ; 1 3
110	14 97 4 108 109	ndvdsi	|- -. ; 1 3 || ; ; 1 3 9
111	1 43	decnncl	|- ; 1 7 e. NN
112		eqid	|- ; 1 7 = ; 1 7
113	2	dec0h	|- 3 = ; 0 3
114		5nn0	|- 5 e. NN0
115		8cn	|- 8 e. CC
116	115	mulid2i	|- ( 1 x. 8 ) = 8
117		5cn	|- 5 e. CC
118	117	addid2i	|- ( 0 + 5 ) = 5
119	116 118	oveq12i	|- ( ( 1 x. 8 ) + ( 0 + 5 ) ) = ( 8 + 5 )
120		8p5e13	|- ( 8 + 5 ) = ; 1 3
121	119 120	eqtri	|- ( ( 1 x. 8 ) + ( 0 + 5 ) ) = ; 1 3
122		8t7e56	|- ( 8 x. 7 ) = ; 5 6
123	115 51 122	mulcomli	|- ( 7 x. 8 ) = ; 5 6
124	114 47 2 123 60	decaddi	|- ( ( 7 x. 8 ) + 3 ) = ; 5 9
125	1 50 46 2 112 113 6 8 114 121 124	decmac	|- ( ( ; 1 7 x. 8 ) + 3 ) = ; ; 1 3 9
126	66 50 2 10	declti	|- 3 < ; 1 7
127	111 6 13 125 126	ndvdsi	|- -. ; 1 7 || ; ; 1 3 9
128	1 4	decnncl	|- ; 1 9 e. NN
129	51	mulid2i	|- ( 1 x. 7 ) = 7
130	129 54	oveq12i	|- ( ( 1 x. 7 ) + ( 0 + 6 ) ) = ( 7 + 6 )
131	130 56	eqtri	|- ( ( 1 x. 7 ) + ( 0 + 6 ) ) = ; 1 3
132	47 2 47 58 61	decaddi	|- ( ( 9 x. 7 ) + 6 ) = ; 6 9
133	1 8 46 47 48 49 50 8 47 131 132	decmac	|- ( ( ; 1 9 x. 7 ) + 6 ) = ; ; 1 3 9
134		6lt10	|- 6 < ; 1 0
135	66 8 47 134	declti	|- 6 < ; 1 9
136	128 50 45 133 135	ndvdsi	|- -. ; 1 9 || ; ; 1 3 9
137	68 13	decnncl	|- ; 2 3 e. NN
138		eqid	|- ; 2 3 = ; 2 3
139		2p1e3	|- ( 2 + 1 ) = 3
140		6t2e12	|- ( 6 x. 2 ) = ; 1 2
141	53 73 140	mulcomli	|- ( 2 x. 6 ) = ; 1 2
142	1 68 139 141	decsuc	|- ( ( 2 x. 6 ) + 1 ) = ; 1 3
143		8p1e9	|- ( 8 + 1 ) = 9
144		6t3e18	|- ( 6 x. 3 ) = ; 1 8
145	53 22 144	mulcomli	|- ( 3 x. 6 ) = ; 1 8
146	1 6 143 145	decsuc	|- ( ( 3 x. 6 ) + 1 ) = ; 1 9
147	68 2 1 138 47 8 1 142 146	decrmac	|- ( ( ; 2 3 x. 6 ) + 1 ) = ; ; 1 3 9
148		2nn	|- 2 e. NN
149	148 2 1 15	declti	|- 1 < ; 2 3
150	137 47 66 147 149	ndvdsi	|- -. ; 2 3 || ; ; 1 3 9
151	5 12 16 19 38 42 65 96 110 127 136 150	prmlem2	|- ; ; 1 3 9 e. Prime