Theorem mettrifi 15847

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 4889	. . . . . . . . . 10 |- (j = 1 -> (j + 1) = (1 + 1))
2	1	opreq2d 4898	. . . . . . . . 9 |- (j = 1 -> (1...(j + 1)) = (1...(1 + 1)))
3	2	raleqdv 2269	. . . . . . . 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 4890	. . . . . . . . 9 |- (j = 1 -> (1...j) = (1...1))
5	4	raleqdv 2269	. . . . . . . 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 690	. . . . . . 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 678	. . . . . 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 4685	. . . . . . . 8 |- (j = 1 -> (F` (j + 1)) = (F` (1 + 1)))
9	8	opreq2d 4898	. . . . . . 7 |- (j = 1 -> ((F` 1)M(F` (j + 1))) = ((F` 1)M(F` (1 + 1))))
10	4	sumeq1d 8250	. . . . . . 7 |- (j = 1 -> sum_k e. (1...j)(G` k) = sum_k e. (1...1)(G` k))
11	9, 10	breq12d 3351	. . . . . 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 688	. . . . 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 4889	. . . . . . . . . 10 |- (j = m -> (j + 1) = (m + 1))
14	13	opreq2d 4898	. . . . . . . . 9 |- (j = m -> (1...(j + 1)) = (1...(m + 1)))
15	14	raleqdv 2269	. . . . . . . 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 4890	. . . . . . . . 9 |- (j = m -> (1...j) = (1...m))
17	16	raleqdv 2269	. . . . . . . 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 690	. . . . . . 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 678	. . . . . 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 4685	. . . . . . . 8 |- (j = m -> (F` (j + 1)) = (F` (m + 1)))
21	20	opreq2d 4898	. . . . . . 7 |- (j = m -> ((F` 1)M(F` (j + 1))) = ((F` 1)M(F` (m + 1))))
22	16	sumeq1d 8250	. . . . . . 7 |- (j = m -> sum_k e. (1...j)(G` k) = sum_k e. (1...m)(G` k))
23	21, 22	breq12d 3351	. . . . . 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 688	. . . . 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 4889	. . . . . . . . . 10 |- (j = (m + 1) -> (j + 1) = ((m + 1) + 1))
26	25	opreq2d 4898	. . . . . . . . 9 |- (j = (m + 1) -> (1...(j + 1)) = (1...((m + 1) + 1)))
27	26	raleqdv 2269	. . . . . . . 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 4890	. . . . . . . . 9 |- (j = (m + 1) -> (1...j) = (1...(m + 1)))
29	28	raleqdv 2269	. . . . . . . 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 690	. . . . . . 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 678	. . . . . 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 4685	. . . . . . . 8 |- (j = (m + 1) -> (F` (j + 1)) = (F` ((m + 1) + 1)))
33	32	opreq2d 4898	. . . . . . 7 |- (j = (m + 1) -> ((F` 1)M(F` (j + 1))) = ((F` 1)M(F` ((m + 1) + 1))))
34	28	sumeq1d 8250	. . . . . . 7 |- (j = (m + 1) -> sum_k e. (1...j)(G` k) = sum_k e. (1...(m + 1))(G` k))
35	33, 34	breq12d 3351	. . . . . 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 688	. . . . 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 4889	. . . . . . . . . 10 |- (j = N -> (j + 1) = (N + 1))
38	37	opreq2d 4898	. . . . . . . . 9 |- (j = N -> (1...(j + 1)) = (1...(N + 1)))
39	38	raleqdv 2269	. . . . . . . 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 4890	. . . . . . . . 9 |- (j = N -> (1...j) = (1...N))
41	40	raleqdv 2269	. . . . . . . 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 690	. . . . . . 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 678	. . . . . 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 4685	. . . . . . . 8 |- (j = N -> (F` (j + 1)) = (F` (N + 1)))
45	44	opreq2d 4898	. . . . . . 7 |- (j = N -> ((F` 1)M(F` (j + 1))) = ((F` 1)M(F` (N + 1))))
46	40	sumeq1d 8250	. . . . . . 7 |- (j = N -> sum_k e. (1...j)(G` k) = sum_k e. (1...N)(G` k))
47	45, 46	breq12d 3351	. . . . . 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 688	. . . . 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		mettrifi.1	. . . . . . . . . 10 |- X = dom dom M
50	49	metcl 9088	. . . . . . . . 9 |- ((M e. Met /\ (F` 1) e. X /\ (F` (1 + 1)) e. X) -> ((F` 1)M(F` (1 + 1))) e. RR)
51	50	3expb 1068	. . . . . . . 8 |- ((M e. Met /\ ((F` 1) e. X /\ (F` (1 + 1)) e. X)) -> ((F` 1)M(F` (1 + 1))) e. RR)
52		df-2 7154	. . . . . . . . . . . . . 14 |- 2 = (1 + 1)
53	52	eleq1i 1960	. . . . . . . . . . . . 13 |- (2 e. (ZZ>=` 1) <-> (1 + 1) e. (ZZ>=` 1))
54		1z 7368	. . . . . . . . . . . . . 14 |- 1 e. ZZ
55	54	eluz1i 7591	. . . . . . . . . . . . 13 |- (2 e. (ZZ>=` 1) <-> (2 e. ZZ /\ 1 <_ 2))
56	53, 55	bitr3i 192	. . . . . . . . . . . 12 |- ((1 + 1) e. (ZZ>=` 1) <-> (2 e. ZZ /\ 1 <_ 2))
57		2z 7369	. . . . . . . . . . . 12 |- 2 e. ZZ
58		1re 6598	. . . . . . . . . . . . 13 |- 1 e. RR
59		2re 7163	. . . . . . . . . . . . 13 |- 2 e. RR
60		1lt2 7212	. . . . . . . . . . . . 13 |- 1 < 2
61	58, 59, 60	ltleii 6756	. . . . . . . . . . . 12 |- 1 <_ 2
62	56, 57, 61	mpbir2an 800	. . . . . . . . . . 11 |- (1 + 1) e. (ZZ>=` 1)
63		eluzfz1 7657	. . . . . . . . . . 11 |- ((1 + 1) e. (ZZ>=` 1) -> 1 e. (1...(1 + 1)))
64	62, 63	ax-mp 7	. . . . . . . . . 10 |- 1 e. (1...(1 + 1))
65		fveq2 4681	. . . . . . . . . . . 12 |- (k = 1 -> (F` k) = (F` 1))
66	65	eleq1d 1963	. . . . . . . . . . 11 |- (k = 1 -> ((F` k) e. X <-> (F` 1) e. X))
67	66	rcla4v 2376	. . . . . . . . . 10 |- (1 e. (1...(1 + 1)) -> (A.k e. (1...(1 + 1))(F` k) e. X -> (F` 1) e. X))
68	64, 67	ax-mp 7	. . . . . . . . 9 |- (A.k e. (1...(1 + 1))(F` k) e. X -> (F` 1) e. X)
69		eluzfz2 7659	. . . . . . . . . . 11 |- ((1 + 1) e. (ZZ>=` 1) -> (1 + 1) e. (1...(1 + 1)))
70	62, 69	ax-mp 7	. . . . . . . . . 10 |- (1 + 1) e. (1...(1 + 1))
71		fveq2 4681	. . . . . . . . . . . 12 |- (k = (1 + 1) -> (F` k) = (F` (1 + 1)))
72	71	eleq1d 1963	. . . . . . . . . . 11 |- (k = (1 + 1) -> ((F` k) e. X <-> (F` (1 + 1)) e. X))
73	72	rcla4v 2376	. . . . . . . . . 10 |- ((1 + 1) e. (1...(1 + 1)) -> (A.k e. (1...(1 + 1))(F` k) e. X -> (F` (1 + 1)) e. X))
74	70, 73	ax-mp 7	. . . . . . . . 9 |- (A.k e. (1...(1 + 1))(F` k) e. X -> (F` (1 + 1)) e. X)
75	68, 74	jca 310	. . . . . . . 8 |- (A.k e. (1...(1 + 1))(F` k) e. X -> ((F` 1) e. X /\ (F` (1 + 1)) e. X))
76	51, 75	sylan2 500	. . . . . . 7 |- ((M e. Met /\ A.k e. (1...(1 + 1))(F` k) e. X) -> ((F` 1)M(F` (1 + 1))) e. RR)
77	76	adantrr 431	. . . . . 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)
78		elfz3 7661	. . . . . . . . . 10 |- (1 e. ZZ -> 1 e. (1...1))
79	54, 78	ax-mp 7	. . . . . . . . 9 |- 1 e. (1...1)
80		fveq2 4681	. . . . . . . . . . 11 |- (k = 1 -> (G` k) = (G` 1))
81		opreq1 4889	. . . . . . . . . . . . 13 |- (k = 1 -> (k + 1) = (1 + 1))
82	81	fveq2d 4685	. . . . . . . . . . . 12 |- (k = 1 -> (F` (k + 1)) = (F` (1 + 1)))
83	65, 82	opreq12d 4900	. . . . . . . . . . 11 |- (k = 1 -> ((F` k)M(F` (k + 1))) = ((F` 1)M(F` (1 + 1))))
84	80, 83	eqeq12d 1899	. . . . . . . . . 10 |- (k = 1 -> ((G` k) = ((F` k)M(F` (k + 1))) <-> (G` 1) = ((F` 1)M(F` (1 + 1)))))
85	84	rcla4v 2376	. . . . . . . . 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)))))
86	79, 85	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))))
87	86	ad2antll 443	. . . . . . 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))))
88		fvex 4689	. . . . . . . 8 |- (G` 1) e. _V
89	80	fsum1i 8265	. . . . . . . 8 |- (((G` 1) e. _V /\ 1 e. ZZ) -> sum_k e. (1...1)(G` k) = (G` 1))
90	88, 54, 89	mp2an 761	. . . . . . 7 |- sum_k e. (1...1)(G` k) = (G` 1)
91	87, 90	syl5req 1941	. . . . . 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))
92		eqle 6746	. . . . . 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))
93	77, 91, 92	syl11anc 524	. . . . 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 7679	. . . . . . . . . . 11 |- ((1 e. ZZ /\ (m + 1) e. ZZ) -> (1...(m + 1)) C_ (1...((m + 1) + 1)))
95		nnz 7362	. . . . . . . . . . . 12 |- (m e. NN -> m e. ZZ)
96	95	peano2zdi 7376	. . . . . . . . . . 11 |- (m e. NN -> (m + 1) e. ZZ)
97	94, 54, 96	sylancr 526	. . . . . . . . . 10 |- (m e. NN -> (1...(m + 1)) C_ (1...((m + 1) + 1)))
98		ssralv 2672	. . . . . . . . . 10 |- ((1...(m + 1)) C_ (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 12	. . . . . . . . 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 7679	. . . . . . . . . . 11 |- ((1 e. ZZ /\ m e. ZZ) -> (1...m) C_ (1...(m + 1)))
101	100, 54, 95	sylancr 526	. . . . . . . . . 10 |- (m e. NN -> (1...m) C_ (1...(m + 1)))
102		ssralv 2672	. . . . . . . . . 10 |- ((1...m) C_ (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 12	. . . . . . . . 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 617	. . . . . . . 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 620	. . . . . . 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 33	. . . . . 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		simplr 449	. . . . . . . . . . . . . . 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))))) -> M e. Met)
108	66	rcla4va 2378	. . . . . . . . . . . . . . . . 17 |- ((1 e. (1...((m + 1) + 1)) /\ A.k e. (1...((m + 1) + 1))(F` k) e. X) -> (F` 1) e. X)
109		peano2nn 7118	. . . . . . . . . . . . . . . . . . . 20 |- (m e. NN -> (m + 1) e. NN)
110		peano2nn 7118	. . . . . . . . . . . . . . . . . . . 20 |- ((m + 1) e. NN -> ((m + 1) + 1) e. NN)
111	109, 110	syl 12	. . . . . . . . . . . . . . . . . . 19 |- (m e. NN -> ((m + 1) + 1) e. NN)
112		elnnuz 7609	. . . . . . . . . . . . . . . . . . 19 |- (((m + 1) + 1) e. NN <-> ((m + 1) + 1) e. (ZZ>=` 1))
113	111, 112	sylib 215	. . . . . . . . . . . . . . . . . 18 |- (m e. NN -> ((m + 1) + 1) e. (ZZ>=` 1))
114		eluzfz1 7657	. . . . . . . . . . . . . . . . . 18 |- (((m + 1) + 1) e. (ZZ>=` 1) -> 1 e. (1...((m + 1) + 1)))
115	113, 114	syl 12	. . . . . . . . . . . . . . . . 17 |- (m e. NN -> 1 e. (1...((m + 1) + 1)))
116	108, 115	sylan 497	. . . . . . . . . . . . . . . 16 |- ((m e. NN /\ A.k e. (1...((m + 1) + 1))(F` k) e. X) -> (F` 1) e. X)
117	116	ad2ant2r 445	. . . . . . . . . . . . . . 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) e. X)
118		fveq2 4681	. . . . . . . . . . . . . . . . . . 19 |- (k = (m + 1) -> (F` k) = (F` (m + 1)))
119	118	eleq1d 1963	. . . . . . . . . . . . . . . . . 18 |- (k = (m + 1) -> ((F` k) e. X <-> (F` (m + 1)) e. X))
120	119	rcla4va 2378	. . . . . . . . . . . . . . . . 17 |- (((m + 1) e. (1...((m + 1) + 1)) /\ A.k e. (1...((m + 1) + 1))(F` k) e. X) -> (F` (m + 1)) e. X)
121	54	a1i 8	. . . . . . . . . . . . . . . . . . 19 |- (m e. NN -> 1 e. ZZ)
122		nnz 7362	. . . . . . . . . . . . . . . . . . . 20 |- (((m + 1) + 1) e. NN -> ((m + 1) + 1) e. ZZ)
123	109, 110, 122	3syl 24	. . . . . . . . . . . . . . . . . . 19 |- (m e. NN -> ((m + 1) + 1) e. ZZ)
124		elfz 7641	. . . . . . . . . . . . . . . . . . 19 |- (((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))))
125	96, 121, 123, 124	syl111anc 1100	. . . . . . . . . . . . . . . . . 18 |- (m e. NN -> ((m + 1) e. (1...((m + 1) + 1)) <-> (1 <_ (m + 1) /\ (m + 1) <_ ((m + 1) + 1))))
126		nnge1 7126	. . . . . . . . . . . . . . . . . . 19 |- ((m + 1) e. NN -> 1 <_ (m + 1))
127	109, 126	syl 12	. . . . . . . . . . . . . . . . . 18 |- (m e. NN -> 1 <_ (m + 1))
128		nnre 7112	. . . . . . . . . . . . . . . . . . 19 |- ((m + 1) e. NN -> (m + 1) e. RR)
129		lep1 6990	. . . . . . . . . . . . . . . . . . 19 |- ((m + 1) e. RR -> (m + 1) <_ ((m + 1) + 1))
130	109, 128, 129	3syl 24	. . . . . . . . . . . . . . . . . 18 |- (m e. NN -> (m + 1) <_ ((m + 1) + 1))
131	125, 127, 130	mpbir2and 802	. . . . . . . . . . . . . . . . 17 |- (m e. NN -> (m + 1) e. (1...((m + 1) + 1)))
132	120, 131	sylan 497	. . . . . . . . . . . . . . . 16 |- ((m e. NN /\ A.k e. (1...((m + 1) + 1))(F` k) e. X) -> (F` (m + 1)) e. X)
133	132	ad2ant2r 445	. . . . . . . . . . . . . . 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` (m + 1)) e. X)
134	49	metcl 9088	. . . . . . . . . . . . . . 15 |- ((M e. Met /\ (F` 1) e. X /\ (F` (m + 1)) e. X) -> ((F` 1)M(F` (m + 1))) e. RR)
135	107, 117, 133, 134	syl111anc 1100	. . . . . . . . . . . . . 14 |- (((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)
136		elnnuz 7609	. . . . . . . . . . . . . . . . 17 |- (m e. NN <-> m e. (ZZ>=` 1))
137	136	biimpi 168	. . . . . . . . . . . . . . . 16 |- (m e. NN -> m e. (ZZ>=` 1))
138	137	ad2antrr 440	. . . . . . . . . . . . . . 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))))) -> m e. (ZZ>=` 1))
139	101	ad2antrr 440	. . . . . . . . . . . . . . . . 17 |- (((m e. NN /\ M e. Met) /\ A.k e. (1...((m + 1) + 1))(F` k) e. X) -> (1...m) C_ (1...(m + 1)))
140		ax-17 1317	. . . . . . . . . . . . . . . . . . 19 |- ((m e. NN /\ M e. Met) -> A.k(m e. NN /\ M e. Met))
141		hbra1 2147	. . . . . . . . . . . . . . . . . . 19 |- (A.k e. (1...((m + 1) + 1))(F` k) e. X -> A.kA.k e. (1...((m + 1) + 1))(F` k) e. X)
142	140, 141	hban 1356	. . . . . . . . . . . . . . . . . 18 |- (((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))
143		eleq1 1957	. . . . . . . . . . . . . . . . . . 19 |- ((G` k) = ((F` k)M(F` (k + 1))) -> ((G` k) e. RR <-> ((F` k)M(F` (k + 1))) e. RR))
144		simpllr 453	. . . . . . . . . . . . . . . . . . . . . 22 |- ((((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)
145		fveq2 4681	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (j = k -> (F` j) = (F` k))
146	145	eleq1d 1963	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (j = k -> ((F` j) e. X <-> (F` k) e. X))
147	146	rcla4va 2378	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((k e. (1...((m + 1) + 1)) /\ A.j e. (1...((m + 1) + 1))(F` j) e. X) -> (F` k) e. X)
148		ssel2 2616	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((1...(m + 1)) C_ (1...((m + 1) + 1)) /\ k e. (1...(m + 1))) -> k e. (1...((m + 1) + 1)))
149	148, 97	sylan 497	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((m e. NN /\ k e. (1...(m + 1))) -> k e. (1...((m + 1) + 1)))
150	147, 149	sylan 497	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((m e. NN /\ k e. (1...(m + 1))) /\ A.j e. (1...((m + 1) + 1))(F` j) e. X) -> (F` k) e. X)
151	150	adantllr 433	. . . . . . . . . . . . . . . . . . . . . 22 |- ((((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)
152		fveq2 4681	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (j = (k + 1) -> (F` j) = (F` (k + 1)))
153	152	eleq1d 1963	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (j = (k + 1) -> ((F` j) e. X <-> (F` (k + 1)) e. X))
154	153	rcla4va 2378	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((k + 1) e. (1...((m + 1) + 1)) /\ A.j e. (1...((m + 1) + 1))(F` j) e. X) -> (F` (k + 1)) e. X)
155		fzp1ss 7680	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((1 e. ZZ /\ ((m + 1) + 1) e. ZZ) -> ((1 + 1)...((m + 1) + 1)) C_ (1...((m + 1) + 1)))
156	155, 54, 123	sylancr 526	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (m e. NN -> ((1 + 1)...((m + 1) + 1)) C_ (1...((m + 1) + 1)))
157	156	adantr 425	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((m e. NN /\ k e. (1...(m + 1))) -> ((1 + 1)...((m + 1) + 1)) C_ (1...((m + 1) + 1)))
158		elfzelz 7652	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (k e. (1...(m + 1)) -> k e. ZZ)
159	158	adantl 424	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((m e. NN /\ k e. (1...(m + 1))) -> k e. ZZ)
160	54	a1i 8	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ((m e. NN /\ k e. ZZ) -> 1 e. ZZ)
161	96	adantr 425	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ((m e. NN /\ k e. ZZ) -> (m + 1) e. ZZ)
162		simpr 350	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ((m e. NN /\ k e. ZZ) -> k e. ZZ)
163		fzaddel 7672	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (((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	160, 161, 162, 160, 163	syl22anc 1101	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((m e. NN /\ k e. ZZ) -> (k e. (1...(m + 1)) <-> (k + 1) e. ((1 + 1)...((m + 1) + 1))))
165	164	biimpd 170	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((m e. NN /\ k e. ZZ) -> (k e. (1...(m + 1)) -> (k + 1) e. ((1 + 1)...((m + 1) + 1))))
166	165	ex 402	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (m e. NN -> (k e. ZZ -> (k e. (1...(m + 1)) -> (k + 1) e. ((1 + 1)...((m + 1) + 1)))))
167	166	com23 36	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (m e. NN -> (k e. (1...(m + 1)) -> (k e. ZZ -> (k + 1) e. ((1 + 1)...((m + 1) + 1)))))
168	167	imp 377	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((m e. NN /\ k e. (1...(m + 1))) -> (k e. ZZ -> (k + 1) e. ((1 + 1)...((m + 1) + 1))))
169	159, 168	mpd 29	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((m e. NN /\ k e. (1...(m + 1))) -> (k + 1) e. ((1 + 1)...((m + 1) + 1)))
170	157, 169	sseldd 2620	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((m e. NN /\ k e. (1...(m + 1))) -> (k + 1) e. (1...((m + 1) + 1)))
171	154, 170	sylan 497	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((m e. NN /\ k e. (1...(m + 1))) /\ A.j e. (1...((m + 1) + 1))(F` j) e. X) -> (F` (k + 1)) e. X)
172	171	adantllr 433	. . . . . . . . . . . . . . . . . . . . . 22 |- ((((m e. NN /\ M e. Met) /\ k e. (1...(m + 1))) /\ A.j e. (1...((m + 1) + 1))(F` j) e. X) -> (F` (k + 1)) e. X)
173	49	metcl 9088	. . . . . . . . . . . . . . . . . . . . . 22 |- ((M e. Met /\ (F` k) e. X /\ (F` (k + 1)) e. X) -> ((F` k)M(F` (k + 1))) e. RR)
174	144, 151, 172, 173	syl111anc 1100	. . . . . . . . . . . . . . . . . . . . 21 |- ((((m e. NN /\ M e. Met) /\ k e. (1...(m + 1))) /\ A.j e. (1...((m + 1) + 1))(F` j) e. X) -> ((F` k)M(F` (k + 1))) e. RR)
175		fveq2 4681	. . . . . . . . . . . . . . . . . . . . . . 23 |- (k = j -> (F` k) = (F` j))
176	175	eleq1d 1963	. . . . . . . . . . . . . . . . . . . . . 22 |- (k = j -> ((F` k) e. X <-> (F` j) e. X))
177	176	cbvralv 2280	. . . . . . . . . . . . . . . . . . . . 21 |- (A.k e. (1...((m + 1) + 1))(F` k) e. X <-> A.j e. (1...((m + 1) + 1))(F` j) e. X)
178	174, 177	sylan2b 501	. . . . . . . . . . . . . . . . . . . 20 |- ((((m e. NN /\ M e. Met) /\ k e. (1...(m + 1))) /\ A.k e. (1...((m + 1) + 1))(F` k) e. X) -> ((F` k)M(F` (k + 1))) e. RR)
179	178	an1rs 547	. . . . . . . . . . . . . . . . . . 19 |- ((((m e. NN /\ M e. Met) /\ A.k e. (1...((m + 1) + 1))(F` k) e. X) /\ k e. (1...(m + 1))) -> ((F` k)M(F` (k + 1))) e. RR)
180	143, 179	syl5cbir 228	. . . . . . . . . . . . . . . . . 18 |- ((((m e. NN /\ M e. Met) /\ A.k e. (1...((m + 1) + 1))(F` k) e. X) /\ k e. (1...(m + 1))) -> ((G` k) = ((F` k)M(F` (k + 1))) -> (G` k) e. RR))
181	142, 180	ralimdaa 2170	. . . . . . . . . . . . . . . . 17 |- (((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))) -> A.k e. (1...(m + 1))(G` k) e. RR))
182		ssralv 2672	. . . . . . . . . . . . . . . . 17 |- ((1...m) C_ (1...(m + 1)) -> (A.k e. (1...(m + 1))(G` k) e. RR -> A.k e. (1...m)(G` k) e. RR))
183	139, 181, 182	sylsyld 32	. . . . . . . . . . . . . . . 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))) -> A.k e. (1...m)(G` k) e. RR))
184	183	impr 422	. . . . . . . . . . . . . . 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))))) -> A.k e. (1...m)(G` k) e. RR)
185		fsumrecl 8277	. . . . . . . . . . . . . . 15 |- ((m e. (ZZ>=` 1) /\ A.k e. (1...m)(G` k) e. RR) -> sum_k e. (1...m)(G` k) e. RR)
186	138, 184, 185	syl11anc 524	. . . . . . . . . . . . . 14 |- (((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))))) -> sum_k e. (1...m)(G` k) e. RR)
187		fveq2 4681	. . . . . . . . . . . . . . . . . . 19 |- (k = ((m + 1) + 1) -> (F` k) = (F` ((m + 1) + 1)))
188	187	eleq1d 1963	. . . . . . . . . . . . . . . . . 18 |- (k = ((m + 1) + 1) -> ((F` k) e. X <-> (F` ((m + 1) + 1)) e. X))
189	188	rcla4va 2378	. . . . . . . . . . . . . . . . 17 |- ((((m + 1) + 1) e. (1...((m + 1) + 1)) /\ A.k e. (1...((m + 1) + 1))(F` k) e. X) -> (F` ((m + 1) + 1)) e. X)
190		eluzfz2 7659	. . . . . . . . . . . . . . . . . 18 |- (((m + 1) + 1) e. (ZZ>=` 1) -> ((m + 1) + 1) e. (1...((m + 1) + 1)))
191	113, 190	syl 12	. . . . . . . . . . . . . . . . 17 |- (m e. NN -> ((m + 1) + 1) e. (1...((m + 1) + 1)))
192	189, 191	sylan 497	. . . . . . . . . . . . . . . 16 |- ((m e. NN /\ A.k e. (1...((m + 1) + 1))(F` k) e. X) -> (F` ((m + 1) + 1)) e. X)
193	192	ad2ant2r 445	. . . . . . . . . . . . . . 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` ((m + 1) + 1)) e. X)
194	49	metcl 9088	. . . . . . . . . . . . . . 15 |- ((M e. Met /\ (F` (m + 1)) e. X /\ (F` ((m + 1) + 1)) e. X) -> ((F` (m + 1))M(F` ((m + 1) + 1))) e. RR)
195	107, 133, 193, 194	syl111anc 1100	. . . . . . . . . . . . . 14 |- (((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))M(F` ((m + 1) + 1))) e. RR)
196		leadd1 6808	. . . . . . . . . . . . . 14 |- ((((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))))))
197	135, 186, 195, 196	syl111anc 1100	. . . . . . . . . . . . 13 |- (((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))) <_ 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))))))
198	197	biimpa 460	. . . . . . . . . . . 12 |- ((((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))) <_ 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)))))
199		fvex 4689	. . . . . . . . . . . . . . . . 17 |- (G` k) e. _V
200		fvex 4689	. . . . . . . . . . . . . . . . 17 |- (G` (m + 1)) e. _V
201		fveq2 4681	. . . . . . . . . . . . . . . . 17 |- (k = (m + 1) -> (G` k) = (G` (m + 1)))
202	199, 200, 201	fsump1i 8266	. . . . . . . . . . . . . . . 16 |- (m e. (ZZ>=` 1) -> sum_k e. (1...(m + 1))(G` k) = (sum_k e. (1...m)(G` k) + (G` (m + 1))))
203	136, 202	sylbi 216	. . . . . . . . . . . . . . 15 |- (m e. NN -> sum_k e. (1...(m + 1))(G` k) = (sum_k e. (1...m)(G` k) + (G` (m + 1))))
204	203	adantr 425	. . . . . . . . . . . . . 14 |- ((m e. NN /\ M e. Met) -> sum_k e. (1...(m + 1))(G` k) = (sum_k e. (1...m)(G` k) + (G` (m + 1))))
205	204	ad2antrr 440	. . . . . . . . . . . . 13 |- ((((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))) <_ sum_k e. (1...m)(G` k)) -> sum_k e. (1...(m + 1))(G` k) = (sum_k e. (1...m)(G` k) + (G` (m + 1))))
206		opreq1 4889	. . . . . . . . . . . . . . . . . . . . 21 |- (k = (m + 1) -> (k + 1) = ((m + 1) + 1))
207	206	fveq2d 4685	. . . . . . . . . . . . . . . . . . . 20 |- (k = (m + 1) -> (F` (k + 1)) = (F` ((m + 1) + 1)))
208	118, 207	opreq12d 4900	. . . . . . . . . . . . . . . . . . 19 |- (k = (m + 1) -> ((F` k)M(F` (k + 1))) = ((F` (m + 1))M(F` ((m + 1) + 1))))
209	201, 208	eqeq12d 1899	. . . . . . . . . . . . . . . . . 18 |- (k = (m + 1) -> ((G` k) = ((F` k)M(F` (k + 1))) <-> (G` (m + 1)) = ((F` (m + 1))M(F` ((m + 1) + 1)))))
210	209	rcla4va 2378	. . . . . . . . . . . . . . . . 17 |- (((m + 1) e. (1...(m + 1)) /\ A.k e. (1...(m + 1))(G` k) = ((F` k)M(F` (k + 1)))) -> (G` (m + 1)) = ((F` (m + 1))M(F` ((m + 1) + 1))))
211		elnnuz 7609	. . . . . . . . . . . . . . . . . . 19 |- ((m + 1) e. NN <-> (m + 1) e. (ZZ>=` 1))
212		eluzfz2 7659	. . . . . . . . . . . . . . . . . . 19 |- ((m + 1) e. (ZZ>=` 1) -> (m + 1) e. (1...(m + 1)))
213	211, 212	sylbi 216	. . . . . . . . . . . . . . . . . 18 |- ((m + 1) e. NN -> (m + 1) e. (1...(m + 1)))
214	109, 213	syl 12	. . . . . . . . . . . . . . . . 17 |- (m e. NN -> (m + 1) e. (1...(m + 1)))
215	210, 214	sylan 497	. . . . . . . . . . . . . . . 16 |- ((m e. NN /\ A.k e. (1...(m + 1))(G` k) = ((F` k)M(F` (k + 1)))) -> (G` (m + 1)) = ((F` (m + 1))M(F` ((m + 1) + 1))))
216	215	ad2ant2rl 447	. . . . . . . . . . . . . . 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))))) -> (G` (m + 1)) = ((F` (m + 1))M(F` ((m + 1) + 1))))
217	216	adantr 425	. . . . . . . . . . . . . 14 |- ((((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))) <_ sum_k e. (1...m)(G` k)) -> (G` (m + 1)) = ((F` (m + 1))M(F` ((m + 1) + 1))))
218	217	opreq2d 4898	. . . . . . . . . . . . 13 |- ((((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))) <_ sum_k e. (1...m)(G` k)) -> (sum_k e. (1...m)(G` k) + (G` (m + 1))) = (sum_k e. (1...m)(G` k) + ((F` (m + 1))M(F` ((m + 1) + 1)))))
219	205, 218	eqtrd 1925	. . . . . . . . . . . 12 |- ((((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))) <_ sum_k e. (1...m)(G` k)) -> sum_k e. (1...(m + 1))(G` k) = (sum_k e. (1...m)(G` k) + ((F` (m + 1))M(F` ((m + 1) + 1)))))
220	198, 219	breqtrrd 3363	. . . . . . . . . . 11 |- ((((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))) <_ 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 + 1))(G` k))
221	220	ex 402	. . . . . . . . . 10 |- (((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))) <_ 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 + 1))(G` k)))
222		simplr 449	. . . . . . . . . . . 12 |- (((m e. NN /\ M e. Met) /\ A.k e. (1...((m + 1) + 1))(F` k) e. X) -> M e. Met)
223	116, 192, 132	3jca 1050	. . . . . . . . . . . . 13 |- ((m e. NN /\ A.k e. (1...((m + 1) + 1))(F` k) e. X) -> ((F` 1) e. X /\ (F` ((m + 1) + 1)) e. X /\ (F` (m + 1)) e. X))
224	223	adantlr 429	. . . . . . . . . . . 12 |- (((m e. NN /\ M e. Met) /\ A.k e. (1...((m + 1) + 1))(F` k) e. X) -> ((F` 1) e. X /\ (F` ((m + 1) + 1)) e. X /\ (F` (m + 1)) e. X))
225	49	mettri 9094	. . . . . . . . . . . 12 |- ((M e. Met /\ ((F` 1) e. X /\ (F` ((m + 1) + 1)) e. X /\ (F` (m + 1)) e. X)) -> ((F` 1)M(F` ((m + 1) + 1))) <_ (((F` 1)M(F` (m + 1))) + ((F` (m + 1))M(F` ((m + 1) + 1)))))
226	222, 224, 225	syl11anc 524	. . . . . . . . . . 11 |- (((m e. NN /\ M e. Met) /\ A.k e. (1...((m + 1) + 1))(F` k) e. X) -> ((F` 1)M(F` ((m + 1) + 1))) <_ (((F` 1)M(F` (m + 1))) + ((F` (m + 1))M(F` ((m + 1) + 1)))))
227	226	adantrr 431	. . . . . . . . . 10 |- (((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) + 1))) <_ (((F` 1)M(F` (m + 1))) + ((F` (m + 1))M(F` ((m + 1) + 1)))))
228	221, 227	jctild 662	. . . . . . . . 9 |- (((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))) <_ sum_k e. (1...m)(G` k) -> (((F` 1)M(F` ((m + 1) + 1))) <_ (((F` 1)M(F` (m + 1))) + ((F` (m + 1))M(F` ((m + 1) + 1)))) /\ (((F` 1)M(F` (m + 1))) + ((F` (m + 1))M(F` ((m + 1) + 1)))) <_ sum_k e. (1...(m + 1))(G` k))))
229	49	metcl 9088	. . . . . . . . . . . . . . 15 |- ((M e. Met /\ (F` 1) e. X /\ (F` ((m + 1) + 1)) e. X) -> ((F` 1)M(F` ((m + 1) + 1))) e. RR)
230	229	3expb 1068	. . . . . . . . . . . . . 14 |- ((M e. Met /\ ((F` 1) e. X /\ (F` ((m + 1) + 1)) e. X)) -> ((F` 1)M(F` ((m + 1) + 1))) e. RR)
231	116, 192	jca 310	. . . . . . . . . . . . . 14 |- ((m e. NN /\ A.k e. (1...((m + 1) + 1))(F` k) e. X) -> ((F` 1) e. X /\ (F` ((m + 1) + 1)) e. X))
232	230, 231	sylan2 500	. . . . . . . . . . . . 13 |- ((M e. Met /\ (m e. NN /\ A.k e. (1...((m + 1) + 1))(F` k) e. X)) -> ((F` 1)M(F` ((m + 1) + 1))) e. RR)
233	232	anassrs 489	. . . . . . . . . . . 12 |- (((M e. Met /\ m e. NN) /\ A.k e. (1...((m + 1) + 1))(F` k) e. X) -> ((F` 1)M(F` ((m + 1) + 1))) e. RR)
234	233	ancom1s 548	. . . . . . . . . . 11 |- (((m e. NN /\ M e. Met) /\ A.k e. (1...((m + 1) + 1))(F` k) e. X) -> ((F` 1)M(F` ((m + 1) + 1))) e. RR)
235	234	adantrr 431	. . . . . . . . . 10 |- (((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) + 1))) e. RR)
236		readdcl 6455	. . . . . . . . . . 11 |- ((((F` 1)M(F` (m + 1))) e. RR /\ ((F` (m + 1))M(F` ((m + 1) + 1))) e. RR) -> (((F` 1)M(F` (m + 1))) + ((F` (m + 1))M(F` ((m + 1) + 1)))) e. RR)
237	135, 195, 236	syl11anc 524	. . . . . . . . . 10 |- (((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))) + ((F` (m + 1))M(F` ((m + 1) + 1)))) e. RR)
238	109, 211	sylib 215	. . . . . . . . . . . 12 |- (m e. NN -> (m + 1) e. (ZZ>=` 1))
239	238	ad2antrr 440	. . . . . . . . . . 11 |- (((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 + 1) e. (ZZ>=` 1))
240	181	impr 422	. . . . . . . . . . 11 |- (((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))))) -> A.k e. (1...(m + 1))(G` k) e. RR)
241		fsumrecl 8277	. . . . . . . . . . 11 |- (((m + 1) e. (ZZ>=` 1) /\ A.k e. (1...(m + 1))(G` k) e. RR) -> sum_k e. (1...(m + 1))(G` k) e. RR)
242	239, 240, 241	syl11anc 524	. . . . . . . . . 10 |- (((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))))) -> sum_k e. (1...(m + 1))(G` k) e. RR)
243		letr 6695	. . . . . . . . . 10 |- ((((F` 1)M(F` ((m + 1) + 1))) e. RR /\ (((F` 1)M(F` (m + 1))) + ((F` (m + 1))M(F` ((m + 1) + 1)))) e. RR /\ sum_k e. (1...(m + 1))(G` k) e. RR) -> ((((F` 1)M(F` ((m + 1) + 1))) <_ (((F` 1)M(F` (m + 1))) + ((F` (m + 1))M(F` ((m + 1) + 1)))) /\ (((F` 1)M(F` (m + 1))) + ((F` (m + 1))M(F` ((m + 1) + 1)))) <_ sum_k e. (1...(m + 1))(G` k)) -> ((F` 1)M(F` ((m + 1) + 1))) <_ sum_k e. (1...(m + 1))(G` k)))
244	235, 237, 242, 243	syl111anc 1100	. . . . . . . . 9 |- (((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) + 1))) <_ (((F` 1)M(F` (m + 1))) + ((F` (m + 1))M(F` ((m + 1) + 1)))) /\ (((F` 1)M(F` (m + 1))) + ((F` (m + 1))M(F` ((m + 1) + 1)))) <_ sum_k e. (1...(m + 1))(G` k)) -> ((F` 1)M(F` ((m + 1) + 1))) <_ sum_k e. (1...(m + 1))(G` k)))
245	228, 244	syld 30	. . . . . . . 8 |- (((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))) <_ sum_k e. (1...m)(G` k) -> ((F` 1)M(F` ((m + 1) + 1))) <_ sum_k e. (1...(m + 1))(G` k)))
246	245	expl 420	. . . . . . 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))))) -> (((F` 1)M(F` (m + 1))) <_ sum_k e. (1...m)(G` k) -> ((F` 1)M(F` ((m + 1) + 1))) <_ sum_k e. (1...(m + 1))(G` k))))
247	246	a2d 16	. . . . . 6 |- (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))) <_ 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) + 1))) <_ sum_k e. (1...(m + 1))(G` k))))
248	106, 247	syld 30	. . . . 5 |- (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) + 1))) <_ sum_k e. (1...(m + 1))(G` k))))
249	12, 24, 36, 48, 93, 248	nnind 7120	. . . 4 |- (N e. NN -> ((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)))
250	249	imp 377	. . 3 |- ((N e. NN /\ (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))
251	250	anassrs 489	. 2 |- (((N e. NN /\ 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))
252	251	ancom1s 548	1 |- (((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))

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240   /\ w3a 858   = wceq 1298   e. wcel 1300  A.wral 2105  _Vcvv 2292   C_ wss 2593   class class class wbr 3338  dom cdm 3986  ` cfv 3998  (class class class)co 4884  RRcr 6385  1c1 6387   + caddc 6389   <_ cle 6448  NNcn 6449  ZZcz 6451  2c2 7145  ZZ>=cuz 7586  ...cfz 7637  sum_csu 8239  Metcme 9066

This theorem is referenced by:  mettrifi2 15848

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  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