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 ⊢ R ∈ ℝ ∧ 0 ≤ R → t ∈ − R R ⟼ 2 ⁢ R 2 − t 2 ∈ 𝐿 1

Proof

Step Hyp Ref Expression
1 renegcl ⊢ R ∈ ℝ → − R ∈ ℝ
2 1 adantr ⊢ R ∈ ℝ ∧ 0 ≤ R → − R ∈ ℝ
3 simpl ⊢ R ∈ ℝ ∧ 0 ≤ R → R ∈ ℝ
4 2cnd ⊢ R ∈ ℝ ∧ 0 ≤ R → 2 ∈ ℂ
5 iccssre ⊢ − R ∈ ℝ ∧ R ∈ ℝ → − R R ⊆ ℝ
6 2 3 5 syl2anc ⊢ R ∈ ℝ ∧ 0 ≤ R → − R R ⊆ ℝ
7 ax-resscn ⊢ ℝ ⊆ ℂ
8 6 7 sstrdi ⊢ R ∈ ℝ ∧ 0 ≤ R → − R R ⊆ ℂ
9 ssidd ⊢ R ∈ ℝ ∧ 0 ≤ R → ℂ ⊆ ℂ
10 cncfmptc ⊢ 2 ∈ ℂ ∧ − R R ⊆ ℂ ∧ ℂ ⊆ ℂ → t ∈ − R R ⟼ 2 : − R R ⟶cn ℂ
11 4 8 9 10 syl3anc ⊢ R ∈ ℝ ∧ 0 ≤ R → t ∈ − R R ⟼ 2 : − R R ⟶cn ℂ
12 areacirclem2 ⊢ R ∈ ℝ ∧ 0 ≤ R → t ∈ − R R ⟼ R 2 − t 2 : − R R ⟶cn ℂ
13 11 12 mulcncf ⊢ R ∈ ℝ ∧ 0 ≤ R → t ∈ − R R ⟼ 2 ⁢ R 2 − t 2 : − R R ⟶cn ℂ
14 cnicciblnc ⊢ − R ∈ ℝ ∧ R ∈ ℝ ∧ t ∈ − R R ⟼ 2 ⁢ R 2 − t 2 : − R R ⟶cn ℂ → t ∈ − R R ⟼ 2 ⁢ R 2 − t 2 ∈ 𝐿 1
15 2 3 13 14 syl3anc ⊢ R ∈ ℝ ∧ 0 ≤ R → t ∈ − R R ⟼ 2 ⁢ R 2 − t 2 ∈ 𝐿 1