# Metamath Proof Explorer

## Theorem iccbnd

Description: A closed interval in RR is bounded. (Contributed by Jeff Madsen, 2-Sep-2009) (Proof shortened by Mario Carneiro, 22-Sep-2015)

Ref Expression
Hypotheses iccbnd.1 ${⊢}{J}=\left[{A},{B}\right]$
iccbnd.2 ${⊢}{M}={\left(\mathrm{abs}\circ -\right)↾}_{\left({J}×{J}\right)}$
Assertion iccbnd ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to {M}\in \mathrm{Bnd}\left({J}\right)$

### Proof

Step Hyp Ref Expression
1 iccbnd.1 ${⊢}{J}=\left[{A},{B}\right]$
2 iccbnd.2 ${⊢}{M}={\left(\mathrm{abs}\circ -\right)↾}_{\left({J}×{J}\right)}$
3 cnmet ${⊢}\mathrm{abs}\circ -\in \mathrm{Met}\left(ℂ\right)$
4 iccssre ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to \left[{A},{B}\right]\subseteq ℝ$
5 1 4 eqsstrid ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to {J}\subseteq ℝ$
6 ax-resscn ${⊢}ℝ\subseteq ℂ$
7 5 6 sstrdi ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to {J}\subseteq ℂ$
8 metres2 ${⊢}\left(\mathrm{abs}\circ -\in \mathrm{Met}\left(ℂ\right)\wedge {J}\subseteq ℂ\right)\to {\left(\mathrm{abs}\circ -\right)↾}_{\left({J}×{J}\right)}\in \mathrm{Met}\left({J}\right)$
9 3 7 8 sylancr ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to {\left(\mathrm{abs}\circ -\right)↾}_{\left({J}×{J}\right)}\in \mathrm{Met}\left({J}\right)$
10 2 9 eqeltrid ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to {M}\in \mathrm{Met}\left({J}\right)$
11 resubcl ${⊢}\left({B}\in ℝ\wedge {A}\in ℝ\right)\to {B}-{A}\in ℝ$
12 11 ancoms ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to {B}-{A}\in ℝ$
13 2 oveqi ${⊢}{x}{M}{y}={x}\left({\left(\mathrm{abs}\circ -\right)↾}_{\left({J}×{J}\right)}\right){y}$
14 ovres ${⊢}\left({x}\in {J}\wedge {y}\in {J}\right)\to {x}\left({\left(\mathrm{abs}\circ -\right)↾}_{\left({J}×{J}\right)}\right){y}={x}\left(\mathrm{abs}\circ -\right){y}$
15 14 adantl ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge \left({x}\in {J}\wedge {y}\in {J}\right)\right)\to {x}\left({\left(\mathrm{abs}\circ -\right)↾}_{\left({J}×{J}\right)}\right){y}={x}\left(\mathrm{abs}\circ -\right){y}$
16 13 15 syl5eq ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge \left({x}\in {J}\wedge {y}\in {J}\right)\right)\to {x}{M}{y}={x}\left(\mathrm{abs}\circ -\right){y}$
17 7 sselda ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge {x}\in {J}\right)\to {x}\in ℂ$
18 7 sselda ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge {y}\in {J}\right)\to {y}\in ℂ$
19 17 18 anim12dan ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge \left({x}\in {J}\wedge {y}\in {J}\right)\right)\to \left({x}\in ℂ\wedge {y}\in ℂ\right)$
20 eqid ${⊢}\mathrm{abs}\circ -=\mathrm{abs}\circ -$
21 20 cnmetdval ${⊢}\left({x}\in ℂ\wedge {y}\in ℂ\right)\to {x}\left(\mathrm{abs}\circ -\right){y}=\left|{x}-{y}\right|$
22 19 21 syl ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge \left({x}\in {J}\wedge {y}\in {J}\right)\right)\to {x}\left(\mathrm{abs}\circ -\right){y}=\left|{x}-{y}\right|$
23 16 22 eqtrd ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge \left({x}\in {J}\wedge {y}\in {J}\right)\right)\to {x}{M}{y}=\left|{x}-{y}\right|$
24 simprr ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge \left({x}\in {J}\wedge {y}\in {J}\right)\right)\to {y}\in {J}$
25 24 1 eleqtrdi ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge \left({x}\in {J}\wedge {y}\in {J}\right)\right)\to {y}\in \left[{A},{B}\right]$
26 elicc2 ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to \left({y}\in \left[{A},{B}\right]↔\left({y}\in ℝ\wedge {A}\le {y}\wedge {y}\le {B}\right)\right)$
27 26 adantr ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge \left({x}\in {J}\wedge {y}\in {J}\right)\right)\to \left({y}\in \left[{A},{B}\right]↔\left({y}\in ℝ\wedge {A}\le {y}\wedge {y}\le {B}\right)\right)$
28 25 27 mpbid ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge \left({x}\in {J}\wedge {y}\in {J}\right)\right)\to \left({y}\in ℝ\wedge {A}\le {y}\wedge {y}\le {B}\right)$
29 28 simp1d ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge \left({x}\in {J}\wedge {y}\in {J}\right)\right)\to {y}\in ℝ$
30 12 adantr ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge \left({x}\in {J}\wedge {y}\in {J}\right)\right)\to {B}-{A}\in ℝ$
31 resubcl ${⊢}\left({y}\in ℝ\wedge {B}-{A}\in ℝ\right)\to {y}-\left({B}-{A}\right)\in ℝ$
32 29 30 31 syl2anc ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge \left({x}\in {J}\wedge {y}\in {J}\right)\right)\to {y}-\left({B}-{A}\right)\in ℝ$
33 simpll ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge \left({x}\in {J}\wedge {y}\in {J}\right)\right)\to {A}\in ℝ$
34 simprl ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge \left({x}\in {J}\wedge {y}\in {J}\right)\right)\to {x}\in {J}$
35 34 1 eleqtrdi ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge \left({x}\in {J}\wedge {y}\in {J}\right)\right)\to {x}\in \left[{A},{B}\right]$
36 elicc2 ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to \left({x}\in \left[{A},{B}\right]↔\left({x}\in ℝ\wedge {A}\le {x}\wedge {x}\le {B}\right)\right)$
37 36 adantr ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge \left({x}\in {J}\wedge {y}\in {J}\right)\right)\to \left({x}\in \left[{A},{B}\right]↔\left({x}\in ℝ\wedge {A}\le {x}\wedge {x}\le {B}\right)\right)$
38 35 37 mpbid ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge \left({x}\in {J}\wedge {y}\in {J}\right)\right)\to \left({x}\in ℝ\wedge {A}\le {x}\wedge {x}\le {B}\right)$
39 38 simp1d ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge \left({x}\in {J}\wedge {y}\in {J}\right)\right)\to {x}\in ℝ$
40 simplr ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge \left({x}\in {J}\wedge {y}\in {J}\right)\right)\to {B}\in ℝ$
41 28 simp3d ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge \left({x}\in {J}\wedge {y}\in {J}\right)\right)\to {y}\le {B}$
42 29 40 33 41 lesub1dd ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge \left({x}\in {J}\wedge {y}\in {J}\right)\right)\to {y}-{A}\le {B}-{A}$
43 29 33 30 42 subled ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge \left({x}\in {J}\wedge {y}\in {J}\right)\right)\to {y}-\left({B}-{A}\right)\le {A}$
44 38 simp2d ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge \left({x}\in {J}\wedge {y}\in {J}\right)\right)\to {A}\le {x}$
45 32 33 39 43 44 letrd ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge \left({x}\in {J}\wedge {y}\in {J}\right)\right)\to {y}-\left({B}-{A}\right)\le {x}$
46 29 30 readdcld ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge \left({x}\in {J}\wedge {y}\in {J}\right)\right)\to {y}+{B}-{A}\in ℝ$
47 38 simp3d ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge \left({x}\in {J}\wedge {y}\in {J}\right)\right)\to {x}\le {B}$
48 28 simp2d ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge \left({x}\in {J}\wedge {y}\in {J}\right)\right)\to {A}\le {y}$
49 33 29 40 48 lesub2dd ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge \left({x}\in {J}\wedge {y}\in {J}\right)\right)\to {B}-{y}\le {B}-{A}$
50 40 29 30 lesubadd2d ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge \left({x}\in {J}\wedge {y}\in {J}\right)\right)\to \left({B}-{y}\le {B}-{A}↔{B}\le {y}+{B}-{A}\right)$
51 49 50 mpbid ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge \left({x}\in {J}\wedge {y}\in {J}\right)\right)\to {B}\le {y}+{B}-{A}$
52 39 40 46 47 51 letrd ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge \left({x}\in {J}\wedge {y}\in {J}\right)\right)\to {x}\le {y}+{B}-{A}$
53 39 29 30 absdifled ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge \left({x}\in {J}\wedge {y}\in {J}\right)\right)\to \left(\left|{x}-{y}\right|\le {B}-{A}↔\left({y}-\left({B}-{A}\right)\le {x}\wedge {x}\le {y}+{B}-{A}\right)\right)$
54 45 52 53 mpbir2and ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge \left({x}\in {J}\wedge {y}\in {J}\right)\right)\to \left|{x}-{y}\right|\le {B}-{A}$
55 23 54 eqbrtrd ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge \left({x}\in {J}\wedge {y}\in {J}\right)\right)\to {x}{M}{y}\le {B}-{A}$
56 55 ralrimivva ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to \forall {x}\in {J}\phantom{\rule{.4em}{0ex}}\forall {y}\in {J}\phantom{\rule{.4em}{0ex}}{x}{M}{y}\le {B}-{A}$
57 breq2 ${⊢}{r}={B}-{A}\to \left({x}{M}{y}\le {r}↔{x}{M}{y}\le {B}-{A}\right)$
58 57 2ralbidv ${⊢}{r}={B}-{A}\to \left(\forall {x}\in {J}\phantom{\rule{.4em}{0ex}}\forall {y}\in {J}\phantom{\rule{.4em}{0ex}}{x}{M}{y}\le {r}↔\forall {x}\in {J}\phantom{\rule{.4em}{0ex}}\forall {y}\in {J}\phantom{\rule{.4em}{0ex}}{x}{M}{y}\le {B}-{A}\right)$
59 58 rspcev ${⊢}\left({B}-{A}\in ℝ\wedge \forall {x}\in {J}\phantom{\rule{.4em}{0ex}}\forall {y}\in {J}\phantom{\rule{.4em}{0ex}}{x}{M}{y}\le {B}-{A}\right)\to \exists {r}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {x}\in {J}\phantom{\rule{.4em}{0ex}}\forall {y}\in {J}\phantom{\rule{.4em}{0ex}}{x}{M}{y}\le {r}$
60 12 56 59 syl2anc ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to \exists {r}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {x}\in {J}\phantom{\rule{.4em}{0ex}}\forall {y}\in {J}\phantom{\rule{.4em}{0ex}}{x}{M}{y}\le {r}$
61 isbnd3b ${⊢}{M}\in \mathrm{Bnd}\left({J}\right)↔\left({M}\in \mathrm{Met}\left({J}\right)\wedge \exists {r}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {x}\in {J}\phantom{\rule{.4em}{0ex}}\forall {y}\in {J}\phantom{\rule{.4em}{0ex}}{x}{M}{y}\le {r}\right)$
62 10 60 61 sylanbrc ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to {M}\in \mathrm{Bnd}\left({J}\right)$