Proof of Theorem areacirclem4
Step | Hyp | Ref
| Expression |
1 | | rpcn 12596 |
. . . 4
⊢ (𝑅 ∈ ℝ+
→ 𝑅 ∈
ℂ) |
2 | 1 | sqcld 13714 |
. . 3
⊢ (𝑅 ∈ ℝ+
→ (𝑅↑2) ∈
ℂ) |
3 | | rpre 12594 |
. . . . . 6
⊢ (𝑅 ∈ ℝ+
→ 𝑅 ∈
ℝ) |
4 | 3 | renegcld 11259 |
. . . . 5
⊢ (𝑅 ∈ ℝ+
→ -𝑅 ∈
ℝ) |
5 | | iccssre 13017 |
. . . . 5
⊢ ((-𝑅 ∈ ℝ ∧ 𝑅 ∈ ℝ) → (-𝑅[,]𝑅) ⊆ ℝ) |
6 | 4, 3, 5 | syl2anc 587 |
. . . 4
⊢ (𝑅 ∈ ℝ+
→ (-𝑅[,]𝑅) ⊆
ℝ) |
7 | | ax-resscn 10786 |
. . . 4
⊢ ℝ
⊆ ℂ |
8 | 6, 7 | sstrdi 3913 |
. . 3
⊢ (𝑅 ∈ ℝ+
→ (-𝑅[,]𝑅) ⊆
ℂ) |
9 | | ssid 3923 |
. . . 4
⊢ ℂ
⊆ ℂ |
10 | 9 | a1i 11 |
. . 3
⊢ (𝑅 ∈ ℝ+
→ ℂ ⊆ ℂ) |
11 | | cncfmptc 23809 |
. . 3
⊢ (((𝑅↑2) ∈ ℂ ∧
(-𝑅[,]𝑅) ⊆ ℂ ∧ ℂ ⊆
ℂ) → (𝑡 ∈
(-𝑅[,]𝑅) ↦ (𝑅↑2)) ∈ ((-𝑅[,]𝑅)–cn→ℂ)) |
12 | 2, 8, 10, 11 | syl3anc 1373 |
. 2
⊢ (𝑅 ∈ ℝ+
→ (𝑡 ∈ (-𝑅[,]𝑅) ↦ (𝑅↑2)) ∈ ((-𝑅[,]𝑅)–cn→ℂ)) |
13 | | eqid 2737 |
. . 3
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
14 | 13 | addcn 23762 |
. . . 4
⊢ + ∈
(((TopOpen‘ℂfld) ×t
(TopOpen‘ℂfld)) Cn
(TopOpen‘ℂfld)) |
15 | 14 | a1i 11 |
. . 3
⊢ (𝑅 ∈ ℝ+
→ + ∈ (((TopOpen‘ℂfld) ×t
(TopOpen‘ℂfld)) Cn
(TopOpen‘ℂfld))) |
16 | 8 | sselda 3901 |
. . . . . . . 8
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅[,]𝑅)) → 𝑡 ∈ ℂ) |
17 | 1 | adantr 484 |
. . . . . . . 8
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅[,]𝑅)) → 𝑅 ∈ ℂ) |
18 | | rpne0 12602 |
. . . . . . . . 9
⊢ (𝑅 ∈ ℝ+
→ 𝑅 ≠
0) |
19 | 18 | adantr 484 |
. . . . . . . 8
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅[,]𝑅)) → 𝑅 ≠ 0) |
20 | 16, 17, 19 | divcld 11608 |
. . . . . . 7
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (𝑡 / 𝑅) ∈ ℂ) |
21 | | asinval 25765 |
. . . . . . 7
⊢ ((𝑡 / 𝑅) ∈ ℂ → (arcsin‘(𝑡 / 𝑅)) = (-i · (log‘((i ·
(𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2))))))) |
22 | 20, 21 | syl 17 |
. . . . . 6
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (arcsin‘(𝑡 / 𝑅)) = (-i · (log‘((i ·
(𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2))))))) |
23 | | ax-icn 10788 |
. . . . . . . . . . . 12
⊢ i ∈
ℂ |
24 | 23 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅[,]𝑅)) → i ∈ ℂ) |
25 | 24, 20 | mulcld 10853 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (i · (𝑡 / 𝑅)) ∈ ℂ) |
26 | | 1cnd 10828 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅[,]𝑅)) → 1 ∈ ℂ) |
27 | 20 | sqcld 13714 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑡 / 𝑅)↑2) ∈ ℂ) |
28 | 26, 27 | subcld 11189 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (1 − ((𝑡 / 𝑅)↑2)) ∈ ℂ) |
29 | 28 | sqrtcld 15001 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (√‘(1 − ((𝑡 / 𝑅)↑2))) ∈ ℂ) |
30 | 25, 29 | addcld 10852 |
. . . . . . . . 9
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅[,]𝑅)) → ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈
ℂ) |
31 | | 0lt1 11354 |
. . . . . . . . . . . . . . 15
⊢ 0 <
1 |
32 | | simp3 1140 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → 𝑡 = 0) |
33 | 32 | oveq1d 7228 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → (𝑡 / 𝑅) = (0 / 𝑅)) |
34 | 1, 18 | div0d 11607 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑅 ∈ ℝ+
→ (0 / 𝑅) =
0) |
35 | 34 | 3ad2ant1 1135 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → (0 / 𝑅) = 0) |
36 | 33, 35 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → (𝑡 / 𝑅) = 0) |
37 | 36 | oveq2d 7229 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → (i · (𝑡 / 𝑅)) = (i · 0)) |
38 | | it0e0 12052 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (i
· 0) = 0 |
39 | 37, 38 | eqtrdi 2794 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → (i · (𝑡 / 𝑅)) = 0) |
40 | 36 | oveq1d 7228 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → ((𝑡 / 𝑅)↑2) = (0↑2)) |
41 | 40 | oveq2d 7229 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → (1 − ((𝑡 / 𝑅)↑2)) = (1 −
(0↑2))) |
42 | 41 | fveq2d 6721 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → (√‘(1 −
((𝑡 / 𝑅)↑2))) = (√‘(1 −
(0↑2)))) |
43 | | sq0 13761 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(0↑2) = 0 |
44 | 43 | oveq2i 7224 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (1
− (0↑2)) = (1 − 0) |
45 | | 1m0e1 11951 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (1
− 0) = 1 |
46 | 44, 45 | eqtri 2765 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (1
− (0↑2)) = 1 |
47 | 46 | fveq2i 6720 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(√‘(1 − (0↑2))) =
(√‘1) |
48 | | sqrt1 14835 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(√‘1) = 1 |
49 | 47, 48 | eqtri 2765 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(√‘(1 − (0↑2))) = 1 |
50 | 42, 49 | eqtrdi 2794 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → (√‘(1 −
((𝑡 / 𝑅)↑2))) = 1) |
51 | 39, 50 | oveq12d 7231 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) = (0 + 1)) |
52 | | 0p1e1 11952 |
. . . . . . . . . . . . . . . . . 18
⊢ (0 + 1) =
1 |
53 | 51, 52 | eqtrdi 2794 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) = 1) |
54 | 53 | breq2d 5065 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → (0 < ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ↔ 0 <
1)) |
55 | | 0red 10836 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → 0 ∈
ℝ) |
56 | | 1red 10834 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → 1 ∈
ℝ) |
57 | 53, 56 | eqeltrd 2838 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈
ℝ) |
58 | 55, 57 | ltnled 10979 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → (0 < ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ↔ ¬ ((i ·
(𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ≤ 0)) |
59 | 54, 58 | bitr3d 284 |
. . . . . . . . . . . . . . 15
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → (0 < 1 ↔ ¬ ((i
· (𝑡 / 𝑅)) + (√‘(1 −
((𝑡 / 𝑅)↑2)))) ≤ 0)) |
60 | 31, 59 | mpbii 236 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → ¬ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ≤ 0) |
61 | 60 | 3expa 1120 |
. . . . . . . . . . . . 13
⊢ (((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅[,]𝑅)) ∧ 𝑡 = 0) → ¬ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ≤ 0) |
62 | 61 | olcd 874 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅[,]𝑅)) ∧ 𝑡 = 0) → (¬ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ ∨ ¬ ((i
· (𝑡 / 𝑅)) + (√‘(1 −
((𝑡 / 𝑅)↑2)))) ≤ 0)) |
63 | | inelr 11820 |
. . . . . . . . . . . . . 14
⊢ ¬ i
∈ ℝ |
64 | 25, 29 | pncand 11190 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) − (√‘(1
− ((𝑡 / 𝑅)↑2)))) = (i ·
(𝑡 / 𝑅))) |
65 | 64 | 3adant3 1134 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → (((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) − (√‘(1
− ((𝑡 / 𝑅)↑2)))) = (i ·
(𝑡 / 𝑅))) |
66 | 65 | oveq1d 7228 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → ((((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) − (√‘(1
− ((𝑡 / 𝑅)↑2)))) · (𝑅 / 𝑡)) = ((i · (𝑡 / 𝑅)) · (𝑅 / 𝑡))) |
67 | 23 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → i ∈
ℂ) |
68 | 20 | 3adant3 1134 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → (𝑡 / 𝑅) ∈ ℂ) |
69 | 1 | 3ad2ant1 1135 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → 𝑅 ∈ ℂ) |
70 | 16 | 3adant3 1134 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → 𝑡 ∈ ℂ) |
71 | | simp3 1140 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → 𝑡 ≠ 0) |
72 | 69, 70, 71 | divcld 11608 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → (𝑅 / 𝑡) ∈ ℂ) |
73 | 67, 68, 72 | mulassd 10856 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → ((i · (𝑡 / 𝑅)) · (𝑅 / 𝑡)) = (i · ((𝑡 / 𝑅) · (𝑅 / 𝑡)))) |
74 | 66, 73 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → ((((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) − (√‘(1
− ((𝑡 / 𝑅)↑2)))) · (𝑅 / 𝑡)) = (i · ((𝑡 / 𝑅) · (𝑅 / 𝑡)))) |
75 | 18 | 3ad2ant1 1135 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → 𝑅 ≠ 0) |
76 | 70, 69, 71, 75 | divcan6d 11627 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → ((𝑡 / 𝑅) · (𝑅 / 𝑡)) = 1) |
77 | 76 | oveq2d 7229 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → (i · ((𝑡 / 𝑅) · (𝑅 / 𝑡))) = (i · 1)) |
78 | 67 | mulid1d 10850 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → (i · 1) =
i) |
79 | 74, 77, 78 | 3eqtrrd 2782 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → i = ((((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) − (√‘(1
− ((𝑡 / 𝑅)↑2)))) · (𝑅 / 𝑡))) |
80 | 79 | adantr 484 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) ∧ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ) → i =
((((i · (𝑡 / 𝑅)) + (√‘(1 −
((𝑡 / 𝑅)↑2)))) − (√‘(1
− ((𝑡 / 𝑅)↑2)))) · (𝑅 / 𝑡))) |
81 | | simpr 488 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) ∧ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ) → ((i
· (𝑡 / 𝑅)) + (√‘(1 −
((𝑡 / 𝑅)↑2)))) ∈
ℝ) |
82 | | 1red 10834 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅[,]𝑅)) → 1 ∈ ℝ) |
83 | 6 | sselda 3901 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅[,]𝑅)) → 𝑡 ∈ ℝ) |
84 | 3 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅[,]𝑅)) → 𝑅 ∈ ℝ) |
85 | 83, 84, 19 | redivcld 11660 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (𝑡 / 𝑅) ∈ ℝ) |
86 | 85 | resqcld 13817 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑡 / 𝑅)↑2) ∈ ℝ) |
87 | 82, 86 | resubcld 11260 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (1 − ((𝑡 / 𝑅)↑2)) ∈ ℝ) |
88 | | elicc2 13000 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((-𝑅 ∈ ℝ ∧ 𝑅 ∈ ℝ) → (𝑡 ∈ (-𝑅[,]𝑅) ↔ (𝑡 ∈ ℝ ∧ -𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅))) |
89 | 4, 3, 88 | syl2anc 587 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑅 ∈ ℝ+
→ (𝑡 ∈ (-𝑅[,]𝑅) ↔ (𝑡 ∈ ℝ ∧ -𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅))) |
90 | | 1red 10834 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ 1 ∈ ℝ) |
91 | | simpr 488 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ 𝑡 ∈
ℝ) |
92 | 3 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ 𝑅 ∈
ℝ) |
93 | 18 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ 𝑅 ≠
0) |
94 | 91, 92, 93 | redivcld 11660 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ (𝑡 / 𝑅) ∈
ℝ) |
95 | 94 | resqcld 13817 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ ((𝑡 / 𝑅)↑2) ∈
ℝ) |
96 | 90, 95 | subge0d 11422 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ (0 ≤ (1 − ((𝑡 / 𝑅)↑2)) ↔ ((𝑡 / 𝑅)↑2) ≤ 1)) |
97 | | recn 10819 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑡 ∈ ℝ → 𝑡 ∈
ℂ) |
98 | 97 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ 𝑡 ∈
ℂ) |
99 | 1 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ 𝑅 ∈
ℂ) |
100 | 98, 99, 93 | sqdivd 13729 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ ((𝑡 / 𝑅)↑2) = ((𝑡↑2) / (𝑅↑2))) |
101 | 100 | breq1d 5063 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ (((𝑡 / 𝑅)↑2) ≤ 1 ↔ ((𝑡↑2) / (𝑅↑2)) ≤ 1)) |
102 | | resqcl 13696 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑡 ∈ ℝ → (𝑡↑2) ∈
ℝ) |
103 | 102 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ (𝑡↑2) ∈
ℝ) |
104 | 3 | resqcld 13817 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑅 ∈ ℝ+
→ (𝑅↑2) ∈
ℝ) |
105 | | rpgt0 12598 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑅 ∈ ℝ+
→ 0 < 𝑅) |
106 | | 0red 10836 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑅 ∈ ℝ+
→ 0 ∈ ℝ) |
107 | | 0le0 11931 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ 0 ≤
0 |
108 | 107 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑅 ∈ ℝ+
→ 0 ≤ 0) |
109 | | rpge0 12599 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑅 ∈ ℝ+
→ 0 ≤ 𝑅) |
110 | 106, 3, 108, 109 | lt2sqd 13825 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑅 ∈ ℝ+
→ (0 < 𝑅 ↔
(0↑2) < (𝑅↑2))) |
111 | 43 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑅 ∈ ℝ+
→ (0↑2) = 0) |
112 | 111 | breq1d 5063 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑅 ∈ ℝ+
→ ((0↑2) < (𝑅↑2) ↔ 0 < (𝑅↑2))) |
113 | 110, 112 | bitrd 282 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑅 ∈ ℝ+
→ (0 < 𝑅 ↔ 0
< (𝑅↑2))) |
114 | 105, 113 | mpbid 235 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑅 ∈ ℝ+
→ 0 < (𝑅↑2)) |
115 | 104, 114 | elrpd 12625 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑅 ∈ ℝ+
→ (𝑅↑2) ∈
ℝ+) |
116 | 115 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ (𝑅↑2) ∈
ℝ+) |
117 | 103, 90, 116 | ledivmuld 12681 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ (((𝑡↑2) /
(𝑅↑2)) ≤ 1 ↔
(𝑡↑2) ≤ ((𝑅↑2) ·
1))) |
118 | | absresq 14866 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑡 ∈ ℝ →
((abs‘𝑡)↑2) =
(𝑡↑2)) |
119 | 118 | eqcomd 2743 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑡 ∈ ℝ → (𝑡↑2) = ((abs‘𝑡)↑2)) |
120 | 2 | mulid1d 10850 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑅 ∈ ℝ+
→ ((𝑅↑2) ·
1) = (𝑅↑2)) |
121 | 119, 120 | breqan12rd 5070 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ ((𝑡↑2) ≤
((𝑅↑2) · 1)
↔ ((abs‘𝑡)↑2) ≤ (𝑅↑2))) |
122 | 97 | abscld 15000 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑡 ∈ ℝ →
(abs‘𝑡) ∈
ℝ) |
123 | 122 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ (abs‘𝑡) ∈
ℝ) |
124 | 97 | absge0d 15008 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑡 ∈ ℝ → 0 ≤
(abs‘𝑡)) |
125 | 124 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ 0 ≤ (abs‘𝑡)) |
126 | 109 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ 0 ≤ 𝑅) |
127 | 123, 92, 125, 126 | le2sqd 13826 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ ((abs‘𝑡) ≤
𝑅 ↔ ((abs‘𝑡)↑2) ≤ (𝑅↑2))) |
128 | 91, 92 | absled 14994 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ ((abs‘𝑡) ≤
𝑅 ↔ (-𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅))) |
129 | 121, 127,
128 | 3bitr2d 310 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ ((𝑡↑2) ≤
((𝑅↑2) · 1)
↔ (-𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅))) |
130 | 117, 129 | bitrd 282 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ (((𝑡↑2) /
(𝑅↑2)) ≤ 1 ↔
(-𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅))) |
131 | 96, 101, 130 | 3bitrrd 309 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ ((-𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅) ↔ 0 ≤ (1 − ((𝑡 / 𝑅)↑2)))) |
132 | 131 | biimpd 232 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ ℝ)
→ ((-𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅) → 0 ≤ (1 − ((𝑡 / 𝑅)↑2)))) |
133 | 132 | exp4b 434 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑅 ∈ ℝ+
→ (𝑡 ∈ ℝ
→ (-𝑅 ≤ 𝑡 → (𝑡 ≤ 𝑅 → 0 ≤ (1 − ((𝑡 / 𝑅)↑2)))))) |
134 | 133 | 3impd 1350 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑅 ∈ ℝ+
→ ((𝑡 ∈ ℝ
∧ -𝑅 ≤ 𝑡 ∧ 𝑡 ≤ 𝑅) → 0 ≤ (1 − ((𝑡 / 𝑅)↑2)))) |
135 | 89, 134 | sylbid 243 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑅 ∈ ℝ+
→ (𝑡 ∈ (-𝑅[,]𝑅) → 0 ≤ (1 − ((𝑡 / 𝑅)↑2)))) |
136 | 135 | imp 410 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅[,]𝑅)) → 0 ≤ (1 − ((𝑡 / 𝑅)↑2))) |
137 | 87, 136 | resqrtcld 14981 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (√‘(1 − ((𝑡 / 𝑅)↑2))) ∈ ℝ) |
138 | 137 | 3adant3 1134 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → (√‘(1 −
((𝑡 / 𝑅)↑2))) ∈ ℝ) |
139 | 138 | adantr 484 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) ∧ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ) →
(√‘(1 − ((𝑡 / 𝑅)↑2))) ∈ ℝ) |
140 | 81, 139 | resubcld 11260 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) ∧ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ) → (((i
· (𝑡 / 𝑅)) + (√‘(1 −
((𝑡 / 𝑅)↑2)))) − (√‘(1
− ((𝑡 / 𝑅)↑2)))) ∈
ℝ) |
141 | 3 | 3ad2ant1 1135 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → 𝑅 ∈ ℝ) |
142 | 83 | 3adant3 1134 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → 𝑡 ∈ ℝ) |
143 | 141, 142,
71 | redivcld 11660 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → (𝑅 / 𝑡) ∈ ℝ) |
144 | 143 | adantr 484 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) ∧ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ) → (𝑅 / 𝑡) ∈ ℝ) |
145 | 140, 144 | remulcld 10863 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) ∧ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ) → ((((i
· (𝑡 / 𝑅)) + (√‘(1 −
((𝑡 / 𝑅)↑2)))) − (√‘(1
− ((𝑡 / 𝑅)↑2)))) · (𝑅 / 𝑡)) ∈ ℝ) |
146 | 80, 145 | eqeltrd 2838 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) ∧ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ) → i ∈
ℝ) |
147 | 146 | ex 416 |
. . . . . . . . . . . . . . 15
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → (((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ → i ∈
ℝ)) |
148 | 147 | 3expa 1120 |
. . . . . . . . . . . . . 14
⊢ (((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅[,]𝑅)) ∧ 𝑡 ≠ 0) → (((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ → i ∈
ℝ)) |
149 | 63, 148 | mtoi 202 |
. . . . . . . . . . . . 13
⊢ (((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅[,]𝑅)) ∧ 𝑡 ≠ 0) → ¬ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈
ℝ) |
150 | 149 | orcd 873 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅[,]𝑅)) ∧ 𝑡 ≠ 0) → (¬ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ ∨ ¬ ((i
· (𝑡 / 𝑅)) + (√‘(1 −
((𝑡 / 𝑅)↑2)))) ≤ 0)) |
151 | 62, 150 | pm2.61dane 3029 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (¬ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ ∨ ¬ ((i
· (𝑡 / 𝑅)) + (√‘(1 −
((𝑡 / 𝑅)↑2)))) ≤ 0)) |
152 | | ianor 982 |
. . . . . . . . . . 11
⊢ (¬
(((i · (𝑡 / 𝑅)) + (√‘(1 −
((𝑡 / 𝑅)↑2)))) ∈ ℝ ∧ ((i
· (𝑡 / 𝑅)) + (√‘(1 −
((𝑡 / 𝑅)↑2)))) ≤ 0) ↔ (¬ ((i
· (𝑡 / 𝑅)) + (√‘(1 −
((𝑡 / 𝑅)↑2)))) ∈ ℝ ∨ ¬ ((i
· (𝑡 / 𝑅)) + (√‘(1 −
((𝑡 / 𝑅)↑2)))) ≤ 0)) |
153 | 151, 152 | sylibr 237 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅[,]𝑅)) → ¬ (((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ ∧ ((i
· (𝑡 / 𝑅)) + (√‘(1 −
((𝑡 / 𝑅)↑2)))) ≤ 0)) |
154 | | mnfxr 10890 |
. . . . . . . . . . . 12
⊢ -∞
∈ ℝ* |
155 | | 0re 10835 |
. . . . . . . . . . . 12
⊢ 0 ∈
ℝ |
156 | | elioc2 12998 |
. . . . . . . . . . . 12
⊢
((-∞ ∈ ℝ* ∧ 0 ∈ ℝ) →
(((i · (𝑡 / 𝑅)) + (√‘(1 −
((𝑡 / 𝑅)↑2)))) ∈ (-∞(,]0) ↔
(((i · (𝑡 / 𝑅)) + (√‘(1 −
((𝑡 / 𝑅)↑2)))) ∈ ℝ ∧ -∞
< ((i · (𝑡 /
𝑅)) + (√‘(1
− ((𝑡 / 𝑅)↑2)))) ∧ ((i ·
(𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ≤ 0))) |
157 | 154, 155,
156 | mp2an 692 |
. . . . . . . . . . 11
⊢ (((i
· (𝑡 / 𝑅)) + (√‘(1 −
((𝑡 / 𝑅)↑2)))) ∈ (-∞(,]0) ↔
(((i · (𝑡 / 𝑅)) + (√‘(1 −
((𝑡 / 𝑅)↑2)))) ∈ ℝ ∧ -∞
< ((i · (𝑡 /
𝑅)) + (√‘(1
− ((𝑡 / 𝑅)↑2)))) ∧ ((i ·
(𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ≤ 0)) |
158 | | 3simpb 1151 |
. . . . . . . . . . 11
⊢ ((((i
· (𝑡 / 𝑅)) + (√‘(1 −
((𝑡 / 𝑅)↑2)))) ∈ ℝ ∧ -∞
< ((i · (𝑡 /
𝑅)) + (√‘(1
− ((𝑡 / 𝑅)↑2)))) ∧ ((i ·
(𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ≤ 0) → (((i ·
(𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ ∧ ((i
· (𝑡 / 𝑅)) + (√‘(1 −
((𝑡 / 𝑅)↑2)))) ≤ 0)) |
159 | 157, 158 | sylbi 220 |
. . . . . . . . . 10
⊢ (((i
· (𝑡 / 𝑅)) + (√‘(1 −
((𝑡 / 𝑅)↑2)))) ∈ (-∞(,]0) →
(((i · (𝑡 / 𝑅)) + (√‘(1 −
((𝑡 / 𝑅)↑2)))) ∈ ℝ ∧ ((i
· (𝑡 / 𝑅)) + (√‘(1 −
((𝑡 / 𝑅)↑2)))) ≤ 0)) |
160 | 153, 159 | nsyl 142 |
. . . . . . . . 9
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅[,]𝑅)) → ¬ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈
(-∞(,]0)) |
161 | 30, 160 | eldifd 3877 |
. . . . . . . 8
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅[,]𝑅)) → ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ (ℂ ∖
(-∞(,]0))) |
162 | | fvres 6736 |
. . . . . . . 8
⊢ (((i
· (𝑡 / 𝑅)) + (√‘(1 −
((𝑡 / 𝑅)↑2)))) ∈ (ℂ ∖
(-∞(,]0)) → ((log ↾ (ℂ ∖
(-∞(,]0)))‘((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2))))) = (log‘((i ·
(𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))))) |
163 | 161, 162 | syl 17 |
. . . . . . 7
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅[,]𝑅)) → ((log ↾ (ℂ ∖
(-∞(,]0)))‘((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2))))) = (log‘((i ·
(𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))))) |
164 | 163 | oveq2d 7229 |
. . . . . 6
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (-i · ((log ↾
(ℂ ∖ (-∞(,]0)))‘((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))))) = (-i · (log‘((i
· (𝑡 / 𝑅)) + (√‘(1 −
((𝑡 / 𝑅)↑2))))))) |
165 | 22, 164 | eqtr4d 2780 |
. . . . 5
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (arcsin‘(𝑡 / 𝑅)) = (-i · ((log ↾ (ℂ
∖ (-∞(,]0)))‘((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2))))))) |
166 | 165 | mpteq2dva 5150 |
. . . 4
⊢ (𝑅 ∈ ℝ+
→ (𝑡 ∈ (-𝑅[,]𝑅) ↦ (arcsin‘(𝑡 / 𝑅))) = (𝑡 ∈ (-𝑅[,]𝑅) ↦ (-i · ((log ↾
(ℂ ∖ (-∞(,]0)))‘((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))))))) |
167 | | negicn 11079 |
. . . . . . 7
⊢ -i ∈
ℂ |
168 | 167 | a1i 11 |
. . . . . 6
⊢ (𝑅 ∈ ℝ+
→ -i ∈ ℂ) |
169 | | cncfmptc 23809 |
. . . . . 6
⊢ ((-i
∈ ℂ ∧ (-𝑅[,]𝑅) ⊆ ℂ ∧ ℂ ⊆
ℂ) → (𝑡 ∈
(-𝑅[,]𝑅) ↦ -i) ∈ ((-𝑅[,]𝑅)–cn→ℂ)) |
170 | 168, 8, 10, 169 | syl3anc 1373 |
. . . . 5
⊢ (𝑅 ∈ ℝ+
→ (𝑡 ∈ (-𝑅[,]𝑅) ↦ -i) ∈ ((-𝑅[,]𝑅)–cn→ℂ)) |
171 | 13 | cnfldtopon 23680 |
. . . . . . . . 9
⊢
(TopOpen‘ℂfld) ∈
(TopOn‘ℂ) |
172 | 171 | a1i 11 |
. . . . . . . 8
⊢ (𝑅 ∈ ℝ+
→ (TopOpen‘ℂfld) ∈
(TopOn‘ℂ)) |
173 | | resttopon 22058 |
. . . . . . . 8
⊢
(((TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
∧ (-𝑅[,]𝑅) ⊆ ℂ) →
((TopOpen‘ℂfld) ↾t (-𝑅[,]𝑅)) ∈ (TopOn‘(-𝑅[,]𝑅))) |
174 | 172, 8, 173 | syl2anc 587 |
. . . . . . 7
⊢ (𝑅 ∈ ℝ+
→ ((TopOpen‘ℂfld) ↾t (-𝑅[,]𝑅)) ∈ (TopOn‘(-𝑅[,]𝑅))) |
175 | 161 | fmpttd 6932 |
. . . . . . . . 9
⊢ (𝑅 ∈ ℝ+
→ (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2))))):(-𝑅[,]𝑅)⟶(ℂ ∖
(-∞(,]0))) |
176 | | difssd 4047 |
. . . . . . . . . 10
⊢ (𝑅 ∈ ℝ+
→ (ℂ ∖ (-∞(,]0)) ⊆ ℂ) |
177 | 16, 17, 19 | divrec2d 11612 |
. . . . . . . . . . . . . . 15
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (𝑡 / 𝑅) = ((1 / 𝑅) · 𝑡)) |
178 | 177 | oveq2d 7229 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (i · (𝑡 / 𝑅)) = (i · ((1 / 𝑅) · 𝑡))) |
179 | 1, 18 | reccld 11601 |
. . . . . . . . . . . . . . . 16
⊢ (𝑅 ∈ ℝ+
→ (1 / 𝑅) ∈
ℂ) |
180 | 179 | adantr 484 |
. . . . . . . . . . . . . . 15
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (1 / 𝑅) ∈ ℂ) |
181 | 24, 180, 16 | mulassd 10856 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅[,]𝑅)) → ((i · (1 / 𝑅)) · 𝑡) = (i · ((1 / 𝑅) · 𝑡))) |
182 | 178, 181 | eqtr4d 2780 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (i · (𝑡 / 𝑅)) = ((i · (1 / 𝑅)) · 𝑡)) |
183 | 182 | mpteq2dva 5150 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ ℝ+
→ (𝑡 ∈ (-𝑅[,]𝑅) ↦ (i · (𝑡 / 𝑅))) = (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((i · (1 / 𝑅)) · 𝑡))) |
184 | 23 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝑅 ∈ ℝ+
→ i ∈ ℂ) |
185 | 184, 179 | mulcld 10853 |
. . . . . . . . . . . . . 14
⊢ (𝑅 ∈ ℝ+
→ (i · (1 / 𝑅))
∈ ℂ) |
186 | | cncfmptc 23809 |
. . . . . . . . . . . . . 14
⊢ (((i
· (1 / 𝑅)) ∈
ℂ ∧ (-𝑅[,]𝑅) ⊆ ℂ ∧ ℂ
⊆ ℂ) → (𝑡
∈ (-𝑅[,]𝑅) ↦ (i · (1 / 𝑅))) ∈ ((-𝑅[,]𝑅)–cn→ℂ)) |
187 | 185, 8, 10, 186 | syl3anc 1373 |
. . . . . . . . . . . . 13
⊢ (𝑅 ∈ ℝ+
→ (𝑡 ∈ (-𝑅[,]𝑅) ↦ (i · (1 / 𝑅))) ∈ ((-𝑅[,]𝑅)–cn→ℂ)) |
188 | | cncfmptid 23810 |
. . . . . . . . . . . . . 14
⊢ (((-𝑅[,]𝑅) ⊆ ℂ ∧ ℂ ⊆
ℂ) → (𝑡 ∈
(-𝑅[,]𝑅) ↦ 𝑡) ∈ ((-𝑅[,]𝑅)–cn→ℂ)) |
189 | 8, 10, 188 | syl2anc 587 |
. . . . . . . . . . . . 13
⊢ (𝑅 ∈ ℝ+
→ (𝑡 ∈ (-𝑅[,]𝑅) ↦ 𝑡) ∈ ((-𝑅[,]𝑅)–cn→ℂ)) |
190 | 187, 189 | mulcncf 24343 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ ℝ+
→ (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((i · (1 / 𝑅)) · 𝑡)) ∈ ((-𝑅[,]𝑅)–cn→ℂ)) |
191 | 183, 190 | eqeltrd 2838 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ ℝ+
→ (𝑡 ∈ (-𝑅[,]𝑅) ↦ (i · (𝑡 / 𝑅))) ∈ ((-𝑅[,]𝑅)–cn→ℂ)) |
192 | 17, 29 | mulcld 10853 |
. . . . . . . . . . . . . . 15
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (𝑅 · (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈
ℂ) |
193 | 192, 17, 19 | divrec2d 11612 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑅 · (√‘(1 − ((𝑡 / 𝑅)↑2)))) / 𝑅) = ((1 / 𝑅) · (𝑅 · (√‘(1 − ((𝑡 / 𝑅)↑2)))))) |
194 | 29, 17, 19 | divcan3d 11613 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑅 · (√‘(1 − ((𝑡 / 𝑅)↑2)))) / 𝑅) = (√‘(1 − ((𝑡 / 𝑅)↑2)))) |
195 | 104 | adantr 484 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (𝑅↑2) ∈ ℝ) |
196 | 3 | sqge0d 13818 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑅 ∈ ℝ+
→ 0 ≤ (𝑅↑2)) |
197 | 196 | adantr 484 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅[,]𝑅)) → 0 ≤ (𝑅↑2)) |
198 | 195, 197,
87, 136 | sqrtmuld 14988 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (√‘((𝑅↑2) · (1 − ((𝑡 / 𝑅)↑2)))) = ((√‘(𝑅↑2)) ·
(√‘(1 − ((𝑡 / 𝑅)↑2))))) |
199 | 2 | adantr 484 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (𝑅↑2) ∈ ℂ) |
200 | 199, 26, 27 | subdid 11288 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑅↑2) · (1 − ((𝑡 / 𝑅)↑2))) = (((𝑅↑2) · 1) − ((𝑅↑2) · ((𝑡 / 𝑅)↑2)))) |
201 | 199 | mulid1d 10850 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑅↑2) · 1) = (𝑅↑2)) |
202 | 16, 17, 19 | sqdivd 13729 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑡 / 𝑅)↑2) = ((𝑡↑2) / (𝑅↑2))) |
203 | 202 | oveq2d 7229 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑅↑2) · ((𝑡 / 𝑅)↑2)) = ((𝑅↑2) · ((𝑡↑2) / (𝑅↑2)))) |
204 | 16 | sqcld 13714 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (𝑡↑2) ∈ ℂ) |
205 | | sqne0 13695 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑅 ∈ ℂ → ((𝑅↑2) ≠ 0 ↔ 𝑅 ≠ 0)) |
206 | 1, 205 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑅 ∈ ℝ+
→ ((𝑅↑2) ≠ 0
↔ 𝑅 ≠
0)) |
207 | 18, 206 | mpbird 260 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑅 ∈ ℝ+
→ (𝑅↑2) ≠
0) |
208 | 207 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (𝑅↑2) ≠ 0) |
209 | 204, 199,
208 | divcan2d 11610 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑅↑2) · ((𝑡↑2) / (𝑅↑2))) = (𝑡↑2)) |
210 | 203, 209 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑅↑2) · ((𝑡 / 𝑅)↑2)) = (𝑡↑2)) |
211 | 201, 210 | oveq12d 7231 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (((𝑅↑2) · 1) − ((𝑅↑2) · ((𝑡 / 𝑅)↑2))) = ((𝑅↑2) − (𝑡↑2))) |
212 | 200, 211 | eqtrd 2777 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑅↑2) · (1 − ((𝑡 / 𝑅)↑2))) = ((𝑅↑2) − (𝑡↑2))) |
213 | 212 | fveq2d 6721 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (√‘((𝑅↑2) · (1 − ((𝑡 / 𝑅)↑2)))) = (√‘((𝑅↑2) − (𝑡↑2)))) |
214 | 109 | adantr 484 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅[,]𝑅)) → 0 ≤ 𝑅) |
215 | 84, 214 | sqrtsqd 14983 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (√‘(𝑅↑2)) = 𝑅) |
216 | 215 | oveq1d 7228 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅[,]𝑅)) → ((√‘(𝑅↑2)) · (√‘(1 −
((𝑡 / 𝑅)↑2)))) = (𝑅 · (√‘(1 − ((𝑡 / 𝑅)↑2))))) |
217 | 198, 213,
216 | 3eqtr3rd 2786 |
. . . . . . . . . . . . . . 15
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (𝑅 · (√‘(1 − ((𝑡 / 𝑅)↑2)))) = (√‘((𝑅↑2) − (𝑡↑2)))) |
218 | 217 | oveq2d 7229 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅[,]𝑅)) → ((1 / 𝑅) · (𝑅 · (√‘(1 − ((𝑡 / 𝑅)↑2))))) = ((1 / 𝑅) · (√‘((𝑅↑2) − (𝑡↑2))))) |
219 | 193, 194,
218 | 3eqtr3d 2785 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (√‘(1 − ((𝑡 / 𝑅)↑2))) = ((1 / 𝑅) · (√‘((𝑅↑2) − (𝑡↑2))))) |
220 | 219 | mpteq2dva 5150 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ ℝ+
→ (𝑡 ∈ (-𝑅[,]𝑅) ↦ (√‘(1 − ((𝑡 / 𝑅)↑2)))) = (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((1 / 𝑅) · (√‘((𝑅↑2) − (𝑡↑2)))))) |
221 | | cncfmptc 23809 |
. . . . . . . . . . . . . 14
⊢ (((1 /
𝑅) ∈ ℂ ∧
(-𝑅[,]𝑅) ⊆ ℂ ∧ ℂ ⊆
ℂ) → (𝑡 ∈
(-𝑅[,]𝑅) ↦ (1 / 𝑅)) ∈ ((-𝑅[,]𝑅)–cn→ℂ)) |
222 | 179, 8, 10, 221 | syl3anc 1373 |
. . . . . . . . . . . . 13
⊢ (𝑅 ∈ ℝ+
→ (𝑡 ∈ (-𝑅[,]𝑅) ↦ (1 / 𝑅)) ∈ ((-𝑅[,]𝑅)–cn→ℂ)) |
223 | | areacirclem2 35603 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ ℝ ∧ 0 ≤
𝑅) → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (√‘((𝑅↑2) − (𝑡↑2)))) ∈ ((-𝑅[,]𝑅)–cn→ℂ)) |
224 | 3, 109, 223 | syl2anc 587 |
. . . . . . . . . . . . 13
⊢ (𝑅 ∈ ℝ+
→ (𝑡 ∈ (-𝑅[,]𝑅) ↦ (√‘((𝑅↑2) − (𝑡↑2)))) ∈ ((-𝑅[,]𝑅)–cn→ℂ)) |
225 | 222, 224 | mulcncf 24343 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ ℝ+
→ (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((1 / 𝑅) · (√‘((𝑅↑2) − (𝑡↑2))))) ∈ ((-𝑅[,]𝑅)–cn→ℂ)) |
226 | 220, 225 | eqeltrd 2838 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ ℝ+
→ (𝑡 ∈ (-𝑅[,]𝑅) ↦ (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ((-𝑅[,]𝑅)–cn→ℂ)) |
227 | 13, 15, 191, 226 | cncfmpt2f 23812 |
. . . . . . . . . 10
⊢ (𝑅 ∈ ℝ+
→ (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2))))) ∈ ((-𝑅[,]𝑅)–cn→ℂ)) |
228 | | cncffvrn 23795 |
. . . . . . . . . 10
⊢
(((ℂ ∖ (-∞(,]0)) ⊆ ℂ ∧ (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2))))) ∈ ((-𝑅[,]𝑅)–cn→ℂ)) → ((𝑡 ∈ (-𝑅[,]𝑅) ↦ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2))))) ∈ ((-𝑅[,]𝑅)–cn→(ℂ ∖ (-∞(,]0))) ↔ (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2))))):(-𝑅[,]𝑅)⟶(ℂ ∖
(-∞(,]0)))) |
229 | 176, 227,
228 | syl2anc 587 |
. . . . . . . . 9
⊢ (𝑅 ∈ ℝ+
→ ((𝑡 ∈ (-𝑅[,]𝑅) ↦ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2))))) ∈ ((-𝑅[,]𝑅)–cn→(ℂ ∖ (-∞(,]0))) ↔ (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2))))):(-𝑅[,]𝑅)⟶(ℂ ∖
(-∞(,]0)))) |
230 | 175, 229 | mpbird 260 |
. . . . . . . 8
⊢ (𝑅 ∈ ℝ+
→ (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2))))) ∈ ((-𝑅[,]𝑅)–cn→(ℂ ∖
(-∞(,]0)))) |
231 | | eqid 2737 |
. . . . . . . . . 10
⊢
((TopOpen‘ℂfld) ↾t (-𝑅[,]𝑅)) = ((TopOpen‘ℂfld)
↾t (-𝑅[,]𝑅)) |
232 | | eqid 2737 |
. . . . . . . . . 10
⊢
((TopOpen‘ℂfld) ↾t (ℂ
∖ (-∞(,]0))) = ((TopOpen‘ℂfld)
↾t (ℂ ∖ (-∞(,]0))) |
233 | 13, 231, 232 | cncfcn 23807 |
. . . . . . . . 9
⊢ (((-𝑅[,]𝑅) ⊆ ℂ ∧ (ℂ ∖
(-∞(,]0)) ⊆ ℂ) → ((-𝑅[,]𝑅)–cn→(ℂ ∖ (-∞(,]0))) =
(((TopOpen‘ℂfld) ↾t (-𝑅[,]𝑅)) Cn ((TopOpen‘ℂfld)
↾t (ℂ ∖ (-∞(,]0))))) |
234 | 8, 176, 233 | syl2anc 587 |
. . . . . . . 8
⊢ (𝑅 ∈ ℝ+
→ ((-𝑅[,]𝑅)–cn→(ℂ ∖ (-∞(,]0))) =
(((TopOpen‘ℂfld) ↾t (-𝑅[,]𝑅)) Cn ((TopOpen‘ℂfld)
↾t (ℂ ∖ (-∞(,]0))))) |
235 | 230, 234 | eleqtrd 2840 |
. . . . . . 7
⊢ (𝑅 ∈ ℝ+
→ (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2))))) ∈
(((TopOpen‘ℂfld) ↾t (-𝑅[,]𝑅)) Cn ((TopOpen‘ℂfld)
↾t (ℂ ∖ (-∞(,]0))))) |
236 | | eqid 2737 |
. . . . . . . . . 10
⊢ (ℂ
∖ (-∞(,]0)) = (ℂ ∖ (-∞(,]0)) |
237 | 236 | logcn 25535 |
. . . . . . . . 9
⊢ (log
↾ (ℂ ∖ (-∞(,]0))) ∈ ((ℂ ∖
(-∞(,]0))–cn→ℂ) |
238 | | difss 4046 |
. . . . . . . . . 10
⊢ (ℂ
∖ (-∞(,]0)) ⊆ ℂ |
239 | | eqid 2737 |
. . . . . . . . . . 11
⊢
((TopOpen‘ℂfld) ↾t ℂ) =
((TopOpen‘ℂfld) ↾t
ℂ) |
240 | 13, 232, 239 | cncfcn 23807 |
. . . . . . . . . 10
⊢
(((ℂ ∖ (-∞(,]0)) ⊆ ℂ ∧ ℂ ⊆
ℂ) → ((ℂ ∖ (-∞(,]0))–cn→ℂ) =
(((TopOpen‘ℂfld) ↾t (ℂ ∖
(-∞(,]0))) Cn ((TopOpen‘ℂfld) ↾t
ℂ))) |
241 | 238, 9, 240 | mp2an 692 |
. . . . . . . . 9
⊢ ((ℂ
∖ (-∞(,]0))–cn→ℂ) =
(((TopOpen‘ℂfld) ↾t (ℂ ∖
(-∞(,]0))) Cn ((TopOpen‘ℂfld) ↾t
ℂ)) |
242 | 237, 241 | eleqtri 2836 |
. . . . . . . 8
⊢ (log
↾ (ℂ ∖ (-∞(,]0))) ∈
(((TopOpen‘ℂfld) ↾t (ℂ ∖
(-∞(,]0))) Cn ((TopOpen‘ℂfld) ↾t
ℂ)) |
243 | 242 | a1i 11 |
. . . . . . 7
⊢ (𝑅 ∈ ℝ+
→ (log ↾ (ℂ ∖ (-∞(,]0))) ∈
(((TopOpen‘ℂfld) ↾t (ℂ ∖
(-∞(,]0))) Cn ((TopOpen‘ℂfld) ↾t
ℂ))) |
244 | 174, 235,
243 | cnmpt11f 22561 |
. . . . . 6
⊢ (𝑅 ∈ ℝ+
→ (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((log ↾ (ℂ ∖
(-∞(,]0)))‘((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))))) ∈
(((TopOpen‘ℂfld) ↾t (-𝑅[,]𝑅)) Cn ((TopOpen‘ℂfld)
↾t ℂ))) |
245 | 13, 231, 239 | cncfcn 23807 |
. . . . . . 7
⊢ (((-𝑅[,]𝑅) ⊆ ℂ ∧ ℂ ⊆
ℂ) → ((-𝑅[,]𝑅)–cn→ℂ) =
(((TopOpen‘ℂfld) ↾t (-𝑅[,]𝑅)) Cn ((TopOpen‘ℂfld)
↾t ℂ))) |
246 | 8, 10, 245 | syl2anc 587 |
. . . . . 6
⊢ (𝑅 ∈ ℝ+
→ ((-𝑅[,]𝑅)–cn→ℂ) =
(((TopOpen‘ℂfld) ↾t (-𝑅[,]𝑅)) Cn ((TopOpen‘ℂfld)
↾t ℂ))) |
247 | 244, 246 | eleqtrrd 2841 |
. . . . 5
⊢ (𝑅 ∈ ℝ+
→ (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((log ↾ (ℂ ∖
(-∞(,]0)))‘((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))))) ∈ ((-𝑅[,]𝑅)–cn→ℂ)) |
248 | 170, 247 | mulcncf 24343 |
. . . 4
⊢ (𝑅 ∈ ℝ+
→ (𝑡 ∈ (-𝑅[,]𝑅) ↦ (-i · ((log ↾
(ℂ ∖ (-∞(,]0)))‘((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2))))))) ∈ ((-𝑅[,]𝑅)–cn→ℂ)) |
249 | 166, 248 | eqeltrd 2838 |
. . 3
⊢ (𝑅 ∈ ℝ+
→ (𝑡 ∈ (-𝑅[,]𝑅) ↦ (arcsin‘(𝑡 / 𝑅))) ∈ ((-𝑅[,]𝑅)–cn→ℂ)) |
250 | 219 | oveq2d 7229 |
. . . . . 6
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑡 / 𝑅) · (√‘(1 − ((𝑡 / 𝑅)↑2)))) = ((𝑡 / 𝑅) · ((1 / 𝑅) · (√‘((𝑅↑2) − (𝑡↑2)))))) |
251 | 199, 204 | subcld 11189 |
. . . . . . . 8
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑅↑2) − (𝑡↑2)) ∈ ℂ) |
252 | 251 | sqrtcld 15001 |
. . . . . . 7
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (√‘((𝑅↑2) − (𝑡↑2))) ∈ ℂ) |
253 | 20, 180, 252 | mulassd 10856 |
. . . . . 6
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (((𝑡 / 𝑅) · (1 / 𝑅)) · (√‘((𝑅↑2) − (𝑡↑2)))) = ((𝑡 / 𝑅) · ((1 / 𝑅) · (√‘((𝑅↑2) − (𝑡↑2)))))) |
254 | 16, 17, 19 | divrecd 11611 |
. . . . . . . . 9
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (𝑡 / 𝑅) = (𝑡 · (1 / 𝑅))) |
255 | 254 | oveq1d 7228 |
. . . . . . . 8
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑡 / 𝑅) · (1 / 𝑅)) = ((𝑡 · (1 / 𝑅)) · (1 / 𝑅))) |
256 | 16, 180, 180 | mulassd 10856 |
. . . . . . . 8
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑡 · (1 / 𝑅)) · (1 / 𝑅)) = (𝑡 · ((1 / 𝑅) · (1 / 𝑅)))) |
257 | 255, 256 | eqtrd 2777 |
. . . . . . 7
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑡 / 𝑅) · (1 / 𝑅)) = (𝑡 · ((1 / 𝑅) · (1 / 𝑅)))) |
258 | 257 | oveq1d 7228 |
. . . . . 6
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅[,]𝑅)) → (((𝑡 / 𝑅) · (1 / 𝑅)) · (√‘((𝑅↑2) − (𝑡↑2)))) = ((𝑡 · ((1 / 𝑅) · (1 / 𝑅))) ·
(√‘((𝑅↑2)
− (𝑡↑2))))) |
259 | 250, 253,
258 | 3eqtr2d 2783 |
. . . . 5
⊢ ((𝑅 ∈ ℝ+
∧ 𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑡 / 𝑅) · (√‘(1 − ((𝑡 / 𝑅)↑2)))) = ((𝑡 · ((1 / 𝑅) · (1 / 𝑅))) · (√‘((𝑅↑2) − (𝑡↑2))))) |
260 | 259 | mpteq2dva 5150 |
. . . 4
⊢ (𝑅 ∈ ℝ+
→ (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((𝑡 / 𝑅) · (√‘(1 − ((𝑡 / 𝑅)↑2))))) = (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((𝑡 · ((1 / 𝑅) · (1 / 𝑅))) · (√‘((𝑅↑2) − (𝑡↑2)))))) |
261 | 179, 179 | mulcld 10853 |
. . . . . . 7
⊢ (𝑅 ∈ ℝ+
→ ((1 / 𝑅) · (1
/ 𝑅)) ∈
ℂ) |
262 | | cncfmptc 23809 |
. . . . . . 7
⊢ ((((1 /
𝑅) · (1 / 𝑅)) ∈ ℂ ∧ (-𝑅[,]𝑅) ⊆ ℂ ∧ ℂ ⊆
ℂ) → (𝑡 ∈
(-𝑅[,]𝑅) ↦ ((1 / 𝑅) · (1 / 𝑅))) ∈ ((-𝑅[,]𝑅)–cn→ℂ)) |
263 | 261, 8, 10, 262 | syl3anc 1373 |
. . . . . 6
⊢ (𝑅 ∈ ℝ+
→ (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((1 / 𝑅) · (1 / 𝑅))) ∈ ((-𝑅[,]𝑅)–cn→ℂ)) |
264 | 189, 263 | mulcncf 24343 |
. . . . 5
⊢ (𝑅 ∈ ℝ+
→ (𝑡 ∈ (-𝑅[,]𝑅) ↦ (𝑡 · ((1 / 𝑅) · (1 / 𝑅)))) ∈ ((-𝑅[,]𝑅)–cn→ℂ)) |
265 | 264, 224 | mulcncf 24343 |
. . . 4
⊢ (𝑅 ∈ ℝ+
→ (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((𝑡 · ((1 / 𝑅) · (1 / 𝑅))) · (√‘((𝑅↑2) − (𝑡↑2))))) ∈ ((-𝑅[,]𝑅)–cn→ℂ)) |
266 | 260, 265 | eqeltrd 2838 |
. . 3
⊢ (𝑅 ∈ ℝ+
→ (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((𝑡 / 𝑅) · (√‘(1 − ((𝑡 / 𝑅)↑2))))) ∈ ((-𝑅[,]𝑅)–cn→ℂ)) |
267 | 13, 15, 249, 266 | cncfmpt2f 23812 |
. 2
⊢ (𝑅 ∈ ℝ+
→ (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((arcsin‘(𝑡 / 𝑅)) + ((𝑡 / 𝑅) · (√‘(1 − ((𝑡 / 𝑅)↑2)))))) ∈ ((-𝑅[,]𝑅)–cn→ℂ)) |
268 | 12, 267 | mulcncf 24343 |
1
⊢ (𝑅 ∈ ℝ+
→ (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑡 / 𝑅)) + ((𝑡 / 𝑅) · (√‘(1 − ((𝑡 / 𝑅)↑2))))))) ∈ ((-𝑅[,]𝑅)–cn→ℂ)) |