Theorem areacirclem3

Description: Integrability of cross-section of circle. (Contributed by Brendan Leahy, 26-Aug-2017) (Revised by Brendan Leahy, 11-Jul-2018)

	Ref	Expression
Assertion	areacirclem3	⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ) → ( 𝑡 ∈ ( - 𝑅 [,] 𝑅 ) ↦ ( 2 · ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) ) ∈ 𝐿1 )

Proof

Step	Hyp	Ref	Expression
1		renegcl	⊢ ( 𝑅 ∈ ℝ → - 𝑅 ∈ ℝ )
2	1	adantr	⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ) → - 𝑅 ∈ ℝ )
3		simpl	⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ) → 𝑅 ∈ ℝ )
4		2cnd	⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ) → 2 ∈ ℂ )
5		iccssre	⊢ ( ( - 𝑅 ∈ ℝ ∧ 𝑅 ∈ ℝ ) → ( - 𝑅 [,] 𝑅 ) ⊆ ℝ )
6	2 3 5	syl2anc	⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ) → ( - 𝑅 [,] 𝑅 ) ⊆ ℝ )
7		ax-resscn	⊢ ℝ ⊆ ℂ
8	6 7	sstrdi	⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ) → ( - 𝑅 [,] 𝑅 ) ⊆ ℂ )
9		ssidd	⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ) → ℂ ⊆ ℂ )
10		cncfmptc	⊢ ( ( 2 ∈ ℂ ∧ ( - 𝑅 [,] 𝑅 ) ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( 𝑡 ∈ ( - 𝑅 [,] 𝑅 ) ↦ 2 ) ∈ ( ( - 𝑅 [,] 𝑅 ) –cn→ ℂ ) )
11	4 8 9 10	syl3anc	⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ) → ( 𝑡 ∈ ( - 𝑅 [,] 𝑅 ) ↦ 2 ) ∈ ( ( - 𝑅 [,] 𝑅 ) –cn→ ℂ ) )
12		areacirclem2	⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ) → ( 𝑡 ∈ ( - 𝑅 [,] 𝑅 ) ↦ ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) ∈ ( ( - 𝑅 [,] 𝑅 ) –cn→ ℂ ) )
13	11 12	mulcncf	⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ) → ( 𝑡 ∈ ( - 𝑅 [,] 𝑅 ) ↦ ( 2 · ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) ) ∈ ( ( - 𝑅 [,] 𝑅 ) –cn→ ℂ ) )
14		cnicciblnc	⊢ ( ( - 𝑅 ∈ ℝ ∧ 𝑅 ∈ ℝ ∧ ( 𝑡 ∈ ( - 𝑅 [,] 𝑅 ) ↦ ( 2 · ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) ) ∈ ( ( - 𝑅 [,] 𝑅 ) –cn→ ℂ ) ) → ( 𝑡 ∈ ( - 𝑅 [,] 𝑅 ) ↦ ( 2 · ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) ) ∈ 𝐿1 )
15	2 3 13 14	syl3anc	⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ) → ( 𝑡 ∈ ( - 𝑅 [,] 𝑅 ) ↦ ( 2 · ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) ) ∈ 𝐿1 )