Theorem 631prm 15098

Description: 631 is a prime number. (Contributed by Mario Carneiro, 1-Mar-2014.) (Proof shortened by Mario Carneiro, 20-Apr-2015.)

Assertion

Ref	Expression
631prm	|- ;; 6 3 1 e. Prime

Proof of Theorem 631prm

Step	Hyp	Ref	Expression
1		6nn0 10890	. . . 4 |- 6 e. NN0
2		3nn0 10887	. . . 4 |- 3 e. NN0
3	1, 2	deccl 11065	. . 3 |- ; 6 3 e. NN0
4		1nn 10620	. . 3 |- 1 e. NN
5	3, 4	decnncl 11064	. 2 |- ;; 6 3 1 e. NN
6		8nn0 10892	. . . 4 |- 8 e. NN0
7		4nn0 10888	. . . 4 |- 4 e. NN0
8	6, 7	deccl 11065	. . 3 |- ; 8 4 e. NN0
9		1nn0 10885	. . 3 |- 1 e. NN0
10		1lt10 10820	. . 3 |- 1 < 10
11		3lt10 10818	. . . 4 |- 3 < 10
12		6lt8 10798	. . . 4 |- 6 < 8
13	1, 6, 2, 7, 11, 12	decltc 11073	. . 3 |- ; 6 3 < ; 8 4
14	3, 8, 9, 9, 10, 13	decltc 11073	. 2 |- ;; 6 3 1 < ;; 8 4 1
15		3nn 10768	. . . 4 |- 3 e. NN
16	1, 15	decnncl 11064	. . 3 |- ; 6 3 e. NN
17	16, 9, 9, 10	declti 11076	. 2 |- 1 < ;; 6 3 1
18		0nn0 10884	. . 3 |- 0 e. NN0
19		2cn 10680	. . . 4 |- 2 e. CC
20	19	mul02i 9822	. . 3 |- ( 0 x. 2 ) = 0
21		1e0p1 11079	. . 3 |- 1 = ( 0 + 1 )
22	3, 18, 20, 21	dec2dvds 15035	. 2 |- -. 2 || ;; 6 3 1
23		2nn0 10886	. . . . 5 |- 2 e. NN0
24	23, 9	deccl 11065	. . . 4 |- ; 2 1 e. NN0
25	24, 18	deccl 11065	. . 3 |- ;; 2 1 0 e. NN0
26		eqid 2451	. . . 4 |- ;; 2 1 0 = ;; 2 1 0
27	9	dec0h 11067	. . . 4 |- 1 = ; 0 1
28		eqid 2451	. . . . 5 |- ; 2 1 = ; 2 1
29		00id 9808	. . . . . 6 |- ( 0 + 0 ) = 0
30	18	dec0h 11067	. . . . . 6 |- 0 = ; 0 0
31	29, 30	eqtri 2473	. . . . 5 |- ( 0 + 0 ) = ; 0 0
32		3t2e6 10761	. . . . . . 7 |- ( 3 x. 2 ) = 6
33	32, 29	oveq12i 6302	. . . . . 6 |- ( ( 3 x. 2 ) + ( 0 + 0 ) ) = ( 6 + 0 )
34		6cn 10691	. . . . . . 7 |- 6 e. CC
35	34	addid1i 9820	. . . . . 6 |- ( 6 + 0 ) = 6
36	33, 35	eqtri 2473	. . . . 5 |- ( ( 3 x. 2 ) + ( 0 + 0 ) ) = 6
37		3t1e3 10760	. . . . . . 7 |- ( 3 x. 1 ) = 3
38	37	oveq1i 6300	. . . . . 6 |- ( ( 3 x. 1 ) + 0 ) = ( 3 + 0 )
39		3cn 10684	. . . . . . 7 |- 3 e. CC
40	39	addid1i 9820	. . . . . 6 |- ( 3 + 0 ) = 3
41	2	dec0h 11067	. . . . . 6 |- 3 = ; 0 3
42	38, 40, 41	3eqtri 2477	. . . . 5 |- ( ( 3 x. 1 ) + 0 ) = ; 0 3
43	23, 9, 18, 18, 28, 31, 2, 2, 18, 36, 42	decma2c 11091	. . . 4 |- ( ( 3 x. ; 2 1 ) + ( 0 + 0 ) ) = ; 6 3
44	39	mul01i 9823	. . . . . 6 |- ( 3 x. 0 ) = 0
45	44	oveq1i 6300	. . . . 5 |- ( ( 3 x. 0 ) + 1 ) = ( 0 + 1 )
46		0p1e1 10721	. . . . 5 |- ( 0 + 1 ) = 1
47	45, 46, 27	3eqtri 2477	. . . 4 |- ( ( 3 x. 0 ) + 1 ) = ; 0 1
48	24, 18, 18, 9, 26, 27, 2, 9, 18, 43, 47	decma2c 11091	. . 3 |- ( ( 3 x. ;; 2 1 0 ) + 1 ) = ;; 6 3 1
49		1lt3 10778	. . 3 |- 1 < 3
50	15, 25, 4, 48, 49	ndvdsi 14391	. 2 |- -. 3 || ;; 6 3 1
51		1lt5 10785	. . 3 |- 1 < 5
52	3, 4, 51	dec5dvds 15036	. 2 |- -. 5 || ;; 6 3 1
53		7nn 10772	. . 3 |- 7 e. NN
54		9nn0 10893	. . . 4 |- 9 e. NN0
55	54, 18	deccl 11065	. . 3 |- ; 9 0 e. NN0
56		eqid 2451	. . . 4 |- ; 9 0 = ; 9 0
57		7nn0 10891	. . . 4 |- 7 e. NN0
58	29	oveq2i 6301	. . . . 5 |- ( ( 7 x. 9 ) + ( 0 + 0 ) ) = ( ( 7 x. 9 ) + 0 )
59		9cn 10697	. . . . . . 7 |- 9 e. CC
60		7cn 10693	. . . . . . 7 |- 7 e. CC
61		9t7e63 11151	. . . . . . 7 |- ( 9 x. 7 ) = ; 6 3
62	59, 60, 61	mulcomli 9650	. . . . . 6 |- ( 7 x. 9 ) = ; 6 3
63	62	oveq1i 6300	. . . . 5 |- ( ( 7 x. 9 ) + 0 ) = (; 6 3 + 0 )
64	3	nn0cni 10881	. . . . . 6 |- ; 6 3 e. CC
65	64	addid1i 9820	. . . . 5 |- (; 6 3 + 0 ) = ; 6 3
66	58, 63, 65	3eqtri 2477	. . . 4 |- ( ( 7 x. 9 ) + ( 0 + 0 ) ) = ; 6 3
67	60	mul01i 9823	. . . . . 6 |- ( 7 x. 0 ) = 0
68	67	oveq1i 6300	. . . . 5 |- ( ( 7 x. 0 ) + 1 ) = ( 0 + 1 )
69	68, 46, 27	3eqtri 2477	. . . 4 |- ( ( 7 x. 0 ) + 1 ) = ; 0 1
70	54, 18, 18, 9, 56, 27, 57, 9, 18, 66, 69	decma2c 11091	. . 3 |- ( ( 7 x. ; 9 0 ) + 1 ) = ;; 6 3 1
71		1lt7 10796	. . 3 |- 1 < 7
72	53, 55, 4, 70, 71	ndvdsi 14391	. 2 |- -. 7 || ;; 6 3 1
73	9, 4	decnncl 11064	. . 3 |- ; 1 1 e. NN
74		5nn0 10889	. . . 4 |- 5 e. NN0
75	74, 57	deccl 11065	. . 3 |- ; 5 7 e. NN0
76		4nn 10769	. . 3 |- 4 e. NN
77		eqid 2451	. . . 4 |- ; 5 7 = ; 5 7
78	7	dec0h 11067	. . . 4 |- 4 = ; 0 4
79	9, 9	deccl 11065	. . . 4 |- ; 1 1 e. NN0
80		eqid 2451	. . . . 5 |- ; 1 1 = ; 1 1
81		8cn 10695	. . . . . . 7 |- 8 e. CC
82	81	addid2i 9821	. . . . . 6 |- ( 0 + 8 ) = 8
83	6	dec0h 11067	. . . . . 6 |- 8 = ; 0 8
84	82, 83	eqtri 2473	. . . . 5 |- ( 0 + 8 ) = ; 0 8
85		5cn 10689	. . . . . . . 8 |- 5 e. CC
86	85	mulid2i 9646	. . . . . . 7 |- ( 1 x. 5 ) = 5
87	86, 46	oveq12i 6302	. . . . . 6 |- ( ( 1 x. 5 ) + ( 0 + 1 ) ) = ( 5 + 1 )
88		5p1e6 10737	. . . . . 6 |- ( 5 + 1 ) = 6
89	87, 88	eqtri 2473	. . . . 5 |- ( ( 1 x. 5 ) + ( 0 + 1 ) ) = 6
90	86	oveq1i 6300	. . . . . 6 |- ( ( 1 x. 5 ) + 8 ) = ( 5 + 8 )
91		8p5e13 11109	. . . . . . 7 |- ( 8 + 5 ) = ; 1 3
92	81, 85, 91	addcomli 9825	. . . . . 6 |- ( 5 + 8 ) = ; 1 3
93	90, 92	eqtri 2473	. . . . 5 |- ( ( 1 x. 5 ) + 8 ) = ; 1 3
94	9, 9, 18, 6, 80, 84, 74, 2, 9, 89, 93	decmac 11090	. . . 4 |- ( (; 1 1 x. 5 ) + ( 0 + 8 ) ) = ; 6 3
95	60	mulid2i 9646	. . . . . . 7 |- ( 1 x. 7 ) = 7
96	95, 46	oveq12i 6302	. . . . . 6 |- ( ( 1 x. 7 ) + ( 0 + 1 ) ) = ( 7 + 1 )
97		7p1e8 10739	. . . . . 6 |- ( 7 + 1 ) = 8
98	96, 97	eqtri 2473	. . . . 5 |- ( ( 1 x. 7 ) + ( 0 + 1 ) ) = 8
99	95	oveq1i 6300	. . . . . 6 |- ( ( 1 x. 7 ) + 4 ) = ( 7 + 4 )
100		7p4e11 11103	. . . . . 6 |- ( 7 + 4 ) = ; 1 1
101	99, 100	eqtri 2473	. . . . 5 |- ( ( 1 x. 7 ) + 4 ) = ; 1 1
102	9, 9, 18, 7, 80, 78, 57, 9, 9, 98, 101	decmac 11090	. . . 4 |- ( (; 1 1 x. 7 ) + 4 ) = ; 8 1
103	74, 57, 18, 7, 77, 78, 79, 9, 6, 94, 102	decma2c 11091	. . 3 |- ( (; 1 1 x. ; 5 7 ) + 4 ) = ;; 6 3 1
104		4lt10 10817	. . . 4 |- 4 < 10
105	4, 9, 7, 104	declti 11076	. . 3 |- 4 < ; 1 1
106	73, 75, 76, 103, 105	ndvdsi 14391	. 2 |- -. ; 1 1 || ;; 6 3 1
107	9, 15	decnncl 11064	. . 3 |- ; 1 3 e. NN
108	7, 6	deccl 11065	. . 3 |- ; 4 8 e. NN0
109		eqid 2451	. . . 4 |- ; 4 8 = ; 4 8
110	57	dec0h 11067	. . . 4 |- 7 = ; 0 7
111	9, 2	deccl 11065	. . . 4 |- ; 1 3 e. NN0
112		eqid 2451	. . . . 5 |- ; 1 3 = ; 1 3
113	79	nn0cni 10881	. . . . . 6 |- ; 1 1 e. CC
114	113	addid2i 9821	. . . . 5 |- ( 0 + ; 1 1 ) = ; 1 1
115		4cn 10687	. . . . . . . 8 |- 4 e. CC
116	115	mulid2i 9646	. . . . . . 7 |- ( 1 x. 4 ) = 4
117		1p1e2 10723	. . . . . . 7 |- ( 1 + 1 ) = 2
118	116, 117	oveq12i 6302	. . . . . 6 |- ( ( 1 x. 4 ) + ( 1 + 1 ) ) = ( 4 + 2 )
119		4p2e6 10744	. . . . . 6 |- ( 4 + 2 ) = 6
120	118, 119	eqtri 2473	. . . . 5 |- ( ( 1 x. 4 ) + ( 1 + 1 ) ) = 6
121		4t3e12 11123	. . . . . . 7 |- ( 4 x. 3 ) = ; 1 2
122	115, 39, 121	mulcomli 9650	. . . . . 6 |- ( 3 x. 4 ) = ; 1 2
123		2p1e3 10733	. . . . . 6 |- ( 2 + 1 ) = 3
124	9, 23, 9, 122, 123	decaddi 11095	. . . . 5 |- ( ( 3 x. 4 ) + 1 ) = ; 1 3
125	9, 2, 9, 9, 112, 114, 7, 2, 9, 120, 124	decmac 11090	. . . 4 |- ( (; 1 3 x. 4 ) + ( 0 + ; 1 1 ) ) = ; 6 3
126	81	mulid2i 9646	. . . . . . 7 |- ( 1 x. 8 ) = 8
127	39	addid2i 9821	. . . . . . 7 |- ( 0 + 3 ) = 3
128	126, 127	oveq12i 6302	. . . . . 6 |- ( ( 1 x. 8 ) + ( 0 + 3 ) ) = ( 8 + 3 )
129		8p3e11 11107	. . . . . 6 |- ( 8 + 3 ) = ; 1 1
130	128, 129	eqtri 2473	. . . . 5 |- ( ( 1 x. 8 ) + ( 0 + 3 ) ) = ; 1 1
131		8t3e24 11140	. . . . . . 7 |- ( 8 x. 3 ) = ; 2 4
132	81, 39, 131	mulcomli 9650	. . . . . 6 |- ( 3 x. 8 ) = ; 2 4
133	60, 115, 100	addcomli 9825	. . . . . 6 |- ( 4 + 7 ) = ; 1 1
134	23, 7, 57, 132, 123, 9, 133	decaddci 11096	. . . . 5 |- ( ( 3 x. 8 ) + 7 ) = ; 3 1
135	9, 2, 18, 57, 112, 110, 6, 9, 2, 130, 134	decmac 11090	. . . 4 |- ( (; 1 3 x. 8 ) + 7 ) = ;; 1 1 1
136	7, 6, 18, 57, 109, 110, 111, 9, 79, 125, 135	decma2c 11091	. . 3 |- ( (; 1 3 x. ; 4 8 ) + 7 ) = ;; 6 3 1
137		7lt10 10814	. . . 4 |- 7 < 10
138	4, 2, 57, 137	declti 11076	. . 3 |- 7 < ; 1 3
139	107, 108, 53, 136, 138	ndvdsi 14391	. 2 |- -. ; 1 3 || ;; 6 3 1
140	9, 53	decnncl 11064	. . 3 |- ; 1 7 e. NN
141	2, 57	deccl 11065	. . 3 |- ; 3 7 e. NN0
142		2nn 10767	. . 3 |- 2 e. NN
143		eqid 2451	. . . 4 |- ; 3 7 = ; 3 7
144	23	dec0h 11067	. . . 4 |- 2 = ; 0 2
145	9, 57	deccl 11065	. . . 4 |- ; 1 7 e. NN0
146	9, 23	deccl 11065	. . . 4 |- ; 1 2 e. NN0
147		eqid 2451	. . . . 5 |- ; 1 7 = ; 1 7
148	146	nn0cni 10881	. . . . . 6 |- ; 1 2 e. CC
149	148	addid2i 9821	. . . . 5 |- ( 0 + ; 1 2 ) = ; 1 2
150	39	mulid2i 9646	. . . . . . 7 |- ( 1 x. 3 ) = 3
151		1p2e3 10734	. . . . . . 7 |- ( 1 + 2 ) = 3
152	150, 151	oveq12i 6302	. . . . . 6 |- ( ( 1 x. 3 ) + ( 1 + 2 ) ) = ( 3 + 3 )
153		3p3e6 10743	. . . . . 6 |- ( 3 + 3 ) = 6
154	152, 153	eqtri 2473	. . . . 5 |- ( ( 1 x. 3 ) + ( 1 + 2 ) ) = 6
155		7t3e21 11134	. . . . . 6 |- ( 7 x. 3 ) = ; 2 1
156	23, 9, 23, 155, 151	decaddi 11095	. . . . 5 |- ( ( 7 x. 3 ) + 2 ) = ; 2 3
157	9, 57, 9, 23, 147, 149, 2, 2, 23, 154, 156	decmac 11090	. . . 4 |- ( (; 1 7 x. 3 ) + ( 0 + ; 1 2 ) ) = ; 6 3
158	85	addid2i 9821	. . . . . . 7 |- ( 0 + 5 ) = 5
159	95, 158	oveq12i 6302	. . . . . 6 |- ( ( 1 x. 7 ) + ( 0 + 5 ) ) = ( 7 + 5 )
160		7p5e12 11104	. . . . . 6 |- ( 7 + 5 ) = ; 1 2
161	159, 160	eqtri 2473	. . . . 5 |- ( ( 1 x. 7 ) + ( 0 + 5 ) ) = ; 1 2
162		7t7e49 11138	. . . . . 6 |- ( 7 x. 7 ) = ; 4 9
163		4p1e5 10736	. . . . . 6 |- ( 4 + 1 ) = 5
164		9p2e11 11113	. . . . . 6 |- ( 9 + 2 ) = ; 1 1
165	7, 54, 23, 162, 163, 9, 164	decaddci 11096	. . . . 5 |- ( ( 7 x. 7 ) + 2 ) = ; 5 1
166	9, 57, 18, 23, 147, 144, 57, 9, 74, 161, 165	decmac 11090	. . . 4 |- ( (; 1 7 x. 7 ) + 2 ) = ;; 1 2 1
167	2, 57, 18, 23, 143, 144, 145, 9, 146, 157, 166	decma2c 11091	. . 3 |- ( (; 1 7 x. ; 3 7 ) + 2 ) = ;; 6 3 1
168		2lt10 10819	. . . 4 |- 2 < 10
169	4, 57, 23, 168	declti 11076	. . 3 |- 2 < ; 1 7
170	140, 141, 142, 167, 169	ndvdsi 14391	. 2 |- -. ; 1 7 || ;; 6 3 1
171		9nn 10774	. . . 4 |- 9 e. NN
172	9, 171	decnncl 11064	. . 3 |- ; 1 9 e. NN
173	2, 2	deccl 11065	. . 3 |- ; 3 3 e. NN0
174		eqid 2451	. . . 4 |- ; 3 3 = ; 3 3
175	9, 54	deccl 11065	. . . 4 |- ; 1 9 e. NN0
176		eqid 2451	. . . . 5 |- ; 1 9 = ; 1 9
177	34	addid2i 9821	. . . . . 6 |- ( 0 + 6 ) = 6
178	1	dec0h 11067	. . . . . 6 |- 6 = ; 0 6
179	177, 178	eqtri 2473	. . . . 5 |- ( 0 + 6 ) = ; 0 6
180	150, 127	oveq12i 6302	. . . . . 6 |- ( ( 1 x. 3 ) + ( 0 + 3 ) ) = ( 3 + 3 )
181	180, 153	eqtri 2473	. . . . 5 |- ( ( 1 x. 3 ) + ( 0 + 3 ) ) = 6
182		9t3e27 11147	. . . . . 6 |- ( 9 x. 3 ) = ; 2 7
183		7p6e13 11105	. . . . . 6 |- ( 7 + 6 ) = ; 1 3
184	23, 57, 1, 182, 123, 2, 183	decaddci 11096	. . . . 5 |- ( ( 9 x. 3 ) + 6 ) = ; 3 3
185	9, 54, 18, 1, 176, 179, 2, 2, 2, 181, 184	decmac 11090	. . . 4 |- ( (; 1 9 x. 3 ) + ( 0 + 6 ) ) = ; 6 3
186	23, 57, 7, 182, 123, 9, 100	decaddci 11096	. . . . 5 |- ( ( 9 x. 3 ) + 4 ) = ; 3 1
187	9, 54, 18, 7, 176, 78, 2, 9, 2, 181, 186	decmac 11090	. . . 4 |- ( (; 1 9 x. 3 ) + 4 ) = ; 6 1
188	2, 2, 18, 7, 174, 78, 175, 9, 1, 185, 187	decma2c 11091	. . 3 |- ( (; 1 9 x. ; 3 3 ) + 4 ) = ;; 6 3 1
189	4, 54, 7, 104	declti 11076	. . 3 |- 4 < ; 1 9
190	172, 173, 76, 188, 189	ndvdsi 14391	. 2 |- -. ; 1 9 || ;; 6 3 1
191	23, 15	decnncl 11064	. . 3 |- ; 2 3 e. NN
192	23, 57	deccl 11065	. . 3 |- ; 2 7 e. NN0
193		10nn 10775	. . 3 |- 10 e. NN
194		eqid 2451	. . . 4 |- ; 2 7 = ; 2 7
195		dec10 11081	. . . 4 |- 10 = ; 1 0
196	23, 2	deccl 11065	. . . 4 |- ; 2 3 e. NN0
197	9, 1	deccl 11065	. . . 4 |- ; 1 6 e. NN0
198		eqid 2451	. . . . 5 |- ; 2 3 = ; 2 3
199		eqid 2451	. . . . . 6 |- ; 1 6 = ; 1 6
200		ax-1cn 9597	. . . . . . 7 |- 1 e. CC
201		6p1e7 10738	. . . . . . 7 |- ( 6 + 1 ) = 7
202	34, 200, 201	addcomli 9825	. . . . . 6 |- ( 1 + 6 ) = 7
203	18, 9, 9, 1, 27, 199, 46, 202	decadd 11092	. . . . 5 |- ( 1 + ; 1 6 ) = ; 1 7
204		2t2e4 10759	. . . . . . 7 |- ( 2 x. 2 ) = 4
205	204, 117	oveq12i 6302	. . . . . 6 |- ( ( 2 x. 2 ) + ( 1 + 1 ) ) = ( 4 + 2 )
206	205, 119	eqtri 2473	. . . . 5 |- ( ( 2 x. 2 ) + ( 1 + 1 ) ) = 6
207	32	oveq1i 6300	. . . . . 6 |- ( ( 3 x. 2 ) + 7 ) = ( 6 + 7 )
208	60, 34, 183	addcomli 9825	. . . . . 6 |- ( 6 + 7 ) = ; 1 3
209	207, 208	eqtri 2473	. . . . 5 |- ( ( 3 x. 2 ) + 7 ) = ; 1 3
210	23, 2, 9, 57, 198, 203, 23, 2, 9, 206, 209	decmac 11090	. . . 4 |- ( (; 2 3 x. 2 ) + ( 1 + ; 1 6 ) ) = ; 6 3
211		7t2e14 11133	. . . . . . . . 9 |- ( 7 x. 2 ) = ; 1 4
212	60, 19, 211	mulcomli 9650	. . . . . . . 8 |- ( 2 x. 7 ) = ; 1 4
213	9, 7, 23, 212, 119	decaddi 11095	. . . . . . 7 |- ( ( 2 x. 7 ) + 2 ) = ; 1 6
214	60, 39, 155	mulcomli 9650	. . . . . . 7 |- ( 3 x. 7 ) = ; 2 1
215	57, 23, 2, 198, 9, 23, 213, 214	decmul1c 11098	. . . . . 6 |- (; 2 3 x. 7 ) = ;; 1 6 1
216	215	oveq1i 6300	. . . . 5 |- ( (; 2 3 x. 7 ) + 0 ) = (;; 1 6 1 + 0 )
217	197, 9	deccl 11065	. . . . . . 7 |- ;; 1 6 1 e. NN0
218	217	nn0cni 10881	. . . . . 6 |- ;; 1 6 1 e. CC
219	218	addid1i 9820	. . . . 5 |- (;; 1 6 1 + 0 ) = ;; 1 6 1
220	216, 219	eqtri 2473	. . . 4 |- ( (; 2 3 x. 7 ) + 0 ) = ;; 1 6 1
221	23, 57, 9, 18, 194, 195, 196, 9, 197, 210, 220	decma2c 11091	. . 3 |- ( (; 2 3 x. ; 2 7 ) + 10 ) = ;; 6 3 1
222		10pos 10712	. . . . 5 |- 0 < 10
223		1lt2 10776	. . . . 5 |- 1 < 2
224	9, 23, 18, 2, 222, 223	decltc 11073	. . . 4 |- ; 1 0 < ; 2 3
225	195, 224	eqbrtri 4422	. . 3 |- 10 < ; 2 3
226	191, 192, 193, 221, 225	ndvdsi 14391	. 2 |- -. ; 2 3 || ;; 6 3 1
227	5, 14, 17, 22, 50, 52, 72, 106, 139, 170, 190, 226	prmlem2 15091	1 |- ;; 6 3 1 e. Prime

Syntax hints:   e. wcel 1887  (class class class)co 6290   0cc0 9539   1c1 9540   + caddc 9542   x. cmul 9544   < clt 9675   2c2 10659   3c3 10660   4c4 10661   5c5 10662   6c6 10663   7c7 10664   8c8 10665   9c9 10666   10c10 10667  ;cdc 11051   Primecprime 14622

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-8 1889  ax-9 1896  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431  ax-sep 4525  ax-nul 4534  ax-pow 4581  ax-pr 4639  ax-un 6583  ax-cnex 9595  ax-resscn 9596  ax-1cn 9597  ax-icn 9598  ax-addcl 9599  ax-addrcl 9600  ax-mulcl 9601  ax-mulrcl 9602  ax-mulcom 9603  ax-addass 9604  ax-mulass 9605  ax-distr 9606  ax-i2m1 9607  ax-1ne0 9608  ax-1rid 9609  ax-rnegex 9610  ax-rrecex 9611  ax-cnre 9612  ax-pre-lttri 9613  ax-pre-lttrn 9614  ax-pre-ltadd 9615  ax-pre-mulgt0 9616  ax-pre-sup 9617

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 986  df-3an 987  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-eu 2303  df-mo 2304  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ne 2624  df-nel 2625  df-ral 2742  df-rex 2743  df-reu 2744  df-rmo 2745  df-rab 2746  df-v 3047  df-sbc 3268  df-csb 3364  df-dif 3407  df-un 3409  df-in 3411  df-ss 3418  df-pss 3420  df-nul 3732  df-if 3882  df-pw 3953  df-sn 3969  df-pr 3971  df-tp 3973  df-op 3975  df-uni 4199  df-int 4235  df-iun 4280  df-br 4403  df-opab 4462  df-mpt 4463  df-tr 4498  df-eprel 4745  df-id 4749  df-po 4755  df-so 4756  df-fr 4793  df-we 4795  df-xp 4840  df-rel 4841  df-cnv 4842  df-co 4843  df-dm 4844  df-rn 4845  df-res 4846  df-ima 4847  df-pred 5380  df-ord 5426  df-on 5427  df-lim 5428  df-suc 5429  df-iota 5546  df-fun 5584  df-fn 5585  df-f 5586  df-f1 5587  df-fo 5588  df-f1o 5589  df-fv 5590  df-riota 6252  df-ov 6293  df-oprab 6294  df-mpt2 6295  df-om 6693  df-1st 6793  df-2nd 6794  df-wrecs 7028  df-recs 7090  df-rdg 7128  df-1o 7182  df-2o 7183  df-oadd 7186  df-er 7363  df-en 7570  df-dom 7571  df-sdom 7572  df-fin 7573  df-sup 7956  df-inf 7957  df-pnf 9677  df-mnf 9678  df-xr 9679  df-ltxr 9680  df-le 9681  df-sub 9862  df-neg 9863  df-div 10270  df-nn 10610  df-2 10668  df-3 10669  df-4 10670  df-5 10671  df-6 10672  df-7 10673  df-8 10674  df-9 10675  df-10 10676  df-n0 10870  df-z 10938  df-dec 11052  df-uz 11160  df-rp 11303  df-fz 11785  df-seq 12214  df-exp 12273  df-cj 13162  df-re 13163  df-im 13164  df-sqrt 13298  df-abs 13299  df-dvds 14306  df-prm 14623

This theorem is referenced by: (None)