HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem infcvglem1 7156
Description: Lemma for infcvg 7159. Use ac6s 4728 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
StepHypRef Expression
1 nnex 5881 . . 3 |- NN e. V
2 infcvg.14 . . . 4 |- (y = (f` k) -> A = B)
32breq1d 2619 . . 3 |- (y = (f` k) -> (A < (S + (1 / k)) <-> B < (S + (1 / k))))
41, 3ac6s 4728 . 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
95, 6, 7, 8infcvgaux1 7154 . . . . . 6 |- (R (_ RR /\ R =/= (/) /\ E.z e. RR A.w e. R w <_ z)
109suprlubi 6010 . . . . 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 6215 . . . . . . 7 |- (k e. NN -> (1 / k) e. RR)
12 infcvg.5b . . . . . . . . 9 |- S = -usup(R, RR, < )
139suprcli 6008 . . . . . . . . . 10 |- sup(R, RR, < ) e. RR
1413renegcl 5388 . . . . . . . . 9 |- -usup(R, RR, < ) e. RR
1512, 14eqeltr 1536 . . . . . . . 8 |- S e. RR
16 axaddrcl 5244 . . . . . . . 8 |- ((S e. RR /\ (1 / k) e. RR) -> (S + (1 / k)) e. RR)
1715, 16mpan 693 . . . . . . 7 |- ((1 / k) e. RR -> (S + (1 / k)) e. RR)
1811, 17syl 10 . . . . . 6 |- (k e. NN -> (S + (1 / k)) e. RR)
19 renegclt 5409 . . . . . 6 |- ((S + (1 / k)) e. RR -> -u(S + (1 / k)) e. RR)
2018, 19syl 10 . . . . 5 |- (k e. NN -> -u(S + (1 / k)) e. RR)
21 nnrecgt0t 5900 . . . . . . . 8 |- (k e. NN -> 0 < (1 / k))
22 ltaddpost 5624 . . . . . . . . . 10 |- (((1 / k) e. RR /\ S e. RR) -> (0 < (1 / k) <-> S < (S + (1 / k))))
2315, 22mpan2 694 . . . . . . . . 9 |- ((1 / k) e. RR -> (0 < (1 / k) <-> S < (S + (1 / k))))
2411, 23syl 10 . . . . . . . 8 |- (k e. NN -> (0 < (1 / k) <-> S < (S + (1 / k))))
2521, 24mpbid 195 . . . . . . 7 |- (k e. NN -> S < (S + (1 / k)))
26 ltnegt 5628 . . . . . . . . 9 |- ((S e. RR /\ (S + (1 / k)) e. RR) -> (S < (S + (1 / k)) <-> -u(S + (1 / k)) < -uS))
2715, 26mpan 693 . . . . . . . 8 |- ((S + (1 / k)) e. RR -> (S < (S + (1 / k)) <-> -u(S + (1 / k)) < -uS))
2818, 27syl 10 . . . . . . 7 |- (k e. NN -> (S < (S + (1 / k)) <-> -u(S + (1 / k)) < -uS))
2925, 28mpbid 195 . . . . . 6 |- (k e. NN -> -u(S + (1 / k)) < -uS)
3015recn 5286 . . . . . . . 8 |- S e. CC
3113recn 5286 . . . . . . . 8 |- sup(R, RR, < ) e. CC
3230, 31negcon2 5380 . . . . . . 7 |- (S = -usup(R, RR, < ) <-> sup(R, RR, < ) = -uS)
3312, 32mpbi 189 . . . . . 6 |- sup(R, RR, < ) = -uS
3429, 33syl6breqr 2645 . . . . 5 |- (k e. NN -> -u(S + (1 / k)) < sup(R, RR, < ))
3510, 20, 34sylanc 471 . . . 4 |- (k e. NN -> E.v e. R -u(S + (1 / k)) < v)
36 visset 1804 . . . . . . . . . 10 |- v e. V
37 eqeq1 1473 . . . . . . . . . . 11 |- (x = v -> (x = -uA <-> v = -uA))
3837rexbidv 1656 . . . . . . . . . 10 |- (x = v -> (E.y e. X x = -uA <-> E.y e. X v = -uA))
3936, 38, 5elab2 1892 . . . . . . . . 9 |- (v e. R <-> E.y e. X v = -uA)
4039anbi1i 480 . . . . . . . 8 |- ((v e. R /\ -u(S + (1 / k)) < v) <-> (E.y e. X v = -uA /\ -u(S + (1 / k)) < v))
41 r19.41v 1755 . . . . . . . 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 2613 . . . . . . . . . 10 |- (v = -uA -> (-u(S + (1 / k)) < v <-> -u(S + (1 / k)) < -uA))
4342pm5.32i 643 . . . . . . . . 9 |- ((v = -uA /\ -u(S + (1 / k)) < v) <-> (v = -uA /\ -u(S + (1 / k)) < -uA))
4443rexbii 1660 . . . . . . . 8 |- (E.y e. X (v = -uA /\ -u(S + (1 / k)) < v) <-> E.y e. X (v = -uA /\ -u(S + (1 / k)) < -uA))
4540, 41, 443bitr2 179 . . . . . . 7 |- ((v e. R /\ -u(S + (1 / k)) < v) <-> E.y e. X (v = -uA /\ -u(S + (1 / k)) < -uA))
4645exbii 1047 . . . . . 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 1642 . . . . . 6 |- (E.v e. R -u(S + (1 / k)) < v <-> E.v(v e. R /\ -u(S + (1 / k)) < v))
48 rexcom4 1815 . . . . . 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))
4946, 47, 483bitr4 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 5337 . . . . . . . . 9 |- -uA e. V
5150isseti 1806 . . . . . . . 8 |- E.v v = -uA
5251biantrur 723 . . . . . . 7 |- (-u(S + (1 / k)) < -uA <-> (E.v v = -uA /\ -u(S + (1 / k)) < -uA))
53 19.41v 1300 . . . . . . 7 |- (E.v(v = -uA /\ -u(S + (1 / k)) < -uA) <-> (E.v v = -uA /\ -u(S + (1 / k)) < -uA))
5452, 53bitr4 176 . . . . . 6 |- (-u(S + (1 / k)) < -uA <-> E.v(v = -uA /\ -u(S + (1 / k)) < -uA))
5554rexbii 1660 . . . . 5 |- (E.y e. X -u(S + (1 / k)) < -uA <-> E.y e. X E.v(v = -uA /\ -u(S + (1 / k)) < -uA))
5649, 55bitr4 176 . . . 4 |- (E.v e. R -u(S + (1 / k)) < v <-> E.y e. X -u(S + (1 / k)) < -uA)
5735, 56sylib 198 . . 3 |- (k e. NN -> E.y e. X -u(S + (1 / k)) < -uA)
58 ltnegt 5628 . . . . . 6 |- ((A e. RR /\ (S + (1 / k)) e. RR) -> (A < (S + (1 / k)) <-> -u(S + (1 / k)) < -uA))
5958, 6, 18syl2an 454 . . . . 5 |- ((y e. X /\ k e. NN) -> (A < (S + (1 / k)) <-> -u(S + (1 / k)) < -uA))
6059ancoms 436 . . . 4 |- ((k e. NN /\ y e. X) -> (A < (S + (1 / k)) <-> -u(S + (1 / k)) < -uA))
6160rexbidva 1652 . . 3 |- (k e. NN -> (E.y e. X A < (S + (1 / k)) <-> E.y e. X -u(S + (1 / k)) < -uA))
6257, 61mpbird 196 . 2 |- (k e. NN -> E.y e. X A < (S + (1 / k)))
634, 62mprg 1692 1 |- E.f(f:NN-->X /\ A.k e. NN B < (S + (1 / k)))
Colors of variables: wff set class
Syntax hints:   -> wi 3   <-> wb 146   /\ wa 223   = wceq 953   e. wcel 955  E.wex 977  {cab 1456  A.wral 1637  E.wrex 1638   class class class wbr 2609  -->wf 3168  ` cfv 3172  (class class class)co 3948  supcsup 4547  RRcr 5205  0cc0 5206  1c1 5207   + caddc 5209  -ucneg 5265   / cdiv 5266   <_ cle 5267  NNcn 5268   < clt 5458
This theorem is referenced by:  infcvglem3 7158
This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-9 962  ax-10 963  ax-11 964  ax-12 965  ax-13 966  ax-14 967  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213  ax-ext 1452  ax-rep 2683  ax-sep 2693  ax-nul 2700  ax-pow 2732 &n