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	$⊢ (R \in ℝ \land 0 \leq R) \to (t \in [- R, R] ⟼ 2 \sqrt{R^{2} - t^{2}}) \in 𝐿^{1}$

Step	Hyp	Ref	Expression
1		renegcl	$⊢ R \in ℝ \to - R \in ℝ$
2	1	adantr	$⊢ (R \in ℝ \land 0 \leq R) \to - R \in ℝ$
3		simpl	$⊢ (R \in ℝ \land 0 \leq R) \to R \in ℝ$
4		2cnd	$⊢ (R \in ℝ \land 0 \leq R) \to 2 \in ℂ$
5		iccssre	$⊢ (- R \in ℝ \land R \in ℝ) \to [- R, R] \subseteq ℝ$
6	2 3 5	syl2anc	$⊢ (R \in ℝ \land 0 \leq R) \to [- R, R] \subseteq ℝ$
7		ax-resscn	$⊢ ℝ \subseteq ℂ$
8	6 7	sstrdi	$⊢ (R \in ℝ \land 0 \leq R) \to [- R, R] \subseteq ℂ$
9		ssidd	$⊢ (R \in ℝ \land 0 \leq R) \to ℂ \subseteq ℂ$
10		cncfmptc	$⊢ (2 \in ℂ \land [- R, R] \subseteq ℂ \land ℂ \subseteq ℂ) \to (t \in [- R, R] ⟼ 2) : [- R, R] \underset{cn}{⟶} ℂ$
11	4 8 9 10	syl3anc	$⊢ (R \in ℝ \land 0 \leq R) \to (t \in [- R, R] ⟼ 2) : [- R, R] \underset{cn}{⟶} ℂ$
12		areacirclem2	$⊢ (R \in ℝ \land 0 \leq R) \to (t \in [- R, R] ⟼ \sqrt{R^{2} - t^{2}}) : [- R, R] \underset{cn}{⟶} ℂ$
13	11 12	mulcncf	$⊢ (R \in ℝ \land 0 \leq R) \to (t \in [- R, R] ⟼ 2 \sqrt{R^{2} - t^{2}}) : [- R, R] \underset{cn}{⟶} ℂ$
14		cnicciblnc	$⊢ (- R \in ℝ \land R \in ℝ \land (t \in [- R, R] ⟼ 2 \sqrt{R^{2} - t^{2}}) : [- R, R] \underset{cn}{⟶} ℂ) \to (t \in [- R, R] ⟼ 2 \sqrt{R^{2} - t^{2}}) \in 𝐿^{1}$
15	2 3 13 14	syl3anc	$⊢ (R \in ℝ \land 0 \leq R) \to (t \in [- R, R] ⟼ 2 \sqrt{R^{2} - t^{2}}) \in 𝐿^{1}$

Metamath Proof Explorer