Theorem 631prm 15095

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 10896	. . . 4 |- 6 e. NN0
2		3nn0 10893	. . . 4 |- 3 e. NN0
3	1, 2	deccl 11071	. . 3 |- ; 6 3 e. NN0
4		1nn 10626	. . 3 |- 1 e. NN
5	3, 4	decnncl 11070	. 2 |- ;; 6 3 1 e. NN
6		8nn0 10898	. . . 4 |- 8 e. NN0
7		4nn0 10894	. . . 4 |- 4 e. NN0
8	6, 7	deccl 11071	. . 3 |- ; 8 4 e. NN0
9		1nn0 10891	. . 3 |- 1 e. NN0
10		1lt10 10826	. . 3 |- 1 < 10
11		3lt10 10824	. . . 4 |- 3 < 10
12		6lt8 10804	. . . 4 |- 6 < 8
13	1, 6, 2, 7, 11, 12	decltc 11079	. . 3 |- ; 6 3 < ; 8 4
14	3, 8, 9, 9, 10, 13	decltc 11079	. 2 |- ;; 6 3 1 < ;; 8 4 1
15		3nn 10774	. . . 4 |- 3 e. NN
16	1, 15	decnncl 11070	. . 3 |- ; 6 3 e. NN
17	16, 9, 9, 10	declti 11082	. 2 |- 1 < ;; 6 3 1
18		0nn0 10890	. . 3 |- 0 e. NN0
19		2cn 10686	. . . 4 |- 2 e. CC
20	19	mul02i 9828	. . 3 |- ( 0 x. 2 ) = 0
21		1e0p1 11085	. . 3 |- 1 = ( 0 + 1 )
22	3, 18, 20, 21	dec2dvds 15032	. 2 |- -. 2 || ;; 6 3 1
23		2nn0 10892	. . . . 5 |- 2 e. NN0
24	23, 9	deccl 11071	. . . 4 |- ; 2 1 e. NN0
25	24, 18	deccl 11071	. . 3 |- ;; 2 1 0 e. NN0
26		eqid 2423	. . . 4 |- ;; 2 1 0 = ;; 2 1 0
27	9	dec0h 11073	. . . 4 |- 1 = ; 0 1
28		eqid 2423	. . . . 5 |- ; 2 1 = ; 2 1
29		00id 9814	. . . . . 6 |- ( 0 + 0 ) = 0
30	18	dec0h 11073	. . . . . 6 |- 0 = ; 0 0
31	29, 30	eqtri 2452	. . . . 5 |- ( 0 + 0 ) = ; 0 0
32		3t2e6 10767	. . . . . . 7 |- ( 3 x. 2 ) = 6
33	32, 29	oveq12i 6316	. . . . . 6 |- ( ( 3 x. 2 ) + ( 0 + 0 ) ) = ( 6 + 0 )
34		6cn 10697	. . . . . . 7 |- 6 e. CC
35	34	addid1i 9826	. . . . . 6 |- ( 6 + 0 ) = 6
36	33, 35	eqtri 2452	. . . . 5 |- ( ( 3 x. 2 ) + ( 0 + 0 ) ) = 6
37		3t1e3 10766	. . . . . . 7 |- ( 3 x. 1 ) = 3
38	37	oveq1i 6314	. . . . . 6 |- ( ( 3 x. 1 ) + 0 ) = ( 3 + 0 )
39		3cn 10690	. . . . . . 7 |- 3 e. CC
40	39	addid1i 9826	. . . . . 6 |- ( 3 + 0 ) = 3
41	2	dec0h 11073	. . . . . 6 |- 3 = ; 0 3
42	38, 40, 41	3eqtri 2456	. . . . 5 |- ( ( 3 x. 1 ) + 0 ) = ; 0 3
43	23, 9, 18, 18, 28, 31, 2, 2, 18, 36, 42	decma2c 11097	. . . 4 |- ( ( 3 x. ; 2 1 ) + ( 0 + 0 ) ) = ; 6 3
44	39	mul01i 9829	. . . . . 6 |- ( 3 x. 0 ) = 0
45	44	oveq1i 6314	. . . . 5 |- ( ( 3 x. 0 ) + 1 ) = ( 0 + 1 )
46		0p1e1 10727	. . . . 5 |- ( 0 + 1 ) = 1
47	45, 46, 27	3eqtri 2456	. . . 4 |- ( ( 3 x. 0 ) + 1 ) = ; 0 1
48	24, 18, 18, 9, 26, 27, 2, 9, 18, 43, 47	decma2c 11097	. . 3 |- ( ( 3 x. ;; 2 1 0 ) + 1 ) = ;; 6 3 1
49		1lt3 10784	. . 3 |- 1 < 3
50	15, 25, 4, 48, 49	ndvdsi 14388	. 2 |- -. 3 || ;; 6 3 1
51		1lt5 10791	. . 3 |- 1 < 5
52	3, 4, 51	dec5dvds 15033	. 2 |- -. 5 || ;; 6 3 1
53		7nn 10778	. . 3 |- 7 e. NN
54		9nn0 10899	. . . 4 |- 9 e. NN0
55	54, 18	deccl 11071	. . 3 |- ; 9 0 e. NN0
56		eqid 2423	. . . 4 |- ; 9 0 = ; 9 0
57		7nn0 10897	. . . 4 |- 7 e. NN0
58	29	oveq2i 6315	. . . . 5 |- ( ( 7 x. 9 ) + ( 0 + 0 ) ) = ( ( 7 x. 9 ) + 0 )
59		9cn 10703	. . . . . . 7 |- 9 e. CC
60		7cn 10699	. . . . . . 7 |- 7 e. CC
61		9t7e63 11157	. . . . . . 7 |- ( 9 x. 7 ) = ; 6 3
62	59, 60, 61	mulcomli 9656	. . . . . 6 |- ( 7 x. 9 ) = ; 6 3
63	62	oveq1i 6314	. . . . 5 |- ( ( 7 x. 9 ) + 0 ) = (; 6 3 + 0 )
64	3	nn0cni 10887	. . . . . 6 |- ; 6 3 e. CC
65	64	addid1i 9826	. . . . 5 |- (; 6 3 + 0 ) = ; 6 3
66	58, 63, 65	3eqtri 2456	. . . 4 |- ( ( 7 x. 9 ) + ( 0 + 0 ) ) = ; 6 3
67	60	mul01i 9829	. . . . . 6 |- ( 7 x. 0 ) = 0
68	67	oveq1i 6314	. . . . 5 |- ( ( 7 x. 0 ) + 1 ) = ( 0 + 1 )
69	68, 46, 27	3eqtri 2456	. . . 4 |- ( ( 7 x. 0 ) + 1 ) = ; 0 1
70	54, 18, 18, 9, 56, 27, 57, 9, 18, 66, 69	decma2c 11097	. . 3 |- ( ( 7 x. ; 9 0 ) + 1 ) = ;; 6 3 1
71		1lt7 10802	. . 3 |- 1 < 7
72	53, 55, 4, 70, 71	ndvdsi 14388	. 2 |- -. 7 || ;; 6 3 1
73	9, 4	decnncl 11070	. . 3 |- ; 1 1 e. NN
74		5nn0 10895	. . . 4 |- 5 e. NN0
75	74, 57	deccl 11071	. . 3 |- ; 5 7 e. NN0
76		4nn 10775	. . 3 |- 4 e. NN
77		eqid 2423	. . . 4 |- ; 5 7 = ; 5 7
78	7	dec0h 11073	. . . 4 |- 4 = ; 0 4
79	9, 9	deccl 11071	. . . 4 |- ; 1 1 e. NN0
80		eqid 2423	. . . . 5 |- ; 1 1 = ; 1 1
81		8cn 10701	. . . . . . 7 |- 8 e. CC
82	81	addid2i 9827	. . . . . 6 |- ( 0 + 8 ) = 8
83	6	dec0h 11073	. . . . . 6 |- 8 = ; 0 8
84	82, 83	eqtri 2452	. . . . 5 |- ( 0 + 8 ) = ; 0 8
85		5cn 10695	. . . . . . . 8 |- 5 e. CC
86	85	mulid2i 9652	. . . . . . 7 |- ( 1 x. 5 ) = 5
87	86, 46	oveq12i 6316	. . . . . 6 |- ( ( 1 x. 5 ) + ( 0 + 1 ) ) = ( 5 + 1 )
88		5p1e6 10743	. . . . . 6 |- ( 5 + 1 ) = 6
89	87, 88	eqtri 2452	. . . . 5 |- ( ( 1 x. 5 ) + ( 0 + 1 ) ) = 6
90	86	oveq1i 6314	. . . . . 6 |- ( ( 1 x. 5 ) + 8 ) = ( 5 + 8 )
91		8p5e13 11115	. . . . . . 7 |- ( 8 + 5 ) = ; 1 3
92	81, 85, 91	addcomli 9831	. . . . . 6 |- ( 5 + 8 ) = ; 1 3
93	90, 92	eqtri 2452	. . . . 5 |- ( ( 1 x. 5 ) + 8 ) = ; 1 3
94	9, 9, 18, 6, 80, 84, 74, 2, 9, 89, 93	decmac 11096	. . . 4 |- ( (; 1 1 x. 5 ) + ( 0 + 8 ) ) = ; 6 3
95	60	mulid2i 9652	. . . . . . 7 |- ( 1 x. 7 ) = 7
96	95, 46	oveq12i 6316	. . . . . 6 |- ( ( 1 x. 7 ) + ( 0 + 1 ) ) = ( 7 + 1 )
97		7p1e8 10745	. . . . . 6 |- ( 7 + 1 ) = 8
98	96, 97	eqtri 2452	. . . . 5 |- ( ( 1 x. 7 ) + ( 0 + 1 ) ) = 8
99	95	oveq1i 6314	. . . . . 6 |- ( ( 1 x. 7 ) + 4 ) = ( 7 + 4 )
100		7p4e11 11109	. . . . . 6 |- ( 7 + 4 ) = ; 1 1
101	99, 100	eqtri 2452	. . . . 5 |- ( ( 1 x. 7 ) + 4 ) = ; 1 1
102	9, 9, 18, 7, 80, 78, 57, 9, 9, 98, 101	decmac 11096	. . . 4 |- ( (; 1 1 x. 7 ) + 4 ) = ; 8 1
103	74, 57, 18, 7, 77, 78, 79, 9, 6, 94, 102	decma2c 11097	. . 3 |- ( (; 1 1 x. ; 5 7 ) + 4 ) = ;; 6 3 1
104		4lt10 10823	. . . 4 |- 4 < 10
105	4, 9, 7, 104	declti 11082	. . 3 |- 4 < ; 1 1
106	73, 75, 76, 103, 105	ndvdsi 14388	. 2 |- -. ; 1 1 || ;; 6 3 1
107	9, 15	decnncl 11070	. . 3 |- ; 1 3 e. NN
108	7, 6	deccl 11071	. . 3 |- ; 4 8 e. NN0
109		eqid 2423	. . . 4 |- ; 4 8 = ; 4 8
110	57	dec0h 11073	. . . 4 |- 7 = ; 0 7
111	9, 2	deccl 11071	. . . 4 |- ; 1 3 e. NN0
112		eqid 2423	. . . . 5 |- ; 1 3 = ; 1 3
113	79	nn0cni 10887	. . . . . 6 |- ; 1 1 e. CC
114	113	addid2i 9827	. . . . 5 |- ( 0 + ; 1 1 ) = ; 1 1
115		4cn 10693	. . . . . . . 8 |- 4 e. CC
116	115	mulid2i 9652	. . . . . . 7 |- ( 1 x. 4 ) = 4
117		1p1e2 10729	. . . . . . 7 |- ( 1 + 1 ) = 2
118	116, 117	oveq12i 6316	. . . . . 6 |- ( ( 1 x. 4 ) + ( 1 + 1 ) ) = ( 4 + 2 )
119		4p2e6 10750	. . . . . 6 |- ( 4 + 2 ) = 6
120	118, 119	eqtri 2452	. . . . 5 |- ( ( 1 x. 4 ) + ( 1 + 1 ) ) = 6
121		4t3e12 11129	. . . . . . 7 |- ( 4 x. 3 ) = ; 1 2
122	115, 39, 121	mulcomli 9656	. . . . . 6 |- ( 3 x. 4 ) = ; 1 2
123		2p1e3 10739	. . . . . 6 |- ( 2 + 1 ) = 3
124	9, 23, 9, 122, 123	decaddi 11101	. . . . 5 |- ( ( 3 x. 4 ) + 1 ) = ; 1 3
125	9, 2, 9, 9, 112, 114, 7, 2, 9, 120, 124	decmac 11096	. . . 4 |- ( (; 1 3 x. 4 ) + ( 0 + ; 1 1 ) ) = ; 6 3
126	81	mulid2i 9652	. . . . . . 7 |- ( 1 x. 8 ) = 8
127	39	addid2i 9827	. . . . . . 7 |- ( 0 + 3 ) = 3
128	126, 127	oveq12i 6316	. . . . . 6 |- ( ( 1 x. 8 ) + ( 0 + 3 ) ) = ( 8 + 3 )
129		8p3e11 11113	. . . . . 6 |- ( 8 + 3 ) = ; 1 1
130	128, 129	eqtri 2452	. . . . 5 |- ( ( 1 x. 8 ) + ( 0 + 3 ) ) = ; 1 1
131		8t3e24 11146	. . . . . . 7 |- ( 8 x. 3 ) = ; 2 4
132	81, 39, 131	mulcomli 9656	. . . . . 6 |- ( 3 x. 8 ) = ; 2 4
133	60, 115, 100	addcomli 9831	. . . . . 6 |- ( 4 + 7 ) = ; 1 1
134	23, 7, 57, 132, 123, 9, 133	decaddci 11102	. . . . 5 |- ( ( 3 x. 8 ) + 7 ) = ; 3 1
135	9, 2, 18, 57, 112, 110, 6, 9, 2, 130, 134	decmac 11096	. . . 4 |- ( (; 1 3 x. 8 ) + 7 ) = ;; 1 1 1
136	7, 6, 18, 57, 109, 110, 111, 9, 79, 125, 135	decma2c 11097	. . 3 |- ( (; 1 3 x. ; 4 8 ) + 7 ) = ;; 6 3 1
137		7lt10 10820	. . . 4 |- 7 < 10
138	4, 2, 57, 137	declti 11082	. . 3 |- 7 < ; 1 3
139	107, 108, 53, 136, 138	ndvdsi 14388	. 2 |- -. ; 1 3 || ;; 6 3 1
140	9, 53	decnncl 11070	. . 3 |- ; 1 7 e. NN
141	2, 57	deccl 11071	. . 3 |- ; 3 7 e. NN0
142		2nn 10773	. . 3 |- 2 e. NN
143		eqid 2423	. . . 4 |- ; 3 7 = ; 3 7
144	23	dec0h 11073	. . . 4 |- 2 = ; 0 2
145	9, 57	deccl 11071	. . . 4 |- ; 1 7 e. NN0
146	9, 23	deccl 11071	. . . 4 |- ; 1 2 e. NN0
147		eqid 2423	. . . . 5 |- ; 1 7 = ; 1 7
148	146	nn0cni 10887	. . . . . 6 |- ; 1 2 e. CC
149	148	addid2i 9827	. . . . 5 |- ( 0 + ; 1 2 ) = ; 1 2
150	39	mulid2i 9652	. . . . . . 7 |- ( 1 x. 3 ) = 3
151		1p2e3 10740	. . . . . . 7 |- ( 1 + 2 ) = 3
152	150, 151	oveq12i 6316	. . . . . 6 |- ( ( 1 x. 3 ) + ( 1 + 2 ) ) = ( 3 + 3 )
153		3p3e6 10749	. . . . . 6 |- ( 3 + 3 ) = 6
154	152, 153	eqtri 2452	. . . . 5 |- ( ( 1 x. 3 ) + ( 1 + 2 ) ) = 6
155		7t3e21 11140	. . . . . 6 |- ( 7 x. 3 ) = ; 2 1
156	23, 9, 23, 155, 151	decaddi 11101	. . . . 5 |- ( ( 7 x. 3 ) + 2 ) = ; 2 3
157	9, 57, 9, 23, 147, 149, 2, 2, 23, 154, 156	decmac 11096	. . . 4 |- ( (; 1 7 x. 3 ) + ( 0 + ; 1 2 ) ) = ; 6 3
158	85	addid2i 9827	. . . . . . 7 |- ( 0 + 5 ) = 5
159	95, 158	oveq12i 6316	. . . . . 6 |- ( ( 1 x. 7 ) + ( 0 + 5 ) ) = ( 7 + 5 )
160		7p5e12 11110	. . . . . 6 |- ( 7 + 5 ) = ; 1 2
161	159, 160	eqtri 2452	. . . . 5 |- ( ( 1 x. 7 ) + ( 0 + 5 ) ) = ; 1 2
162		7t7e49 11144	. . . . . 6 |- ( 7 x. 7 ) = ; 4 9
163		4p1e5 10742	. . . . . 6 |- ( 4 + 1 ) = 5
164		9p2e11 11119	. . . . . 6 |- ( 9 + 2 ) = ; 1 1
165	7, 54, 23, 162, 163, 9, 164	decaddci 11102	. . . . 5 |- ( ( 7 x. 7 ) + 2 ) = ; 5 1
166	9, 57, 18, 23, 147, 144, 57, 9, 74, 161, 165	decmac 11096	. . . 4 |- ( (; 1 7 x. 7 ) + 2 ) = ;; 1 2 1
167	2, 57, 18, 23, 143, 144, 145, 9, 146, 157, 166	decma2c 11097	. . 3 |- ( (; 1 7 x. ; 3 7 ) + 2 ) = ;; 6 3 1
168		2lt10 10825	. . . 4 |- 2 < 10
169	4, 57, 23, 168	declti 11082	. . 3 |- 2 < ; 1 7
170	140, 141, 142, 167, 169	ndvdsi 14388	. 2 |- -. ; 1 7 || ;; 6 3 1
171		9nn 10780	. . . 4 |- 9 e. NN
172	9, 171	decnncl 11070	. . 3 |- ; 1 9 e. NN
173	2, 2	deccl 11071	. . 3 |- ; 3 3 e. NN0
174		eqid 2423	. . . 4 |- ; 3 3 = ; 3 3
175	9, 54	deccl 11071	. . . 4 |- ; 1 9 e. NN0
176		eqid 2423	. . . . 5 |- ; 1 9 = ; 1 9
177	34	addid2i 9827	. . . . . 6 |- ( 0 + 6 ) = 6
178	1	dec0h 11073	. . . . . 6 |- 6 = ; 0 6
179	177, 178	eqtri 2452	. . . . 5 |- ( 0 + 6 ) = ; 0 6
180	150, 127	oveq12i 6316	. . . . . 6 |- ( ( 1 x. 3 ) + ( 0 + 3 ) ) = ( 3 + 3 )
181	180, 153	eqtri 2452	. . . . 5 |- ( ( 1 x. 3 ) + ( 0 + 3 ) ) = 6
182		9t3e27 11153	. . . . . 6 |- ( 9 x. 3 ) = ; 2 7
183		7p6e13 11111	. . . . . 6 |- ( 7 + 6 ) = ; 1 3
184	23, 57, 1, 182, 123, 2, 183	decaddci 11102	. . . . 5 |- ( ( 9 x. 3 ) + 6 ) = ; 3 3
185	9, 54, 18, 1, 176, 179, 2, 2, 2, 181, 184	decmac 11096	. . . 4 |- ( (; 1 9 x. 3 ) + ( 0 + 6 ) ) = ; 6 3
186	23, 57, 7, 182, 123, 9, 100	decaddci 11102	. . . . 5 |- ( ( 9 x. 3 ) + 4 ) = ; 3 1
187	9, 54, 18, 7, 176, 78, 2, 9, 2, 181, 186	decmac 11096	. . . 4 |- ( (; 1 9 x. 3 ) + 4 ) = ; 6 1
188	2, 2, 18, 7, 174, 78, 175, 9, 1, 185, 187	decma2c 11097	. . 3 |- ( (; 1 9 x. ; 3 3 ) + 4 ) = ;; 6 3 1
189	4, 54, 7, 104	declti 11082	. . 3 |- 4 < ; 1 9
190	172, 173, 76, 188, 189	ndvdsi 14388	. 2 |- -. ; 1 9 || ;; 6 3 1
191	23, 15	decnncl 11070	. . 3 |- ; 2 3 e. NN
192	23, 57	deccl 11071	. . 3 |- ; 2 7 e. NN0
193		10nn 10781	. . 3 |- 10 e. NN
194		eqid 2423	. . . 4 |- ; 2 7 = ; 2 7
195		dec10 11087	. . . 4 |- 10 = ; 1 0
196	23, 2	deccl 11071	. . . 4 |- ; 2 3 e. NN0
197	9, 1	deccl 11071	. . . 4 |- ; 1 6 e. NN0
198		eqid 2423	. . . . 5 |- ; 2 3 = ; 2 3
199		eqid 2423	. . . . . 6 |- ; 1 6 = ; 1 6
200		ax-1cn 9603	. . . . . . 7 |- 1 e. CC
201		6p1e7 10744	. . . . . . 7 |- ( 6 + 1 ) = 7
202	34, 200, 201	addcomli 9831	. . . . . 6 |- ( 1 + 6 ) = 7
203	18, 9, 9, 1, 27, 199, 46, 202	decadd 11098	. . . . 5 |- ( 1 + ; 1 6 ) = ; 1 7
204		2t2e4 10765	. . . . . . 7 |- ( 2 x. 2 ) = 4
205	204, 117	oveq12i 6316	. . . . . 6 |- ( ( 2 x. 2 ) + ( 1 + 1 ) ) = ( 4 + 2 )
206	205, 119	eqtri 2452	. . . . 5 |- ( ( 2 x. 2 ) + ( 1 + 1 ) ) = 6
207	32	oveq1i 6314	. . . . . 6 |- ( ( 3 x. 2 ) + 7 ) = ( 6 + 7 )
208	60, 34, 183	addcomli 9831	. . . . . 6 |- ( 6 + 7 ) = ; 1 3
209	207, 208	eqtri 2452	. . . . 5 |- ( ( 3 x. 2 ) + 7 ) = ; 1 3
210	23, 2, 9, 57, 198, 203, 23, 2, 9, 206, 209	decmac 11096	. . . 4 |- ( (; 2 3 x. 2 ) + ( 1 + ; 1 6 ) ) = ; 6 3
211		7t2e14 11139	. . . . . . . . 9 |- ( 7 x. 2 ) = ; 1 4
212	60, 19, 211	mulcomli 9656	. . . . . . . 8 |- ( 2 x. 7 ) = ; 1 4
213	9, 7, 23, 212, 119	decaddi 11101	. . . . . . 7 |- ( ( 2 x. 7 ) + 2 ) = ; 1 6
214	60, 39, 155	mulcomli 9656	. . . . . . 7 |- ( 3 x. 7 ) = ; 2 1
215	57, 23, 2, 198, 9, 23, 213, 214	decmul1c 11104	. . . . . 6 |- (; 2 3 x. 7 ) = ;; 1 6 1
216	215	oveq1i 6314	. . . . 5 |- ( (; 2 3 x. 7 ) + 0 ) = (;; 1 6 1 + 0 )
217	197, 9	deccl 11071	. . . . . . 7 |- ;; 1 6 1 e. NN0
218	217	nn0cni 10887	. . . . . 6 |- ;; 1 6 1 e. CC
219	218	addid1i 9826	. . . . 5 |- (;; 1 6 1 + 0 ) = ;; 1 6 1
220	216, 219	eqtri 2452	. . . 4 |- ( (; 2 3 x. 7 ) + 0 ) = ;; 1 6 1
221	23, 57, 9, 18, 194, 195, 196, 9, 197, 210, 220	decma2c 11097	. . 3 |- ( (; 2 3 x. ; 2 7 ) + 10 ) = ;; 6 3 1
222		10pos 10718	. . . . 5 |- 0 < 10
223		1lt2 10782	. . . . 5 |- 1 < 2
224	9, 23, 18, 2, 222, 223	decltc 11079	. . . 4 |- ; 1 0 < ; 2 3
225	195, 224	eqbrtri 4442	. . 3 |- 10 < ; 2 3
226	191, 192, 193, 221, 225	ndvdsi 14388	. 2 |- -. ; 2 3 || ;; 6 3 1
227	5, 14, 17, 22, 50, 52, 72, 106, 139, 170, 190, 226	prmlem2 15088	1 |- ;; 6 3 1 e. Prime

Syntax hints:   e. wcel 1869  (class class class)co 6304   0cc0 9545   1c1 9546   + caddc 9548   x. cmul 9550   < clt 9681   2c2 10665   3c3 10666   4c4 10667   5c5 10668   6c6 10669   7c7 10670   8c8 10671   9c9 10672   10c10 10673  ;cdc 11057   Primecprime 14619

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-8 1871  ax-9 1873  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401  ax-sep 4545  ax-nul 4554  ax-pow 4601  ax-pr 4659  ax-un 6596  ax-cnex 9601  ax-resscn 9602  ax-1cn 9603  ax-icn 9604  ax-addcl 9605  ax-addrcl 9606  ax-mulcl 9607  ax-mulrcl 9608  ax-mulcom 9609  ax-addass 9610  ax-mulass 9611  ax-distr 9612  ax-i2m1 9613  ax-1ne0 9614  ax-1rid 9615  ax-rnegex 9616  ax-rrecex 9617  ax-cnre 9618  ax-pre-lttri 9619  ax-pre-lttrn 9620  ax-pre-ltadd 9621  ax-pre-mulgt0 9622  ax-pre-sup 9623

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 984  df-3an 985  df-tru 1441  df-ex 1661  df-nf 1665  df-sb 1788  df-eu 2270  df-mo 2271  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2573  df-ne 2621  df-nel 2622  df-ral 2781  df-rex 2782  df-reu 2783  df-rmo 2784  df-rab 2785  df-v 3084  df-sbc 3302  df-csb 3398  df-dif 3441  df-un 3443  df-in 3445  df-ss 3452  df-pss 3454  df-nul 3764  df-if 3912  df-pw 3983  df-sn 3999  df-pr 4001  df-tp 4003  df-op 4005  df-uni 4219  df-int 4255  df-iun 4300  df-br 4423  df-opab 4482  df-mpt 4483  df-tr 4518  df-eprel 4763  df-id 4767  df-po 4773  df-so 4774  df-fr 4811  df-we 4813  df-xp 4858  df-rel 4859  df-cnv 4860  df-co 4861  df-dm 4862  df-rn 4863  df-res 4864  df-ima 4865  df-pred 5398  df-ord 5444  df-on 5445  df-lim 5446  df-suc 5447  df-iota 5564  df-fun 5602  df-fn 5603  df-f 5604  df-f1 5605  df-fo 5606  df-f1o 5607  df-fv 5608  df-riota 6266  df-ov 6307  df-oprab 6308  df-mpt2 6309  df-om 6706  df-1st 6806  df-2nd 6807  df-wrecs 7038  df-recs 7100  df-rdg 7138  df-1o 7192  df-2o 7193  df-oadd 7196  df-er 7373  df-en 7580  df-dom 7581  df-sdom 7582  df-fin 7583  df-sup 7964  df-inf 7965  df-pnf 9683  df-mnf 9684  df-xr 9685  df-ltxr 9686  df-le 9687  df-sub 9868  df-neg 9869  df-div 10276  df-nn 10616  df-2 10674  df-3 10675  df-4 10676  df-5 10677  df-6 10678  df-7 10679  df-8 10680  df-9 10681  df-10 10682  df-n0 10876  df-z 10944  df-dec 11058  df-uz 11166  df-rp 11309  df-fz 11791  df-seq 12219  df-exp 12278  df-cj 13160  df-re 13161  df-im 13162  df-sqrt 13296  df-abs 13297  df-dvds 14303  df-prm 14620

This theorem is referenced by: (None)