Step | Hyp | Ref
| Expression |
1 | | reelprrecn 10821 |
. . . 4
⊢ ℝ
∈ {ℝ, ℂ} |
2 | 1 | a1i 11 |
. . 3
⊢ (𝑅 ∈ ℝ+
→ ℝ ∈ {ℝ, ℂ}) |
3 | | elioore 12965 |
. . . . . . . 8
⊢ (𝑡 ∈ (-𝑅(,)𝑅) → 𝑡 ∈ ℝ) |
4 | 3 | recnd 10861 |
. . . . . . 7
⊢ (𝑡 ∈ (-𝑅(,)𝑅) → 𝑡 ∈ ℂ) |
5 | 4 | adantl 485 |
. . . . . 6
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → 𝑡 ∈ ℂ) |
6 | | rpcn 12596 |
. . . . . . 7
⊢ (𝑅 ∈ ℝ+
→ 𝑅 ∈
ℂ) |
7 | 6 | adantr 484 |
. . . . . 6
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → 𝑅 ∈ ℂ) |
8 | | rpne0 12602 |
. . . . . . 7
⊢ (𝑅 ∈ ℝ+
→ 𝑅 ≠
0) |
9 | 8 | adantr 484 |
. . . . . 6
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → 𝑅 ≠ 0) |
10 | 5, 7, 9 | divcld 11608 |
. . . . 5
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (𝑡 / 𝑅) ∈ ℂ) |
11 | | asincl 25756 |
. . . . 5
⊢ ((𝑡 / 𝑅) ∈ ℂ → (arcsin‘(𝑡 / 𝑅)) ∈ ℂ) |
12 | 10, 11 | syl 17 |
. . . 4
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (arcsin‘(𝑡 / 𝑅)) ∈ ℂ) |
13 | | 1cnd 10828 |
. . . . . . 7
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → 1 ∈ ℂ) |
14 | 10 | sqcld 13714 |
. . . . . . 7
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → ((𝑡 / 𝑅)↑2) ∈ ℂ) |
15 | 13, 14 | subcld 11189 |
. . . . . 6
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (1 − ((𝑡 / 𝑅)↑2)) ∈ ℂ) |
16 | 15 | sqrtcld 15001 |
. . . . 5
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (√‘(1 − ((𝑡 / 𝑅)↑2))) ∈ ℂ) |
17 | 10, 16 | mulcld 10853 |
. . . 4
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → ((𝑡 / 𝑅) · (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈
ℂ) |
18 | 12, 17 | addcld 10852 |
. . 3
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → ((arcsin‘(𝑡 / 𝑅)) + ((𝑡 / 𝑅) · (√‘(1 − ((𝑡 / 𝑅)↑2))))) ∈
ℂ) |
19 | | ovexd 7248 |
. . 3
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → ((2 · (√‘(1
− ((𝑡 / 𝑅)↑2)))) · (1 / 𝑅)) ∈ V) |
20 | | rpre 12594 |
. . . . . . . . . 10
⊢ (𝑅 ∈ ℝ+
→ 𝑅 ∈
ℝ) |
21 | 20 | renegcld 11259 |
. . . . . . . . 9
⊢ (𝑅 ∈ ℝ+
→ -𝑅 ∈
ℝ) |
22 | 21 | rexrd 10883 |
. . . . . . . 8
⊢ (𝑅 ∈ ℝ+
→ -𝑅 ∈
ℝ*) |
23 | | rpxr 12595 |
. . . . . . . 8
⊢ (𝑅 ∈ ℝ+
→ 𝑅 ∈
ℝ*) |
24 | | elioo2 12976 |
. . . . . . . 8
⊢ ((-𝑅 ∈ ℝ*
∧ 𝑅 ∈
ℝ*) → (𝑡 ∈ (-𝑅(,)𝑅) ↔ (𝑡 ∈ ℝ ∧ -𝑅 < 𝑡 ∧ 𝑡 < 𝑅))) |
25 | 22, 23, 24 | syl2anc 587 |
. . . . . . 7
⊢ (𝑅 ∈ ℝ+
→ (𝑡 ∈ (-𝑅(,)𝑅) ↔ (𝑡 ∈ ℝ ∧ -𝑅 < 𝑡 ∧ 𝑡 < 𝑅))) |
26 | | simpr 488 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ 𝑡 ∈
ℝ) |
27 | 20 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ 𝑅 ∈
ℝ) |
28 | 8 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ 𝑅 ≠
0) |
29 | 26, 27, 28 | redivcld 11660 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ (𝑡 / 𝑅) ∈
ℝ) |
30 | 29 | a1d 25 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ ((-𝑅 < 𝑡 ∧ 𝑡 < 𝑅) → (𝑡 / 𝑅) ∈ ℝ)) |
31 | 6 | mulm1d 11284 |
. . . . . . . . . . . . . . 15
⊢ (𝑅 ∈ ℝ+
→ (-1 · 𝑅) =
-𝑅) |
32 | 31 | adantr 484 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ (-1 · 𝑅) =
-𝑅) |
33 | 32 | breq1d 5063 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ ((-1 · 𝑅)
< 𝑡 ↔ -𝑅 < 𝑡)) |
34 | | neg1rr 11945 |
. . . . . . . . . . . . . . 15
⊢ -1 ∈
ℝ |
35 | 34 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ -1 ∈ ℝ) |
36 | | simpl 486 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ 𝑅 ∈
ℝ+) |
37 | 35, 26, 36 | ltmuldivd 12675 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ ((-1 · 𝑅)
< 𝑡 ↔ -1 <
(𝑡 / 𝑅))) |
38 | 33, 37 | bitr3d 284 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ (-𝑅 < 𝑡 ↔ -1 < (𝑡 / 𝑅))) |
39 | 38 | biimpd 232 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ (-𝑅 < 𝑡 → -1 < (𝑡 / 𝑅))) |
40 | 39 | adantrd 495 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ ((-𝑅 < 𝑡 ∧ 𝑡 < 𝑅) → -1 < (𝑡 / 𝑅))) |
41 | | 1red 10834 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ 1 ∈ ℝ) |
42 | 26, 41, 36 | ltdivmuld 12679 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ ((𝑡 / 𝑅) < 1 ↔ 𝑡 < (𝑅 · 1))) |
43 | 6 | mulid1d 10850 |
. . . . . . . . . . . . . . 15
⊢ (𝑅 ∈ ℝ+
→ (𝑅 · 1) =
𝑅) |
44 | 43 | adantr 484 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ (𝑅 · 1) =
𝑅) |
45 | 44 | breq2d 5065 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ (𝑡 < (𝑅 · 1) ↔ 𝑡 < 𝑅)) |
46 | 42, 45 | bitr2d 283 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ (𝑡 < 𝑅 ↔ (𝑡 / 𝑅) < 1)) |
47 | 46 | biimpd 232 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ (𝑡 < 𝑅 → (𝑡 / 𝑅) < 1)) |
48 | 47 | adantld 494 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ ((-𝑅 < 𝑡 ∧ 𝑡 < 𝑅) → (𝑡 / 𝑅) < 1)) |
49 | 30, 40, 48 | 3jcad 1131 |
. . . . . . . . 9
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ ((-𝑅 < 𝑡 ∧ 𝑡 < 𝑅) → ((𝑡 / 𝑅) ∈ ℝ ∧ -1 < (𝑡 / 𝑅) ∧ (𝑡 / 𝑅) < 1))) |
50 | 49 | exp4b 434 |
. . . . . . . 8
⊢ (𝑅 ∈ ℝ+
→ (𝑡 ∈ ℝ
→ (-𝑅 < 𝑡 → (𝑡 < 𝑅 → ((𝑡 / 𝑅) ∈ ℝ ∧ -1 < (𝑡 / 𝑅) ∧ (𝑡 / 𝑅) < 1))))) |
51 | 50 | 3impd 1350 |
. . . . . . 7
⊢ (𝑅 ∈ ℝ+
→ ((𝑡 ∈ ℝ
∧ -𝑅 < 𝑡 ∧ 𝑡 < 𝑅) → ((𝑡 / 𝑅) ∈ ℝ ∧ -1 < (𝑡 / 𝑅) ∧ (𝑡 / 𝑅) < 1))) |
52 | 25, 51 | sylbid 243 |
. . . . . 6
⊢ (𝑅 ∈ ℝ+
→ (𝑡 ∈ (-𝑅(,)𝑅) → ((𝑡 / 𝑅) ∈ ℝ ∧ -1 < (𝑡 / 𝑅) ∧ (𝑡 / 𝑅) < 1))) |
53 | 52 | imp 410 |
. . . . 5
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → ((𝑡 / 𝑅) ∈ ℝ ∧ -1 < (𝑡 / 𝑅) ∧ (𝑡 / 𝑅) < 1)) |
54 | 34 | rexri 10891 |
. . . . . 6
⊢ -1 ∈
ℝ* |
55 | | 1xr 10892 |
. . . . . 6
⊢ 1 ∈
ℝ* |
56 | | elioo2 12976 |
. . . . . 6
⊢ ((-1
∈ ℝ* ∧ 1 ∈ ℝ*) → ((𝑡 / 𝑅) ∈ (-1(,)1) ↔ ((𝑡 / 𝑅) ∈ ℝ ∧ -1 < (𝑡 / 𝑅) ∧ (𝑡 / 𝑅) < 1))) |
57 | 54, 55, 56 | mp2an 692 |
. . . . 5
⊢ ((𝑡 / 𝑅) ∈ (-1(,)1) ↔ ((𝑡 / 𝑅) ∈ ℝ ∧ -1 < (𝑡 / 𝑅) ∧ (𝑡 / 𝑅) < 1)) |
58 | 53, 57 | sylibr 237 |
. . . 4
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (𝑡 / 𝑅) ∈ (-1(,)1)) |
59 | | ovexd 7248 |
. . . 4
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (1 / 𝑅) ∈ V) |
60 | | elioore 12965 |
. . . . . . 7
⊢ (𝑢 ∈ (-1(,)1) → 𝑢 ∈
ℝ) |
61 | 60 | recnd 10861 |
. . . . . 6
⊢ (𝑢 ∈ (-1(,)1) → 𝑢 ∈
ℂ) |
62 | | asincl 25756 |
. . . . . . 7
⊢ (𝑢 ∈ ℂ →
(arcsin‘𝑢) ∈
ℂ) |
63 | | id 22 |
. . . . . . . 8
⊢ (𝑢 ∈ ℂ → 𝑢 ∈
ℂ) |
64 | | 1cnd 10828 |
. . . . . . . . . 10
⊢ (𝑢 ∈ ℂ → 1 ∈
ℂ) |
65 | | sqcl 13690 |
. . . . . . . . . 10
⊢ (𝑢 ∈ ℂ → (𝑢↑2) ∈
ℂ) |
66 | 64, 65 | subcld 11189 |
. . . . . . . . 9
⊢ (𝑢 ∈ ℂ → (1
− (𝑢↑2)) ∈
ℂ) |
67 | 66 | sqrtcld 15001 |
. . . . . . . 8
⊢ (𝑢 ∈ ℂ →
(√‘(1 − (𝑢↑2))) ∈ ℂ) |
68 | 63, 67 | mulcld 10853 |
. . . . . . 7
⊢ (𝑢 ∈ ℂ → (𝑢 · (√‘(1
− (𝑢↑2))))
∈ ℂ) |
69 | 62, 68 | addcld 10852 |
. . . . . 6
⊢ (𝑢 ∈ ℂ →
((arcsin‘𝑢) + (𝑢 · (√‘(1
− (𝑢↑2)))))
∈ ℂ) |
70 | 61, 69 | syl 17 |
. . . . 5
⊢ (𝑢 ∈ (-1(,)1) →
((arcsin‘𝑢) + (𝑢 · (√‘(1
− (𝑢↑2)))))
∈ ℂ) |
71 | 70 | adantl 485 |
. . . 4
⊢ ((𝑅 ∈ ℝ+
∧ 𝑢 ∈ (-1(,)1))
→ ((arcsin‘𝑢) +
(𝑢 ·
(√‘(1 − (𝑢↑2))))) ∈ ℂ) |
72 | | ovexd 7248 |
. . . 4
⊢ ((𝑅 ∈ ℝ+
∧ 𝑢 ∈ (-1(,)1))
→ (2 · (√‘(1 − (𝑢↑2)))) ∈ V) |
73 | | recn 10819 |
. . . . . . 7
⊢ (𝑡 ∈ ℝ → 𝑡 ∈
ℂ) |
74 | 73 | adantl 485 |
. . . . . 6
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ 𝑡 ∈
ℂ) |
75 | | 1cnd 10828 |
. . . . . 6
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ 1 ∈ ℂ) |
76 | 2 | dvmptid 24854 |
. . . . . 6
⊢ (𝑅 ∈ ℝ+
→ (ℝ D (𝑡 ∈
ℝ ↦ 𝑡)) =
(𝑡 ∈ ℝ ↦
1)) |
77 | | ioossre 12996 |
. . . . . . 7
⊢ (-𝑅(,)𝑅) ⊆ ℝ |
78 | 77 | a1i 11 |
. . . . . 6
⊢ (𝑅 ∈ ℝ+
→ (-𝑅(,)𝑅) ⊆
ℝ) |
79 | | eqid 2737 |
. . . . . . 7
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
80 | 79 | tgioo2 23700 |
. . . . . 6
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t ℝ) |
81 | | iooretop 23663 |
. . . . . . 7
⊢ (-𝑅(,)𝑅) ∈ (topGen‘ran
(,)) |
82 | 81 | a1i 11 |
. . . . . 6
⊢ (𝑅 ∈ ℝ+
→ (-𝑅(,)𝑅) ∈ (topGen‘ran
(,))) |
83 | 2, 74, 75, 76, 78, 80, 79, 82 | dvmptres 24860 |
. . . . 5
⊢ (𝑅 ∈ ℝ+
→ (ℝ D (𝑡 ∈
(-𝑅(,)𝑅) ↦ 𝑡)) = (𝑡 ∈ (-𝑅(,)𝑅) ↦ 1)) |
84 | 2, 5, 13, 83, 6, 8 | dvmptdivc 24862 |
. . . 4
⊢ (𝑅 ∈ ℝ+
→ (ℝ D (𝑡 ∈
(-𝑅(,)𝑅) ↦ (𝑡 / 𝑅))) = (𝑡 ∈ (-𝑅(,)𝑅) ↦ (1 / 𝑅))) |
85 | 61, 62 | syl 17 |
. . . . . . 7
⊢ (𝑢 ∈ (-1(,)1) →
(arcsin‘𝑢) ∈
ℂ) |
86 | 85 | adantl 485 |
. . . . . 6
⊢ ((𝑅 ∈ ℝ+
∧ 𝑢 ∈ (-1(,)1))
→ (arcsin‘𝑢)
∈ ℂ) |
87 | | ovexd 7248 |
. . . . . 6
⊢ ((𝑅 ∈ ℝ+
∧ 𝑢 ∈ (-1(,)1))
→ (1 / (√‘(1 − (𝑢↑2)))) ∈ V) |
88 | | asinf 25755 |
. . . . . . . . . 10
⊢
arcsin:ℂ⟶ℂ |
89 | 88 | a1i 11 |
. . . . . . . . 9
⊢ (𝑅 ∈ ℝ+
→ arcsin:ℂ⟶ℂ) |
90 | | ioossre 12996 |
. . . . . . . . . . 11
⊢ (-1(,)1)
⊆ ℝ |
91 | | ax-resscn 10786 |
. . . . . . . . . . 11
⊢ ℝ
⊆ ℂ |
92 | 90, 91 | sstri 3910 |
. . . . . . . . . 10
⊢ (-1(,)1)
⊆ ℂ |
93 | 92 | a1i 11 |
. . . . . . . . 9
⊢ (𝑅 ∈ ℝ+
→ (-1(,)1) ⊆ ℂ) |
94 | 89, 93 | feqresmpt 6781 |
. . . . . . . 8
⊢ (𝑅 ∈ ℝ+
→ (arcsin ↾ (-1(,)1)) = (𝑢 ∈ (-1(,)1) ↦ (arcsin‘𝑢))) |
95 | 94 | oveq2d 7229 |
. . . . . . 7
⊢ (𝑅 ∈ ℝ+
→ (ℝ D (arcsin ↾ (-1(,)1))) = (ℝ D (𝑢 ∈ (-1(,)1) ↦ (arcsin‘𝑢)))) |
96 | | dvreasin 35600 |
. . . . . . 7
⊢ (ℝ
D (arcsin ↾ (-1(,)1))) = (𝑢 ∈ (-1(,)1) ↦ (1 /
(√‘(1 − (𝑢↑2))))) |
97 | 95, 96 | eqtr3di 2793 |
. . . . . 6
⊢ (𝑅 ∈ ℝ+
→ (ℝ D (𝑢 ∈
(-1(,)1) ↦ (arcsin‘𝑢))) = (𝑢 ∈ (-1(,)1) ↦ (1 /
(√‘(1 − (𝑢↑2)))))) |
98 | 61, 68 | syl 17 |
. . . . . . 7
⊢ (𝑢 ∈ (-1(,)1) → (𝑢 · (√‘(1
− (𝑢↑2))))
∈ ℂ) |
99 | 98 | adantl 485 |
. . . . . 6
⊢ ((𝑅 ∈ ℝ+
∧ 𝑢 ∈ (-1(,)1))
→ (𝑢 ·
(√‘(1 − (𝑢↑2)))) ∈ ℂ) |
100 | | ovexd 7248 |
. . . . . 6
⊢ ((𝑅 ∈ ℝ+
∧ 𝑢 ∈ (-1(,)1))
→ ((1 · (√‘(1 − (𝑢↑2)))) + ((-𝑢 / (√‘(1 − (𝑢↑2)))) · 𝑢)) ∈ V) |
101 | 61 | adantl 485 |
. . . . . . 7
⊢ ((𝑅 ∈ ℝ+
∧ 𝑢 ∈ (-1(,)1))
→ 𝑢 ∈
ℂ) |
102 | | 1cnd 10828 |
. . . . . . 7
⊢ ((𝑅 ∈ ℝ+
∧ 𝑢 ∈ (-1(,)1))
→ 1 ∈ ℂ) |
103 | | recn 10819 |
. . . . . . . . 9
⊢ (𝑢 ∈ ℝ → 𝑢 ∈
ℂ) |
104 | 103 | adantl 485 |
. . . . . . . 8
⊢ ((𝑅 ∈ ℝ+
∧ 𝑢 ∈ ℝ)
→ 𝑢 ∈
ℂ) |
105 | | 1cnd 10828 |
. . . . . . . 8
⊢ ((𝑅 ∈ ℝ+
∧ 𝑢 ∈ ℝ)
→ 1 ∈ ℂ) |
106 | 2 | dvmptid 24854 |
. . . . . . . 8
⊢ (𝑅 ∈ ℝ+
→ (ℝ D (𝑢 ∈
ℝ ↦ 𝑢)) =
(𝑢 ∈ ℝ ↦
1)) |
107 | 90 | a1i 11 |
. . . . . . . 8
⊢ (𝑅 ∈ ℝ+
→ (-1(,)1) ⊆ ℝ) |
108 | | iooretop 23663 |
. . . . . . . . 9
⊢ (-1(,)1)
∈ (topGen‘ran (,)) |
109 | 108 | a1i 11 |
. . . . . . . 8
⊢ (𝑅 ∈ ℝ+
→ (-1(,)1) ∈ (topGen‘ran (,))) |
110 | 2, 104, 105, 106, 107, 80, 79, 109 | dvmptres 24860 |
. . . . . . 7
⊢ (𝑅 ∈ ℝ+
→ (ℝ D (𝑢 ∈
(-1(,)1) ↦ 𝑢)) =
(𝑢 ∈ (-1(,)1) ↦
1)) |
111 | 61, 67 | syl 17 |
. . . . . . . 8
⊢ (𝑢 ∈ (-1(,)1) →
(√‘(1 − (𝑢↑2))) ∈ ℂ) |
112 | 111 | adantl 485 |
. . . . . . 7
⊢ ((𝑅 ∈ ℝ+
∧ 𝑢 ∈ (-1(,)1))
→ (√‘(1 − (𝑢↑2))) ∈ ℂ) |
113 | | ovexd 7248 |
. . . . . . 7
⊢ ((𝑅 ∈ ℝ+
∧ 𝑢 ∈ (-1(,)1))
→ (-𝑢 /
(√‘(1 − (𝑢↑2)))) ∈ V) |
114 | | 1red 10834 |
. . . . . . . . . . . 12
⊢ (𝑢 ∈ (-1(,)1) → 1 ∈
ℝ) |
115 | 60 | resqcld 13817 |
. . . . . . . . . . . 12
⊢ (𝑢 ∈ (-1(,)1) → (𝑢↑2) ∈
ℝ) |
116 | 114, 115 | resubcld 11260 |
. . . . . . . . . . 11
⊢ (𝑢 ∈ (-1(,)1) → (1
− (𝑢↑2)) ∈
ℝ) |
117 | | elioo2 12976 |
. . . . . . . . . . . . 13
⊢ ((-1
∈ ℝ* ∧ 1 ∈ ℝ*) → (𝑢 ∈ (-1(,)1) ↔ (𝑢 ∈ ℝ ∧ -1 <
𝑢 ∧ 𝑢 < 1))) |
118 | 54, 55, 117 | mp2an 692 |
. . . . . . . . . . . 12
⊢ (𝑢 ∈ (-1(,)1) ↔ (𝑢 ∈ ℝ ∧ -1 <
𝑢 ∧ 𝑢 < 1)) |
119 | | id 22 |
. . . . . . . . . . . . . . . 16
⊢ (𝑢 ∈ ℝ → 𝑢 ∈
ℝ) |
120 | | 1red 10834 |
. . . . . . . . . . . . . . . 16
⊢ (𝑢 ∈ ℝ → 1 ∈
ℝ) |
121 | 119, 120 | absltd 14993 |
. . . . . . . . . . . . . . 15
⊢ (𝑢 ∈ ℝ →
((abs‘𝑢) < 1
↔ (-1 < 𝑢 ∧
𝑢 <
1))) |
122 | 103 | abscld 15000 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑢 ∈ ℝ →
(abs‘𝑢) ∈
ℝ) |
123 | 103 | absge0d 15008 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑢 ∈ ℝ → 0 ≤
(abs‘𝑢)) |
124 | | 0le1 11355 |
. . . . . . . . . . . . . . . . . 18
⊢ 0 ≤
1 |
125 | 124 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑢 ∈ ℝ → 0 ≤
1) |
126 | 122, 120,
123, 125 | lt2sqd 13825 |
. . . . . . . . . . . . . . . 16
⊢ (𝑢 ∈ ℝ →
((abs‘𝑢) < 1
↔ ((abs‘𝑢)↑2) < (1↑2))) |
127 | | absresq 14866 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑢 ∈ ℝ →
((abs‘𝑢)↑2) =
(𝑢↑2)) |
128 | | sq1 13764 |
. . . . . . . . . . . . . . . . . 18
⊢
(1↑2) = 1 |
129 | 128 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑢 ∈ ℝ →
(1↑2) = 1) |
130 | 127, 129 | breq12d 5066 |
. . . . . . . . . . . . . . . 16
⊢ (𝑢 ∈ ℝ →
(((abs‘𝑢)↑2)
< (1↑2) ↔ (𝑢↑2) < 1)) |
131 | | resqcl 13696 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑢 ∈ ℝ → (𝑢↑2) ∈
ℝ) |
132 | 131, 120 | posdifd 11419 |
. . . . . . . . . . . . . . . 16
⊢ (𝑢 ∈ ℝ → ((𝑢↑2) < 1 ↔ 0 < (1
− (𝑢↑2)))) |
133 | 126, 130,
132 | 3bitrd 308 |
. . . . . . . . . . . . . . 15
⊢ (𝑢 ∈ ℝ →
((abs‘𝑢) < 1
↔ 0 < (1 − (𝑢↑2)))) |
134 | 121, 133 | bitr3d 284 |
. . . . . . . . . . . . . 14
⊢ (𝑢 ∈ ℝ → ((-1 <
𝑢 ∧ 𝑢 < 1) ↔ 0 < (1 − (𝑢↑2)))) |
135 | 134 | biimpd 232 |
. . . . . . . . . . . . 13
⊢ (𝑢 ∈ ℝ → ((-1 <
𝑢 ∧ 𝑢 < 1) → 0 < (1 − (𝑢↑2)))) |
136 | 135 | 3impib 1118 |
. . . . . . . . . . . 12
⊢ ((𝑢 ∈ ℝ ∧ -1 <
𝑢 ∧ 𝑢 < 1) → 0 < (1 − (𝑢↑2))) |
137 | 118, 136 | sylbi 220 |
. . . . . . . . . . 11
⊢ (𝑢 ∈ (-1(,)1) → 0 <
(1 − (𝑢↑2))) |
138 | 116, 137 | elrpd 12625 |
. . . . . . . . . 10
⊢ (𝑢 ∈ (-1(,)1) → (1
− (𝑢↑2)) ∈
ℝ+) |
139 | 138 | adantl 485 |
. . . . . . . . 9
⊢ ((𝑅 ∈ ℝ+
∧ 𝑢 ∈ (-1(,)1))
→ (1 − (𝑢↑2)) ∈
ℝ+) |
140 | | negex 11076 |
. . . . . . . . . 10
⊢ -(2
· 𝑢) ∈
V |
141 | 140 | a1i 11 |
. . . . . . . . 9
⊢ ((𝑅 ∈ ℝ+
∧ 𝑢 ∈ (-1(,)1))
→ -(2 · 𝑢)
∈ V) |
142 | | rpcn 12596 |
. . . . . . . . . . 11
⊢ (𝑣 ∈ ℝ+
→ 𝑣 ∈
ℂ) |
143 | 142 | sqrtcld 15001 |
. . . . . . . . . 10
⊢ (𝑣 ∈ ℝ+
→ (√‘𝑣)
∈ ℂ) |
144 | 143 | adantl 485 |
. . . . . . . . 9
⊢ ((𝑅 ∈ ℝ+
∧ 𝑣 ∈
ℝ+) → (√‘𝑣) ∈ ℂ) |
145 | | ovexd 7248 |
. . . . . . . . 9
⊢ ((𝑅 ∈ ℝ+
∧ 𝑣 ∈
ℝ+) → (1 / (2 · (√‘𝑣))) ∈ V) |
146 | | 1cnd 10828 |
. . . . . . . . . . . 12
⊢ (𝑢 ∈ ℝ → 1 ∈
ℂ) |
147 | 103 | sqcld 13714 |
. . . . . . . . . . . 12
⊢ (𝑢 ∈ ℝ → (𝑢↑2) ∈
ℂ) |
148 | 146, 147 | subcld 11189 |
. . . . . . . . . . 11
⊢ (𝑢 ∈ ℝ → (1
− (𝑢↑2)) ∈
ℂ) |
149 | 148 | adantl 485 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ ℝ+
∧ 𝑢 ∈ ℝ)
→ (1 − (𝑢↑2)) ∈ ℂ) |
150 | 140 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ ℝ+
∧ 𝑢 ∈ ℝ)
→ -(2 · 𝑢)
∈ V) |
151 | | 0red 10836 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ ℝ+
∧ 𝑢 ∈ ℝ)
→ 0 ∈ ℝ) |
152 | | 1cnd 10828 |
. . . . . . . . . . . . 13
⊢ (𝑅 ∈ ℝ+
→ 1 ∈ ℂ) |
153 | 2, 152 | dvmptc 24855 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ ℝ+
→ (ℝ D (𝑢 ∈
ℝ ↦ 1)) = (𝑢
∈ ℝ ↦ 0)) |
154 | 147 | adantl 485 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ ℝ+
∧ 𝑢 ∈ ℝ)
→ (𝑢↑2) ∈
ℂ) |
155 | | ovexd 7248 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ ℝ+
∧ 𝑢 ∈ ℝ)
→ (2 · 𝑢)
∈ V) |
156 | 79 | cnfldtopon 23680 |
. . . . . . . . . . . . . 14
⊢
(TopOpen‘ℂfld) ∈
(TopOn‘ℂ) |
157 | | toponmax 21823 |
. . . . . . . . . . . . . 14
⊢
((TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
→ ℂ ∈ (TopOpen‘ℂfld)) |
158 | 156, 157 | mp1i 13 |
. . . . . . . . . . . . 13
⊢ (𝑅 ∈ ℝ+
→ ℂ ∈ (TopOpen‘ℂfld)) |
159 | | df-ss 3883 |
. . . . . . . . . . . . . . 15
⊢ (ℝ
⊆ ℂ ↔ (ℝ ∩ ℂ) = ℝ) |
160 | 91, 159 | mpbi 233 |
. . . . . . . . . . . . . 14
⊢ (ℝ
∩ ℂ) = ℝ |
161 | 160 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝑅 ∈ ℝ+
→ (ℝ ∩ ℂ) = ℝ) |
162 | 65 | adantl 485 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ ℝ+
∧ 𝑢 ∈ ℂ)
→ (𝑢↑2) ∈
ℂ) |
163 | | ovexd 7248 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ ℝ+
∧ 𝑢 ∈ ℂ)
→ (2 · 𝑢)
∈ V) |
164 | | 2nn 11903 |
. . . . . . . . . . . . . . . 16
⊢ 2 ∈
ℕ |
165 | | dvexp 24850 |
. . . . . . . . . . . . . . . 16
⊢ (2 ∈
ℕ → (ℂ D (𝑢 ∈ ℂ ↦ (𝑢↑2))) = (𝑢 ∈ ℂ ↦ (2 · (𝑢↑(2 −
1))))) |
166 | 164, 165 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢ (ℂ
D (𝑢 ∈ ℂ ↦
(𝑢↑2))) = (𝑢 ∈ ℂ ↦ (2
· (𝑢↑(2 −
1)))) |
167 | | 2m1e1 11956 |
. . . . . . . . . . . . . . . . . . 19
⊢ (2
− 1) = 1 |
168 | 167 | oveq2i 7224 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑢↑(2 − 1)) = (𝑢↑1) |
169 | | exp1 13641 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑢 ∈ ℂ → (𝑢↑1) = 𝑢) |
170 | 168, 169 | syl5eq 2790 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑢 ∈ ℂ → (𝑢↑(2 − 1)) = 𝑢) |
171 | 170 | oveq2d 7229 |
. . . . . . . . . . . . . . . 16
⊢ (𝑢 ∈ ℂ → (2
· (𝑢↑(2 −
1))) = (2 · 𝑢)) |
172 | 171 | mpteq2ia 5146 |
. . . . . . . . . . . . . . 15
⊢ (𝑢 ∈ ℂ ↦ (2
· (𝑢↑(2 −
1)))) = (𝑢 ∈ ℂ
↦ (2 · 𝑢)) |
173 | 166, 172 | eqtri 2765 |
. . . . . . . . . . . . . 14
⊢ (ℂ
D (𝑢 ∈ ℂ ↦
(𝑢↑2))) = (𝑢 ∈ ℂ ↦ (2
· 𝑢)) |
174 | 173 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝑅 ∈ ℝ+
→ (ℂ D (𝑢 ∈
ℂ ↦ (𝑢↑2))) = (𝑢 ∈ ℂ ↦ (2 · 𝑢))) |
175 | 79, 2, 158, 161, 162, 163, 174 | dvmptres3 24853 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ ℝ+
→ (ℝ D (𝑢 ∈
ℝ ↦ (𝑢↑2))) = (𝑢 ∈ ℝ ↦ (2 · 𝑢))) |
176 | 2, 105, 151, 153, 154, 155, 175 | dvmptsub 24864 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ ℝ+
→ (ℝ D (𝑢 ∈
ℝ ↦ (1 − (𝑢↑2)))) = (𝑢 ∈ ℝ ↦ (0 − (2
· 𝑢)))) |
177 | | df-neg 11065 |
. . . . . . . . . . . 12
⊢ -(2
· 𝑢) = (0 − (2
· 𝑢)) |
178 | 177 | mpteq2i 5147 |
. . . . . . . . . . 11
⊢ (𝑢 ∈ ℝ ↦ -(2
· 𝑢)) = (𝑢 ∈ ℝ ↦ (0
− (2 · 𝑢))) |
179 | 176, 178 | eqtr4di 2796 |
. . . . . . . . . 10
⊢ (𝑅 ∈ ℝ+
→ (ℝ D (𝑢 ∈
ℝ ↦ (1 − (𝑢↑2)))) = (𝑢 ∈ ℝ ↦ -(2 · 𝑢))) |
180 | 2, 149, 150, 179, 107, 80, 79, 109 | dvmptres 24860 |
. . . . . . . . 9
⊢ (𝑅 ∈ ℝ+
→ (ℝ D (𝑢 ∈
(-1(,)1) ↦ (1 − (𝑢↑2)))) = (𝑢 ∈ (-1(,)1) ↦ -(2 · 𝑢))) |
181 | | dvsqrt 25628 |
. . . . . . . . . 10
⊢ (ℝ
D (𝑣 ∈
ℝ+ ↦ (√‘𝑣))) = (𝑣 ∈ ℝ+ ↦ (1 / (2
· (√‘𝑣)))) |
182 | 181 | a1i 11 |
. . . . . . . . 9
⊢ (𝑅 ∈ ℝ+
→ (ℝ D (𝑣 ∈
ℝ+ ↦ (√‘𝑣))) = (𝑣 ∈ ℝ+ ↦ (1 / (2
· (√‘𝑣))))) |
183 | | fveq2 6717 |
. . . . . . . . 9
⊢ (𝑣 = (1 − (𝑢↑2)) →
(√‘𝑣) =
(√‘(1 − (𝑢↑2)))) |
184 | 183 | oveq2d 7229 |
. . . . . . . . . 10
⊢ (𝑣 = (1 − (𝑢↑2)) → (2 ·
(√‘𝑣)) = (2
· (√‘(1 − (𝑢↑2))))) |
185 | 184 | oveq2d 7229 |
. . . . . . . . 9
⊢ (𝑣 = (1 − (𝑢↑2)) → (1 / (2
· (√‘𝑣))) = (1 / (2 · (√‘(1
− (𝑢↑2)))))) |
186 | 2, 2, 139, 141, 144, 145, 180, 182, 183, 185 | dvmptco 24869 |
. . . . . . . 8
⊢ (𝑅 ∈ ℝ+
→ (ℝ D (𝑢 ∈
(-1(,)1) ↦ (√‘(1 − (𝑢↑2))))) = (𝑢 ∈ (-1(,)1) ↦ ((1 / (2 ·
(√‘(1 − (𝑢↑2))))) · -(2 · 𝑢)))) |
187 | | 2cnd 11908 |
. . . . . . . . . . . 12
⊢ (𝑢 ∈ (-1(,)1) → 2 ∈
ℂ) |
188 | 187, 61 | mulneg2d 11286 |
. . . . . . . . . . 11
⊢ (𝑢 ∈ (-1(,)1) → (2
· -𝑢) = -(2 ·
𝑢)) |
189 | 188 | oveq1d 7228 |
. . . . . . . . . 10
⊢ (𝑢 ∈ (-1(,)1) → ((2
· -𝑢) / (2 ·
(√‘(1 − (𝑢↑2))))) = (-(2 · 𝑢) / (2 ·
(√‘(1 − (𝑢↑2)))))) |
190 | 61 | negcld 11176 |
. . . . . . . . . . 11
⊢ (𝑢 ∈ (-1(,)1) → -𝑢 ∈
ℂ) |
191 | 137 | gt0ne0d 11396 |
. . . . . . . . . . . 12
⊢ (𝑢 ∈ (-1(,)1) → (1
− (𝑢↑2)) ≠
0) |
192 | 61, 66 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝑢 ∈ (-1(,)1) → (1
− (𝑢↑2)) ∈
ℂ) |
193 | 192 | adantr 484 |
. . . . . . . . . . . . . . 15
⊢ ((𝑢 ∈ (-1(,)1) ∧
(√‘(1 − (𝑢↑2))) = 0) → (1 − (𝑢↑2)) ∈
ℂ) |
194 | | simpr 488 |
. . . . . . . . . . . . . . 15
⊢ ((𝑢 ∈ (-1(,)1) ∧
(√‘(1 − (𝑢↑2))) = 0) → (√‘(1
− (𝑢↑2))) =
0) |
195 | 193, 194 | sqr00d 15005 |
. . . . . . . . . . . . . 14
⊢ ((𝑢 ∈ (-1(,)1) ∧
(√‘(1 − (𝑢↑2))) = 0) → (1 − (𝑢↑2)) = 0) |
196 | 195 | ex 416 |
. . . . . . . . . . . . 13
⊢ (𝑢 ∈ (-1(,)1) →
((√‘(1 − (𝑢↑2))) = 0 → (1 − (𝑢↑2)) = 0)) |
197 | 196 | necon3d 2961 |
. . . . . . . . . . . 12
⊢ (𝑢 ∈ (-1(,)1) → ((1
− (𝑢↑2)) ≠ 0
→ (√‘(1 − (𝑢↑2))) ≠ 0)) |
198 | 191, 197 | mpd 15 |
. . . . . . . . . . 11
⊢ (𝑢 ∈ (-1(,)1) →
(√‘(1 − (𝑢↑2))) ≠ 0) |
199 | | 2ne0 11934 |
. . . . . . . . . . . 12
⊢ 2 ≠
0 |
200 | 199 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑢 ∈ (-1(,)1) → 2 ≠
0) |
201 | 190, 111,
187, 198, 200 | divcan5d 11634 |
. . . . . . . . . 10
⊢ (𝑢 ∈ (-1(,)1) → ((2
· -𝑢) / (2 ·
(√‘(1 − (𝑢↑2))))) = (-𝑢 / (√‘(1 − (𝑢↑2))))) |
202 | 187, 61 | mulcld 10853 |
. . . . . . . . . . . 12
⊢ (𝑢 ∈ (-1(,)1) → (2
· 𝑢) ∈
ℂ) |
203 | 202 | negcld 11176 |
. . . . . . . . . . 11
⊢ (𝑢 ∈ (-1(,)1) → -(2
· 𝑢) ∈
ℂ) |
204 | 187, 111 | mulcld 10853 |
. . . . . . . . . . 11
⊢ (𝑢 ∈ (-1(,)1) → (2
· (√‘(1 − (𝑢↑2)))) ∈ ℂ) |
205 | 187, 111,
200, 198 | mulne0d 11484 |
. . . . . . . . . . 11
⊢ (𝑢 ∈ (-1(,)1) → (2
· (√‘(1 − (𝑢↑2)))) ≠ 0) |
206 | 203, 204,
205 | divrec2d 11612 |
. . . . . . . . . 10
⊢ (𝑢 ∈ (-1(,)1) → (-(2
· 𝑢) / (2 ·
(√‘(1 − (𝑢↑2))))) = ((1 / (2 ·
(√‘(1 − (𝑢↑2))))) · -(2 · 𝑢))) |
207 | 189, 201,
206 | 3eqtr3rd 2786 |
. . . . . . . . 9
⊢ (𝑢 ∈ (-1(,)1) → ((1 / (2
· (√‘(1 − (𝑢↑2))))) · -(2 · 𝑢)) = (-𝑢 / (√‘(1 − (𝑢↑2))))) |
208 | 207 | mpteq2ia 5146 |
. . . . . . . 8
⊢ (𝑢 ∈ (-1(,)1) ↦ ((1 /
(2 · (√‘(1 − (𝑢↑2))))) · -(2 · 𝑢))) = (𝑢 ∈ (-1(,)1) ↦ (-𝑢 / (√‘(1 − (𝑢↑2))))) |
209 | 186, 208 | eqtrdi 2794 |
. . . . . . 7
⊢ (𝑅 ∈ ℝ+
→ (ℝ D (𝑢 ∈
(-1(,)1) ↦ (√‘(1 − (𝑢↑2))))) = (𝑢 ∈ (-1(,)1) ↦ (-𝑢 / (√‘(1 − (𝑢↑2)))))) |
210 | 2, 101, 102, 110, 112, 113, 209 | dvmptmul 24858 |
. . . . . 6
⊢ (𝑅 ∈ ℝ+
→ (ℝ D (𝑢 ∈
(-1(,)1) ↦ (𝑢
· (√‘(1 − (𝑢↑2)))))) = (𝑢 ∈ (-1(,)1) ↦ ((1 ·
(√‘(1 − (𝑢↑2)))) + ((-𝑢 / (√‘(1 − (𝑢↑2)))) · 𝑢)))) |
211 | 2, 86, 87, 97, 99, 100, 210 | dvmptadd 24857 |
. . . . 5
⊢ (𝑅 ∈ ℝ+
→ (ℝ D (𝑢 ∈
(-1(,)1) ↦ ((arcsin‘𝑢) + (𝑢 · (√‘(1 − (𝑢↑2))))))) = (𝑢 ∈ (-1(,)1) ↦ ((1 /
(√‘(1 − (𝑢↑2)))) + ((1 · (√‘(1
− (𝑢↑2)))) +
((-𝑢 / (√‘(1
− (𝑢↑2))))
· 𝑢))))) |
212 | 111 | mulid2d 10851 |
. . . . . . . . . 10
⊢ (𝑢 ∈ (-1(,)1) → (1
· (√‘(1 − (𝑢↑2)))) = (√‘(1 −
(𝑢↑2)))) |
213 | 190, 111,
198 | divcld 11608 |
. . . . . . . . . . . 12
⊢ (𝑢 ∈ (-1(,)1) → (-𝑢 / (√‘(1 −
(𝑢↑2)))) ∈
ℂ) |
214 | 213, 61 | mulcomd 10854 |
. . . . . . . . . . 11
⊢ (𝑢 ∈ (-1(,)1) → ((-𝑢 / (√‘(1 −
(𝑢↑2)))) ·
𝑢) = (𝑢 · (-𝑢 / (√‘(1 − (𝑢↑2)))))) |
215 | 61, 190, 111, 198 | divassd 11643 |
. . . . . . . . . . 11
⊢ (𝑢 ∈ (-1(,)1) → ((𝑢 · -𝑢) / (√‘(1 − (𝑢↑2)))) = (𝑢 · (-𝑢 / (√‘(1 − (𝑢↑2)))))) |
216 | 61, 61 | mulneg2d 11286 |
. . . . . . . . . . . . 13
⊢ (𝑢 ∈ (-1(,)1) → (𝑢 · -𝑢) = -(𝑢 · 𝑢)) |
217 | 61 | sqvald 13713 |
. . . . . . . . . . . . . 14
⊢ (𝑢 ∈ (-1(,)1) → (𝑢↑2) = (𝑢 · 𝑢)) |
218 | 217 | negeqd 11072 |
. . . . . . . . . . . . 13
⊢ (𝑢 ∈ (-1(,)1) → -(𝑢↑2) = -(𝑢 · 𝑢)) |
219 | 216, 218 | eqtr4d 2780 |
. . . . . . . . . . . 12
⊢ (𝑢 ∈ (-1(,)1) → (𝑢 · -𝑢) = -(𝑢↑2)) |
220 | 219 | oveq1d 7228 |
. . . . . . . . . . 11
⊢ (𝑢 ∈ (-1(,)1) → ((𝑢 · -𝑢) / (√‘(1 − (𝑢↑2)))) = (-(𝑢↑2) / (√‘(1
− (𝑢↑2))))) |
221 | 214, 215,
220 | 3eqtr2d 2783 |
. . . . . . . . . 10
⊢ (𝑢 ∈ (-1(,)1) → ((-𝑢 / (√‘(1 −
(𝑢↑2)))) ·
𝑢) = (-(𝑢↑2) / (√‘(1 − (𝑢↑2))))) |
222 | 212, 221 | oveq12d 7231 |
. . . . . . . . 9
⊢ (𝑢 ∈ (-1(,)1) → ((1
· (√‘(1 − (𝑢↑2)))) + ((-𝑢 / (√‘(1 − (𝑢↑2)))) · 𝑢)) = ((√‘(1 −
(𝑢↑2))) + (-(𝑢↑2) / (√‘(1
− (𝑢↑2)))))) |
223 | 61 | sqcld 13714 |
. . . . . . . . . . . 12
⊢ (𝑢 ∈ (-1(,)1) → (𝑢↑2) ∈
ℂ) |
224 | 223 | negcld 11176 |
. . . . . . . . . . 11
⊢ (𝑢 ∈ (-1(,)1) → -(𝑢↑2) ∈
ℂ) |
225 | 224, 111,
198 | divcld 11608 |
. . . . . . . . . 10
⊢ (𝑢 ∈ (-1(,)1) → (-(𝑢↑2) / (√‘(1
− (𝑢↑2))))
∈ ℂ) |
226 | 111, 225 | addcomd 11034 |
. . . . . . . . 9
⊢ (𝑢 ∈ (-1(,)1) →
((√‘(1 − (𝑢↑2))) + (-(𝑢↑2) / (√‘(1 − (𝑢↑2))))) = ((-(𝑢↑2) / (√‘(1
− (𝑢↑2)))) +
(√‘(1 − (𝑢↑2))))) |
227 | 222, 226 | eqtrd 2777 |
. . . . . . . 8
⊢ (𝑢 ∈ (-1(,)1) → ((1
· (√‘(1 − (𝑢↑2)))) + ((-𝑢 / (√‘(1 − (𝑢↑2)))) · 𝑢)) = ((-(𝑢↑2) / (√‘(1 − (𝑢↑2)))) + (√‘(1
− (𝑢↑2))))) |
228 | 227 | oveq2d 7229 |
. . . . . . 7
⊢ (𝑢 ∈ (-1(,)1) → ((1 /
(√‘(1 − (𝑢↑2)))) + ((1 · (√‘(1
− (𝑢↑2)))) +
((-𝑢 / (√‘(1
− (𝑢↑2))))
· 𝑢))) = ((1 /
(√‘(1 − (𝑢↑2)))) + ((-(𝑢↑2) / (√‘(1 − (𝑢↑2)))) + (√‘(1
− (𝑢↑2)))))) |
229 | 111 | 2timesd 12073 |
. . . . . . . 8
⊢ (𝑢 ∈ (-1(,)1) → (2
· (√‘(1 − (𝑢↑2)))) = ((√‘(1 −
(𝑢↑2))) +
(√‘(1 − (𝑢↑2))))) |
230 | 64, 65 | negsubd 11195 |
. . . . . . . . . . . . 13
⊢ (𝑢 ∈ ℂ → (1 +
-(𝑢↑2)) = (1 −
(𝑢↑2))) |
231 | 66 | sqsqrtd 15003 |
. . . . . . . . . . . . 13
⊢ (𝑢 ∈ ℂ →
((√‘(1 − (𝑢↑2)))↑2) = (1 − (𝑢↑2))) |
232 | 67 | sqvald 13713 |
. . . . . . . . . . . . 13
⊢ (𝑢 ∈ ℂ →
((√‘(1 − (𝑢↑2)))↑2) = ((√‘(1
− (𝑢↑2)))
· (√‘(1 − (𝑢↑2))))) |
233 | 230, 231,
232 | 3eqtr2d 2783 |
. . . . . . . . . . . 12
⊢ (𝑢 ∈ ℂ → (1 +
-(𝑢↑2)) =
((√‘(1 − (𝑢↑2))) · (√‘(1 −
(𝑢↑2))))) |
234 | 61, 233 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑢 ∈ (-1(,)1) → (1 +
-(𝑢↑2)) =
((√‘(1 − (𝑢↑2))) · (√‘(1 −
(𝑢↑2))))) |
235 | 234 | oveq1d 7228 |
. . . . . . . . . 10
⊢ (𝑢 ∈ (-1(,)1) → ((1 +
-(𝑢↑2)) /
(√‘(1 − (𝑢↑2)))) = (((√‘(1 −
(𝑢↑2))) ·
(√‘(1 − (𝑢↑2)))) / (√‘(1 −
(𝑢↑2))))) |
236 | | 1cnd 10828 |
. . . . . . . . . . 11
⊢ (𝑢 ∈ (-1(,)1) → 1 ∈
ℂ) |
237 | 236, 224,
111, 198 | divdird 11646 |
. . . . . . . . . 10
⊢ (𝑢 ∈ (-1(,)1) → ((1 +
-(𝑢↑2)) /
(√‘(1 − (𝑢↑2)))) = ((1 / (√‘(1 −
(𝑢↑2)))) + (-(𝑢↑2) / (√‘(1
− (𝑢↑2)))))) |
238 | 111, 111,
198 | divcan3d 11613 |
. . . . . . . . . 10
⊢ (𝑢 ∈ (-1(,)1) →
(((√‘(1 − (𝑢↑2))) · (√‘(1 −
(𝑢↑2)))) /
(√‘(1 − (𝑢↑2)))) = (√‘(1 −
(𝑢↑2)))) |
239 | 235, 237,
238 | 3eqtr3rd 2786 |
. . . . . . . . 9
⊢ (𝑢 ∈ (-1(,)1) →
(√‘(1 − (𝑢↑2))) = ((1 / (√‘(1 −
(𝑢↑2)))) + (-(𝑢↑2) / (√‘(1
− (𝑢↑2)))))) |
240 | 239 | oveq1d 7228 |
. . . . . . . 8
⊢ (𝑢 ∈ (-1(,)1) →
((√‘(1 − (𝑢↑2))) + (√‘(1 − (𝑢↑2)))) = (((1 /
(√‘(1 − (𝑢↑2)))) + (-(𝑢↑2) / (√‘(1 − (𝑢↑2))))) + (√‘(1
− (𝑢↑2))))) |
241 | 111, 198 | reccld 11601 |
. . . . . . . . 9
⊢ (𝑢 ∈ (-1(,)1) → (1 /
(√‘(1 − (𝑢↑2)))) ∈ ℂ) |
242 | 241, 225,
111 | addassd 10855 |
. . . . . . . 8
⊢ (𝑢 ∈ (-1(,)1) → (((1 /
(√‘(1 − (𝑢↑2)))) + (-(𝑢↑2) / (√‘(1 − (𝑢↑2))))) + (√‘(1
− (𝑢↑2)))) = ((1
/ (√‘(1 − (𝑢↑2)))) + ((-(𝑢↑2) / (√‘(1 − (𝑢↑2)))) + (√‘(1
− (𝑢↑2)))))) |
243 | 229, 240,
242 | 3eqtrrd 2782 |
. . . . . . 7
⊢ (𝑢 ∈ (-1(,)1) → ((1 /
(√‘(1 − (𝑢↑2)))) + ((-(𝑢↑2) / (√‘(1 − (𝑢↑2)))) + (√‘(1
− (𝑢↑2))))) = (2
· (√‘(1 − (𝑢↑2))))) |
244 | 228, 243 | eqtrd 2777 |
. . . . . 6
⊢ (𝑢 ∈ (-1(,)1) → ((1 /
(√‘(1 − (𝑢↑2)))) + ((1 · (√‘(1
− (𝑢↑2)))) +
((-𝑢 / (√‘(1
− (𝑢↑2))))
· 𝑢))) = (2 ·
(√‘(1 − (𝑢↑2))))) |
245 | 244 | mpteq2ia 5146 |
. . . . 5
⊢ (𝑢 ∈ (-1(,)1) ↦ ((1 /
(√‘(1 − (𝑢↑2)))) + ((1 · (√‘(1
− (𝑢↑2)))) +
((-𝑢 / (√‘(1
− (𝑢↑2))))
· 𝑢)))) = (𝑢 ∈ (-1(,)1) ↦ (2
· (√‘(1 − (𝑢↑2))))) |
246 | 211, 245 | eqtrdi 2794 |
. . . 4
⊢ (𝑅 ∈ ℝ+
→ (ℝ D (𝑢 ∈
(-1(,)1) ↦ ((arcsin‘𝑢) + (𝑢 · (√‘(1 − (𝑢↑2))))))) = (𝑢 ∈ (-1(,)1) ↦ (2
· (√‘(1 − (𝑢↑2)))))) |
247 | | fveq2 6717 |
. . . . 5
⊢ (𝑢 = (𝑡 / 𝑅) → (arcsin‘𝑢) = (arcsin‘(𝑡 / 𝑅))) |
248 | | id 22 |
. . . . . 6
⊢ (𝑢 = (𝑡 / 𝑅) → 𝑢 = (𝑡 / 𝑅)) |
249 | | oveq1 7220 |
. . . . . . . 8
⊢ (𝑢 = (𝑡 / 𝑅) → (𝑢↑2) = ((𝑡 / 𝑅)↑2)) |
250 | 249 | oveq2d 7229 |
. . . . . . 7
⊢ (𝑢 = (𝑡 / 𝑅) → (1 − (𝑢↑2)) = (1 − ((𝑡 / 𝑅)↑2))) |
251 | 250 | fveq2d 6721 |
. . . . . 6
⊢ (𝑢 = (𝑡 / 𝑅) → (√‘(1 − (𝑢↑2))) = (√‘(1
− ((𝑡 / 𝑅)↑2)))) |
252 | 248, 251 | oveq12d 7231 |
. . . . 5
⊢ (𝑢 = (𝑡 / 𝑅) → (𝑢 · (√‘(1 − (𝑢↑2)))) = ((𝑡 / 𝑅) · (√‘(1 − ((𝑡 / 𝑅)↑2))))) |
253 | 247, 252 | oveq12d 7231 |
. . . 4
⊢ (𝑢 = (𝑡 / 𝑅) → ((arcsin‘𝑢) + (𝑢 · (√‘(1 − (𝑢↑2))))) =
((arcsin‘(𝑡 / 𝑅)) + ((𝑡 / 𝑅) · (√‘(1 − ((𝑡 / 𝑅)↑2)))))) |
254 | 251 | oveq2d 7229 |
. . . 4
⊢ (𝑢 = (𝑡 / 𝑅) → (2 · (√‘(1
− (𝑢↑2)))) = (2
· (√‘(1 − ((𝑡 / 𝑅)↑2))))) |
255 | 2, 2, 58, 59, 71, 72, 84, 246, 253, 254 | dvmptco 24869 |
. . 3
⊢ (𝑅 ∈ ℝ+
→ (ℝ D (𝑡 ∈
(-𝑅(,)𝑅) ↦ ((arcsin‘(𝑡 / 𝑅)) + ((𝑡 / 𝑅) · (√‘(1 − ((𝑡 / 𝑅)↑2))))))) = (𝑡 ∈ (-𝑅(,)𝑅) ↦ ((2 · (√‘(1
− ((𝑡 / 𝑅)↑2)))) · (1 / 𝑅)))) |
256 | 6 | sqcld 13714 |
. . 3
⊢ (𝑅 ∈ ℝ+
→ (𝑅↑2) ∈
ℂ) |
257 | 2, 18, 19, 255, 256 | dvmptcmul 24861 |
. 2
⊢ (𝑅 ∈ ℝ+
→ (ℝ D (𝑡 ∈
(-𝑅(,)𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑡 / 𝑅)) + ((𝑡 / 𝑅) · (√‘(1 − ((𝑡 / 𝑅)↑2)))))))) = (𝑡 ∈ (-𝑅(,)𝑅) ↦ ((𝑅↑2) · ((2 ·
(√‘(1 − ((𝑡 / 𝑅)↑2)))) · (1 / 𝑅))))) |
258 | | 2cnd 11908 |
. . . . . . 7
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → 2 ∈ ℂ) |
259 | 258, 16 | mulcld 10853 |
. . . . . 6
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (2 · (√‘(1
− ((𝑡 / 𝑅)↑2)))) ∈
ℂ) |
260 | 6, 8 | reccld 11601 |
. . . . . . 7
⊢ (𝑅 ∈ ℝ+
→ (1 / 𝑅) ∈
ℂ) |
261 | 260 | adantr 484 |
. . . . . 6
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (1 / 𝑅) ∈ ℂ) |
262 | 259, 261 | mulcomd 10854 |
. . . . 5
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → ((2 · (√‘(1
− ((𝑡 / 𝑅)↑2)))) · (1 / 𝑅)) = ((1 / 𝑅) · (2 · (√‘(1
− ((𝑡 / 𝑅)↑2)))))) |
263 | 262 | oveq2d 7229 |
. . . 4
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → ((𝑅↑2) · ((2 ·
(√‘(1 − ((𝑡 / 𝑅)↑2)))) · (1 / 𝑅))) = ((𝑅↑2) · ((1 / 𝑅) · (2 · (√‘(1
− ((𝑡 / 𝑅)↑2))))))) |
264 | 256 | adantr 484 |
. . . . 5
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (𝑅↑2) ∈ ℂ) |
265 | 264, 261,
259 | mulassd 10856 |
. . . 4
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (((𝑅↑2) · (1 / 𝑅)) · (2 · (√‘(1
− ((𝑡 / 𝑅)↑2))))) = ((𝑅↑2) · ((1 / 𝑅) · (2 ·
(√‘(1 − ((𝑡 / 𝑅)↑2))))))) |
266 | 6 | sqvald 13713 |
. . . . . . . . 9
⊢ (𝑅 ∈ ℝ+
→ (𝑅↑2) = (𝑅 · 𝑅)) |
267 | 266 | oveq1d 7228 |
. . . . . . . 8
⊢ (𝑅 ∈ ℝ+
→ ((𝑅↑2) / 𝑅) = ((𝑅 · 𝑅) / 𝑅)) |
268 | 256, 6, 8 | divrecd 11611 |
. . . . . . . 8
⊢ (𝑅 ∈ ℝ+
→ ((𝑅↑2) / 𝑅) = ((𝑅↑2) · (1 / 𝑅))) |
269 | 6, 6, 8 | divcan3d 11613 |
. . . . . . . 8
⊢ (𝑅 ∈ ℝ+
→ ((𝑅 · 𝑅) / 𝑅) = 𝑅) |
270 | 267, 268,
269 | 3eqtr3d 2785 |
. . . . . . 7
⊢ (𝑅 ∈ ℝ+
→ ((𝑅↑2) ·
(1 / 𝑅)) = 𝑅) |
271 | 270 | adantr 484 |
. . . . . 6
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → ((𝑅↑2) · (1 / 𝑅)) = 𝑅) |
272 | 271 | oveq1d 7228 |
. . . . 5
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (((𝑅↑2) · (1 / 𝑅)) · (2 · (√‘(1
− ((𝑡 / 𝑅)↑2))))) = (𝑅 · (2 ·
(√‘(1 − ((𝑡 / 𝑅)↑2)))))) |
273 | 7, 258, 16 | mul12d 11041 |
. . . . 5
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (𝑅 · (2 · (√‘(1
− ((𝑡 / 𝑅)↑2))))) = (2 ·
(𝑅 ·
(√‘(1 − ((𝑡 / 𝑅)↑2)))))) |
274 | 20 | resqcld 13817 |
. . . . . . . . 9
⊢ (𝑅 ∈ ℝ+
→ (𝑅↑2) ∈
ℝ) |
275 | 274 | adantr 484 |
. . . . . . . 8
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (𝑅↑2) ∈ ℝ) |
276 | 20 | sqge0d 13818 |
. . . . . . . . 9
⊢ (𝑅 ∈ ℝ+
→ 0 ≤ (𝑅↑2)) |
277 | 276 | adantr 484 |
. . . . . . . 8
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → 0 ≤ (𝑅↑2)) |
278 | | 1red 10834 |
. . . . . . . . 9
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → 1 ∈ ℝ) |
279 | 3 | adantl 485 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → 𝑡 ∈ ℝ) |
280 | 20 | adantr 484 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → 𝑅 ∈ ℝ) |
281 | 279, 280,
9 | redivcld 11660 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (𝑡 / 𝑅) ∈ ℝ) |
282 | 281 | resqcld 13817 |
. . . . . . . . 9
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → ((𝑡 / 𝑅)↑2) ∈ ℝ) |
283 | 278, 282 | resubcld 11260 |
. . . . . . . 8
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (1 − ((𝑡 / 𝑅)↑2)) ∈ ℝ) |
284 | | 0red 10836 |
. . . . . . . . 9
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → 0 ∈ ℝ) |
285 | 26, 27 | absltd 14993 |
. . . . . . . . . . . . . . 15
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ ((abs‘𝑡) <
𝑅 ↔ (-𝑅 < 𝑡 ∧ 𝑡 < 𝑅))) |
286 | 73 | abscld 15000 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑡 ∈ ℝ →
(abs‘𝑡) ∈
ℝ) |
287 | 286 | adantl 485 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ (abs‘𝑡) ∈
ℝ) |
288 | 73 | absge0d 15008 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑡 ∈ ℝ → 0 ≤
(abs‘𝑡)) |
289 | 288 | adantl 485 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ 0 ≤ (abs‘𝑡)) |
290 | | rpge0 12599 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑅 ∈ ℝ+
→ 0 ≤ 𝑅) |
291 | 290 | adantr 484 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ 0 ≤ 𝑅) |
292 | 287, 27, 289, 291 | lt2sqd 13825 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ ((abs‘𝑡) <
𝑅 ↔ ((abs‘𝑡)↑2) < (𝑅↑2))) |
293 | | absresq 14866 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑡 ∈ ℝ →
((abs‘𝑡)↑2) =
(𝑡↑2)) |
294 | 293 | adantl 485 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ ((abs‘𝑡)↑2) = (𝑡↑2)) |
295 | 256 | adantr 484 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ (𝑅↑2) ∈
ℂ) |
296 | 295 | mulid1d 10850 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ ((𝑅↑2) ·
1) = (𝑅↑2)) |
297 | 296 | eqcomd 2743 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ (𝑅↑2) = ((𝑅↑2) ·
1)) |
298 | 294, 297 | breq12d 5066 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ (((abs‘𝑡)↑2) < (𝑅↑2) ↔ (𝑡↑2) < ((𝑅↑2) · 1))) |
299 | 6 | adantr 484 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ 𝑅 ∈
ℂ) |
300 | 74, 299, 28 | sqdivd 13729 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ ((𝑡 / 𝑅)↑2) = ((𝑡↑2) / (𝑅↑2))) |
301 | 300 | breq1d 5063 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ (((𝑡 / 𝑅)↑2) < 1 ↔ ((𝑡↑2) / (𝑅↑2)) < 1)) |
302 | 29 | resqcld 13817 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ ((𝑡 / 𝑅)↑2) ∈
ℝ) |
303 | 302, 41 | posdifd 11419 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ (((𝑡 / 𝑅)↑2) < 1 ↔ 0 <
(1 − ((𝑡 / 𝑅)↑2)))) |
304 | | resqcl 13696 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑡 ∈ ℝ → (𝑡↑2) ∈
ℝ) |
305 | 304 | adantl 485 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ (𝑡↑2) ∈
ℝ) |
306 | | rpgt0 12598 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑅 ∈ ℝ+
→ 0 < 𝑅) |
307 | | 0red 10836 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑅 ∈ ℝ+
→ 0 ∈ ℝ) |
308 | | 0le0 11931 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 0 ≤
0 |
309 | 308 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑅 ∈ ℝ+
→ 0 ≤ 0) |
310 | 307, 20, 309, 290 | lt2sqd 13825 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑅 ∈ ℝ+
→ (0 < 𝑅 ↔
(0↑2) < (𝑅↑2))) |
311 | | sq0 13761 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(0↑2) = 0 |
312 | 311 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑅 ∈ ℝ+
→ (0↑2) = 0) |
313 | 312 | breq1d 5063 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑅 ∈ ℝ+
→ ((0↑2) < (𝑅↑2) ↔ 0 < (𝑅↑2))) |
314 | 310, 313 | bitrd 282 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑅 ∈ ℝ+
→ (0 < 𝑅 ↔ 0
< (𝑅↑2))) |
315 | 306, 314 | mpbid 235 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑅 ∈ ℝ+
→ 0 < (𝑅↑2)) |
316 | 274, 315 | elrpd 12625 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑅 ∈ ℝ+
→ (𝑅↑2) ∈
ℝ+) |
317 | 316 | adantr 484 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ (𝑅↑2) ∈
ℝ+) |
318 | 305, 41, 317 | ltdivmuld 12679 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ (((𝑡↑2) /
(𝑅↑2)) < 1 ↔
(𝑡↑2) < ((𝑅↑2) ·
1))) |
319 | 301, 303,
318 | 3bitr3rd 313 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ ((𝑡↑2) <
((𝑅↑2) · 1)
↔ 0 < (1 − ((𝑡 / 𝑅)↑2)))) |
320 | 292, 298,
319 | 3bitrd 308 |
. . . . . . . . . . . . . . 15
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ ((abs‘𝑡) <
𝑅 ↔ 0 < (1 −
((𝑡 / 𝑅)↑2)))) |
321 | 285, 320 | bitr3d 284 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ ((-𝑅 < 𝑡 ∧ 𝑡 < 𝑅) ↔ 0 < (1 − ((𝑡 / 𝑅)↑2)))) |
322 | 321 | biimpd 232 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ ((-𝑅 < 𝑡 ∧ 𝑡 < 𝑅) → 0 < (1 − ((𝑡 / 𝑅)↑2)))) |
323 | 322 | exp4b 434 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ ℝ+
→ (𝑡 ∈ ℝ
→ (-𝑅 < 𝑡 → (𝑡 < 𝑅 → 0 < (1 − ((𝑡 / 𝑅)↑2)))))) |
324 | 323 | 3impd 1350 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ ℝ+
→ ((𝑡 ∈ ℝ
∧ -𝑅 < 𝑡 ∧ 𝑡 < 𝑅) → 0 < (1 − ((𝑡 / 𝑅)↑2)))) |
325 | 25, 324 | sylbid 243 |
. . . . . . . . . 10
⊢ (𝑅 ∈ ℝ+
→ (𝑡 ∈ (-𝑅(,)𝑅) → 0 < (1 − ((𝑡 / 𝑅)↑2)))) |
326 | 325 | imp 410 |
. . . . . . . . 9
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → 0 < (1 − ((𝑡 / 𝑅)↑2))) |
327 | 284, 283,
326 | ltled 10980 |
. . . . . . . 8
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → 0 ≤ (1 − ((𝑡 / 𝑅)↑2))) |
328 | 275, 277,
283, 327 | sqrtmuld 14988 |
. . . . . . 7
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (√‘((𝑅↑2) · (1 − ((𝑡 / 𝑅)↑2)))) = ((√‘(𝑅↑2)) ·
(√‘(1 − ((𝑡 / 𝑅)↑2))))) |
329 | 264, 13, 14 | subdid 11288 |
. . . . . . . . 9
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → ((𝑅↑2) · (1 − ((𝑡 / 𝑅)↑2))) = (((𝑅↑2) · 1) − ((𝑅↑2) · ((𝑡 / 𝑅)↑2)))) |
330 | 264 | mulid1d 10850 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → ((𝑅↑2) · 1) = (𝑅↑2)) |
331 | 5, 7, 9 | sqdivd 13729 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → ((𝑡 / 𝑅)↑2) = ((𝑡↑2) / (𝑅↑2))) |
332 | 331 | oveq2d 7229 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → ((𝑅↑2) · ((𝑡 / 𝑅)↑2)) = ((𝑅↑2) · ((𝑡↑2) / (𝑅↑2)))) |
333 | 4 | sqcld 13714 |
. . . . . . . . . . . . 13
⊢ (𝑡 ∈ (-𝑅(,)𝑅) → (𝑡↑2) ∈ ℂ) |
334 | 333 | adantl 485 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (𝑡↑2) ∈ ℂ) |
335 | | sqne0 13695 |
. . . . . . . . . . . . . . 15
⊢ (𝑅 ∈ ℂ → ((𝑅↑2) ≠ 0 ↔ 𝑅 ≠ 0)) |
336 | 6, 335 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝑅 ∈ ℝ+
→ ((𝑅↑2) ≠ 0
↔ 𝑅 ≠
0)) |
337 | 8, 336 | mpbird 260 |
. . . . . . . . . . . . 13
⊢ (𝑅 ∈ ℝ+
→ (𝑅↑2) ≠
0) |
338 | 337 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (𝑅↑2) ≠ 0) |
339 | 334, 264,
338 | divcan2d 11610 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → ((𝑅↑2) · ((𝑡↑2) / (𝑅↑2))) = (𝑡↑2)) |
340 | 332, 339 | eqtrd 2777 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → ((𝑅↑2) · ((𝑡 / 𝑅)↑2)) = (𝑡↑2)) |
341 | 330, 340 | oveq12d 7231 |
. . . . . . . . 9
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (((𝑅↑2) · 1) − ((𝑅↑2) · ((𝑡 / 𝑅)↑2))) = ((𝑅↑2) − (𝑡↑2))) |
342 | 329, 341 | eqtrd 2777 |
. . . . . . . 8
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → ((𝑅↑2) · (1 − ((𝑡 / 𝑅)↑2))) = ((𝑅↑2) − (𝑡↑2))) |
343 | 342 | fveq2d 6721 |
. . . . . . 7
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (√‘((𝑅↑2) · (1 − ((𝑡 / 𝑅)↑2)))) = (√‘((𝑅↑2) − (𝑡↑2)))) |
344 | 20, 290 | sqrtsqd 14983 |
. . . . . . . . 9
⊢ (𝑅 ∈ ℝ+
→ (√‘(𝑅↑2)) = 𝑅) |
345 | 344 | adantr 484 |
. . . . . . . 8
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (√‘(𝑅↑2)) = 𝑅) |
346 | 345 | oveq1d 7228 |
. . . . . . 7
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → ((√‘(𝑅↑2)) · (√‘(1 −
((𝑡 / 𝑅)↑2)))) = (𝑅 · (√‘(1 − ((𝑡 / 𝑅)↑2))))) |
347 | 328, 343,
346 | 3eqtr3rd 2786 |
. . . . . 6
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (𝑅 · (√‘(1 − ((𝑡 / 𝑅)↑2)))) = (√‘((𝑅↑2) − (𝑡↑2)))) |
348 | 347 | oveq2d 7229 |
. . . . 5
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (2 · (𝑅 · (√‘(1 − ((𝑡 / 𝑅)↑2))))) = (2 ·
(√‘((𝑅↑2)
− (𝑡↑2))))) |
349 | 272, 273,
348 | 3eqtrd 2781 |
. . . 4
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → (((𝑅↑2) · (1 / 𝑅)) · (2 · (√‘(1
− ((𝑡 / 𝑅)↑2))))) = (2 ·
(√‘((𝑅↑2)
− (𝑡↑2))))) |
350 | 263, 265,
349 | 3eqtr2d 2783 |
. . 3
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅(,)𝑅)) → ((𝑅↑2) · ((2 ·
(√‘(1 − ((𝑡 / 𝑅)↑2)))) · (1 / 𝑅))) = (2 · (√‘((𝑅↑2) − (𝑡↑2))))) |
351 | 350 | mpteq2dva 5150 |
. 2
⊢ (𝑅 ∈ ℝ+
→ (𝑡 ∈ (-𝑅(,)𝑅) ↦ ((𝑅↑2) · ((2 ·
(√‘(1 − ((𝑡 / 𝑅)↑2)))) · (1 / 𝑅)))) = (𝑡 ∈ (-𝑅(,)𝑅) ↦ (2 · (√‘((𝑅↑2) − (𝑡↑2)))))) |
352 | 257, 351 | eqtrd 2777 |
1
⊢ (𝑅 ∈ ℝ+
→ (ℝ D (𝑡 ∈
(-𝑅(,)𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑡 / 𝑅)) + ((𝑡 / 𝑅) · (√‘(1 − ((𝑡 / 𝑅)↑2)))))))) = (𝑡 ∈ (-𝑅(,)𝑅) ↦ (2 · (√‘((𝑅↑2) − (𝑡↑2)))))) |