Theorem mettrifi 11912

Description: Generalized triangle inequality for arbitrary finite sums.

Hypothesis

Ref	Expression
mettrifi.1	|- X = dom dom M

Assertion

Ref	Expression
mettrifi	|- (((M e. Met /\ N e. NN) /\ (A.k e. (1...(N + 1))(F` k) e. X /\ A.k e. (1...N)(G` k) = ((F` k)M(F` (k + 1))))) -> ((F` 1)M(F` (N + 1))) <_ sum_k e. (1...N)(G` k))

Distinct variable groups:   k,M   k,N   k,F   k,G   k,X

Proof of Theorem mettrifi

Step	Hyp	Ref	Expression
1		opreq1 4026	. . . . . . . . . 10 |- (j = 1 -> (j + 1) = (1 + 1))
2	1	opreq2d 4034	. . . . . . . . 9 |- (j = 1 -> (1...(j + 1)) = (1...(1 + 1)))
3	2	raleq1d 1835	. . . . . . . 8 |- (j = 1 -> (A.k e. (1...(j + 1))(F` k) e. X <-> A.k e. (1...(1 + 1))(F` k) e. X))
4		opreq2 4027	. . . . . . . . 9 |- (j = 1 -> (1...j) = (1...1))
5	4	raleq1d 1835	. . . . . . . 8 |- (j = 1 -> (A.k e. (1...j)(G` k) = ((F` k)M(F` (k + 1))) <-> A.k e. (1...1)(G` k) = ((F` k)M(F` (k + 1)))))
6	3, 5	anbi12d 631	. . . . . . 7 |- (j = 1 -> ((A.k e. (1...(j + 1))(F` k) e. X /\ A.k e. (1...j)(G` k) = ((F` k)M(F` (k + 1)))) <-> (A.k e. (1...(1 + 1))(F` k) e. X /\ A.k e. (1...1)(G` k) = ((F` k)M(F` (k + 1))))))
7	6	anbi2d 619	. . . . . 6 |- (j = 1 -> ((M e. Met /\ (A.k e. (1...(j + 1))(F` k) e. X /\ A.k e. (1...j)(G` k) = ((F` k)M(F` (k + 1))))) <-> (M e. Met /\ (A.k e. (1...(1 + 1))(F` k) e. X /\ A.k e. (1...1)(G` k) = ((F` k)M(F` (k + 1)))))))
8	1	fveq2d 3839	. . . . . . . 8 |- (j = 1 -> (F` (j + 1)) = (F` (1 + 1)))
9	8	opreq2d 4034	. . . . . . 7 |- (j = 1 -> ((F` 1)M(F` (j + 1))) = ((F` 1)M(F` (1 + 1))))
10	4	sumeq1d 7193	. . . . . . 7 |- (j = 1 -> sum_k e. (1...j)(G` k) = sum_k e. (1...1)(G` k))
11	9, 10	breq12d 2704	. . . . . 6 |- (j = 1 -> (((F` 1)M(F` (j + 1))) <_ sum_k e. (1...j)(G` k) <-> ((F` 1)M(F` (1 + 1))) <_ sum_k e. (1...1)(G` k)))
12	7, 11	imbi12d 629	. . . . 5 |- (j = 1 -> (((M e. Met /\ (A.k e. (1...(j + 1))(F` k) e. X /\ A.k e. (1...j)(G` k) = ((F` k)M(F` (k + 1))))) -> ((F` 1)M(F` (j + 1))) <_ sum_k e. (1...j)(G` k)) <-> ((M e. Met /\ (A.k e. (1...(1 + 1))(F` k) e. X /\ A.k e. (1...1)(G` k) = ((F` k)M(F` (k + 1))))) -> ((F` 1)M(F` (1 + 1))) <_ sum_k e. (1...1)(G` k))))
13		opreq1 4026	. . . . . . . . . 10 |- (j = m -> (j + 1) = (m + 1))
14	13	opreq2d 4034	. . . . . . . . 9 |- (j = m -> (1...(j + 1)) = (1...(m + 1)))
15	14	raleq1d 1835	. . . . . . . 8 |- (j = m -> (A.k e. (1...(j + 1))(F` k) e. X <-> A.k e. (1...(m + 1))(F` k) e. X))
16		opreq2 4027	. . . . . . . . 9 |- (j = m -> (1...j) = (1...m))
17	16	raleq1d 1835	. . . . . . . 8 |- (j = m -> (A.k e. (1...j)(G` k) = ((F` k)M(F` (k + 1))) <-> A.k e. (1...m)(G` k) = ((F` k)M(F` (k + 1)))))
18	15, 17	anbi12d 631	. . . . . . 7 |- (j = m -> ((A.k e. (1...(j + 1))(F` k) e. X /\ A.k e. (1...j)(G` k) = ((F` k)M(F` (k + 1)))) <-> (A.k e. (1...(m + 1))(F` k) e. X /\ A.k e. (1...m)(G` k) = ((F` k)M(F` (k + 1))))))
19	18	anbi2d 619	. . . . . 6 |- (j = m -> ((M e. Met /\ (A.k e. (1...(j + 1))(F` k) e. X /\ A.k e. (1...j)(G` k) = ((F` k)M(F` (k + 1))))) <-> (M e. Met /\ (A.k e. (1...(m + 1))(F` k) e. X /\ A.k e. (1...m)(G` k) = ((F` k)M(F` (k + 1)))))))
20	13	fveq2d 3839	. . . . . . . 8 |- (j = m -> (F` (j + 1)) = (F` (m + 1)))
21	20	opreq2d 4034	. . . . . . 7 |- (j = m -> ((F` 1)M(F` (j + 1))) = ((F` 1)M(F` (m + 1))))
22	16	sumeq1d 7193	. . . . . . 7 |- (j = m -> sum_k e. (1...j)(G` k) = sum_k e. (1...m)(G` k))
23	21, 22	breq12d 2704	. . . . . 6 |- (j = m -> (((F` 1)M(F` (j + 1))) <_ sum_k e. (1...j)(G` k) <-> ((F` 1)M(F` (m + 1))) <_ sum_k e. (1...m)(G` k)))
24	19, 23	imbi12d 629	. . . . 5 |- (j = m -> (((M e. Met /\ (A.k e. (1...(j + 1))(F` k) e. X /\ A.k e. (1...j)(G` k) = ((F` k)M(F` (k + 1))))) -> ((F` 1)M(F` (j + 1))) <_ sum_k e. (1...j)(G` k)) <-> ((M e. Met /\ (A.k e. (1...(m + 1))(F` k) e. X /\ A.k e. (1...m)(G` k) = ((F` k)M(F` (k + 1))))) -> ((F` 1)M(F` (m + 1))) <_ sum_k e. (1...m)(G` k))))
25		opreq1 4026	. . . . . . . . . 10 |- (j = (m + 1) -> (j + 1) = ((m + 1) + 1))
26	25	opreq2d 4034	. . . . . . . . 9 |- (j = (m + 1) -> (1...(j + 1)) = (1...((m + 1) + 1)))
27	26	raleq1d 1835	. . . . . . . 8 |- (j = (m + 1) -> (A.k e. (1...(j + 1))(F` k) e. X <-> A.k e. (1...((m + 1) + 1))(F` k) e. X))
28		opreq2 4027	. . . . . . . . 9 |- (j = (m + 1) -> (1...j) = (1...(m + 1)))
29	28	raleq1d 1835	. . . . . . . 8 |- (j = (m + 1) -> (A.k e. (1...j)(G` k) = ((F` k)M(F` (k + 1))) <-> A.k e. (1...(m + 1))(G` k) = ((F` k)M(F` (k + 1)))))
30	27, 29	anbi12d 631	. . . . . . 7 |- (j = (m + 1) -> ((A.k e. (1...(j + 1))(F` k) e. X /\ A.k e. (1...j)(G` k) = ((F` k)M(F` (k + 1)))) <-> (A.k e. (1...((m + 1) + 1))(F` k) e. X /\ A.k e. (1...(m + 1))(G` k) = ((F` k)M(F` (k + 1))))))
31	30	anbi2d 619	. . . . . 6 |- (j = (m + 1) -> ((M e. Met /\ (A.k e. (1...(j + 1))(F` k) e. X /\ A.k e. (1...j)(G` k) = ((F` k)M(F` (k + 1))))) <-> (M e. Met /\ (A.k e. (1...((m + 1) + 1))(F` k) e. X /\ A.k e. (1...(m + 1))(G` k) = ((F` k)M(F` (k + 1)))))))
32	25	fveq2d 3839	. . . . . . . 8 |- (j = (m + 1) -> (F` (j + 1)) = (F` ((m + 1) + 1)))
33	32	opreq2d 4034	. . . . . . 7 |- (j = (m + 1) -> ((F` 1)M(F` (j + 1))) = ((F` 1)M(F` ((m + 1) + 1))))
34	28	sumeq1d 7193	. . . . . . 7 |- (j = (m + 1) -> sum_k e. (1...j)(G` k) = sum_k e. (1...(m + 1))(G` k))
35	33, 34	breq12d 2704	. . . . . 6 |- (j = (m + 1) -> (((F` 1)M(F` (j + 1))) <_ sum_k e. (1...j)(G` k) <-> ((F` 1)M(F` ((m + 1) + 1))) <_ sum_k e. (1...(m + 1))(G` k)))
36	31, 35	imbi12d 629	. . . . 5 |- (j = (m + 1) -> (((M e. Met /\ (A.k e. (1...(j + 1))(F` k) e. X /\ A.k e. (1...j)(G` k) = ((F` k)M(F` (k + 1))))) -> ((F` 1)M(F` (j + 1))) <_ sum_k e. (1...j)(G` k)) <-> ((M e. Met /\ (A.k e. (1...((m + 1) + 1))(F` k) e. X /\ A.k e. (1...(m + 1))(G` k) = ((F` k)M(F` (k + 1))))) -> ((F` 1)M(F` ((m + 1) + 1))) <_ sum_k e. (1...(m + 1))(G` k))))
37		opreq1 4026	. . . . . . . . . 10 |- (j = N -> (j + 1) = (N + 1))
38	37	opreq2d 4034	. . . . . . . . 9 |- (j = N -> (1...(j + 1)) = (1...(N + 1)))
39	38	raleq1d 1835	. . . . . . . 8 |- (j = N -> (A.k e. (1...(j + 1))(F` k) e. X <-> A.k e. (1...(N + 1))(F` k) e. X))
40		opreq2 4027	. . . . . . . . 9 |- (j = N -> (1...j) = (1...N))
41	40	raleq1d 1835	. . . . . . . 8 |- (j = N -> (A.k e. (1...j)(G` k) = ((F` k)M(F` (k + 1))) <-> A.k e. (1...N)(G` k) = ((F` k)M(F` (k + 1)))))
42	39, 41	anbi12d 631	. . . . . . 7 |- (j = N -> ((A.k e. (1...(j + 1))(F` k) e. X /\ A.k e. (1...j)(G` k) = ((F` k)M(F` (k + 1)))) <-> (A.k e. (1...(N + 1))(F` k) e. X /\ A.k e. (1...N)(G` k) = ((F` k)M(F` (k + 1))))))
43	42	anbi2d 619	. . . . . 6 |- (j = N -> ((M e. Met /\ (A.k e. (1...(j + 1))(F` k) e. X /\ A.k e. (1...j)(G` k) = ((F` k)M(F` (k + 1))))) <-> (M e. Met /\ (A.k e. (1...(N + 1))(F` k) e. X /\ A.k e. (1...N)(G` k) = ((F` k)M(F` (k + 1)))))))
44	37	fveq2d 3839	. . . . . . . 8 |- (j = N -> (F` (j + 1)) = (F` (N + 1)))
45	44	opreq2d 4034	. . . . . . 7 |- (j = N -> ((F` 1)M(F` (j + 1))) = ((F` 1)M(F` (N + 1))))
46	40	sumeq1d 7193	. . . . . . 7 |- (j = N -> sum_k e. (1...j)(G` k) = sum_k e. (1...N)(G` k))
47	45, 46	breq12d 2704	. . . . . 6 |- (j = N -> (((F` 1)M(F` (j + 1))) <_ sum_k e. (1...j)(G` k) <-> ((F` 1)M(F` (N + 1))) <_ sum_k e. (1...N)(G` k)))
48	43, 47	imbi12d 629	. . . . 5 |- (j = N -> (((M e. Met /\ (A.k e. (1...(j + 1))(F` k) e. X /\ A.k e. (1...j)(G` k) = ((F` k)M(F` (k + 1))))) -> ((F` 1)M(F` (j + 1))) <_ sum_k e. (1...j)(G` k)) <-> ((M e. Met /\ (A.k e. (1...(N + 1))(F` k) e. X /\ A.k e. (1...N)(G` k) = ((F` k)M(F` (k + 1))))) -> ((F` 1)M(F` (N + 1))) <_ sum_k e. (1...N)(G` k))))
49		eqle 5725	. . . . . 6 |- ((((F` 1)M(F` (1 + 1))) e. RR /\ ((F` 1)M(F` (1 + 1))) = sum_k e. (1...1)(G` k)) -> ((F` 1)M(F` (1 + 1))) <_ sum_k e. (1...1)(G` k))
50		mettrifi.1	. . . . . . . . . 10 |- X = dom dom M
51	50	metcl 8021	. . . . . . . . 9 |- ((M e. Met /\ (F` 1) e. X /\ (F` (1 + 1)) e. X) -> ((F` 1)M(F` (1 + 1))) e. RR)
52	51	3expb 840	. . . . . . . 8 |- ((M e. Met /\ ((F` 1) e. X /\ (F` (1 + 1)) e. X)) -> ((F` 1)M(F` (1 + 1))) e. RR)
53		df-2 6116	. . . . . . . . . . . . . 14 |- 2 = (1 + 1)
54	53	eleq1i 1580	. . . . . . . . . . . . 13 |- (2 e. (ZZ>=` 1) <-> (1 + 1) e. (ZZ>=` 1))
55		1z 6327	. . . . . . . . . . . . . 14 |- 1 e. ZZ
56	55	eluz1i 6549	. . . . . . . . . . . . 13 |- (2 e. (ZZ>=` 1) <-> (2 e. ZZ /\ 1 <_ 2))
57	54, 56	bitr3i 173	. . . . . . . . . . . 12 |- ((1 + 1) e. (ZZ>=` 1) <-> (2 e. ZZ /\ 1 <_ 2))
58		2z 6328	. . . . . . . . . . . 12 |- 2 e. ZZ
59		1re 5589	. . . . . . . . . . . . 13 |- 1 e. RR
60		2re 6125	. . . . . . . . . . . . 13 |- 2 e. RR
61		1lt2 6174	. . . . . . . . . . . . 13 |- 1 < 2
62	59, 60, 61	ltleii 5735	. . . . . . . . . . . 12 |- 1 <_ 2
63	57, 58, 62	mpbir2an 735	. . . . . . . . . . 11 |- (1 + 1) e. (ZZ>=` 1)
64		eluzfz1 6615	. . . . . . . . . . 11 |- ((1 + 1) e. (ZZ>=` 1) -> 1 e. (1...(1 + 1)))
65	63, 64	ax-mp 7	. . . . . . . . . 10 |- 1 e. (1...(1 + 1))
66		fveq2 3835	. . . . . . . . . . . 12 |- (k = 1 -> (F` k) = (F` 1))
67	66	eleq1d 1583	. . . . . . . . . . 11 |- (k = 1 -> ((F` k) e. X <-> (F` 1) e. X))
68	67	rcla4v 1919	. . . . . . . . . 10 |- (1 e. (1...(1 + 1)) -> (A.k e. (1...(1 + 1))(F` k) e. X -> (F` 1) e. X))
69	65, 68	ax-mp 7	. . . . . . . . 9 |- (A.k e. (1...(1 + 1))(F` k) e. X -> (F` 1) e. X)
70		eluzfz2 6617	. . . . . . . . . . 11 |- ((1 + 1) e. (ZZ>=` 1) -> (1 + 1) e. (1...(1 + 1)))
71	63, 70	ax-mp 7	. . . . . . . . . 10 |- (1 + 1) e. (1...(1 + 1))
72		fveq2 3835	. . . . . . . . . . . 12 |- (k = (1 + 1) -> (F` k) = (F` (1 + 1)))
73	72	eleq1d 1583	. . . . . . . . . . 11 |- (k = (1 + 1) -> ((F` k) e. X <-> (F` (1 + 1)) e. X))
74	73	rcla4v 1919	. . . . . . . . . 10 |- ((1 + 1) e. (1...(1 + 1)) -> (A.k e. (1...(1 + 1))(F` k) e. X -> (F` (1 + 1)) e. X))
75	71, 74	ax-mp 7	. . . . . . . . 9 |- (A.k e. (1...(1 + 1))(F` k) e. X -> (F` (1 + 1)) e. X)
76	69, 75	jca 286	. . . . . . . 8 |- (A.k e. (1...(1 + 1))(F` k) e. X -> ((F` 1) e. X /\ (F` (1 + 1)) e. X))
77	52, 76	sylan2 453	. . . . . . 7 |- ((M e. Met /\ A.k e. (1...(1 + 1))(F` k) e. X) -> ((F` 1)M(F` (1 + 1))) e. RR)
78	77	adantrr 395	. . . . . 6 |- ((M e. Met /\ (A.k e. (1...(1 + 1))(F` k) e. X /\ A.k e. (1...1)(G` k) = ((F` k)M(F` (k + 1))))) -> ((F` 1)M(F` (1 + 1))) e. RR)
79		elfz3 6619	. . . . . . . . . 10 |- (1 e. ZZ -> 1 e. (1...1))
80	55, 79	ax-mp 7	. . . . . . . . 9 |- 1 e. (1...1)
81		fveq2 3835	. . . . . . . . . . 11 |- (k = 1 -> (G` k) = (G` 1))
82		opreq1 4026	. . . . . . . . . . . . 13 |- (k = 1 -> (k + 1) = (1 + 1))
83	82	fveq2d 3839	. . . . . . . . . . . 12 |- (k = 1 -> (F` (k + 1)) = (F` (1 + 1)))
84	66, 83	opreq12d 4036	. . . . . . . . . . 11 |- (k = 1 -> ((F` k)M(F` (k + 1))) = ((F` 1)M(F` (1 + 1))))
85	81, 84	eqeq12d 1532	. . . . . . . . . 10 |- (k = 1 -> ((G` k) = ((F` k)M(F` (k + 1))) <-> (G` 1) = ((F` 1)M(F` (1 + 1)))))
86	85	rcla4v 1919	. . . . . . . . 9 |- (1 e. (1...1) -> (A.k e. (1...1)(G` k) = ((F` k)M(F` (k + 1))) -> (G` 1) = ((F` 1)M(F` (1 + 1)))))
87	80, 86	ax-mp 7	. . . . . . . 8 |- (A.k e. (1...1)(G` k) = ((F` k)M(F` (k + 1))) -> (G` 1) = ((F` 1)M(F` (1 + 1))))
88	87	ad2antll 407	. . . . . . 7 |- ((M e. Met /\ (A.k e. (1...(1 + 1))(F` k) e. X /\ A.k e. (1...1)(G` k) = ((F` k)M(F` (k + 1))))) -> (G` 1) = ((F` 1)M(F` (1 + 1))))
89		fvex 3843	. . . . . . . 8 |- (G` 1) e. V
90	81	fsum1i 7208	. . . . . . . 8 |- (((G` 1) e. V /\ 1 e. ZZ) -> sum_k e. (1...1)(G` k) = (G` 1))
91	89, 55, 90	mp2an 701	. . . . . . 7 |- sum_k e. (1...1)(G` k) = (G` 1)
92	88, 91	syl5req 1563	. . . . . 6 |- ((M e. Met /\ (A.k e. (1...(1 + 1))(F` k) e. X /\ A.k e. (1...1)(G` k) = ((F` k)M(F` (k + 1))))) -> ((F` 1)M(F` (1 + 1))) = sum_k e. (1...1)(G` k))
93	49, 78, 92	sylanc 473	. . . . 5 |- ((M e. Met /\ (A.k e. (1...(1 + 1))(F` k) e. X /\ A.k e. (1...1)(G` k) = ((F` k)M(F` (k + 1))))) -> ((F` 1)M(F` (1 + 1))) <_ sum_k e. (1...1)(G` k))
94		fzssp1 6637	. . . . . . . . . . 11 |- ((1 e. ZZ /\ (m + 1) e. ZZ) -> (1...(m + 1)) (_ (1...((m + 1) + 1)))
95		nnz 6321	. . . . . . . . . . . 12 |- (m e. NN -> m e. ZZ)
96	95	peano2zdi 6335	. . . . . . . . . . 11 |- (m e. NN -> (m + 1) e. ZZ)
97	94, 55, 96	sylancr 474	. . . . . . . . . 10 |- (m e. NN -> (1...(m + 1)) (_ (1...((m + 1) + 1)))
98		ssralv 2166	. . . . . . . . . 10 |- ((1...(m + 1)) (_ (1...((m + 1) + 1)) -> (A.k e. (1...((m + 1) + 1))(F` k) e. X -> A.k e. (1...(m + 1))(F` k) e. X))
99	97, 98	syl 10	. . . . . . . . 9 |- (m e. NN -> (A.k e. (1...((m + 1) + 1))(F` k) e. X -> A.k e. (1...(m + 1))(F` k) e. X))
100		fzssp1 6637	. . . . . . . . . . 11 |- ((1 e. ZZ /\ m e. ZZ) -> (1...m) (_ (1...(m + 1)))
101	100, 55, 95	sylancr 474	. . . . . . . . . 10 |- (m e. NN -> (1...m) (_ (1...(m + 1)))
102		ssralv 2166	. . . . . . . . . 10 |- ((1...m) (_ (1...(m + 1)) -> (A.k e. (1...(m + 1))(G` k) = ((F` k)M(F` (k + 1))) -> A.k e. (1...m)(G` k) = ((F` k)M(F` (k + 1)))))
103	101, 102	syl 10	. . . . . . . . 9 |- (m e. NN -> (A.k e. (1...(m + 1))(G` k) = ((F` k)M(F` (k + 1))) -> A.k e. (1...m)(G` k) = ((F` k)M(F` (k + 1)))))
104	99, 103	anim12d 561	. . . . . . . 8 |- (m e. NN -> ((A.k e. (1...((m + 1) + 1))(F` k) e. X /\ A.k e. (1...(m + 1))(G` k) = ((F` k)M(F` (k + 1)))) -> (A.k e. (1...(m + 1))(F` k) e. X /\ A.k e. (1...m)(G` k) = ((F` k)M(F` (k + 1))))))
105	104	anim2d 564	. . . . . . 7 |- (m e. NN -> ((M e. Met /\ (A.k e. (1...((m + 1) + 1))(F` k) e. X /\ A.k e. (1...(m + 1))(G` k) = ((F` k)M(F` (k + 1))))) -> (M e. Met /\ (A.k e. (1...(m + 1))(F` k) e. X /\ A.k e. (1...m)(G` k) = ((F` k)M(F` (k + 1)))))))
106	105	imim1d 28	. . . . . 6 |- (m e. NN -> (((M e. Met /\ (A.k e. (1...(m + 1))(F` k) e. X /\ A.k e. (1...m)(G` k) = ((F` k)M(F` (k + 1))))) -> ((F` 1)M(F` (m + 1))) <_ sum_k e. (1...m)(G` k)) -> ((M e. Met /\ (A.k e. (1...((m + 1) + 1))(F` k) e. X /\ A.k e. (1...(m + 1))(G` k) = ((F` k)M(F` (k + 1))))) -> ((F` 1)M(F` (m + 1))) <_ sum_k e. (1...m)(G` k))))
107		leadd1 5779	. . . . . . . . . . . . . . 15 |- ((((F` 1)M(F` (m + 1))) e. RR /\ sum_k e. (1...m)(G` k) e. RR /\ ((F` (m + 1))M(F` ((m + 1) + 1))) e. RR) -> (((F` 1)M(F` (m + 1))) <_ sum_k e. (1...m)(G` k) <-> (((F` 1)M(F` (m + 1))) + ((F` (m + 1))M(F` ((m + 1) + 1)))) <_ (sum_k e. (1...m)(G` k) + ((F` (m + 1))M(F` ((m + 1) + 1))))))
108	50	metcl 8021	. . . . . . . . . . . . . . . 16 |- ((M e. Met /\ (F` 1) e. X /\ (F` (m + 1)) e. X) -> ((F` 1)M(F` (m + 1))) e. RR)
109		simplr 413	. . . . . . . . . . . . . . . 16 |- (((m e. NN /\ M e. Met) /\ (A.k e. (1...((m + 1) + 1))(F` k) e. X /\ A.k e. (1...(m + 1))(G` k) = ((F` k)M(F` (k + 1))))) -> M e. Met)
110	67	rcla4va 1921	. . . . . . . . . . . . . . . . . 18 |- ((1 e. (1...((m + 1) + 1)) /\ A.k e. (1...((m + 1) + 1))(F` k) e. X) -> (F` 1) e. X)
111		peano2nn 6080	. . . . . . . . . . . . . . . . . . . . 21 |- (m e. NN -> (m + 1) e. NN)
112		peano2nn 6080	. . . . . . . . . . . . . . . . . . . . 21 |- ((m + 1) e. NN -> ((m + 1) + 1) e. NN)
113	111, 112	syl 10	. . . . . . . . . . . . . . . . . . . 20 |- (m e. NN -> ((m + 1) + 1) e. NN)
114		elnnuz 6567	. . . . . . . . . . . . . . . . . . . 20 |- (((m + 1) + 1) e. NN <-> ((m + 1) + 1) e. (ZZ>=` 1))
115	113, 114	sylib 196	. . . . . . . . . . . . . . . . . . 19 |- (m e. NN -> ((m + 1) + 1) e. (ZZ>=` 1))
116		eluzfz1 6615	. . . . . . . . . . . . . . . . . . 19 |- (((m + 1) + 1) e. (ZZ>=` 1) -> 1 e. (1...((m + 1) + 1)))
117	115, 116	syl 10	. . . . . . . . . . . . . . . . . 18 |- (m e. NN -> 1 e. (1...((m + 1) + 1)))
118	110, 117	sylan 450	. . . . . . . . . . . . . . . . 17 |- ((m e. NN /\ A.k e. (1...((m + 1) + 1))(F` k) e. X) -> (F` 1) e. X)
119	118	ad2ant2r 409	. . . . . . . . . . . . . . . 16 |- (((m e. NN /\ M e. Met) /\ (A.k e. (1...((m + 1) + 1))(F` k) e. X /\ A.k e. (1...(m + 1))(G` k) = ((F` k)M(F` (k + 1))))) -> (F` 1) e. X)
120		fveq2 3835	. . . . . . . . . . . . . . . . . . . 20 |- (k = (m + 1) -> (F` k) = (F` (m + 1)))
121	120	eleq1d 1583	. . . . . . . . . . . . . . . . . . 19 |- (k = (m + 1) -> ((F` k) e. X <-> (F` (m + 1)) e. X))
122	121	rcla4va 1921	. . . . . . . . . . . . . . . . . 18 |- (((m + 1) e. (1...((m + 1) + 1)) /\ A.k e. (1...((m + 1) + 1))(F` k) e. X) -> (F` (m + 1)) e. X)
123		nnge1 6088	. . . . . . . . . . . . . . . . . . . . 21 |- ((m + 1) e. NN -> 1 <_ (m + 1))
124	111, 123	syl 10	. . . . . . . . . . . . . . . . . . . 20 |- (m e. NN -> 1 <_ (m + 1))
125		nnre 6074	. . . . . . . . . . . . . . . . . . . . 21 |- ((m + 1) e. NN -> (m + 1) e. RR)
126		lep1 5952	. . . . . . . . . . . . . . . . . . . . 21 |- ((m + 1) e. RR -> (m + 1) <_ ((m + 1) + 1))
127	111, 125, 126	3syl 20	. . . . . . . . . . . . . . . . . . . 20 |- (m e. NN -> (m + 1) <_ ((m + 1) + 1))
128	124, 127	jca 286	. . . . . . . . . . . . . . . . . . 19 |- (m e. NN -> (1 <_ (m + 1) /\ (m + 1) <_ ((m + 1) + 1)))
129		elfz 6599	. . . . . . . . . . . . . . . . . . . 20 |- (((m + 1) e. ZZ /\ 1 e. ZZ /\ ((m + 1) + 1) e. ZZ) -> ((m + 1) e. (1...((m + 1) + 1)) <-> (1 <_ (m + 1) /\ (m + 1) <_ ((m + 1) + 1))))
130	55	a1i 8	. . . . . . . . . . . . . . . . . . . 20 |- (m e. NN -> 1 e. ZZ)
131		nnz 6321	. . . . . . . . . . . . . . . . . . . . 21 |- (((m + 1) + 1) e. NN -> ((m + 1) + 1) e. ZZ)
132	111, 112, 131	3syl 20	. . . . . . . . . . . . . . . . . . . 20 |- (m e. NN -> ((m + 1) + 1) e. ZZ)
133	129, 96, 130, 132	syl3anc 864	. . . . . . . . . . . . . . . . . . 19 |- (m e. NN -> ((m + 1) e. (1...((m + 1) + 1)) <-> (1 <_ (m + 1) /\ (m + 1) <_ ((m + 1) + 1))))
134	128, 133	mpbird 194	. . . . . . . . . . . . . . . . . 18 |- (m e. NN -> (m + 1) e. (1...((m + 1) + 1)))
135	122, 134	sylan 450	. . . . . . . . . . . . . . . . 17 |- ((m e. NN /\ A.k e. (1...((m + 1) + 1))(F` k) e. X) -> (F` (m + 1)) e. X)
136	135	ad2ant2r 409	. . . . . . . . . . . . . . . 16 |- (((m e. NN /\ M e. Met) /\ (A.k e. (1...((m + 1) + 1))(F` k) e. X /\ A.k e. (1...(m + 1))(G` k) = ((F` k)M(F` (k + 1))))) -> (F` (m + 1)) e. X)
137	108, 109, 119, 136	syl3anc 864	. . . . . . . . . . . . . . 15 |- (((m e. NN /\ M e. Met) /\ (A.k e. (1...((m + 1) + 1))(F` k) e. X /\ A.k e. (1...(m + 1))(G` k) = ((F` k)M(F` (k + 1))))) -> ((F` 1)M(F` (m + 1))) e. RR)
138		fsumrecl 7220	. . . . . . . . . . . . . . . 16 |- ((m e. (ZZ>=` 1) /\ A.k e. (1...m)(G` k) e. RR) -> sum_k e. (1...m)(G` k) e. RR)
139		elnnuz 6567	. . . . . . . . . . . . . . . . . 18 |- (m e. NN <-> m e. (ZZ>=` 1))
140	139	biimpi 149	. . . . . . . . . . . . . . . . 17 |- (m e. NN -> m e. (ZZ>=` 1))
141	140	ad2antrr 404	. . . . . . . . . . . . . . . 16 |- (((m e. NN /\ M e. Met) /\ (A.k e. (1...((m + 1) + 1))(F` k) e. X /\ A.k e. (1...(m + 1))(G` k) = ((F` k)M(F` (k + 1))))) -> m e. (ZZ>=` 1))
142		ax-17 1007	. . . . . . . . . . . . . . . . . . . 20 |- ((m e. NN /\ M e. Met) -> A.k(m e. NN /\ M e. Met))
143		hbra1 1733	. . . . . . . . . . . . . . . . . . . 20 |- (A.k e. (1...((m + 1) + 1))(F` k) e. X -> A.kA.k e. (1...((m + 1) + 1))(F` k) e. X)
144	142, 143	hban 1045	. . . . . . . . . . . . . . . . . . 19 |- (((m e. NN /\ M e. Met) /\ A.k e. (1...((m + 1) + 1))(F` k) e. X) -> A.k((m e. NN /\ M e. Met) /\ A.k e. (1...((m + 1) + 1))(F` k) e. X))
145		eleq1 1577	. . . . . . . . . . . . . . . . . . . 20 |- ((G` k) = ((F` k)M(F` (k + 1))) -> ((G` k) e. RR <-> ((F` k)M(F` (k + 1))) e. RR))
146	50	metcl 8021	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((M e. Met /\ (F` k) e. X /\ (F` (k + 1)) e. X) -> ((F` k)M(F` (k + 1))) e. RR)
147		simpllr 11363	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((((m e. NN /\ M e. Met) /\ k e. (1...(m + 1))) /\ A.j e. (1...((m + 1) + 1))(F` j) e. X) -> M e. Met)
148		fveq2 3835	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (j = k -> (F` j) = (F` k))
149	148	eleq1d 1583	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (j = k -> ((F` j) e. X <-> (F` k) e. X))
150	149	rcla4va 1921	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((k e. (1...((m + 1) + 1)) /\ A.j e. (1...((m + 1) + 1))(F` j) e. X) -> (F` k) e. X)
151		ssel2 2116	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (((1...(m + 1)) (_ (1...((m + 1) + 1)) /\ k e. (1...(m + 1))) -> k e. (1...((m + 1) + 1)))
152	151, 97	sylan 450	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((m e. NN /\ k e. (1...(m + 1))) -> k e. (1...((m + 1) + 1)))
153	150, 152	sylan 450	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((m e. NN /\ k e. (1...(m + 1))) /\ A.j e. (1...((m + 1) + 1))(F` j) e. X) -> (F` k) e. X)
154	153	adantllr 397	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((((m e. NN /\ M e. Met) /\ k e. (1...(m + 1))) /\ A.j e. (1...((m + 1) + 1))(F` j) e. X) -> (F` k) e. X)
155		fveq2 3835	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (j = (k + 1) -> (F` j) = (F` (k + 1)))
156	155	eleq1d 1583	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (j = (k + 1) -> ((F` j) e. X <-> (F` (k + 1)) e. X))
157	156	rcla4va 1921	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((k + 1) e. (1...((m + 1) + 1)) /\ A.j e. (1...((m + 1) + 1))(F` j) e. X) -> (F` (k + 1)) e. X)
158		fzp1ss 6638	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((1 e. ZZ /\ ((m + 1) + 1) e. ZZ) -> ((1 + 1)...((m + 1) + 1)) (_ (1...((m + 1) + 1)))
159	158, 55, 132	sylancr 474	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (m e. NN -> ((1 + 1)...((m + 1) + 1)) (_ (1...((m + 1) + 1)))
160	159	adantr 389	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((m e. NN /\ k e. (1...(m + 1))) -> ((1 + 1)...((m + 1) + 1)) (_ (1...((m + 1) + 1)))
161		elfzelz 6610	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (k e. (1...(m + 1)) -> k e. ZZ)
162	161	adantl 388	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((m e. NN /\ k e. (1...(m + 1))) -> k e. ZZ)
163		fzaddel 6630	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (((1 e. ZZ /\ (m + 1) e. ZZ) /\ (k e. ZZ /\ 1 e. ZZ)) -> (k e. (1...(m + 1)) <-> (k + 1) e. ((1 + 1)...((m + 1) + 1))))
164	55	a1i 8	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ((m e. NN /\ k e. ZZ) -> 1 e. ZZ)
165	96	adantr 389	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ((m e. NN /\ k e. ZZ) -> (m + 1) e. ZZ)
166		pm3.27 321	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ((m e. NN /\ k e. ZZ) -> k e. ZZ)
167	163, 164, 165, 166, 164	syl2anc 475	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ((m e. NN /\ k e. ZZ) -> (k e. (1...(m + 1)) <-> (k + 1) e. ((1 + 1)...((m + 1) + 1))))
168	167	biimpd 151	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((m e. NN /\ k e. ZZ) -> (k e. (1...(m + 1)) -> (k + 1) e. ((1 + 1)...((m + 1) + 1))))
169	168	ex 371	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (m e. NN -> (k e. ZZ -> (k e. (1...(m + 1)) -> (k + 1) e. ((1 + 1)...((m + 1) + 1)))))
170	169	com23 32	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (m e. NN -> (k e. (1...(m + 1)) -> (k e. ZZ -> (k + 1) e. ((1 + 1)...((m + 1) + 1)))))
171	170	imp 348	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((m e. NN /\ k e. (1...(m + 1))) -> (k e. ZZ -> (k + 1) e. ((1 + 1)...((m + 1) + 1))))
172	162, 171	mpd 26	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((m