Metamath Proof Explorer


Theorem blbnd

Description: A ball is bounded. (Contributed by Jeff Madsen, 2-Sep-2009) (Proof shortened by Mario Carneiro, 15-Jan-2014)

Ref Expression
Assertion blbnd M ∞Met X Y X R M Y ball M R × Y ball M R Bnd Y ball M R

Proof

Step Hyp Ref Expression
1 simp1 M ∞Met X Y X R M ∞Met X
2 rexr R R *
3 blssm M ∞Met X Y X R * Y ball M R X
4 2 3 syl3an3 M ∞Met X Y X R Y ball M R X
5 xmetres2 M ∞Met X Y ball M R X M Y ball M R × Y ball M R ∞Met Y ball M R
6 1 4 5 syl2anc M ∞Met X Y X R M Y ball M R × Y ball M R ∞Met Y ball M R
7 6 adantr M ∞Met X Y X R Y ball M R = M Y ball M R × Y ball M R ∞Met Y ball M R
8 rzal Y ball M R = x Y ball M R r + Y ball M R = x ball M Y ball M R × Y ball M R r
9 8 adantl M ∞Met X Y X R Y ball M R = x Y ball M R r + Y ball M R = x ball M Y ball M R × Y ball M R r
10 isbndx M Y ball M R × Y ball M R Bnd Y ball M R M Y ball M R × Y ball M R ∞Met Y ball M R x Y ball M R r + Y ball M R = x ball M Y ball M R × Y ball M R r
11 7 9 10 sylanbrc M ∞Met X Y X R Y ball M R = M Y ball M R × Y ball M R Bnd Y ball M R
12 6 adantr M ∞Met X Y X R Y ball M R M Y ball M R × Y ball M R ∞Met Y ball M R
13 1 adantr M ∞Met X Y X R Y ball M R M ∞Met X
14 simpl2 M ∞Met X Y X R Y ball M R Y X
15 simpl3 M ∞Met X Y X R Y ball M R R
16 xbln0 M ∞Met X Y X R * Y ball M R 0 < R
17 2 16 syl3an3 M ∞Met X Y X R Y ball M R 0 < R
18 17 biimpa M ∞Met X Y X R Y ball M R 0 < R
19 15 18 elrpd M ∞Met X Y X R Y ball M R R +
20 blcntr M ∞Met X Y X R + Y Y ball M R
21 13 14 19 20 syl3anc M ∞Met X Y X R Y ball M R Y Y ball M R
22 14 21 elind M ∞Met X Y X R Y ball M R Y X Y ball M R
23 15 rexrd M ∞Met X Y X R Y ball M R R *
24 eqid M Y ball M R × Y ball M R = M Y ball M R × Y ball M R
25 24 blres M ∞Met X Y X Y ball M R R * Y ball M Y ball M R × Y ball M R R = Y ball M R Y ball M R
26 13 22 23 25 syl3anc M ∞Met X Y X R Y ball M R Y ball M Y ball M R × Y ball M R R = Y ball M R Y ball M R
27 inidm Y ball M R Y ball M R = Y ball M R
28 26 27 syl6req M ∞Met X Y X R Y ball M R Y ball M R = Y ball M Y ball M R × Y ball M R R
29 rspceov Y Y ball M R R + Y ball M R = Y ball M Y ball M R × Y ball M R R x Y ball M R r + Y ball M R = x ball M Y ball M R × Y ball M R r
30 21 19 28 29 syl3anc M ∞Met X Y X R Y ball M R x Y ball M R r + Y ball M R = x ball M Y ball M R × Y ball M R r
31 isbnd2 M Y ball M R × Y ball M R Bnd Y ball M R Y ball M R M Y ball M R × Y ball M R ∞Met Y ball M R x Y ball M R r + Y ball M R = x ball M Y ball M R × Y ball M R r
32 12 30 31 sylanbrc M ∞Met X Y X R Y ball M R M Y ball M R × Y ball M R Bnd Y ball M R Y ball M R
33 32 simpld M ∞Met X Y X R Y ball M R M Y ball M R × Y ball M R Bnd Y ball M R
34 11 33 pm2.61dane M ∞Met X Y X R M Y ball M R × Y ball M R Bnd Y ball M R