Theorem seq1ublem 6911

Description: Lemma for seq1ub 6912.

Hypothesis

Ref	Expression
seq1ub.1	|- F:NN-->RR

Assertion

Ref	Expression
seq1ublem	|- (B e. NN -> (ran ( F |` {x e. NN | x <_ B}) (_ RR /\ ran ( F |` {x e. NN | x <_ B}) =/= (/) /\ E.y e. RR A.z e. ran ( F |` {x e. NN | x <_ B})z <_ y))

Distinct variable groups:   x,y,z,B   y,F,z

Proof of Theorem seq1ublem

Step	Hyp	Ref	Expression
1		seq1ub.1	. . . . 5 |- F:NN-->RR
2		ssrab2 2134	. . . . 5 |- {x e. NN | x <_ B} (_ NN
3		fssres 3649	. . . . 5 |- ((F:NN-->RR /\ {x e. NN | x <_ B} (_ NN) -> (F |` {x e. NN | x <_ B}):{x e. NN | x <_ B}-->RR)
4	1, 2, 3	mp2an 699	. . . 4 |- (F |` {x e. NN | x <_ B}):{x e. NN | x <_ B}-->RR
5		frn 3639	. . . 4 |- ((F |` {x e. NN | x <_ B}):{x e. NN | x <_ B}-->RR -> ran ( F |` {x e. NN | x <_ B}) (_ RR)
6	4, 5	ax-mp 7	. . 3 |- ran ( F |` {x e. NN | x <_ B}) (_ RR
7	6	a1i 8	. 2 |- (B e. NN -> ran ( F |` {x e. NN | x <_ B}) (_ RR)
8		nnge1t 5945	. . . . . . 7 |- (B e. NN -> 1 <_ B)
9		1nn 5936	. . . . . . 7 |- 1 e. NN
10	8, 9	jctil 292	. . . . . 6 |- (B e. NN -> (1 e. NN /\ 1 <_ B))
11		breq1 2627	. . . . . . 7 |- (x = 1 -> (x <_ B <-> 1 <_ B))
12	11	elrab 1908	. . . . . 6 |- (1 e. {x e. NN | x <_ B} <-> (1 e. NN /\ 1 <_ B))
13	10, 12	sylibr 200	. . . . 5 |- (B e. NN -> 1 e. {x e. NN | x <_ B})
14		ffn 3633	. . . . . . 7 |- (F:NN-->RR -> F Fn NN)
15	1, 14	ax-mp 7	. . . . . 6 |- F Fn NN
16		fnssres 3606	. . . . . 6 |- ((F Fn NN /\ {x e. NN | x <_ B} (_ NN) -> (F |` {x e. NN | x <_ B}) Fn {x e. NN | x <_ B})
17	15, 2, 16	mp2an 699	. . . . 5 |- (F |` {x e. NN | x <_ B}) Fn {x e. NN | x <_ B}
18	13, 17	jctil 292	. . . 4 |- (B e. NN -> ((F |` {x e. NN | x <_ B}) Fn {x e. NN | x <_ B} /\ 1 e. {x e. NN | x <_ B}))
19		fnfvelrn 3819	. . . 4 |- (((F |` {x e. NN | x <_ B}) Fn {x e. NN | x <_ B} /\ 1 e. {x e. NN | x <_ B}) -> ((F |` {x e. NN | x <_ B})` 1) e. ran ( F |` {x e. NN | x <_ B}))
20	18, 19	syl 10	. . 3 |- (B e. NN -> ((F |` {x e. NN | x <_ B})` 1) e. ran ( F |` {x e. NN | x <_ B}))
21		ne0i 2289	. . 3 |- (((F |` {x e. NN | x <_ B})` 1) e. ran ( F |` {x e. NN | x <_ B}) -> ran ( F |` {x e. NN | x <_ B}) =/= (/))
22	20, 21	syl 10	. 2 |- (B e. NN -> ran ( F |` {x e. NN | x <_ B}) =/= (/))
23		axresscn 5280	. . . . 5 |- RR (_ CC
24		fss 3641	. . . . 5 |- ((F:NN-->RR /\ RR (_ CC) -> F:NN-->CC)
25	1, 23, 24	mp2an 699	. . . 4 |- F:NN-->CC
26	25	seq1bnd 6910	. . 3 |- (B e. NN -> E.y e. RR A.w e. NN (w <_ B -> (abs` (F` w)) < y))
27		breq1 2627	. . . . . . . . . . . . . . . 16 |- (w = v -> (w <_ B <-> v <_ B))
28		fveq2 3730	. . . . . . . . . . . . . . . . . 18 |- (w = v -> (F` w) = (F` v))
29	28	fveq2d 3734	. . . . . . . . . . . . . . . . 17 |- (w = v -> (abs` (F` w)) = (abs` (F` v)))
30	29	breq1d 2634	. . . . . . . . . . . . . . . 16 |- (w = v -> ((abs` (F` w)) < y <-> (abs` (F` v)) < y))
31	27, 30	imbi12d 628	. . . . . . . . . . . . . . 15 |- (w = v -> ((w <_ B -> (abs` (F` w)) < y) <-> (v <_ B -> (abs` (F` v)) < y)))
32	31	rcla4cv 1877	. . . . . . . . . . . . . 14 |- (A.w e. NN (w <_ B -> (abs` (F` w)) < y) -> (v e. NN -> (v <_ B -> (abs` (F` v)) < y)))
33	32	imp32 363	. . . . . . . . . . . . 13 |- ((A.w e. NN (w <_ B -> (abs` (F` w)) < y) /\ (v e. NN /\ v <_ B)) -> (abs` (F` v)) < y)
34	33	adantll 394	. . . . . . . . . . . 12 |- (((y e. RR /\ A.w e. NN (w <_ B -> (abs` (F` w)) < y)) /\ (v e. NN /\ v <_ B)) -> (abs` (F` v)) < y)
35	34	adantr 391	. . . . . . . . . . 11 |- ((((y e. RR /\ A.w e. NN (w <_ B -> (abs` (F` w)) < y)) /\ (v e. NN /\ v <_ B)) /\ ((F |` {x e. NN | x <_ B})` v) = z) -> (abs` (F` v)) < y)
36		leabst 6864	. . . . . . . . . . . . . . . . . . . 20 |- ((F` v) e. RR -> (F` v) <_ (abs` (F` v)))
37	36	adantr 391	. . . . . . . . . . . . . . . . . . 19 |- (((F` v) e. RR /\ y e. RR) -> (F` v) <_ (abs` (F` v)))
38		lelttrt 5535	. . . . . . . . . . . . . . . . . . . . 21 |- (((F` v) e. RR /\ (abs` (F` v)) e. RR /\ y e. RR) -> (((F` v) <_ (abs` (F` v)) /\ (abs` (F` v)) < y) -> (F` v) < y))
39	38	3expa 835	. . . . . . . . . . . . . . . . . . . 20 |- ((((F` v) e. RR /\ (abs` (F` v)) e. RR) /\ y e. RR) -> (((F` v) <_ (abs` (F` v)) /\ (abs` (F` v)) < y) -> (F` v) < y))
40		recnt 5325	. . . . . . . . . . . . . . . . . . . . . 22 |- ((F` v) e. RR -> (F` v) e. CC)
41		absclt 6833	. . . . . . . . . . . . . . . . . . . . . 22 |- ((F` v) e. CC -> (abs` (F` v)) e. RR)
42	40, 41	syl 10	. . . . . . . . . . . . . . . . . . . . 21 |- ((F` v) e. RR -> (abs` (F` v)) e. RR)
43	42	ancli 296	. . . . . . . . . . . . . . . . . . . 20 |- ((F` v) e. RR -> ((F` v) e. RR /\ (abs` (F` v)) e. RR))
44	39, 43	sylan 450	. . . . . . . . . . . . . . . . . . 19 |- (((F` v) e. RR /\ y e. RR) -> (((F` v) <_ (abs` (F` v)) /\ (abs` (F` v)) < y) -> (F` v) < y))
45	37, 44	mpand 703	. . . . . . . . . . . . . . . . . 18 |- (((F` v) e. RR /\ y e. RR) -> ((abs` (F` v)) < y -> (F` v) < y))
46		ltlet 5532	. . . . . . . . . . . . . . . . . 18 |- (((F` v) e. RR /\ y e. RR) -> ((F` v) < y -> (F` v) <_ y))
47	45, 46	syld 27	. . . . . . . . . . . . . . . . 17 |- (((F` v) e. RR /\ y e. RR) -> ((abs` (F` v)) < y -> (F` v) <_ y))
48	1	ffvelrni 3821	. . . . . . . . . . . . . . . . 17 |- (v e. NN -> (F` v) e. RR)
49	47, 48	sylan 450	. . . . . . . . . . . . . . . 16 |- ((v e. NN /\ y e. RR) -> ((abs` (F` v)) < y -> (F` v) <_ y))
50	49	ancoms 438	. . . . . . . . . . . . . . 15 |- ((y e. RR /\ v e. NN) -> ((abs` (F` v)) < y -> (F` v) <_ y))
51	50	adantrr 397	. . . . . . . . . . . . . 14 |- ((y e. RR /\ (v e. NN /\ v <_ B)) -> ((abs` (F` v)) < y -> (F` v) <_ y))
52		breq1 2627	. . . . . . . . . . . . . . . . . 18 |- (x = v -> (x <_ B <-> v <_ B))
53	52	elrab 1908	. . . . . . . . . . . . . . . . 17 |- (v e. {x e. NN | x <_ B} <-> (v e. NN /\ v <_ B))
54		fvres 3740	. . . . . . . . . . . . . . . . 17 |- (v e. {x e. NN | x <_ B} -> ((F |` {x e. NN | x <_ B})` v) = (F` v))
55	53, 54	sylbir 201	. . . . . . . . . . . . . . . 16 |- ((v e. NN /\ v <_ B) -> ((F |` {x e. NN | x <_ B})` v) = (F` v))
56	55	breq1d 2634	. . . . . . . . . . . . . . 15 |- ((v e. NN /\ v <_ B) -> (((F |` {x e. NN | x <_ B})` v) <_ y <-> (F` v) <_ y))
57	56	adantl 390	. . . . . . . . . . . . . 14 |- ((y e. RR /\ (v e. NN /\ v <_ B)) -> (((F |` {x e. NN | x <_ B})` v) <_ y <-> (F` v) <_ y))
58	51, 57	sylibrd 204	. . . . . . . . . . . . 13 |- ((y e. RR /\ (v e. NN /\ v <_ B)) -> ((abs` (F` v)) < y -> ((F |` {x e. NN | x <_ B})` v) <_ y))
59		breq1 2627	. . . . . . . . . . . . . 14 |- (((F |` {x e. NN | x <_ B})` v) = z -> (((F |` {x e. NN | x <_ B})` v) <_ y <-> z <_ y))
60	59	biimpd 153	. . . . . . . . . . . . 13 |- (((F |` {x e. NN | x <_ B})` v) =