Theorem 139prm

Description: 139 is a prime number. (Contributed by Mario Carneiro, 19-Feb-2014) (Proof shortened by Mario Carneiro, 20-Apr-2015)

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