Metamath Proof Explorer

Theorem bl2ioo

Description: A ball in terms of an open interval of reals. (Contributed by NM, 18-May-2007) (Revised by Mario Carneiro, 13-Nov-2013)

Ref Expression
Hypothesis remet.1 ⊒ 𝐷 = ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) )
Assertion bl2ioo ( ( 𝐴 ∈ ℝ ∧ 𝐡 ∈ ℝ ) β†’ ( 𝐴 ( ball β€˜ 𝐷 ) 𝐡 ) = ( ( 𝐴 βˆ’ 𝐡 ) (,) ( 𝐴 + 𝐡 ) ) )

Proof

Step Hyp Ref Expression
1 remet.1 ⊒ 𝐷 = ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) )
2 1 remetdval ⊒ ( ( 𝐴 ∈ ℝ ∧ π‘₯ ∈ ℝ ) β†’ ( 𝐴 𝐷 π‘₯ ) = ( abs β€˜ ( 𝐴 βˆ’ π‘₯ ) ) )
3 recn ⊒ ( 𝐴 ∈ ℝ β†’ 𝐴 ∈ β„‚ )
4 recn ⊒ ( π‘₯ ∈ ℝ β†’ π‘₯ ∈ β„‚ )
5 abssub ⊒ ( ( 𝐴 ∈ β„‚ ∧ π‘₯ ∈ β„‚ ) β†’ ( abs β€˜ ( 𝐴 βˆ’ π‘₯ ) ) = ( abs β€˜ ( π‘₯ βˆ’ 𝐴 ) ) )
6 3 4 5 syl2an ⊒ ( ( 𝐴 ∈ ℝ ∧ π‘₯ ∈ ℝ ) β†’ ( abs β€˜ ( 𝐴 βˆ’ π‘₯ ) ) = ( abs β€˜ ( π‘₯ βˆ’ 𝐴 ) ) )
7 2 6 eqtrd ⊒ ( ( 𝐴 ∈ ℝ ∧ π‘₯ ∈ ℝ ) β†’ ( 𝐴 𝐷 π‘₯ ) = ( abs β€˜ ( π‘₯ βˆ’ 𝐴 ) ) )
8 7 breq1d ⊒ ( ( 𝐴 ∈ ℝ ∧ π‘₯ ∈ ℝ ) β†’ ( ( 𝐴 𝐷 π‘₯ ) < 𝐡 ↔ ( abs β€˜ ( π‘₯ βˆ’ 𝐴 ) ) < 𝐡 ) )
9 8 adantlr ⊒ ( ( ( 𝐴 ∈ ℝ ∧ 𝐡 ∈ ℝ ) ∧ π‘₯ ∈ ℝ ) β†’ ( ( 𝐴 𝐷 π‘₯ ) < 𝐡 ↔ ( abs β€˜ ( π‘₯ βˆ’ 𝐴 ) ) < 𝐡 ) )
10 absdiflt ⊒ ( ( π‘₯ ∈ ℝ ∧ 𝐴 ∈ ℝ ∧ 𝐡 ∈ ℝ ) β†’ ( ( abs β€˜ ( π‘₯ βˆ’ 𝐴 ) ) < 𝐡 ↔ ( ( 𝐴 βˆ’ 𝐡 ) < π‘₯ ∧ π‘₯ < ( 𝐴 + 𝐡 ) ) ) )
11 10 3expb ⊒ ( ( π‘₯ ∈ ℝ ∧ ( 𝐴 ∈ ℝ ∧ 𝐡 ∈ ℝ ) ) β†’ ( ( abs β€˜ ( π‘₯ βˆ’ 𝐴 ) ) < 𝐡 ↔ ( ( 𝐴 βˆ’ 𝐡 ) < π‘₯ ∧ π‘₯ < ( 𝐴 + 𝐡 ) ) ) )
12 11 ancoms ⊒ ( ( ( 𝐴 ∈ ℝ ∧ 𝐡 ∈ ℝ ) ∧ π‘₯ ∈ ℝ ) β†’ ( ( abs β€˜ ( π‘₯ βˆ’ 𝐴 ) ) < 𝐡 ↔ ( ( 𝐴 βˆ’ 𝐡 ) < π‘₯ ∧ π‘₯ < ( 𝐴 + 𝐡 ) ) ) )
13 9 12 bitrd ⊒ ( ( ( 𝐴 ∈ ℝ ∧ 𝐡 ∈ ℝ ) ∧ π‘₯ ∈ ℝ ) β†’ ( ( 𝐴 𝐷 π‘₯ ) < 𝐡 ↔ ( ( 𝐴 βˆ’ 𝐡 ) < π‘₯ ∧ π‘₯ < ( 𝐴 + 𝐡 ) ) ) )
14 13 pm5.32da ⊒ ( ( 𝐴 ∈ ℝ ∧ 𝐡 ∈ ℝ ) β†’ ( ( π‘₯ ∈ ℝ ∧ ( 𝐴 𝐷 π‘₯ ) < 𝐡 ) ↔ ( π‘₯ ∈ ℝ ∧ ( ( 𝐴 βˆ’ 𝐡 ) < π‘₯ ∧ π‘₯ < ( 𝐴 + 𝐡 ) ) ) ) )
15 3anass ⊒ ( ( π‘₯ ∈ ℝ ∧ ( 𝐴 βˆ’ 𝐡 ) < π‘₯ ∧ π‘₯ < ( 𝐴 + 𝐡 ) ) ↔ ( π‘₯ ∈ ℝ ∧ ( ( 𝐴 βˆ’ 𝐡 ) < π‘₯ ∧ π‘₯ < ( 𝐴 + 𝐡 ) ) ) )
16 14 15 bitr4di ⊒ ( ( 𝐴 ∈ ℝ ∧ 𝐡 ∈ ℝ ) β†’ ( ( π‘₯ ∈ ℝ ∧ ( 𝐴 𝐷 π‘₯ ) < 𝐡 ) ↔ ( π‘₯ ∈ ℝ ∧ ( 𝐴 βˆ’ 𝐡 ) < π‘₯ ∧ π‘₯ < ( 𝐴 + 𝐡 ) ) ) )
17 rexr ⊒ ( 𝐡 ∈ ℝ β†’ 𝐡 ∈ ℝ* )
18 1 rexmet ⊒ 𝐷 ∈ ( ∞Met β€˜ ℝ )
19 elbl ⊒ ( ( 𝐷 ∈ ( ∞Met β€˜ ℝ ) ∧ 𝐴 ∈ ℝ ∧ 𝐡 ∈ ℝ* ) β†’ ( π‘₯ ∈ ( 𝐴 ( ball β€˜ 𝐷 ) 𝐡 ) ↔ ( π‘₯ ∈ ℝ ∧ ( 𝐴 𝐷 π‘₯ ) < 𝐡 ) ) )
20 18 19 mp3an1 ⊒ ( ( 𝐴 ∈ ℝ ∧ 𝐡 ∈ ℝ* ) β†’ ( π‘₯ ∈ ( 𝐴 ( ball β€˜ 𝐷 ) 𝐡 ) ↔ ( π‘₯ ∈ ℝ ∧ ( 𝐴 𝐷 π‘₯ ) < 𝐡 ) ) )
21 17 20 sylan2 ⊒ ( ( 𝐴 ∈ ℝ ∧ 𝐡 ∈ ℝ ) β†’ ( π‘₯ ∈ ( 𝐴 ( ball β€˜ 𝐷 ) 𝐡 ) ↔ ( π‘₯ ∈ ℝ ∧ ( 𝐴 𝐷 π‘₯ ) < 𝐡 ) ) )
22 resubcl ⊒ ( ( 𝐴 ∈ ℝ ∧ 𝐡 ∈ ℝ ) β†’ ( 𝐴 βˆ’ 𝐡 ) ∈ ℝ )
23 readdcl ⊒ ( ( 𝐴 ∈ ℝ ∧ 𝐡 ∈ ℝ ) β†’ ( 𝐴 + 𝐡 ) ∈ ℝ )
24 rexr ⊒ ( ( 𝐴 βˆ’ 𝐡 ) ∈ ℝ β†’ ( 𝐴 βˆ’ 𝐡 ) ∈ ℝ* )
25 rexr ⊒ ( ( 𝐴 + 𝐡 ) ∈ ℝ β†’ ( 𝐴 + 𝐡 ) ∈ ℝ* )
26 elioo2 ⊒ ( ( ( 𝐴 βˆ’ 𝐡 ) ∈ ℝ* ∧ ( 𝐴 + 𝐡 ) ∈ ℝ* ) β†’ ( π‘₯ ∈ ( ( 𝐴 βˆ’ 𝐡 ) (,) ( 𝐴 + 𝐡 ) ) ↔ ( π‘₯ ∈ ℝ ∧ ( 𝐴 βˆ’ 𝐡 ) < π‘₯ ∧ π‘₯ < ( 𝐴 + 𝐡 ) ) ) )
27 24 25 26 syl2an ⊒ ( ( ( 𝐴 βˆ’ 𝐡 ) ∈ ℝ ∧ ( 𝐴 + 𝐡 ) ∈ ℝ ) β†’ ( π‘₯ ∈ ( ( 𝐴 βˆ’ 𝐡 ) (,) ( 𝐴 + 𝐡 ) ) ↔ ( π‘₯ ∈ ℝ ∧ ( 𝐴 βˆ’ 𝐡 ) < π‘₯ ∧ π‘₯ < ( 𝐴 + 𝐡 ) ) ) )
28 22 23 27 syl2anc ⊒ ( ( 𝐴 ∈ ℝ ∧ 𝐡 ∈ ℝ ) β†’ ( π‘₯ ∈ ( ( 𝐴 βˆ’ 𝐡 ) (,) ( 𝐴 + 𝐡 ) ) ↔ ( π‘₯ ∈ ℝ ∧ ( 𝐴 βˆ’ 𝐡 ) < π‘₯ ∧ π‘₯ < ( 𝐴 + 𝐡 ) ) ) )
29 16 21 28 3bitr4d ⊒ ( ( 𝐴 ∈ ℝ ∧ 𝐡 ∈ ℝ ) β†’ ( π‘₯ ∈ ( 𝐴 ( ball β€˜ 𝐷 ) 𝐡 ) ↔ π‘₯ ∈ ( ( 𝐴 βˆ’ 𝐡 ) (,) ( 𝐴 + 𝐡 ) ) ) )
30 29 eqrdv ⊒ ( ( 𝐴 ∈ ℝ ∧ 𝐡 ∈ ℝ ) β†’ ( 𝐴 ( ball β€˜ 𝐷 ) 𝐡 ) = ( ( 𝐴 βˆ’ 𝐡 ) (,) ( 𝐴 + 𝐡 ) ) )