Theorem climubi 7089

Description: The limit of a monotonic sequence is an upper bound.

Hypotheses

Ref	Expression
climub.1	|- A e. V
climub.2	|- F:NN-->RR
climub.3	|- (k e. NN -> (F` k) <_ (F` (k + 1)))
climub.4	|- F ~~> A
climubi.5	|- N e. NN

Assertion

Ref	Expression
climubi	|- (F` N) <_ A

Distinct variable group:   k,F

Proof of Theorem climubi

Step	Hyp	Ref	Expression
1		breq2 2613	. . . . . . . . . 10 |- (j = (N + m) -> (m <_ j <-> m <_ (N + m)))
2		fveq2 3709	. . . . . . . . . . . . 13 |- (j = (N + m) -> (F` j) = (F` (N + m)))
3	2	opreq1d 3960	. . . . . . . . . . . 12 |- (j = (N + m) -> ((F` j) - A) = ((F` (N + m)) - A))
4	3	fveq2d 3713	. . . . . . . . . . 11 |- (j = (N + m) -> (abs` ((F` j) - A)) = (abs` ((F` (N + m)) - A)))
5	4	breq1d 2619	. . . . . . . . . 10 |- (j = (N + m) -> ((abs` ((F` j) - A)) < ((F` N) - A) <-> (abs` ((F` (N + m)) - A)) < ((F` N) - A)))
6	1, 5	imbi12d 624	. . . . . . . . 9 |- (j = (N + m) -> ((m <_ j -> (abs` ((F` j) - A)) < ((F` N) - A)) <-> (m <_ (N + m) -> (abs` ((F` (N + m)) - A)) < ((F` N) - A))))
7	6	negbid 609	. . . . . . . 8 |- (j = (N + m) -> (-. (m <_ j -> (abs` ((F` j) - A)) < ((F` N) - A)) <-> -. (m <_ (N + m) -> (abs` ((F` (N + m)) - A)) < ((F` N) - A))))
8	7	rcla4ev 1868	. . . . . . 7 |- (((N + m) e. NN /\ -. (m <_ (N + m) -> (abs` ((F` (N + m)) - A)) < ((F` N) - A))) -> E.j e. NN -. (m <_ j -> (abs` ((F` j) - A)) < ((F` N) - A)))
9		climubi.5	. . . . . . . 8 |- N e. NN
10		nnaddclt 5888	. . . . . . . 8 |- ((N e. NN /\ m e. NN) -> (N + m) e. NN)
11	9, 10	mpan 693	. . . . . . 7 |- (m e. NN -> (N + m) e. NN)
12		nnret 5877	. . . . . . . . . 10 |- (m e. NN -> m e. RR)
13	9	nnnn0 6054	. . . . . . . . . . 11 |- N e. NN0
14		nn0addge2t 6078	. . . . . . . . . . 11 |- ((m e. RR /\ N e. NN0) -> m <_ (N + m))
15	13, 14	mpan2 694	. . . . . . . . . 10 |- (m e. RR -> m <_ (N + m))
16	12, 15	syl 10	. . . . . . . . 9 |- (m e. NN -> m <_ (N + m))
17		climub.2	. . . . . . . . . . . . . 14 |- F:NN-->RR
18		ffvelrn 3799	. . . . . . . . . . . . . 14 |- ((F:NN-->RR /\ N e. NN) -> (F` N) e. RR)
19	17, 9, 18	mp2an 695	. . . . . . . . . . . . 13 |- (F` N) e. RR
20		climub.1	. . . . . . . . . . . . . 14 |- A e. V
21		climub.4	. . . . . . . . . . . . . 14 |- F ~~> A
22	20, 17, 21	climfnrcl 7048	. . . . . . . . . . . . 13 |- A e. RR
23	19, 22	resubcl 5411	. . . . . . . . . . . 12 |- ((F` N) - A) e. RR
24		letrt 5498	. . . . . . . . . . . 12 |- ((((F` N) - A) e. RR /\ ((F` (N + m)) - A) e. RR /\ (abs` ((F` (N + m)) - A)) e. RR) -> ((((F` N) - A) <_ ((F` (N + m)) - A) /\ ((F` (N + m)) - A) <_ (abs` ((F` (N + m)) - A))) -> ((F` N) - A) <_ (abs` ((F` (N + m)) - A))))
25	23, 24	mp3an1 900	. . . . . . . . . . 11 |- ((((F` (N + m)) - A) e. RR /\ (abs` ((F` (N + m)) - A)) e. RR) -> ((((F` N) - A) <_ ((F` (N + m)) - A) /\ ((F` (N + m)) - A) <_ (abs` ((F` (N + m)) - A))) -> ((F` N) - A) <_ (abs` ((F` (N + m)) - A))))
26	17	ffvelrni 3800	. . . . . . . . . . . . . 14 |- ((N + m) e. NN -> (F` (N + m)) e. RR)
27	11, 26	syl 10	. . . . . . . . . . . . 13 |- (m e. NN -> (F` (N + m)) e. RR)
28		resubclt 5410	. . . . . . . . . . . . . 14 |- (((F` (N + m)) e. RR /\ A e. RR) -> ((F` (N + m)) - A) e. RR)
29	22, 28	mpan2 694	. . . . . . . . . . . . 13 |- ((F` (N + m)) e. RR -> ((F` (N + m)) - A) e. RR)
30	27, 29	syl 10	. . . . . . . . . . . 12 |- (m e. NN -> ((F` (N + m)) - A) e. RR)
31		recnt 5285	. . . . . . . . . . . . . 14 |- (((F` (N + m)) - A) e. RR -> ((F` (N + m)) - A) e. CC)
32	30, 31	syl 10	. . . . . . . . . . . . 13 |- (m e. NN -> ((F` (N + m)) - A) e. CC)
33		absclt 6768	. . . . . . . . . . . . 13 |- (((F` (N + m)) - A) e. CC -> (abs` ((F` (N + m)) - A)) e. RR)
34	32, 33	syl 10	. . . . . . . . . . . 12 |- (m e. NN -> (abs` ((F` (N + m)) - A)) e. RR)
35	30, 34	jca 288	. . . . . . . . . . 11 |- (m e. NN -> (((F` (N + m)) - A) e. RR /\ (abs` ((F` (N + m)) - A)) e. RR))
36		climub.3	. . . . . . . . . . . . . . . 16 |- (k e. NN -> (F` k) <_ (F` (k + 1)))
37	17, 36	monoord 6231	. . . . . . . . . . . . . . 15 |- ((N e. NN /\ (N + m) e. NN /\ N <_ (N + m)) -> (F` N) <_ (F` (N + m)))
38	9, 37	mp3an1 900	. . . . . . . . . . . . . 14 |- (((N + m) e. NN /\ N <_ (N + m)) -> (F` N) <_ (F` (N + m)))
39		nnnn0t 6053	. . . . . . . . . . . . . . 15 |- (m e. NN -> m e. NN0)
40	9	nnre 5879	. . . . . . . . . . . . . . . 16 |- N e. RR
41		nn0addge1t 6077	. . . . . . . . . . . . . . . 16 |- ((N e. RR /\ m e. NN0) -> N <_ (N + m))
42	40, 41	mpan 693	. . . . . . . . . . . . . . 15 |- (m e. NN0 -> N <_ (N + m))
43	39, 42	syl 10	. . . . . . . . . . . . . 14 |- (m e. NN -> N <_ (N + m))
44	38, 11, 43	sylanc 471	. . . . . . . . . . . . 13 |- (m e. NN -> (F` N) <_ (F` (N + m)))
45		lesub1t 5633	. . . . . . . . . . . . . . 15 |- (((F` N) e. RR /\ (F` (N + m)) e. RR /\ A e. RR) -> ((F` N) <_ (F` (N + m)) <-> ((F` N) - A) <_ ((F` (N + m)) - A)))
46	19, 22, 45	mp3an13 904	. . . . . . . . . . . . . 14 |- ((F` (N + m)) e. RR -> ((F` N) <_ (F` (N + m)) <-> ((F` N) - A) <_ ((F` (N + m)) - A)))
47	27, 46	syl 10	. . . . . . . . . . . . 13 |- (m e. NN -> ((F` N) <_ (F` (N + m)) <-> ((F` N) - A) <_ ((F` (N + m)) - A)))
48	44, 47	mpbid 195	. . . . . . . . . . . 12 |- (m e. NN -> ((F` N) - A) <_ ((F` (N + m)) - A))
49		leabst 6799	. . . . . . . . . . . . 13 |- (((F` (N + m)) - A) e. RR -> ((F` (N + m)) - A) <_ (abs` ((F` (N + m)) - A)))
50	30, 49	syl 10	. . . . . . . . . . . 12 |- (m e. NN -> ((F` (N + m)) - A) <_ (abs` ((F` (N + m)) - A)))
51	48, 50	jca 288	. . . . . . . . . . 11 |- (m e. NN -> (((F` N) - A) <_ ((F` (N + m)) - A) /\ ((F` (N + m)) - A) <_ (abs` ((F` (N + m)) - A))))
52	25, 35, 51	sylc 68	. . . . . . . . . 10 |- (m e. NN -> ((F` N) - A) <_ (abs` ((F` (N + m)) - A)))
53		lenltt 5482	. . . . . . . . . . . 12 |- ((((F` N) - A) e. RR /\ (abs` ((F` (N + m)) - A)) e. RR) -> (((F` N) - A) <_ (abs` ((F` (N + m)) - A)) <-> -. (abs` ((F` (N + m)) - A)) < ((F` N) - A)))
54	23, 53	mpan 693	. . . . . . . . . . 11 |- ((abs` ((F` (N + m)) - A)) e. RR -> (((F` N) - A) <_ (abs` ((F` (N + m)) - A)) <-> -. (abs` ((F` (N + m)) - A)) < ((F` N) - A)))
55	34, 54	syl 10	. . . . . . . . . 10 |- (m e. NN -> (((F` N) - A) <_ (abs` ((F` (N + m)) - A)) <-> -. (abs` ((F` (N + m)) - A)) < ((F` N) - A)))
56	52, 55	mpbid 195	. . . . . . . . 9 |- (m