Theorem arisumi 8487

Description: Arithmetic series sum of the first (N + 1) non-negative integers. (Contributed by FL, 10-Dec-2006.)

Hypothesis

Ref	Expression
arisumi.1	|- N e. NN

Assertion

Ref	Expression
arisumi	|- sum_k e. (0...N)k = ((((N + 1)^2) - (N + 1)) / 2)

Distinct variable group:   k,N

Proof of Theorem arisumi

Step	Hyp	Ref	Expression
1		arisumi.1	. . . . . . . . . . 11 |- N e. NN
2	1	nnnn0i 7316	. . . . . . . . . 10 |- N e. NN0
3		elnn0uz 7610	. . . . . . . . . 10 |- (N e. NN0 <-> N e. (ZZ>=` 0))
4	2, 3	mpbi 206	. . . . . . . . 9 |- N e. (ZZ>=` 0)
5		ax1cn 6422	. . . . . . . . 9 |- 1 e. CC
6		fsumconst 8298	. . . . . . . . 9 |- ((N e. (ZZ>=` 0) /\ 1 e. CC) -> sum_k e. (0...N)1 = (((N - 0) + 1) x. 1))
7	4, 5, 6	mp2an 761	. . . . . . . 8 |- sum_k e. (0...N)1 = (((N - 0) + 1) x. 1)
8	1	nncni 7115	. . . . . . . . . . 11 |- N e. CC
9		0cn 6481	. . . . . . . . . . 11 |- 0 e. CC
10	8, 9	subcli 6523	. . . . . . . . . 10 |- (N - 0) e. CC
11	10, 5	addcli 6473	. . . . . . . . 9 |- ((N - 0) + 1) e. CC
12	11	mulid1i 6485	. . . . . . . 8 |- (((N - 0) + 1) x. 1) = ((N - 0) + 1)
13	8	subid1i 6552	. . . . . . . . 9 |- (N - 0) = N
14	13	opreq1i 4892	. . . . . . . 8 |- ((N - 0) + 1) = (N + 1)
15	7, 12, 14	3eqtrri 1913	. . . . . . 7 |- (N + 1) = sum_k e. (0...N)1
16	15	opreq2i 4893	. . . . . 6 |- ((2 x. sum_k e. (0...N)k) + (N + 1)) = ((2 x. sum_k e. (0...N)k) + sum_k e. (0...N)1)
17		2cn 7164	. . . . . . . 8 |- 2 e. CC
18		elfzelz 7652	. . . . . . . . . 10 |- (k e. (0...N) -> k e. ZZ)
19		zcn 7349	. . . . . . . . . 10 |- (k e. ZZ -> k e. CC)
20	18, 19	syl 12	. . . . . . . . 9 |- (k e. (0...N) -> k e. CC)
21	20	rgen 2159	. . . . . . . 8 |- A.k e. (0...N)k e. CC
22		fsummulc1 8293	. . . . . . . 8 |- ((N e. (ZZ>=` 0) /\ 2 e. CC /\ A.k e. (0...N)k e. CC) -> (2 x. sum_k e. (0...N)k) = sum_k e. (0...N)(2 x. k))
23	4, 17, 21, 22	mp3an 1191	. . . . . . 7 |- (2 x. sum_k e. (0...N)k) = sum_k e. (0...N)(2 x. k)
24	23	opreq1i 4892	. . . . . 6 |- ((2 x. sum_k e. (0...N)k) + sum_k e. (0...N)1) = (sum_k e. (0...N)(2 x. k) + sum_k e. (0...N)1)
25		peano2nn 7118	. . . . . . . . . . 11 |- (N e. NN -> (N + 1) e. NN)
26	1, 25	ax-mp 7	. . . . . . . . . 10 |- (N + 1) e. NN
27	26	nnnn0i 7316	. . . . . . . . 9 |- (N + 1) e. NN0
28		elfznn0 7668	. . . . . . . . . . 11 |- (k e. (0...(N + 1)) -> k e. NN0)
29		nn0cn 7318	. . . . . . . . . . 11 |- (k e. NN0 -> k e. CC)
30		sqcl 7856	. . . . . . . . . . 11 |- (k e. CC -> (k^2) e. CC)
31	28, 29, 30	3syl 24	. . . . . . . . . 10 |- (k e. (0...(N + 1)) -> (k^2) e. CC)
32	31	rgen 2159	. . . . . . . . 9 |- A.k e. (0...(N + 1))(k^2) e. CC
33		fsum0cl 8276	. . . . . . . . 9 |- (((N + 1) e. NN0 /\ A.k e. (0...(N + 1))(k^2) e. CC) -> sum_k e. (0...(N + 1))(k^2) e. CC)
34	27, 32, 33	mp2an 761	. . . . . . . 8 |- sum_k e. (0...(N + 1))(k^2) e. CC
35		elfznn0 7668	. . . . . . . . . . 11 |- (k e. (0...N) -> k e. NN0)
36	35, 29, 30	3syl 24	. . . . . . . . . 10 |- (k e. (0...N) -> (k^2) e. CC)
37	36	rgen 2159	. . . . . . . . 9 |- A.k e. (0...N)(k^2) e. CC
38		fsum0cl 8276	. . . . . . . . 9 |- ((N e. NN0 /\ A.k e. (0...N)(k^2) e. CC) -> sum_k e. (0...N)(k^2) e. CC)
39	2, 37, 38	mp2an 761	. . . . . . . 8 |- sum_k e. (0...N)(k^2) e. CC
40		mulcl 6456	. . . . . . . . . . . 12 |- ((2 e. CC /\ k e. CC) -> (2 x. k) e. CC)
41	35, 29	syl 12	. . . . . . . . . . . 12 |- (k e. (0...N) -> k e. CC)
42	40, 17, 41	sylancr 526	. . . . . . . . . . 11 |- (k e. (0...N) -> (2 x. k) e. CC)
43	42	rgen 2159	. . . . . . . . . 10 |- A.k e. (0...N)(2 x. k) e. CC
44		fsum0cl 8276	. . . . . . . . . 10 |- ((N e. NN0 /\ A.k e. (0...N)(2 x. k) e. CC) -> sum_k e. (0...N)(2 x. k) e. CC)
45	2, 43, 44	mp2an 761	. . . . . . . . 9 |- sum_k e. (0...N)(2 x. k) e. CC
46	5	a1i 8	. . . . . . . . . . 11 |- (k e. (0...N) -> 1 e. CC)
47	46	rgen 2159	. . . . . . . . . 10 |- A.k e. (0...N)1 e. CC
48		fsum0cl 8276	. . . . . . . . . 10 |- ((N e. NN0 /\ A.k e. (0...N)1 e. CC) -> sum_k e. (0...N)1 e. CC)
49	2, 47, 48	mp2an 761	. . . . . . . . 9 |- sum_k e. (0...N)1 e. CC
50	45, 49	addcli 6473	. . . . . . . 8 |- (sum_k e. (0...N)(2 x. k) + sum_k e. (0...N)1) e. CC
51		binom2 7896	. . . . . . . . . . . . . 14 |- ((k e. CC /\ 1 e. CC) -> ((k + 1)^2) = (((k^2) + (2 x. (k x. 1))) + (1^2)))
52	5, 51	mpan2 760	. . . . . . . . . . . . 13 |- (k e. CC -> ((k + 1)^2) = (((k^2) + (2 x. (k x. 1))) + (1^2)))
53		ax1id 6435	. . . . . . . . . . . . . . . 16 |- (k e. CC -> (k x. 1) = k)
54	53	opreq2d 4898	. . . . . . . . . . . . . . 15 |- (k e. CC -> (2 x. (k x. 1)) = (2 x. k))
55	54	opreq2d 4898	. . . . . . . . . . . . . 14 |- (k e. CC -> ((k^2) + (2 x. (k x. 1))) = ((k^2) + (2 x. k)))
56		sq1 7882	. . . . . . . . . . . . . . 15 |- (1^2) = 1
57	56	a1i 8	. . . . . . . . . . . . . 14 |- (k e. CC -> (1^2) = 1)
58	55, 57	opreq12d 4900	. . . . . . . . . . . . 13 |- (k e. CC -> (((k^2) + (2 x. (k x. 1))) + (1^2)) = (((k^2) + (2 x. k)) + 1))
59	52, 58	eqtrd 1925	. . . . . . . . . . . 12 |- (k e. CC -> ((k + 1)^2) = (((k^2) + (2 x. k)) + 1))
60	35, 29, 59	3syl 24	. . . . . . . . . . 11 |- (k e. (0...N) -> ((k + 1)^2) = (((k^2) + (2 x. k)) + 1))
61	60	sumeq2i 8248	. . . . . . . . . 10 |- sum_k e. (0...N)((k + 1)^2) = sum_k e. (0...N)(((k^2) + (2 x. k)) + 1)
62		addcl 6454	. . . . . . . . . . . . . 14 |- (((k^2) e. CC /\ (2 x. k) e. CC) -> ((k^2) + (2 x. k)) e. CC)
63	36, 42, 62	syl11anc 524	. . . . . . . . . . . . 13 |- (k e. (0...N) -> ((k^2) + (2 x. k)) e. CC)
64	63, 5	jctir 317	. . . . . . . . . . . 12 |- (k e. (0...N) -> (((k^2) + (2 x. k)) e. CC /\ 1 e. CC))
65	64	rgen 2159	. . . . . . . . . . 11 |- A.k e. (0...N)(((k^2) + (2 x. k)) e. CC /\ 1 e. CC)
66		fsumadd 8282	. . . . . . . . . . 11 |- ((N e. (ZZ>=` 0) /\ A.k e. (0...N)(((k^2) + (2 x. k)) e. CC /\ 1 e. CC)) -> sum_k e. (0...N)(((k^2) + (2 x. k)) + 1) = (sum_k e. (0...N)((k^2) + (2 x. k)) + sum_k e. (0...N)1))
67	4, 65, 66	mp2an 761	. . . . . . . . . 10 |- sum_k e. (0...N)(((k^2) + (2 x. k)) + 1) = (sum_k e. (0...N)((k^2) + (2 x. k)) + sum_k e. (0...N)1)
68	36, 42	jca 310	. . . . . . . . . . . 12 |- (k e. (0...N) -> ((k^2) e. CC /\ (2 x. k) e. CC))
69	68	rgen 2159	. . . . . . . . . . 11 |- A.k e. (0...N)((k^2) e. CC /\ (2 x. k) e. CC)
70		fsumadd 8282	. . . . . . . . . . . 12 |- ((N e. (ZZ>=` 0) /\ A.k e. (0...N)((k^2) e. CC /\ (2 x. k) e. CC)) -> sum_k e. (0...N)((k^2) + (2 x. k)) = (sum_k e. (0...N)(k^2) + sum_k e. (0...N)(2 x. k)))
71	70	opreq1d 4897	. . . . . . . . . . 11 |- ((N e. (ZZ>=` 0) /\ A.k e. (0...N)((k^2) e. CC /\ (2 x. k) e. CC)) -> (sum_k e. (0...N)((k^2) + (2 x. k)) + sum_k e. (0...N)1) = ((sum_k e. (0...N)(k^2) + sum_k e. (0...N)(2 x. k)) + sum_k e. (0...N)1))
72	4, 69, 71	mp2an 761	. . . . . . . . . 10 |- (sum_k e. (0...N)((k^2) + (2 x. k)) + sum_k e. (0...N)1) = ((sum_k e. (0...N)(k^2) + sum_k e. (0...N)(2 x. k)) + sum_k e. (0...N)1)
73	61, 67, 72	3eqtri 1912	. . . . . . . . 9 |- sum_k e. (0...N)((k + 1)^2) = ((sum_k e. (0...N)(k^2) + sum_k e. (0...N)(2 x. k)) + sum_k e. (0...N)1)
74		0z 7355	. . . . . . . . . . . . . . 15 |- 0 e. ZZ
75		1z 7368	. . . . . . . . . . . . . . 15 |- 1 e. ZZ
76		zaddcl 7374	. . . . . . . . . . . . . . 15 |- ((0 e. ZZ /\ 1 e. ZZ) -> (0 + 1) e. ZZ)
77	74, 75, 76	mp2an 761	. . . . . . . . . . . . . 14 |- (0 + 1) e. ZZ
78	77	eluz1i 7591	. . . . . . . . . . . . 13 |- ((N + 1) e. (ZZ>=` (0 + 1)) <-> ((N + 1) e. ZZ /\ (0 + 1) <_ (N + 1)))
79		nnz 7362	. . . . . . . . . . . . . . 15 |- (N e. NN -> N e. ZZ)
80	1, 79	ax-mp 7	. . . . . . . . . . . . . 14 |- N e. ZZ
81		zaddcl 7374	. . . . . . . . . . . . . 14 |- ((N e. ZZ /\ 1 e. ZZ) -> (N + 1) e. ZZ)
82	80, 75, 81	mp2an 761	. . . . . . . . . . . . 13 |- (N + 1) e. ZZ
83		nngt0 7129	. . . . . . . . . . . . . . . 16 |- (N e. NN -> 0 < N)
84		0re 6603	. . . . . . . . . . . . . . . . 17 |- 0 e. RR
85	1	nnrei 7114	. . . . . . . . . . . . . . . . 17 |- N e. RR
86	84, 85	ltlei 6755	. . . . . . . . . . . . . . . 16 |- (0 < N -> 0 <_ N)
87	83, 86	syl 12	. . . . . . . . . . . . . . 15 |- (N e. NN -> 0 <_ N)
88	1, 87	ax-mp 7	. . . . . . . . . . . . . 14 |- 0 <_ N
89		1re 6598	. . . . . . . . . . . . . . 15 |- 1 e. RR
90	84, 85, 89	leadd1i 6767	. . . . . . . . . . . . . 14 |- (0 <_ N <-> (0 + 1) <_ (N + 1))
91	88, 90	mpbi 206	. . . . . . . . . . . . 13 |- (0 + 1) <_ (N + 1)
92	78, 82, 91	mpbir2an 800	. . . . . . . . . . . 12 |- (N + 1) e. (ZZ>=` (0 + 1))
93		elfzelz 7652	. . . . . . . . . . . . . 14 |- (k e. ((0 + 1)...(N + 1)) -> k e. ZZ)
94	93, 19, 30	3syl 24	. . . . . . . . . . . . 13 |- (k e. ((0 + 1)...(N + 1)) -> (k^2) e. CC)
95	94	rgen 2159	. . . . . . . . . . . 12 |- A.k e. ((0 + 1)...(N + 1))(k^2) e. CC
96		fsumcl 8275	. . . . . . . . . . . 12 |- (((N + 1) e. (ZZ>=` (0 + 1)) /\ A.k e. ((0 + 1)...(N + 1))(k^2) e. CC) -> sum_k e. ((0 + 1)...(N + 1))(k^2) e. CC)
97	92, 95, 96	mp2an 761	. . . . . . . . . . 11 |- sum_k e. ((0 + 1)...(N + 1))(k^2) e. CC
98	97	addid2i 6484	. . . . . . . . . 10 |- (0 + sum_k e. ((0 + 1)...(N + 1))(k^2)) = sum_k e. ((0 + 1)...(N + 1))(k^2)
99		nnnn0 7315	. . . . . . . . . . . . . 14 |- ((N + 1) e. NN -> (N + 1) e. NN0)
100	25, 99	syl 12	. . . . . . . . . . . . 13 |- (N e. NN -> (N + 1) e. NN0)
101	1, 100	ax-mp 7	. . . . . . . . . . . 12 |- (N + 1) e. NN0
102		elnn0uz 7610	. . . . . . . . . . . 12 |- ((N + 1) e. NN0 <-> (N + 1) e. (ZZ>=` 0))
103	101, 102	mpbi 206	. . . . . . . . . . 11 |- (N + 1) e. (ZZ>=` 0)
104	1	nngt0i 7133	. . . . . . . . . . . 12 |- 0 < N
105		lt01 6871	. . . . . . . . . . . 12 |- 0 < 1
106	85, 89, 104, 105	addgt0ii 6781	. . . . . . . . . . 11 |- 0 < (N + 1)
107		sq0i 7881	. . . . . . . . . . . 12 |- (k = 0 -> (k^2) = 0)
108	107	fsum1p 8279	. . . . . . . . . . 11 |- (((N + 1) e. (ZZ>=` 0) /\ 0 < (N + 1) /\ A.k e. (0...(N + 1))(k^2) e. CC) -> sum_k e. (0...(N + 1))(k^2) = (0 + sum_k e. ((0 + 1)...(N + 1))(k^2)))
109	103, 106, 32, 108	mp3an 1191	. . . . . . . . . 10 |- sum_k e. (0...(N + 1))(k^2) = (0 + sum_k e. ((0 + 1)...(N + 1))(k^2))
110	1	arisumilem 8486	. . . . . . . . . . 11 |- sum_k e. (0...N)((k + 1)^2) = sum_j e. (1...(N + 1))(j^2)
111		ax-17 1317	. . . . . . . . . . . 12 |- (x e. (j^2) -> A.k x e. (j^2))
112		ax-17 1317	. . . . . . . . . . . 12 |- (x e. (k^2) -> A.j x e. (k^2))
113		opreq1 4889	. . . . . . . . . . . 12 |- (j = k -> (j^2) = (k^2))
114	111, 112, 113	cbvsumi 8246	. . . . . . . . . . 11 |- sum_j e. (1...(N + 1))(j^2) = sum_k e. (1...(N + 1))(k^2)
115	5	addid2i 6484	. . . . . . . . . . . . . 14 |- (0 + 1) = 1
116	115	eqcomi 1888	. . . . . . . . . . . . 13 |- 1 = (0 + 1)
117	116	opreq1i 4892	. . . . . . . . . . . 12 |- (1...(N + 1)) = ((0 + 1)...(N + 1))
118	117	sumeq1i 8247	. . . . . . . . . . 11 |- sum_k e. (1...(N + 1))(k^2) = sum_k e. ((0 + 1)...(N + 1))(k^2)
119	110, 114, 118	3eqtri 1912	. . . . . . . . . 10 |- sum_k e. (0...N)((k + 1)^2) = sum_k e. ((0 + 1)...(N + 1))(k^2)
120	98, 109, 119	3eqtr4ri 1923	. . . . . . . . 9 |- sum_k e. (0...N)((k + 1)^2) = sum_k e. (0...(N + 1))(k^2)
121	39, 45, 49	addassi 6477	. . . . . . . . 9 |- ((sum_k e. (0...N)(k^2) + sum_k e. (0...N)(2 x. k)) + sum_k e. (0...N)1) = (sum_k e. (0...N)(k^2) + (sum_k e. (0...N)(2 x. k) + sum_k e. (0...N)1))
122	73, 120, 121	3eqtr3ri 1920	. . . . . . . 8 |- (sum_k e. (0...N)(k^2) + (sum_k e. (0...N)(2 x. k) + sum_k e. (0...N)1)) = sum_k e. (0...(N + 1))(k^2)
123	34, 39, 50, 122	subaddrii 6529	. . . . . . 7 |- (sum_k e. (0...(N + 1))(k^2) - sum_k e. (0...N)(k^2)) = (sum_k e. (0...N)(2 x. k) + sum_k e. (0...N)1)
124	8, 5	addcli 6473	. . . . . . . . 9 |- (N + 1) e. CC
125	124	sqcli 7860	. . . . . . . 8 |- ((N + 1)^2) e. CC
126		oprex 4907	. . . . . . . . . . 11 |- (k^2) e. _V
127		oprex 4907	. . . . . . . . . . 11 |- ((N + 1)^2) e. _V
128		opreq1 4889	. . . . . . . . . . 11 |- (k = (N + 1) -> (k^2) = ((N + 1)^2))
129	126, 127, 128	fsump1i 8266	. . . . . . . . . 10 |- (N e. (ZZ>=` 0) -> sum_k e. (0...(N + 1))(k^2) = (sum_k e. (0...N)(k^2) + ((N + 1)^2)))
130	4, 129	ax-mp 7	. . . . . . . . 9 |- sum_k e. (0...(N + 1))(k^2) = (sum_k e. (0...N)(k^2) + ((N + 1)^2))
131	130	eqcomi 1888	. . . . . . . 8 |- (sum_k e. (0...N)(k^2) + ((N + 1)^2)) = sum_k e. (0...(N + 1))(k^2)
132	34, 39, 125, 131	subaddrii 6529	. . . . . . 7 |- (sum_k e. (0...(N + 1))(k^2) - sum_k e. (0...N)(k^2)) = ((N + 1)^2)
133	123, 132	eqtr3i 1910	. . . . . 6 |- (sum_k e. (0...N)(2 x. k) + sum_k e. (0...N)1) = ((N + 1)^2)
134	16, 24, 133	3eqtri 1912	. . . . 5 |- ((2 x. sum_k e. (0...N)k) + (N + 1)) = ((N + 1)^2)
135		fsum0cl 8276	. . . . . . . 8 |- ((N e. NN0 /\ A.k e. (0...N)k e. CC) -> sum_k e. (0...N)k e. CC)
136	2, 21, 135	mp2an 761	. . . . . . 7 |- sum_k e. (0...N)k e. CC
137	17, 136	mulcli 6474	. . . . . 6 |- (2 x. sum_k e. (0...N)k) e. CC
138	125, 124, 137	subadd2i 6530	. . . . 5 |- ((((N + 1)^2) - (N + 1)) = (2 x. sum_k e. (0...N)k) <-> ((2 x. sum_k e. (0...N)k) + (N + 1)) = ((N + 1)^2))
139	134, 138	mpbir 207	. . . 4 |- (((N + 1)^2) - (N + 1)) = (2 x. sum_k e. (0...N)k)
140	139	eqcomi 1888	. . 3 |- (2 x. sum_k e. (0...N)k) = (((N + 1)^2) - (N + 1))
141	125, 124	subcli 6523	. . . 4 |- (((N + 1)^2) - (N + 1)) e. CC
142		2re 7163	. . . . 5 |- 2 e. RR
143	142	recni 6467	. . . 4 |- 2 e. CC
144		2ne0 7174	. . . 4 |- 2 =/= 0
145	141, 143, 136, 144	divmuli 6894	. . 3 |- (((((N + 1)^2) - (N + 1)) / 2) = sum_k e. (0...N)k <-> (2 x. sum_k e. (0...N)k) = (((N + 1)^2) - (N + 1)))
146	140, 145	mpbir 207	. 2 |- ((((N + 1)^2) - (N + 1)) / 2) = sum_k e. (0...N)k
147	146	eqcomi 1888	1 |- sum_k e. (0...N)k = ((((N + 1)^2) - (N + 1)) / 2)

Syntax hints:   /\ wa 240   = wceq 1298   e. wcel 1300  A.wral 2105   class class class wbr 3338  ` cfv 3998  (class class class)co 4884  CCcc 6384  0cc0 6386  1c1 6387   + caddc 6389   x. cmul 6391   - cmin 6445   / cdiv 6447   <_ cle 6448  NNcn 6449  NN0cn0 6450  ZZcz 6451   < clt 6653  2c2 7145  ZZ>=cuz 7586  ...cfz 7637  ^cexp 7811  sum_csu 8239

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-5 1302  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-13 1311  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-rep 3428  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524  ax-un 3790  ax-inf2 5731

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3or 859  df-3an 860  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-nel 2020  df-ral 2109  df-rex 2110  df-reu 2111  df-rab 2112  df-v 2294  df-sbc 2454  df-csb 2541  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-pss 2607  df-nul 2876  df-if 2983  df-pw 3035  df-sn 3049  df-pr 3050  df-tp 3052  df-op 3053  df-uni 3178  df-int 3215  df-iun 3257  df-br 3339  df-opab 3396  df-tr 3412  df-eprel 3583  df-id 3586  df-po 3591  df-so 3604  df-fr 3625  df-we 3644  df-ord 3660  df-on 3661  df-lim 3662  df-suc 3663  df-om 3950  df-xp 4000  df-rel 4001  df-cnv 4002  df-co 4003  df-dm 4004  df-rn 4005  df-res 4006  df-ima 4007  df-fun 4008  df-fn 4009  df-f 4010  df-f1 4011  df-fo 4012  df-f1o 4013  df-fv 4014  df-opr 4886  df-oprab 4887  df-mpt 5006  df-1st 5020  df-2nd 5021  df-iota 5089  df-rdg 5140  df-1o 5177  df-oadd 5179  df-omul 5180  df-er 5318  df-ec 5320  df-qs 5323  df-en 5427  df-dom 5428  df-sdom 5429  df-undef 5556  df-riota 5560  df-ni 6152  df-pli 6153  df-mi 6154  df-lti 6155  df-plpq 6187  df-mpq 6188  df-enq 6189  df-nq 6190  df-plq 6191  df-mq 6192  df-rq 6193  df-ltq 6194  df-1q 6195  df-np 6238  df-1p 6239  df-plp 6240  df-mp 6241  df-ltp 6242  df-plpr 6316  df-mpr 6317  df-enr 6318  df-nr 6319  df-plr 6320  df-mr 6321  df-ltr 6322  df-0r 6323  df-1r 6324  df-m1r 6325  df-c 6392  df-0 6393  df-1 6394  df-i 6395  df-r 6396  df-plus 6397  df-mul 6398  df-lt 6399  df-sub 6511  df-neg 6513  df-pnf 6654  df-mnf 6655  df-xr 6656  df-ltxr 6657  df-le 6658  df-div 6892  df-n 7108  df-2 7154  df-n0 7309  df-z 7345  df-q 7436  df-uz 7587  df-fz 7638  df-seq1 7721  df-shft 7754  df-seqz 7776  df-exp 7812  df-sum 8240

Copyright terms: Public domain