Theorem fsequb 7702

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 4890	. . . . . 6 |- (j = M -> (M...j) = (M...M))
2	1	raleqdv 2269	. . . . 5 |- (j = M -> (A.n e. (M...j)(F` n) e. RR <-> A.n e. (M...M)(F` n) e. RR))
3	1	raleqdv 2269	. . . . . 6 |- (j = M -> (A.k e. (M...j)(F` k) < x <-> A.k e. (M...M)(F` k) < x))
4	3	rexbidv 2124	. . . . 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 688	. . . 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 4890	. . . . . 6 |- (j = m -> (M...j) = (M...m))
7	6	raleqdv 2269	. . . . 5 |- (j = m -> (A.n e. (M...j)(F` n) e. RR <-> A.n e. (M...m)(F` n) e. RR))
8	6	raleqdv 2269	. . . . . 6 |- (j = m -> (A.k e. (M...j)(F` k) < x <-> A.k e. (M...m)(F` k) < x))
9	8	rexbidv 2124	. . . . 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 688	. . . 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 4890	. . . . . 6 |- (j = (m + 1) -> (M...j) = (M...(m + 1)))
12	11	raleqdv 2269	. . . . 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	raleqdv 2269	. . . . . 6 |- (j = (m + 1) -> (A.k e. (M...j)(F` k) < x <-> A.k e. (M...(m + 1))(F` k) < x))
14	13	rexbidv 2124	. . . . 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 688	. . . 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 4890	. . . . . 6 |- (j = N -> (M...j) = (M...N))
17	16	raleqdv 2269	. . . . 5 |- (j = N -> (A.n e. (M...j)(F` n) e. RR <-> A.n e. (M...N)(F` n) e. RR))
18	16	raleqdv 2269	. . . . . 6 |- (j = N -> (A.k e. (M...j)(F` k) < x <-> A.k e. (M...N)(F` k) < x))
19	18	rexbidv 2124	. . . . 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 688	. . . 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 7661	. . . . . 6 |- (M e. ZZ -> M e. (M...M))
22		fveq2 4681	. . . . . . . 8 |- (n = M -> (F` n) = (F` M))
23	22	eleq1d 1963	. . . . . . 7 |- (n = M -> ((F` n) e. RR <-> (F` M) e. RR))
24	23	rcla4v 2376	. . . . . 6 |- (M e. (M...M) -> (A.n e. (M...M)(F` n) e. RR -> (F` M) e. RR))
25	21, 24	syl 12	. . . . 5 |- (M e. ZZ -> (A.n e. (M...M)(F` n) e. RR -> (F` M) e. RR))
26		peano2re 6599	. . . . . . . 8 |- ((F` M) e. RR -> ((F` M) + 1) e. RR)
27		fveq2 4681	. . . . . . . . . . . 12 |- (k = M -> (F` k) = (F` M))
28	27	breq1d 3348	. . . . . . . . . . 11 |- (k = M -> ((F` k) < ((F` M) + 1) <-> (F` M) < ((F` M) + 1)))
29		ltp1 6989	. . . . . . . . . . 11 |- ((F` M) e. RR -> (F` M) < ((F` M) + 1))
30	28, 29	syl5cbir 228	. . . . . . . . . 10 |- ((F` M) e. RR -> (k = M -> (F` k) < ((F` M) + 1)))
31		elfz1eq 7662	. . . . . . . . . 10 |- (k e. (M...M) -> k = M)
32	30, 31	syl5 20	. . . . . . . . 9 |- ((F` M) e. RR -> (k e. (M...M) -> (F` k) < ((F` M) + 1)))
33	32	r19.21aiv 2175	. . . . . . . 8 |- ((F` M) e. RR -> A.k e. (M...M)(F` k) < ((F` M) + 1))
34	26, 33	jca 310	. . . . . . 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 3342	. . . . . . . 8 |- (x = ((F` M) + 1) -> ((F` k) < x <-> (F` k) < ((F` M) + 1)))
37	36	ralbidv 2123	. . . . . . 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 2381	. . . . . 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 25	. . . . 5 |- (M e. ZZ -> ((F` M) e. RR -> E.x e. RR A.k e. (M...M)(F` k) < x))
40	25, 39	syld 30	. . . 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		eluzel2 7593	. . . . . . . . . . . 12 |- (m e. (ZZ>=` M) -> M e. ZZ)
42		eluzelz 7592	. . . . . . . . . . . 12 |- (m e. (ZZ>=` M) -> m e. ZZ)
43		fzssp1 7679	. . . . . . . . . . . 12 |- ((M e. ZZ /\ m e. ZZ) -> (M...m) C_ (M...(m + 1)))
44	41, 42, 43	syl11anc 524	. . . . . . . . . . 11 |- (m e. (ZZ>=` M) -> (M...m) C_ (M...(m + 1)))
45	44	sseld 2619	. . . . . . . . . 10 |- (m e. (ZZ>=` M) -> (n e. (M...m) -> n e. (M...(m + 1))))
46	45	imim1d 33	. . . . . . . . 9 |- (m e. (ZZ>=` M) -> ((n e. (M...(m + 1)) -> (F` n) e. RR) -> (n e. (M...m) -> (F` n) e. RR)))
47	46	ralimdv2 2173	. . . . . . . 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 33	. . . . . . 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 390	. . . . . 6 |- ((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)
50		fveq2 4681	. . . . . . . . . 10 |- (n = (m + 1) -> (F` n) = (F` (m + 1)))
51	50	eleq1d 1963	. . . . . . . . 9 |- (n = (m + 1) -> ((F` n) e. RR <-> (F` (m + 1)) e. RR))
52	51	rcla4va 2378	. . . . . . . 8 |- (((m + 1) e. (M...(m + 1)) /\ A.n e. (M...(m + 1))(F` n) e. RR) -> (F` (m + 1)) e. RR)
53		peano2uz 7616	. . . . . . . . 9 |- (m e. (ZZ>=` M) -> (m + 1) e. (ZZ>=` M))
54		eluzfz2 7659	. . . . . . . . 9 |- ((m + 1) e. (ZZ>=` M) -> (m + 1) e. (M...(m + 1)))
55	53, 54	syl 12	. . . . . . . 8 |- (m e. (ZZ>=` M) -> (m + 1) e. (M...(m + 1)))
56	52, 55	sylan 497	. . . . . . 7 |- ((m e. (ZZ>=` M) /\ A.n e. (M...(m + 1))(F` n) e. RR) -> (F` (m + 1)) e. RR)
57	56	adantrl 430	. . . . . 6 |- ((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)) -> (F` (m + 1)) e. RR)
58		elfzp1 7683	. . . . . . . . . . . . . . . . . . 19 |- (m e. (ZZ>=` M) -> (k e. (M...(m + 1)) <-> (k e. (M...m) \/ k = (m + 1))))
59	58	adantr 425	. . . . . . . . . . . . . . . . . 18 |- ((m e. (ZZ>=` M) /\ A.n e. (M...(m + 1))(F` n) e. RR) -> (k e. (M...(m + 1)) <-> (k e. (M...m) \/ k = (m + 1))))
60	59	ad2antrr 440	. . . . . . . . . . . . . . . . 17 |- ((((m e. (ZZ>=` M) /\ A.n e. (M...(m + 1))(F` n) e. RR) /\ (x e. RR /\ (F` (m + 1)) e. RR)) /\ (k e. (M...m) -> (F` k) < x)) -> (k e. (M...(m + 1)) <-> (k e. (M...m) \/ k = (m + 1))))
61		max2 7100	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((((F` (m + 1)) + 1) e. RR /\ x e. RR) -> x <_ if(((F` (m + 1)) + 1) <_ x, x, ((F` (m + 1)) + 1)))
62		peano2re 6599	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((F` (m + 1)) e. RR -> ((F` (m + 1)) + 1) e. RR)
63	61, 62	sylan 497	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((F` (m + 1)) e. RR /\ x e. RR) -> x <_ if(((F` (m + 1)) + 1) <_ x, x, ((F` (m + 1)) + 1)))
64	63	ancoms 484	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((x e. RR /\ (F` (m + 1)) e. RR) -> x <_ if(((F` (m + 1)) + 1) <_ x, x, ((F` (m + 1)) + 1)))
65	64	ad2antlr 441	. . . . . . . . . . . . . . . . . . . . . 22 |- ((((m e. (ZZ>=` M) /\ A.n e. (M...(m + 1))(F` n) e. RR) /\ (x e. RR /\ (F` (m + 1)) e. RR)) /\ k e. (M...m)) -> x <_ if(((F` (m + 1)) + 1) <_ x, x, ((F` (m + 1)) + 1)))
66		fveq2 4681	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (n = k -> (F` n) = (F` k))
67	66	eleq1d 1963	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (n = k -> ((F` n) e. RR <-> (F` k) e. RR))
68	67	rcla4va 2378	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((k e. (M...(m + 1)) /\ A.n e. (M...(m + 1))(F` n) e. RR) -> (F` k) e. RR)
69		fzelp1 7681	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((m e. (ZZ>=` M) /\ k e. (M...m)) -> k e. (M...(m + 1)))
70	68, 69	sylan 497	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((m e. (ZZ>=` M) /\ k e. (M...m)) /\ A.n e. (M...(m + 1))(F` n) e. RR) -> (F` k) e. RR)
71	70	an1rs 547	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((m e. (ZZ>=` M) /\ A.n e. (M...(m + 1))(F` n) e. RR) /\ k e. (M...m)) -> (F` k) e. RR)
72	71	adantlr 429	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((((m e. (ZZ>=` M) /\ A.n e. (M...(m + 1))(F` n) e. RR) /\ (x e. RR /\ (F` (m + 1)) e. RR)) /\ k e. (M...m)) -> (F` k) e. RR)
73		simplrl 454	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((((m e. (ZZ>=` M) /\ A.n e. (M...(m + 1))(F` n) e. RR) /\ (x e. RR /\ (F` (m + 1)) e. RR)) /\ k e. (M...m)) -> x e. RR)
74		ifcl 3007	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((x e. RR /\ ((F` (m + 1)) + 1) e. RR) -> if(((F` (m + 1)) + 1) <_ x, x, ((F` (m + 1)) + 1)) e. RR)
75	74, 62	sylan2 500	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((x e. RR /\ (F` (m + 1)) e. RR) -> if(((F` (m + 1)) + 1) <_ x, x, ((F` (m + 1)) + 1)) e. RR)
76	75	ad2antlr 441	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((((m e. (ZZ>=` M) /\ A.n e. (M...(m + 1))(F` n) e. RR) /\ (x e. RR /\ (F` (m + 1)) e. RR)) /\ k e. (M...m)) -> if(((F` (m + 1)) + 1) <_ x, x, ((F` (m + 1)) + 1)) e. RR)
77		ltletr 6694	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((F` k) e. RR /\ x e. RR /\ if(((F` (m + 1)) + 1) <_ x, x, ((F` (m + 1)) + 1)) e. RR) -> (((F` k) < x /\ x <_ if(((F` (m + 1)) + 1) <_ x, x, ((F` (m + 1)) + 1))) -> (F` k) < if(((F` (m + 1)) + 1) <_ x, x, ((F` (m + 1)) + 1))))
78	72, 73, 76, 77	syl111anc 1100	. . . . . . . . . . . . . . . . . . . . . 22 |- ((((m e. (ZZ>=` M) /\ A.n e. (M...(m + 1))(F` n) e. RR) /\ (x e. RR /\ (F` (m + 1)) e. RR)) /\ k e. (M...m)) -> (((F` k) < x /\ x <_ if(((F` (m + 1)) + 1) <_ x, x, ((F` (m + 1)) + 1))) -> (F` k) < if(((F` (m + 1)) + 1) <_ x, x, ((F` (m + 1)) + 1))))
79	65, 78	mpan2d 766	. . . . . . . . . . . . . . . . . . . . 21 |- ((((m e. (ZZ>=` M) /\ A.n e. (M...(m + 1))(F` n) e. RR) /\ (x e. RR /\ (F` (m + 1)) e. RR)) /\ k e. (M...m)) -> ((F` k) < x -> (F` k) < if(((F` (m + 1)) + 1) <_ x, x, ((F` (m + 1)) + 1))))
80	79	ex 402	. . . . . . . . . . . . . . . . . . . 20 |- (((m e. (ZZ>=` M) /\ A.n e. (M...(m + 1))(F` n) e. RR) /\ (x e. RR /\ (F` (m + 1)) e. RR)) -> (k e. (M...m) -> ((F` k) < x -> (F` k) < if(((F` (m + 1)) + 1) <_ x, x, ((F` (m + 1)) + 1)))))
81	80	a2d 16	. . . . . . . . . . . . . . . . . . 19 |- (((m e. (ZZ>=` M) /\ A.n e. (M...(m + 1))(F` n) e. RR) /\ (x e. RR /\ (F` (m + 1)) e. RR)) -> ((k e. (M...m) -> (F` k) < x) -> (k e. (M...m) -> (F` k) < if(((F` (m + 1)) + 1) <_ x, x, ((F` (m + 1)) + 1)))))
82	81	imp 377	. . . . . . . . . . . . . . . . . 18 |- ((((m e. (ZZ>=` M) /\ A.n e. (M...(m + 1))(F` n) e. RR) /\ (x e. RR /\ (F` (m + 1)) e. RR)) /\ (k e. (M...m) -> (F` k) < x)) -> (k e. (M...m) -> (F` k) < if(((F` (m + 1)) + 1) <_ x, x, ((F` (m + 1)) + 1))))
83		fveq2 4681	. . . . . . . . . . . . . . . . . . . . 21 |- (k = (m + 1) -> (F` k) = (F` (m + 1)))
84	83	breq1d 3348	. . . . . . . . . . . . . . . . . . . 20 |- (k = (m + 1) -> ((F` k) < if(((F` (m + 1)) + 1) <_ x, x, ((F` (m + 1)) + 1)) <-> (F` (m + 1)) < if(((F` (m + 1)) + 1) <_ x, x, ((F` (m + 1)) + 1))))
85		simpr 350	. . . . . . . . . . . . . . . . . . . . 21 |- ((x e. RR /\ (F` (m + 1)) e. RR) -> (F` (m + 1)) e. RR)
86	62	adantl 424	. . . . . . . . . . . . . . . . . . . . 21 |- ((x e. RR /\ (F` (m + 1)) e. RR) -> ((F` (m + 1)) + 1) e. RR)
87		ltp1 6989	. . . . . . . . . . . . . . . . . . . . . 22 |- ((F` (m + 1)) e. RR -> (F` (m + 1)) < ((F` (m + 1)) + 1))
88	87	adantl 424	. . . . . . . . . . . . . . . . . . . . 21 |- ((x e. RR /\ (F` (m + 1)) e. RR) -> (F` (m + 1)) < ((F` (m + 1)) + 1))
89		max1ALT 7099	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((F` (m + 1)) + 1) e. RR -> ((F` (m + 1)) + 1) <_ if(((F` (m + 1)) + 1) <_ x, x, ((F` (m + 1)) + 1)))
90	62, 89	syl 12	. . . . . . . . . . . . . . . . . . . . . 22 |- ((F` (m + 1)) e. RR -> ((F` (m + 1)) + 1) <_ if(((F` (m + 1)) + 1) <_ x, x, ((F` (m + 1)) + 1)))
91	90	adantl 424	. . . . . . . . . . . . . . . . . . . . 21 |- ((x e. RR /\ (F` (m + 1)) e. RR) -> ((F` (m + 1)) + 1) <_ if(((F` (m + 1)) + 1) <_ x, x, ((F` (m + 1)) + 1)))
92	85, 86, 75, 88, 91	ltletrd 6698	. . . . . . . . . . . . . . . . . . . 20 |- ((x e. RR /\ (F` (m + 1)) e. RR) -> (F` (m + 1)) < if(((F` (m + 1)) + 1) <_ x, x, ((F` (m + 1)) + 1)))
93	84, 92	syl5cbir 228	. . . . . . . . . . . . . . . . . . 19 |- ((x e. RR /\ (F` (m + 1)) e. RR) -> (k = (m + 1) -> (F` k) < if(((F` (m + 1)) + 1) <_ x, x, ((F` (m + 1)) + 1))))
94	93	ad2antlr 441	. . . . . . . . . . . . . . . . . 18 |- ((((m e. (ZZ>=` M) /\ A.n e. (M...(m + 1))(F` n) e. RR) /\ (x e. RR /\ (F` (m + 1)) e. RR)) /\ (k e. (M...m) -> (F` k) < x)) -> (k = (m + 1) -> (F` k) < if(((F` (m + 1)) + 1) <_ x, x, ((F` (m + 1)) + 1))))
95	82, 94	jaod 469	. . . . . . . . . . . . . . . . 17 |- ((((m e. (ZZ>=` M) /\ A.n e. (M...(m + 1))(F` n) e. RR) /\ (x e. RR /\ (F` (m + 1)) e. RR)) /\ (k e. (M...m) -> (F` k) < x)) -> ((k e. (M...m) \/ k = (m + 1)) -> (F` k) < if(((F` (m + 1)) + 1) <_ x, x, ((F` (m + 1)) + 1))))
96	60, 95	sylbid 220	. . . . . . . . . . . . . . . 16 |- ((((m e. (ZZ>=` M) /\ A.n e. (M...(m + 1))(F` n) e. RR) /\ (x e. RR /\ (F` (m + 1)) e. RR)) /\ (k e. (M...m) -> (F` k) < x)) -> (k e. (M...(m + 1)) -> (F` k) < if(((F` (m + 1)) + 1) <_ x, x, ((F` (m + 1)) + 1))))
97	96	ex 402	. . . . . . . . . . . . . . 15 |- (((m e. (ZZ>=` M) /\ A.n e. (M...(m + 1))(F` n) e. RR) /\ (x e. RR /\ (F` (m + 1)) e. RR)) -> ((k e. (M...m) -> (F` k) < x) -> (k e. (M...(m + 1)) -> (F` k) < if(((F` (m + 1)) + 1) <_ x, x, ((F` (m + 1)) + 1)))))
98	97	ralimdv2 2173	. . . . . . . . . . . . . 14 |- (((m e. (ZZ>=` M) /\ A.n e. (M...(m + 1))(F` n) e. RR) /\ (x e. RR /\ (F` (m + 1)) e. RR)) -> (A.k e. (M...m)(F` k) < x -> A.k e. (M...(m + 1))(F` k) < if(((F` (m + 1)) + 1) <_ x, x, ((F` (m + 1)) + 1))))
99	75	adantl 424	. . . . . . . . . . . . . 14 |- (((m e. (ZZ>=` M) /\ A.n e. (M...(m + 1))(F` n) e. RR) /\ (x e. RR /\ (F` (m + 1)) e. RR)) -> if(((F` (m + 1)) + 1) <_ x, x, ((F` (m + 1)) + 1)) e. RR)
100	98, 99	jctild 662	. . . . . . . . . . . . 13 |- (((m e. (ZZ>=` M) /\ A.n e. (M...(m + 1))(F` n) e. RR) /\ (x e. RR /\ (F` (m + 1)) e. RR)) -> (A.k e. (M...m)(F` k) < x -> (if(((F` (m + 1)) + 1) <_ x, x, ((F` (m + 1)) + 1)) e. RR /\ A.k e. (M...(m + 1))(F` k) < if(((F` (m + 1)) + 1) <_ x, x, ((F` (m + 1)) + 1)))))
101		breq2 3342	. . . . . . . . . . . . . . 15 |- (y = if(((F` (m + 1)) + 1) <_ x, x, ((F` (m + 1)) + 1)) -> ((F` k) < y <-> (F` k) < if(((F` (m + 1)) + 1) <_ x, x, ((F` (m + 1)) + 1))))
102	101	ralbidv 2123	. . . . . . . . . . . . . 14 |- (y = if(((F` (m + 1)) + 1) <_ x, x, ((F` (m + 1)) + 1)) -> (A.k e. (M...(m + 1))(F` k) < y <-> A.k e. (M...(m + 1))(F` k) < if(((F` (m + 1)) + 1) <_ x, x, ((F` (m + 1)) + 1))))
103	102	rcla4ev 2381	. . . . . . . . . . . . 13 |- ((if(((F` (m + 1)) + 1) <_ x, x, ((F` (m + 1)) + 1)) e. RR /\ A.k e. (M...(m + 1))(F` k) < if(((F` (m + 1)) + 1) <_ x, x, ((F` (m + 1)) + 1))) -> E.y e. RR A.k e. (M...(m + 1))(F` k) < y)
104	100, 103	syl6 25	. . . . . . . . . . . 12 |- (((m e. (ZZ>=` M) /\ A.n e. (M...(m + 1))(F` n) e. RR) /\ (x e. RR /\ (F` (m + 1)) e. RR)) -> (A.k e. (M...m)(F` k) < x -> E.y e. RR A.k e. (M...(m + 1))(F` k) < y))
105	104	exp32 408	. . . . . . . . . . 11 |- ((m e. (ZZ>=` M) /\ A.n e. (M...(m + 1))(F` n) e. RR) -> (x e. RR -> ((F` (m + 1)) e. RR -> (A.k e. (M...m)(F` k) < x -> E.y e. RR A.k e. (M...(m + 1))(F` k) < y))))
106	105	com34 40	. . . . . . . . . 10 |- ((m e. (ZZ>=` M) /\ A.n e. (M...(m + 1))(F` n) e. RR) -> (x e. RR -> (A.k e. (M...m)(F` k) < x -> ((F` (m + 1)) e. RR -> E.y e. RR A.k e. (M...(m + 1))(F` k) < y))))
107	106	r19.23adv 2215	. . . . . . . . 9 |- ((m e. (ZZ>=` M) /\ A.n e. (M...(m + 1))(F` n) e. RR) -> (E.x e. RR A.k e. (M...m)(F` k) < x -> ((F` (m + 1)) e. RR -> E.y e. RR A.k e. (M...(m + 1))(F` k) < y)))
108	107	imp3a 388	. . . . . . . 8 |- ((m e. (ZZ>=` M) /\ A.n e. (M...(m + 1))(F` n) e. RR) -> ((E.x e. RR A.k e. (M...m)(F` k) < x /\ (F` (m + 1)) e. RR) -> E.y e. RR A.k e. (M...(m + 1))(F` k) < y))
109		breq2 3342	. . . . . . . . . 10 |- (y = x -> ((F` k) < y <-> (F` k) < x))
110	109	ralbidv 2123	. . . . . . . . 9 |- (y = x -> (A.k e. (M...(m + 1))(F` k) < y <-> A.k e. (M...(m + 1))(F` k) < x))
111	110	cbvrexv 2281	. . . . . . . 8 |- (E.y e. RR A.k e. (M...(m + 1))(F` k) < y <-> E.x e. RR A.k e. (M...(m + 1))(F` k) < x)
112	108, 111	syl6ib 229	. . . . . . 7 |- ((m e. (ZZ>=` M) /\ A.n e. (M...(m + 1))(F` n) e. RR) -> ((E.x e. RR A.k e. (M...m)(F` k) < x /\ (F` (m + 1)) e. RR) -> E.x e. RR A.k e. (M...(m + 1))(F` k) < x))
113	112	adantrl 430	. . . . . 6 |- ((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 /\ (F` (m + 1)) e. RR) -> E.x e. RR A.k e. (M...(m + 1))(F` k) < x))
114	49, 57, 113	mp2and 767	. . . . 5 |- ((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 + 1))(F` k) < x)
115	114	exp32 408	. . . 4 |- (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 + 1))(F` k) < x)))
116	5, 10, 15, 20, 40, 115	uzind4 7619	. . 3 |- (N e. (ZZ>=` M) -> (A.n e. (M...N)(F` n) e. RR -> E.x e. RR A.k e. (M...N)(F` k) < x))
117	116	imp 377	. 2 |- ((N e. (ZZ>=` M) /\ A.n e. (M...N)(F` n) e. RR) -> E.x e. RR A.k e. (M...N)(F` k) < x)
118		fveq2 4681	. . . 4 |- (k = n -> (F` k) = (F` n))
119	118	eleq1d 1963	. . 3 |- (k = n -> ((F` k) e. RR <-> (F` n) e. RR))
120	119	cbvralv 2280	. 2 |- (A.k e. (M...N)(F` k) e. RR <-> A.n e. (M...N)(F` n) e. RR)
121	117, 120	sylan2b 501	1 |- ((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)

Syntax hints:   -> wi 3   <-> wb 163   \/ wo 239   /\ wa 240   = wceq 1298   e. wcel 1300  A.wral 2105  E.wrex 2106   C_ wss 2593  ifcif 2982   class class class wbr 3338  ` cfv 3998  (class class class)co 4884  RRcr 6385  1c1 6387   + caddc 6389   <_ cle 6448  ZZcz 6451   < clt 6653  ZZ>=cuz 7586  ...cfz 7637

This theorem is referenced by:  fsequb2 7703

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-n0 7309  df-z 7345  df-uz 7587  df-fz 7638

Copyright terms: Public domain