Theorem 631prm 14614

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 10733	. . . 4 |- 6 e. NN0
2		3nn0 10730	. . . 4 |- 3 e. NN0
3	1, 2	deccl 10909	. . 3 |- ; 6 3 e. NN0
4		1nn 10463	. . 3 |- 1 e. NN
5	3, 4	decnncl 10908	. 2 |- ;; 6 3 1 e. NN
6		8nn0 10735	. . . 4 |- 8 e. NN0
7		4nn0 10731	. . . 4 |- 4 e. NN0
8	6, 7	deccl 10909	. . 3 |- ; 8 4 e. NN0
9		1nn0 10728	. . 3 |- 1 e. NN0
10		1lt10 10663	. . 3 |- 1 < 10
11		3lt10 10661	. . . 4 |- 3 < 10
12		6lt8 10641	. . . 4 |- 6 < 8
13	1, 6, 2, 7, 11, 12	decltc 10917	. . 3 |- ; 6 3 < ; 8 4
14	3, 8, 9, 9, 10, 13	decltc 10917	. 2 |- ;; 6 3 1 < ;; 8 4 1
15		3nn 10611	. . . 4 |- 3 e. NN
16	1, 15	decnncl 10908	. . 3 |- ; 6 3 e. NN
17	16, 9, 9, 10	declti 10920	. 2 |- 1 < ;; 6 3 1
18		0nn0 10727	. . 3 |- 0 e. NN0
19		2cn 10523	. . . 4 |- 2 e. CC
20	19	mul02i 9680	. . 3 |- ( 0 x. 2 ) = 0
21		1e0p1 10923	. . 3 |- 1 = ( 0 + 1 )
22	3, 18, 20, 21	dec2dvds 14551	. 2 |- -. 2 || ;; 6 3 1
23		2nn0 10729	. . . . 5 |- 2 e. NN0
24	23, 9	deccl 10909	. . . 4 |- ; 2 1 e. NN0
25	24, 18	deccl 10909	. . 3 |- ;; 2 1 0 e. NN0
26		eqid 2382	. . . 4 |- ;; 2 1 0 = ;; 2 1 0
27	9	dec0h 10911	. . . 4 |- 1 = ; 0 1
28		eqid 2382	. . . . 5 |- ; 2 1 = ; 2 1
29		00id 9666	. . . . . 6 |- ( 0 + 0 ) = 0
30	18	dec0h 10911	. . . . . 6 |- 0 = ; 0 0
31	29, 30	eqtri 2411	. . . . 5 |- ( 0 + 0 ) = ; 0 0
32		3t2e6 10604	. . . . . . 7 |- ( 3 x. 2 ) = 6
33	32, 29	oveq12i 6208	. . . . . 6 |- ( ( 3 x. 2 ) + ( 0 + 0 ) ) = ( 6 + 0 )
34		6cn 10534	. . . . . . 7 |- 6 e. CC
35	34	addid1i 9678	. . . . . 6 |- ( 6 + 0 ) = 6
36	33, 35	eqtri 2411	. . . . 5 |- ( ( 3 x. 2 ) + ( 0 + 0 ) ) = 6
37		3t1e3 10603	. . . . . . 7 |- ( 3 x. 1 ) = 3
38	37	oveq1i 6206	. . . . . 6 |- ( ( 3 x. 1 ) + 0 ) = ( 3 + 0 )
39		3cn 10527	. . . . . . 7 |- 3 e. CC
40	39	addid1i 9678	. . . . . 6 |- ( 3 + 0 ) = 3
41	2	dec0h 10911	. . . . . 6 |- 3 = ; 0 3
42	38, 40, 41	3eqtri 2415	. . . . 5 |- ( ( 3 x. 1 ) + 0 ) = ; 0 3
43	23, 9, 18, 18, 28, 31, 2, 2, 18, 36, 42	decma2c 10935	. . . 4 |- ( ( 3 x. ; 2 1 ) + ( 0 + 0 ) ) = ; 6 3
44	39	mul01i 9681	. . . . . 6 |- ( 3 x. 0 ) = 0
45	44	oveq1i 6206	. . . . 5 |- ( ( 3 x. 0 ) + 1 ) = ( 0 + 1 )
46		0p1e1 10564	. . . . 5 |- ( 0 + 1 ) = 1
47	45, 46, 27	3eqtri 2415	. . . 4 |- ( ( 3 x. 0 ) + 1 ) = ; 0 1
48	24, 18, 18, 9, 26, 27, 2, 9, 18, 43, 47	decma2c 10935	. . 3 |- ( ( 3 x. ;; 2 1 0 ) + 1 ) = ;; 6 3 1
49		1lt3 10621	. . 3 |- 1 < 3
50	15, 25, 4, 48, 49	ndvdsi 14070	. 2 |- -. 3 || ;; 6 3 1
51		1lt5 10628	. . 3 |- 1 < 5
52	3, 4, 51	dec5dvds 14552	. 2 |- -. 5 || ;; 6 3 1
53		7nn 10615	. . 3 |- 7 e. NN
54		9nn0 10736	. . . 4 |- 9 e. NN0
55	54, 18	deccl 10909	. . 3 |- ; 9 0 e. NN0
56		eqid 2382	. . . 4 |- ; 9 0 = ; 9 0
57		7nn0 10734	. . . 4 |- 7 e. NN0
58	29	oveq2i 6207	. . . . 5 |- ( ( 7 x. 9 ) + ( 0 + 0 ) ) = ( ( 7 x. 9 ) + 0 )
59		9cn 10540	. . . . . . 7 |- 9 e. CC
60		7cn 10536	. . . . . . 7 |- 7 e. CC
61		9t7e63 10995	. . . . . . 7 |- ( 9 x. 7 ) = ; 6 3
62	59, 60, 61	mulcomli 9514	. . . . . 6 |- ( 7 x. 9 ) = ; 6 3
63	62	oveq1i 6206	. . . . 5 |- ( ( 7 x. 9 ) + 0 ) = (; 6 3 + 0 )
64	3	nn0cni 10724	. . . . . 6 |- ; 6 3 e. CC
65	64	addid1i 9678	. . . . 5 |- (; 6 3 + 0 ) = ; 6 3
66	58, 63, 65	3eqtri 2415	. . . 4 |- ( ( 7 x. 9 ) + ( 0 + 0 ) ) = ; 6 3
67	60	mul01i 9681	. . . . . 6 |- ( 7 x. 0 ) = 0
68	67	oveq1i 6206	. . . . 5 |- ( ( 7 x. 0 ) + 1 ) = ( 0 + 1 )
69	68, 46, 27	3eqtri 2415	. . . 4 |- ( ( 7 x. 0 ) + 1 ) = ; 0 1
70	54, 18, 18, 9, 56, 27, 57, 9, 18, 66, 69	decma2c 10935	. . 3 |- ( ( 7 x. ; 9 0 ) + 1 ) = ;; 6 3 1
71		1lt7 10639	. . 3 |- 1 < 7
72	53, 55, 4, 70, 71	ndvdsi 14070	. 2 |- -. 7 || ;; 6 3 1
73	9, 4	decnncl 10908	. . 3 |- ; 1 1 e. NN
74		5nn0 10732	. . . 4 |- 5 e. NN0
75	74, 57	deccl 10909	. . 3 |- ; 5 7 e. NN0
76		4nn 10612	. . 3 |- 4 e. NN
77		eqid 2382	. . . 4 |- ; 5 7 = ; 5 7
78	7	dec0h 10911	. . . 4 |- 4 = ; 0 4
79	9, 9	deccl 10909	. . . 4 |- ; 1 1 e. NN0
80		eqid 2382	. . . . 5 |- ; 1 1 = ; 1 1
81		8cn 10538	. . . . . . 7 |- 8 e. CC
82	81	addid2i 9679	. . . . . 6 |- ( 0 + 8 ) = 8
83	6	dec0h 10911	. . . . . 6 |- 8 = ; 0 8
84	82, 83	eqtri 2411	. . . . 5 |- ( 0 + 8 ) = ; 0 8
85		5cn 10532	. . . . . . . 8 |- 5 e. CC
86	85	mulid2i 9510	. . . . . . 7 |- ( 1 x. 5 ) = 5
87	86, 46	oveq12i 6208	. . . . . 6 |- ( ( 1 x. 5 ) + ( 0 + 1 ) ) = ( 5 + 1 )
88		5p1e6 10580	. . . . . 6 |- ( 5 + 1 ) = 6
89	87, 88	eqtri 2411	. . . . 5 |- ( ( 1 x. 5 ) + ( 0 + 1 ) ) = 6
90	86	oveq1i 6206	. . . . . 6 |- ( ( 1 x. 5 ) + 8 ) = ( 5 + 8 )
91		8p5e13 10953	. . . . . . 7 |- ( 8 + 5 ) = ; 1 3
92	81, 85, 91	addcomli 9683	. . . . . 6 |- ( 5 + 8 ) = ; 1 3
93	90, 92	eqtri 2411	. . . . 5 |- ( ( 1 x. 5 ) + 8 ) = ; 1 3
94	9, 9, 18, 6, 80, 84, 74, 2, 9, 89, 93	decmac 10934	. . . 4 |- ( (; 1 1 x. 5 ) + ( 0 + 8 ) ) = ; 6 3
95	60	mulid2i 9510	. . . . . . 7 |- ( 1 x. 7 ) = 7
96	95, 46	oveq12i 6208	. . . . . 6 |- ( ( 1 x. 7 ) + ( 0 + 1 ) ) = ( 7 + 1 )
97		7p1e8 10582	. . . . . 6 |- ( 7 + 1 ) = 8
98	96, 97	eqtri 2411	. . . . 5 |- ( ( 1 x. 7 ) + ( 0 + 1 ) ) = 8
99	95	oveq1i 6206	. . . . . 6 |- ( ( 1 x. 7 ) + 4 ) = ( 7 + 4 )
100		7p4e11 10947	. . . . . 6 |- ( 7 + 4 ) = ; 1 1
101	99, 100	eqtri 2411	. . . . 5 |- ( ( 1 x. 7 ) + 4 ) = ; 1 1
102	9, 9, 18, 7, 80, 78, 57, 9, 9, 98, 101	decmac 10934	. . . 4 |- ( (; 1 1 x. 7 ) + 4 ) = ; 8 1
103	74, 57, 18, 7, 77, 78, 79, 9, 6, 94, 102	decma2c 10935	. . 3 |- ( (; 1 1 x. ; 5 7 ) + 4 ) = ;; 6 3 1
104		4lt10 10660	. . . 4 |- 4 < 10
105	4, 9, 7, 104	declti 10920	. . 3 |- 4 < ; 1 1
106	73, 75, 76, 103, 105	ndvdsi 14070	. 2 |- -. ; 1 1 || ;; 6 3 1
107	9, 15	decnncl 10908	. . 3 |- ; 1 3 e. NN
108	7, 6	deccl 10909	. . 3 |- ; 4 8 e. NN0
109		eqid 2382	. . . 4 |- ; 4 8 = ; 4 8
110	57	dec0h 10911	. . . 4 |- 7 = ; 0 7
111	9, 2	deccl 10909	. . . 4 |- ; 1 3 e. NN0
112		eqid 2382	. . . . 5 |- ; 1 3 = ; 1 3
113	79	nn0cni 10724	. . . . . 6 |- ; 1 1 e. CC
114	113	addid2i 9679	. . . . 5 |- ( 0 + ; 1 1 ) = ; 1 1
115		4cn 10530	. . . . . . . 8 |- 4 e. CC
116	115	mulid2i 9510	. . . . . . 7 |- ( 1 x. 4 ) = 4
117		1p1e2 10566	. . . . . . 7 |- ( 1 + 1 ) = 2
118	116, 117	oveq12i 6208	. . . . . 6 |- ( ( 1 x. 4 ) + ( 1 + 1 ) ) = ( 4 + 2 )
119		4p2e6 10587	. . . . . 6 |- ( 4 + 2 ) = 6
120	118, 119	eqtri 2411	. . . . 5 |- ( ( 1 x. 4 ) + ( 1 + 1 ) ) = 6
121		4t3e12 10967	. . . . . . 7 |- ( 4 x. 3 ) = ; 1 2
122	115, 39, 121	mulcomli 9514	. . . . . 6 |- ( 3 x. 4 ) = ; 1 2
123		2p1e3 10576	. . . . . 6 |- ( 2 + 1 ) = 3
124	9, 23, 9, 122, 123	decaddi 10939	. . . . 5 |- ( ( 3 x. 4 ) + 1 ) = ; 1 3
125	9, 2, 9, 9, 112, 114, 7, 2, 9, 120, 124	decmac 10934	. . . 4 |- ( (; 1 3 x. 4 ) + ( 0 + ; 1 1 ) ) = ; 6 3
126	81	mulid2i 9510	. . . . . . 7 |- ( 1 x. 8 ) = 8
127	39	addid2i 9679	. . . . . . 7 |- ( 0 + 3 ) = 3
128	126, 127	oveq12i 6208	. . . . . 6 |- ( ( 1 x. 8 ) + ( 0 + 3 ) ) = ( 8 + 3 )
129		8p3e11 10951	. . . . . 6 |- ( 8 + 3 ) = ; 1 1
130	128, 129	eqtri 2411	. . . . 5 |- ( ( 1 x. 8 ) + ( 0 + 3 ) ) = ; 1 1
131		8t3e24 10984	. . . . . . 7 |- ( 8 x. 3 ) = ; 2 4
132	81, 39, 131	mulcomli 9514	. . . . . 6 |- ( 3 x. 8 ) = ; 2 4
133	60, 115, 100	addcomli 9683	. . . . . 6 |- ( 4 + 7 ) = ; 1 1
134	23, 7, 57, 132, 123, 9, 133	decaddci 10940	. . . . 5 |- ( ( 3 x. 8 ) + 7 ) = ; 3 1
135	9, 2, 18, 57, 112, 110, 6, 9, 2, 130, 134	decmac 10934	. . . 4 |- ( (; 1 3 x. 8 ) + 7 ) = ;; 1 1 1
136	7, 6, 18, 57, 109, 110, 111, 9, 79, 125, 135	decma2c 10935	. . 3 |- ( (; 1 3 x. ; 4 8 ) + 7 ) = ;; 6 3 1
137		7lt10 10657	. . . 4 |- 7 < 10
138	4, 2, 57, 137	declti 10920	. . 3 |- 7 < ; 1 3
139	107, 108, 53, 136, 138	ndvdsi 14070	. 2 |- -. ; 1 3 || ;; 6 3 1
140	9, 53	decnncl 10908	. . 3 |- ; 1 7 e. NN
141	2, 57	deccl 10909	. . 3 |- ; 3 7 e. NN0
142		2nn 10610	. . 3 |- 2 e. NN
143		eqid 2382	. . . 4 |- ; 3 7 = ; 3 7
144	23	dec0h 10911	. . . 4 |- 2 = ; 0 2
145	9, 57	deccl 10909	. . . 4 |- ; 1 7 e. NN0
146	9, 23	deccl 10909	. . . 4 |- ; 1 2 e. NN0
147		eqid 2382	. . . . 5 |- ; 1 7 = ; 1 7
148	146	nn0cni 10724	. . . . . 6 |- ; 1 2 e. CC
149	148	addid2i 9679	. . . . 5 |- ( 0 + ; 1 2 ) = ; 1 2
150	39	mulid2i 9510	. . . . . . 7 |- ( 1 x. 3 ) = 3
151		1p2e3 10577	. . . . . . 7 |- ( 1 + 2 ) = 3
152	150, 151	oveq12i 6208	. . . . . 6 |- ( ( 1 x. 3 ) + ( 1 + 2 ) ) = ( 3 + 3 )
153		3p3e6 10586	. . . . . 6 |- ( 3 + 3 ) = 6
154	152, 153	eqtri 2411	. . . . 5 |- ( ( 1 x. 3 ) + ( 1 + 2 ) ) = 6
155		7t3e21 10978	. . . . . 6 |- ( 7 x. 3 ) = ; 2 1
156	23, 9, 23, 155, 151	decaddi 10939	. . . . 5 |- ( ( 7 x. 3 ) + 2 ) = ; 2 3
157	9, 57, 9, 23, 147, 149, 2, 2, 23, 154, 156	decmac 10934	. . . 4 |- ( (; 1 7 x. 3 ) + ( 0 + ; 1 2 ) ) = ; 6 3
158	85	addid2i 9679	. . . . . . 7 |- ( 0 + 5 ) = 5
159	95, 158	oveq12i 6208	. . . . . 6 |- ( ( 1 x. 7 ) + ( 0 + 5 ) ) = ( 7 + 5 )
160		7p5e12 10948	. . . . . 6 |- ( 7 + 5 ) = ; 1 2
161	159, 160	eqtri 2411	. . . . 5 |- ( ( 1 x. 7 ) + ( 0 + 5 ) ) = ; 1 2
162		7t7e49 10982	. . . . . 6 |- ( 7 x. 7 ) = ; 4 9
163		4p1e5 10579	. . . . . 6 |- ( 4 + 1 ) = 5
164		9p2e11 10957	. . . . . 6 |- ( 9 + 2 ) = ; 1 1
165	7, 54, 23, 162, 163, 9, 164	decaddci 10940	. . . . 5 |- ( ( 7 x. 7 ) + 2 ) = ; 5 1
166	9, 57, 18, 23, 147, 144, 57, 9, 74, 161, 165	decmac 10934	. . . 4 |- ( (; 1 7 x. 7 ) + 2 ) = ;; 1 2 1
167	2, 57, 18, 23, 143, 144, 145, 9, 146, 157, 166	decma2c 10935	. . 3 |- ( (; 1 7 x. ; 3 7 ) + 2 ) = ;; 6 3 1
168		2lt10 10662	. . . 4 |- 2 < 10
169	4, 57, 23, 168	declti 10920	. . 3 |- 2 < ; 1 7
170	140, 141, 142, 167, 169	ndvdsi 14070	. 2 |- -. ; 1 7 || ;; 6 3 1
171		9nn 10617	. . . 4 |- 9 e. NN
172	9, 171	decnncl 10908	. . 3 |- ; 1 9 e. NN
173	2, 2	deccl 10909	. . 3 |- ; 3 3 e. NN0
174		eqid 2382	. . . 4 |- ; 3 3 = ; 3 3
175	9, 54	deccl 10909	. . . 4 |- ; 1 9 e. NN0
176		eqid 2382	. . . . 5 |- ; 1 9 = ; 1 9
177	34	addid2i 9679	. . . . . 6 |- ( 0 + 6 ) = 6
178	1	dec0h 10911	. . . . . 6 |- 6 = ; 0 6
179	177, 178	eqtri 2411	. . . . 5 |- ( 0 + 6 ) = ; 0 6
180	150, 127	oveq12i 6208	. . . . . 6 |- ( ( 1 x. 3 ) + ( 0 + 3 ) ) = ( 3 + 3 )
181	180, 153	eqtri 2411	. . . . 5 |- ( ( 1 x. 3 ) + ( 0 + 3 ) ) = 6
182		9t3e27 10991	. . . . . 6 |- ( 9 x. 3 ) = ; 2 7
183		7p6e13 10949	. . . . . 6 |- ( 7 + 6 ) = ; 1 3
184	23, 57, 1, 182, 123, 2, 183	decaddci 10940	. . . . 5 |- ( ( 9 x. 3 ) + 6 ) = ; 3 3
185	9, 54, 18, 1, 176, 179, 2, 2, 2, 181, 184	decmac 10934	. . . 4 |- ( (; 1 9 x. 3 ) + ( 0 + 6 ) ) = ; 6 3
186	23, 57, 7, 182, 123, 9, 100	decaddci 10940	. . . . 5 |- ( ( 9 x. 3 ) + 4 ) = ; 3 1
187	9, 54, 18, 7, 176, 78, 2, 9, 2, 181, 186	decmac 10934	. . . 4 |- ( (; 1 9 x. 3 ) + 4 ) = ; 6 1
188	2, 2, 18, 7, 174, 78, 175, 9, 1, 185, 187	decma2c 10935	. . 3 |- ( (; 1 9 x. ; 3 3 ) + 4 ) = ;; 6 3 1
189	4, 54, 7, 104	declti 10920	. . 3 |- 4 < ; 1 9
190	172, 173, 76, 188, 189	ndvdsi 14070	. 2 |- -. ; 1 9 || ;; 6 3 1
191	23, 15	decnncl 10908	. . 3 |- ; 2 3 e. NN
192	23, 57	deccl 10909	. . 3 |- ; 2 7 e. NN0
193		10nn 10618	. . 3 |- 10 e. NN
194		eqid 2382	. . . 4 |- ; 2 7 = ; 2 7
195		dec10 10925	. . . 4 |- 10 = ; 1 0
196	23, 2	deccl 10909	. . . 4 |- ; 2 3 e. NN0
197	9, 1	deccl 10909	. . . 4 |- ; 1 6 e. NN0
198		eqid 2382	. . . . 5 |- ; 2 3 = ; 2 3
199		eqid 2382	. . . . . 6 |- ; 1 6 = ; 1 6
200		ax-1cn 9461	. . . . . . 7 |- 1 e. CC
201		6p1e7 10581	. . . . . . 7 |- ( 6 + 1 ) = 7
202	34, 200, 201	addcomli 9683	. . . . . 6 |- ( 1 + 6 ) = 7
203	18, 9, 9, 1, 27, 199, 46, 202	decadd 10936	. . . . 5 |- ( 1 + ; 1 6 ) = ; 1 7
204		2t2e4 10602	. . . . . . 7 |- ( 2 x. 2 ) = 4
205	204, 117	oveq12i 6208	. . . . . 6 |- ( ( 2 x. 2 ) + ( 1 + 1 ) ) = ( 4 + 2 )
206	205, 119	eqtri 2411	. . . . 5 |- ( ( 2 x. 2 ) + ( 1 + 1 ) ) = 6
207	32	oveq1i 6206	. . . . . 6 |- ( ( 3 x. 2 ) + 7 ) = ( 6 + 7 )
208	60, 34, 183	addcomli 9683	. . . . . 6 |- ( 6 + 7 ) = ; 1 3
209	207, 208	eqtri 2411	. . . . 5 |- ( ( 3 x. 2 ) + 7 ) = ; 1 3
210	23, 2, 9, 57, 198, 203, 23, 2, 9, 206, 209	decmac 10934	. . . 4 |- ( (; 2 3 x. 2 ) + ( 1 + ; 1 6 ) ) = ; 6 3
211		7t2e14 10977	. . . . . . . . 9 |- ( 7 x. 2 ) = ; 1 4
212	60, 19, 211	mulcomli 9514	. . . . . . . 8 |- ( 2 x. 7 ) = ; 1 4
213	9, 7, 23, 212, 119	decaddi 10939	. . . . . . 7 |- ( ( 2 x. 7 ) + 2 ) = ; 1 6
214	60, 39, 155	mulcomli 9514	. . . . . . 7 |- ( 3 x. 7 ) = ; 2 1
215	57, 23, 2, 198, 9, 23, 213, 214	decmul1c 10942	. . . . . 6 |- (; 2 3 x. 7 ) = ;; 1 6 1
216	215	oveq1i 6206	. . . . 5 |- ( (; 2 3 x. 7 ) + 0 ) = (;; 1 6 1 + 0 )
217	197, 9	deccl 10909	. . . . . . 7 |- ;; 1 6 1 e. NN0
218	217	nn0cni 10724	. . . . . 6 |- ;; 1 6 1 e. CC
219	218	addid1i 9678	. . . . 5 |- (;; 1 6 1 + 0 ) = ;; 1 6 1
220	216, 219	eqtri 2411	. . . 4 |- ( (; 2 3 x. 7 ) + 0 ) = ;; 1 6 1
221	23, 57, 9, 18, 194, 195, 196, 9, 197, 210, 220	decma2c 10935	. . 3 |- ( (; 2 3 x. ; 2 7 ) + 10 ) = ;; 6 3 1
222		10pos 10555	. . . . 5 |- 0 < 10
223		1lt2 10619	. . . . 5 |- 1 < 2
224	9, 23, 18, 2, 222, 223	decltc 10917	. . . 4 |- ; 1 0 < ; 2 3
225	195, 224	eqbrtri 4386	. . 3 |- 10 < ; 2 3
226	191, 192, 193, 221, 225	ndvdsi 14070	. 2 |- -. ; 2 3 || ;; 6 3 1
227	5, 14, 17, 22, 50, 52, 72, 106, 139, 170, 190, 226	prmlem2 14607	1 |- ;; 6 3 1 e. Prime

Syntax hints:   e. wcel 1826  (class class class)co 6196   0cc0 9403   1c1 9404   + caddc 9406   x. cmul 9408   < clt 9539   2c2 10502   3c3 10503   4c4 10504   5c5 10505   6c6 10506   7c7 10507   8c8 10508   9c9 10509   10c10 10510  ;cdc 10895   Primecprime 14219

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-8 1828  ax-9 1830  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360  ax-sep 4488  ax-nul 4496  ax-pow 4543  ax-pr 4601  ax-un 6491  ax-cnex 9459  ax-resscn 9460  ax-1cn 9461  ax-icn 9462  ax-addcl 9463  ax-addrcl 9464  ax-mulcl 9465  ax-mulrcl 9466  ax-mulcom 9467  ax-addass 9468  ax-mulass 9469  ax-distr 9470  ax-i2m1 9471  ax-1ne0 9472  ax-1rid 9473  ax-rnegex 9474  ax-rrecex 9475  ax-cnre 9476  ax-pre-lttri 9477  ax-pre-lttrn 9478  ax-pre-ltadd 9479  ax-pre-mulgt0 9480  ax-pre-sup 9481

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 972  df-3an 973  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-eu 2222  df-mo 2223  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-ne 2579  df-nel 2580  df-ral 2737  df-rex 2738  df-reu 2739  df-rmo 2740  df-rab 2741  df-v 3036  df-sbc 3253  df-csb 3349  df-dif 3392  df-un 3394  df-in 3396  df-ss 3403  df-pss 3405  df-nul 3712  df-if 3858  df-pw 3929  df-sn 3945  df-pr 3947  df-tp 3949  df-op 3951  df-uni 4164  df-int 4200  df-iun 4245  df-br 4368  df-opab 4426  df-mpt 4427  df-tr 4461  df-eprel 4705  df-id 4709  df-po 4714  df-so 4715  df-fr 4752  df-we 4754  df-ord 4795  df-on 4796  df-lim 4797  df-suc 4798  df-xp 4919  df-rel 4920  df-cnv 4921  df-co 4922  df-dm 4923  df-rn 4924  df-res 4925  df-ima 4926  df-iota 5460  df-fun 5498  df-fn 5499  df-f 5500  df-f1 5501  df-fo 5502  df-f1o 5503  df-fv 5504  df-riota 6158  df-ov 6199  df-oprab 6200  df-mpt2 6201  df-om 6600  df-1st 6699  df-2nd 6700  df-recs 6960  df-rdg 6994  df-1o 7048  df-2o 7049  df-oadd 7052  df-er 7229  df-en 7436  df-dom 7437  df-sdom 7438  df-fin 7439  df-sup 7816  df-pnf 9541  df-mnf 9542  df-xr 9543  df-ltxr 9544  df-le 9545  df-sub 9720  df-neg 9721  df-div 10124  df-nn 10453  df-2 10511  df-3 10512  df-4 10513  df-5 10514  df-6 10515  df-7 10516  df-8 10517  df-9 10518  df-10 10519  df-n0 10713  df-z 10782  df-dec 10896  df-uz 11002  df-rp 11140  df-fz 11594  df-seq 12011  df-exp 12070  df-cj 12934  df-re 12935  df-im 12936  df-sqrt 13070  df-abs 13071  df-dvds 13989  df-prm 14220

This theorem is referenced by: (None)