Theorem cnblcld

Description: Two ways to write the closed ball centered at zero. (Contributed by Mario Carneiro, 8-Sep-2015)

	Ref	Expression
Hypothesis	cnblcld.1	⊢ 𝐷 = ( abs ∘ − )
Assertion	cnblcld	⊢ ( 𝑅 ∈ ℝ* → ( ◡ abs “ ( 0 [,] 𝑅 ) ) = { 𝑥 ∈ ℂ ∣ ( 0 𝐷 𝑥 ) ≤ 𝑅 } )

Proof

Step	Hyp	Ref	Expression
1		cnblcld.1	⊢ 𝐷 = ( abs ∘ − )
2		absf	⊢ abs : ℂ ⟶ ℝ
3		ffn	⊢ ( abs : ℂ ⟶ ℝ → abs Fn ℂ )
4		elpreima	⊢ ( abs Fn ℂ → ( 𝑥 ∈ ( ◡ abs “ ( 0 [,] 𝑅 ) ) ↔ ( 𝑥 ∈ ℂ ∧ ( abs ‘ 𝑥 ) ∈ ( 0 [,] 𝑅 ) ) ) )
5	2 3 4	mp2b	⊢ ( 𝑥 ∈ ( ◡ abs “ ( 0 [,] 𝑅 ) ) ↔ ( 𝑥 ∈ ℂ ∧ ( abs ‘ 𝑥 ) ∈ ( 0 [,] 𝑅 ) ) )
6		df-3an	⊢ ( ( ( abs ‘ 𝑥 ) ∈ ℝ* ∧ 0 ≤ ( abs ‘ 𝑥 ) ∧ ( abs ‘ 𝑥 ) ≤ 𝑅 ) ↔ ( ( ( abs ‘ 𝑥 ) ∈ ℝ* ∧ 0 ≤ ( abs ‘ 𝑥 ) ) ∧ ( abs ‘ 𝑥 ) ≤ 𝑅 ) )
7		abscl	⊢ ( 𝑥 ∈ ℂ → ( abs ‘ 𝑥 ) ∈ ℝ )
8	7	rexrd	⊢ ( 𝑥 ∈ ℂ → ( abs ‘ 𝑥 ) ∈ ℝ* )
9		absge0	⊢ ( 𝑥 ∈ ℂ → 0 ≤ ( abs ‘ 𝑥 ) )
10	8 9	jca	⊢ ( 𝑥 ∈ ℂ → ( ( abs ‘ 𝑥 ) ∈ ℝ* ∧ 0 ≤ ( abs ‘ 𝑥 ) ) )
11	10	adantl	⊢ ( ( 𝑅 ∈ ℝ* ∧ 𝑥 ∈ ℂ ) → ( ( abs ‘ 𝑥 ) ∈ ℝ* ∧ 0 ≤ ( abs ‘ 𝑥 ) ) )
12	11	biantrurd	⊢ ( ( 𝑅 ∈ ℝ* ∧ 𝑥 ∈ ℂ ) → ( ( abs ‘ 𝑥 ) ≤ 𝑅 ↔ ( ( ( abs ‘ 𝑥 ) ∈ ℝ* ∧ 0 ≤ ( abs ‘ 𝑥 ) ) ∧ ( abs ‘ 𝑥 ) ≤ 𝑅 ) ) )
13	6 12	bitr4id	⊢ ( ( 𝑅 ∈ ℝ* ∧ 𝑥 ∈ ℂ ) → ( ( ( abs ‘ 𝑥 ) ∈ ℝ* ∧ 0 ≤ ( abs ‘ 𝑥 ) ∧ ( abs ‘ 𝑥 ) ≤ 𝑅 ) ↔ ( abs ‘ 𝑥 ) ≤ 𝑅 ) )
14		0xr	⊢ 0 ∈ ℝ*
15		simpl	⊢ ( ( 𝑅 ∈ ℝ* ∧ 𝑥 ∈ ℂ ) → 𝑅 ∈ ℝ* )
16		elicc1	⊢ ( ( 0 ∈ ℝ* ∧ 𝑅 ∈ ℝ* ) → ( ( abs ‘ 𝑥 ) ∈ ( 0 [,] 𝑅 ) ↔ ( ( abs ‘ 𝑥 ) ∈ ℝ* ∧ 0 ≤ ( abs ‘ 𝑥 ) ∧ ( abs ‘ 𝑥 ) ≤ 𝑅 ) ) )
17	14 15 16	sylancr	⊢ ( ( 𝑅 ∈ ℝ* ∧ 𝑥 ∈ ℂ ) → ( ( abs ‘ 𝑥 ) ∈ ( 0 [,] 𝑅 ) ↔ ( ( abs ‘ 𝑥 ) ∈ ℝ* ∧ 0 ≤ ( abs ‘ 𝑥 ) ∧ ( abs ‘ 𝑥 ) ≤ 𝑅 ) ) )
18		0cn	⊢ 0 ∈ ℂ
19	1	cnmetdval	⊢ ( ( 0 ∈ ℂ ∧ 𝑥 ∈ ℂ ) → ( 0 𝐷 𝑥 ) = ( abs ‘ ( 0 − 𝑥 ) ) )
20		abssub	⊢ ( ( 0 ∈ ℂ ∧ 𝑥 ∈ ℂ ) → ( abs ‘ ( 0 − 𝑥 ) ) = ( abs ‘ ( 𝑥 − 0 ) ) )
21	19 20	eqtrd	⊢ ( ( 0 ∈ ℂ ∧ 𝑥 ∈ ℂ ) → ( 0 𝐷 𝑥 ) = ( abs ‘ ( 𝑥 − 0 ) ) )
22	18 21	mpan	⊢ ( 𝑥 ∈ ℂ → ( 0 𝐷 𝑥 ) = ( abs ‘ ( 𝑥 − 0 ) ) )
23		subid1	⊢ ( 𝑥 ∈ ℂ → ( 𝑥 − 0 ) = 𝑥 )
24	23	fveq2d	⊢ ( 𝑥 ∈ ℂ → ( abs ‘ ( 𝑥 − 0 ) ) = ( abs ‘ 𝑥 ) )
25	22 24	eqtrd	⊢ ( 𝑥 ∈ ℂ → ( 0 𝐷 𝑥 ) = ( abs ‘ 𝑥 ) )
26	25	adantl	⊢ ( ( 𝑅 ∈ ℝ* ∧ 𝑥 ∈ ℂ ) → ( 0 𝐷 𝑥 ) = ( abs ‘ 𝑥 ) )
27	26	breq1d	⊢ ( ( 𝑅 ∈ ℝ* ∧ 𝑥 ∈ ℂ ) → ( ( 0 𝐷 𝑥 ) ≤ 𝑅 ↔ ( abs ‘ 𝑥 ) ≤ 𝑅 ) )
28	13 17 27	3bitr4d	⊢ ( ( 𝑅 ∈ ℝ* ∧ 𝑥 ∈ ℂ ) → ( ( abs ‘ 𝑥 ) ∈ ( 0 [,] 𝑅 ) ↔ ( 0 𝐷 𝑥 ) ≤ 𝑅 ) )
29	28	pm5.32da	⊢ ( 𝑅 ∈ ℝ* → ( ( 𝑥 ∈ ℂ ∧ ( abs ‘ 𝑥 ) ∈ ( 0 [,] 𝑅 ) ) ↔ ( 𝑥 ∈ ℂ ∧ ( 0 𝐷 𝑥 ) ≤ 𝑅 ) ) )
30	5 29	syl5bb	⊢ ( 𝑅 ∈ ℝ* → ( 𝑥 ∈ ( ◡ abs “ ( 0 [,] 𝑅 ) ) ↔ ( 𝑥 ∈ ℂ ∧ ( 0 𝐷 𝑥 ) ≤ 𝑅 ) ) )
31	30	abbi2dv	⊢ ( 𝑅 ∈ ℝ* → ( ◡ abs “ ( 0 [,] 𝑅 ) ) = { 𝑥 ∣ ( 𝑥 ∈ ℂ ∧ ( 0 𝐷 𝑥 ) ≤ 𝑅 ) } )
32		df-rab	⊢ { 𝑥 ∈ ℂ ∣ ( 0 𝐷 𝑥 ) ≤ 𝑅 } = { 𝑥 ∣ ( 𝑥 ∈ ℂ ∧ ( 0 𝐷 𝑥 ) ≤ 𝑅 ) }
33	31 32	eqtr4di	⊢ ( 𝑅 ∈ ℝ* → ( ◡ abs “ ( 0 [,] 𝑅 ) ) = { 𝑥 ∈ ℂ ∣ ( 0 𝐷 𝑥 ) ≤ 𝑅 } )