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 = ( A [,] B )
	iccbnd.2	|- M = ( ( abs o. - ) |` ( J X. J ) )
Assertion	iccbnd	|- ( ( A e. RR /\ B e. RR ) -> M e. ( Bnd ` J ) )

Proof

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