# Metamath Proof Explorer

## Theorem nmobndseqi

Description: A bounded sequence determines a bounded operator. (Contributed by NM, 18-Jan-2008) (Revised by Mario Carneiro, 7-Apr-2013) (New usage is discouraged.)

Ref Expression
Hypotheses nmoubi.1 ${⊢}{X}=\mathrm{BaseSet}\left({U}\right)$
nmoubi.y ${⊢}{Y}=\mathrm{BaseSet}\left({W}\right)$
nmoubi.l ${⊢}{L}={norm}_{CV}\left({U}\right)$
nmoubi.m ${⊢}{M}={norm}_{CV}\left({W}\right)$
nmoubi.3 ${⊢}{N}={U}{normOp}_{\mathrm{OLD}}{W}$
nmoubi.u ${⊢}{U}\in \mathrm{NrmCVec}$
nmoubi.w ${⊢}{W}\in \mathrm{NrmCVec}$
Assertion nmobndseqi ${⊢}\left({T}:{X}⟶{Y}\wedge \forall {f}\phantom{\rule{.4em}{0ex}}\left(\left({f}:ℕ⟶{X}\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}{L}\left({f}\left({k}\right)\right)\le 1\right)\to \exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}{M}\left({T}\left({f}\left({k}\right)\right)\right)\le {k}\right)\right)\to {N}\left({T}\right)\in ℝ$

### Proof

Step Hyp Ref Expression
1 nmoubi.1 ${⊢}{X}=\mathrm{BaseSet}\left({U}\right)$
2 nmoubi.y ${⊢}{Y}=\mathrm{BaseSet}\left({W}\right)$
3 nmoubi.l ${⊢}{L}={norm}_{CV}\left({U}\right)$
4 nmoubi.m ${⊢}{M}={norm}_{CV}\left({W}\right)$
5 nmoubi.3 ${⊢}{N}={U}{normOp}_{\mathrm{OLD}}{W}$
6 nmoubi.u ${⊢}{U}\in \mathrm{NrmCVec}$
7 nmoubi.w ${⊢}{W}\in \mathrm{NrmCVec}$
8 impexp ${⊢}\left(\left({f}:ℕ⟶{X}\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}{L}\left({f}\left({k}\right)\right)\le 1\right)\to \exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}{M}\left({T}\left({f}\left({k}\right)\right)\right)\le {k}\right)↔\left({f}:ℕ⟶{X}\to \left(\forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}{L}\left({f}\left({k}\right)\right)\le 1\to \exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}{M}\left({T}\left({f}\left({k}\right)\right)\right)\le {k}\right)\right)$
9 r19.35 ${⊢}\exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({L}\left({f}\left({k}\right)\right)\le 1\to {M}\left({T}\left({f}\left({k}\right)\right)\right)\le {k}\right)↔\left(\forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}{L}\left({f}\left({k}\right)\right)\le 1\to \exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}{M}\left({T}\left({f}\left({k}\right)\right)\right)\le {k}\right)$
10 9 imbi2i ${⊢}\left({f}:ℕ⟶{X}\to \exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({L}\left({f}\left({k}\right)\right)\le 1\to {M}\left({T}\left({f}\left({k}\right)\right)\right)\le {k}\right)\right)↔\left({f}:ℕ⟶{X}\to \left(\forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}{L}\left({f}\left({k}\right)\right)\le 1\to \exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}{M}\left({T}\left({f}\left({k}\right)\right)\right)\le {k}\right)\right)$
11 8 10 bitr4i ${⊢}\left(\left({f}:ℕ⟶{X}\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}{L}\left({f}\left({k}\right)\right)\le 1\right)\to \exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}{M}\left({T}\left({f}\left({k}\right)\right)\right)\le {k}\right)↔\left({f}:ℕ⟶{X}\to \exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({L}\left({f}\left({k}\right)\right)\le 1\to {M}\left({T}\left({f}\left({k}\right)\right)\right)\le {k}\right)\right)$
12 11 albii ${⊢}\forall {f}\phantom{\rule{.4em}{0ex}}\left(\left({f}:ℕ⟶{X}\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}{L}\left({f}\left({k}\right)\right)\le 1\right)\to \exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}{M}\left({T}\left({f}\left({k}\right)\right)\right)\le {k}\right)↔\forall {f}\phantom{\rule{.4em}{0ex}}\left({f}:ℕ⟶{X}\to \exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({L}\left({f}\left({k}\right)\right)\le 1\to {M}\left({T}\left({f}\left({k}\right)\right)\right)\le {k}\right)\right)$
13 1 fvexi ${⊢}{X}\in \mathrm{V}$
14 nnenom ${⊢}ℕ\approx \mathrm{\omega }$
15 fveq2 ${⊢}{y}={f}\left({k}\right)\to {L}\left({y}\right)={L}\left({f}\left({k}\right)\right)$
16 15 breq1d ${⊢}{y}={f}\left({k}\right)\to \left({L}\left({y}\right)\le 1↔{L}\left({f}\left({k}\right)\right)\le 1\right)$
17 2fveq3 ${⊢}{y}={f}\left({k}\right)\to {M}\left({T}\left({y}\right)\right)={M}\left({T}\left({f}\left({k}\right)\right)\right)$
18 17 breq1d ${⊢}{y}={f}\left({k}\right)\to \left({M}\left({T}\left({y}\right)\right)\le {k}↔{M}\left({T}\left({f}\left({k}\right)\right)\right)\le {k}\right)$
19 16 18 imbi12d ${⊢}{y}={f}\left({k}\right)\to \left(\left({L}\left({y}\right)\le 1\to {M}\left({T}\left({y}\right)\right)\le {k}\right)↔\left({L}\left({f}\left({k}\right)\right)\le 1\to {M}\left({T}\left({f}\left({k}\right)\right)\right)\le {k}\right)\right)$
20 19 notbid ${⊢}{y}={f}\left({k}\right)\to \left(¬\left({L}\left({y}\right)\le 1\to {M}\left({T}\left({y}\right)\right)\le {k}\right)↔¬\left({L}\left({f}\left({k}\right)\right)\le 1\to {M}\left({T}\left({f}\left({k}\right)\right)\right)\le {k}\right)\right)$
21 13 14 20 axcc4 ${⊢}\forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\exists {y}\in {X}\phantom{\rule{.4em}{0ex}}¬\left({L}\left({y}\right)\le 1\to {M}\left({T}\left({y}\right)\right)\le {k}\right)\to \exists {f}\phantom{\rule{.4em}{0ex}}\left({f}:ℕ⟶{X}\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}¬\left({L}\left({f}\left({k}\right)\right)\le 1\to {M}\left({T}\left({f}\left({k}\right)\right)\right)\le {k}\right)\right)$
22 21 con3i ${⊢}¬\exists {f}\phantom{\rule{.4em}{0ex}}\left({f}:ℕ⟶{X}\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}¬\left({L}\left({f}\left({k}\right)\right)\le 1\to {M}\left({T}\left({f}\left({k}\right)\right)\right)\le {k}\right)\right)\to ¬\forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\exists {y}\in {X}\phantom{\rule{.4em}{0ex}}¬\left({L}\left({y}\right)\le 1\to {M}\left({T}\left({y}\right)\right)\le {k}\right)$
23 dfrex2 ${⊢}\exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({L}\left({f}\left({k}\right)\right)\le 1\to {M}\left({T}\left({f}\left({k}\right)\right)\right)\le {k}\right)↔¬\forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}¬\left({L}\left({f}\left({k}\right)\right)\le 1\to {M}\left({T}\left({f}\left({k}\right)\right)\right)\le {k}\right)$
24 23 imbi2i ${⊢}\left({f}:ℕ⟶{X}\to \exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({L}\left({f}\left({k}\right)\right)\le 1\to {M}\left({T}\left({f}\left({k}\right)\right)\right)\le {k}\right)\right)↔\left({f}:ℕ⟶{X}\to ¬\forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}¬\left({L}\left({f}\left({k}\right)\right)\le 1\to {M}\left({T}\left({f}\left({k}\right)\right)\right)\le {k}\right)\right)$
25 24 albii ${⊢}\forall {f}\phantom{\rule{.4em}{0ex}}\left({f}:ℕ⟶{X}\to \exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({L}\left({f}\left({k}\right)\right)\le 1\to {M}\left({T}\left({f}\left({k}\right)\right)\right)\le {k}\right)\right)↔\forall {f}\phantom{\rule{.4em}{0ex}}\left({f}:ℕ⟶{X}\to ¬\forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}¬\left({L}\left({f}\left({k}\right)\right)\le 1\to {M}\left({T}\left({f}\left({k}\right)\right)\right)\le {k}\right)\right)$
26 alinexa ${⊢}\forall {f}\phantom{\rule{.4em}{0ex}}\left({f}:ℕ⟶{X}\to ¬\forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}¬\left({L}\left({f}\left({k}\right)\right)\le 1\to {M}\left({T}\left({f}\left({k}\right)\right)\right)\le {k}\right)\right)↔¬\exists {f}\phantom{\rule{.4em}{0ex}}\left({f}:ℕ⟶{X}\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}¬\left({L}\left({f}\left({k}\right)\right)\le 1\to {M}\left({T}\left({f}\left({k}\right)\right)\right)\le {k}\right)\right)$
27 25 26 bitri ${⊢}\forall {f}\phantom{\rule{.4em}{0ex}}\left({f}:ℕ⟶{X}\to \exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({L}\left({f}\left({k}\right)\right)\le 1\to {M}\left({T}\left({f}\left({k}\right)\right)\right)\le {k}\right)\right)↔¬\exists {f}\phantom{\rule{.4em}{0ex}}\left({f}:ℕ⟶{X}\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}¬\left({L}\left({f}\left({k}\right)\right)\le 1\to {M}\left({T}\left({f}\left({k}\right)\right)\right)\le {k}\right)\right)$
28 dfral2 ${⊢}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({L}\left({y}\right)\le 1\to {M}\left({T}\left({y}\right)\right)\le {k}\right)↔¬\exists {y}\in {X}\phantom{\rule{.4em}{0ex}}¬\left({L}\left({y}\right)\le 1\to {M}\left({T}\left({y}\right)\right)\le {k}\right)$
29 28 rexbii ${⊢}\exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({L}\left({y}\right)\le 1\to {M}\left({T}\left({y}\right)\right)\le {k}\right)↔\exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}¬\exists {y}\in {X}\phantom{\rule{.4em}{0ex}}¬\left({L}\left({y}\right)\le 1\to {M}\left({T}\left({y}\right)\right)\le {k}\right)$
30 rexnal ${⊢}\exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}¬\exists {y}\in {X}\phantom{\rule{.4em}{0ex}}¬\left({L}\left({y}\right)\le 1\to {M}\left({T}\left({y}\right)\right)\le {k}\right)↔¬\forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\exists {y}\in {X}\phantom{\rule{.4em}{0ex}}¬\left({L}\left({y}\right)\le 1\to {M}\left({T}\left({y}\right)\right)\le {k}\right)$
31 29 30 bitri ${⊢}\exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({L}\left({y}\right)\le 1\to {M}\left({T}\left({y}\right)\right)\le {k}\right)↔¬\forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\exists {y}\in {X}\phantom{\rule{.4em}{0ex}}¬\left({L}\left({y}\right)\le 1\to {M}\left({T}\left({y}\right)\right)\le {k}\right)$
32 22 27 31 3imtr4i ${⊢}\forall {f}\phantom{\rule{.4em}{0ex}}\left({f}:ℕ⟶{X}\to \exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({L}\left({f}\left({k}\right)\right)\le 1\to {M}\left({T}\left({f}\left({k}\right)\right)\right)\le {k}\right)\right)\to \exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({L}\left({y}\right)\le 1\to {M}\left({T}\left({y}\right)\right)\le {k}\right)$
33 nnre ${⊢}{k}\in ℕ\to {k}\in ℝ$
34 33 anim1i ${⊢}\left({k}\in ℕ\wedge \forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({L}\left({y}\right)\le 1\to {M}\left({T}\left({y}\right)\right)\le {k}\right)\right)\to \left({k}\in ℝ\wedge \forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({L}\left({y}\right)\le 1\to {M}\left({T}\left({y}\right)\right)\le {k}\right)\right)$
35 34 reximi2 ${⊢}\exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({L}\left({y}\right)\le 1\to {M}\left({T}\left({y}\right)\right)\le {k}\right)\to \exists {k}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({L}\left({y}\right)\le 1\to {M}\left({T}\left({y}\right)\right)\le {k}\right)$
36 32 35 syl ${⊢}\forall {f}\phantom{\rule{.4em}{0ex}}\left({f}:ℕ⟶{X}\to \exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({L}\left({f}\left({k}\right)\right)\le 1\to {M}\left({T}\left({f}\left({k}\right)\right)\right)\le {k}\right)\right)\to \exists {k}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({L}\left({y}\right)\le 1\to {M}\left({T}\left({y}\right)\right)\le {k}\right)$
37 12 36 sylbi ${⊢}\forall {f}\phantom{\rule{.4em}{0ex}}\left(\left({f}:ℕ⟶{X}\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}{L}\left({f}\left({k}\right)\right)\le 1\right)\to \exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}{M}\left({T}\left({f}\left({k}\right)\right)\right)\le {k}\right)\to \exists {k}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({L}\left({y}\right)\le 1\to {M}\left({T}\left({y}\right)\right)\le {k}\right)$
38 1 2 3 4 5 6 7 nmobndi ${⊢}{T}:{X}⟶{Y}\to \left({N}\left({T}\right)\in ℝ↔\exists {k}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({L}\left({y}\right)\le 1\to {M}\left({T}\left({y}\right)\right)\le {k}\right)\right)$
39 37 38 syl5ibr ${⊢}{T}:{X}⟶{Y}\to \left(\forall {f}\phantom{\rule{.4em}{0ex}}\left(\left({f}:ℕ⟶{X}\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}{L}\left({f}\left({k}\right)\right)\le 1\right)\to \exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}{M}\left({T}\left({f}\left({k}\right)\right)\right)\le {k}\right)\to {N}\left({T}\right)\in ℝ\right)$
40 39 imp ${⊢}\left({T}:{X}⟶{Y}\wedge \forall {f}\phantom{\rule{.4em}{0ex}}\left(\left({f}:ℕ⟶{X}\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}{L}\left({f}\left({k}\right)\right)\le 1\right)\to \exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}{M}\left({T}\left({f}\left({k}\right)\right)\right)\le {k}\right)\right)\to {N}\left({T}\right)\in ℝ$