Theorem infcvglem1 7221

Description: Lemma for infcvg 7224. Use ac6s 4756 to show the existence of a sequence f with values extracted from R.

Hypotheses

Ref	Expression
infcvg.1	|- R = {x | E.y e. X x = -uA}
infcvg.2	|- (y e. X -> A e. RR)
infcvg.3	|- Z e. X
infcvg.4	|- E.z e. RR A.w e. R w <_ z
infcvg.5b	|- S = -usup(R, RR, < )
infcvg.14	|- (y = (f` k) -> A = B)

Assertion

Ref	Expression
infcvglem1	|- E.f(f:NN-->X /\ A.k e. NN B < (S + (1 / k)))

Distinct variable groups:   x,f,A   x,y,B   z,w,R   f,k,S,y   f,X   x,k,y,X   x,Z,y   y,S

Proof of Theorem infcvglem1

Step	Hyp	Ref	Expression
1		nnex 5933	. . 3 |- NN e. V
2		infcvg.14	. . . 4 |- (y = (f` k) -> A = B)
3	2	breq1d 2629	. . 3 |- (y = (f` k) -> (A < (S + (1 / k)) <-> B < (S + (1 / k))))
4	1, 3	ac6s 4756	. 2 |- (A.k e. NN E.y e. X A < (S + (1 / k)) -> E.f(f:NN-->X /\ A.k e. NN B < (S + (1 / k))))
5		infcvg.1	. . . . . . 7 |- R = {x | E.y e. X x = -uA}
6		infcvg.2	. . . . . . 7 |- (y e. X -> A e. RR)
7		infcvg.3	. . . . . . 7 |- Z e. X
8		infcvg.4	. . . . . . 7 |- E.z e. RR A.w e. R w <_ z
9	5, 6, 7, 8	infcvgaux1 7219	. . . . . 6 |- (R (_ RR /\ R =/= (/) /\ E.z e. RR A.w e. R w <_ z)
10	9	suprlubi 6063	. . . . 5 |- ((-u(S + (1 / k)) e. RR /\ -u(S + (1 / k)) < sup(R, RR, < )) -> E.v e. R -u(S + (1 / k)) < v)
11		nnrecret 5952	. . . . . . 7 |- (k e. NN -> (1 / k) e. RR)
12		infcvg.5b	. . . . . . . . 9 |- S = -usup(R, RR, < )
13	9	suprcli 6061	. . . . . . . . . 10 |- sup(R, RR, < ) e. RR
14	13	renegcl 5416	. . . . . . . . 9 |- -usup(R, RR, < ) e. RR
15	12, 14	eqeltr 1544	. . . . . . . 8 |- S e. RR
16		axaddrcl 5272	. . . . . . . 8 |- ((S e. RR /\ (1 / k) e. RR) -> (S + (1 / k)) e. RR)
17	15, 16	mpan 695	. . . . . . 7 |- ((1 / k) e. RR -> (S + (1 / k)) e. RR)
18	11, 17	syl 10	. . . . . 6 |- (k e. NN -> (S + (1 / k)) e. RR)
19		renegclt 5437	. . . . . 6 |- ((S + (1 / k)) e. RR -> -u(S + (1 / k)) e. RR)
20	18, 19	syl 10	. . . . 5 |- (k e. NN -> -u(S + (1 / k)) e. RR)
21		nnrecgt0t 5953	. . . . . . . 8 |- (k e. NN -> 0 < (1 / k))
22		ltaddpost 5651	. . . . . . . . . 10 |- (((1 / k) e. RR /\ S e. RR) -> (0 < (1 / k) <-> S < (S + (1 / k))))
23	15, 22	mpan2 696	. . . . . . . . 9 |- ((1 / k) e. RR -> (0 < (1 / k) <-> S < (S + (1 / k))))
24	11, 23	syl 10	. . . . . . . 8 |- (k e. NN -> (0 < (1 / k) <-> S < (S + (1 / k))))
25	21, 24	mpbid 195	. . . . . . 7 |- (k e. NN -> S < (S + (1 / k)))
26		ltnegt 5655	. . . . . . . . 9 |- ((S e. RR /\ (S + (1 / k)) e. RR) -> (S < (S + (1 / k)) <-> -u(S + (1 / k)) < -uS))
27	15, 26	mpan 695	. . . . . . . 8 |- ((S + (1 / k)) e. RR -> (S < (S + (1 / k)) <-> -u(S + (1 / k)) < -uS))
28	18, 27	syl 10	. . . . . . 7 |- (k e. NN -> (S < (S + (1 / k)) <-> -u(S + (1 / k)) < -uS))
29	25, 28	mpbid 195	. . . . . 6 |- (k e. NN -> -u(S + (1 / k)) < -uS)
30	15	recn 5314	. . . . . . . 8 |- S e. CC
31	13	recn 5314	. . . . . . . 8 |- sup(R, RR, < ) e. CC
32	30, 31	negcon2 5408	. . . . . . 7 |- (S = -usup(R, RR, < ) <-> sup(R, RR, < ) = -uS)
33	12, 32	mpbi 189	. . . . . 6 |- sup(R, RR, < ) = -uS
34	29, 33	syl6breqr 2655	. . . . 5 |- (k e. NN -> -u(S + (1 / k)) < sup(R, RR, < ))
35	10, 20, 34	sylanc 471	. . . 4 |- (k e. NN -> E.v e. R -u(S + (1 / k)) < v)
36		visset 1813	. . . . . . . . . 10 |- v e. V
37		eqeq1 1481	. . . . . . . . . . 11 |- (x = v -> (x = -uA <-> v = -uA))
38	37	rexbidv 1664	. . . . . . . . . 10 |- (x = v -> (E.y e. X x = -uA <-> E.y e. X v = -uA))
39	36, 38, 5	elab2 1901	. . . . . . . . 9 |- (v e. R <-> E.y e. X v = -uA)
40	39	anbi1i 481	. . . . . . . 8 |- ((v e. R /\ -u(S + (1 / k)) < v) <-> (E.y e. X v = -uA /\ -u(S + (1 / k)) < v))
41		r19.41v 1763	. . . . . . . 8 |- (E.y e. X (v = -uA /\ -u(S + (1 / k)) < v) <-> (E.y e. X v = -uA /\ -u(S + (1 / k)) < v))
42		breq2 2623	. . . . . . . . . 10 |- (v = -uA -> (-u(S + (1 / k)) < v <-> -u(S + (1 / k)) < -uA))
43	42	pm5.32i 645	. . . . . . . . 9 |- ((v = -uA /\ -u(S + (1 / k)) < v) <-> (v = -uA /\ -u(S + (1 / k)) < -uA))
44	43	rexbii 1668	. . . . . . . 8 |- (E.y e. X (v = -uA /\ -u(S + (1 / k)) < v) <-> E.y e. X (v = -uA /\ -u(S + (1 / k)) < -uA))
45	40, 41, 44	3bitr2 179	. . . . . . 7 |- ((v e. R /\ -u(S + (1 / k)) < v) <-> E.y e. X (v = -uA /\ -u(S + (1 / k)) < -uA))
46	45	exbii 1051	. . . . . 6 |- (E.v(v e. R /\ -u(S + (1 / k)) < v) <-> E.vE.y e. X (v = -uA /\ -u(S + (1 / k)) < -uA))
47		df-rex 1650	. . . . . 6 |- (E.v e. R -u(S + (1 / k)) < v <-> E.v(v e. R /\ -u(S + (1 / k)) < v))
48		rexcom4 1824	. . . . . 6 |- (E.y e. X E.v(v = -uA /\ -u(S + (1 / k)) < -uA) <-> E.vE.y e. X (v = -uA /\ -u(S + (1 / k)) < -uA))
49	46, 47, 48	3bitr4 183	. . . . 5 |- (E.v e. R -u(S + (1 / k)) < v <-> E.y e. X E.v(v = -uA /\ -u(S + (1 / k)) < -uA))
50		negex 5365	. . . . . . . . 9 |- -uA e. V
51	50	isseti 1815	. . . . . . . 8 |- E.v v = -uA
52	51	biantrur 725	. . . . . . 7 |- (-u(S + (1 / k)) < -uA <-> (E.v v = -uA /\ -u(S + (1 / k)) < -uA))
53		19.41v 1305	. . . . . . 7 |- (E.v(v = -uA /\ -u(S + (1 / k)) < -uA) <-> (E.v v = -uA /\ -u(S + (1 / k)) < -uA))
54	52, 53	bitr4 176	. . . . . 6 |- (-u(S + (1 / k)) < -uA <-> E.v(v = -uA /\ -u(S + (1 / k)) < -uA))
55	54	rexbii 1668	. . . . 5 |- (E.y e. X -u(S + (1 / k)) < -uA <-> E.y e. X E.v(v = -uA /\ -u(S + (1 / k)) < -uA))
56	49, 55	bitr4 176	. . . 4 |- (E.v e. R -u(S + (1 / k)) < v <-> E.y e. X -u(S + (1 / k)) < -uA)
57	35, 56	sylib 198	. . 3 |- (k e. NN -> E.y e. X -u(S + (1 / k)) < -uA)
58		ltnegt 5655	. . . . . 6 |- ((A e. RR /\ (S + (1 / k)) e. RR) -> (A < (S + (1 / k)) <-> -u(S + (1 / k)) < -uA))
59	58, 6, 18	syl2an 454	. . . . 5 |- ((y e. X /\ k e. NN) -> (A < (S + (1 / k)) <-> -u(S + (1 / k)) < -uA))
60	59	ancoms 436	. . . 4 |- ((k e. NN /\ y e. X) -> (A < (S + (1 / k)) <-> -u(S + (1 / k)) < -uA))
61	60	rexbidva 1660	. . 3 |- (k e. NN -> (E.y e. X A < (S + (1 / k)) <-> E.y e. X -u(S + (1 / k)) < -uA))
62	57, 61	mpbird 196	. 2 |- (k e. NN -> E.y e. X A < (S + (1 / k)))
63	4, 62	mprg 1700	1 |- E.f(f:NN-->X /\ A.k e. NN B < (S + (1 / k)))

Syntax hints:   -> wi 3   <-> wb 146   /\ wa 223   = wceq 956   e. wcel 958  E.wex 980  {cab 1463  A.wral 1645  E.wrex 1646   class class class wbr 2619  -->wf 3178  ` cfv 3182  (class class class)co 3963  supcsup 4573  RRcr 5233  0cc0 5234  1c1 5235   + caddc 5237  -ucneg 5293   / cdiv 5294   <_ cle 5295  NNcn 5296   < clt 5486

This theorem is referenced by:  infcvglem3 7223

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-9 965  ax-10 966  ax-11 967  ax-12 968  ax-13 969  ax-14 970  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459  ax-rep 2693  ax-sep 2703  ax-nul 2710  ax-pow