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 ) |