Theorem seq1bnd 6855

Description: An initial segment of an infinite sequence of complex numbers is bounded.

Hypothesis

Ref	Expression
seq1bnd.1	|- F:NN-->CC

Assertion

Ref	Expression
seq1bnd	|- (A e. NN -> E.x e. RR A.y e. NN (y <_ A -> (abs` (F` y)) < x))

Distinct variable groups:   x,y,A   x,F,y

Proof of Theorem seq1bnd

Step	Hyp	Ref	Expression
1		breq2 2618	. . . 4 |- (z = 1 -> (y <_ z <-> y <_ 1))
2	1	imbi1d 612	. . 3 |- (z = 1 -> ((y <_ z -> (abs` (F` y)) < x) <-> (y <_ 1 -> (abs` (F` y)) < x)))
3	2	rexralbidv 1679	. 2 |- (z = 1 -> (E.x e. RR A.y e. NN (y <_ z -> (abs` (F` y)) < x) <-> E.x e. RR A.y e. NN (y <_ 1 -> (abs` (F` y)) < x)))
4		breq2 2618	. . . 4 |- (z = w -> (y <_ z <-> y <_ w))
5	4	imbi1d 612	. . 3 |- (z = w -> ((y <_ z -> (abs` (F` y)) < x) <-> (y <_ w -> (abs` (F` y)) < x)))
6	5	rexralbidv 1679	. 2 |- (z = w -> (E.x e. RR A.y e. NN (y <_ z -> (abs` (F` y)) < x) <-> E.x e. RR A.y e. NN (y <_ w -> (abs` (F` y)) < x)))
7		breq2 2618	. . . 4 |- (z = (w + 1) -> (y <_ z <-> y <_ (w + 1)))
8	7	imbi1d 612	. . 3 |- (z = (w + 1) -> ((y <_ z -> (abs` (F` y)) < x) <-> (y <_ (w + 1) -> (abs` (F` y)) < x)))
9	8	rexralbidv 1679	. 2 |- (z = (w + 1) -> (E.x e. RR A.y e. NN (y <_ z -> (abs` (F` y)) < x) <-> E.x e. RR A.y e. NN (y <_ (w + 1) -> (abs` (F` y)) < x)))
10		breq2 2618	. . . 4 |- (z = A -> (y <_ z <-> y <_ A))
11	10	imbi1d 612	. . 3 |- (z = A -> ((y <_ z -> (abs` (F` y)) < x) <-> (y <_ A -> (abs` (F` y)) < x)))
12	11	rexralbidv 1679	. 2 |- (z = A -> (E.x e. RR A.y e. NN (y <_ z -> (abs` (F` y)) < x) <-> E.x e. RR A.y e. NN (y <_ A -> (abs` (F` y)) < x)))
13		seq1bnd.1	. . . . . 6 |- F:NN-->CC
14		1nn 5890	. . . . . 6 |- 1 e. NN
15		ffvelrn 3805	. . . . . 6 |- ((F:NN-->CC /\ 1 e. NN) -> (F` 1) e. CC)
16	13, 14, 15	mp2an 696	. . . . 5 |- (F` 1) e. CC
17	16	abscl 6782	. . . 4 |- (abs` (F` 1)) e. RR
18		1re 5415	. . . 4 |- 1 e. RR
19	17, 18	readdcl 5314	. . 3 |- ((abs` (F` 1)) + 1) e. RR
20		nnle1eq1t 5901	. . . . 5 |- (y e. NN -> (y <_ 1 <-> y = 1))
21		fveq2 3715	. . . . . . 7 |- (y = 1 -> (F` y) = (F` 1))
22	21	fveq2d 3719	. . . . . 6 |- (y = 1 -> (abs` (F` y)) = (abs` (F` 1)))
23	17	ltp1 5777	. . . . . 6 |- (abs` (F` 1)) < ((abs` (F` 1)) + 1)
24	22, 23	syl6eqbr 2647	. . . . 5 |- (y = 1 -> (abs` (F` y)) < ((abs` (F` 1)) + 1))
25	20, 24	syl6bi 214	. . . 4 |- (y e. NN -> (y <_ 1 -> (abs` (F` y)) < ((abs` (F` 1)) + 1)))
26	25	rgen 1695	. . 3 |- A.y e. NN (y <_ 1 -> (abs` (F` y)) < ((abs` (F` 1)) + 1))
27		breq2 2618	. . . . . 6 |- (x = ((abs` (F` 1)) + 1) -> ((abs` (F` y)) < x <-> (abs` (F` y)) < ((abs` (F` 1)) + 1)))
28	27	imbi2d 611	. . . . 5 |- (x = ((abs` (F` 1)) + 1) -> ((y <_ 1 -> (abs` (F` y)) < x) <-> (y <_ 1 -> (abs` (F` y)) < ((abs` (F` 1)) + 1))))
29	28	ralbidv 1660	. . . 4 |- (x = ((abs` (F` 1)) + 1) -> (A.y e. NN (y <_ 1 -> (abs` (F` y)) < x) <-> A.y e. NN (y <_ 1 -> (abs` (F` y)) < ((abs` (F` 1)) + 1))))
30	29	rcla4ev 1873	. . 3 |- ((((abs` (F` 1)) + 1) e. RR /\ A.y e. NN (y <_ 1 -> (abs` (F` y)) < ((abs` (F` 1)) + 1))) -> E.x e. RR A.y e. NN (y <_ 1 -> (abs` (F` y)) < x))
31	19, 26, 30	mp2an 696	. 2 |- E.x e. RR A.y e. NN (y <_ 1 -> (abs` (F` y)) < x)
32		leloet 5499	. . . . . . . . . . . . . 14 |- ((y e. RR /\ (w + 1) e. RR) -> (y <_ (w + 1) <-> (y < (w + 1) \/ y = (w + 1))))
33		nnret 5885	. . . . . . . . . . . . . 14 |- (y e. NN -> y e. RR)
34		peano2nn 5891	. . . . . . . . . . . . . . 15 |- (w e. NN -> (w + 1) e. NN)
35		nnret 5885	. . . . . . . . . . . . . . 15 |- ((w + 1) e. NN -> (w + 1) e. RR)
36	34, 35	syl 10	. . . . . . . . . . . . . 14 |- (w e. NN -> (w + 1) e. RR)
37	32, 33, 36	syl2an 454	. . . . . . . . . . . . 13 |- ((y e. NN /\ w e. NN) -> (y <_ (w + 1) <-> (y < (w + 1) \/ y = (w + 1))))
38		nnleltp1t 5909	. . . . . . . . . . . . . 14 |- ((y e. NN /\ w e. NN) -> (y <_ w <-> y < (w + 1)))
39	38	orbi1d 614	. . . . . . . . . . . . 13 |- ((y e. NN /\ w e. NN) -> ((y <_ w \/ y = (w + 1)) <-> (y < (w + 1) \/ y = (w + 1))))
40	37, 39	bitr4d 530	. . . . . . . . . . . 12 |- ((y e. NN /\ w e. NN) -> (y <_ (w + 1) <-> (y <_ w \/ y = (w + 1))))
41	40	ancoms 436	. . . . . . . . . . 11 |- ((w e. NN /\ y e. NN) -> (y <_ (w + 1) <-> (y <_ w \/ y = (w + 1))))
42	41	adantlr 393	. . . . . . . . . 10 |- (((w e. NN /\ z e. RR) /\ y e. NN) -> (y <_ (w + 1) <-> (y <_ w \/ y = (w + 1))))
43	42	adantr 389	. . . . . . . . 9 |- ((((w e. NN /\ z e. RR) /\ y e. NN) /\ (y <_ w -> (abs` (F` y)) < z)) -> (y <_ (w + 1) <-> (y <_ w \/ y = (w + 1))))
44		max1ALT 5872	. . . . . . . . . . . . . 14 |- (z e. RR -> z <_ if(z <_ ((abs` (F` (w + 1))) + 1), ((abs` (F` (w + 1))) + 1), z))
45	44	ad2antlr 405	. . . . . . . . . . . . 13 |- (((w e. NN /\ z e. RR) /\ y e. NN) -> z <_ if(z <_ ((abs` (F` (w + 1))) + 1), ((abs` (F` (w + 1))) + 1), z))
46		ltletrt 5505	. . . . . . . . . . . . . 14 |- (((abs` (F` y)) e. RR /\ z e. RR /\ if(z <_ ((abs` (F` (w + 1))) + 1), ((abs` (F` (w + 1))) + 1), z) e. RR) -> (((abs` (F` y)) < z /\ z <_ if(z <_ ((abs` (F` (w + 1))) + 1), ((abs` (F` (w + 1))) + 1), z)) -> (abs` (F` y)) < if(z <_ ((abs` (F` (w + 1))) + 1), ((abs` (F` (w + 1))) + 1), z)))
47	13	ffvelrni 3806	. . . . . . . . . . . . . . . 16 |- (y e. NN -> (F` y) e. CC)
48		absclt 6776	. . . . . . . . . . . . . . . 16 |- ((F` y) e. CC -> (abs` (F` y)) e. RR)
49	47, 48	syl 10	. . . . . . . . . . . . . . 15 |- (y e. NN -> (abs` (F` y)) e. RR)
50	49	adantl 388	. . . . . . . . . . . . . 14 |- (((w e. NN /\ z e. RR) /\ y e. NN) -> (abs` (F` y)) e. RR)
51		simplr 413	. . . . . . . . . . . . . 14 |- (((w e. NN /\ z e. RR) /\ y e. NN) -> z e. RR)
52		ifcl 2376	. . . . . . . . . . . . . . . 16 |- ((((abs` (F` (w + 1))) + 1) e. RR /\ z e. RR) -> if(z <_ ((abs` (F` (w + 1))) + 1), ((abs` (F` (w + 1))) + 1), z) e. RR)
53	13	ffvelrni 3806	. . . . . . . . . . . . . . . . . 18 |- ((w + 1) e. NN -> (F` (w + 1)) e. CC)
54	34, 53	syl 10	. . . . . . . . . . . . . . . . 17 |- (w e. NN -> (F` (w + 1)) e. CC)
55		absclt 6776	. . . . . . . . . . . . . . . . 17 |- ((F` (w + 1)) e. CC -> (abs` (F` (