Theorem infcvglem1 7164

Description: Lemma for infcvg 7167. Use ac6s 4736 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 5889	. . 3 |- NN e. V
2		infcvg.14	. . . 4 |- (y = (f` k) -> A = B)
3	2	breq1d 2624	. . 3 |- (y = (f` k) -> (A < (S + (1 / k)) <-> B < (S + (1 / k))))
4	1, 3	ac6s 4736	. 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 7162	. . . . . 6 |- (R (_ RR /\ R =/= (/) /\ E.z e. RR A.w e. R w <_ z)
10	9	suprlubi 6018	. . . . 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 6223	. . . . . . 7 |- (k e. NN -> (1 / k) e. RR)
12		infcvg.5b	. . . . . . . . 9 |- S = -usup(R, RR, < )
13	9	suprcli 6016	. . . . . . . . . 10 |- sup(R, RR, < ) e. RR
14	13	renegcl 5396	. . . . . . . . 9 |- -usup(R, RR, < ) e. RR
15	12, 14	eqeltr 1541	. . . . . . . 8 |- S e. RR
16		axaddrcl 5252	. . . . . . . 8 |- ((S e. RR /\ (1 / k) e. RR) -> (S + (1 / k)) e. RR)
17	15, 16	mpan 694	. . . . . . 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 5417	. . . . . 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 5908	. . . . . . . 8 |- (k e. NN -> 0 < (1 / k))
22		ltaddpost 5632	. . . . . . . . . 10 |- (((1 / k) e. RR /\ S e. RR) -> (0 < (1 / k) <-> S < (S + (1 / k))))
23	15, 22	mpan2 695	. . . . . . . . 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 5636	. . . . . . . . 9 |- ((S e. RR /\ (S + (1 / k)) e. RR) -> (S < (S + (1 / k)) <-> -u(S + (1 / k)) < -uS))
27	15, 26	mpan 694	. . . . . . . 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 5294	. . . . . . . 8 |- S e. CC
31	13	recn 5294	. . . . . . . 8 |- sup(R, RR, < ) e. CC
32	30, 31	negcon2 5388	. . . . . . 7 |- (S = -usup(R, RR, < ) <-> sup(R, RR, < ) = -uS)
33	12, 32	mpbi 189	. . . . . 6 |- sup(R, RR, < ) = -uS
34	29, 33	syl6breqr 2650	. . . . 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 1809	. . . . . . . . . 10 |- v e. V
37		eqeq1 1478	. . . . . . . . . . 11 |- (x = v -> (x = -uA <-> v = -uA))
38	37	rexbidv 1661	. . . . . . . . . 10 |- (x = v -> (E.y e. X x = -uA <-> E.y e. X v = -uA))
39	36, 38, 5	elab2 1897	. . . . . . . . 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 1760	. . . . . . . 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 2618	. . . . . . . . . 10 |- (v = -uA -> (-u(S + (1 / k)) < v <-> -u(S + (1 / k)) < -uA))
43	42	pm5.32i 644	. . . . . . . . 9 |- ((v = -uA /\ -u(S + (1 / k)) < v) <-> (v = -uA /\ -u(S + (1 / k)) < -uA))
44	43	rexbii 1665	. . . . . . . 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 1049	. . . . . 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 1647	. . . . . 6 |- (E.v e. R -u(S + (1 / k)) < v <-> E.v(v e. R /\ -u(S + (1 / k)) < v))
48		rexcom4 1820	. . . . . 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 5345	. . . . . . . . 9 |- -uA e. V
51	50	isseti 1811	. . . . . . . 8 |- E.v v = -uA
52	51	biantrur 724	. . . . . . 7 |- (-u(S + (1 / k)) < -uA <-> (E.v v = -uA /\ -u(S + (1 / k)) < -uA))
53		19.41v 1303	. . . . . . 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 1665	. . . . 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 5636	. . . . . 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 1657	. . 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 1697	1 |- E.f(f:NN-->X /\ A.k e. NN B < (S + (1 / k)))

Syntax hints:   -> wi 3   <-> wb 146   /\ wa 223   = wceq 954   e. wcel 956  E.wex 978  {cab 1461  A.wral 1642  E.wrex 1643   class class class wbr 2614  -->wf 3173  ` cfv 3177  (class class class)co 3954  supcsup 4553  RRcr 5213  0cc0 5214  1c1 5215   + caddc 5217  -ucneg 5273   / cdiv 5274   <_ cle 5275  NNcn 5276   < clt 5466

This theorem is referenced by:  infcvglem3 7166

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-9 963  ax-10 964  ax-11 965  ax-12 966  ax-13 967  ax-14 968  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457  ax-rep 2688  ax-sep 2698  ax-nul 2705  ax-pow 2737