Metamath Proof Explorer


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 )