Theorem fsequb 6583

Description: The values of a finite real sequence have an upper bound. Warning: The HTML proof page is 1/2 megabyte in size.

Assertion

Ref	Expression
fsequb	|- ((N e. (ZZ>` M) /\ A.k e. (M...N)(F` k) e. RR) -> E.x e. RR A.k e. (M...N)(F` k) < x)

Distinct variable groups:   x,k,F   k,M,x   k,N,x

Proof of Theorem fsequb

Step	Hyp	Ref	Expression
1		opreq2 4045	. . . . . 6 |- (j = M -> (M...j) = (M...M))
2	1	raleq1d 1827	. . . . 5 |- (j = M -> (A.n e. (M...j)(F` n) e. RR <-> A.n e. (M...M)(F` n) e. RR))
3	1	raleq1d 1827	. . . . . 6 |- (j = M -> (A.k e. (M...j)(F` k) < x <-> A.k e. (M...M)(F` k) < x))
4	3	rexbidv 1702	. . . . 5 |- (j = M -> (E.x e. RR A.k e. (M...j)(F` k) < x <-> E.x e. RR A.k e. (M...M)(F` k) < x))
5	2, 4	imbi12d 628	. . . 4 |- (j = M -> ((A.n e. (M...j)(F` n) e. RR -> E.x e. RR A.k e. (M...j)(F` k) < x) <-> (A.n e. (M...M)(F` n) e. RR -> E.x e. RR A.k e. (M...M)(F` k) < x)))
6		opreq2 4045	. . . . . 6 |- (j = m -> (M...j) = (M...m))
7	6	raleq1d 1827	. . . . 5 |- (j = m -> (A.n e. (M...j)(F` n) e. RR <-> A.n e. (M...m)(F` n) e. RR))
8	6	raleq1d 1827	. . . . . 6 |- (j = m -> (A.k e. (M...j)(F` k) < x <-> A.k e. (M...m)(F` k) < x))
9	8	rexbidv 1702	. . . . 5 |- (j = m -> (E.x e. RR A.k e. (M...j)(F` k) < x <-> E.x e. RR A.k e. (M...m)(F` k) < x))
10	7, 9	imbi12d 628	. . . 4 |- (j = m -> ((A.n e. (M...j)(F` n) e. RR -> E.x e. RR A.k e. (M...j)(F` k) < x) <-> (A.n e. (M...m)(F` n) e. RR -> E.x e. RR A.k e. (M...m)(F` k) < x)))
11		opreq2 4045	. . . . . 6 |- (j = (m + 1) -> (M...j) = (M...(m + 1)))
12	11	raleq1d 1827	. . . . 5 |- (j = (m + 1) -> (A.n e. (M...j)(F` n) e. RR <-> A.n e. (M...(m + 1))(F` n) e. RR))
13	11	raleq1d 1827	. . . . . 6 |- (j = (m + 1) -> (A.k e. (M...j)(F` k) < x <-> A.k e. (M...(m + 1))(F` k) < x))
14	13	rexbidv 1702	. . . . 5 |- (j = (m + 1) -> (E.x e. RR A.k e. (M...j)(F` k) < x <-> E.x e. RR A.k e. (M...(m + 1))(F` k) < x))
15	12, 14	imbi12d 628	. . . 4 |- (j = (m + 1) -> ((A.n e. (M...j)(F` n) e. RR -> E.x e. RR A.k e. (M...j)(F` k) < x) <-> (A.n e. (M...(m + 1))(F` n) e. RR -> E.x e. RR A.k e. (M...(m + 1))(F` k) < x)))
16		opreq2 4045	. . . . . 6 |- (j = N -> (M...j) = (M...N))
17	16	raleq1d 1827	. . . . 5 |- (j = N -> (A.n e. (M...j)(F` n) e. RR <-> A.n e. (M...N)(F` n) e. RR))
18	16	raleq1d 1827	. . . . . 6 |- (j = N -> (A.k e. (M...j)(F` k) < x <-> A.k e. (M...N)(F` k) < x))
19	18	rexbidv 1702	. . . . 5 |- (j = N -> (E.x e. RR A.k e. (M...j)(F` k) < x <-> E.x e. RR A.k e. (M...N)(F` k) < x))
20	17, 19	imbi12d 628	. . . 4 |- (j = N -> ((A.n e. (M...j)(F` n) e. RR -> E.x e. RR A.k e. (M...j)(F` k) < x) <-> (A.n e. (M...N)(F` n) e. RR -> E.x e. RR A.k e. (M...N)(F` k) < x)))
21		elfz3 6551	. . . . . 6 |- (M e. ZZ -> M e. (M...M))
22		fveq2 3800	. . . . . . . 8 |- (n = M -> (F` n) = (F` M))
23	22	eleq1d 1577	. . . . . . 7 |- (n = M -> ((F` n) e. RR <-> (F` M) e. RR))
24	23	rcla4v 1911	. . . . . 6 |- (M e. (M...M) -> (A.n e. (M...M)(F` n) e. RR -> (F` M) e. RR))
25	21, 24	syl 10	. . . . 5 |- (M e. ZZ -> (A.n e. (M...M)(F` n) e. RR -> (F` M) e. RR))
26		peano2re 5525	. . . . . . . 8 |- ((F` M) e. RR -> ((F` M) + 1) e. RR)
27		fveq2 3800	. . . . . . . . . . . 12 |- (k = M -> (F` k) = (F` M))
28	27	breq1d 2679	. . . . . . . . . . 11 |- (k = M -> ((F` k) < ((F` M) + 1) <-> (F` M) < ((F` M) + 1)))
29		ltp1 5895	. . . . . . . . . . 11 |- ((F` M) e. RR -> (F` M) < ((F` M) + 1))
30	28, 29	syl5cbir 209	. . . . . . . . . 10 |- ((F` M) e. RR -> (k = M -> (F` k) < ((F` M) + 1)))
31		elfz1eq 6552	. . . . . . . . . 10 |- (k e. (M...M) -> k = M)
32	30, 31	syl5 21	. . . . . . . . 9 |- ((F` M) e. RR -> (k e. (M...M) -> (F` k) < ((F` M) + 1)))
33	32	r19.21aiv 1751	. . . . . . . 8 |- ((F` M) e. RR -> A.k e. (M...M)(F` k) < ((F` M) + 1))
34	26, 33	jca 286	. . . . . . 7 |- ((F` M) e. RR -> (((F` M) + 1) e. RR /\ A.k e. (M...M)(F` k) < ((F` M) + 1)))
35	34	a1i 8	. . . . . 6 |- (M e. ZZ -> ((F` M) e. RR -> (((F` M) + 1) e. RR /\ A.k e. (M...M)(F` k) < ((F` M) + 1))))
36		breq2 2673	. . . . . . . 8 |- (x = ((F` M) + 1) -> ((F` k) < x <-> (F` k) < ((F` M) + 1)))
37	36	ralbidv 1701	. . . . . . 7 |- (x = ((F` M) + 1) -> (A.k e. (M...M)(F` k) < x <-> A.k e. (M...M)(F` k) < ((F` M) + 1)))
38	37	rcla4ev 1915	. . . . . 6 |- ((((F` M) + 1) e. RR /\ A.k e. (M...M)(F` k) < ((F` M) + 1)) -> E.x e. RR A.k e. (M...M)(F` k) < x)
39	35, 38	syl6 22	. . . . 5 |- (M e. ZZ -> ((F` M) e. RR -> E.x e. RR A.k e. (M...M)(F` k) < x))
40	25, 39	syld 27	. . . 4 |- (M e. ZZ -> (A.n e. (M...M)(F` n) e. RR -> E.x e. RR A.k e. (M...M)(F` k) < x))
41		fzssp1 6566	. . . . . . . . . . . 12 |- ((M e. ZZ /\ m e. ZZ) -> (M...m) (_ (M...(m + 1)))
42		eluzel2 6484	. . . . . . . . . . . 12 |- (m e. (ZZ>` M) -> M e. ZZ)
43		eluzelz 6483	. . . . . . . . . . . 12 |- (m e. (ZZ>` M) -> m e. ZZ)
44	41, 42, 43	sylanc 473	. . . . . . . . . . 11 |- (m e. (ZZ>` M) -> (M...m) (_ (M...(m + 1)))
45	44	sseld 2111	. . . . . . . . . 10 |- (m e. (ZZ>` M) -> (n e. (M...m) -> n e. (M...(m + 1))))
46	45	imim1d 28	. . . . . . . . 9 |- (m e. (ZZ>` M) -> ((n e. (M...(m + 1)) -> (F` n) e. RR) -> (n e. (M...m) -> (F` n) e. RR)))
47	46	r19.20dv2 1749	. . . . . . . 8 |- (m e. (ZZ>` M) -> (A.n e. (M...(m + 1))(F` n) e. RR -> A.n e. (M...m)(F` n) e. RR))
48	47	imim1d 28	. . . . . . 7 |- (m e. (ZZ>` M) -> ((A.n e. (M...m)(F` n) e. RR -> E.x e. RR A.k e. (M...m)(F` k) < x) -> (A.n e. (M...(m + 1))(F` n) e. RR -> E.x e. RR A.k e. (M...m)(F` k) < x)))
49	48	imp32 361	. . . . . 6 |- ((m e. (ZZ>` M) /\ ((A.n e. (M...m)(F` n) e. RR -> E.x e. RR A.k e. (M...m)(