Theorem 631prm 14136

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 10587	. . . 4 |- 6 e. NN0
2		3nn0 10584	. . . 4 |- 3 e. NN0
3	1, 2	deccl 10756	. . 3 |- ; 6 3 e. NN0
4		1nn 10320	. . 3 |- 1 e. NN
5	3, 4	decnncl 10755	. 2 |- ;; 6 3 1 e. NN
6		8nn0 10589	. . . 4 |- 8 e. NN0
7		4nn0 10585	. . . 4 |- 4 e. NN0
8	6, 7	deccl 10756	. . 3 |- ; 8 4 e. NN0
9		1nn0 10582	. . 3 |- 1 e. NN0
10		1lt10 10519	. . 3 |- 1 < 10
11		3lt10 10517	. . . 4 |- 3 < 10
12		6lt8 10497	. . . 4 |- 6 < 8
13	1, 6, 2, 7, 11, 12	decltc 10764	. . 3 |- ; 6 3 < ; 8 4
14	3, 8, 9, 9, 10, 13	decltc 10764	. 2 |- ;; 6 3 1 < ;; 8 4 1
15		3nn 10467	. . . 4 |- 3 e. NN
16	1, 15	decnncl 10755	. . 3 |- ; 6 3 e. NN
17	16, 9, 9, 10	declti 10767	. 2 |- 1 < ;; 6 3 1
18		0nn0 10581	. . 3 |- 0 e. NN0
19		2cn 10379	. . . 4 |- 2 e. CC
20	19	mul02i 9545	. . 3 |- ( 0 x. 2 ) = 0
21		1e0p1 10770	. . 3 |- 1 = ( 0 + 1 )
22	3, 18, 20, 21	dec2dvds 14074	. 2 |- -. 2 || ;; 6 3 1
23		2nn0 10583	. . . . 5 |- 2 e. NN0
24	23, 9	deccl 10756	. . . 4 |- ; 2 1 e. NN0
25	24, 18	deccl 10756	. . 3 |- ;; 2 1 0 e. NN0
26		eqid 2433	. . . 4 |- ;; 2 1 0 = ;; 2 1 0
27	9	dec0h 10758	. . . 4 |- 1 = ; 0 1
28		eqid 2433	. . . . 5 |- ; 2 1 = ; 2 1
29		00id 9531	. . . . . 6 |- ( 0 + 0 ) = 0
30	18	dec0h 10758	. . . . . 6 |- 0 = ; 0 0
31	29, 30	eqtri 2453	. . . . 5 |- ( 0 + 0 ) = ; 0 0
32		3t2e6 10460	. . . . . . 7 |- ( 3 x. 2 ) = 6
33	32, 29	oveq12i 6092	. . . . . 6 |- ( ( 3 x. 2 ) + ( 0 + 0 ) ) = ( 6 + 0 )
34		6cn 10390	. . . . . . 7 |- 6 e. CC
35	34	addid1i 9543	. . . . . 6 |- ( 6 + 0 ) = 6
36	33, 35	eqtri 2453	. . . . 5 |- ( ( 3 x. 2 ) + ( 0 + 0 ) ) = 6
37		3t1e3 10459	. . . . . . 7 |- ( 3 x. 1 ) = 3
38	37	oveq1i 6090	. . . . . 6 |- ( ( 3 x. 1 ) + 0 ) = ( 3 + 0 )
39		3cn 10383	. . . . . . 7 |- 3 e. CC
40	39	addid1i 9543	. . . . . 6 |- ( 3 + 0 ) = 3
41	2	dec0h 10758	. . . . . 6 |- 3 = ; 0 3
42	38, 40, 41	3eqtri 2457	. . . . 5 |- ( ( 3 x. 1 ) + 0 ) = ; 0 3
43	23, 9, 18, 18, 28, 31, 2, 2, 18, 36, 42	decma2c 10782	. . . 4 |- ( ( 3 x. ; 2 1 ) + ( 0 + 0 ) ) = ; 6 3
44	39	mul01i 9546	. . . . . 6 |- ( 3 x. 0 ) = 0
45	44	oveq1i 6090	. . . . 5 |- ( ( 3 x. 0 ) + 1 ) = ( 0 + 1 )
46		0p1e1 10420	. . . . 5 |- ( 0 + 1 ) = 1
47	45, 46, 27	3eqtri 2457	. . . 4 |- ( ( 3 x. 0 ) + 1 ) = ; 0 1
48	24, 18, 18, 9, 26, 27, 2, 9, 18, 43, 47	decma2c 10782	. . 3 |- ( ( 3 x. ;; 2 1 0 ) + 1 ) = ;; 6 3 1
49		1lt3 10477	. . 3 |- 1 < 3
50	15, 25, 4, 48, 49	ndvdsi 13596	. 2 |- -. 3 || ;; 6 3 1
51		1lt5 10484	. . 3 |- 1 < 5
52	3, 4, 51	dec5dvds 14075	. 2 |- -. 5 || ;; 6 3 1
53		7nn 10471	. . 3 |- 7 e. NN
54		9nn0 10590	. . . 4 |- 9 e. NN0
55	54, 18	deccl 10756	. . 3 |- ; 9 0 e. NN0
56		eqid 2433	. . . 4 |- ; 9 0 = ; 9 0
57		7nn0 10588	. . . 4 |- 7 e. NN0
58	29	oveq2i 6091	. . . . 5 |- ( ( 7 x. 9 ) + ( 0 + 0 ) ) = ( ( 7 x. 9 ) + 0 )
59		9cn 10396	. . . . . . 7 |- 9 e. CC
60		7cn 10392	. . . . . . 7 |- 7 e. CC
61		9t7e63 10842	. . . . . . 7 |- ( 9 x. 7 ) = ; 6 3
62	59, 60, 61	mulcomli 9380	. . . . . 6 |- ( 7 x. 9 ) = ; 6 3
63	62	oveq1i 6090	. . . . 5 |- ( ( 7 x. 9 ) + 0 ) = (; 6 3 + 0 )
64	3	nn0cni 10578	. . . . . 6 |- ; 6 3 e. CC
65	64	addid1i 9543	. . . . 5 |- (; 6 3 + 0 ) = ; 6 3
66	58, 63, 65	3eqtri 2457	. . . 4 |- ( ( 7 x. 9 ) + ( 0 + 0 ) ) = ; 6 3
67	60	mul01i 9546	. . . . . 6 |- ( 7 x. 0 ) = 0
68	67	oveq1i 6090	. . . . 5 |- ( ( 7 x. 0 ) + 1 ) = ( 0 + 1 )
69	68, 46, 27	3eqtri 2457	. . . 4 |- ( ( 7 x. 0 ) + 1 ) = ; 0 1
70	54, 18, 18, 9, 56, 27, 57, 9, 18, 66, 69	decma2c 10782	. . 3 |- ( ( 7 x. ; 9 0 ) + 1 ) = ;; 6 3 1
71		1lt7 10495	. . 3 |- 1 < 7
72	53, 55, 4, 70, 71	ndvdsi 13596	. 2 |- -. 7 || ;; 6 3 1
73	9, 4	decnncl 10755	. . 3 |- ; 1 1 e. NN
74		5nn0 10586	. . . 4 |- 5 e. NN0
75	74, 57	deccl 10756	. . 3 |- ; 5 7 e. NN0
76		4nn 10468	. . 3 |- 4 e. NN
77		eqid 2433	. . . 4 |- ; 5 7 = ; 5 7
78	7	dec0h 10758	. . . 4 |- 4 = ; 0 4
79	9, 9	deccl 10756	. . . 4 |- ; 1 1 e. NN0
80		eqid 2433	. . . . 5 |- ; 1 1 = ; 1 1
81		8cn 10394	. . . . . . 7 |- 8 e. CC
82	81	addid2i 9544	. . . . . 6 |- ( 0 + 8 ) = 8
83	6	dec0h 10758	. . . . . 6 |- 8 = ; 0 8
84	82, 83	eqtri 2453	. . . . 5 |- ( 0 + 8 ) = ; 0 8
85		5cn 10388	. . . . . . . 8 |- 5 e. CC
86	85	mulid2i 9376	. . . . . . 7 |- ( 1 x. 5 ) = 5
87	86, 46	oveq12i 6092	. . . . . 6 |- ( ( 1 x. 5 ) + ( 0 + 1 ) ) = ( 5 + 1 )
88		5p1e6 10436	. . . . . 6 |- ( 5 + 1 ) = 6
89	87, 88	eqtri 2453	. . . . 5 |- ( ( 1 x. 5 ) + ( 0 + 1 ) ) = 6
90	86	oveq1i 6090	. . . . . 6 |- ( ( 1 x. 5 ) + 8 ) = ( 5 + 8 )
91		8p5e13 10800	. . . . . . 7 |- ( 8 + 5 ) = ; 1 3
92	81, 85, 91	addcomli 9548	. . . . . 6 |- ( 5 + 8 ) = ; 1 3
93	90, 92	eqtri 2453	. . . . 5 |- ( ( 1 x. 5 ) + 8 ) = ; 1 3
94	9, 9, 18, 6, 80, 84, 74, 2, 9, 89, 93	decmac 10781	. . . 4 |- ( (; 1 1 x. 5 ) + ( 0 + 8 ) ) = ; 6 3
95	60	mulid2i 9376	. . . . . . 7 |- ( 1 x. 7 ) = 7
96	95, 46	oveq12i 6092	. . . . . 6 |- ( ( 1 x. 7 ) + ( 0 + 1 ) ) = ( 7 + 1 )
97		7p1e8 10438	. . . . . 6 |- ( 7 + 1 ) = 8
98	96, 97	eqtri 2453	. . . . 5 |- ( ( 1 x. 7 ) + ( 0 + 1 ) ) = 8
99	95	oveq1i 6090	. . . . . 6 |- ( ( 1 x. 7 ) + 4 ) = ( 7 + 4 )
100		7p4e11 10794	. . . . . 6 |- ( 7 + 4 ) = ; 1 1
101	99, 100	eqtri 2453	. . . . 5 |- ( ( 1 x. 7 ) + 4 ) = ; 1 1
102	9, 9, 18, 7, 80, 78, 57, 9, 9, 98, 101	decmac 10781	. . . 4 |- ( (; 1 1 x. 7 ) + 4 ) = ; 8 1
103	74, 57, 18, 7, 77, 78, 79, 9, 6, 94, 102	decma2c 10782	. . 3 |- ( (; 1 1 x. ; 5 7 ) + 4 ) = ;; 6 3 1
104		4lt10 10516	. . . 4 |- 4 < 10
105	4, 9, 7, 104	declti 10767	. . 3 |- 4 < ; 1 1
106	73, 75, 76, 103, 105	ndvdsi 13596	. 2 |- -. ; 1 1 || ;; 6 3 1
107	9, 15	decnncl 10755	. . 3 |- ; 1 3 e. NN
108	7, 6	deccl 10756	. . 3 |- ; 4 8 e. NN0
109		eqid 2433	. . . 4 |- ; 4 8 = ; 4 8
110	57	dec0h 10758	. . . 4 |- 7 = ; 0 7
111	9, 2	deccl 10756	. . . 4 |- ; 1 3 e. NN0
112		eqid 2433	. . . . 5 |- ; 1 3 = ; 1 3
113	79	nn0cni 10578	. . . . . 6 |- ; 1 1 e. CC
114	113	addid2i 9544	. . . . 5 |- ( 0 + ; 1 1 ) = ; 1 1
115		4cn 10386	. . . . . . . 8 |- 4 e. CC
116	115	mulid2i 9376	. . . . . . 7 |- ( 1 x. 4 ) = 4
117		1p1e2 10422	. . . . . . 7 |- ( 1 + 1 ) = 2
118	116, 117	oveq12i 6092	. . . . . 6 |- ( ( 1 x. 4 ) + ( 1 + 1 ) ) = ( 4 + 2 )
119		4p2e6 10443	. . . . . 6 |- ( 4 + 2 ) = 6
120	118, 119	eqtri 2453	. . . . 5 |- ( ( 1 x. 4 ) + ( 1 + 1 ) ) = 6
121		4t3e12 10814	. . . . . . 7 |- ( 4 x. 3 ) = ; 1 2
122	115, 39, 121	mulcomli 9380	. . . . . 6 |- ( 3 x. 4 ) = ; 1 2
123		2p1e3 10432	. . . . . 6 |- ( 2 + 1 ) = 3
124	9, 23, 9, 122, 123	decaddi 10786	. . . . 5 |- ( ( 3 x. 4 ) + 1 ) = ; 1 3
125	9, 2, 9, 9, 112, 114, 7, 2, 9, 120, 124	decmac 10781	. . . 4 |- ( (; 1 3 x. 4 ) + ( 0 + ; 1 1 ) ) = ; 6 3
126	81	mulid2i 9376	. . . . . . 7 |- ( 1 x. 8 ) = 8
127	39	addid2i 9544	. . . . . . 7 |- ( 0 + 3 ) = 3
128	126, 127	oveq12i 6092	. . . . . 6 |- ( ( 1 x. 8 ) + ( 0 + 3 ) ) = ( 8 + 3 )
129		8p3e11 10798	. . . . . 6 |- ( 8 + 3 ) = ; 1 1
130	128, 129	eqtri 2453	. . . . 5 |- ( ( 1 x. 8 ) + ( 0 + 3 ) ) = ; 1 1
131		8t3e24 10831	. . . . . . 7 |- ( 8 x. 3 ) = ; 2 4
132	81, 39, 131	mulcomli 9380	. . . . . 6 |- ( 3 x. 8 ) = ; 2 4
133	60, 115, 100	addcomli 9548	. . . . . 6 |- ( 4 + 7 ) = ; 1 1
134	23, 7, 57, 132, 123, 9, 133	decaddci 10787	. . . . 5 |- ( ( 3 x. 8 ) + 7 ) = ; 3 1
135	9, 2, 18, 57, 112, 110, 6, 9, 2, 130, 134	decmac 10781	. . . 4 |- ( (; 1 3 x. 8 ) + 7 ) = ;; 1 1 1
136	7, 6, 18, 57, 109, 110, 111, 9, 79, 125, 135	decma2c 10782	. . 3 |- ( (; 1 3 x. ; 4 8 ) + 7 ) = ;; 6 3 1
137		7lt10 10513	. . . 4 |- 7 < 10
138	4, 2, 57, 137	declti 10767	. . 3 |- 7 < ; 1 3
139	107, 108, 53, 136, 138	ndvdsi 13596	. 2 |- -. ; 1 3 || ;; 6 3 1
140	9, 53	decnncl 10755	. . 3 |- ; 1 7 e. NN
141	2, 57	deccl 10756	. . 3 |- ; 3 7 e. NN0
142		2nn 10466	. . 3 |- 2 e. NN
143		eqid 2433	. . . 4 |- ; 3 7 = ; 3 7
144	23	dec0h 10758	. . . 4 |- 2 = ; 0 2
145	9, 57	deccl 10756	. . . 4 |- ; 1 7 e. NN0
146	9, 23	deccl 10756	. . . 4 |- ; 1 2 e. NN0
147		eqid 2433	. . . . 5 |- ; 1 7 = ; 1 7
148	146	nn0cni 10578	. . . . . 6 |- ; 1 2 e. CC
149	148	addid2i 9544	. . . . 5 |- ( 0 + ; 1 2 ) = ; 1 2
150	39	mulid2i 9376	. . . . . . 7 |- ( 1 x. 3 ) = 3
151		1p2e3 10433	. . . . . . 7 |- ( 1 + 2 ) = 3
152	150, 151	oveq12i 6092	. . . . . 6 |- ( ( 1 x. 3 ) + ( 1 + 2 ) ) = ( 3 + 3 )
153		3p3e6 10442	. . . . . 6 |- ( 3 + 3 ) = 6
154	152, 153	eqtri 2453	. . . . 5 |- ( ( 1 x. 3 ) + ( 1 + 2 ) ) = 6
155		7t3e21 10825	. . . . . 6 |- ( 7 x. 3 ) = ; 2 1
156	23, 9, 23, 155, 151	decaddi 10786	. . . . 5 |- ( ( 7 x. 3 ) + 2 ) = ; 2 3
157	9, 57, 9, 23, 147, 149, 2, 2, 23, 154, 156	decmac 10781	. . . 4 |- ( (; 1 7 x. 3 ) + ( 0 + ; 1 2 ) ) = ; 6 3
158	85	addid2i 9544	. . . . . . 7 |- ( 0 + 5 ) = 5
159	95, 158	oveq12i 6092	. . . . . 6 |- ( ( 1 x. 7 ) + ( 0 + 5 ) ) = ( 7 + 5 )
160		7p5e12 10795	. . . . . 6 |- ( 7 + 5 ) = ; 1 2
161	159, 160	eqtri 2453	. . . . 5 |- ( ( 1 x. 7 ) + ( 0 + 5 ) ) = ; 1 2
162		7t7e49 10829	. . . . . 6 |- ( 7 x. 7 ) = ; 4 9
163		4p1e5 10435	. . . . . 6 |- ( 4 + 1 ) = 5
164		9p2e11 10804	. . . . . 6 |- ( 9 + 2 ) = ; 1 1
165	7, 54, 23, 162, 163, 9, 164	decaddci 10787	. . . . 5 |- ( ( 7 x. 7 ) + 2 ) = ; 5 1
166	9, 57, 18, 23, 147, 144, 57, 9, 74, 161, 165	decmac 10781	. . . 4 |- ( (; 1 7 x. 7 ) + 2 ) = ;; 1 2 1
167	2, 57, 18, 23, 143, 144, 145, 9, 146, 157, 166	decma2c 10782	. . 3 |- ( (; 1 7 x. ; 3 7 ) + 2 ) = ;; 6 3 1
168		2lt10 10518	. . . 4 |- 2 < 10
169	4, 57, 23, 168	declti 10767	. . 3 |- 2 < ; 1 7
170	140, 141, 142, 167, 169	ndvdsi 13596	. 2 |- -. ; 1 7 || ;; 6 3 1
171		9nn 10473	. . . 4 |- 9 e. NN
172	9, 171	decnncl 10755	. . 3 |- ; 1 9 e. NN
173	2, 2	deccl 10756	. . 3 |- ; 3 3 e. NN0
174		eqid 2433	. . . 4 |- ; 3 3 = ; 3 3
175	9, 54	deccl 10756	. . . 4 |- ; 1 9 e. NN0
176		eqid 2433	. . . . 5 |- ; 1 9 = ; 1 9
177	34	addid2i 9544	. . . . . 6 |- ( 0 + 6 ) = 6
178	1	dec0h 10758	. . . . . 6 |- 6 = ; 0 6
179	177, 178	eqtri 2453	. . . . 5 |- ( 0 + 6 ) = ; 0 6
180	150, 127	oveq12i 6092	. . . . . 6 |- ( ( 1 x. 3 ) + ( 0 + 3 ) ) = ( 3 + 3 )
181	180, 153	eqtri 2453	. . . . 5 |- ( ( 1 x. 3 ) + ( 0 + 3 ) ) = 6
182		9t3e27 10838	. . . . . 6 |- ( 9 x. 3 ) = ; 2 7
183		7p6e13 10796	. . . . . 6 |- ( 7 + 6 ) = ; 1 3
184	23, 57, 1, 182, 123, 2, 183	decaddci 10787	. . . . 5 |- ( ( 9 x. 3 ) + 6 ) = ; 3 3
185	9, 54, 18, 1, 176, 179, 2, 2, 2, 181, 184	decmac 10781	. . . 4 |- ( (; 1 9 x. 3 ) + ( 0 + 6 ) ) = ; 6 3
186	23, 57, 7, 182, 123, 9, 100	decaddci 10787	. . . . 5 |- ( ( 9 x. 3 ) + 4 ) = ; 3 1
187	9, 54, 18, 7, 176, 78, 2, 9, 2, 181, 186	decmac 10781	. . . 4 |- ( (; 1 9 x. 3 ) + 4 ) = ; 6 1
188	2, 2, 18, 7, 174, 78, 175, 9, 1, 185, 187	decma2c 10782	. . 3 |- ( (; 1 9 x. ; 3 3 ) + 4 ) = ;; 6 3 1
189	4, 54, 7, 104	declti 10767	. . 3 |- 4 < ; 1 9
190	172, 173, 76, 188, 189	ndvdsi 13596	. 2 |- -. ; 1 9 || ;; 6 3 1
191	23, 15	decnncl 10755	. . 3 |- ; 2 3 e. NN
192	23, 57	deccl 10756	. . 3 |- ; 2 7 e. NN0
193		10nn 10474	. . 3 |- 10 e. NN
194		eqid 2433	. . . 4 |- ; 2 7 = ; 2 7
195		dec10 10772	. . . 4 |- 10 = ; 1 0
196	23, 2	deccl 10756	. . . 4 |- ; 2 3 e. NN0
197	9, 1	deccl 10756	. . . 4 |- ; 1 6 e. NN0
198		eqid 2433	. . . . 5 |- ; 2 3 = ; 2 3
199		eqid 2433	. . . . . 6 |- ; 1 6 = ; 1 6
200		ax-1cn 9327	. . . . . . 7 |- 1 e. CC
201		6p1e7 10437	. . . . . . 7 |- ( 6 + 1 ) = 7
202	34, 200, 201	addcomli 9548	. . . . . 6 |- ( 1 + 6 ) = 7
203	18, 9, 9, 1, 27, 199, 46, 202	decadd 10783	. . . . 5 |- ( 1 + ; 1 6 ) = ; 1 7
204		2t2e4 10458	. . . . . . 7 |- ( 2 x. 2 ) = 4
205	204, 117	oveq12i 6092	. . . . . 6 |- ( ( 2 x. 2 ) + ( 1 + 1 ) ) = ( 4 + 2 )
206	205, 119	eqtri 2453	. . . . 5 |- ( ( 2 x. 2 ) + ( 1 + 1 ) ) = 6
207	32	oveq1i 6090	. . . . . 6 |- ( ( 3 x. 2 ) + 7 ) = ( 6 + 7 )
208	60, 34, 183	addcomli 9548	. . . . . 6 |- ( 6 + 7 ) = ; 1 3
209	207, 208	eqtri 2453	. . . . 5 |- ( ( 3 x. 2 ) + 7 ) = ; 1 3
210	23, 2, 9, 57, 198, 203, 23, 2, 9, 206, 209	decmac 10781	. . . 4 |- ( (; 2 3 x. 2 ) + ( 1 + ; 1 6 ) ) = ; 6 3
211		7t2e14 10824	. . . . . . . . 9 |- ( 7 x. 2 ) = ; 1 4
212	60, 19, 211	mulcomli 9380	. . . . . . . 8 |- ( 2 x. 7 ) = ; 1 4
213	9, 7, 23, 212, 119	decaddi 10786	. . . . . . 7 |- ( ( 2 x. 7 ) + 2 ) = ; 1 6
214	60, 39, 155	mulcomli 9380	. . . . . . 7 |- ( 3 x. 7 ) = ; 2 1
215	57, 23, 2, 198, 9, 23, 213, 214	decmul1c 10789	. . . . . 6 |- (; 2 3 x. 7 ) = ;; 1 6 1
216	215	oveq1i 6090	. . . . 5 |- ( (; 2 3 x. 7 ) + 0 ) = (;; 1 6 1 + 0 )
217	197, 9	deccl 10756	. . . . . . 7 |- ;; 1 6 1 e. NN0
218	217	nn0cni 10578	. . . . . 6 |- ;; 1 6 1 e. CC
219	218	addid1i 9543	. . . . 5 |- (;; 1 6 1 + 0 ) = ;; 1 6 1
220	216, 219	eqtri 2453	. . . 4 |- ( (; 2 3 x. 7 ) + 0 ) = ;; 1 6 1
221	23, 57, 9, 18, 194, 195, 196, 9, 197, 210, 220	decma2c 10782	. . 3 |- ( (; 2 3 x. ; 2 7 ) + 10 ) = ;; 6 3 1
222		10pos 10411	. . . . 5 |- 0 < 10
223		1lt2 10475	. . . . 5 |- 1 < 2
224	9, 23, 18, 2, 222, 223	decltc 10764	. . . 4 |- ; 1 0 < ; 2 3
225	195, 224	eqbrtri 4299	. . 3 |- 10 < ; 2 3
226	191, 192, 193, 221, 225	ndvdsi 13596	. 2 |- -. ; 2 3 || ;; 6 3 1
227	5, 14, 17, 22, 50, 52, 72, 106, 139, 170, 190, 226	prmlem2 14129	1 |- ;; 6 3 1 e. Prime

Syntax hints:   e. wcel 1755  (class class class)co 6080   0cc0 9269   1c1 9270   + caddc 9272   x. cmul 9274   < clt 9405   2c2 10358   3c3 10359   4c4 10360   5c5 10361   6c6 10362   7c7 10363   8c8 10364   9c9 10365   10c10 10366  ;cdc 10742   Primecprime 13745

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-8 1757  ax-9 1759  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414  ax-sep 4401  ax-nul 4409  ax-pow 4458  ax-pr 4519  ax-un 6361  ax-cnex 9325  ax-resscn 9326  ax-1cn 9327  ax-icn 9328  ax-addcl 9329  ax-addrcl 9330  ax-mulcl 9331  ax-mulrcl 9332  ax-mulcom 9333  ax-addass 9334  ax-mulass 9335  ax-distr 9336  ax-i2m1 9337  ax-1ne0 9338  ax-1rid 9339  ax-rnegex 9340  ax-rrecex 9341  ax-cnre 9342  ax-pre-lttri 9343  ax-pre-lttrn 9344  ax-pre-ltadd 9345  ax-pre-mulgt0 9346  ax-pre-sup 9347

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 959  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-eu 2258  df-mo 2259  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ne 2598  df-nel 2599  df-ral 2710  df-rex 2711  df-reu 2712  df-rmo 2713  df-rab 2714  df-v 2964  df-sbc 3176  df-csb 3277  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-pss 3332  df-nul 3626  df-if 3780  df-pw 3850  df-sn 3866  df-pr 3868  df-tp 3870  df-op 3872  df-uni 4080  df-int 4117  df-iun 4161  df-br 4281  df-opab 4339  df-mpt 4340  df-tr 4374  df-eprel 4619  df-id 4623  df-po 4628  df-so 4629  df-fr 4666  df-we 4668  df-ord 4709  df-on 4710  df-lim 4711  df-suc 4712  df-xp 4833  df-rel 4834  df-cnv 4835  df-co 4836  df-dm 4837  df-rn 4838  df-res 4839  df-ima 4840  df-iota 5369  df-fun 5408  df-fn 5409  df-f 5410  df-f1 5411  df-fo 5412  df-f1o 5413  df-fv 5414  df-riota 6039  df-ov 6083  df-oprab 6084  df-mpt2 6085  df-om 6466  df-1st 6566  df-2nd 6567  df-recs 6818  df-rdg 6852  df-1o 6908  df-2o 6909  df-oadd 6912  df-er 7089  df-en 7299  df-dom 7300  df-sdom 7301  df-fin 7302  df-sup 7679  df-pnf 9407  df-mnf 9408  df-xr 9409  df-ltxr 9410  df-le 9411  df-sub 9584  df-neg 9585  df-div 9981  df-nn 10310  df-2 10367  df-3 10368  df-4 10369  df-5 10370  df-6 10371  df-7 10372  df-8 10373  df-9 10374  df-10 10375  df-n0 10567  df-z 10634  df-dec 10743  df-uz 10849  df-rp 10979  df-fz 11424  df-seq 11790  df-exp 11849  df-cj 12571  df-re 12572  df-im 12573  df-sqr 12707  df-abs 12708  df-dvds 13518  df-prm 13746

This theorem is referenced by: (None)