Step | Hyp | Ref
| Expression |
1 | | areacirc.1 |
. . . . . 6
⊢ 𝑆 = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ((𝑥↑2) + (𝑦↑2)) ≤ (𝑅↑2))} |
2 | | opabssxp 5116 |
. . . . . 6
⊢
{〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ((𝑥↑2) + (𝑦↑2)) ≤ (𝑅↑2))} ⊆ (ℝ ×
ℝ) |
3 | 1, 2 | eqsstri 3598 |
. . . . 5
⊢ 𝑆 ⊆ (ℝ ×
ℝ) |
4 | 3 | a1i 11 |
. . . 4
⊢ ((𝑅 ∈ ℝ ∧ 0 ≤
𝑅) → 𝑆 ⊆ (ℝ ×
ℝ)) |
5 | 1 | areacirclem5 32674 |
. . . . . . 7
⊢ ((𝑅 ∈ ℝ ∧ 0 ≤
𝑅 ∧ 𝑡 ∈ ℝ) → (𝑆 “ {𝑡}) = if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))),
∅)) |
6 | | resqcl 12793 |
. . . . . . . . . . . . . . 15
⊢ (𝑅 ∈ ℝ → (𝑅↑2) ∈
ℝ) |
7 | 6 | 3ad2ant1 1075 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ ℝ ∧ 0 ≤
𝑅 ∧ 𝑡 ∈ ℝ) → (𝑅↑2) ∈ ℝ) |
8 | | resqcl 12793 |
. . . . . . . . . . . . . . 15
⊢ (𝑡 ∈ ℝ → (𝑡↑2) ∈
ℝ) |
9 | 8 | 3ad2ant3 1077 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ ℝ ∧ 0 ≤
𝑅 ∧ 𝑡 ∈ ℝ) → (𝑡↑2) ∈ ℝ) |
10 | 7, 9 | resubcld 10337 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ ℝ ∧ 0 ≤
𝑅 ∧ 𝑡 ∈ ℝ) → ((𝑅↑2) − (𝑡↑2)) ∈ ℝ) |
11 | 10 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈ ℝ ∧ 0 ≤
𝑅 ∧ 𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → ((𝑅↑2) − (𝑡↑2)) ∈ ℝ) |
12 | | absresq 13890 |
. . . . . . . . . . . . . . . 16
⊢ (𝑡 ∈ ℝ →
((abs‘𝑡)↑2) =
(𝑡↑2)) |
13 | 12 | 3ad2ant3 1077 |
. . . . . . . . . . . . . . 15
⊢ ((𝑅 ∈ ℝ ∧ 0 ≤
𝑅 ∧ 𝑡 ∈ ℝ) → ((abs‘𝑡)↑2) = (𝑡↑2)) |
14 | 13 | breq1d 4593 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ ℝ ∧ 0 ≤
𝑅 ∧ 𝑡 ∈ ℝ) → (((abs‘𝑡)↑2) ≤ (𝑅↑2) ↔ (𝑡↑2) ≤ (𝑅↑2))) |
15 | | recn 9905 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑡 ∈ ℝ → 𝑡 ∈
ℂ) |
16 | 15 | abscld 14023 |
. . . . . . . . . . . . . . . 16
⊢ (𝑡 ∈ ℝ →
(abs‘𝑡) ∈
ℝ) |
17 | 16 | 3ad2ant3 1077 |
. . . . . . . . . . . . . . 15
⊢ ((𝑅 ∈ ℝ ∧ 0 ≤
𝑅 ∧ 𝑡 ∈ ℝ) → (abs‘𝑡) ∈
ℝ) |
18 | | simp1 1054 |
. . . . . . . . . . . . . . 15
⊢ ((𝑅 ∈ ℝ ∧ 0 ≤
𝑅 ∧ 𝑡 ∈ ℝ) → 𝑅 ∈ ℝ) |
19 | 15 | absge0d 14031 |
. . . . . . . . . . . . . . . 16
⊢ (𝑡 ∈ ℝ → 0 ≤
(abs‘𝑡)) |
20 | 19 | 3ad2ant3 1077 |
. . . . . . . . . . . . . . 15
⊢ ((𝑅 ∈ ℝ ∧ 0 ≤
𝑅 ∧ 𝑡 ∈ ℝ) → 0 ≤
(abs‘𝑡)) |
21 | | simp2 1055 |
. . . . . . . . . . . . . . 15
⊢ ((𝑅 ∈ ℝ ∧ 0 ≤
𝑅 ∧ 𝑡 ∈ ℝ) → 0 ≤ 𝑅) |
22 | 17, 18, 20, 21 | le2sqd 12906 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ ℝ ∧ 0 ≤
𝑅 ∧ 𝑡 ∈ ℝ) → ((abs‘𝑡) ≤ 𝑅 ↔ ((abs‘𝑡)↑2) ≤ (𝑅↑2))) |
23 | 7, 9 | subge0d 10496 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ ℝ ∧ 0 ≤
𝑅 ∧ 𝑡 ∈ ℝ) → (0 ≤ ((𝑅↑2) − (𝑡↑2)) ↔ (𝑡↑2) ≤ (𝑅↑2))) |
24 | 14, 22, 23 | 3bitr4d 299 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ ℝ ∧ 0 ≤
𝑅 ∧ 𝑡 ∈ ℝ) → ((abs‘𝑡) ≤ 𝑅 ↔ 0 ≤ ((𝑅↑2) − (𝑡↑2)))) |
25 | 24 | biimpa 500 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈ ℝ ∧ 0 ≤
𝑅 ∧ 𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → 0 ≤ ((𝑅↑2) − (𝑡↑2))) |
26 | 11, 25 | resqrtcld 14004 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ ℝ ∧ 0 ≤
𝑅 ∧ 𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → (√‘((𝑅↑2) − (𝑡↑2))) ∈ ℝ) |
27 | 26 | renegcld 10336 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ ℝ ∧ 0 ≤
𝑅 ∧ 𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → -(√‘((𝑅↑2) − (𝑡↑2))) ∈ ℝ) |
28 | | iccmbl 23141 |
. . . . . . . . . 10
⊢
((-(√‘((𝑅↑2) − (𝑡↑2))) ∈ ℝ ∧
(√‘((𝑅↑2)
− (𝑡↑2))) ∈
ℝ) → (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))) ∈ dom
vol) |
29 | 27, 26, 28 | syl2anc 691 |
. . . . . . . . 9
⊢ (((𝑅 ∈ ℝ ∧ 0 ≤
𝑅 ∧ 𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))) ∈ dom
vol) |
30 | | mblvol 23105 |
. . . . . . . . . . . 12
⊢
((-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))) ∈ dom vol
→ (vol‘(-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2))))) =
(vol*‘(-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))))) |
31 | 29, 30 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ ℝ ∧ 0 ≤
𝑅 ∧ 𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → (vol‘(-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2))))) =
(vol*‘(-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))))) |
32 | 11, 25 | sqrtge0d 14007 |
. . . . . . . . . . . . . 14
⊢ (((𝑅 ∈ ℝ ∧ 0 ≤
𝑅 ∧ 𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → 0 ≤ (√‘((𝑅↑2) − (𝑡↑2)))) |
33 | 26, 26, 32, 32 | addge0d 10482 |
. . . . . . . . . . . . 13
⊢ (((𝑅 ∈ ℝ ∧ 0 ≤
𝑅 ∧ 𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → 0 ≤ ((√‘((𝑅↑2) − (𝑡↑2))) +
(√‘((𝑅↑2)
− (𝑡↑2))))) |
34 | | recn 9905 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑅 ∈ ℝ → 𝑅 ∈
ℂ) |
35 | 34 | sqcld 12868 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑅 ∈ ℝ → (𝑅↑2) ∈
ℂ) |
36 | 35 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑅 ∈ ℝ ∧ 0 ≤
𝑅 ∧ 𝑡 ∈ ℝ) → (𝑅↑2) ∈ ℂ) |
37 | 15 | sqcld 12868 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑡 ∈ ℝ → (𝑡↑2) ∈
ℂ) |
38 | 37 | 3ad2ant3 1077 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑅 ∈ ℝ ∧ 0 ≤
𝑅 ∧ 𝑡 ∈ ℝ) → (𝑡↑2) ∈ ℂ) |
39 | 36, 38 | subcld 10271 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑅 ∈ ℝ ∧ 0 ≤
𝑅 ∧ 𝑡 ∈ ℝ) → ((𝑅↑2) − (𝑡↑2)) ∈ ℂ) |
40 | 39 | sqrtcld 14024 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑅 ∈ ℝ ∧ 0 ≤
𝑅 ∧ 𝑡 ∈ ℝ) →
(√‘((𝑅↑2)
− (𝑡↑2))) ∈
ℂ) |
41 | 40 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑅 ∈ ℝ ∧ 0 ≤
𝑅 ∧ 𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → (√‘((𝑅↑2) − (𝑡↑2))) ∈ ℂ) |
42 | 41, 41 | subnegd 10278 |
. . . . . . . . . . . . . . 15
⊢ (((𝑅 ∈ ℝ ∧ 0 ≤
𝑅 ∧ 𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → ((√‘((𝑅↑2) − (𝑡↑2))) − -(√‘((𝑅↑2) − (𝑡↑2)))) =
((√‘((𝑅↑2)
− (𝑡↑2))) +
(√‘((𝑅↑2)
− (𝑡↑2))))) |
43 | 42 | breq2d 4595 |
. . . . . . . . . . . . . 14
⊢ (((𝑅 ∈ ℝ ∧ 0 ≤
𝑅 ∧ 𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → (0 ≤ ((√‘((𝑅↑2) − (𝑡↑2))) −
-(√‘((𝑅↑2)
− (𝑡↑2))))
↔ 0 ≤ ((√‘((𝑅↑2) − (𝑡↑2))) + (√‘((𝑅↑2) − (𝑡↑2)))))) |
44 | 26, 27 | subge0d 10496 |
. . . . . . . . . . . . . 14
⊢ (((𝑅 ∈ ℝ ∧ 0 ≤
𝑅 ∧ 𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → (0 ≤ ((√‘((𝑅↑2) − (𝑡↑2))) −
-(√‘((𝑅↑2)
− (𝑡↑2))))
↔ -(√‘((𝑅↑2) − (𝑡↑2))) ≤ (√‘((𝑅↑2) − (𝑡↑2))))) |
45 | 43, 44 | bitr3d 269 |
. . . . . . . . . . . . 13
⊢ (((𝑅 ∈ ℝ ∧ 0 ≤
𝑅 ∧ 𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → (0 ≤ ((√‘((𝑅↑2) − (𝑡↑2))) +
(√‘((𝑅↑2)
− (𝑡↑2))))
↔ -(√‘((𝑅↑2) − (𝑡↑2))) ≤ (√‘((𝑅↑2) − (𝑡↑2))))) |
46 | 33, 45 | mpbid 221 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈ ℝ ∧ 0 ≤
𝑅 ∧ 𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → -(√‘((𝑅↑2) − (𝑡↑2))) ≤ (√‘((𝑅↑2) − (𝑡↑2)))) |
47 | | ovolicc 23098 |
. . . . . . . . . . . 12
⊢
((-(√‘((𝑅↑2) − (𝑡↑2))) ∈ ℝ ∧
(√‘((𝑅↑2)
− (𝑡↑2))) ∈
ℝ ∧ -(√‘((𝑅↑2) − (𝑡↑2))) ≤ (√‘((𝑅↑2) − (𝑡↑2)))) →
(vol*‘(-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2))))) =
((√‘((𝑅↑2)
− (𝑡↑2)))
− -(√‘((𝑅↑2) − (𝑡↑2))))) |
48 | 27, 26, 46, 47 | syl3anc 1318 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ ℝ ∧ 0 ≤
𝑅 ∧ 𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) →
(vol*‘(-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2))))) =
((√‘((𝑅↑2)
− (𝑡↑2)))
− -(√‘((𝑅↑2) − (𝑡↑2))))) |
49 | 31, 48 | eqtrd 2644 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ ℝ ∧ 0 ≤
𝑅 ∧ 𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → (vol‘(-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2))))) =
((√‘((𝑅↑2)
− (𝑡↑2)))
− -(√‘((𝑅↑2) − (𝑡↑2))))) |
50 | 26, 27 | resubcld 10337 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ ℝ ∧ 0 ≤
𝑅 ∧ 𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → ((√‘((𝑅↑2) − (𝑡↑2))) − -(√‘((𝑅↑2) − (𝑡↑2)))) ∈
ℝ) |
51 | 49, 50 | eqeltrd 2688 |
. . . . . . . . 9
⊢ (((𝑅 ∈ ℝ ∧ 0 ≤
𝑅 ∧ 𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → (vol‘(-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2))))) ∈
ℝ) |
52 | | volf 23104 |
. . . . . . . . . 10
⊢ vol:dom
vol⟶(0[,]+∞) |
53 | | ffn 5958 |
. . . . . . . . . 10
⊢ (vol:dom
vol⟶(0[,]+∞) → vol Fn dom vol) |
54 | | elpreima 6245 |
. . . . . . . . . 10
⊢ (vol Fn
dom vol → ((-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))) ∈ (◡vol “ ℝ) ↔
((-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))) ∈ dom vol ∧
(vol‘(-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2))))) ∈
ℝ))) |
55 | 52, 53, 54 | mp2b 10 |
. . . . . . . . 9
⊢
((-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))) ∈ (◡vol “ ℝ) ↔
((-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))) ∈ dom vol ∧
(vol‘(-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2))))) ∈
ℝ)) |
56 | 29, 51, 55 | sylanbrc 695 |
. . . . . . . 8
⊢ (((𝑅 ∈ ℝ ∧ 0 ≤
𝑅 ∧ 𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))) ∈ (◡vol “ ℝ)) |
57 | | 0mbl 23114 |
. . . . . . . . . 10
⊢ ∅
∈ dom vol |
58 | | mblvol 23105 |
. . . . . . . . . . . . 13
⊢ (∅
∈ dom vol → (vol‘∅) =
(vol*‘∅)) |
59 | 57, 58 | ax-mp 5 |
. . . . . . . . . . . 12
⊢
(vol‘∅) = (vol*‘∅) |
60 | | ovol0 23068 |
. . . . . . . . . . . 12
⊢
(vol*‘∅) = 0 |
61 | 59, 60 | eqtri 2632 |
. . . . . . . . . . 11
⊢
(vol‘∅) = 0 |
62 | | 0re 9919 |
. . . . . . . . . . 11
⊢ 0 ∈
ℝ |
63 | 61, 62 | eqeltri 2684 |
. . . . . . . . . 10
⊢
(vol‘∅) ∈ ℝ |
64 | | elpreima 6245 |
. . . . . . . . . . 11
⊢ (vol Fn
dom vol → (∅ ∈ (◡vol
“ ℝ) ↔ (∅ ∈ dom vol ∧ (vol‘∅)
∈ ℝ))) |
65 | 52, 53, 64 | mp2b 10 |
. . . . . . . . . 10
⊢ (∅
∈ (◡vol “ ℝ) ↔
(∅ ∈ dom vol ∧ (vol‘∅) ∈
ℝ)) |
66 | 57, 63, 65 | mpbir2an 957 |
. . . . . . . . 9
⊢ ∅
∈ (◡vol “
ℝ) |
67 | 66 | a1i 11 |
. . . . . . . 8
⊢ (((𝑅 ∈ ℝ ∧ 0 ≤
𝑅 ∧ 𝑡 ∈ ℝ) ∧ ¬ (abs‘𝑡) ≤ 𝑅) → ∅ ∈ (◡vol “ ℝ)) |
68 | 56, 67 | ifclda 4070 |
. . . . . . 7
⊢ ((𝑅 ∈ ℝ ∧ 0 ≤
𝑅 ∧ 𝑡 ∈ ℝ) → if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅) ∈
(◡vol “
ℝ)) |
69 | 5, 68 | eqeltrd 2688 |
. . . . . 6
⊢ ((𝑅 ∈ ℝ ∧ 0 ≤
𝑅 ∧ 𝑡 ∈ ℝ) → (𝑆 “ {𝑡}) ∈ (◡vol “ ℝ)) |
70 | 69 | 3expa 1257 |
. . . . 5
⊢ (((𝑅 ∈ ℝ ∧ 0 ≤
𝑅) ∧ 𝑡 ∈ ℝ) → (𝑆 “ {𝑡}) ∈ (◡vol “ ℝ)) |
71 | 70 | ralrimiva 2949 |
. . . 4
⊢ ((𝑅 ∈ ℝ ∧ 0 ≤
𝑅) → ∀𝑡 ∈ ℝ (𝑆 “ {𝑡}) ∈ (◡vol “ ℝ)) |
72 | 5 | fveq2d 6107 |
. . . . . . 7
⊢ ((𝑅 ∈ ℝ ∧ 0 ≤
𝑅 ∧ 𝑡 ∈ ℝ) → (vol‘(𝑆 “ {𝑡})) = (vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))),
∅))) |
73 | 72 | 3expa 1257 |
. . . . . 6
⊢ (((𝑅 ∈ ℝ ∧ 0 ≤
𝑅) ∧ 𝑡 ∈ ℝ) → (vol‘(𝑆 “ {𝑡})) = (vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))),
∅))) |
74 | 73 | mpteq2dva 4672 |
. . . . 5
⊢ ((𝑅 ∈ ℝ ∧ 0 ≤
𝑅) → (𝑡 ∈ ℝ ↦
(vol‘(𝑆 “
{𝑡}))) = (𝑡 ∈ ℝ ↦
(vol‘if((abs‘𝑡)
≤ 𝑅,
(-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))),
∅)))) |
75 | | renegcl 10223 |
. . . . . . . 8
⊢ (𝑅 ∈ ℝ → -𝑅 ∈
ℝ) |
76 | 75 | adantr 480 |
. . . . . . 7
⊢ ((𝑅 ∈ ℝ ∧ 0 ≤
𝑅) → -𝑅 ∈
ℝ) |
77 | | simpl 472 |
. . . . . . 7
⊢ ((𝑅 ∈ ℝ ∧ 0 ≤
𝑅) → 𝑅 ∈ ℝ) |
78 | | iccssre 12126 |
. . . . . . 7
⊢ ((-𝑅 ∈ ℝ ∧ 𝑅 ∈ ℝ) → (-𝑅[,]𝑅) ⊆ ℝ) |
79 | 76, 77, 78 | syl2anc 691 |
. . . . . 6
⊢ ((𝑅 ∈ ℝ ∧ 0 ≤
𝑅) → (-𝑅[,]𝑅) ⊆ ℝ) |
80 | | rembl 23115 |
. . . . . . 7
⊢ ℝ
∈ dom vol |
81 | 80 | a1i 11 |
. . . . . 6
⊢ ((𝑅 ∈ ℝ ∧ 0 ≤
𝑅) → ℝ ∈
dom vol) |
82 | | fvex 6113 |
. . . . . . 7
⊢
(vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) ∈
V |
83 | 82 | a1i 11 |
. . . . . 6
⊢ (((𝑅 ∈ ℝ ∧ 0 ≤
𝑅) ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) ∈
V) |
84 | | eldif 3550 |
. . . . . . . . 9
⊢ (𝑡 ∈ (ℝ ∖ (-𝑅[,]𝑅)) ↔ (𝑡 ∈ ℝ ∧ ¬ 𝑡 ∈ (-𝑅[,]𝑅))) |
85 | | 3anass 1035 |
. . . . . . . . . . . . . . 15
⊢ ((𝑡 ∈ ℝ ∧ -𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅) ↔ (𝑡 ∈ ℝ ∧ (-𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅))) |
86 | 85 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ ℝ ∧ 0 ≤
𝑅 ∧ 𝑡 ∈ ℝ) → ((𝑡 ∈ ℝ ∧ -𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅) ↔ (𝑡 ∈ ℝ ∧ (-𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅)))) |
87 | 75 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . 15
⊢ ((𝑅 ∈ ℝ ∧ 0 ≤
𝑅 ∧ 𝑡 ∈ ℝ) → -𝑅 ∈ ℝ) |
88 | | elicc2 12109 |
. . . . . . . . . . . . . . 15
⊢ ((-𝑅 ∈ ℝ ∧ 𝑅 ∈ ℝ) → (𝑡 ∈ (-𝑅[,]𝑅) ↔ (𝑡 ∈ ℝ ∧ -𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅))) |
89 | 87, 18, 88 | syl2anc 691 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ ℝ ∧ 0 ≤
𝑅 ∧ 𝑡 ∈ ℝ) → (𝑡 ∈ (-𝑅[,]𝑅) ↔ (𝑡 ∈ ℝ ∧ -𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅))) |
90 | | simp3 1056 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑅 ∈ ℝ ∧ 0 ≤
𝑅 ∧ 𝑡 ∈ ℝ) → 𝑡 ∈ ℝ) |
91 | 90, 18 | absled 14017 |
. . . . . . . . . . . . . . 15
⊢ ((𝑅 ∈ ℝ ∧ 0 ≤
𝑅 ∧ 𝑡 ∈ ℝ) → ((abs‘𝑡) ≤ 𝑅 ↔ (-𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅))) |
92 | 90 | biantrurd 528 |
. . . . . . . . . . . . . . 15
⊢ ((𝑅 ∈ ℝ ∧ 0 ≤
𝑅 ∧ 𝑡 ∈ ℝ) → ((-𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅) ↔ (𝑡 ∈ ℝ ∧ (-𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅)))) |
93 | 91, 92 | bitrd 267 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ ℝ ∧ 0 ≤
𝑅 ∧ 𝑡 ∈ ℝ) → ((abs‘𝑡) ≤ 𝑅 ↔ (𝑡 ∈ ℝ ∧ (-𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅)))) |
94 | 86, 89, 93 | 3bitr4rd 300 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ ℝ ∧ 0 ≤
𝑅 ∧ 𝑡 ∈ ℝ) → ((abs‘𝑡) ≤ 𝑅 ↔ 𝑡 ∈ (-𝑅[,]𝑅))) |
95 | 94 | biimpd 218 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ ℝ ∧ 0 ≤
𝑅 ∧ 𝑡 ∈ ℝ) → ((abs‘𝑡) ≤ 𝑅 → 𝑡 ∈ (-𝑅[,]𝑅))) |
96 | 95 | con3d 147 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ ℝ ∧ 0 ≤
𝑅 ∧ 𝑡 ∈ ℝ) → (¬ 𝑡 ∈ (-𝑅[,]𝑅) → ¬ (abs‘𝑡) ≤ 𝑅)) |
97 | 96 | 3expia 1259 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ ℝ ∧ 0 ≤
𝑅) → (𝑡 ∈ ℝ → (¬
𝑡 ∈ (-𝑅[,]𝑅) → ¬ (abs‘𝑡) ≤ 𝑅))) |
98 | 97 | impd 446 |
. . . . . . . . 9
⊢ ((𝑅 ∈ ℝ ∧ 0 ≤
𝑅) → ((𝑡 ∈ ℝ ∧ ¬
𝑡 ∈ (-𝑅[,]𝑅)) → ¬ (abs‘𝑡) ≤ 𝑅)) |
99 | 84, 98 | syl5bi 231 |
. . . . . . . 8
⊢ ((𝑅 ∈ ℝ ∧ 0 ≤
𝑅) → (𝑡 ∈ (ℝ ∖ (-𝑅[,]𝑅)) → ¬ (abs‘𝑡) ≤ 𝑅)) |
100 | 99 | imp 444 |
. . . . . . 7
⊢ (((𝑅 ∈ ℝ ∧ 0 ≤
𝑅) ∧ 𝑡 ∈ (ℝ ∖ (-𝑅[,]𝑅))) → ¬ (abs‘𝑡) ≤ 𝑅) |
101 | | iffalse 4045 |
. . . . . . . . 9
⊢ (¬
(abs‘𝑡) ≤ 𝑅 → if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅) =
∅) |
102 | 101 | fveq2d 6107 |
. . . . . . . 8
⊢ (¬
(abs‘𝑡) ≤ 𝑅 →
(vol‘if((abs‘𝑡)
≤ 𝑅,
(-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) =
(vol‘∅)) |
103 | 102, 61 | syl6eq 2660 |
. . . . . . 7
⊢ (¬
(abs‘𝑡) ≤ 𝑅 →
(vol‘if((abs‘𝑡)
≤ 𝑅,
(-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) =
0) |
104 | 100, 103 | syl 17 |
. . . . . 6
⊢ (((𝑅 ∈ ℝ ∧ 0 ≤
𝑅) ∧ 𝑡 ∈ (ℝ ∖ (-𝑅[,]𝑅))) → (vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) =
0) |
105 | 76, 77, 88 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ ℝ ∧ 0 ≤
𝑅) → (𝑡 ∈ (-𝑅[,]𝑅) ↔ (𝑡 ∈ ℝ ∧ -𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅))) |
106 | 91 | biimprd 237 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑅 ∈ ℝ ∧ 0 ≤
𝑅 ∧ 𝑡 ∈ ℝ) → ((-𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅) → (abs‘𝑡) ≤ 𝑅)) |
107 | 106 | expd 451 |
. . . . . . . . . . . . . . 15
⊢ ((𝑅 ∈ ℝ ∧ 0 ≤
𝑅 ∧ 𝑡 ∈ ℝ) → (-𝑅 ≤ 𝑡 → (𝑡 ≤ 𝑅 → (abs‘𝑡) ≤ 𝑅))) |
108 | 107 | 3expia 1259 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ ℝ ∧ 0 ≤
𝑅) → (𝑡 ∈ ℝ → (-𝑅 ≤ 𝑡 → (𝑡 ≤ 𝑅 → (abs‘𝑡) ≤ 𝑅)))) |
109 | 108 | 3impd 1273 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ ℝ ∧ 0 ≤
𝑅) → ((𝑡 ∈ ℝ ∧ -𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅) → (abs‘𝑡) ≤ 𝑅)) |
110 | 105, 109 | sylbid 229 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ ℝ ∧ 0 ≤
𝑅) → (𝑡 ∈ (-𝑅[,]𝑅) → (abs‘𝑡) ≤ 𝑅)) |
111 | 110 | 3impia 1253 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ ℝ ∧ 0 ≤
𝑅 ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (abs‘𝑡) ≤ 𝑅) |
112 | | iftrue 4042 |
. . . . . . . . . . . 12
⊢
((abs‘𝑡) ≤
𝑅 →
if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅) =
(-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2))))) |
113 | 112 | fveq2d 6107 |
. . . . . . . . . . 11
⊢
((abs‘𝑡) ≤
𝑅 →
(vol‘if((abs‘𝑡)
≤ 𝑅,
(-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) =
(vol‘(-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))))) |
114 | 111, 113 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ ℝ ∧ 0 ≤
𝑅 ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) =
(vol‘(-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))))) |
115 | 6 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . 15
⊢ ((𝑅 ∈ ℝ ∧ 0 ≤
𝑅 ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (𝑅↑2) ∈ ℝ) |
116 | 75, 78 | mpancom 700 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑅 ∈ ℝ → (-𝑅[,]𝑅) ⊆ ℝ) |
117 | 116 | sselda 3568 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑅 ∈ ℝ ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → 𝑡 ∈ ℝ) |
118 | 117 | 3adant2 1073 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑅 ∈ ℝ ∧ 0 ≤
𝑅 ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → 𝑡 ∈ ℝ) |
119 | 118 | resqcld 12897 |
. . . . . . . . . . . . . . 15
⊢ ((𝑅 ∈ ℝ ∧ 0 ≤
𝑅 ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (𝑡↑2) ∈ ℝ) |
120 | 115, 119 | resubcld 10337 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ ℝ ∧ 0 ≤
𝑅 ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑅↑2) − (𝑡↑2)) ∈ ℝ) |
121 | 75, 88 | mpancom 700 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑅 ∈ ℝ → (𝑡 ∈ (-𝑅[,]𝑅) ↔ (𝑡 ∈ ℝ ∧ -𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅))) |
122 | 121 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑅 ∈ ℝ ∧ 0 ≤
𝑅) → (𝑡 ∈ (-𝑅[,]𝑅) ↔ (𝑡 ∈ ℝ ∧ -𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅))) |
123 | 22, 91, 14 | 3bitr3rd 298 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑅 ∈ ℝ ∧ 0 ≤
𝑅 ∧ 𝑡 ∈ ℝ) → ((𝑡↑2) ≤ (𝑅↑2) ↔ (-𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅))) |
124 | 23, 123 | bitrd 267 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑅 ∈ ℝ ∧ 0 ≤
𝑅 ∧ 𝑡 ∈ ℝ) → (0 ≤ ((𝑅↑2) − (𝑡↑2)) ↔ (-𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅))) |
125 | 124 | biimprd 237 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑅 ∈ ℝ ∧ 0 ≤
𝑅 ∧ 𝑡 ∈ ℝ) → ((-𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅) → 0 ≤ ((𝑅↑2) − (𝑡↑2)))) |
126 | 125 | expd 451 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑅 ∈ ℝ ∧ 0 ≤
𝑅 ∧ 𝑡 ∈ ℝ) → (-𝑅 ≤ 𝑡 → (𝑡 ≤ 𝑅 → 0 ≤ ((𝑅↑2) − (𝑡↑2))))) |
127 | 126 | 3expia 1259 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑅 ∈ ℝ ∧ 0 ≤
𝑅) → (𝑡 ∈ ℝ → (-𝑅 ≤ 𝑡 → (𝑡 ≤ 𝑅 → 0 ≤ ((𝑅↑2) − (𝑡↑2)))))) |
128 | 127 | 3impd 1273 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑅 ∈ ℝ ∧ 0 ≤
𝑅) → ((𝑡 ∈ ℝ ∧ -𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅) → 0 ≤ ((𝑅↑2) − (𝑡↑2)))) |
129 | 122, 128 | sylbid 229 |
. . . . . . . . . . . . . . 15
⊢ ((𝑅 ∈ ℝ ∧ 0 ≤
𝑅) → (𝑡 ∈ (-𝑅[,]𝑅) → 0 ≤ ((𝑅↑2) − (𝑡↑2)))) |
130 | 129 | 3impia 1253 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ ℝ ∧ 0 ≤
𝑅 ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → 0 ≤ ((𝑅↑2) − (𝑡↑2))) |
131 | 120, 130 | resqrtcld 14004 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ ℝ ∧ 0 ≤
𝑅 ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (√‘((𝑅↑2) − (𝑡↑2))) ∈ ℝ) |
132 | 131 | renegcld 10336 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ ℝ ∧ 0 ≤
𝑅 ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → -(√‘((𝑅↑2) − (𝑡↑2))) ∈
ℝ) |
133 | 132, 131,
28 | syl2anc 691 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ ℝ ∧ 0 ≤
𝑅 ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))) ∈ dom
vol) |
134 | 133, 30 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ ℝ ∧ 0 ≤
𝑅 ∧ 𝑡 ∈ (-𝑅[,]𝑅)) →
(vol‘(-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2))))) =
(vol*‘(-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))))) |
135 | 120 | recnd 9947 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ ℝ ∧ 0 ≤
𝑅 ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑅↑2) − (𝑡↑2)) ∈ ℂ) |
136 | 135 | sqrtcld 14024 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ ℝ ∧ 0 ≤
𝑅 ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (√‘((𝑅↑2) − (𝑡↑2))) ∈ ℂ) |
137 | 136, 136 | subnegd 10278 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ ℝ ∧ 0 ≤
𝑅 ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → ((√‘((𝑅↑2) − (𝑡↑2))) −
-(√‘((𝑅↑2)
− (𝑡↑2)))) =
((√‘((𝑅↑2)
− (𝑡↑2))) +
(√‘((𝑅↑2)
− (𝑡↑2))))) |
138 | 120, 130 | sqrtge0d 14007 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ ℝ ∧ 0 ≤
𝑅 ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → 0 ≤ (√‘((𝑅↑2) − (𝑡↑2)))) |
139 | 131, 131,
138, 138 | addge0d 10482 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ ℝ ∧ 0 ≤
𝑅 ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → 0 ≤ ((√‘((𝑅↑2) − (𝑡↑2))) +
(√‘((𝑅↑2)
− (𝑡↑2))))) |
140 | 137 | breq2d 4595 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ ℝ ∧ 0 ≤
𝑅 ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (0 ≤ ((√‘((𝑅↑2) − (𝑡↑2))) −
-(√‘((𝑅↑2)
− (𝑡↑2))))
↔ 0 ≤ ((√‘((𝑅↑2) − (𝑡↑2))) + (√‘((𝑅↑2) − (𝑡↑2)))))) |
141 | 131, 132 | subge0d 10496 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ ℝ ∧ 0 ≤
𝑅 ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (0 ≤ ((√‘((𝑅↑2) − (𝑡↑2))) −
-(√‘((𝑅↑2)
− (𝑡↑2))))
↔ -(√‘((𝑅↑2) − (𝑡↑2))) ≤ (√‘((𝑅↑2) − (𝑡↑2))))) |
142 | 140, 141 | bitr3d 269 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ ℝ ∧ 0 ≤
𝑅 ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (0 ≤ ((√‘((𝑅↑2) − (𝑡↑2))) +
(√‘((𝑅↑2)
− (𝑡↑2))))
↔ -(√‘((𝑅↑2) − (𝑡↑2))) ≤ (√‘((𝑅↑2) − (𝑡↑2))))) |
143 | 139, 142 | mpbid 221 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ ℝ ∧ 0 ≤
𝑅 ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → -(√‘((𝑅↑2) − (𝑡↑2))) ≤
(√‘((𝑅↑2)
− (𝑡↑2)))) |
144 | 132, 131,
143, 47 | syl3anc 1318 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ ℝ ∧ 0 ≤
𝑅 ∧ 𝑡 ∈ (-𝑅[,]𝑅)) →
(vol*‘(-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2))))) =
((√‘((𝑅↑2)
− (𝑡↑2)))
− -(√‘((𝑅↑2) − (𝑡↑2))))) |
145 | 136 | 2timesd 11152 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ ℝ ∧ 0 ≤
𝑅 ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (2 · (√‘((𝑅↑2) − (𝑡↑2)))) =
((√‘((𝑅↑2)
− (𝑡↑2))) +
(√‘((𝑅↑2)
− (𝑡↑2))))) |
146 | 137, 144,
145 | 3eqtr4d 2654 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ ℝ ∧ 0 ≤
𝑅 ∧ 𝑡 ∈ (-𝑅[,]𝑅)) →
(vol*‘(-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2))))) = (2 ·
(√‘((𝑅↑2)
− (𝑡↑2))))) |
147 | 114, 134,
146 | 3eqtrd 2648 |
. . . . . . . . 9
⊢ ((𝑅 ∈ ℝ ∧ 0 ≤
𝑅 ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) = (2
· (√‘((𝑅↑2) − (𝑡↑2))))) |
148 | 147 | 3expa 1257 |
. . . . . . . 8
⊢ (((𝑅 ∈ ℝ ∧ 0 ≤
𝑅) ∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) = (2
· (√‘((𝑅↑2) − (𝑡↑2))))) |
149 | 148 | mpteq2dva 4672 |
. . . . . . 7
⊢ ((𝑅 ∈ ℝ ∧ 0 ≤
𝑅) → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅))) = (𝑡 ∈ (-𝑅[,]𝑅) ↦ (2 · (√‘((𝑅↑2) − (𝑡↑2)))))) |
150 | | areacirclem3 32672 |
. . . . . . 7
⊢ ((𝑅 ∈ ℝ ∧ 0 ≤
𝑅) → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (2 · (√‘((𝑅↑2) − (𝑡↑2))))) ∈
𝐿1) |
151 | 149, 150 | eqeltrd 2688 |
. . . . . 6
⊢ ((𝑅 ∈ ℝ ∧ 0 ≤
𝑅) → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅))) ∈
𝐿1) |
152 | 79, 81, 83, 104, 151 | iblss2 23378 |
. . . . 5
⊢ ((𝑅 ∈ ℝ ∧ 0 ≤
𝑅) → (𝑡 ∈ ℝ ↦
(vol‘if((abs‘𝑡)
≤ 𝑅,
(-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅))) ∈
𝐿1) |
153 | 74, 152 | eqeltrd 2688 |
. . . 4
⊢ ((𝑅 ∈ ℝ ∧ 0 ≤
𝑅) → (𝑡 ∈ ℝ ↦
(vol‘(𝑆 “
{𝑡}))) ∈
𝐿1) |
154 | | dmarea 24484 |
. . . 4
⊢ (𝑆 ∈ dom area ↔ (𝑆 ⊆ (ℝ ×
ℝ) ∧ ∀𝑡
∈ ℝ (𝑆 “
{𝑡}) ∈ (◡vol “ ℝ) ∧ (𝑡 ∈ ℝ ↦
(vol‘(𝑆 “
{𝑡}))) ∈
𝐿1)) |
155 | 4, 71, 153, 154 | syl3anbrc 1239 |
. . 3
⊢ ((𝑅 ∈ ℝ ∧ 0 ≤
𝑅) → 𝑆 ∈ dom area) |
156 | | areaval 24491 |
. . 3
⊢ (𝑆 ∈ dom area →
(area‘𝑆) =
∫ℝ(vol‘(𝑆
“ {𝑡})) d𝑡) |
157 | 155, 156 | syl 17 |
. 2
⊢ ((𝑅 ∈ ℝ ∧ 0 ≤
𝑅) → (area‘𝑆) =
∫ℝ(vol‘(𝑆
“ {𝑡})) d𝑡) |
158 | | elioore 12076 |
. . . . . 6
⊢ (𝑡 ∈ (-𝑅(,)𝑅) → 𝑡 ∈ ℝ) |
159 | 5 | 3expa 1257 |
. . . . . 6
⊢ (((𝑅 ∈ ℝ ∧ 0 ≤
𝑅) ∧ 𝑡 ∈ ℝ) → (𝑆 “ {𝑡}) = if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))),
∅)) |
160 | 158, 159 | sylan2 490 |
. . . . 5
⊢ (((𝑅 ∈ ℝ ∧ 0 ≤
𝑅) ∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (𝑆 “ {𝑡}) = if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))),
∅)) |
161 | 160 | fveq2d 6107 |
. . . 4
⊢ (((𝑅 ∈ ℝ ∧ 0 ≤
𝑅) ∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (vol‘(𝑆 “ {𝑡})) = (vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))),
∅))) |
162 | 161 | itgeq2dv 23354 |
. . 3
⊢ ((𝑅 ∈ ℝ ∧ 0 ≤
𝑅) → ∫(-𝑅(,)𝑅)(vol‘(𝑆 “ {𝑡})) d𝑡 = ∫(-𝑅(,)𝑅)(vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) d𝑡) |
163 | | ioossre 12106 |
. . . . 5
⊢ (-𝑅(,)𝑅) ⊆ ℝ |
164 | 163 | a1i 11 |
. . . 4
⊢ ((𝑅 ∈ ℝ ∧ 0 ≤
𝑅) → (-𝑅(,)𝑅) ⊆ ℝ) |
165 | | eldif 3550 |
. . . . . 6
⊢ (𝑡 ∈ (ℝ ∖ (-𝑅(,)𝑅)) ↔ (𝑡 ∈ ℝ ∧ ¬ 𝑡 ∈ (-𝑅(,)𝑅))) |
166 | 75 | rexrd 9968 |
. . . . . . . . . . . . . 14
⊢ (𝑅 ∈ ℝ → -𝑅 ∈
ℝ*) |
167 | | rexr 9964 |
. . . . . . . . . . . . . 14
⊢ (𝑅 ∈ ℝ → 𝑅 ∈
ℝ*) |
168 | | elioo2 12087 |
. . . . . . . . . . . . . 14
⊢ ((-𝑅 ∈ ℝ*
∧ 𝑅 ∈
ℝ*) → (𝑡 ∈ (-𝑅(,)𝑅) ↔ (𝑡 ∈ ℝ ∧ -𝑅 < 𝑡 ∧ 𝑡 < 𝑅))) |
169 | 166, 167,
168 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ (𝑅 ∈ ℝ → (𝑡 ∈ (-𝑅(,)𝑅) ↔ (𝑡 ∈ ℝ ∧ -𝑅 < 𝑡 ∧ 𝑡 < 𝑅))) |
170 | 169 | 3ad2ant1 1075 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ ℝ ∧ 0 ≤
𝑅 ∧ 𝑡 ∈ ℝ) → (𝑡 ∈ (-𝑅(,)𝑅) ↔ (𝑡 ∈ ℝ ∧ -𝑅 < 𝑡 ∧ 𝑡 < 𝑅))) |
171 | 90 | biantrurd 528 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ ℝ ∧ 0 ≤
𝑅 ∧ 𝑡 ∈ ℝ) → ((-𝑅 < 𝑡 ∧ 𝑡 < 𝑅) ↔ (𝑡 ∈ ℝ ∧ (-𝑅 < 𝑡 ∧ 𝑡 < 𝑅)))) |
172 | 90, 18 | absltd 14016 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ ℝ ∧ 0 ≤
𝑅 ∧ 𝑡 ∈ ℝ) → ((abs‘𝑡) < 𝑅 ↔ (-𝑅 < 𝑡 ∧ 𝑡 < 𝑅))) |
173 | | 3anass 1035 |
. . . . . . . . . . . . . 14
⊢ ((𝑡 ∈ ℝ ∧ -𝑅 < 𝑡 ∧ 𝑡 < 𝑅) ↔ (𝑡 ∈ ℝ ∧ (-𝑅 < 𝑡 ∧ 𝑡 < 𝑅))) |
174 | 173 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ ℝ ∧ 0 ≤
𝑅 ∧ 𝑡 ∈ ℝ) → ((𝑡 ∈ ℝ ∧ -𝑅 < 𝑡 ∧ 𝑡 < 𝑅) ↔ (𝑡 ∈ ℝ ∧ (-𝑅 < 𝑡 ∧ 𝑡 < 𝑅)))) |
175 | 171, 172,
174 | 3bitr4rd 300 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ ℝ ∧ 0 ≤
𝑅 ∧ 𝑡 ∈ ℝ) → ((𝑡 ∈ ℝ ∧ -𝑅 < 𝑡 ∧ 𝑡 < 𝑅) ↔ (abs‘𝑡) < 𝑅)) |
176 | 170, 175 | bitrd 267 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ ℝ ∧ 0 ≤
𝑅 ∧ 𝑡 ∈ ℝ) → (𝑡 ∈ (-𝑅(,)𝑅) ↔ (abs‘𝑡) < 𝑅)) |
177 | 176 | notbid 307 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ ℝ ∧ 0 ≤
𝑅 ∧ 𝑡 ∈ ℝ) → (¬ 𝑡 ∈ (-𝑅(,)𝑅) ↔ ¬ (abs‘𝑡) < 𝑅)) |
178 | 18, 17 | lenltd 10062 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ ℝ ∧ 0 ≤
𝑅 ∧ 𝑡 ∈ ℝ) → (𝑅 ≤ (abs‘𝑡) ↔ ¬ (abs‘𝑡) < 𝑅)) |
179 | 177, 178 | bitr4d 270 |
. . . . . . . . 9
⊢ ((𝑅 ∈ ℝ ∧ 0 ≤
𝑅 ∧ 𝑡 ∈ ℝ) → (¬ 𝑡 ∈ (-𝑅(,)𝑅) ↔ 𝑅 ≤ (abs‘𝑡))) |
180 | 5 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈ ℝ ∧ 0 ≤
𝑅 ∧ 𝑡 ∈ ℝ) ∧ 𝑅 ≤ (abs‘𝑡)) → (𝑆 “ {𝑡}) = if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))),
∅)) |
181 | 180 | fveq2d 6107 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ ℝ ∧ 0 ≤
𝑅 ∧ 𝑡 ∈ ℝ) ∧ 𝑅 ≤ (abs‘𝑡)) → (vol‘(𝑆 “ {𝑡})) = (vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))),
∅))) |
182 | 17 | anim1i 590 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑅 ∈ ℝ ∧ 0 ≤
𝑅 ∧ 𝑡 ∈ ℝ) ∧ (abs‘𝑡) = 𝑅) → ((abs‘𝑡) ∈ ℝ ∧ (abs‘𝑡) = 𝑅)) |
183 | | eqle 10018 |
. . . . . . . . . . . . . . . 16
⊢
(((abs‘𝑡)
∈ ℝ ∧ (abs‘𝑡) = 𝑅) → (abs‘𝑡) ≤ 𝑅) |
184 | 182, 183,
113 | 3syl 18 |
. . . . . . . . . . . . . . 15
⊢ (((𝑅 ∈ ℝ ∧ 0 ≤
𝑅 ∧ 𝑡 ∈ ℝ) ∧ (abs‘𝑡) = 𝑅) → (vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) =
(vol‘(-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))))) |
185 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . 18
⊢
((abs‘𝑡) =
𝑅 → ((abs‘𝑡)↑2) = (𝑅↑2)) |
186 | 185 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑅 ∈ ℝ ∧ 0 ≤
𝑅 ∧ 𝑡 ∈ ℝ) ∧ (abs‘𝑡) = 𝑅) → ((abs‘𝑡)↑2) = (𝑅↑2)) |
187 | 13 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑅 ∈ ℝ ∧ 0 ≤
𝑅 ∧ 𝑡 ∈ ℝ) ∧ (abs‘𝑡) = 𝑅) → ((abs‘𝑡)↑2) = (𝑡↑2)) |
188 | 186, 187 | eqtr3d 2646 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑅 ∈ ℝ ∧ 0 ≤
𝑅 ∧ 𝑡 ∈ ℝ) ∧ (abs‘𝑡) = 𝑅) → (𝑅↑2) = (𝑡↑2)) |
189 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑅↑2) = (𝑡↑2) → ((𝑅↑2) − (𝑡↑2)) = ((𝑡↑2) − (𝑡↑2))) |
190 | 189 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑅↑2) = (𝑡↑2) → (√‘((𝑅↑2) − (𝑡↑2))) =
(√‘((𝑡↑2)
− (𝑡↑2)))) |
191 | 190 | negeqd 10154 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑅↑2) = (𝑡↑2) → -(√‘((𝑅↑2) − (𝑡↑2))) =
-(√‘((𝑡↑2)
− (𝑡↑2)))) |
192 | 191, 190 | oveq12d 6567 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑅↑2) = (𝑡↑2) → (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))) =
(-(√‘((𝑡↑2) − (𝑡↑2)))[,](√‘((𝑡↑2) − (𝑡↑2))))) |
193 | 8 | recnd 9947 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑡 ∈ ℝ → (𝑡↑2) ∈
ℂ) |
194 | 193 | subidd 10259 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑡 ∈ ℝ → ((𝑡↑2) − (𝑡↑2)) = 0) |
195 | 194 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑡 ∈ ℝ →
(√‘((𝑡↑2)
− (𝑡↑2))) =
(√‘0)) |
196 | 195 | negeqd 10154 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑡 ∈ ℝ →
-(√‘((𝑡↑2)
− (𝑡↑2))) =
-(√‘0)) |
197 | | sqrt0 13830 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(√‘0) = 0 |
198 | 197 | negeqi 10153 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
-(√‘0) = -0 |
199 | | neg0 10206 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ -0 =
0 |
200 | 198, 199 | eqtri 2632 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
-(√‘0) = 0 |
201 | 196, 200 | syl6eq 2660 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑡 ∈ ℝ →
-(√‘((𝑡↑2)
− (𝑡↑2))) =
0) |
202 | 195, 197 | syl6eq 2660 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑡 ∈ ℝ →
(√‘((𝑡↑2)
− (𝑡↑2))) =
0) |
203 | 201, 202 | oveq12d 6567 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑡 ∈ ℝ →
(-(√‘((𝑡↑2) − (𝑡↑2)))[,](√‘((𝑡↑2) − (𝑡↑2)))) =
(0[,]0)) |
204 | 203 | 3ad2ant3 1077 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑅 ∈ ℝ ∧ 0 ≤
𝑅 ∧ 𝑡 ∈ ℝ) →
(-(√‘((𝑡↑2) − (𝑡↑2)))[,](√‘((𝑡↑2) − (𝑡↑2)))) =
(0[,]0)) |
205 | 192, 204 | sylan9eqr 2666 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑅 ∈ ℝ ∧ 0 ≤
𝑅 ∧ 𝑡 ∈ ℝ) ∧ (𝑅↑2) = (𝑡↑2)) → (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))) =
(0[,]0)) |
206 | 205 | fveq2d 6107 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑅 ∈ ℝ ∧ 0 ≤
𝑅 ∧ 𝑡 ∈ ℝ) ∧ (𝑅↑2) = (𝑡↑2)) →
(vol‘(-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2))))) =
(vol‘(0[,]0))) |
207 | | iccmbl 23141 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((0
∈ ℝ ∧ 0 ∈ ℝ) → (0[,]0) ∈ dom
vol) |
208 | 62, 62, 207 | mp2an 704 |
. . . . . . . . . . . . . . . . . . 19
⊢ (0[,]0)
∈ dom vol |
209 | | mblvol 23105 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((0[,]0)
∈ dom vol → (vol‘(0[,]0)) =
(vol*‘(0[,]0))) |
210 | 208, 209 | ax-mp 5 |
. . . . . . . . . . . . . . . . . 18
⊢
(vol‘(0[,]0)) = (vol*‘(0[,]0)) |
211 | | 0xr 9965 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 0 ∈
ℝ* |
212 | | iccid 12091 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (0 ∈
ℝ* → (0[,]0) = {0}) |
213 | 212 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (0 ∈
ℝ* → (vol*‘(0[,]0)) =
(vol*‘{0})) |
214 | 211, 213 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
⊢
(vol*‘(0[,]0)) = (vol*‘{0}) |
215 | | ovolsn 23070 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (0 ∈
ℝ → (vol*‘{0}) = 0) |
216 | 62, 215 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
⊢
(vol*‘{0}) = 0 |
217 | 214, 216 | eqtri 2632 |
. . . . . . . . . . . . . . . . . 18
⊢
(vol*‘(0[,]0)) = 0 |
218 | 210, 217 | eqtri 2632 |
. . . . . . . . . . . . . . . . 17
⊢
(vol‘(0[,]0)) = 0 |
219 | 206, 218 | syl6eq 2660 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑅 ∈ ℝ ∧ 0 ≤
𝑅 ∧ 𝑡 ∈ ℝ) ∧ (𝑅↑2) = (𝑡↑2)) →
(vol‘(-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2))))) =
0) |
220 | 188, 219 | syldan 486 |
. . . . . . . . . . . . . . 15
⊢ (((𝑅 ∈ ℝ ∧ 0 ≤
𝑅 ∧ 𝑡 ∈ ℝ) ∧ (abs‘𝑡) = 𝑅) → (vol‘(-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2))))) =
0) |
221 | 184, 220 | eqtrd 2644 |
. . . . . . . . . . . . . 14
⊢ (((𝑅 ∈ ℝ ∧ 0 ≤
𝑅 ∧ 𝑡 ∈ ℝ) ∧ (abs‘𝑡) = 𝑅) → (vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) =
0) |
222 | 221 | ex 449 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ ℝ ∧ 0 ≤
𝑅 ∧ 𝑡 ∈ ℝ) → ((abs‘𝑡) = 𝑅 → (vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) =
0)) |
223 | 222 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈ ℝ ∧ 0 ≤
𝑅 ∧ 𝑡 ∈ ℝ) ∧ 𝑅 ≤ (abs‘𝑡)) → ((abs‘𝑡) = 𝑅 → (vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) =
0)) |
224 | 18, 17 | ltnled 10063 |
. . . . . . . . . . . . . . 15
⊢ ((𝑅 ∈ ℝ ∧ 0 ≤
𝑅 ∧ 𝑡 ∈ ℝ) → (𝑅 < (abs‘𝑡) ↔ ¬ (abs‘𝑡) ≤ 𝑅)) |
225 | 224 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ (((𝑅 ∈ ℝ ∧ 0 ≤
𝑅 ∧ 𝑡 ∈ ℝ) ∧ 𝑅 ≤ (abs‘𝑡)) → (𝑅 < (abs‘𝑡) ↔ ¬ (abs‘𝑡) ≤ 𝑅)) |
226 | | simpl1 1057 |
. . . . . . . . . . . . . . 15
⊢ (((𝑅 ∈ ℝ ∧ 0 ≤
𝑅 ∧ 𝑡 ∈ ℝ) ∧ 𝑅 ≤ (abs‘𝑡)) → 𝑅 ∈ ℝ) |
227 | 17 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ (((𝑅 ∈ ℝ ∧ 0 ≤
𝑅 ∧ 𝑡 ∈ ℝ) ∧ 𝑅 ≤ (abs‘𝑡)) → (abs‘𝑡) ∈ ℝ) |
228 | | simpr 476 |
. . . . . . . . . . . . . . 15
⊢ (((𝑅 ∈ ℝ ∧ 0 ≤
𝑅 ∧ 𝑡 ∈ ℝ) ∧ 𝑅 ≤ (abs‘𝑡)) → 𝑅 ≤ (abs‘𝑡)) |
229 | 226, 227,
228 | leltned 10069 |
. . . . . . . . . . . . . 14
⊢ (((𝑅 ∈ ℝ ∧ 0 ≤
𝑅 ∧ 𝑡 ∈ ℝ) ∧ 𝑅 ≤ (abs‘𝑡)) → (𝑅 < (abs‘𝑡) ↔ (abs‘𝑡) ≠ 𝑅)) |
230 | 225, 229 | bitr3d 269 |
. . . . . . . . . . . . 13
⊢ (((𝑅 ∈ ℝ ∧ 0 ≤
𝑅 ∧ 𝑡 ∈ ℝ) ∧ 𝑅 ≤ (abs‘𝑡)) → (¬ (abs‘𝑡) ≤ 𝑅 ↔ (abs‘𝑡) ≠ 𝑅)) |
231 | 230, 103 | syl6bir 243 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈ ℝ ∧ 0 ≤
𝑅 ∧ 𝑡 ∈ ℝ) ∧ 𝑅 ≤ (abs‘𝑡)) → ((abs‘𝑡) ≠ 𝑅 → (vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) =
0)) |
232 | 223, 231 | pm2.61dne 2868 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ ℝ ∧ 0 ≤
𝑅 ∧ 𝑡 ∈ ℝ) ∧ 𝑅 ≤ (abs‘𝑡)) → (vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) =
0) |
233 | 181, 232 | eqtrd 2644 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ ℝ ∧ 0 ≤
𝑅 ∧ 𝑡 ∈ ℝ) ∧ 𝑅 ≤ (abs‘𝑡)) → (vol‘(𝑆 “ {𝑡})) = 0) |
234 | 233 | ex 449 |
. . . . . . . . 9
⊢ ((𝑅 ∈ ℝ ∧ 0 ≤
𝑅 ∧ 𝑡 ∈ ℝ) → (𝑅 ≤ (abs‘𝑡) → (vol‘(𝑆 “ {𝑡})) = 0)) |
235 | 179, 234 | sylbid 229 |
. . . . . . . 8
⊢ ((𝑅 ∈ ℝ ∧ 0 ≤
𝑅 ∧ 𝑡 ∈ ℝ) → (¬ 𝑡 ∈ (-𝑅(,)𝑅) → (vol‘(𝑆 “ {𝑡})) = 0)) |
236 | 235 | 3expia 1259 |
. . . . . . 7
⊢ ((𝑅 ∈ ℝ ∧ 0 ≤
𝑅) → (𝑡 ∈ ℝ → (¬
𝑡 ∈ (-𝑅(,)𝑅) → (vol‘(𝑆 “ {𝑡})) = 0))) |
237 | 236 | impd 446 |
. . . . . 6
⊢ ((𝑅 ∈ ℝ ∧ 0 ≤
𝑅) → ((𝑡 ∈ ℝ ∧ ¬
𝑡 ∈ (-𝑅(,)𝑅)) → (vol‘(𝑆 “ {𝑡})) = 0)) |
238 | 165, 237 | syl5bi 231 |
. . . . 5
⊢ ((𝑅 ∈ ℝ ∧ 0 ≤
𝑅) → (𝑡 ∈ (ℝ ∖ (-𝑅(,)𝑅)) → (vol‘(𝑆 “ {𝑡})) = 0)) |
239 | 238 | imp 444 |
. . . 4
⊢ (((𝑅 ∈ ℝ ∧ 0 ≤
𝑅) ∧ 𝑡 ∈ (ℝ ∖ (-𝑅(,)𝑅))) → (vol‘(𝑆 “ {𝑡})) = 0) |
240 | 164, 239 | itgss 23384 |
. . 3
⊢ ((𝑅 ∈ ℝ ∧ 0 ≤
𝑅) → ∫(-𝑅(,)𝑅)(vol‘(𝑆 “ {𝑡})) d𝑡 = ∫ℝ(vol‘(𝑆 “ {𝑡})) d𝑡) |
241 | | negeq 10152 |
. . . . . . . . . 10
⊢ (𝑅 = 0 → -𝑅 = -0) |
242 | 241, 199 | syl6eq 2660 |
. . . . . . . . 9
⊢ (𝑅 = 0 → -𝑅 = 0) |
243 | | id 22 |
. . . . . . . . 9
⊢ (𝑅 = 0 → 𝑅 = 0) |
244 | 242, 243 | oveq12d 6567 |
. . . . . . . 8
⊢ (𝑅 = 0 → (-𝑅(,)𝑅) = (0(,)0)) |
245 | | iooid 12074 |
. . . . . . . 8
⊢ (0(,)0) =
∅ |
246 | 244, 245 | syl6eq 2660 |
. . . . . . 7
⊢ (𝑅 = 0 → (-𝑅(,)𝑅) = ∅) |
247 | 246 | adantl 481 |
. . . . . 6
⊢ (((𝑅 ∈ ℝ ∧ 0 ≤
𝑅) ∧ 𝑅 = 0) → (-𝑅(,)𝑅) = ∅) |
248 | | itgeq1 23345 |
. . . . . 6
⊢ ((-𝑅(,)𝑅) = ∅ → ∫(-𝑅(,)𝑅)(vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) d𝑡 =
∫∅(vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) d𝑡) |
249 | 247, 248 | syl 17 |
. . . . 5
⊢ (((𝑅 ∈ ℝ ∧ 0 ≤
𝑅) ∧ 𝑅 = 0) → ∫(-𝑅(,)𝑅)(vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) d𝑡 =
∫∅(vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) d𝑡) |
250 | | itg0 23352 |
. . . . . 6
⊢
∫∅(vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) d𝑡 = 0 |
251 | | oveq1 6556 |
. . . . . . . . 9
⊢ (𝑅 = 0 → (𝑅↑2) = (0↑2)) |
252 | 251 | oveq2d 6565 |
. . . . . . . 8
⊢ (𝑅 = 0 → (π ·
(𝑅↑2)) = (π
· (0↑2))) |
253 | | sq0 12817 |
. . . . . . . . . 10
⊢
(0↑2) = 0 |
254 | 253 | oveq2i 6560 |
. . . . . . . . 9
⊢ (π
· (0↑2)) = (π · 0) |
255 | | picn 24015 |
. . . . . . . . . 10
⊢ π
∈ ℂ |
256 | 255 | mul01i 10105 |
. . . . . . . . 9
⊢ (π
· 0) = 0 |
257 | 254, 256 | eqtr2i 2633 |
. . . . . . . 8
⊢ 0 = (π
· (0↑2)) |
258 | 252, 257 | syl6reqr 2663 |
. . . . . . 7
⊢ (𝑅 = 0 → 0 = (π ·
(𝑅↑2))) |
259 | 258 | adantl 481 |
. . . . . 6
⊢ (((𝑅 ∈ ℝ ∧ 0 ≤
𝑅) ∧ 𝑅 = 0) → 0 = (π · (𝑅↑2))) |
260 | 250, 259 | syl5eq 2656 |
. . . . 5
⊢ (((𝑅 ∈ ℝ ∧ 0 ≤
𝑅) ∧ 𝑅 = 0) →
∫∅(vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) d𝑡 = (π · (𝑅↑2))) |
261 | 249, 260 | eqtrd 2644 |
. . . 4
⊢ (((𝑅 ∈ ℝ ∧ 0 ≤
𝑅) ∧ 𝑅 = 0) → ∫(-𝑅(,)𝑅)(vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) d𝑡 = (π · (𝑅↑2))) |
262 | | simp1 1054 |
. . . . . . 7
⊢ ((𝑅 ∈ ℝ ∧ 0 ≤
𝑅 ∧ 𝑅 ≠ 0) → 𝑅 ∈ ℝ) |
263 | | 0red 9920 |
. . . . . . . . 9
⊢ ((𝑅 ∈ ℝ ∧ 0 ≤
𝑅) → 0 ∈
ℝ) |
264 | | simpr 476 |
. . . . . . . . 9
⊢ ((𝑅 ∈ ℝ ∧ 0 ≤
𝑅) → 0 ≤ 𝑅) |
265 | 263, 77, 264 | leltned 10069 |
. . . . . . . 8
⊢ ((𝑅 ∈ ℝ ∧ 0 ≤
𝑅) → (0 < 𝑅 ↔ 𝑅 ≠ 0)) |
266 | 265 | biimp3ar 1425 |
. . . . . . 7
⊢ ((𝑅 ∈ ℝ ∧ 0 ≤
𝑅 ∧ 𝑅 ≠ 0) → 0 < 𝑅) |
267 | 262, 266 | elrpd 11745 |
. . . . . 6
⊢ ((𝑅 ∈ ℝ ∧ 0 ≤
𝑅 ∧ 𝑅 ≠ 0) → 𝑅 ∈
ℝ+) |
268 | 267 | 3expa 1257 |
. . . . 5
⊢ (((𝑅 ∈ ℝ ∧ 0 ≤
𝑅) ∧ 𝑅 ≠ 0) → 𝑅 ∈
ℝ+) |
269 | 158, 16 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑡 ∈ (-𝑅(,)𝑅) → (abs‘𝑡) ∈ ℝ) |
270 | 269 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (abs‘𝑡) ∈ ℝ) |
271 | | rpre 11715 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ ℝ+
→ 𝑅 ∈
ℝ) |
272 | 271 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → 𝑅 ∈ ℝ) |
273 | 271 | renegcld 10336 |
. . . . . . . . . . . . . 14
⊢ (𝑅 ∈ ℝ+
→ -𝑅 ∈
ℝ) |
274 | 273 | rexrd 9968 |
. . . . . . . . . . . . 13
⊢ (𝑅 ∈ ℝ+
→ -𝑅 ∈
ℝ*) |
275 | | rpxr 11716 |
. . . . . . . . . . . . 13
⊢ (𝑅 ∈ ℝ+
→ 𝑅 ∈
ℝ*) |
276 | 274, 275,
168 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ ℝ+
→ (𝑡 ∈ (-𝑅(,)𝑅) ↔ (𝑡 ∈ ℝ ∧ -𝑅 < 𝑡 ∧ 𝑡 < 𝑅))) |
277 | | simpr 476 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ 𝑡 ∈
ℝ) |
278 | 271 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ 𝑅 ∈
ℝ) |
279 | 277, 278 | absltd 14016 |
. . . . . . . . . . . . . . 15
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ ((abs‘𝑡) <
𝑅 ↔ (-𝑅 < 𝑡 ∧ 𝑡 < 𝑅))) |
280 | 279 | biimprd 237 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ ((-𝑅 < 𝑡 ∧ 𝑡 < 𝑅) → (abs‘𝑡) < 𝑅)) |
281 | 280 | exp4b 630 |
. . . . . . . . . . . . 13
⊢ (𝑅 ∈ ℝ+
→ (𝑡 ∈ ℝ
→ (-𝑅 < 𝑡 → (𝑡 < 𝑅 → (abs‘𝑡) < 𝑅)))) |
282 | 281 | 3impd 1273 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ ℝ+
→ ((𝑡 ∈ ℝ
∧ -𝑅 < 𝑡 ∧ 𝑡 < 𝑅) → (abs‘𝑡) < 𝑅)) |
283 | 276, 282 | sylbid 229 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ ℝ+
→ (𝑡 ∈ (-𝑅(,)𝑅) → (abs‘𝑡) < 𝑅)) |
284 | 283 | imp 444 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (abs‘𝑡) < 𝑅) |
285 | 270, 272,
284 | ltled 10064 |
. . . . . . . . 9
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (abs‘𝑡) ≤ 𝑅) |
286 | 285, 113 | syl 17 |
. . . . . . . 8
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) =
(vol‘(-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))))) |
287 | 271 | resqcld 12897 |
. . . . . . . . . . . . . . 15
⊢ (𝑅 ∈ ℝ+
→ (𝑅↑2) ∈
ℝ) |
288 | 287 | recnd 9947 |
. . . . . . . . . . . . . 14
⊢ (𝑅 ∈ ℝ+
→ (𝑅↑2) ∈
ℂ) |
289 | 288 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ (𝑅↑2) ∈
ℂ) |
290 | 193 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ (𝑡↑2) ∈
ℂ) |
291 | 289, 290 | subcld 10271 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ ((𝑅↑2) −
(𝑡↑2)) ∈
ℂ) |
292 | 291 | sqrtcld 14024 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ (√‘((𝑅↑2) − (𝑡↑2))) ∈ ℂ) |
293 | 292, 292 | subnegd 10278 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ ((√‘((𝑅↑2) − (𝑡↑2))) − -(√‘((𝑅↑2) − (𝑡↑2)))) =
((√‘((𝑅↑2)
− (𝑡↑2))) +
(√‘((𝑅↑2)
− (𝑡↑2))))) |
294 | 158, 293 | sylan2 490 |
. . . . . . . . 9
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → ((√‘((𝑅↑2) − (𝑡↑2))) −
-(√‘((𝑅↑2)
− (𝑡↑2)))) =
((√‘((𝑅↑2)
− (𝑡↑2))) +
(√‘((𝑅↑2)
− (𝑡↑2))))) |
295 | 287 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ (𝑅↑2) ∈
ℝ) |
296 | 8 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ (𝑡↑2) ∈
ℝ) |
297 | 295, 296 | resubcld 10337 |
. . . . . . . . . . . . . . 15
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ ((𝑅↑2) −
(𝑡↑2)) ∈
ℝ) |
298 | 158, 297 | sylan2 490 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → ((𝑅↑2) − (𝑡↑2)) ∈ ℝ) |
299 | | 0red 9920 |
. . . . . . . . . . . . . . 15
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → 0 ∈ ℝ) |
300 | 16 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ (abs‘𝑡) ∈
ℝ) |
301 | 19 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ 0 ≤ (abs‘𝑡)) |
302 | | rpge0 11721 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑅 ∈ ℝ+
→ 0 ≤ 𝑅) |
303 | 302 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ 0 ≤ 𝑅) |
304 | 300, 278,
301, 303 | lt2sqd 12905 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ ((abs‘𝑡) <
𝑅 ↔ ((abs‘𝑡)↑2) < (𝑅↑2))) |
305 | 12 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ ((abs‘𝑡)↑2) = (𝑡↑2)) |
306 | 305 | breq1d 4593 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ (((abs‘𝑡)↑2) < (𝑅↑2) ↔ (𝑡↑2) < (𝑅↑2))) |
307 | 304, 279,
306 | 3bitr3rd 298 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ ((𝑡↑2) <
(𝑅↑2) ↔ (-𝑅 < 𝑡 ∧ 𝑡 < 𝑅))) |
308 | 296, 295 | posdifd 10493 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ ((𝑡↑2) <
(𝑅↑2) ↔ 0 <
((𝑅↑2) − (𝑡↑2)))) |
309 | 307, 308 | bitr3d 269 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ ((-𝑅 < 𝑡 ∧ 𝑡 < 𝑅) ↔ 0 < ((𝑅↑2) − (𝑡↑2)))) |
310 | 309 | biimpd 218 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ ((-𝑅 < 𝑡 ∧ 𝑡 < 𝑅) → 0 < ((𝑅↑2) − (𝑡↑2)))) |
311 | 310 | exp4b 630 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑅 ∈ ℝ+
→ (𝑡 ∈ ℝ
→ (-𝑅 < 𝑡 → (𝑡 < 𝑅 → 0 < ((𝑅↑2) − (𝑡↑2)))))) |
312 | 311 | 3impd 1273 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑅 ∈ ℝ+
→ ((𝑡 ∈ ℝ
∧ -𝑅 < 𝑡 ∧ 𝑡 < 𝑅) → 0 < ((𝑅↑2) − (𝑡↑2)))) |
313 | 276, 312 | sylbid 229 |
. . . . . . . . . . . . . . . 16
⊢ (𝑅 ∈ ℝ+
→ (𝑡 ∈ (-𝑅(,)𝑅) → 0 < ((𝑅↑2) − (𝑡↑2)))) |
314 | 313 | imp 444 |
. . . . . . . . . . . . . . 15
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → 0 < ((𝑅↑2) − (𝑡↑2))) |
315 | 299, 298,
314 | ltled 10064 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → 0 ≤ ((𝑅↑2) − (𝑡↑2))) |
316 | 298, 315 | resqrtcld 14004 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (√‘((𝑅↑2) − (𝑡↑2))) ∈ ℝ) |
317 | 316 | renegcld 10336 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → -(√‘((𝑅↑2) − (𝑡↑2))) ∈
ℝ) |
318 | 317, 316,
28 | syl2anc 691 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))) ∈ dom
vol) |
319 | 318, 30 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) →
(vol‘(-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2))))) =
(vol*‘(-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))))) |
320 | 298, 315 | sqrtge0d 14007 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → 0 ≤ (√‘((𝑅↑2) − (𝑡↑2)))) |
321 | 316, 316,
320, 320 | addge0d 10482 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → 0 ≤ ((√‘((𝑅↑2) − (𝑡↑2))) +
(√‘((𝑅↑2)
− (𝑡↑2))))) |
322 | 294 | breq2d 4595 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (0 ≤ ((√‘((𝑅↑2) − (𝑡↑2))) −
-(√‘((𝑅↑2)
− (𝑡↑2))))
↔ 0 ≤ ((√‘((𝑅↑2) − (𝑡↑2))) + (√‘((𝑅↑2) − (𝑡↑2)))))) |
323 | 316, 317 | subge0d 10496 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (0 ≤ ((√‘((𝑅↑2) − (𝑡↑2))) −
-(√‘((𝑅↑2)
− (𝑡↑2))))
↔ -(√‘((𝑅↑2) − (𝑡↑2))) ≤ (√‘((𝑅↑2) − (𝑡↑2))))) |
324 | 322, 323 | bitr3d 269 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (0 ≤ ((√‘((𝑅↑2) − (𝑡↑2))) +
(√‘((𝑅↑2)
− (𝑡↑2))))
↔ -(√‘((𝑅↑2) − (𝑡↑2))) ≤ (√‘((𝑅↑2) − (𝑡↑2))))) |
325 | 321, 324 | mpbid 221 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → -(√‘((𝑅↑2) − (𝑡↑2))) ≤
(√‘((𝑅↑2)
− (𝑡↑2)))) |
326 | 317, 316,
325, 47 | syl3anc 1318 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) →
(vol*‘(-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2))))) =
((√‘((𝑅↑2)
− (𝑡↑2)))
− -(√‘((𝑅↑2) − (𝑡↑2))))) |
327 | 319, 326 | eqtrd 2644 |
. . . . . . . . 9
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) →
(vol‘(-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2))))) =
((√‘((𝑅↑2)
− (𝑡↑2)))
− -(√‘((𝑅↑2) − (𝑡↑2))))) |
328 | | ax-resscn 9872 |
. . . . . . . . . . . . . . 15
⊢ ℝ
⊆ ℂ |
329 | 328 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝑅 ∈ ℝ+
→ ℝ ⊆ ℂ) |
330 | 273, 271,
78 | syl2anc 691 |
. . . . . . . . . . . . . 14
⊢ (𝑅 ∈ ℝ+
→ (-𝑅[,]𝑅) ⊆
ℝ) |
331 | | rpcn 11717 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑅 ∈ ℝ+
→ 𝑅 ∈
ℂ) |
332 | 331 | sqcld 12868 |
. . . . . . . . . . . . . . . 16
⊢ (𝑅 ∈ ℝ+
→ (𝑅↑2) ∈
ℂ) |
333 | 332 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝑅 ∈ ℝ+
∧ 𝑢 ∈ (-𝑅[,]𝑅)) → (𝑅↑2) ∈ ℂ) |
334 | 330 | sselda 3568 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑅 ∈ ℝ+
∧ 𝑢 ∈ (-𝑅[,]𝑅)) → 𝑢 ∈ ℝ) |
335 | 334 | recnd 9947 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑅 ∈ ℝ+
∧ 𝑢 ∈ (-𝑅[,]𝑅)) → 𝑢 ∈ ℂ) |
336 | 331 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑅 ∈ ℝ+
∧ 𝑢 ∈ (-𝑅[,]𝑅)) → 𝑅 ∈ ℂ) |
337 | | rpne0 11724 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑅 ∈ ℝ+
→ 𝑅 ≠
0) |
338 | 337 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑅 ∈ ℝ+
∧ 𝑢 ∈ (-𝑅[,]𝑅)) → 𝑅 ≠ 0) |
339 | 335, 336,
338 | divcld 10680 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑅 ∈ ℝ+
∧ 𝑢 ∈ (-𝑅[,]𝑅)) → (𝑢 / 𝑅) ∈ ℂ) |
340 | | asincl 24400 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑢 / 𝑅) ∈ ℂ → (arcsin‘(𝑢 / 𝑅)) ∈ ℂ) |
341 | 339, 340 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑅 ∈ ℝ+
∧ 𝑢 ∈ (-𝑅[,]𝑅)) → (arcsin‘(𝑢 / 𝑅)) ∈ ℂ) |
342 | | 1cnd 9935 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑅 ∈ ℝ+
∧ 𝑢 ∈ (-𝑅[,]𝑅)) → 1 ∈ ℂ) |
343 | 339 | sqcld 12868 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑅 ∈ ℝ+
∧ 𝑢 ∈ (-𝑅[,]𝑅)) → ((𝑢 / 𝑅)↑2) ∈ ℂ) |
344 | 342, 343 | subcld 10271 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑅 ∈ ℝ+
∧ 𝑢 ∈ (-𝑅[,]𝑅)) → (1 − ((𝑢 / 𝑅)↑2)) ∈ ℂ) |
345 | 344 | sqrtcld 14024 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑅 ∈ ℝ+
∧ 𝑢 ∈ (-𝑅[,]𝑅)) → (√‘(1 − ((𝑢 / 𝑅)↑2))) ∈ ℂ) |
346 | 339, 345 | mulcld 9939 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑅 ∈ ℝ+
∧ 𝑢 ∈ (-𝑅[,]𝑅)) → ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))) ∈
ℂ) |
347 | 341, 346 | addcld 9938 |
. . . . . . . . . . . . . . 15
⊢ ((𝑅 ∈ ℝ+
∧ 𝑢 ∈ (-𝑅[,]𝑅)) → ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2))))) ∈
ℂ) |
348 | 333, 347 | mulcld 9939 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ ℝ+
∧ 𝑢 ∈ (-𝑅[,]𝑅)) → ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))) ∈
ℂ) |
349 | | eqid 2610 |
. . . . . . . . . . . . . . 15
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
350 | 349 | tgioo2 22414 |
. . . . . . . . . . . . . 14
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t ℝ) |
351 | | iccntr 22432 |
. . . . . . . . . . . . . . 15
⊢ ((-𝑅 ∈ ℝ ∧ 𝑅 ∈ ℝ) →
((int‘(topGen‘ran (,)))‘(-𝑅[,]𝑅)) = (-𝑅(,)𝑅)) |
352 | 273, 271,
351 | syl2anc 691 |
. . . . . . . . . . . . . 14
⊢ (𝑅 ∈ ℝ+
→ ((int‘(topGen‘ran (,)))‘(-𝑅[,]𝑅)) = (-𝑅(,)𝑅)) |
353 | 329, 330,
348, 350, 349, 352 | dvmptntr 23540 |
. . . . . . . . . . . . 13
⊢ (𝑅 ∈ ℝ+
→ (ℝ D (𝑢 ∈
(-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))))) = (ℝ D (𝑢 ∈ (-𝑅(,)𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2))))))))) |
354 | | areacirclem1 32670 |
. . . . . . . . . . . . 13
⊢ (𝑅 ∈ ℝ+
→ (ℝ D (𝑢 ∈
(-𝑅(,)𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))))) = (𝑢 ∈ (-𝑅(,)𝑅) ↦ (2 · (√‘((𝑅↑2) − (𝑢↑2)))))) |
355 | 353, 354 | eqtrd 2644 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ ℝ+
→ (ℝ D (𝑢 ∈
(-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))))) = (𝑢 ∈ (-𝑅(,)𝑅) ↦ (2 · (√‘((𝑅↑2) − (𝑢↑2)))))) |
356 | 355 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (ℝ D (𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))))) = (𝑢 ∈ (-𝑅(,)𝑅) ↦ (2 · (√‘((𝑅↑2) − (𝑢↑2)))))) |
357 | | oveq1 6556 |
. . . . . . . . . . . . . . 15
⊢ (𝑢 = 𝑡 → (𝑢↑2) = (𝑡↑2)) |
358 | 357 | oveq2d 6565 |
. . . . . . . . . . . . . 14
⊢ (𝑢 = 𝑡 → ((𝑅↑2) − (𝑢↑2)) = ((𝑅↑2) − (𝑡↑2))) |
359 | 358 | fveq2d 6107 |
. . . . . . . . . . . . 13
⊢ (𝑢 = 𝑡 → (√‘((𝑅↑2) − (𝑢↑2))) = (√‘((𝑅↑2) − (𝑡↑2)))) |
360 | 359 | oveq2d 6565 |
. . . . . . . . . . . 12
⊢ (𝑢 = 𝑡 → (2 · (√‘((𝑅↑2) − (𝑢↑2)))) = (2 ·
(√‘((𝑅↑2)
− (𝑡↑2))))) |
361 | 360 | adantl 481 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) ∧ 𝑢 = 𝑡) → (2 · (√‘((𝑅↑2) − (𝑢↑2)))) = (2 ·
(√‘((𝑅↑2)
− (𝑡↑2))))) |
362 | | simpr 476 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → 𝑡 ∈ (-𝑅(,)𝑅)) |
363 | | ovex 6577 |
. . . . . . . . . . . 12
⊢ (2
· (√‘((𝑅↑2) − (𝑡↑2)))) ∈ V |
364 | 363 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (2 · (√‘((𝑅↑2) − (𝑡↑2)))) ∈
V) |
365 | 356, 361,
362, 364 | fvmptd 6197 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → ((ℝ D (𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2))))))))‘𝑡) = (2 · (√‘((𝑅↑2) − (𝑡↑2))))) |
366 | 158, 292 | sylan2 490 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (√‘((𝑅↑2) − (𝑡↑2))) ∈ ℂ) |
367 | 366 | 2timesd 11152 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (2 · (√‘((𝑅↑2) − (𝑡↑2)))) =
((√‘((𝑅↑2)
− (𝑡↑2))) +
(√‘((𝑅↑2)
− (𝑡↑2))))) |
368 | 365, 367 | eqtrd 2644 |
. . . . . . . . 9
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → ((ℝ D (𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2))))))))‘𝑡) = ((√‘((𝑅↑2) − (𝑡↑2))) + (√‘((𝑅↑2) − (𝑡↑2))))) |
369 | 294, 327,
368 | 3eqtr4rd 2655 |
. . . . . . . 8
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → ((ℝ D (𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2))))))))‘𝑡) = (vol‘(-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))))) |
370 | 286, 369 | eqtr4d 2647 |
. . . . . . 7
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) =
((ℝ D (𝑢 ∈
(-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2))))))))‘𝑡)) |
371 | 370 | itgeq2dv 23354 |
. . . . . 6
⊢ (𝑅 ∈ ℝ+
→ ∫(-𝑅(,)𝑅)(vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) d𝑡 = ∫(-𝑅(,)𝑅)((ℝ D (𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2))))))))‘𝑡) d𝑡) |
372 | 271, 271,
302, 302 | addge0d 10482 |
. . . . . . . 8
⊢ (𝑅 ∈ ℝ+
→ 0 ≤ (𝑅 + 𝑅)) |
373 | 331, 331 | subnegd 10278 |
. . . . . . . . . 10
⊢ (𝑅 ∈ ℝ+
→ (𝑅 − -𝑅) = (𝑅 + 𝑅)) |
374 | 373 | breq2d 4595 |
. . . . . . . . 9
⊢ (𝑅 ∈ ℝ+
→ (0 ≤ (𝑅 −
-𝑅) ↔ 0 ≤ (𝑅 + 𝑅))) |
375 | 271, 273 | subge0d 10496 |
. . . . . . . . 9
⊢ (𝑅 ∈ ℝ+
→ (0 ≤ (𝑅 −
-𝑅) ↔ -𝑅 ≤ 𝑅)) |
376 | 374, 375 | bitr3d 269 |
. . . . . . . 8
⊢ (𝑅 ∈ ℝ+
→ (0 ≤ (𝑅 + 𝑅) ↔ -𝑅 ≤ 𝑅)) |
377 | 372, 376 | mpbid 221 |
. . . . . . 7
⊢ (𝑅 ∈ ℝ+
→ -𝑅 ≤ 𝑅) |
378 | | 2cn 10968 |
. . . . . . . . . . 11
⊢ 2 ∈
ℂ |
379 | 163, 328 | sstri 3577 |
. . . . . . . . . . 11
⊢ (-𝑅(,)𝑅) ⊆ ℂ |
380 | | ssid 3587 |
. . . . . . . . . . 11
⊢ ℂ
⊆ ℂ |
381 | 378, 379,
380 | 3pm3.2i 1232 |
. . . . . . . . . 10
⊢ (2 ∈
ℂ ∧ (-𝑅(,)𝑅) ⊆ ℂ ∧ ℂ
⊆ ℂ) |
382 | | cncfmptc 22522 |
. . . . . . . . . 10
⊢ ((2
∈ ℂ ∧ (-𝑅(,)𝑅) ⊆ ℂ ∧ ℂ ⊆
ℂ) → (𝑢 ∈
(-𝑅(,)𝑅) ↦ 2) ∈ ((-𝑅(,)𝑅)–cn→ℂ)) |
383 | 381, 382 | mp1i 13 |
. . . . . . . . 9
⊢ (𝑅 ∈ ℝ+
→ (𝑢 ∈ (-𝑅(,)𝑅) ↦ 2) ∈ ((-𝑅(,)𝑅)–cn→ℂ)) |
384 | | ioossicc 12130 |
. . . . . . . . . . 11
⊢ (-𝑅(,)𝑅) ⊆ (-𝑅[,]𝑅) |
385 | | resmpt 5369 |
. . . . . . . . . . 11
⊢ ((-𝑅(,)𝑅) ⊆ (-𝑅[,]𝑅) → ((𝑢 ∈ (-𝑅[,]𝑅) ↦ (√‘((𝑅↑2) − (𝑢↑2)))) ↾ (-𝑅(,)𝑅)) = (𝑢 ∈ (-𝑅(,)𝑅) ↦ (√‘((𝑅↑2) − (𝑢↑2))))) |
386 | 384, 385 | ax-mp 5 |
. . . . . . . . . 10
⊢ ((𝑢 ∈ (-𝑅[,]𝑅) ↦ (√‘((𝑅↑2) − (𝑢↑2)))) ↾ (-𝑅(,)𝑅)) = (𝑢 ∈ (-𝑅(,)𝑅) ↦ (√‘((𝑅↑2) − (𝑢↑2)))) |
387 | | areacirclem2 32671 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ ℝ ∧ 0 ≤
𝑅) → (𝑢 ∈ (-𝑅[,]𝑅) ↦ (√‘((𝑅↑2) − (𝑢↑2)))) ∈ ((-𝑅[,]𝑅)–cn→ℂ)) |
388 | 271, 302,
387 | syl2anc 691 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ ℝ+
→ (𝑢 ∈ (-𝑅[,]𝑅) ↦ (√‘((𝑅↑2) − (𝑢↑2)))) ∈ ((-𝑅[,]𝑅)–cn→ℂ)) |
389 | | rescncf 22508 |
. . . . . . . . . . 11
⊢ ((-𝑅(,)𝑅) ⊆ (-𝑅[,]𝑅) → ((𝑢 ∈ (-𝑅[,]𝑅) ↦ (√‘((𝑅↑2) − (𝑢↑2)))) ∈ ((-𝑅[,]𝑅)–cn→ℂ) → ((𝑢 ∈ (-𝑅[,]𝑅) ↦ (√‘((𝑅↑2) − (𝑢↑2)))) ↾ (-𝑅(,)𝑅)) ∈ ((-𝑅(,)𝑅)–cn→ℂ))) |
390 | 384, 388,
389 | mpsyl 66 |
. . . . . . . . . 10
⊢ (𝑅 ∈ ℝ+
→ ((𝑢 ∈ (-𝑅[,]𝑅) ↦ (√‘((𝑅↑2) − (𝑢↑2)))) ↾ (-𝑅(,)𝑅)) ∈ ((-𝑅(,)𝑅)–cn→ℂ)) |
391 | 386, 390 | syl5eqelr 2693 |
. . . . . . . . 9
⊢ (𝑅 ∈ ℝ+
→ (𝑢 ∈ (-𝑅(,)𝑅) ↦ (√‘((𝑅↑2) − (𝑢↑2)))) ∈ ((-𝑅(,)𝑅)–cn→ℂ)) |
392 | 383, 391 | mulcncf 23023 |
. . . . . . . 8
⊢ (𝑅 ∈ ℝ+
→ (𝑢 ∈ (-𝑅(,)𝑅) ↦ (2 · (√‘((𝑅↑2) − (𝑢↑2))))) ∈ ((-𝑅(,)𝑅)–cn→ℂ)) |
393 | 355, 392 | eqeltrd 2688 |
. . . . . . 7
⊢ (𝑅 ∈ ℝ+
→ (ℝ D (𝑢 ∈
(-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))))) ∈ ((-𝑅(,)𝑅)–cn→ℂ)) |
394 | 384 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ ℝ ∧ 0 ≤
𝑅) → (-𝑅(,)𝑅) ⊆ (-𝑅[,]𝑅)) |
395 | | ioombl 23140 |
. . . . . . . . . . 11
⊢ (-𝑅(,)𝑅) ∈ dom vol |
396 | 395 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ ℝ ∧ 0 ≤
𝑅) → (-𝑅(,)𝑅) ∈ dom vol) |
397 | | ovex 6577 |
. . . . . . . . . . 11
⊢ (2
· (√‘((𝑅↑2) − (𝑢↑2)))) ∈ V |
398 | 397 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ ℝ ∧ 0 ≤
𝑅) ∧ 𝑢 ∈ (-𝑅[,]𝑅)) → (2 · (√‘((𝑅↑2) − (𝑢↑2)))) ∈
V) |
399 | | areacirclem3 32672 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ ℝ ∧ 0 ≤
𝑅) → (𝑢 ∈ (-𝑅[,]𝑅) ↦ (2 · (√‘((𝑅↑2) − (𝑢↑2))))) ∈
𝐿1) |
400 | 394, 396,
398, 399 | iblss 23377 |
. . . . . . . . 9
⊢ ((𝑅 ∈ ℝ ∧ 0 ≤
𝑅) → (𝑢 ∈ (-𝑅(,)𝑅) ↦ (2 · (√‘((𝑅↑2) − (𝑢↑2))))) ∈
𝐿1) |
401 | 271, 302,
400 | syl2anc 691 |
. . . . . . . 8
⊢ (𝑅 ∈ ℝ+
→ (𝑢 ∈ (-𝑅(,)𝑅) ↦ (2 · (√‘((𝑅↑2) − (𝑢↑2))))) ∈
𝐿1) |
402 | 355, 401 | eqeltrd 2688 |
. . . . . . 7
⊢ (𝑅 ∈ ℝ+
→ (ℝ D (𝑢 ∈
(-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))))) ∈
𝐿1) |
403 | | areacirclem4 32673 |
. . . . . . 7
⊢ (𝑅 ∈ ℝ+
→ (𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2))))))) ∈ ((-𝑅[,]𝑅)–cn→ℂ)) |
404 | 273, 271,
377, 393, 402, 403 | ftc2nc 32664 |
. . . . . 6
⊢ (𝑅 ∈ ℝ+
→ ∫(-𝑅(,)𝑅)((ℝ D (𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2))))))))‘𝑡) d𝑡 = (((𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))))‘𝑅) − ((𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))))‘-𝑅))) |
405 | | eqidd 2611 |
. . . . . . . . . 10
⊢ (𝑅 ∈ ℝ+
→ (𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2))))))) = (𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))))) |
406 | | oveq1 6556 |
. . . . . . . . . . . . . 14
⊢ (𝑢 = 𝑅 → (𝑢 / 𝑅) = (𝑅 / 𝑅)) |
407 | 406 | fveq2d 6107 |
. . . . . . . . . . . . 13
⊢ (𝑢 = 𝑅 → (arcsin‘(𝑢 / 𝑅)) = (arcsin‘(𝑅 / 𝑅))) |
408 | 406 | oveq1d 6564 |
. . . . . . . . . . . . . . . 16
⊢ (𝑢 = 𝑅 → ((𝑢 / 𝑅)↑2) = ((𝑅 / 𝑅)↑2)) |
409 | 408 | oveq2d 6565 |
. . . . . . . . . . . . . . 15
⊢ (𝑢 = 𝑅 → (1 − ((𝑢 / 𝑅)↑2)) = (1 − ((𝑅 / 𝑅)↑2))) |
410 | 409 | fveq2d 6107 |
. . . . . . . . . . . . . 14
⊢ (𝑢 = 𝑅 → (√‘(1 − ((𝑢 / 𝑅)↑2))) = (√‘(1 −
((𝑅 / 𝑅)↑2)))) |
411 | 406, 410 | oveq12d 6567 |
. . . . . . . . . . . . 13
⊢ (𝑢 = 𝑅 → ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))) = ((𝑅 / 𝑅) · (√‘(1 − ((𝑅 / 𝑅)↑2))))) |
412 | 407, 411 | oveq12d 6567 |
. . . . . . . . . . . 12
⊢ (𝑢 = 𝑅 → ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2))))) = ((arcsin‘(𝑅 / 𝑅)) + ((𝑅 / 𝑅) · (√‘(1 − ((𝑅 / 𝑅)↑2)))))) |
413 | 412 | oveq2d 6565 |
. . . . . . . . . . 11
⊢ (𝑢 = 𝑅 → ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))) = ((𝑅↑2) · ((arcsin‘(𝑅 / 𝑅)) + ((𝑅 / 𝑅) · (√‘(1 − ((𝑅 / 𝑅)↑2))))))) |
414 | 413 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ ℝ+
∧ 𝑢 = 𝑅) → ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))) = ((𝑅↑2) · ((arcsin‘(𝑅 / 𝑅)) + ((𝑅 / 𝑅) · (√‘(1 − ((𝑅 / 𝑅)↑2))))))) |
415 | | ubicc2 12160 |
. . . . . . . . . . 11
⊢ ((-𝑅 ∈ ℝ*
∧ 𝑅 ∈
ℝ* ∧ -𝑅 ≤ 𝑅) → 𝑅 ∈ (-𝑅[,]𝑅)) |
416 | 274, 275,
377, 415 | syl3anc 1318 |
. . . . . . . . . 10
⊢ (𝑅 ∈ ℝ+
→ 𝑅 ∈ (-𝑅[,]𝑅)) |
417 | | ovex 6577 |
. . . . . . . . . . 11
⊢ ((𝑅↑2) ·
((arcsin‘(𝑅 / 𝑅)) + ((𝑅 / 𝑅) · (√‘(1 − ((𝑅 / 𝑅)↑2)))))) ∈ V |
418 | 417 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑅 ∈ ℝ+
→ ((𝑅↑2) ·
((arcsin‘(𝑅 / 𝑅)) + ((𝑅 / 𝑅) · (√‘(1 − ((𝑅 / 𝑅)↑2)))))) ∈ V) |
419 | 405, 414,
416, 418 | fvmptd 6197 |
. . . . . . . . 9
⊢ (𝑅 ∈ ℝ+
→ ((𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))))‘𝑅) = ((𝑅↑2) · ((arcsin‘(𝑅 / 𝑅)) + ((𝑅 / 𝑅) · (√‘(1 − ((𝑅 / 𝑅)↑2))))))) |
420 | 331, 337 | dividd 10678 |
. . . . . . . . . . . . . 14
⊢ (𝑅 ∈ ℝ+
→ (𝑅 / 𝑅) = 1) |
421 | 420 | fveq2d 6107 |
. . . . . . . . . . . . 13
⊢ (𝑅 ∈ ℝ+
→ (arcsin‘(𝑅 /
𝑅)) =
(arcsin‘1)) |
422 | | asin1 24421 |
. . . . . . . . . . . . 13
⊢
(arcsin‘1) = (π / 2) |
423 | 421, 422 | syl6eq 2660 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ ℝ+
→ (arcsin‘(𝑅 /
𝑅)) = (π /
2)) |
424 | 420 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑅 ∈ ℝ+
→ ((𝑅 / 𝑅)↑2) =
(1↑2)) |
425 | | sq1 12820 |
. . . . . . . . . . . . . . . . . . 19
⊢
(1↑2) = 1 |
426 | 424, 425 | syl6eq 2660 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑅 ∈ ℝ+
→ ((𝑅 / 𝑅)↑2) = 1) |
427 | 426 | oveq2d 6565 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑅 ∈ ℝ+
→ (1 − ((𝑅 /
𝑅)↑2)) = (1 −
1)) |
428 | | 1cnd 9935 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑅 ∈ ℝ+
→ 1 ∈ ℂ) |
429 | 428 | subidd 10259 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑅 ∈ ℝ+
→ (1 − 1) = 0) |
430 | 427, 429 | eqtrd 2644 |
. . . . . . . . . . . . . . . 16
⊢ (𝑅 ∈ ℝ+
→ (1 − ((𝑅 /
𝑅)↑2)) =
0) |
431 | 430 | fveq2d 6107 |
. . . . . . . . . . . . . . 15
⊢ (𝑅 ∈ ℝ+
→ (√‘(1 − ((𝑅 / 𝑅)↑2))) =
(√‘0)) |
432 | 431, 197 | syl6eq 2660 |
. . . . . . . . . . . . . 14
⊢ (𝑅 ∈ ℝ+
→ (√‘(1 − ((𝑅 / 𝑅)↑2))) = 0) |
433 | 432 | oveq2d 6565 |
. . . . . . . . . . . . 13
⊢ (𝑅 ∈ ℝ+
→ ((𝑅 / 𝑅) · (√‘(1
− ((𝑅 / 𝑅)↑2)))) = ((𝑅 / 𝑅) · 0)) |
434 | 331, 331,
337 | divcld 10680 |
. . . . . . . . . . . . . 14
⊢ (𝑅 ∈ ℝ+
→ (𝑅 / 𝑅) ∈
ℂ) |
435 | 434 | mul01d 10114 |
. . . . . . . . . . . . 13
⊢ (𝑅 ∈ ℝ+
→ ((𝑅 / 𝑅) · 0) =
0) |
436 | 433, 435 | eqtrd 2644 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ ℝ+
→ ((𝑅 / 𝑅) · (√‘(1
− ((𝑅 / 𝑅)↑2)))) =
0) |
437 | 423, 436 | oveq12d 6567 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ ℝ+
→ ((arcsin‘(𝑅 /
𝑅)) + ((𝑅 / 𝑅) · (√‘(1 − ((𝑅 / 𝑅)↑2))))) = ((π / 2) +
0)) |
438 | | 2ne0 10990 |
. . . . . . . . . . . . . 14
⊢ 2 ≠
0 |
439 | 255, 378,
438 | divcli 10646 |
. . . . . . . . . . . . 13
⊢ (π /
2) ∈ ℂ |
440 | 439 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ ℝ+
→ (π / 2) ∈ ℂ) |
441 | 440 | addid1d 10115 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ ℝ+
→ ((π / 2) + 0) = (π / 2)) |
442 | 437, 441 | eqtrd 2644 |
. . . . . . . . . 10
⊢ (𝑅 ∈ ℝ+
→ ((arcsin‘(𝑅 /
𝑅)) + ((𝑅 / 𝑅) · (√‘(1 − ((𝑅 / 𝑅)↑2))))) = (π / 2)) |
443 | 442 | oveq2d 6565 |
. . . . . . . . 9
⊢ (𝑅 ∈ ℝ+
→ ((𝑅↑2) ·
((arcsin‘(𝑅 / 𝑅)) + ((𝑅 / 𝑅) · (√‘(1 − ((𝑅 / 𝑅)↑2)))))) = ((𝑅↑2) · (π /
2))) |
444 | 419, 443 | eqtrd 2644 |
. . . . . . . 8
⊢ (𝑅 ∈ ℝ+
→ ((𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))))‘𝑅) = ((𝑅↑2) · (π /
2))) |
445 | | oveq1 6556 |
. . . . . . . . . . . . . 14
⊢ (𝑢 = -𝑅 → (𝑢 / 𝑅) = (-𝑅 / 𝑅)) |
446 | 445 | fveq2d 6107 |
. . . . . . . . . . . . 13
⊢ (𝑢 = -𝑅 → (arcsin‘(𝑢 / 𝑅)) = (arcsin‘(-𝑅 / 𝑅))) |
447 | 445 | oveq1d 6564 |
. . . . . . . . . . . . . . . 16
⊢ (𝑢 = -𝑅 → ((𝑢 / 𝑅)↑2) = ((-𝑅 / 𝑅)↑2)) |
448 | 447 | oveq2d 6565 |
. . . . . . . . . . . . . . 15
⊢ (𝑢 = -𝑅 → (1 − ((𝑢 / 𝑅)↑2)) = (1 − ((-𝑅 / 𝑅)↑2))) |
449 | 448 | fveq2d 6107 |
. . . . . . . . . . . . . 14
⊢ (𝑢 = -𝑅 → (√‘(1 − ((𝑢 / 𝑅)↑2))) = (√‘(1 −
((-𝑅 / 𝑅)↑2)))) |
450 | 445, 449 | oveq12d 6567 |
. . . . . . . . . . . . 13
⊢ (𝑢 = -𝑅 → ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))) = ((-𝑅 / 𝑅) · (√‘(1 −
((-𝑅 / 𝑅)↑2))))) |
451 | 446, 450 | oveq12d 6567 |
. . . . . . . . . . . 12
⊢ (𝑢 = -𝑅 → ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2))))) = ((arcsin‘(-𝑅 / 𝑅)) + ((-𝑅 / 𝑅) · (√‘(1 −
((-𝑅 / 𝑅)↑2)))))) |
452 | 451 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ ℝ+
∧ 𝑢 = -𝑅) → ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2))))) = ((arcsin‘(-𝑅 / 𝑅)) + ((-𝑅 / 𝑅) · (√‘(1 −
((-𝑅 / 𝑅)↑2)))))) |
453 | 452 | oveq2d 6565 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ ℝ+
∧ 𝑢 = -𝑅) → ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))) = ((𝑅↑2) · ((arcsin‘(-𝑅 / 𝑅)) + ((-𝑅 / 𝑅) · (√‘(1 −
((-𝑅 / 𝑅)↑2))))))) |
454 | | lbicc2 12159 |
. . . . . . . . . . 11
⊢ ((-𝑅 ∈ ℝ*
∧ 𝑅 ∈
ℝ* ∧ -𝑅 ≤ 𝑅) → -𝑅 ∈ (-𝑅[,]𝑅)) |
455 | 274, 275,
377, 454 | syl3anc 1318 |
. . . . . . . . . 10
⊢ (𝑅 ∈ ℝ+
→ -𝑅 ∈ (-𝑅[,]𝑅)) |
456 | | ovex 6577 |
. . . . . . . . . . 11
⊢ ((𝑅↑2) ·
((arcsin‘(-𝑅 / 𝑅)) + ((-𝑅 / 𝑅) · (√‘(1 −
((-𝑅 / 𝑅)↑2)))))) ∈ V |
457 | 456 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑅 ∈ ℝ+
→ ((𝑅↑2) ·
((arcsin‘(-𝑅 / 𝑅)) + ((-𝑅 / 𝑅) · (√‘(1 −
((-𝑅 / 𝑅)↑2)))))) ∈ V) |
458 | 405, 453,
455, 457 | fvmptd 6197 |
. . . . . . . . 9
⊢ (𝑅 ∈ ℝ+
→ ((𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))))‘-𝑅) = ((𝑅↑2) · ((arcsin‘(-𝑅 / 𝑅)) + ((-𝑅 / 𝑅) · (√‘(1 −
((-𝑅 / 𝑅)↑2))))))) |
459 | 331, 331,
337 | divnegd 10693 |
. . . . . . . . . . . . . . 15
⊢ (𝑅 ∈ ℝ+
→ -(𝑅 / 𝑅) = (-𝑅 / 𝑅)) |
460 | 420 | negeqd 10154 |
. . . . . . . . . . . . . . 15
⊢ (𝑅 ∈ ℝ+
→ -(𝑅 / 𝑅) = -1) |
461 | 459, 460 | eqtr3d 2646 |
. . . . . . . . . . . . . 14
⊢ (𝑅 ∈ ℝ+
→ (-𝑅 / 𝑅) = -1) |
462 | 461 | fveq2d 6107 |
. . . . . . . . . . . . 13
⊢ (𝑅 ∈ ℝ+
→ (arcsin‘(-𝑅 /
𝑅)) =
(arcsin‘-1)) |
463 | | ax-1cn 9873 |
. . . . . . . . . . . . . . 15
⊢ 1 ∈
ℂ |
464 | | asinneg 24413 |
. . . . . . . . . . . . . . 15
⊢ (1 ∈
ℂ → (arcsin‘-1) = -(arcsin‘1)) |
465 | 463, 464 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢
(arcsin‘-1) = -(arcsin‘1) |
466 | 422 | negeqi 10153 |
. . . . . . . . . . . . . 14
⊢
-(arcsin‘1) = -(π / 2) |
467 | 465, 466 | eqtri 2632 |
. . . . . . . . . . . . 13
⊢
(arcsin‘-1) = -(π / 2) |
468 | 462, 467 | syl6eq 2660 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ ℝ+
→ (arcsin‘(-𝑅 /
𝑅)) = -(π /
2)) |
469 | 461 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑅 ∈ ℝ+
→ ((-𝑅 / 𝑅)↑2) =
(-1↑2)) |
470 | | neg1sqe1 12821 |
. . . . . . . . . . . . . . . . . . 19
⊢
(-1↑2) = 1 |
471 | 469, 470 | syl6eq 2660 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑅 ∈ ℝ+
→ ((-𝑅 / 𝑅)↑2) = 1) |
472 | 471 | oveq2d 6565 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑅 ∈ ℝ+
→ (1 − ((-𝑅 /
𝑅)↑2)) = (1 −
1)) |
473 | 472, 429 | eqtrd 2644 |
. . . . . . . . . . . . . . . 16
⊢ (𝑅 ∈ ℝ+
→ (1 − ((-𝑅 /
𝑅)↑2)) =
0) |
474 | 473 | fveq2d 6107 |
. . . . . . . . . . . . . . 15
⊢ (𝑅 ∈ ℝ+
→ (√‘(1 − ((-𝑅 / 𝑅)↑2))) =
(√‘0)) |
475 | 474, 197 | syl6eq 2660 |
. . . . . . . . . . . . . 14
⊢ (𝑅 ∈ ℝ+
→ (√‘(1 − ((-𝑅 / 𝑅)↑2))) = 0) |
476 | 475 | oveq2d 6565 |
. . . . . . . . . . . . 13
⊢ (𝑅 ∈ ℝ+
→ ((-𝑅 / 𝑅) · (√‘(1
− ((-𝑅 / 𝑅)↑2)))) = ((-𝑅 / 𝑅) · 0)) |
477 | 273 | recnd 9947 |
. . . . . . . . . . . . . . 15
⊢ (𝑅 ∈ ℝ+
→ -𝑅 ∈
ℂ) |
478 | 477, 331,
337 | divcld 10680 |
. . . . . . . . . . . . . 14
⊢ (𝑅 ∈ ℝ+
→ (-𝑅 / 𝑅) ∈
ℂ) |
479 | 478 | mul01d 10114 |
. . . . . . . . . . . . 13
⊢ (𝑅 ∈ ℝ+
→ ((-𝑅 / 𝑅) · 0) =
0) |
480 | 476, 479 | eqtrd 2644 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ ℝ+
→ ((-𝑅 / 𝑅) · (√‘(1
− ((-𝑅 / 𝑅)↑2)))) =
0) |
481 | 468, 480 | oveq12d 6567 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ ℝ+
→ ((arcsin‘(-𝑅 /
𝑅)) + ((-𝑅 / 𝑅) · (√‘(1 −
((-𝑅 / 𝑅)↑2))))) = (-(π / 2) +
0)) |
482 | 439 | negcli 10228 |
. . . . . . . . . . . . 13
⊢ -(π /
2) ∈ ℂ |
483 | 482 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ ℝ+
→ -(π / 2) ∈ ℂ) |
484 | 483 | addid1d 10115 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ ℝ+
→ (-(π / 2) + 0) = -(π / 2)) |
485 | 481, 484 | eqtrd 2644 |
. . . . . . . . . 10
⊢ (𝑅 ∈ ℝ+
→ ((arcsin‘(-𝑅 /
𝑅)) + ((-𝑅 / 𝑅) · (√‘(1 −
((-𝑅 / 𝑅)↑2))))) = -(π /
2)) |
486 | 485 | oveq2d 6565 |
. . . . . . . . 9
⊢ (𝑅 ∈ ℝ+
→ ((𝑅↑2) ·
((arcsin‘(-𝑅 / 𝑅)) + ((-𝑅 / 𝑅) · (√‘(1 −
((-𝑅 / 𝑅)↑2)))))) = ((𝑅↑2) · -(π /
2))) |
487 | 458, 486 | eqtrd 2644 |
. . . . . . . 8
⊢ (𝑅 ∈ ℝ+
→ ((𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))))‘-𝑅) = ((𝑅↑2) · -(π /
2))) |
488 | 444, 487 | oveq12d 6567 |
. . . . . . 7
⊢ (𝑅 ∈ ℝ+
→ (((𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))))‘𝑅) − ((𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))))‘-𝑅)) = (((𝑅↑2) · (π / 2)) −
((𝑅↑2) · -(π
/ 2)))) |
489 | 439, 439 | subnegi 10239 |
. . . . . . . . . . 11
⊢ ((π /
2) − -(π / 2)) = ((π / 2) + (π / 2)) |
490 | | pidiv2halves 24023 |
. . . . . . . . . . 11
⊢ ((π /
2) + (π / 2)) = π |
491 | 489, 490 | eqtri 2632 |
. . . . . . . . . 10
⊢ ((π /
2) − -(π / 2)) = π |
492 | 491 | a1i 11 |
. . . . . . . . 9
⊢ (𝑅 ∈ ℝ+
→ ((π / 2) − -(π / 2)) = π) |
493 | 492 | oveq2d 6565 |
. . . . . . . 8
⊢ (𝑅 ∈ ℝ+
→ ((𝑅↑2) ·
((π / 2) − -(π / 2))) = ((𝑅↑2) · π)) |
494 | 332, 440,
483 | subdid 10365 |
. . . . . . . 8
⊢ (𝑅 ∈ ℝ+
→ ((𝑅↑2) ·
((π / 2) − -(π / 2))) = (((𝑅↑2) · (π / 2)) −
((𝑅↑2) · -(π
/ 2)))) |
495 | 255 | a1i 11 |
. . . . . . . . 9
⊢ (𝑅 ∈ ℝ+
→ π ∈ ℂ) |
496 | 332, 495 | mulcomd 9940 |
. . . . . . . 8
⊢ (𝑅 ∈ ℝ+
→ ((𝑅↑2) ·
π) = (π · (𝑅↑2))) |
497 | 493, 494,
496 | 3eqtr3d 2652 |
. . . . . . 7
⊢ (𝑅 ∈ ℝ+
→ (((𝑅↑2)
· (π / 2)) − ((𝑅↑2) · -(π / 2))) = (π
· (𝑅↑2))) |
498 | 488, 497 | eqtrd 2644 |
. . . . . 6
⊢ (𝑅 ∈ ℝ+
→ (((𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))))‘𝑅) − ((𝑢 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑢 / 𝑅)) + ((𝑢 / 𝑅) · (√‘(1 − ((𝑢 / 𝑅)↑2)))))))‘-𝑅)) = (π · (𝑅↑2))) |
499 | 371, 404,
498 | 3eqtrd 2648 |
. . . . 5
⊢ (𝑅 ∈ ℝ+
→ ∫(-𝑅(,)𝑅)(vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) d𝑡 = (π · (𝑅↑2))) |
500 | 268, 499 | syl 17 |
. . . 4
⊢ (((𝑅 ∈ ℝ ∧ 0 ≤
𝑅) ∧ 𝑅 ≠ 0) → ∫(-𝑅(,)𝑅)(vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) d𝑡 = (π · (𝑅↑2))) |
501 | 261, 500 | pm2.61dane 2869 |
. . 3
⊢ ((𝑅 ∈ ℝ ∧ 0 ≤
𝑅) → ∫(-𝑅(,)𝑅)(vol‘if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) d𝑡 = (π · (𝑅↑2))) |
502 | 162, 240,
501 | 3eqtr3d 2652 |
. 2
⊢ ((𝑅 ∈ ℝ ∧ 0 ≤
𝑅) →
∫ℝ(vol‘(𝑆
“ {𝑡})) d𝑡 = (π · (𝑅↑2))) |
503 | 157, 502 | eqtrd 2644 |
1
⊢ ((𝑅 ∈ ℝ ∧ 0 ≤
𝑅) → (area‘𝑆) = (π · (𝑅↑2))) |