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 = [A, B]$
	iccbnd.2	$⊢ M = {(abs \circ -) ↾}_{(J \times J)}$
Assertion	iccbnd	$⊢ (A \in ℝ \land B \in ℝ) \to M \in Bnd (J)$

Proof

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

Metamath Proof Explorer

Theorem iccbnd

Proof