Theorem mettrifi2 15848

Description: Generalized triangle inequality for arbitrary finite sums.

Hypotheses

Ref	Expression
mettrifi2.1	|- X = dom dom M
mettrifi2.2	|- S e. _V

Assertion

Ref	Expression
mettrifi2	|- (((M e. Met /\ F:S-->X) /\ (N e. ZZ /\ P e. (ZZ>=` (N + 1)) /\ (N...P) C_ S)) -> ((F` N)M(F` P)) <_ sum_k e. (N...(P - 1))((F` k)M(F` (k + 1))))

Distinct variable groups:   k,M   k,N   k,F   S,k   k,X   P,k

Proof of Theorem mettrifi2

Step	Hyp	Ref	Expression
1		simpll 448	. . 3 |- (((M e. Met /\ F:S-->X) /\ (N e. ZZ /\ P e. (ZZ>=` (N + 1)) /\ (N...P) C_ S)) -> M e. Met)
2		eluzadd 15782	. . . . . . . 8 |- ((P e. (ZZ>=` (N + 1)) /\ -uN e. ZZ) -> (P + -uN) e. (ZZ>=` ((N + 1) + -uN)))
3		znegcl 7372	. . . . . . . 8 |- (N e. ZZ -> -uN e. ZZ)
4	2, 3	sylan2 500	. . . . . . 7 |- ((P e. (ZZ>=` (N + 1)) /\ N e. ZZ) -> (P + -uN) e. (ZZ>=` ((N + 1) + -uN)))
5	4	ancoms 484	. . . . . 6 |- ((N e. ZZ /\ P e. (ZZ>=` (N + 1))) -> (P + -uN) e. (ZZ>=` ((N + 1) + -uN)))
6		eluzelz 7592	. . . . . . . . . 10 |- (P e. (ZZ>=` (N + 1)) -> P e. ZZ)
7		zcn 7349	. . . . . . . . . 10 |- (P e. ZZ -> P e. CC)
8	6, 7	syl 12	. . . . . . . . 9 |- (P e. (ZZ>=` (N + 1)) -> P e. CC)
9	8	adantl 424	. . . . . . . 8 |- ((N e. ZZ /\ P e. (ZZ>=` (N + 1))) -> P e. CC)
10		zcn 7349	. . . . . . . . 9 |- (N e. ZZ -> N e. CC)
11	10	adantr 425	. . . . . . . 8 |- ((N e. ZZ /\ P e. (ZZ>=` (N + 1))) -> N e. CC)
12		negsub 6540	. . . . . . . 8 |- ((P e. CC /\ N e. CC) -> (P + -uN) = (P - N))
13	9, 11, 12	syl11anc 524	. . . . . . 7 |- ((N e. ZZ /\ P e. (ZZ>=` (N + 1))) -> (P + -uN) = (P - N))
14		peano2z 7375	. . . . . . . . . . . . 13 |- (N e. ZZ -> (N + 1) e. ZZ)
15		zcn 7349	. . . . . . . . . . . . 13 |- ((N + 1) e. ZZ -> (N + 1) e. CC)
16	14, 15	syl 12	. . . . . . . . . . . 12 |- (N e. ZZ -> (N + 1) e. CC)
17		negsub 6540	. . . . . . . . . . . 12 |- (((N + 1) e. CC /\ N e. CC) -> ((N + 1) + -uN) = ((N + 1) - N))
18	16, 10, 17	syl11anc 524	. . . . . . . . . . 11 |- (N e. ZZ -> ((N + 1) + -uN) = ((N + 1) - N))
19		pncan2 6558	. . . . . . . . . . . 12 |- ((N e. CC /\ 1 e. CC) -> ((N + 1) - N) = 1)
20		ax1cn 6422	. . . . . . . . . . . 12 |- 1 e. CC
21	19, 10, 20	sylancl 525	. . . . . . . . . . 11 |- (N e. ZZ -> ((N + 1) - N) = 1)
22	18, 21	eqtrd 1925	. . . . . . . . . 10 |- (N e. ZZ -> ((N + 1) + -uN) = 1)
23	22	fveq2d 4685	. . . . . . . . 9 |- (N e. ZZ -> (ZZ>=` ((N + 1) + -uN)) = (ZZ>=` 1))
24		nnuz 7608	. . . . . . . . 9 |- NN = (ZZ>=` 1)
25	23, 24	syl6eqr 1946	. . . . . . . 8 |- (N e. ZZ -> (ZZ>=` ((N + 1) + -uN)) = NN)
26	25	adantr 425	. . . . . . 7 |- ((N e. ZZ /\ P e. (ZZ>=` (N + 1))) -> (ZZ>=` ((N + 1) + -uN)) = NN)
27	13, 26	eleq12d 1965	. . . . . 6 |- ((N e. ZZ /\ P e. (ZZ>=` (N + 1))) -> ((P + -uN) e. (ZZ>=` ((N + 1) + -uN)) <-> (P - N) e. NN))
28	5, 27	mpbid 212	. . . . 5 |- ((N e. ZZ /\ P e. (ZZ>=` (N + 1))) -> (P - N) e. NN)
29	28	3adant3 896	. . . 4 |- ((N e. ZZ /\ P e. (ZZ>=` (N + 1)) /\ (N...P) C_ S) -> (P - N) e. NN)
30	29	adantl 424	. . 3 |- (((M e. Met /\ F:S-->X) /\ (N e. ZZ /\ P e. (ZZ>=` (N + 1)) /\ (N...P) C_ S)) -> (P - N) e. NN)
31		mettrifi2.2	. . . . . . . . . 10 |- S e. _V
32		fex 4595	. . . . . . . . . 10 |- ((F:S-->X /\ S e. _V) -> F e. _V)
33	31, 32	mpan2 760	. . . . . . . . 9 |- (F:S-->X -> F e. _V)
34		opreq1 4889	. . . . . . . . . . . . 13 |- (f = F -> (f shift -u(N - 1)) = (F shift -u(N - 1)))
35	34	fveq1d 4683	. . . . . . . . . . . 12 |- (f = F -> ((f shift -u(N - 1))` k) = ((F shift -u(N - 1))` k))
36		fveq1 4680	. . . . . . . . . . . 12 |- (f = F -> (f` ((N - 1) + k)) = (F` ((N - 1) + k)))
37	35, 36	eqeq12d 1899	. . . . . . . . . . 11 |- (f = F -> (((f shift -u(N - 1))` k) = (f` ((N - 1) + k)) <-> ((F shift -u(N - 1))` k) = (F` ((N - 1) + k))))
38	37	imbi2d 674	. . . . . . . . . 10 |- (f = F -> ((((N e. ZZ /\ P e. (ZZ>=` (N + 1)) /\ (N...P) C_ S) /\ k e. (1...((P - N) + 1))) -> ((f shift -u(N - 1))` k) = (f` ((N - 1) + k))) <-> (((N e. ZZ /\ P e. (ZZ>=` (N + 1)) /\ (N...P) C_ S) /\ k e. (1...((P - N) + 1))) -> ((F shift -u(N - 1))` k) = (F` ((N - 1) + k)))))
39		visset 2295	. . . . . . . . . . . 12 |- f e. _V
40	39	shftval4 7762	. . . . . . . . . . 11 |- (((N - 1) e. CC /\ k e. CC) -> ((f shift -u(N - 1))` k) = (f` ((N - 1) + k)))
41		subcl 6524	. . . . . . . . . . . . 13 |- ((N e. CC /\ 1 e. CC) -> (N - 1) e. CC)
42	41, 10, 20	sylancl 525	. . . . . . . . . . . 12 |- (N e. ZZ -> (N - 1) e. CC)
43	42	3ad2ant1 897	. . . . . . . . . . 11 |- ((N e. ZZ /\ P e. (ZZ>=` (N + 1)) /\ (N...P) C_ S) -> (N - 1) e. CC)
44		elfzuz 7658	. . . . . . . . . . . 12 |- (k e. (1...((P - N) + 1)) -> k e. (ZZ>=` 1))
45		eluzelz 7592	. . . . . . . . . . . 12 |- (k e. (ZZ>=` 1) -> k e. ZZ)
46		zcn 7349	. . . . . . . . . . . 12 |- (k e. ZZ -> k e. CC)
47	44, 45, 46	3syl 24	. . . . . . . . . . 11 |- (k e. (1...((P - N) + 1)) -> k e. CC)
48	40, 43, 47	syl2an 503	. . . . . . . . . 10 |- (((N e. ZZ /\ P e. (ZZ>=` (N + 1)) /\ (N...P) C_ S) /\ k e. (1...((P - N) + 1))) -> ((f shift -u(N - 1))` k) = (f` ((N - 1) + k)))
49	38, 48	vtoclg 2346	. . . . . . . . 9 |- (F e. _V -> (((N e. ZZ /\ P e. (ZZ>=` (N + 1)) /\ (N...P) C_ S) /\ k e. (1...((P - N) + 1))) -> ((F shift -u(N - 1))` k) = (F` ((N - 1) + k))))
50	33, 49	syl 12	. . . . . . . 8 |- (F:S-->X -> (((N e. ZZ /\ P e. (ZZ>=` (N + 1)) /\ (N...P) C_ S) /\ k e. (1...((P - N) + 1))) -> ((F shift -u(N - 1))` k) = (F` ((N - 1) + k))))
51	50	imp 377	. . . . . . 7 |- ((F:S-->X /\ ((N e. ZZ /\ P e. (ZZ>=` (N + 1)) /\ (N...P) C_ S) /\ k e. (1...((P - N) + 1)))) -> ((F shift -u(N - 1))` k) = (F` ((N - 1) + k)))
52	51	anassrs 489	. . . . . 6 |- (((F:S-->X /\ (N e. ZZ /\ P e. (ZZ>=` (N + 1)) /\ (N...P) C_ S)) /\ k e. (1...((P - N) + 1))) -> ((F shift -u(N - 1))` k) = (F` ((N - 1) + k)))
53	52	adantlll 432	. . . . 5 |- ((((M e. Met /\ F:S-->X) /\ (N e. ZZ /\ P e. (ZZ>=` (N + 1)) /\ (N...P) C_ S)) /\ k e. (1...((P - N) + 1))) -> ((F shift -u(N - 1))` k) = (F` ((N - 1) + k)))
54		1z 7368	. . . . . . . . . . . . 13 |- 1 e. ZZ
55	54	a1i 8	. . . . . . . . . . . 12 |- ((((M e. Met /\ F:S-->X) /\ (N e. ZZ /\ P e. (ZZ>=` (N + 1)) /\ (N...P) C_ S)) /\ k e. (1...((P - N) + 1))) -> 1 e. ZZ)
56	6	3ad2ant2 898	. . . . . . . . . . . . . . 15 |- ((N e. ZZ /\ P e. (ZZ>=` (N + 1)) /\ (N...P) C_ S) -> P e. ZZ)
57		simp1 876	. . . . . . . . . . . . . . 15 |- ((N e. ZZ /\ P e. (ZZ>=` (N + 1)) /\ (N...P) C_ S) -> N e. ZZ)
58		zsubcl 7377	. . . . . . . . . . . . . . 15 |- ((P e. ZZ /\ N e. ZZ) -> (P - N) e. ZZ)
59	56, 57, 58	syl11anc 524	. . . . . . . . . . . . . 14 |- ((N e. ZZ /\ P e. (ZZ>=` (N + 1)) /\ (N...P) C_ S) -> (P - N) e. ZZ)
60	59	peano2zdi 7376	. . . . . . . . . . . . 13 |- ((N e. ZZ /\ P e. (ZZ>=` (N + 1)) /\ (N...P) C_ S) -> ((P - N) + 1) e. ZZ)
61	60	ad2antlr 441	. . . . . . . . . . . 12 |- ((((M e. Met /\ F:S-->X) /\ (N e. ZZ /\ P e. (ZZ>=` (N + 1)) /\ (N...P) C_ S)) /\ k e. (1...((P - N) + 1))) -> ((P - N) + 1) e. ZZ)
62		elfzelz 7652	. . . . . . . . . . . . 13 |- (k e. (1...((P - N) + 1)) -> k e. ZZ)
63	62	adantl 424	. . . . . . . . . . . 12 |- ((((M e. Met /\ F:S-->X) /\ (N e. ZZ /\ P e. (ZZ>=` (N + 1)) /\ (N...P) C_ S)) /\ k e. (1...((P - N) + 1))) -> k e. ZZ)
64		peano2zm 7378	. . . . . . . . . . . . . 14 |- (N e. ZZ -> (N - 1) e. ZZ)
65	64	3ad2ant1 897	. . . . . . . . . . . . 13 |- ((N e. ZZ /\ P e. (ZZ>=` (N + 1)) /\ (N...P) C_ S) -> (N - 1) e. ZZ)
66	65	ad2antlr 441	. . . . . . . . . . . 12 |- ((((M e. Met /\ F:S-->X) /\ (N e. ZZ /\ P e. (ZZ>=` (N + 1)) /\ (N...P) C_ S)) /\ k e. (1...((P - N) + 1))) -> (N - 1) e. ZZ)
67		fzaddel 7672	. . . . . . . . . . . 12 |- (((1 e. ZZ /\ ((P - N) + 1) e. ZZ) /\ (k e. ZZ /\ (N - 1) e. ZZ)) -> (k e. (1...((P - N) + 1)) <-> (k + (N - 1)) e. ((1 + (N - 1))...(((P - N) + 1) + (N - 1)))))
68	55, 61, 63, 66, 67	syl22anc 1101	. . . . . . . . . . 11 |- ((((M e. Met /\ F:S-->X) /\ (N e. ZZ /\ P e. (ZZ>=` (N + 1)) /\ (N...P) C_ S)) /\ k e. (1...((P - N) + 1))) -> (k e. (1...((P - N) + 1)) <-> (k + (N - 1)) e. ((1 + (N - 1))...(((P - N) + 1) + (N - 1)))))
69	68	biimpd 170	. . . . . . . . . 10 |- ((((M e. Met /\ F:S-->X) /\ (N e. ZZ /\ P e. (ZZ>=` (N + 1)) /\ (N...P) C_ S)) /\ k e. (1...((P - N) + 1))) -> (k e. (1...((P - N) + 1)) -> (k + (N - 1)) e. ((1 + (N - 1))...(((P - N) + 1) + (N - 1)))))
70	47	adantl 424	. . . . . . . . . . . 12 |- ((((M e. Met /\ F:S-->X) /\ (N e. ZZ /\ P e. (ZZ>=` (N + 1)) /\ (N...P) C_ S)) /\ k e. (1...((P - N) + 1))) -> k e. CC)
71	43	ad2antlr 441	. . . . . . . . . . . 12 |- ((((M e. Met /\ F:S-->X) /\ (N e. ZZ /\ P e. (ZZ>=` (N + 1)) /\ (N...P) C_ S)) /\ k e. (1...((P - N) + 1))) -> (N - 1) e. CC)
72		addcom 6458	. . . . . . . . . . . 12 |- ((k e. CC /\ (N - 1) e. CC) -> (k + (N - 1)) = ((N - 1) + k))
73	70, 71, 72	syl11anc 524	. . . . . . . . . . 11 |- ((((M e. Met /\ F:S-->X) /\ (N e. ZZ /\ P e. (ZZ>=` (N + 1)) /\ (N...P) C_ S)) /\ k e. (1...((P - N) + 1))) -> (k + (N - 1)) = ((N - 1) + k))
74		pncan3 6534	. . . . . . . . . . . . . 14 |- ((1 e. CC /\ N e. CC) -> (1 + (N - 1)) = N)
75	10	3ad2ant1 897	. . . . . . . . . . . . . 14 |- ((N e. ZZ /\ P e. (ZZ>=` (N + 1)) /\ (N...P) C_ S) -> N e. CC)
76	74, 20, 75	sylancr 526	. . . . . . . . . . . . 13 |- ((N e. ZZ /\ P e. (ZZ>=` (N + 1)) /\ (N...P) C_ S) -> (1 + (N - 1)) = N)
77	8	3ad2ant2 898	. . . . . . . . . . . . . 14 |- ((N e. ZZ /\ P e. (ZZ>=` (N + 1)) /\ (N...P) C_ S) -> P e. CC)
78		addcl 6454	. . . . . . . . . . . . . . . . 17 |- (((P - N) e. CC /\ 1 e. CC) -> ((P - N) + 1) e. CC)
79		subcl 6524	. . . . . . . . . . . . . . . . . 18 |- ((P e. CC /\ N e. CC) -> (P - N) e. CC)
80	79	ancoms 484	. . . . . . . . . . . . . . . . 17 |- ((N e. CC /\ P e. CC) -> (P - N) e. CC)
81	78, 80, 20	sylancl 525	. . . . . . . . . . . . . . . 16 |- ((N e. CC /\ P e. CC) -> ((P - N) + 1) e. CC)
82		simpl 346	. . . . . . . . . . . . . . . 16 |- ((N e. CC /\ P e. CC) -> N e. CC)
83	20	a1i 8	. . . . . . . . . . . . . . . 16 |- ((N e. CC /\ P e. CC) -> 1 e. CC)
84		addsub12 6545	. . . . . . . . . . . . . . . 16 |- ((((P - N) + 1) e. CC /\ N e. CC /\ 1 e. CC) -> (((P - N) + 1) + (N - 1)) = (N + (((P - N) + 1) - 1)))
85	81, 82, 83, 84	syl111anc 1100	. . . . . . . . . . . . . . 15 |- ((N e. CC /\ P e. CC) -> (((P - N) + 1) + (N - 1)) = (N + (((P - N) + 1) - 1)))
86		pncan 6557	. . . . . . . . . . . . . . . . 17 |- (((P - N) e. CC /\ 1 e. CC) -> (((P - N) + 1) - 1) = (P - N))
87	86, 80, 20	sylancl 525	. . . . . . . . . . . . . . . 16 |- ((N e. CC /\ P e. CC) -> (((P - N) + 1) - 1) = (P - N))
88	87	opreq2d 4898	. . . . . . . . . . . . . . 15 |- ((N e. CC /\ P e. CC) -> (N + (((P - N) + 1) - 1)) = (N + (P - N)))
89		pncan3 6534	. . . . . . . . . . . . . . 15 |- ((N e. CC /\ P e. CC) -> (N + (P - N)) = P)
90	85, 88, 89	3eqtrd 1929	. . . . . . . . . . . . . 14 |- ((N e. CC /\ P e. CC) -> (((P - N) + 1) + (N - 1)) = P)
91	75, 77, 90	syl11anc 524	. . . . . . . . . . . . 13 |- ((N e. ZZ /\ P e. (ZZ>=` (N + 1)) /\ (N...P) C_ S) -> (((P - N) + 1) + (N - 1)) = P)
92	76, 91	opreq12d 4900	. . . . . . . . . . . 12 |- ((N e. ZZ /\ P e. (ZZ>=` (N + 1)) /\ (N...P) C_ S) -> ((1 + (N - 1))...(((P - N) + 1) + (N - 1))) = (N...P))
93	92	ad2antlr 441	. . . . . . . . . . 11 |- ((((M e. Met /\ F:S-->X) /\ (N e. ZZ /\ P e. (ZZ>=` (N + 1)) /\ (N...P) C_ S)) /\ k e. (1...((P - N) + 1))) -> ((1 + (N - 1))...(((P - N) + 1) + (N - 1))) = (N...P))
94	73, 93	eleq12d 1965	. . . . . . . . . 10 |- ((((M e. Met /\ F:S-->X) /\ (N e. ZZ /\ P e. (ZZ>=` (N + 1)) /\ (N...P) C_ S)) /\ k e. (1...((P - N) + 1))) -> ((k + (N - 1)) e. ((1 + (N - 1))...(((P - N) + 1) + (N - 1))) <-> ((N - 1) + k) e. (N...P)))
95	69, 94	sylibd 219	. . . . . . . . 9 |- ((((M e. Met /\ F:S-->X) /\ (N e. ZZ /\ P e. (ZZ>=` (N + 1)) /\ (N...P) C_ S)) /\ k e. (1...((P - N) + 1))) -> (k e. (1...((P - N) + 1)) -> ((N - 1) + k) e. (N...P)))
96	95	ex 402	. . . . . . . 8 |- (((M e. Met /\ F:S-->X) /\ (N e. ZZ /\ P e. (ZZ>=` (N + 1)) /\ (N...P) C_ S)) -> (k e. (1...((P - N) + 1)) -> (k e. (1...((P - N) + 1)) -> ((N - 1) + k) e. (N...P))))
97	96	pm2.43d 79	. . . . . . 7 |- (((M e. Met /\ F:S-->X) /\ (N e. ZZ /\ P e. (ZZ>=` (N + 1)) /\ (N...P) C_ S)) -> (k e. (1...((P - N) + 1)) -> ((N - 1) + k) e. (N...P)))
98		ffvelrn 4787	. . . . . . . . . . . 12 |- ((F:S-->X /\ ((N - 1) + k) e. S) -> (F` ((N - 1) + k)) e. X)
99	98	ex 402	. . . . . . . . . . 11 |- (F:S-->X -> (((N - 1) + k) e. S -> (F` ((N - 1) + k)) e. X))
100		ssel2 2616	. . . . . . . . . . 11 |- (((N...P) C_ S /\ ((N - 1) + k) e. (N...P)) -> ((N - 1) + k) e. S)
101	99, 100	syl5 20	. . . . . . . . . 10 |- (F:S-->X -> (((N...P) C_ S /\ ((N - 1) + k) e. (N...P)) -> (F` ((N - 1) + k)) e. X))
102	101	expdimp 406	. . . . . . . . 9 |- ((F:S-->X /\ (N...P) C_ S) -> (((N - 1) + k) e. (N...P) -> (F` ((N - 1) + k)) e. X))
103	102	3ad2antr3 1043	. . . . . . . 8 |- ((F:S-->X /\ (N e. ZZ /\ P e. (ZZ>=` (N + 1)) /\ (N...P) C_ S)) -> (((N - 1) + k) e. (N...P) -> (F` ((N - 1) + k)) e. X))
104	103	adantll 428	. . . . . . 7 |- (((M e. Met /\ F:S-->X) /\ (N e. ZZ /\ P e. (ZZ>=` (N + 1)) /\ (N...P) C_ S)) -> (((N - 1) + k) e. (N...P) -> (F` ((N - 1) + k)) e. X))
105	97, 104	syld 30	. . . . . 6 |- (((M e. Met /\ F:S-->X) /\ (N e. ZZ /\ P e. (ZZ>=` (N + 1)) /\ (N...P) C_ S)) -> (k e. (1...((P - N) + 1)) -> (F` ((N - 1) + k)) e. X))
106	105	imp 377	. . . . 5 |- ((((M e. Met /\ F:S-->X) /\ (N e. ZZ /\ P e. (ZZ>=` (N + 1)) /\ (N...P) C_ S)) /\ k e. (1...((P - N) + 1))) -> (F` ((N - 1) + k)) e. X)
107	53, 106	eqeltrd 1971	. . . 4 |- ((((M e. Met /\ F:S-->X) /\ (N e. ZZ /\ P e. (ZZ>=` (N + 1)) /\ (N...P) C_ S)) /\ k e. (1...((P - N) + 1))) -> ((F shift -u(N - 1))` k) e. X)
108	107	r19.21aiva 2176	. . 3 |- (((M e. Met /\ F:S-->X) /\ (N e. ZZ /\ P e. (ZZ>=` (N + 1)) /\ (N...P) C_ S)) -> A.k e. (1...((P - N) + 1))((F shift -u(N - 1))` k) e. X)
109		fveq2 4681	. . . . . . 7 |- (j = k -> ((F shift -u(N - 1))` j) = ((F shift -u(N - 1))` k))
110		opreq1 4889	. . . . . . . 8 |- (j = k -> (j + 1) = (k + 1))
111	110	fveq2d 4685	. . . . . . 7 |- (j = k -> ((F shift -u(N - 1))` (j + 1)) = ((F shift -u(N - 1))` (k + 1)))
112	109, 111	opreq12d 4900	. . . . . 6 |- (j = k -> (((F shift -u(N - 1))` j)M((F shift -u(N - 1))` (j + 1))) = (((F shift -u(N - 1))` k)M((F shift -u(N - 1))` (k + 1))))
113		eqid 1884	. . . . . 6 |- {<.j, z>. | (j e. (1...(P - N)) /\ z = (((F shift -u(N - 1))` j)M((F shift -u(N - 1))` (j + 1))))} = {<.j, z>. | (j e. (1...(P - N)) /\ z = (((F shift -u(N - 1))` j)M((F shift -u(N - 1))` (j + 1))))}
114		oprex 4907	. . . . . 6 |- (((F shift -u(N - 1))` k)M((F shift -u(N - 1))` (k + 1))) e. _V
115	112, 113, 114	fvopab4 4743	. . . . 5 |- (k e. (1...(P - N)) -> ({<.j, z>. | (j e. (1...(P - N)) /\ z = (((F shift -u(N - 1))` j)M((F shift -u(N - 1))` (j + 1))))}` k) = (((F shift -u(N - 1))` k)M((F shift -u(N - 1))` (k + 1))))
116	115	rgen 2159	. . . 4 |- A.k e. (1...(P - N))({<.j, z>. | (j e. (1...(P - N)) /\ z = (((F shift -u(N - 1))` j)M((F shift -u(N - 1))` (j + 1))))}` k) = (((F shift -u(N - 1))` k)M((F shift -u(N - 1))` (k + 1)))
117	116	a1i 8	. . 3 |- (((M e. Met /\ F:S-->X) /\ (N e. ZZ /\ P e. (ZZ>=` (N + 1)) /\ (N...P) C_ S)) -> A.k e. (1...(P - N))({<.j, z>. | (j e. (1...(P - N)) /\ z = (((F shift -u(N - 1))` j)M((F shift -u(N - 1))` (j + 1))))}` k) = (((F shift -u(N - 1))` k)M((F shift -u(N - 1))` (k + 1))))
118		mettrifi2.1	. . . 4 |- X = dom dom M
119	118	mettrifi 15847	. . 3 |- (((M e. Met /\ (P - N) e. NN) /\ (A.k e. (1...((P - N) + 1))((F shift -u(N - 1))` k) e. X /\ A.k e. (1...(P - N))({<.j, z>. | (j e. (1...(P - N)) /\ z = (((F shift -u(N - 1))` j)M((F shift -u(N - 1))` (j + 1))))}` k) = (((F shift -u(N - 1))` k)M((F shift -u(N - 1))` (k + 1))))) -> (((F shift -u(N - 1))` 1)M((F shift -u(N - 1))` ((P - N) + 1))) <_ sum_k e. (1...(P - N))({<.j, z>. | (j e. (1...(P - N)) /\ z = (((F shift -u(N - 1))` j)M((F shift -u(N - 1))` (j + 1))))}` k))
120	1, 30, 108, 117, 119	syl22anc 1101	. 2 |- (((M e. Met /\ F:S-->X) /\ (N e. ZZ /\ P e. (ZZ>=` (N + 1)) /\ (N...P) C_ S)) -> (((F shift -u(N - 1))` 1)M((F shift -u(N - 1))` ((P - N) + 1))) <_ sum_k e. (1...(P - N))({<.j, z>. | (j e. (1...(P - N)) /\ z = (((F shift -u(N - 1))` j)M((F shift -u(N - 1))` (j + 1))))}` k))
121	34	fveq1d 4683	. . . . . . . . 9 |- (f = F -> ((f shift -u(N - 1))` 1) = ((F shift -u(N - 1))` 1))
122	34	fveq1d 4683	. . . . . . . . 9 |- (f = F -> ((f shift -u(N - 1))` ((P - N) + 1)) = ((F shift -u(N - 1))` ((P - N) + 1)))
123	121, 122	opreq12d 4900	. . . . . . . 8 |- (f = F -> (((f shift -u(N - 1))` 1)M((f shift -u(N - 1))` ((P - N) + 1))) = (((F shift -u(N - 1))` 1)M((F shift -u(N - 1))` ((P - N) + 1))))
124		fveq1 4680	. . . . . . . . 9 |- (f = F -> (f` N) = (F` N))
125		fveq1 4680	. . . . . . . . 9 |- (f = F -> (f` P) = (F` P))
126	124, 125	opreq12d 4900	. . . . . . . 8 |- (f = F -> ((f` N)M(f` P)) = ((F` N)M(F` P)))
127	123, 126	eqeq12d 1899	. . . . . . 7 |- (f = F -> ((((f shift -u(N - 1))` 1)M((f shift -u(N - 1))` ((P - N) + 1))) = ((f` N)M(f` P)) <-> (((F shift -u(N - 1))` 1)M((F shift -u(N - 1))` ((P - N) + 1))) = ((F` N)M(F` P))))
128	127	imbi2d 674	. . . . . 6 |- (f = F -> (((N e. ZZ /\ P e. (ZZ>=` (N + 1)) /\ (N...P) C_ S) -> (((f shift -u(N - 1))` 1)M((f shift -u(N - 1))` ((P - N) + 1))) = ((f` N)M(f` P))) <-> ((N e. ZZ /\ P e. (ZZ>=` (N + 1)) /\ (N...P) C_ S) -> (((F shift -u(N - 1))` 1)M((F shift -u(N - 1))` ((P - N) + 1))) = ((F` N)M(F` P)))))
129	39	shftval4 7762	. . . . . . . . . 10 |- (((N - 1) e. CC /\ 1 e. CC) -> ((f shift -u(N - 1))` 1) = (f` ((N - 1) + 1)))
130	20, 41	mpan2 760	. . . . . . . . . . 11 |- (N e. CC -> (N - 1) e. CC)
131	130	adantr 425	. . . . . . . . . 10 |- ((N e. CC /\ P e. CC) -> (N - 1) e. CC)
132	129, 131, 20	sylancl 525	. . . . . . . . 9 |- ((N e. CC /\ P e. CC) -> ((f shift -u(N - 1))` 1) = (f` ((N - 1) + 1)))
133		npcan 6559	. . . . . . . . . . 11 |- ((N e. CC /\ 1 e. CC) -> ((N - 1) + 1) = N)
134	20	a1i 8	. . . . . . . . . . 11 |- (P e. CC -> 1 e. CC)
135	133, 134	sylan2 500	. . . . . . . . . 10 |- ((N e. CC /\ P e. CC) -> ((N - 1) + 1) = N)
136	135	fveq2d 4685	. . . . . . . . 9 |- ((N e. CC /\ P e. CC) -> (f` ((N - 1) + 1)) = (f` N))
137	132, 136	eqtrd 1925	. . . . . . . 8 |- ((N e. CC /\ P e. CC) -> ((f shift -u(N - 1))` 1) = (f` N))
138	39	shftval4 7762	. . . . . . . . . 10 |- (((N - 1) e. CC /\ ((P - N) + 1) e. CC) -> ((f shift -u(N - 1))` ((P - N) + 1)) = (f` ((N - 1) + ((P - N) + 1))))
139	131, 81, 138	syl11anc 524	. . . . . . . . 9 |- ((N e. CC /\ P e. CC) -> ((f shift -u(N - 1))` ((P - N) + 1)) = (f` ((N - 1) + ((P - N) + 1))))
140		subadd23 6544	. . . . . . . . . . . 12 |- ((N e. CC /\ 1 e. CC /\ ((P - N) + 1) e. CC) -> ((N - 1) + ((P - N) + 1)) = (N + (((P - N) + 1) - 1)))
141	82, 83, 81, 140	syl111anc 1100	. . . . . . . . . . 11 |- ((N e. CC /\ P e. CC) -> ((N - 1) + ((P - N) + 1)) = (N + (((P - N) + 1) - 1)))
142	141, 88, 89	3eqtrd 1929	. . . . . . . . . 10 |- ((N e. CC /\ P e. CC) -> ((N - 1) + ((P - N) + 1)) = P)
143	142	fveq2d 4685	. . . . . . . . 9 |- ((N e. CC /\ P e. CC) -> (f` ((N - 1) + ((P - N) + 1))) = (f` P))
144	139, 143	eqtrd 1925	. . . . . . . 8 |- ((N e. CC /\ P e. CC) -> ((f shift -u(N - 1))` ((P - N) + 1)) = (f` P))
145	137, 144	opreq12d 4900	. . . . . . 7 |- ((N e. CC /\ P e. CC) -> (((f shift -u(N - 1))` 1)M((f shift -u(N - 1))` ((P - N) + 1))) = ((f` N)M(f` P)))
146	75, 77, 145	syl11anc 524	. . . . . 6 |- ((N e. ZZ /\ P e. (ZZ>=` (N + 1)) /\ (N...P) C_ S) -> (((f shift -u(N - 1))` 1)M((f shift -u(N - 1))` ((P - N) + 1))) = ((f` N)M(f` P)))
147	128, 146	vtoclg 2346	. . . . 5 |- (F e. _V -> ((N e. ZZ /\ P e. (ZZ>=` (N + 1)) /\ (N...P) C_ S) -> (((F shift -u(N - 1))` 1)M((F shift -u(N - 1))` ((P - N) + 1))) = ((F` N)M(F` P))))
148	33, 147	syl 12	. . . 4 |- (F:S-->X -> ((N e. ZZ /\ P e. (ZZ>=` (N + 1)) /\ (N...P) C_ S) -> (((F shift -u(N - 1))` 1)M((F shift -u(N - 1))` ((P - N) + 1))) = ((F` N)M(F` P))))
149	148	imp 377	. . 3 |- ((F:S-->X /\ (N e. ZZ /\ P e. (ZZ>=` (N + 1)) /\ (N...P) C_ S)) -> (((F shift -u(N - 1))` 1)M((F shift -u(N - 1))` ((P - N) + 1))) = ((F` N)M(F` P)))
150	149	adantll 428	. 2 |- (((M e. Met /\ F:S-->X) /\ (N e. ZZ /\ P e. (ZZ>=` (N + 1)) /\ (N...P) C_ S)) -> (((F shift -u(N - 1))` 1)M((F shift -u(N - 1))` ((P - N) + 1))) = ((F` N)M(F` P)))
151	115	sumeq2i 8248	. . . 4 |- sum_k e. (1...(P - N))({<.j, z>. | (j e. (1...(P - N)) /\ z = (((F shift -u(N - 1))` j)M((F shift -u(N - 1))` (j + 1))))}` k) = sum_k e. (1...(P - N))(((F shift -u(N - 1))` k)M((F shift -u(N - 1))` (k + 1)))
152	151	a1i 8	. . 3 |- (((M e. Met /\ F:S-->X) /\ (N e. ZZ /\ P e. (ZZ>=` (N + 1)) /\ (N...P) C_ S)) -> sum_k e. (1...(P - N))({<.j, z>. | (j e. (1...(P - N)) /\ z = (((F shift -u(N - 1))` j)M((F shift -u(N - 1))` (j + 1))))}` k) = sum_k e. (1...(P - N))(((F shift -u(N - 1))` k)M((F shift -u(N - 1))` (k + 1))))
153	28, 24	syl6eleq 1981	. . . . . 6 |- ((N e. ZZ /\ P e. (ZZ>=` (N + 1))) -> (P - N) e. (ZZ>=` 1))
154	153	3adant3 896	. . . . 5 |- ((N e. ZZ /\ P e. (ZZ>=` (N + 1)) /\ (N...P) C_ S) -> (P - N) e. (ZZ>=` 1))
155	154	adantl 424	. . . 4 |- (((M e. Met /\ F:S-->X) /\ (N e. ZZ /\ P e. (ZZ>=` (N + 1)) /\ (N...P) C_ S)) -> (P - N) e. (ZZ>=` 1))
156	65	adantl 424	. . . 4 |- (((M e. Met /\ F:S-->X) /\ (N e. ZZ /\ P e. (ZZ>=` (N + 1)) /\ (N...P) C_ S)) -> (N - 1) e. ZZ)
157		simplll 452	. . . . . . 7 |- ((((M e. Met /\ F:S-->X) /\ (N e. ZZ /\ P e. (ZZ>=` (N + 1)) /\ (N...P) C_ S)) /\ k e. (1...(P - N))) -> M e. Met)
158		oprex 4907	. . . . . . . . 9 |- (P - N) e. _V
159	158	fzelp1i 7682	. . . . . . . 8 |- (k e. (1...(P - N)) -> k e. (1...((P - N) + 1)))
160	107, 159	sylan2 500	. . . . . . 7 |- ((((M e. Met /\ F:S-->X) /\ (N e. ZZ /\ P e. (ZZ>=` (N + 1)) /\ (N...P) C_ S)) /\ k e. (1...(P - N))) -> ((F shift -u(N - 1))` k) e. X)
161	34	fveq1d 4683	. . . . . . . . . . . . . . . 16 |- (f = F -> ((f shift -u(N - 1))` (k + 1)) = ((F shift -u(N - 1))` (k + 1)))
162		fveq1 4680	. . . . . . . . . . . . . . . 16 |- (f = F -> (f` ((N - 1) + (k + 1))) = (F` ((N - 1) + (k + 1))))
163	161, 162	eqeq12d 1899	. . . . . . . . . . . . . . 15 |- (f = F -> (((f shift -u(N - 1))` (k + 1)) = (f` ((N - 1) + (k + 1))) <-> ((F shift -u(N - 1))` (k + 1)) = (F` ((N - 1) + (k + 1)))))
164	163	imbi2d 674	. . . . . . . . . . . . . 14 |- (f = F -> ((((N e. ZZ /\ P e. (ZZ>=` (N + 1)) /\ (N...P) C_ S) /\ k e. (1...(P - N))) -> ((f shift -u(N - 1))` (k + 1)) = (f` ((N - 1) + (k + 1)))) <-> (((N e. ZZ /\ P e. (ZZ>=` (N + 1)) /\ (N...P) C_ S) /\ k e. (1...(P - N))) -> ((F shift -u(N - 1))` (k + 1)) = (F` ((N - 1) + (k + 1))))))
165	39	shftval4 7762	. . . . . . . . . . . . . . 15 |- (((N - 1) e. CC /\ (k + 1) e. CC) -> ((f shift -u(N - 1))` (k + 1)) = (f` ((N - 1) + (k + 1))))
166		elfzuz 7658	. . . . . . . . . . . . . . . 16 |- (k e. (1...(P - N)) -> k e. (ZZ>=` 1))
167		peano2z 7375	. . . . . . . . . . . . . . . . 17 |- (k e. ZZ -> (k + 1) e. ZZ)
168		zcn 7349	. . . . . . . . . . . . . . . . 17 |- ((k + 1) e. ZZ -> (k + 1) e. CC)
169	167, 168	syl 12	. . . . . . . . . . . . . . . 16 |- (k e. ZZ -> (k + 1) e. CC)
170	166, 45, 169	3syl 24	. . . . . . . . . . . . . . 15 |- (k e. (1...(P - N)) -> (k + 1) e. CC)
171	165, 43, 170	syl2an 503	. . . . . . . . . . . . . 14 |- (((N e. ZZ /\ P e. (ZZ>=` (N + 1)) /\ (N...P) C_ S) /\ k e. (1...(P - N))) -> ((f shift -u(N - 1))` (k + 1)) = (f` ((N - 1) + (k + 1))))
172	164, 171	vtoclg 2346	. . . . . . . . . . . . 13 |- (F e. _V -> (((N e. ZZ /\ P e. (ZZ>=` (N + 1)) /\ (N...P) C_ S) /\ k e. (1...(P - N))) -> ((F shift -u(N - 1))` (k + 1)) = (F` ((N - 1) + (k + 1)))))
173	33, 172	syl 12	. . . . . . . . . . . 12 |- (F:S-->X -> (((N e. ZZ /\ P e. (ZZ>=` (N + 1)) /\ (N...P) C_ S) /\ k e. (1...(P - N))) -> ((F shift -u(N - 1))` (k + 1)) = (F` ((N - 1) + (k + 1)))))
174	173	imp 377	. . . . . . . . . . 11 |- ((F:S-->X /\ ((N e. ZZ /\ P e. (ZZ>=` (N + 1)) /\ (N...P) C_ S) /\ k e. (1...(P - N)))) -> ((F shift -u(N - 1))` (k + 1)) = (F` ((N - 1) + (k + 1))))
175	174	anassrs 489	. . . . . . . . . 10 |- (((F:S-->X /\ (N e. ZZ /\ P e. (ZZ>=` (N + 1)) /\ (N...P) C_ S)) /\ k e. (1...(P - N))) -> ((F shift -u(N - 1))` (k + 1)) = (F` ((N - 1) + (k + 1))))
176	175	adantlll 432	. . . . . . . . 9 |- ((((M e. Met /\ F:S-->X) /\ (N e. ZZ /\ P e. (ZZ>=` (N + 1)) /\ (N...P) C_ S)) /\ k e. (1...(P - N))) -> ((F shift -u(N - 1))` (k + 1)) = (F` ((N - 1) + (k + 1))))
177		simpl 346	. . . . . . . . . . . . . 14 |- ((N e. CC /\ k e. CC) -> N e. CC)
178	20	a1i 8	. . . . . . . . . . . . . 14 |- ((N e. CC /\ k e. CC) -> 1 e. CC)
179		peano2cn 6498	. . . . . . . . . . . . . . 15 |- (k e. CC -> (k + 1) e. CC)
180	179	adantl 424	. . . . . . . . . . . . . 14 |- ((N e. CC /\ k e. CC) -> (k + 1) e. CC)
181		subadd23 6544	. . . . . . . . . . . . . 14 |- ((N e. CC /\ 1 e. CC /\ (k + 1) e. CC) -> ((N - 1) + (k + 1)) = (N + ((k + 1) - 1)))
182	177, 178, 180, 181	syl111anc 1100	. . . . . . . . . . . . 13 |- ((N e. CC /\ k e. CC) -> ((N - 1) + (k + 1)) = (N + ((k + 1) - 1)))
183		pncan 6557	. . . . . . . . . . . . . . 15 |- ((k e. CC /\ 1 e. CC) -> ((k + 1) - 1) = k)
184		simpr 350	. . . . . . . . . . . . . . 15 |- ((N e. CC /\ k e. CC) -> k e. CC)
185	183, 184, 20	sylancl 525	. . . . . . . . . . . . . 14 |- ((N e. CC /\ k e. CC) -> ((k + 1) - 1) = k)
186	185	opreq2d 4898	. . . . . . . . . . . . 13 |- ((N e. CC /\ k e. CC) -> (N + ((k + 1) - 1)) = (N + k))
187		addcom 6458	. . . . . . . . . . . . 13 |- ((N e. CC /\ k e. CC) -> (N + k) = (k + N))
188	182, 186, 187	3eqtrd 1929	. . . . . . . . . . . 12 |- ((N e. CC /\ k e. CC) -> ((N - 1) + (k + 1)) = (k + N))
189	166, 45, 46	3syl 24	. . . . . . . . . . . 12 |- (k e. (1...(P - N)) -> k e. CC)
190	188, 75, 189	syl2an 503	. . . . . . . . . . 11 |- (((N e. ZZ /\ P e. (ZZ>=` (N + 1)) /\ (N...P) C_ S) /\ k e. (1...(P - N))) -> ((N - 1) + (k + 1)) = (k + N))
191	190	fveq2d 4685	. . . . . . . . . 10 |- (((N e. ZZ /\ P e. (ZZ>=` (N + 1)) /\ (N...P) C_ S) /\ k e. (1...(P - N))) -> (F` ((N - 1) + (k + 1))) = (F` (k + N)))
192	191	adantll 428	. . . . . . . . 9 |- ((((M e. Met /\ F:S-->X) /\ (N e. ZZ /\ P e. (ZZ>=` (N + 1)) /\ (N...P) C_ S)) /\ k e. (1...(P - N))) -> (F` ((N - 1) + (k + 1))) = (F` (k + N)))
193	176, 192	eqtrd 1925	. . . . . . . 8 |- ((((M e. Met /\ F:S-->X) /\ (N e. ZZ /\ P e. (ZZ>=` (N + 1)) /\ (N...P) C_ S)) /\ k e. (1...(P - N))) -> ((F shift -u(N - 1))` (k + 1)) = (F` (k + N)))
194		simpr 350	. . . . . . . . 9 |- ((((M e. Met /\ F:S-->X) /\ (N e. ZZ /\ P e. (ZZ>=` (N + 1)) /\ (N...P) C_ S)) /\ k e. (1...(P - N))) -> k e. (1...(P - N)))
195	54	a1i 8	. . . . . . . . . . . . . 14 |- (((N e. ZZ /\ P e. (ZZ>=` (N + 1)) /\ (N...P) C_ S) /\ k e. (1...(P - N))) -> 1 e. ZZ)
196	59	adantr 425	. . . . . . . . . . . . . 14 |- (((N e. ZZ /\ P e. (ZZ>=` (N + 1)) /\ (N...P) C_ S) /\ k e. (1...(P - N))) -> (P - N) e. ZZ)
197		elfzelz 7652	. . . . . . . . . . . . . . 15 |- (k e. (1...(P - N)) -> k e. ZZ)
198	197	adantl 424	. . . . . . . . . . . . . 14 |- (((N e. ZZ /\ P e. (ZZ>=` (N + 1)) /\ (N...P) C_ S) /\ k e. (1...(P - N))) -> k e. ZZ)
199		simpl1 879	. . . . . . . . . . . . . 14 |- (((N e. ZZ /\ P e. (ZZ>=` (N + 1)) /\ (N...P) C_ S) /\ k e. (1...(P - N))) -> N e. ZZ)
200		fzaddel 7672	. . . . . . . . . . . . . 14 |- (((1 e. ZZ /\ (P - N) e. ZZ) /\ (k e. ZZ /\ N e. ZZ)) -> (k e. (1...(P - N)) <-> (k + N) e. ((1 + N)...((P - N) + N))))
201	195, 196, 198, 199, 200	syl22anc 1101	. . . . . . . . . . . . 13 |- (((N e. ZZ /\ P e. (ZZ>=` (N + 1)) /\ (N...P) C_ S) /\ k e. (1...(P - N))) -> (k e. (1...(P - N)) <-> (k + N) e. ((1 + N)...((P - N) + N))))
202	20	a1i 8	. . . . . . . . . . . . . . . . . 18 |- ((P e. CC /\ N e. CC) -> 1 e. CC)
203		addcom 6458	. . . . . . . . . . . . . . . . . 18 |- ((1 e. CC /\ N e. CC) -> (1 + N) = (N + 1))
204	202, 203	sylancom 531	. . . . . . . . . . . . . . . . 17 |- ((P e. CC /\ N e. CC) -> (1 + N) = (N + 1))
205		npcan 6559	. . . . . . . . . . . . . . . . 17 |- ((P e. CC /\ N e. CC) -> ((P - N) + N) = P)
206	204, 205	opreq12d 4900	. . . . . . . . . . . . . . . 16 |- ((P e. CC /\ N e. CC) -> ((1 + N)...((P - N) + N)) = ((N + 1)...P))
207	77, 75, 206	syl11anc 524	. . . . . . . . . . . . . . 15 |- ((N e. ZZ /\ P e. (ZZ>=` (N + 1)) /\ (N...P) C_ S) -> ((1 + N)...((P - N) + N)) = ((N + 1)...P))
208	207	adantr 425	. . . . . . . . . . . . . 14 |- (((N e. ZZ /\ P e. (ZZ>=` (N + 1)) /\ (N...P) C_ S) /\ k e. (1...(P - N))) -> ((1 + N)...((P - N) + N)) = ((N + 1)...P))
209	208	eleq2d 1964	. . . . . . . . . . . . 13 |- (((N e. ZZ /\ P e. (ZZ>=` (N + 1)) /\ (N...P) C_ S) /\ k e. (1...(P - N))) -> ((k + N) e. ((1 + N)...((P - N) + N)) <-> (k + N) e. ((N + 1)...P)))
210	201, 209	bitrd 587	. . . . . . . . . . . 12 |- (((N e. ZZ /\ P e. (ZZ>=` (N + 1)) /\ (N...P) C_ S) /\ k e. (1...(P - N))) -> (k e. (1...(P - N)) <-> (k + N) e. ((N + 1)...P)))
211	210	adantll 428	. . . . . . . . . . 11 |- ((((M e. Met /\ F:S-->X) /\ (N e. ZZ /\ P e. (ZZ>=` (N + 1)) /\ (N...P) C_ S)) /\ k e. (1...(P - N))) -> (k e. (1...(P - N)) <-> (k + N) e. ((N + 1)...P)))
212		fzp1ss 7680	. . . . . . . . . . . . . 14 |- ((N e. ZZ /\ P e. ZZ) -> ((N + 1)...P) C_ (N...P))
213	57, 56, 212	syl11anc 524	. . . . . . . . . . . . 13 |- ((N e. ZZ /\ P e. (ZZ>=` (N + 1)) /\ (N...P) C_ S) -> ((N + 1)...P) C_ (N...P))
214	213	ad2antlr 441	. . . . . . . . . . . 12 |- ((((M e. Met /\ F:S-->X) /\ (N e. ZZ /\ P e. (ZZ>=` (N + 1)) /\ (N...P) C_ S)) /\ k e. (1...(P - N))) -> ((N + 1)...P) C_ (N...P))
215	214	sseld 2619	. . . . . . . . . . 11 |- ((((M e. Met /\ F:S-->X) /\ (N e. ZZ /\ P e. (ZZ>=` (N + 1)) /\ (N...P) C_ S)) /\ k e. (1...(P - N))) -> ((k + N) e. ((N + 1)...P) -> (k + N) e. (N...P)))
216	211, 215	sylbid 220	. . . . . . . . . 10 |- ((((M e. Met /\ F:S-->X) /\ (N e. ZZ /\ P e. (ZZ>=` (N + 1)) /\ (N...P) C_ S)) /\ k e. (1...(P - N))) -> (k e. (1...(P - N)) -> (k + N) e. (N...P)))
217		ffvelrn 4787	. . . . . . . . . . . . . . . 16 |- ((F:S-->X /\ (k + N) e. S) -> (F` (k + N)) e. X)
218	217	ex 402	. . . . . . . . . . . . . . 15 |- (F:S-->X -> ((k + N) e. S -> (F` (k + N)) e. X))
219		ssel2 2616	. . . . . . . . . . . . . . 15 |- (((N...P) C_ S /\ (k + N) e. (N...P)) -> (k + N) e. S)
220	218, 219	syl5 20	. . . . . . . . . . . . . 14 |- (F:S-->X -> (((N...P) C_ S /\ (k + N) e. (N...P)) -> (F` (k + N)) e. X))
221	220	expdimp 406	. . . . . . . . . . . . 13 |- ((F:S-->X /\ (N...P) C_ S) -> ((k + N) e. (N...P) -> (F` (k + N)) e. X))
222	221	3ad2antr3 1043	. . . . . . . . . . . 12 |- ((F:S-->X /\ (N e. ZZ /\ P e. (ZZ>=` (N + 1)) /\ (N...P) C_ S)) -> ((k + N) e. (N...P) -> (F` (k + N)) e. X))
223	222	adantr 425	. . . . . . . . . . 11 |- (((F:S-->X /\ (N e. ZZ /\ P e. (ZZ>=` (N + 1)) /\ (N...P) C_ S)) /\ k e. (1...(P - N))) -> ((k + N) e. (N...P) -> (F` (k + N)) e. X))
224	223	adantlll 432	. . . . . . . . . 10 |- ((((M e. Met /\ F:S-->X) /\ (N e. ZZ /\ P e. (ZZ>=` (N + 1)) /\ (N...P) C_ S)) /\ k e. (1...(P - N))) -> ((k + N) e. (N...P) -> (F` (k + N)) e. X))
225	216, 224	syld 30	. . . . . . . . 9 |- ((((M e. Met /\ F:S-->X) /\ (N e. ZZ /\ P e. (ZZ>=` (N + 1)) /\ (N...P) C_ S)) /\ k e. (1...(P - N))) -> (k e. (1...(P - N)) -> (F` (k + N)) e. X))
226	194, 225	mpd 29	. . . . . . . 8 |- ((((M e. Met /\ F:S-->X) /\ (N e. ZZ /\ P e. (ZZ>=` (N + 1)) /\ (N...P) C_ S)) /\ k e. (1...(P - N))) -> (F` (k + N)) e. X)
227	193, 226	eqeltrd 1971	. . . . . . 7 |- ((((M e. Met /\ F:S-->X) /\ (N e. ZZ /\ P e. (ZZ>=` (N + 1)) /\ (N...P) C_ S)) /\ k e. (1...(P - N))) -> ((F shift -u(N - 1))` (k + 1)) e. X)
228	118	metcl 9088	. . . . . . 7 |- ((M e. Met /\ ((F shift -u(N - 1))` k) e. X /\ ((F shift -u(N - 1))` (k + 1)) e. X) -> (((F shift -u(N - 1))` k)M((F shift -u(N - 1))` (k + 1))) e. RR)
229	157, 160, 227, 228	syl111anc 1100	. . . . . 6 |- ((((M e. Met /\ F:S-->X) /\ (N e. ZZ /\ P e. (ZZ>=` (N + 1)) /\ (N...P) C_ S)) /\ k e. (1...(P - N))) -> (((F shift -u(N - 1))` k)M((F shift -u(N - 1))` (k + 1))) e. RR)
230	229	recnd 6468	. . . . 5 |- ((((M e. Met /\ F:S-->X) /\ (N e. ZZ /\ P e. (ZZ>=` (N + 1)) /\ (N...P) C_ S)) /\ k e. (1...(P - N))) -> (((F shift -u(N - 1))` k)M((F shift -u(N - 1))` (k + 1))) e. CC)
231	230	r19.21aiva 2176	. . . 4 |- (((M e. Met /\ F:S-->X) /\ (N e. ZZ /\ P e. (ZZ>=` (N + 1)) /\ (N...P) C_ S)) -> A.k e. (1...(P - N))(((F shift -u(N - 1))` k)M((F shift -u(N - 1))` (k + 1))) e. CC)
232		fsumshft 8291	. . . 4 |- (((P - N) e. (ZZ>=` 1) /\ (N - 1) e. ZZ /\ A.k e. (1...(P - N))(((F shift -u(N - 1))` k)M((F shift -u(N - 1))` (k + 1))) e. CC) -> sum_k e. (1...(P - N))(((F shift -u(N - 1))` k)M((F shift -u(N - 1))` (k + 1))) = sum_j e. ((1 + (N - 1))...((P - N) + (N - 1)))[_(j - (N - 1)) / k]_(((F shift -u(N - 1))` k)M((F shift -u(N - 1))` (k + 1))))
233	155, 156, 231, 232	syl111anc 1100	. . 3 |- (((M e. Met /\ F:S-->X) /\ (N e. ZZ /\ P e. (ZZ>=` (N + 1)) /\ (N...P) C_ S)) -> sum_k e. (1...(P - N))(((F shift -u(N - 1))` k)M((F shift -u(N - 1))` (k + 1))) = sum_j e. ((1 + (N - 1))...((P - N) + (N - 1)))[_(j - (N - 1)) / k]_(((F shift -u(N - 1))` k)M((F shift -u(N - 1))` (k + 1))))
234	20, 74	mpan 759	. . . . . . . . . . 11 |- (N e. CC -> (1 + (N - 1)) = N)
235	234	adantr 425	. . . . . . . . . 10 |- ((N e. CC /\ P e. CC) -> (1 + (N - 1)) = N)
236		npncan 6560	. . . . . . . . . . . 12 |- ((P e. CC /\ N e. CC /\ 1 e. CC) -> ((P - N) + (N - 1)) = (P - 1))
237	20, 236	mp3an3 1180	. . . . . . . . . . 11 |- ((P e. CC /\ N e. CC) -> ((P - N) + (N - 1)) = (P - 1))
238	237	ancoms 484	. . . . . . . . . 10 |- ((N e. CC /\ P e. CC) -> ((P - N) + (N - 1)) = (P - 1))
239	235, 238	opreq12d 4900	. . . . . . . . 9 |- ((N e. CC /\ P e. CC) -> ((1 + (N - 1))...((P - N) + (N - 1))) = (N...(P - 1)))
240	239, 10, 8	syl2an 503	. . . . . . . 8 |- ((N e. ZZ /\ P e. (ZZ>=` (N + 1))) -> ((1 + (N - 1))...((P - N) + (N - 1))) = (N...(P - 1)))
241	240	adantl 424	. . . . . . 7 |- ((F:S-->X /\ (N e. ZZ /\ P e. (ZZ>=` (N + 1)))) -> ((1 + (N - 1))...((P - N) + (N - 1))) = (N...(P - 1)))
242	34	fveq1d 4683	. . . . . . . . . . . . . . 15 |- (f = F -> ((f shift -u(N - 1))` (j - (N - 1))) = ((F shift -u(N - 1))` (j - (N - 1))))
243	34	fveq1d 4683	. . . . . . . . . . . . . . 15 |- (f = F -> ((f shift -u(N - 1))` ((j - (N - 1)) + 1)) = ((F shift -u(N - 1))` ((j - (N - 1)) + 1)))
244	242, 243	opreq12d 4900	. . . . . . . . . . . . . 14 |- (f = F -> (((f shift -u(N - 1))` (j - (N - 1)))M((f shift -u(N - 1))` ((j - (N - 1)) + 1))) = (((F shift -u(N - 1))` (j - (N - 1)))M((F shift -u(N - 1))` ((j - (N - 1)) + 1))))
245		fveq1 4680	. . . . . . . . . . . . . . 15 |- (f = F -> (f` j) = (F` j))
246		fveq1 4680	. . . . . . . . . . . . . . 15 |- (f = F -> (f` (j + 1)) = (F` (j + 1)))
247	245, 246	opreq12d 4900	. . . . . . . . . . . . . 14 |- (f = F -> ((f` j)M(f` (j + 1))) = ((F` j)M(F` (j + 1))))
248	244, 247	eqeq12d 1899	. . . . . . . . . . . . 13 |- (f = F -> ((((f shift -u(N - 1))` (j - (N - 1)))M((f shift -u(N - 1))` ((j - (N - 1)) + 1))) = ((f` j)M(f` (j + 1))) <-> (((F shift -u(N - 1))` (j - (N - 1)))M((F shift -u(N - 1))` ((j - (N - 1)) + 1))) = ((F` j)M(F` (j + 1)))))
249	248	imbi2d 674	. . . . . . . . . . . 12 |- (f = F -> ((((N e. ZZ /\ P e. (ZZ>=` (N + 1))) /\ j e. ((1 + (N - 1))...((P - N) + (N - 1)))) -> (((f shift -u(N - 1))` (j - (N - 1)))M((f shift -u(N - 1))` ((j - (N - 1)) + 1))) = ((f` j)M(f` (j + 1)))) <-> (((N e. ZZ /\ P e. (ZZ>=` (N + 1))) /\ j e. ((1 + (N - 1))...((P - N) + (N - 1)))) -> (((F shift -u(N - 1))` (j - (N - 1)))M((F shift -u(N - 1))` ((j - (N - 1)) + 1))) = ((F` j)M(F` (j + 1))))))
250	130	3ad2ant1 897	. . . . . . . . . . . . . . . . 17 |- ((N e. CC /\ P e. CC /\ j e. CC) -> (N - 1) e. CC)
251		simp3 878	. . . . . . . . . . . . . . . . . 18 |- ((N e. CC /\ P e. CC /\ j e. CC) -> j e. CC)
252		subcl 6524	. . . . . . . . . . . . . . . . . 18 |- ((j e. CC /\ (N - 1) e. CC) -> (j - (N - 1)) e. CC)
253	251, 250, 252	syl11anc 524	. . . . . . . . . . . . . . . . 17 |- ((N e. CC /\ P e. CC /\ j e. CC) -> (j - (N - 1)) e. CC)
254	39	shftval4 7762	. . . . . . . . . . . . . . . . 17 |- (((N - 1) e. CC /\ (j - (N - 1)) e. CC) -> ((f shift -u(N - 1))` (j - (N - 1))) = (f` ((N - 1) + (j - (N - 1)))))
255	250, 253, 254	syl11anc 524	. . . . . . . . . . . . . . . 16 |- ((N e. CC /\ P e. CC /\ j e. CC) -> ((f shift -u(N - 1))` (j - (N - 1))) = (f` ((N - 1) + (j - (N - 1)))))
256		pncan3 6534	. . . . . . . . . . . . . . . . . 18 |- (((N - 1) e. CC /\ j e. CC) -> ((N - 1) + (j - (N - 1))) = j)
257	250, 251, 256	syl11anc 524	. . . . . . . . . . . . . . . . 17 |- ((N e. CC /\ P e. CC /\ j e. CC) -> ((N - 1) + (j - (N - 1))) = j)
258	257	fveq2d 4685	. . . . . . . . . . . . . . . 16 |- ((N e. CC /\ P e. CC /\ j e. CC) -> (f` ((N - 1) + (j - (N - 1)))) = (f` j))
259	255, 258	eqtrd 1925	. . . . . . . . . . . . . . 15 |- ((N e. CC /\ P e. CC /\ j e. CC) -> ((f shift -u(N - 1))` (j - (N - 1))) = (f` j))
260		peano2cn 6498	. . . . . . . . . . . . . . . . . 18 |- ((j - (N - 1)) e. CC -> ((j - (N - 1)) + 1) e. CC)
261	253, 260	syl 12	. . . . . . . . . . . . . . . . 17 |- ((N e. CC /\ P e. CC /\ j e. CC) -> ((j - (N - 1)) + 1) e. CC)
262	39	shftval4 7762	. . . . . . . . . . . . . . . . 17 |- (((N - 1) e. CC /\ ((j - (N - 1)) + 1) e. CC) -> ((f shift -u(N - 1))` ((j - (N - 1)) + 1)) = (f` ((N - 1) + ((j - (N - 1)) + 1))))
263	250, 261, 262	syl11anc 524	. . . . . . . . . . . . . . . 16 |- ((N e. CC /\ P e. CC /\ j e. CC) -> ((f shift -u(N - 1))` ((j - (N - 1)) + 1)) = (f` ((N - 1) + ((j - (N - 1)) + 1))))
264	20	a1i 8	. . . . . . . . . . . . . . . . . . 19 |- ((N e. CC /\ P e. CC /\ j e. CC) -> 1 e. CC)
265		addass 6460	. . . . . . . . . . . . . . . . . . 19 |- (((N - 1) e. CC /\ (j - (N - 1)) e. CC /\ 1 e. CC) -> (((N - 1) + (j - (N - 1))) + 1) = ((N - 1) + ((j - (N - 1)) + 1)))
266	250, 253, 264, 265	syl111anc 1100	. . . . . . . . . . . . . . . . . 18 |- ((N e. CC /\ P e. CC /\ j e. CC) -> (((N - 1) + (j - (N - 1))) + 1) = ((N - 1) + ((j - (N - 1)) + 1)))
267	257	opreq1d 4897	. . . . . . . . . . . . . . . . . 18 |- ((N e. CC /\ P e. CC /\ j e. CC) -> (((N - 1) + (j - (N - 1))) + 1) = (j + 1))
268	266, 267	eqtr3d 1927	. . . . . . . . . . . . . . . . 17 |- ((N e. CC /\ P e. CC /\ j e. CC) -> ((N - 1) + ((j - (N - 1)) + 1)) = (j + 1))
269	268	fveq2d 4685	. . . . . . . . . . . . . . . 16 |- ((N e. CC /\ P e. CC /\ j e. CC) -> (f` ((N - 1) + ((j - (N - 1)) + 1))) = (f` (j + 1)))
270	263, 269	eqtrd 1925	. . . . . . . . . . . . . . 15 |- ((N e. CC /\ P e. CC /\ j e. CC) -> ((f shift -u(N - 1))` ((j - (N - 1)) + 1)) = (f` (j + 1)))
271	259, 270	opreq12d 4900	. . . . . . . . . . . . . 14 |- ((N e. CC /\ P e. CC /\ j e. CC) -> (((f shift -u(N - 1))` (j - (N - 1)))M((f shift -u(N - 1))` ((j - (N - 1)) + 1))) = ((f` j)M(f` (j + 1))))
272		elfzuz 7658	. . . . . . . . . . . . . . 15 |- (j e. ((1 + (N - 1))...((P - N) + (N - 1))) -> j e. (ZZ>=` (1 + (N - 1))))
273		eluzelz 7592	. . . . . . . . . . . . . . 15 |- (j e. (ZZ>=` (1 + (N - 1))) -> j e. ZZ)
274		zcn 7349	. . . . . . . . . . . . . . 15 |- (j e. ZZ -> j e. CC)
275	272, 273, 274	3syl 24	. . . . . . . . . . . . . 14 |- (j e. ((1 + (N - 1))...((P - N) + (N - 1))) -> j e. CC)
276	271, 10, 8, 275	syl3an 1139	. . . . . . . . . . . . 13 |- ((N e. ZZ /\ P e. (ZZ>=` (N + 1)) /\ j e. ((1 + (N - 1))...((P - N) + (N - 1)))) -> (((f shift -u(N - 1))` (j - (N - 1)))M((f shift -u(N - 1))` ((j - (N - 1)) + 1))) = ((f` j)M(f` (j + 1))))
277	276	3expa 1067	. . . . . . . . . . . 12 |- (((N e. ZZ /\ P e. (ZZ>=` (N + 1))) /\ j e. ((1 + (N - 1))...((P - N) + (N - 1)))) -> (((f shift -u(N - 1))` (j - (N - 1)))M((f shift -u(N - 1))` ((j - (N - 1)) + 1))) = ((f` j)M(f` (j + 1))))
278	249, 277	vtoclg 2346	. . . . . . . . . . 11 |- (F e. _V -> (((N e. ZZ /\ P e. (ZZ>=` (N + 1))) /\ j e. ((1 + (N - 1))...((P - N) + (N - 1)))) -> (((F shift -u(N - 1))` (j - (N - 1)))M((F shift -u(N - 1))` ((j - (N - 1)) + 1))) = ((F` j)M(F` (j + 1)))))
279	33, 278	syl 12	. . . . . . . . . 10 |- (F:S-->X -> (((N e. ZZ /\ P e. (ZZ>=` (N + 1))) /\ j e. ((1 + (N - 1))...((P - N) + (N - 1)))) -> (((F shift -u(N - 1))` (j - (N - 1)))M((F shift -u(N - 1))` ((j - (N - 1)) + 1))) = ((F` j)M(F` (j + 1)))))
280	279	imp 377	. . . . . . . . 9 |- ((F:S-->X /\ ((N e. ZZ /\ P e. (ZZ>=` (N + 1))) /\ j e. ((1 + (N - 1))...((P - N) + (N - 1))))) -> (((F shift -u(N - 1))` (j - (N - 1)))M((F shift -u(N - 1))` ((j - (N - 1)) + 1))) = ((F` j)M(F` (j + 1))))
281	280	anassrs 489	. . . . . . . 8 |- (((F:S-->X /\ (N e. ZZ /\ P e. (ZZ>=` (N + 1)))) /\ j e. ((1 + (N - 1))...((P - N) + (N - 1)))) -> (((F shift -u(N - 1))` (j - (N - 1)))M((F shift -u(N - 1))` ((j - (N - 1)) + 1))) = ((F` j)M(F` (j + 1))))
282		oprex 4907	. . . . . . . . 9 |- (j - (N - 1)) e. _V
283		ax-17 1317	. . . . . . . . 9 |- (z e. (((F shift -u(N - 1))` (j - (N - 1)))M((F shift -u(N - 1))` ((j - (N - 1)) + 1))) -> A.k z e. (((F shift -u(N - 1))` (j - (N - 1)))M((F shift -u(N - 1))` ((j - (N - 1)) + 1))))
284		fveq2 4681	. . . . . . . . . 10 |- (k = (j - (N - 1)) -> ((F shift -u(N - 1))` k) = ((F shift -u(N - 1))` (j - (N - 1))))
285		opreq1 4889	. . . . . . . . . . 11 |- (k = (j - (N - 1)) -> (k + 1) = ((j - (N - 1)) + 1))
286	285	fveq2d 4685	. . . . . . . . . 10 |- (k = (j - (N - 1)) -> ((F shift -u(N - 1))` (k + 1)) = ((F shift -u(N - 1))` ((j - (N - 1)) + 1)))
287	284, 286	opreq12d 4900	. . . . . . . . 9 |- (k = (j - (N - 1)) -> (((F shift -u(N - 1))` k)M((F shift -u(N - 1))` (k + 1))) = (((F shift -u(N - 1))` (j - (N - 1)))M((F shift -u(N - 1))` ((j - (N - 1)) + 1))))
288	282, 283, 287	csbief 2576	. . . . . . . 8 |- [_(j - (N - 1)) / k]_(((F shift -u(N - 1))` k)M((F shift -u(N - 1))` (k + 1))) = (((F shift -u(N - 1))` (j - (N - 1)))M((F shift -u(N - 1))` ((j - (N - 1)) + 1)))
289	281, 288	syl5eq 1940	. . . . . . 7 |- (((F:S-->X /\ (N e. ZZ /\ P e. (ZZ>=` (N + 1)))) /\ j e. ((1 + (N - 1))...((P - N) + (N - 1)))) -> [_(j - (N - 1)) / k]_(((F shift -u(N - 1))` k)M((F shift -u(N - 1))` (k + 1))) = ((F` j)M(F` (j + 1))))
290	241, 289	sumeq12dv 8255	. . . . . 6 |- ((F:S-->X /\ (N e. ZZ /\ P e. (ZZ>=` (N + 1)))) -> sum_j e. ((1 + (N - 1))...((P - N) + (N - 1)))[_(j - (N - 1)) / k]_(((F shift -u(N - 1))` k)M((F shift -u(N - 1))` (k + 1))) = sum_j e. (N...(P - 1))((F` j)M(F` (j + 1))))
291	290	3adantr3 1037	. . . . 5 |- ((F:S-->X /\ (N e. ZZ /\ P e. (ZZ>=` (N + 1)) /\ (N...P) C_ S)) -> sum_j e. ((1 + (N - 1))...((P - N) + (N - 1)))[_(j - (N - 1)) / k]_(((F shift -u(N - 1))` k)M((F shift -u(N - 1))` (k + 1))) = sum_j e. (N...(P - 1))((F` j)M(F` (j + 1))))
292	291	adantll 428	. . . 4 |- (((M e. Met /\ F:S-->X) /\ (N e. ZZ /\ P e. (ZZ>=` (N + 1)) /\ (N...P) C_ S)) -> sum_j e. ((1 + (N - 1))...((P - N) + (N - 1)))[_(j - (N - 1)) / k]_(((F shift -u(N - 1))` k)M((F shift -u(N - 1))` (k + 1))) = sum_j e. (N...(P - 1))((F` j)M(F` (j + 1))))
293		ax-17 1317	. . . . 5 |- (z e. ((F` j)M(F` (j + 1))) -> A.k z e. ((F` j)M(F` (j + 1))))
294		ax-17 1317	. . . . 5 |- (z e. ((F` k)M(F` (k + 1))) -> A.j z e. ((F` k)M(F` (k + 1))))
295		fveq2 4681	. . . . . 6 |- (j = k -> (F` j) = (F` k))
296	110	fveq2d 4685	. . . . . 6 |- (j = k -> (F` (j + 1)) = (F` (k + 1)))
297	295, 296	opreq12d 4900	. . . . 5 |- (j = k -> ((F` j)M(F` (j + 1))) = ((F` k)M(F` (k + 1))))
298	293, 294, 297	cbvsumi 8246	. . . 4 |- sum_j e. (N...(P - 1))((F` j)M(F` (j + 1))) = sum_k e. (N...(P - 1))((F` k)M(F` (k + 1)))
299	292, 298	syl6eq 1944	. . 3 |- (((M e. Met /\ F:S-->X) /\ (N e. ZZ /\ P e. (ZZ>=` (N + 1)) /\ (N...P) C_ S)) -> sum_j e. ((1 + (N - 1))...((P - N) + (N - 1)))[_(j - (N - 1)) / k]_(((F shift -u(N - 1))` k)M((F shift -u(N - 1))` (k + 1))) = sum_k e. (N...(P - 1))((F` k)M(F` (k + 1))))
300	152, 233, 299	3eqtrd 1929	. 2 |- (((M e. Met /\ F:S-->X) /\ (N e. ZZ /\ P e. (ZZ>=` (N + 1)) /\ (N...P) C_ S)) -> sum_k e. (1...(P - N))({<.j, z>. | (j e. (1...(P - N)) /\ z = (((F shift -u(N - 1))` j)M((F shift -u(N - 1))` (j + 1))))}` k) = sum_k e. (N...(P - 1))((F` k)M(F` (k + 1))))
301	120, 150, 300	3brtr3d 3366	1 |- (((M e. Met /\ F:S-->X) /\ (N e. ZZ /\ P e. (ZZ>=` (N + 1)) /\ (N...P) C_ S)) -> ((F` N)M(F` P)) <_ sum_k e. (N...(P - 1))((F` k)M(F` (k + 1))))

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240   /\ w3a 858   = wceq 1298   e. wcel 1300  A.wral 2105  _Vcvv 2292  [_csb 2540   C_ wss 2593   class class class wbr 3338  {copab 3395  dom cdm 3986  -->wf 3994  ` cfv 3998  (class class class)co 4884  CCcc 6384  RRcr 6385  1c1 6387   + caddc 6389   - cmin 6445  -ucneg 6446   <_ cle 6448  NNcn 6449  ZZcz 6451  ZZ>=cuz 7586  ...cfz 7637   shift cshi 7753  sum_csu 8239  Metcme 9066

This theorem is referenced by:  geomcau 15849

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-n 7108  df-2 7154  df-n0 7309  df-z 7345  df-uz 7587  df-fz 7638  df-seq1 7721  df-shft 7754  df-seqz 7776  df-sum 8240  df-met 9070

Copyright terms: Public domain