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 ⊢ 𝐽 = ( 𝐴 [,] 𝐵 )
iccbnd.2 ⊢ 𝑀 = ( ( abs ∘ − ) ↾ ( 𝐽 × 𝐽 ) )
Assertion iccbnd ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → 𝑀 ∈ ( Bnd ‘ 𝐽 ) )

Proof

Step Hyp Ref Expression
1 iccbnd.1 ⊢ 𝐽 = ( 𝐴 [,] 𝐵 )
2 iccbnd.2 ⊢ 𝑀 = ( ( abs ∘ − ) ↾ ( 𝐽 × 𝐽 ) )
3 cnmet ⊢ ( abs ∘ − ) ∈ ( Met ‘ ℂ )
4 iccssre ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
5 1 4 eqsstrid ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → 𝐽 ⊆ ℝ )
6 ax-resscn ⊢ ℝ ⊆ ℂ
7 5 6 sstrdi ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → 𝐽 ⊆ ℂ )
8 metres2 ⊢ ( ( ( abs ∘ − ) ∈ ( Met ‘ ℂ ) ∧ 𝐽 ⊆ ℂ ) → ( ( abs ∘ − ) ↾ ( 𝐽 × 𝐽 ) ) ∈ ( Met ‘ 𝐽 ) )
9 3 7 8 sylancr ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( abs ∘ − ) ↾ ( 𝐽 × 𝐽 ) ) ∈ ( Met ‘ 𝐽 ) )
10 2 9 eqeltrid ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → 𝑀 ∈ ( Met ‘ 𝐽 ) )
11 resubcl ⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( 𝐵 − 𝐴 ) ∈ ℝ )
12 11 ancoms ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐵 − 𝐴 ) ∈ ℝ )
13 2 oveqi ⊢ ( 𝑥 𝑀 𝑦 ) = ( 𝑥 ( ( abs ∘ − ) ↾ ( 𝐽 × 𝐽 ) ) 𝑦 )
14 ovres ⊢ ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) → ( 𝑥 ( ( abs ∘ − ) ↾ ( 𝐽 × 𝐽 ) ) 𝑦 ) = ( 𝑥 ( abs ∘ − ) 𝑦 ) )
15 14 adantl ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) → ( 𝑥 ( ( abs ∘ − ) ↾ ( 𝐽 × 𝐽 ) ) 𝑦 ) = ( 𝑥 ( abs ∘ − ) 𝑦 ) )
16 13 15 syl5eq ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) → ( 𝑥 𝑀 𝑦 ) = ( 𝑥 ( abs ∘ − ) 𝑦 ) )
17 7 sselda ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝑥 ∈ 𝐽 ) → 𝑥 ∈ ℂ )
18 7 sselda ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝑦 ∈ 𝐽 ) → 𝑦 ∈ ℂ )
19 17 18 anim12dan ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) → ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) )
20 eqid ⊢ ( abs ∘ − ) = ( abs ∘ − )
21 20 cnmetdval ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝑥 ( abs ∘ − ) 𝑦 ) = ( abs ‘ ( 𝑥 − 𝑦 ) ) )
22 19 21 syl ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) → ( 𝑥 ( abs ∘ − ) 𝑦 ) = ( abs ‘ ( 𝑥 − 𝑦 ) ) )
23 16 22 eqtrd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) → ( 𝑥 𝑀 𝑦 ) = ( abs ‘ ( 𝑥 − 𝑦 ) ) )
24 simprr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) → 𝑦 ∈ 𝐽 )
25 24 1 eleqtrdi ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) → 𝑦 ∈ ( 𝐴 [,] 𝐵 ) )
26 elicc2 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝑦 ∈ ℝ ∧ 𝐴 ≤ 𝑦 ∧ 𝑦 ≤ 𝐵 ) ) )
27 26 adantr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) → ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝑦 ∈ ℝ ∧ 𝐴 ≤ 𝑦 ∧ 𝑦 ≤ 𝐵 ) ) )
28 25 27 mpbid ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) → ( 𝑦 ∈ ℝ ∧ 𝐴 ≤ 𝑦 ∧ 𝑦 ≤ 𝐵 ) )
29 28 simp1d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) → 𝑦 ∈ ℝ )
30 12 adantr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) → ( 𝐵 − 𝐴 ) ∈ ℝ )
31 resubcl ⊢ ( ( 𝑦 ∈ ℝ ∧ ( 𝐵 − 𝐴 ) ∈ ℝ ) → ( 𝑦 − ( 𝐵 − 𝐴 ) ) ∈ ℝ )
32 29 30 31 syl2anc ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) → ( 𝑦 − ( 𝐵 − 𝐴 ) ) ∈ ℝ )
33 simpll ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) → 𝐴 ∈ ℝ )
34 simprl ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) → 𝑥 ∈ 𝐽 )
35 34 1 eleqtrdi ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) → 𝑥 ∈ ( 𝐴 [,] 𝐵 ) )
36 elicc2 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵 ) ) )
37 36 adantr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) → ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵 ) ) )
38 35 37 mpbid ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) → ( 𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵 ) )
39 38 simp1d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) → 𝑥 ∈ ℝ )
40 simplr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) → 𝐵 ∈ ℝ )
41 28 simp3d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) → 𝑦 ≤ 𝐵 )
42 29 40 33 41 lesub1dd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) → ( 𝑦 − 𝐴 ) ≤ ( 𝐵 − 𝐴 ) )
43 29 33 30 42 subled ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) → ( 𝑦 − ( 𝐵 − 𝐴 ) ) ≤ 𝐴 )
44 38 simp2d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) → 𝐴 ≤ 𝑥 )
45 32 33 39 43 44 letrd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) → ( 𝑦 − ( 𝐵 − 𝐴 ) ) ≤ 𝑥 )
46 29 30 readdcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) → ( 𝑦 + ( 𝐵 − 𝐴 ) ) ∈ ℝ )
47 38 simp3d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) → 𝑥 ≤ 𝐵 )
48 28 simp2d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) → 𝐴 ≤ 𝑦 )
49 33 29 40 48 lesub2dd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) → ( 𝐵 − 𝑦 ) ≤ ( 𝐵 − 𝐴 ) )
50 40 29 30 lesubadd2d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) → ( ( 𝐵 − 𝑦 ) ≤ ( 𝐵 − 𝐴 ) ↔ 𝐵 ≤ ( 𝑦 + ( 𝐵 − 𝐴 ) ) ) )
51 49 50 mpbid ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) → 𝐵 ≤ ( 𝑦 + ( 𝐵 − 𝐴 ) ) )
52 39 40 46 47 51 letrd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) → 𝑥 ≤ ( 𝑦 + ( 𝐵 − 𝐴 ) ) )
53 39 29 30 absdifled ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) → ( ( abs ‘ ( 𝑥 − 𝑦 ) ) ≤ ( 𝐵 − 𝐴 ) ↔ ( ( 𝑦 − ( 𝐵 − 𝐴 ) ) ≤ 𝑥 ∧ 𝑥 ≤ ( 𝑦 + ( 𝐵 − 𝐴 ) ) ) ) )
54 45 52 53 mpbir2and ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) → ( abs ‘ ( 𝑥 − 𝑦 ) ) ≤ ( 𝐵 − 𝐴 ) )
55 23 54 eqbrtrd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) → ( 𝑥 𝑀 𝑦 ) ≤ ( 𝐵 − 𝐴 ) )
56 55 ralrimivva ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ∀ 𝑥 ∈ 𝐽 ∀ 𝑦 ∈ 𝐽 ( 𝑥 𝑀 𝑦 ) ≤ ( 𝐵 − 𝐴 ) )
57 breq2 ⊢ ( 𝑟 = ( 𝐵 − 𝐴 ) → ( ( 𝑥 𝑀 𝑦 ) ≤ 𝑟 ↔ ( 𝑥 𝑀 𝑦 ) ≤ ( 𝐵 − 𝐴 ) ) )
58 57 2ralbidv ⊢ ( 𝑟 = ( 𝐵 − 𝐴 ) → ( ∀ 𝑥 ∈ 𝐽 ∀ 𝑦 ∈ 𝐽 ( 𝑥 𝑀 𝑦 ) ≤ 𝑟 ↔ ∀ 𝑥 ∈ 𝐽 ∀ 𝑦 ∈ 𝐽 ( 𝑥 𝑀 𝑦 ) ≤ ( 𝐵 − 𝐴 ) ) )
59 58 rspcev ⊢ ( ( ( 𝐵 − 𝐴 ) ∈ ℝ ∧ ∀ 𝑥 ∈ 𝐽 ∀ 𝑦 ∈ 𝐽 ( 𝑥 𝑀 𝑦 ) ≤ ( 𝐵 − 𝐴 ) ) → ∃ 𝑟 ∈ ℝ ∀ 𝑥 ∈ 𝐽 ∀ 𝑦 ∈ 𝐽 ( 𝑥 𝑀 𝑦 ) ≤ 𝑟 )
60 12 56 59 syl2anc ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ∃ 𝑟 ∈ ℝ ∀ 𝑥 ∈ 𝐽 ∀ 𝑦 ∈ 𝐽 ( 𝑥 𝑀 𝑦 ) ≤ 𝑟 )
61 isbnd3b ⊢ ( 𝑀 ∈ ( Bnd ‘ 𝐽 ) ↔ ( 𝑀 ∈ ( Met ‘ 𝐽 ) ∧ ∃ 𝑟 ∈ ℝ ∀ 𝑥 ∈ 𝐽 ∀ 𝑦 ∈ 𝐽 ( 𝑥 𝑀 𝑦 ) ≤ 𝑟 ) )
62 10 60 61 sylanbrc ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → 𝑀 ∈ ( Bnd ‘ 𝐽 ) )