Users' Mathboxes Mathbox for Brendan Leahy < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  dvasin Structured version   Visualization version   GIF version

Theorem dvasin 33977
Description: Derivative of arcsine. (Contributed by Brendan Leahy, 18-Dec-2018.)
Hypothesis
Ref Expression
dvasin.d 𝐷 = (ℂ ∖ ((-∞(,]-1) ∪ (1[,)+∞)))
Assertion
Ref Expression
dvasin (ℂ D (arcsin ↾ 𝐷)) = (𝑥𝐷 ↦ (1 / (√‘(1 − (𝑥↑2)))))
Distinct variable group:   𝑥,𝐷

Proof of Theorem dvasin
Dummy variables 𝑦 𝑧 𝑤 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-asin 24941 . . . . 5 arcsin = (𝑥 ∈ ℂ ↦ (-i · (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2)))))))
21reseq1i 5595 . . . 4 (arcsin ↾ 𝐷) = ((𝑥 ∈ ℂ ↦ (-i · (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))))) ↾ 𝐷)
3 dvasin.d . . . . . 6 𝐷 = (ℂ ∖ ((-∞(,]-1) ∪ (1[,)+∞)))
4 difss 3934 . . . . . 6 (ℂ ∖ ((-∞(,]-1) ∪ (1[,)+∞))) ⊆ ℂ
53, 4eqsstri 3830 . . . . 5 𝐷 ⊆ ℂ
6 resmpt 5660 . . . . 5 (𝐷 ⊆ ℂ → ((𝑥 ∈ ℂ ↦ (-i · (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))))) ↾ 𝐷) = (𝑥𝐷 ↦ (-i · (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))))))
75, 6ax-mp 5 . . . 4 ((𝑥 ∈ ℂ ↦ (-i · (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))))) ↾ 𝐷) = (𝑥𝐷 ↦ (-i · (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2)))))))
82, 7eqtri 2820 . . 3 (arcsin ↾ 𝐷) = (𝑥𝐷 ↦ (-i · (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2)))))))
98oveq2i 6888 . 2 (ℂ D (arcsin ↾ 𝐷)) = (ℂ D (𝑥𝐷 ↦ (-i · (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))))))
10 cnelprrecn 10316 . . . . 5 ℂ ∈ {ℝ, ℂ}
1110a1i 11 . . . 4 (⊤ → ℂ ∈ {ℝ, ℂ})
125sseli 3793 . . . . . . 7 (𝑥𝐷𝑥 ∈ ℂ)
13 ax-icn 10282 . . . . . . . . 9 i ∈ ℂ
14 mulcl 10307 . . . . . . . . 9 ((i ∈ ℂ ∧ 𝑥 ∈ ℂ) → (i · 𝑥) ∈ ℂ)
1513, 14mpan 682 . . . . . . . 8 (𝑥 ∈ ℂ → (i · 𝑥) ∈ ℂ)
16 ax-1cn 10281 . . . . . . . . . 10 1 ∈ ℂ
17 sqcl 13176 . . . . . . . . . 10 (𝑥 ∈ ℂ → (𝑥↑2) ∈ ℂ)
18 subcl 10570 . . . . . . . . . 10 ((1 ∈ ℂ ∧ (𝑥↑2) ∈ ℂ) → (1 − (𝑥↑2)) ∈ ℂ)
1916, 17, 18sylancr 582 . . . . . . . . 9 (𝑥 ∈ ℂ → (1 − (𝑥↑2)) ∈ ℂ)
2019sqrtcld 14514 . . . . . . . 8 (𝑥 ∈ ℂ → (√‘(1 − (𝑥↑2))) ∈ ℂ)
2115, 20addcld 10347 . . . . . . 7 (𝑥 ∈ ℂ → ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℂ)
2212, 21syl 17 . . . . . 6 (𝑥𝐷 → ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℂ)
23 asinlem 24944 . . . . . . 7 (𝑥 ∈ ℂ → ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≠ 0)
2412, 23syl 17 . . . . . 6 (𝑥𝐷 → ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≠ 0)
2522, 24logcld 24655 . . . . 5 (𝑥𝐷 → (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))) ∈ ℂ)
2625adantl 474 . . . 4 ((⊤ ∧ 𝑥𝐷) → (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))) ∈ ℂ)
27 ovexd 6911 . . . 4 ((⊤ ∧ 𝑥𝐷) → (i / (√‘(1 − (𝑥↑2)))) ∈ V)
28 simpr 478 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ ℂ ∧ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ) → ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ)
29 asinlem3 24947 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ℂ → 0 ≤ (ℜ‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))))
30 rere 14200 . . . . . . . . . . . . . . . . . . 19 (((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ → (ℜ‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))) = ((i · 𝑥) + (√‘(1 − (𝑥↑2)))))
3130breq2d 4854 . . . . . . . . . . . . . . . . . 18 (((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ → (0 ≤ (ℜ‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))) ↔ 0 ≤ ((i · 𝑥) + (√‘(1 − (𝑥↑2))))))
3231biimpac 471 . . . . . . . . . . . . . . . . 17 ((0 ≤ (ℜ‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))) ∧ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ) → 0 ≤ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))))
3329, 32sylan 576 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ ℂ ∧ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ) → 0 ≤ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))))
3423adantr 473 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ ℂ ∧ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ) → ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≠ 0)
3528, 33, 34ne0gt0d 10463 . . . . . . . . . . . . . . 15 ((𝑥 ∈ ℂ ∧ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ) → 0 < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))))
36 0re 10329 . . . . . . . . . . . . . . . . 17 0 ∈ ℝ
37 ltnle 10406 . . . . . . . . . . . . . . . . 17 ((0 ∈ ℝ ∧ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ) → (0 < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ↔ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0))
3836, 37mpan 682 . . . . . . . . . . . . . . . 16 (((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ → (0 < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ↔ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0))
3938adantl 474 . . . . . . . . . . . . . . 15 ((𝑥 ∈ ℂ ∧ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ) → (0 < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ↔ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0))
4035, 39mpbid 224 . . . . . . . . . . . . . 14 ((𝑥 ∈ ℂ ∧ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ) → ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0)
4140ex 402 . . . . . . . . . . . . 13 (𝑥 ∈ ℂ → (((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ → ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0))
4212, 41syl 17 . . . . . . . . . . . 12 (𝑥𝐷 → (((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ → ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0))
43 imor 880 . . . . . . . . . . . 12 ((((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ → ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0) ↔ (¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ ∨ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0))
4442, 43sylib 210 . . . . . . . . . . 11 (𝑥𝐷 → (¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ ∨ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0))
4544orcomd 898 . . . . . . . . . 10 (𝑥𝐷 → (¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0 ∨ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ))
4645olcd 901 . . . . . . . . 9 (𝑥𝐷 → (¬ -∞ < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∨ (¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0 ∨ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ)))
47 3ianor 1133 . . . . . . . . . . 11 (¬ (((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ ∧ -∞ < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∧ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0) ↔ (¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ ∨ ¬ -∞ < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∨ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0))
48 3orrot 1113 . . . . . . . . . . 11 ((¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ ∨ ¬ -∞ < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∨ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0) ↔ (¬ -∞ < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∨ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0 ∨ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ))
49 3orass 1111 . . . . . . . . . . 11 ((¬ -∞ < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∨ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0 ∨ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ) ↔ (¬ -∞ < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∨ (¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0 ∨ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ)))
5047, 48, 493bitrri 290 . . . . . . . . . 10 ((¬ -∞ < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∨ (¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0 ∨ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ)) ↔ ¬ (((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ ∧ -∞ < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∧ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0))
51 mnfxr 10385 . . . . . . . . . . 11 -∞ ∈ ℝ*
52 elioc2 12482 . . . . . . . . . . 11 ((-∞ ∈ ℝ* ∧ 0 ∈ ℝ) → (((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ (-∞(,]0) ↔ (((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ ∧ -∞ < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∧ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0)))
5351, 36, 52mp2an 684 . . . . . . . . . 10 (((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ (-∞(,]0) ↔ (((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ ∧ -∞ < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∧ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0))
5450, 53xchbinxr 327 . . . . . . . . 9 ((¬ -∞ < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∨ (¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0 ∨ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ)) ↔ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ (-∞(,]0))
5546, 54sylib 210 . . . . . . . 8 (𝑥𝐷 → ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ (-∞(,]0))
5622, 55eldifd 3779 . . . . . . 7 (𝑥𝐷 → ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ (ℂ ∖ (-∞(,]0)))
5756adantl 474 . . . . . 6 ((⊤ ∧ 𝑥𝐷) → ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ (ℂ ∖ (-∞(,]0)))
58 ovexd 6911 . . . . . 6 ((⊤ ∧ 𝑥𝐷) → ((i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) / (√‘(1 − (𝑥↑2)))) ∈ V)
59 eldifi 3929 . . . . . . . 8 (𝑦 ∈ (ℂ ∖ (-∞(,]0)) → 𝑦 ∈ ℂ)
60 eldifn 3930 . . . . . . . . 9 (𝑦 ∈ (ℂ ∖ (-∞(,]0)) → ¬ 𝑦 ∈ (-∞(,]0))
61 0xr 10374 . . . . . . . . . . . 12 0 ∈ ℝ*
62 mnflt0 12203 . . . . . . . . . . . 12 -∞ < 0
63 ubioc1 12473 . . . . . . . . . . . 12 ((-∞ ∈ ℝ* ∧ 0 ∈ ℝ* ∧ -∞ < 0) → 0 ∈ (-∞(,]0))
6451, 61, 62, 63mp3an 1586 . . . . . . . . . . 11 0 ∈ (-∞(,]0)
65 eleq1 2865 . . . . . . . . . . 11 (𝑦 = 0 → (𝑦 ∈ (-∞(,]0) ↔ 0 ∈ (-∞(,]0)))
6664, 65mpbiri 250 . . . . . . . . . 10 (𝑦 = 0 → 𝑦 ∈ (-∞(,]0))
6766necon3bi 2996 . . . . . . . . 9 𝑦 ∈ (-∞(,]0) → 𝑦 ≠ 0)
6860, 67syl 17 . . . . . . . 8 (𝑦 ∈ (ℂ ∖ (-∞(,]0)) → 𝑦 ≠ 0)
6959, 68logcld 24655 . . . . . . 7 (𝑦 ∈ (ℂ ∖ (-∞(,]0)) → (log‘𝑦) ∈ ℂ)
7069adantl 474 . . . . . 6 ((⊤ ∧ 𝑦 ∈ (ℂ ∖ (-∞(,]0))) → (log‘𝑦) ∈ ℂ)
71 ovexd 6911 . . . . . 6 ((⊤ ∧ 𝑦 ∈ (ℂ ∖ (-∞(,]0))) → (1 / 𝑦) ∈ V)
7213a1i 11 . . . . . . . . . 10 (𝑥𝐷 → i ∈ ℂ)
7372, 12mulcld 10348 . . . . . . . . 9 (𝑥𝐷 → (i · 𝑥) ∈ ℂ)
7473adantl 474 . . . . . . . 8 ((⊤ ∧ 𝑥𝐷) → (i · 𝑥) ∈ ℂ)
7513a1i 11 . . . . . . . 8 ((⊤ ∧ 𝑥𝐷) → i ∈ ℂ)
7612adantl 474 . . . . . . . . . 10 ((⊤ ∧ 𝑥𝐷) → 𝑥 ∈ ℂ)
77 1cnd 10322 . . . . . . . . . 10 ((⊤ ∧ 𝑥𝐷) → 1 ∈ ℂ)
78 simpr 478 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ ℂ) → 𝑥 ∈ ℂ)
79 1cnd 10322 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ ℂ) → 1 ∈ ℂ)
8011dvmptid 24058 . . . . . . . . . . 11 (⊤ → (ℂ D (𝑥 ∈ ℂ ↦ 𝑥)) = (𝑥 ∈ ℂ ↦ 1))
815a1i 11 . . . . . . . . . . 11 (⊤ → 𝐷 ⊆ ℂ)
82 eqid 2798 . . . . . . . . . . . . 13 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
8382cnfldtopon 22911 . . . . . . . . . . . 12 (TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
8483toponrestid 21051 . . . . . . . . . . 11 (TopOpen‘ℂfld) = ((TopOpen‘ℂfld) ↾t ℂ)
8582recld2 22942 . . . . . . . . . . . . . . 15 ℝ ∈ (Clsd‘(TopOpen‘ℂfld))
86 neg1rr 11432 . . . . . . . . . . . . . . . . . 18 -1 ∈ ℝ
87 iocmnfcld 22897 . . . . . . . . . . . . . . . . . 18 (-1 ∈ ℝ → (-∞(,]-1) ∈ (Clsd‘(topGen‘ran (,))))
8886, 87ax-mp 5 . . . . . . . . . . . . . . . . 17 (-∞(,]-1) ∈ (Clsd‘(topGen‘ran (,)))
89 1re 10327 . . . . . . . . . . . . . . . . . 18 1 ∈ ℝ
90 icopnfcld 22896 . . . . . . . . . . . . . . . . . 18 (1 ∈ ℝ → (1[,)+∞) ∈ (Clsd‘(topGen‘ran (,))))
9189, 90ax-mp 5 . . . . . . . . . . . . . . . . 17 (1[,)+∞) ∈ (Clsd‘(topGen‘ran (,)))
92 uncld 21171 . . . . . . . . . . . . . . . . 17 (((-∞(,]-1) ∈ (Clsd‘(topGen‘ran (,))) ∧ (1[,)+∞) ∈ (Clsd‘(topGen‘ran (,)))) → ((-∞(,]-1) ∪ (1[,)+∞)) ∈ (Clsd‘(topGen‘ran (,))))
9388, 91, 92mp2an 684 . . . . . . . . . . . . . . . 16 ((-∞(,]-1) ∪ (1[,)+∞)) ∈ (Clsd‘(topGen‘ran (,)))
9482tgioo2 22931 . . . . . . . . . . . . . . . . 17 (topGen‘ran (,)) = ((TopOpen‘ℂfld) ↾t ℝ)
9594fveq2i 6413 . . . . . . . . . . . . . . . 16 (Clsd‘(topGen‘ran (,))) = (Clsd‘((TopOpen‘ℂfld) ↾t ℝ))
9693, 95eleqtri 2875 . . . . . . . . . . . . . . 15 ((-∞(,]-1) ∪ (1[,)+∞)) ∈ (Clsd‘((TopOpen‘ℂfld) ↾t ℝ))
97 restcldr 21304 . . . . . . . . . . . . . . 15 ((ℝ ∈ (Clsd‘(TopOpen‘ℂfld)) ∧ ((-∞(,]-1) ∪ (1[,)+∞)) ∈ (Clsd‘((TopOpen‘ℂfld) ↾t ℝ))) → ((-∞(,]-1) ∪ (1[,)+∞)) ∈ (Clsd‘(TopOpen‘ℂfld)))
9885, 96, 97mp2an 684 . . . . . . . . . . . . . 14 ((-∞(,]-1) ∪ (1[,)+∞)) ∈ (Clsd‘(TopOpen‘ℂfld))
9983toponunii 21046 . . . . . . . . . . . . . . 15 ℂ = (TopOpen‘ℂfld)
10099cldopn 21161 . . . . . . . . . . . . . 14 (((-∞(,]-1) ∪ (1[,)+∞)) ∈ (Clsd‘(TopOpen‘ℂfld)) → (ℂ ∖ ((-∞(,]-1) ∪ (1[,)+∞))) ∈ (TopOpen‘ℂfld))
10198, 100ax-mp 5 . . . . . . . . . . . . 13 (ℂ ∖ ((-∞(,]-1) ∪ (1[,)+∞))) ∈ (TopOpen‘ℂfld)
1023, 101eqeltri 2873 . . . . . . . . . . . 12 𝐷 ∈ (TopOpen‘ℂfld)
103102a1i 11 . . . . . . . . . . 11 (⊤ → 𝐷 ∈ (TopOpen‘ℂfld))
10411, 78, 79, 80, 81, 84, 82, 103dvmptres 24064 . . . . . . . . . 10 (⊤ → (ℂ D (𝑥𝐷𝑥)) = (𝑥𝐷 ↦ 1))
10513a1i 11 . . . . . . . . . 10 (⊤ → i ∈ ℂ)
10611, 76, 77, 104, 105dvmptcmul 24065 . . . . . . . . 9 (⊤ → (ℂ D (𝑥𝐷 ↦ (i · 𝑥))) = (𝑥𝐷 ↦ (i · 1)))
10713mulid1i 10332 . . . . . . . . . 10 (i · 1) = i
108107mpteq2i 4933 . . . . . . . . 9 (𝑥𝐷 ↦ (i · 1)) = (𝑥𝐷 ↦ i)
109106, 108syl6eq 2848 . . . . . . . 8 (⊤ → (ℂ D (𝑥𝐷 ↦ (i · 𝑥))) = (𝑥𝐷 ↦ i))
11012sqcld 13257 . . . . . . . . . . 11 (𝑥𝐷 → (𝑥↑2) ∈ ℂ)
11116, 110, 18sylancr 582 . . . . . . . . . 10 (𝑥𝐷 → (1 − (𝑥↑2)) ∈ ℂ)
112111sqrtcld 14514 . . . . . . . . 9 (𝑥𝐷 → (√‘(1 − (𝑥↑2))) ∈ ℂ)
113112adantl 474 . . . . . . . 8 ((⊤ ∧ 𝑥𝐷) → (√‘(1 − (𝑥↑2))) ∈ ℂ)
114 ovexd 6911 . . . . . . . 8 ((⊤ ∧ 𝑥𝐷) → (-𝑥 / (√‘(1 − (𝑥↑2)))) ∈ V)
115 elin 3993 . . . . . . . . . . . . . . 15 (𝑥 ∈ (𝐷 ∩ ℝ) ↔ (𝑥𝐷𝑥 ∈ ℝ))
1163asindmre 33976 . . . . . . . . . . . . . . . . 17 (𝐷 ∩ ℝ) = (-1(,)1)
117116eqimssi 3854 . . . . . . . . . . . . . . . 16 (𝐷 ∩ ℝ) ⊆ (-1(,)1)
118117sseli 3793 . . . . . . . . . . . . . . 15 (𝑥 ∈ (𝐷 ∩ ℝ) → 𝑥 ∈ (-1(,)1))
119115, 118sylbir 227 . . . . . . . . . . . . . 14 ((𝑥𝐷𝑥 ∈ ℝ) → 𝑥 ∈ (-1(,)1))
120 incom 4002 . . . . . . . . . . . . . . . 16 ((0(,)+∞) ∩ (-∞(,]0)) = ((-∞(,]0) ∩ (0(,)+∞))
121 pnfxr 10381 . . . . . . . . . . . . . . . . 17 +∞ ∈ ℝ*
122 df-ioc 12426 . . . . . . . . . . . . . . . . . 18 (,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧𝑧𝑦)})
123 df-ioo 12425 . . . . . . . . . . . . . . . . . 18 (,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧𝑧 < 𝑦)})
124 xrltnle 10394 . . . . . . . . . . . . . . . . . 18 ((0 ∈ ℝ*𝑤 ∈ ℝ*) → (0 < 𝑤 ↔ ¬ 𝑤 ≤ 0))
125122, 123, 124ixxdisj 12436 . . . . . . . . . . . . . . . . 17 ((-∞ ∈ ℝ* ∧ 0 ∈ ℝ* ∧ +∞ ∈ ℝ*) → ((-∞(,]0) ∩ (0(,)+∞)) = ∅)
12651, 61, 121, 125mp3an 1586 . . . . . . . . . . . . . . . 16 ((-∞(,]0) ∩ (0(,)+∞)) = ∅
127120, 126eqtri 2820 . . . . . . . . . . . . . . 15 ((0(,)+∞) ∩ (-∞(,]0)) = ∅
128 elioore 12451 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ (-1(,)1) → 𝑥 ∈ ℝ)
129128resqcld 13288 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (-1(,)1) → (𝑥↑2) ∈ ℝ)
130 resubcl 10636 . . . . . . . . . . . . . . . . . 18 ((1 ∈ ℝ ∧ (𝑥↑2) ∈ ℝ) → (1 − (𝑥↑2)) ∈ ℝ)
13189, 129, 130sylancr 582 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (-1(,)1) → (1 − (𝑥↑2)) ∈ ℝ)
13286rexri 10386 . . . . . . . . . . . . . . . . . . 19 -1 ∈ ℝ*
13389rexri 10386 . . . . . . . . . . . . . . . . . . 19 1 ∈ ℝ*
134 elioo2 12462 . . . . . . . . . . . . . . . . . . 19 ((-1 ∈ ℝ* ∧ 1 ∈ ℝ*) → (𝑥 ∈ (-1(,)1) ↔ (𝑥 ∈ ℝ ∧ -1 < 𝑥𝑥 < 1)))
135132, 133, 134mp2an 684 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (-1(,)1) ↔ (𝑥 ∈ ℝ ∧ -1 < 𝑥𝑥 < 1))
136 recn 10313 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 ∈ ℝ → 𝑥 ∈ ℂ)
137136abscld 14513 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ ℝ → (abs‘𝑥) ∈ ℝ)
138136absge0d 14521 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ ℝ → 0 ≤ (abs‘𝑥))
139 0le1 10842 . . . . . . . . . . . . . . . . . . . . . . 23 0 ≤ 1
140 lt2sq 13188 . . . . . . . . . . . . . . . . . . . . . . 23 ((((abs‘𝑥) ∈ ℝ ∧ 0 ≤ (abs‘𝑥)) ∧ (1 ∈ ℝ ∧ 0 ≤ 1)) → ((abs‘𝑥) < 1 ↔ ((abs‘𝑥)↑2) < (1↑2)))
14189, 139, 140mpanr12 697 . . . . . . . . . . . . . . . . . . . . . 22 (((abs‘𝑥) ∈ ℝ ∧ 0 ≤ (abs‘𝑥)) → ((abs‘𝑥) < 1 ↔ ((abs‘𝑥)↑2) < (1↑2)))
142137, 138, 141syl2anc 580 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ ℝ → ((abs‘𝑥) < 1 ↔ ((abs‘𝑥)↑2) < (1↑2)))
143 abslt 14392 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑥 ∈ ℝ ∧ 1 ∈ ℝ) → ((abs‘𝑥) < 1 ↔ (-1 < 𝑥𝑥 < 1)))
14489, 143mpan2 683 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ ℝ → ((abs‘𝑥) < 1 ↔ (-1 < 𝑥𝑥 < 1)))
145 absresq 14380 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 ∈ ℝ → ((abs‘𝑥)↑2) = (𝑥↑2))
146 sq1 13209 . . . . . . . . . . . . . . . . . . . . . . . 24 (1↑2) = 1
147146a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 ∈ ℝ → (1↑2) = 1)
148145, 147breq12d 4855 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ ℝ → (((abs‘𝑥)↑2) < (1↑2) ↔ (𝑥↑2) < 1))
149 resqcl 13182 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 ∈ ℝ → (𝑥↑2) ∈ ℝ)
150 posdif 10812 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑥↑2) ∈ ℝ ∧ 1 ∈ ℝ) → ((𝑥↑2) < 1 ↔ 0 < (1 − (𝑥↑2))))
151149, 89, 150sylancl 581 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ ℝ → ((𝑥↑2) < 1 ↔ 0 < (1 − (𝑥↑2))))
152148, 151bitrd 271 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ ℝ → (((abs‘𝑥)↑2) < (1↑2) ↔ 0 < (1 − (𝑥↑2))))
153142, 144, 1523bitr3d 301 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ ℝ → ((-1 < 𝑥𝑥 < 1) ↔ 0 < (1 − (𝑥↑2))))
154153biimpd 221 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ℝ → ((-1 < 𝑥𝑥 < 1) → 0 < (1 − (𝑥↑2))))
1551543impib 1145 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ ℝ ∧ -1 < 𝑥𝑥 < 1) → 0 < (1 − (𝑥↑2)))
156135, 155sylbi 209 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (-1(,)1) → 0 < (1 − (𝑥↑2)))
157131, 156elrpd 12111 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (-1(,)1) → (1 − (𝑥↑2)) ∈ ℝ+)
158 ioorp 12497 . . . . . . . . . . . . . . . 16 (0(,)+∞) = ℝ+
159157, 158syl6eleqr 2888 . . . . . . . . . . . . . . 15 (𝑥 ∈ (-1(,)1) → (1 − (𝑥↑2)) ∈ (0(,)+∞))
160 disjel 4218 . . . . . . . . . . . . . . 15 ((((0(,)+∞) ∩ (-∞(,]0)) = ∅ ∧ (1 − (𝑥↑2)) ∈ (0(,)+∞)) → ¬ (1 − (𝑥↑2)) ∈ (-∞(,]0))
161127, 159, 160sylancr 582 . . . . . . . . . . . . . 14 (𝑥 ∈ (-1(,)1) → ¬ (1 − (𝑥↑2)) ∈ (-∞(,]0))
162119, 161syl 17 . . . . . . . . . . . . 13 ((𝑥𝐷𝑥 ∈ ℝ) → ¬ (1 − (𝑥↑2)) ∈ (-∞(,]0))
163 elioc2 12482 . . . . . . . . . . . . . . . . . . . . . . . 24 ((-∞ ∈ ℝ* ∧ 0 ∈ ℝ) → ((1 − (𝑥↑2)) ∈ (-∞(,]0) ↔ ((1 − (𝑥↑2)) ∈ ℝ ∧ -∞ < (1 − (𝑥↑2)) ∧ (1 − (𝑥↑2)) ≤ 0)))
16451, 36, 163mp2an 684 . . . . . . . . . . . . . . . . . . . . . . 23 ((1 − (𝑥↑2)) ∈ (-∞(,]0) ↔ ((1 − (𝑥↑2)) ∈ ℝ ∧ -∞ < (1 − (𝑥↑2)) ∧ (1 − (𝑥↑2)) ≤ 0))
165164biimpi 208 . . . . . . . . . . . . . . . . . . . . . 22 ((1 − (𝑥↑2)) ∈ (-∞(,]0) → ((1 − (𝑥↑2)) ∈ ℝ ∧ -∞ < (1 − (𝑥↑2)) ∧ (1 − (𝑥↑2)) ≤ 0))
166165simp1d 1173 . . . . . . . . . . . . . . . . . . . . 21 ((1 − (𝑥↑2)) ∈ (-∞(,]0) → (1 − (𝑥↑2)) ∈ ℝ)
167 resubcl 10636 . . . . . . . . . . . . . . . . . . . . 21 ((1 ∈ ℝ ∧ (1 − (𝑥↑2)) ∈ ℝ) → (1 − (1 − (𝑥↑2))) ∈ ℝ)
16889, 166, 167sylancr 582 . . . . . . . . . . . . . . . . . . . 20 ((1 − (𝑥↑2)) ∈ (-∞(,]0) → (1 − (1 − (𝑥↑2))) ∈ ℝ)
169 nncan 10601 . . . . . . . . . . . . . . . . . . . . . . 23 ((1 ∈ ℂ ∧ (𝑥↑2) ∈ ℂ) → (1 − (1 − (𝑥↑2))) = (𝑥↑2))
17016, 169mpan 682 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑥↑2) ∈ ℂ → (1 − (1 − (𝑥↑2))) = (𝑥↑2))
171170eleq1d 2862 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥↑2) ∈ ℂ → ((1 − (1 − (𝑥↑2))) ∈ ℝ ↔ (𝑥↑2) ∈ ℝ))
172171biimpa 469 . . . . . . . . . . . . . . . . . . . 20 (((𝑥↑2) ∈ ℂ ∧ (1 − (1 − (𝑥↑2))) ∈ ℝ) → (𝑥↑2) ∈ ℝ)
173168, 172sylan2 587 . . . . . . . . . . . . . . . . . . 19 (((𝑥↑2) ∈ ℂ ∧ (1 − (𝑥↑2)) ∈ (-∞(,]0)) → (𝑥↑2) ∈ ℝ)
174166adantl 474 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑥↑2) ∈ ℂ ∧ (1 − (𝑥↑2)) ∈ (-∞(,]0)) → (1 − (𝑥↑2)) ∈ ℝ)
175165simp3d 1175 . . . . . . . . . . . . . . . . . . . . . . 23 ((1 − (𝑥↑2)) ∈ (-∞(,]0) → (1 − (𝑥↑2)) ≤ 0)
176175adantl 474 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑥↑2) ∈ ℂ ∧ (1 − (𝑥↑2)) ∈ (-∞(,]0)) → (1 − (𝑥↑2)) ≤ 0)
177 letr 10420 . . . . . . . . . . . . . . . . . . . . . . . 24 (((1 − (𝑥↑2)) ∈ ℝ ∧ 0 ∈ ℝ ∧ 1 ∈ ℝ) → (((1 − (𝑥↑2)) ≤ 0 ∧ 0 ≤ 1) → (1 − (𝑥↑2)) ≤ 1))
17836, 89, 177mp3an23 1578 . . . . . . . . . . . . . . . . . . . . . . 23 ((1 − (𝑥↑2)) ∈ ℝ → (((1 − (𝑥↑2)) ≤ 0 ∧ 0 ≤ 1) → (1 − (𝑥↑2)) ≤ 1))
179139, 178mpan2i 689 . . . . . . . . . . . . . . . . . . . . . 22 ((1 − (𝑥↑2)) ∈ ℝ → ((1 − (𝑥↑2)) ≤ 0 → (1 − (𝑥↑2)) ≤ 1))
180174, 176, 179sylc 65 . . . . . . . . . . . . . . . . . . . . 21 (((𝑥↑2) ∈ ℂ ∧ (1 − (𝑥↑2)) ∈ (-∞(,]0)) → (1 − (𝑥↑2)) ≤ 1)
181 subge0 10832 . . . . . . . . . . . . . . . . . . . . . 22 ((1 ∈ ℝ ∧ (1 − (𝑥↑2)) ∈ ℝ) → (0 ≤ (1 − (1 − (𝑥↑2))) ↔ (1 − (𝑥↑2)) ≤ 1))
18289, 174, 181sylancr 582 . . . . . . . . . . . . . . . . . . . . 21 (((𝑥↑2) ∈ ℂ ∧ (1 − (𝑥↑2)) ∈ (-∞(,]0)) → (0 ≤ (1 − (1 − (𝑥↑2))) ↔ (1 − (𝑥↑2)) ≤ 1))
183180, 182mpbird 249 . . . . . . . . . . . . . . . . . . . 20 (((𝑥↑2) ∈ ℂ ∧ (1 − (𝑥↑2)) ∈ (-∞(,]0)) → 0 ≤ (1 − (1 − (𝑥↑2))))
184170adantr 473 . . . . . . . . . . . . . . . . . . . 20 (((𝑥↑2) ∈ ℂ ∧ (1 − (𝑥↑2)) ∈ (-∞(,]0)) → (1 − (1 − (𝑥↑2))) = (𝑥↑2))
185183, 184breqtrd 4868 . . . . . . . . . . . . . . . . . . 19 (((𝑥↑2) ∈ ℂ ∧ (1 − (𝑥↑2)) ∈ (-∞(,]0)) → 0 ≤ (𝑥↑2))
186173, 185resqrtcld 14494 . . . . . . . . . . . . . . . . . 18 (((𝑥↑2) ∈ ℂ ∧ (1 − (𝑥↑2)) ∈ (-∞(,]0)) → (√‘(𝑥↑2)) ∈ ℝ)
18717, 186sylan 576 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ ℂ ∧ (1 − (𝑥↑2)) ∈ (-∞(,]0)) → (√‘(𝑥↑2)) ∈ ℝ)
188 eleq1 2865 . . . . . . . . . . . . . . . . 17 (𝑥 = (√‘(𝑥↑2)) → (𝑥 ∈ ℝ ↔ (√‘(𝑥↑2)) ∈ ℝ))
189187, 188syl5ibrcom 239 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ ℂ ∧ (1 − (𝑥↑2)) ∈ (-∞(,]0)) → (𝑥 = (√‘(𝑥↑2)) → 𝑥 ∈ ℝ))
190187renegcld 10748 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ ℂ ∧ (1 − (𝑥↑2)) ∈ (-∞(,]0)) → -(√‘(𝑥↑2)) ∈ ℝ)
191 eleq1 2865 . . . . . . . . . . . . . . . . 17 (𝑥 = -(√‘(𝑥↑2)) → (𝑥 ∈ ℝ ↔ -(√‘(𝑥↑2)) ∈ ℝ))
192190, 191syl5ibrcom 239 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ ℂ ∧ (1 − (𝑥↑2)) ∈ (-∞(,]0)) → (𝑥 = -(√‘(𝑥↑2)) → 𝑥 ∈ ℝ))
193 eqid 2798 . . . . . . . . . . . . . . . . . 18 (𝑥↑2) = (𝑥↑2)
194 eqsqrtor 14444 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ ℂ ∧ (𝑥↑2) ∈ ℂ) → ((𝑥↑2) = (𝑥↑2) ↔ (𝑥 = (√‘(𝑥↑2)) ∨ 𝑥 = -(√‘(𝑥↑2)))))
19517, 194mpdan 679 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ℂ → ((𝑥↑2) = (𝑥↑2) ↔ (𝑥 = (√‘(𝑥↑2)) ∨ 𝑥 = -(√‘(𝑥↑2)))))
196193, 195mpbii 225 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ℂ → (𝑥 = (√‘(𝑥↑2)) ∨ 𝑥 = -(√‘(𝑥↑2))))
197196adantr 473 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ ℂ ∧ (1 − (𝑥↑2)) ∈ (-∞(,]0)) → (𝑥 = (√‘(𝑥↑2)) ∨ 𝑥 = -(√‘(𝑥↑2))))
198189, 192, 197mpjaod 887 . . . . . . . . . . . . . . 15 ((𝑥 ∈ ℂ ∧ (1 − (𝑥↑2)) ∈ (-∞(,]0)) → 𝑥 ∈ ℝ)
199198stoic1a 1868 . . . . . . . . . . . . . 14 ((𝑥 ∈ ℂ ∧ ¬ 𝑥 ∈ ℝ) → ¬ (1 − (𝑥↑2)) ∈ (-∞(,]0))
20012, 199sylan 576 . . . . . . . . . . . . 13 ((𝑥𝐷 ∧ ¬ 𝑥 ∈ ℝ) → ¬ (1 − (𝑥↑2)) ∈ (-∞(,]0))
201162, 200pm2.61dan 848 . . . . . . . . . . . 12 (𝑥𝐷 → ¬ (1 − (𝑥↑2)) ∈ (-∞(,]0))
202111, 201eldifd 3779 . . . . . . . . . . 11 (𝑥𝐷 → (1 − (𝑥↑2)) ∈ (ℂ ∖ (-∞(,]0)))
203202adantl 474 . . . . . . . . . 10 ((⊤ ∧ 𝑥𝐷) → (1 − (𝑥↑2)) ∈ (ℂ ∖ (-∞(,]0)))
204 2cnd 11388 . . . . . . . . . . . . . 14 (𝑥 ∈ ℂ → 2 ∈ ℂ)
205 id 22 . . . . . . . . . . . . . 14 (𝑥 ∈ ℂ → 𝑥 ∈ ℂ)
206204, 205mulcld 10348 . . . . . . . . . . . . 13 (𝑥 ∈ ℂ → (2 · 𝑥) ∈ ℂ)
207206negcld 10670 . . . . . . . . . . . 12 (𝑥 ∈ ℂ → -(2 · 𝑥) ∈ ℂ)
208207adantl 474 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ ℂ) → -(2 · 𝑥) ∈ ℂ)
20912, 208sylan2 587 . . . . . . . . . 10 ((⊤ ∧ 𝑥𝐷) → -(2 · 𝑥) ∈ ℂ)
21059sqrtcld 14514 . . . . . . . . . . 11 (𝑦 ∈ (ℂ ∖ (-∞(,]0)) → (√‘𝑦) ∈ ℂ)
211210adantl 474 . . . . . . . . . 10 ((⊤ ∧ 𝑦 ∈ (ℂ ∖ (-∞(,]0))) → (√‘𝑦) ∈ ℂ)
212 ovexd 6911 . . . . . . . . . 10 ((⊤ ∧ 𝑦 ∈ (ℂ ∖ (-∞(,]0))) → (1 / (2 · (√‘𝑦))) ∈ V)
21319adantl 474 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ ℂ) → (1 − (𝑥↑2)) ∈ ℂ)
21436a1i 11 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑥 ∈ ℂ) → 0 ∈ ℝ)
215 1cnd 10322 . . . . . . . . . . . . . 14 (⊤ → 1 ∈ ℂ)
21611, 215dvmptc 24059 . . . . . . . . . . . . 13 (⊤ → (ℂ D (𝑥 ∈ ℂ ↦ 1)) = (𝑥 ∈ ℂ ↦ 0))
21717adantl 474 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑥 ∈ ℂ) → (𝑥↑2) ∈ ℂ)
218 2cn 11385 . . . . . . . . . . . . . . 15 2 ∈ ℂ
219 mulcl 10307 . . . . . . . . . . . . . . 15 ((2 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (2 · 𝑥) ∈ ℂ)
220218, 219mpan 682 . . . . . . . . . . . . . 14 (𝑥 ∈ ℂ → (2 · 𝑥) ∈ ℂ)
221220adantl 474 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑥 ∈ ℂ) → (2 · 𝑥) ∈ ℂ)
222 2nn 11383 . . . . . . . . . . . . . . . 16 2 ∈ ℕ
223 dvexp 24054 . . . . . . . . . . . . . . . 16 (2 ∈ ℕ → (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑2))) = (𝑥 ∈ ℂ ↦ (2 · (𝑥↑(2 − 1)))))
224222, 223ax-mp 5 . . . . . . . . . . . . . . 15 (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑2))) = (𝑥 ∈ ℂ ↦ (2 · (𝑥↑(2 − 1))))
225 2m1e1 11443 . . . . . . . . . . . . . . . . . . 19 (2 − 1) = 1
226225oveq2i 6888 . . . . . . . . . . . . . . . . . 18 (𝑥↑(2 − 1)) = (𝑥↑1)
227 exp1 13117 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ℂ → (𝑥↑1) = 𝑥)
228226, 227syl5eq 2844 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ℂ → (𝑥↑(2 − 1)) = 𝑥)
229228oveq2d 6893 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ℂ → (2 · (𝑥↑(2 − 1))) = (2 · 𝑥))
230229mpteq2ia 4932 . . . . . . . . . . . . . . 15 (𝑥 ∈ ℂ ↦ (2 · (𝑥↑(2 − 1)))) = (𝑥 ∈ ℂ ↦ (2 · 𝑥))
231224, 230eqtri 2820 . . . . . . . . . . . . . 14 (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑2))) = (𝑥 ∈ ℂ ↦ (2 · 𝑥))
232231a1i 11 . . . . . . . . . . . . 13 (⊤ → (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑2))) = (𝑥 ∈ ℂ ↦ (2 · 𝑥)))
23311, 79, 214, 216, 217, 221, 232dvmptsub 24068 . . . . . . . . . . . 12 (⊤ → (ℂ D (𝑥 ∈ ℂ ↦ (1 − (𝑥↑2)))) = (𝑥 ∈ ℂ ↦ (0 − (2 · 𝑥))))
234 df-neg 10558 . . . . . . . . . . . . 13 -(2 · 𝑥) = (0 − (2 · 𝑥))
235234mpteq2i 4933 . . . . . . . . . . . 12 (𝑥 ∈ ℂ ↦ -(2 · 𝑥)) = (𝑥 ∈ ℂ ↦ (0 − (2 · 𝑥)))
236233, 235syl6eqr 2850 . . . . . . . . . . 11 (⊤ → (ℂ D (𝑥 ∈ ℂ ↦ (1 − (𝑥↑2)))) = (𝑥 ∈ ℂ ↦ -(2 · 𝑥)))
23711, 213, 208, 236, 81, 84, 82, 103dvmptres 24064 . . . . . . . . . 10 (⊤ → (ℂ D (𝑥𝐷 ↦ (1 − (𝑥↑2)))) = (𝑥𝐷 ↦ -(2 · 𝑥)))
238 eqid 2798 . . . . . . . . . . . 12 (ℂ ∖ (-∞(,]0)) = (ℂ ∖ (-∞(,]0))
239238dvcnsqrt 24826 . . . . . . . . . . 11 (ℂ D (𝑦 ∈ (ℂ ∖ (-∞(,]0)) ↦ (√‘𝑦))) = (𝑦 ∈ (ℂ ∖ (-∞(,]0)) ↦ (1 / (2 · (√‘𝑦))))
240239a1i 11 . . . . . . . . . 10 (⊤ → (ℂ D (𝑦 ∈ (ℂ ∖ (-∞(,]0)) ↦ (√‘𝑦))) = (𝑦 ∈ (ℂ ∖ (-∞(,]0)) ↦ (1 / (2 · (√‘𝑦)))))
241 fveq2 6410 . . . . . . . . . 10 (𝑦 = (1 − (𝑥↑2)) → (√‘𝑦) = (√‘(1 − (𝑥↑2))))
242241oveq2d 6893 . . . . . . . . . . 11 (𝑦 = (1 − (𝑥↑2)) → (2 · (√‘𝑦)) = (2 · (√‘(1 − (𝑥↑2)))))
243242oveq2d 6893 . . . . . . . . . 10 (𝑦 = (1 − (𝑥↑2)) → (1 / (2 · (√‘𝑦))) = (1 / (2 · (√‘(1 − (𝑥↑2))))))
24411, 11, 203, 209, 211, 212, 237, 240, 241, 243dvmptco 24073 . . . . . . . . 9 (⊤ → (ℂ D (𝑥𝐷 ↦ (√‘(1 − (𝑥↑2))))) = (𝑥𝐷 ↦ ((1 / (2 · (√‘(1 − (𝑥↑2))))) · -(2 · 𝑥))))
245 mulneg2 10758 . . . . . . . . . . . . 13 ((2 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (2 · -𝑥) = -(2 · 𝑥))
246218, 12, 245sylancr 582 . . . . . . . . . . . 12 (𝑥𝐷 → (2 · -𝑥) = -(2 · 𝑥))
247246oveq1d 6892 . . . . . . . . . . 11 (𝑥𝐷 → ((2 · -𝑥) / (2 · (√‘(1 − (𝑥↑2))))) = (-(2 · 𝑥) / (2 · (√‘(1 − (𝑥↑2))))))
24812negcld 10670 . . . . . . . . . . . 12 (𝑥𝐷 → -𝑥 ∈ ℂ)
249 eldifn 3930 . . . . . . . . . . . . . . 15 (𝑥 ∈ (ℂ ∖ ((-∞(,]-1) ∪ (1[,)+∞))) → ¬ 𝑥 ∈ ((-∞(,]-1) ∪ (1[,)+∞)))
250249, 3eleq2s 2895 . . . . . . . . . . . . . 14 (𝑥𝐷 → ¬ 𝑥 ∈ ((-∞(,]-1) ∪ (1[,)+∞)))
251 id 22 . . . . . . . . . . . . . . . . . 18 (𝑥 = -1 → 𝑥 = -1)
252 mnflt 12201 . . . . . . . . . . . . . . . . . . . 20 (-1 ∈ ℝ → -∞ < -1)
25386, 252ax-mp 5 . . . . . . . . . . . . . . . . . . 19 -∞ < -1
254 ubioc1 12473 . . . . . . . . . . . . . . . . . . 19 ((-∞ ∈ ℝ* ∧ -1 ∈ ℝ* ∧ -∞ < -1) → -1 ∈ (-∞(,]-1))
25551, 132, 253, 254mp3an 1586 . . . . . . . . . . . . . . . . . 18 -1 ∈ (-∞(,]-1)
256251, 255syl6eqel 2885 . . . . . . . . . . . . . . . . 17 (𝑥 = -1 → 𝑥 ∈ (-∞(,]-1))
257 id 22 . . . . . . . . . . . . . . . . . 18 (𝑥 = 1 → 𝑥 = 1)
258 ltpnf 12198 . . . . . . . . . . . . . . . . . . . 20 (1 ∈ ℝ → 1 < +∞)
25989, 258ax-mp 5 . . . . . . . . . . . . . . . . . . 19 1 < +∞
260 lbico1 12474 . . . . . . . . . . . . . . . . . . 19 ((1 ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ 1 < +∞) → 1 ∈ (1[,)+∞))
261133, 121, 259, 260mp3an 1586 . . . . . . . . . . . . . . . . . 18 1 ∈ (1[,)+∞)
262257, 261syl6eqel 2885 . . . . . . . . . . . . . . . . 17 (𝑥 = 1 → 𝑥 ∈ (1[,)+∞))
263256, 262orim12i 933 . . . . . . . . . . . . . . . 16 ((𝑥 = -1 ∨ 𝑥 = 1) → (𝑥 ∈ (-∞(,]-1) ∨ 𝑥 ∈ (1[,)+∞)))
264263orcoms 899 . . . . . . . . . . . . . . 15 ((𝑥 = 1 ∨ 𝑥 = -1) → (𝑥 ∈ (-∞(,]-1) ∨ 𝑥 ∈ (1[,)+∞)))
265 elun 3950 . . . . . . . . . . . . . . 15 (𝑥 ∈ ((-∞(,]-1) ∪ (1[,)+∞)) ↔ (𝑥 ∈ (-∞(,]-1) ∨ 𝑥 ∈ (1[,)+∞)))
266264, 265sylibr 226 . . . . . . . . . . . . . 14 ((𝑥 = 1 ∨ 𝑥 = -1) → 𝑥 ∈ ((-∞(,]-1) ∪ (1[,)+∞)))
267250, 266nsyl 138 . . . . . . . . . . . . 13 (𝑥𝐷 → ¬ (𝑥 = 1 ∨ 𝑥 = -1))
268 1cnd 10322 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) = 0) → 1 ∈ ℂ)
26917adantr 473 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) = 0) → (𝑥↑2) ∈ ℂ)
27019adantr 473 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) = 0) → (1 − (𝑥↑2)) ∈ ℂ)
271 simpr 478 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) = 0) → (√‘(1 − (𝑥↑2))) = 0)
272270, 271sqr00d 14518 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) = 0) → (1 − (𝑥↑2)) = 0)
273268, 269, 272subeq0d 10691 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) = 0) → 1 = (𝑥↑2))
274146, 273syl5req 2845 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) = 0) → (𝑥↑2) = (1↑2))
275274ex 402 . . . . . . . . . . . . . . 15 (𝑥 ∈ ℂ → ((√‘(1 − (𝑥↑2))) = 0 → (𝑥↑2) = (1↑2)))
276 sqeqor 13229 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑥↑2) = (1↑2) ↔ (𝑥 = 1 ∨ 𝑥 = -1)))
27716, 276mpan2 683 . . . . . . . . . . . . . . 15 (𝑥 ∈ ℂ → ((𝑥↑2) = (1↑2) ↔ (𝑥 = 1 ∨ 𝑥 = -1)))
278275, 277sylibd 231 . . . . . . . . . . . . . 14 (𝑥 ∈ ℂ → ((√‘(1 − (𝑥↑2))) = 0 → (𝑥 = 1 ∨ 𝑥 = -1)))
279278necon3bd 2984 . . . . . . . . . . . . 13 (𝑥 ∈ ℂ → (¬ (𝑥 = 1 ∨ 𝑥 = -1) → (√‘(1 − (𝑥↑2))) ≠ 0))
28012, 267, 279sylc 65 . . . . . . . . . . . 12 (𝑥𝐷 → (√‘(1 − (𝑥↑2))) ≠ 0)
281 2cnne0 11527 . . . . . . . . . . . . 13 (2 ∈ ℂ ∧ 2 ≠ 0)
282 divcan5 11018 . . . . . . . . . . . . 13 ((-𝑥 ∈ ℂ ∧ ((√‘(1 − (𝑥↑2))) ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) ≠ 0) ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → ((2 · -𝑥) / (2 · (√‘(1 − (𝑥↑2))))) = (-𝑥 / (√‘(1 − (𝑥↑2)))))
283281, 282mp3an3 1575 . . . . . . . . . . . 12 ((-𝑥 ∈ ℂ ∧ ((√‘(1 − (𝑥↑2))) ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) ≠ 0)) → ((2 · -𝑥) / (2 · (√‘(1 − (𝑥↑2))))) = (-𝑥 / (√‘(1 − (𝑥↑2)))))
284248, 112, 280, 283syl12anc 866 . . . . . . . . . . 11 (𝑥𝐷 → ((2 · -𝑥) / (2 · (√‘(1 − (𝑥↑2))))) = (-𝑥 / (√‘(1 − (𝑥↑2)))))
285218, 12, 219sylancr 582 . . . . . . . . . . . . 13 (𝑥𝐷 → (2 · 𝑥) ∈ ℂ)
286285negcld 10670 . . . . . . . . . . . 12 (𝑥𝐷 → -(2 · 𝑥) ∈ ℂ)
287 mulcl 10307 . . . . . . . . . . . . 13 ((2 ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) ∈ ℂ) → (2 · (√‘(1 − (𝑥↑2)))) ∈ ℂ)
288218, 112, 287sylancr 582 . . . . . . . . . . . 12 (𝑥𝐷 → (2 · (√‘(1 − (𝑥↑2)))) ∈ ℂ)
289 mulne0 10960 . . . . . . . . . . . . . 14 (((2 ∈ ℂ ∧ 2 ≠ 0) ∧ ((√‘(1 − (𝑥↑2))) ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) ≠ 0)) → (2 · (√‘(1 − (𝑥↑2)))) ≠ 0)
290281, 289mpan 682 . . . . . . . . . . . . 13 (((√‘(1 − (𝑥↑2))) ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) ≠ 0) → (2 · (√‘(1 − (𝑥↑2)))) ≠ 0)
291112, 280, 290syl2anc 580 . . . . . . . . . . . 12 (𝑥𝐷 → (2 · (√‘(1 − (𝑥↑2)))) ≠ 0)
292286, 288, 291divrec2d 11096 . . . . . . . . . . 11 (𝑥𝐷 → (-(2 · 𝑥) / (2 · (√‘(1 − (𝑥↑2))))) = ((1 / (2 · (√‘(1 − (𝑥↑2))))) · -(2 · 𝑥)))
293247, 284, 2923eqtr3rd 2841 . . . . . . . . . 10 (𝑥𝐷 → ((1 / (2 · (√‘(1 − (𝑥↑2))))) · -(2 · 𝑥)) = (-𝑥 / (√‘(1 − (𝑥↑2)))))
294293mpteq2ia 4932 . . . . . . . . 9 (𝑥𝐷 ↦ ((1 / (2 · (√‘(1 − (𝑥↑2))))) · -(2 · 𝑥))) = (𝑥𝐷 ↦ (-𝑥 / (√‘(1 − (𝑥↑2)))))
295244, 294syl6eq 2848 . . . . . . . 8 (⊤ → (ℂ D (𝑥𝐷 ↦ (√‘(1 − (𝑥↑2))))) = (𝑥𝐷 ↦ (-𝑥 / (√‘(1 − (𝑥↑2))))))
29611, 74, 75, 109, 113, 114, 295dvmptadd 24061 . . . . . . 7 (⊤ → (ℂ D (𝑥𝐷 ↦ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))))) = (𝑥𝐷 ↦ (i + (-𝑥 / (√‘(1 − (𝑥↑2)))))))
297 mulcl 10307 . . . . . . . . . . . 12 ((i ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) ∈ ℂ) → (i · (√‘(1 − (𝑥↑2)))) ∈ ℂ)
29813, 20, 297sylancr 582 . . . . . . . . . . 11 (𝑥 ∈ ℂ → (i · (√‘(1 − (𝑥↑2)))) ∈ ℂ)
29912, 298syl 17 . . . . . . . . . 10 (𝑥𝐷 → (i · (√‘(1 − (𝑥↑2)))) ∈ ℂ)
300299, 248, 112, 280divdird 11130 . . . . . . . . 9 (𝑥𝐷 → (((i · (√‘(1 − (𝑥↑2)))) + -𝑥) / (√‘(1 − (𝑥↑2)))) = (((i · (√‘(1 − (𝑥↑2)))) / (√‘(1 − (𝑥↑2)))) + (-𝑥 / (√‘(1 − (𝑥↑2))))))
301 ixi 10947 . . . . . . . . . . . . . . . 16 (i · i) = -1
302301eqcomi 2807 . . . . . . . . . . . . . . 15 -1 = (i · i)
303302oveq1i 6887 . . . . . . . . . . . . . 14 (-1 · 𝑥) = ((i · i) · 𝑥)
304 mulm1 10762 . . . . . . . . . . . . . 14 (𝑥 ∈ ℂ → (-1 · 𝑥) = -𝑥)
305 mulass 10311 . . . . . . . . . . . . . . 15 ((i ∈ ℂ ∧ i ∈ ℂ ∧ 𝑥 ∈ ℂ) → ((i · i) · 𝑥) = (i · (i · 𝑥)))
30613, 13, 305mp3an12 1576 . . . . . . . . . . . . . 14 (𝑥 ∈ ℂ → ((i · i) · 𝑥) = (i · (i · 𝑥)))
307303, 304, 3063eqtr3a 2856 . . . . . . . . . . . . 13 (𝑥 ∈ ℂ → -𝑥 = (i · (i · 𝑥)))
308307oveq1d 6892 . . . . . . . . . . . 12 (𝑥 ∈ ℂ → (-𝑥 + (i · (√‘(1 − (𝑥↑2))))) = ((i · (i · 𝑥)) + (i · (√‘(1 − (𝑥↑2))))))
309 negcl 10571 . . . . . . . . . . . . 13 (𝑥 ∈ ℂ → -𝑥 ∈ ℂ)
310298, 309addcomd 10527 . . . . . . . . . . . 12 (𝑥 ∈ ℂ → ((i · (√‘(1 − (𝑥↑2)))) + -𝑥) = (-𝑥 + (i · (√‘(1 − (𝑥↑2))))))
31113a1i 11 . . . . . . . . . . . . 13 (𝑥 ∈ ℂ → i ∈ ℂ)
312311, 15, 20adddid 10352 . . . . . . . . . . . 12 (𝑥 ∈ ℂ → (i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) = ((i · (i · 𝑥)) + (i · (√‘(1 − (𝑥↑2))))))
313308, 310, 3123eqtr4d 2842 . . . . . . . . . . 11 (𝑥 ∈ ℂ → ((i · (√‘(1 − (𝑥↑2)))) + -𝑥) = (i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))))
31412, 313syl 17 . . . . . . . . . 10 (𝑥𝐷 → ((i · (√‘(1 − (𝑥↑2)))) + -𝑥) = (i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))))
315314oveq1d 6892 . . . . . . . . 9 (𝑥𝐷 → (((i · (√‘(1 − (𝑥↑2)))) + -𝑥) / (√‘(1 − (𝑥↑2)))) = ((i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) / (√‘(1 − (𝑥↑2)))))
31672, 112, 280divcan4d 11098 . . . . . . . . . 10 (𝑥𝐷 → ((i · (√‘(1 − (𝑥↑2)))) / (√‘(1 − (𝑥↑2)))) = i)
317316oveq1d 6892 . . . . . . . . 9 (𝑥𝐷 → (((i · (√‘(1 − (𝑥↑2)))) / (√‘(1 − (𝑥↑2)))) + (-𝑥 / (√‘(1 − (𝑥↑2))))) = (i + (-𝑥 / (√‘(1 − (𝑥↑2))))))
318300, 315, 3173eqtr3rd 2841 . . . . . . . 8 (𝑥𝐷 → (i + (-𝑥 / (√‘(1 − (𝑥↑2))))) = ((i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) / (√‘(1 − (𝑥↑2)))))
319318mpteq2ia 4932 . . . . . . 7 (𝑥𝐷 ↦ (i + (-𝑥 / (√‘(1 − (𝑥↑2)))))) = (𝑥𝐷 ↦ ((i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) / (√‘(1 − (𝑥↑2)))))
320296, 319syl6eq 2848 . . . . . 6 (⊤ → (ℂ D (𝑥𝐷 ↦ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))))) = (𝑥𝐷 ↦ ((i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) / (√‘(1 − (𝑥↑2))))))
321238dvlog 24735 . . . . . . 7 (ℂ D (log ↾ (ℂ ∖ (-∞(,]0)))) = (𝑦 ∈ (ℂ ∖ (-∞(,]0)) ↦ (1 / 𝑦))
322 logf1o 24649 . . . . . . . . . 10 log:(ℂ ∖ {0})–1-1-onto→ran log
323 f1of 6355 . . . . . . . . . 10 (log:(ℂ ∖ {0})–1-1-onto→ran log → log:(ℂ ∖ {0})⟶ran log)
324322, 323mp1i 13 . . . . . . . . 9 (⊤ → log:(ℂ ∖ {0})⟶ran log)
325 snssi 4526 . . . . . . . . . . 11 (0 ∈ (-∞(,]0) → {0} ⊆ (-∞(,]0))
32664, 325ax-mp 5 . . . . . . . . . 10 {0} ⊆ (-∞(,]0)
327 sscon 3941 . . . . . . . . . 10 ({0} ⊆ (-∞(,]0) → (ℂ ∖ (-∞(,]0)) ⊆ (ℂ ∖ {0}))
328326, 327mp1i 13 . . . . . . . . 9 (⊤ → (ℂ ∖ (-∞(,]0)) ⊆ (ℂ ∖ {0}))
329324, 328feqresmpt 6474 . . . . . . . 8 (⊤ → (log ↾ (ℂ ∖ (-∞(,]0))) = (𝑦 ∈ (ℂ ∖ (-∞(,]0)) ↦ (log‘𝑦)))
330329oveq2d 6893 . . . . . . 7 (⊤ → (ℂ D (log ↾ (ℂ ∖ (-∞(,]0)))) = (ℂ D (𝑦 ∈ (ℂ ∖ (-∞(,]0)) ↦ (log‘𝑦))))
331321, 330syl5reqr 2847 . . . . . 6 (⊤ → (ℂ D (𝑦 ∈ (ℂ ∖ (-∞(,]0)) ↦ (log‘𝑦))) = (𝑦 ∈ (ℂ ∖ (-∞(,]0)) ↦ (1 / 𝑦)))
332 fveq2 6410 . . . . . 6 (𝑦 = ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) → (log‘𝑦) = (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))))
333 oveq2 6885 . . . . . 6 (𝑦 = ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) → (1 / 𝑦) = (1 / ((i · 𝑥) + (√‘(1 − (𝑥↑2))))))
33411, 11, 57, 58, 70, 71, 320, 331, 332, 333dvmptco 24073 . . . . 5 (⊤ → (ℂ D (𝑥𝐷 ↦ (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))))) = (𝑥𝐷 ↦ ((1 / ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) · ((i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) / (√‘(1 − (𝑥↑2)))))))
33522, 24reccld 11085 . . . . . . . 8 (𝑥𝐷 → (1 / ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) ∈ ℂ)
336 mulcl 10307 . . . . . . . . . 10 ((i ∈ ℂ ∧ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℂ) → (i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) ∈ ℂ)
33713, 21, 336sylancr 582 . . . . . . . . 9 (𝑥 ∈ ℂ → (i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) ∈ ℂ)
33812, 337syl 17 . . . . . . . 8 (𝑥𝐷 → (i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) ∈ ℂ)
339335, 338, 112, 280divassd 11127 . . . . . . 7 (𝑥𝐷 → (((1 / ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) · (i · ((i · 𝑥) + (√‘(1 − (𝑥↑2)))))) / (√‘(1 − (𝑥↑2)))) = ((1 / ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) · ((i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) / (√‘(1 − (𝑥↑2))))))
340338, 22, 24divrec2d 11096 . . . . . . . . 9 (𝑥𝐷 → ((i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) / ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) = ((1 / ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) · (i · ((i · 𝑥) + (√‘(1 − (𝑥↑2)))))))
34172, 22, 24divcan4d 11098 . . . . . . . . 9 (𝑥𝐷 → ((i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) / ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) = i)
342340, 341eqtr3d 2834 . . . . . . . 8 (𝑥𝐷 → ((1 / ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) · (i · ((i · 𝑥) + (√‘(1 − (𝑥↑2)))))) = i)
343342oveq1d 6892 . . . . . . 7 (𝑥𝐷 → (((1 / ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) · (i · ((i · 𝑥) + (√‘(1 − (𝑥↑2)))))) / (√‘(1 − (𝑥↑2)))) = (i / (√‘(1 − (𝑥↑2)))))
344339, 343eqtr3d 2834 . . . . . 6 (𝑥𝐷 → ((1 / ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) · ((i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) / (√‘(1 − (𝑥↑2))))) = (i / (√‘(1 − (𝑥↑2)))))
345344mpteq2ia 4932 . . . . 5 (𝑥𝐷 ↦ ((1 / ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) · ((i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) / (√‘(1 − (𝑥↑2)))))) = (𝑥𝐷 ↦ (i / (√‘(1 − (𝑥↑2)))))
346334, 345syl6eq 2848 . . . 4 (⊤ → (ℂ D (𝑥𝐷 ↦ (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))))) = (𝑥𝐷 ↦ (i / (√‘(1 − (𝑥↑2))))))
347 negicn 10572 . . . . 5 -i ∈ ℂ
348347a1i 11 . . . 4 (⊤ → -i ∈ ℂ)
34911, 26, 27, 346, 348dvmptcmul 24065 . . 3 (⊤ → (ℂ D (𝑥𝐷 ↦ (-i · (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2)))))))) = (𝑥𝐷 ↦ (-i · (i / (√‘(1 − (𝑥↑2)))))))
350349mptru 1661 . 2 (ℂ D (𝑥𝐷 ↦ (-i · (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2)))))))) = (𝑥𝐷 ↦ (-i · (i / (√‘(1 − (𝑥↑2))))))
35113, 13mulneg1i 10767 . . . . . 6 (-i · i) = -(i · i)
352301negeqi 10564 . . . . . 6 -(i · i) = --1
353 negneg1e1 11435 . . . . . 6 --1 = 1
354351, 352, 3533eqtri 2824 . . . . 5 (-i · i) = 1
355354oveq1i 6887 . . . 4 ((-i · i) / (√‘(1 − (𝑥↑2)))) = (1 / (√‘(1 − (𝑥↑2))))
356 divass 10994 . . . . . 6 ((-i ∈ ℂ ∧ i ∈ ℂ ∧ ((√‘(1 − (𝑥↑2))) ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) ≠ 0)) → ((-i · i) / (√‘(1 − (𝑥↑2)))) = (-i · (i / (√‘(1 − (𝑥↑2))))))
357347, 13, 356mp3an12 1576 . . . . 5 (((√‘(1 − (𝑥↑2))) ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) ≠ 0) → ((-i · i) / (√‘(1 − (𝑥↑2)))) = (-i · (i / (√‘(1 − (𝑥↑2))))))
358112, 280, 357syl2anc 580 . . . 4 (𝑥𝐷 → ((-i · i) / (√‘(1 − (𝑥↑2)))) = (-i · (i / (√‘(1 − (𝑥↑2))))))
359355, 358syl5reqr 2847 . . 3 (𝑥𝐷 → (-i · (i / (√‘(1 − (𝑥↑2))))) = (1 / (√‘(1 − (𝑥↑2)))))
360359mpteq2ia 4932 . 2 (𝑥𝐷 ↦ (-i · (i / (√‘(1 − (𝑥↑2)))))) = (𝑥𝐷 ↦ (1 / (√‘(1 − (𝑥↑2)))))
3619, 350, 3603eqtri 2824 1 (ℂ D (arcsin ↾ 𝐷)) = (𝑥𝐷 ↦ (1 / (√‘(1 − (𝑥↑2)))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 198  wa 385  wo 874  w3o 1107  w3a 1108   = wceq 1653  wtru 1654  wcel 2157  wne 2970  Vcvv 3384  cdif 3765  cun 3766  cin 3767  wss 3768  c0 4114  {csn 4367  {cpr 4369   class class class wbr 4842  cmpt 4921  ran crn 5312  cres 5313  wf 6096  1-1-ontowf1o 6099  cfv 6100  (class class class)co 6877  cc 10221  cr 10222  0cc0 10223  1c1 10224  ici 10225   + caddc 10226   · cmul 10228  +∞cpnf 10359  -∞cmnf 10360  *cxr 10361   < clt 10362  cle 10363  cmin 10555  -cneg 10556   / cdiv 10975  cn 11311  2c2 11365  +crp 12071  (,)cioo 12421  (,]cioc 12422  [,)cico 12423  cexp 13111  cre 14175  csqrt 14311  abscabs 14312  t crest 16393  TopOpenctopn 16394  topGenctg 16410  fldccnfld 20065  Clsdccld 21146   D cdv 23965  logclog 24639  arcsincasin 24938
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-8 2159  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-13 2377  ax-ext 2776  ax-rep 4963  ax-sep 4974  ax-nul 4982  ax-pow 5034  ax-pr 5096  ax-un 7182  ax-inf2 8787  ax-cnex 10279  ax-resscn 10280  ax-1cn 10281  ax-icn 10282  ax-addcl 10283  ax-addrcl 10284  ax-mulcl 10285  ax-mulrcl 10286  ax-mulcom 10287  ax-addass 10288  ax-mulass 10289  ax-distr 10290  ax-i2m1 10291  ax-1ne0 10292  ax-1rid 10293  ax-rnegex 10294  ax-rrecex 10295  ax-cnre 10296  ax-pre-lttri 10297  ax-pre-lttrn 10298  ax-pre-ltadd 10299  ax-pre-mulgt0 10300  ax-pre-sup 10301  ax-addf 10302  ax-mulf 10303
This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-3or 1109  df-3an 1110  df-tru 1657  df-fal 1667  df-ex 1876  df-nf 1880  df-sb 2065  df-mo 2591  df-eu 2609  df-clab 2785  df-cleq 2791  df-clel 2794  df-nfc 2929  df-ne 2971  df-nel 3074  df-ral 3093  df-rex 3094  df-reu 3095  df-rmo 3096  df-rab 3097  df-v 3386  df-sbc 3633  df-csb 3728  df-dif 3771  df-un 3773  df-in 3775  df-ss 3782  df-pss 3784  df-nul 4115  df-if 4277  df-pw 4350  df-sn 4368  df-pr 4370  df-tp 4372  df-op 4374  df-uni 4628  df-int 4667  df-iun 4711  df-iin 4712  df-br 4843  df-opab 4905  df-mpt 4922  df-tr 4945  df-id 5219  df-eprel 5224  df-po 5232  df-so 5233  df-fr 5270  df-se 5271  df-we 5272  df-xp 5317  df-rel 5318  df-cnv 5319  df-co 5320  df-dm 5321  df-rn 5322  df-res 5323  df-ima 5324  df-pred 5897  df-ord 5943  df-on 5944  df-lim 5945  df-suc 5946  df-iota 6063  df-fun 6102  df-fn 6103  df-f 6104  df-f1 6105  df-fo 6106  df-f1o 6107  df-fv 6108  df-isom 6109  df-riota 6838  df-ov 6880  df-oprab 6881  df-mpt2 6882  df-of 7130  df-om 7299  df-1st 7400  df-2nd 7401  df-supp 7532  df-wrecs 7644  df-recs 7706  df-rdg 7744  df-1o 7798  df-2o 7799  df-oadd 7802  df-er 7981  df-map 8096  df-pm 8097  df-ixp 8148  df-en 8195  df-dom 8196  df-sdom 8197  df-fin 8198  df-fsupp 8517  df-fi 8558  df-sup 8589  df-inf 8590  df-oi 8656  df-card 9050  df-cda 9277  df-pnf 10364  df-mnf 10365  df-xr 10366  df-ltxr 10367  df-le 10368  df-sub 10557  df-neg 10558  df-div 10976  df-nn 11312  df-2 11373  df-3 11374  df-4 11375  df-5 11376  df-6 11377  df-7 11378  df-8 11379  df-9 11380  df-n0 11578  df-z 11664  df-dec 11781  df-uz 11928  df-q 12031  df-rp 12072  df-xneg 12190  df-xadd 12191  df-xmul 12192  df-ioo 12425  df-ioc 12426  df-ico 12427  df-icc 12428  df-fz 12578  df-fzo 12718  df-fl 12845  df-mod 12921  df-seq 13053  df-exp 13112  df-fac 13311  df-bc 13340  df-hash 13368  df-shft 14145  df-cj 14177  df-re 14178  df-im 14179  df-sqrt 14313  df-abs 14314  df-limsup 14540  df-clim 14557  df-rlim 14558  df-sum 14755  df-ef 15131  df-sin 15133  df-cos 15134  df-tan 15135  df-pi 15136  df-struct 16183  df-ndx 16184  df-slot 16185  df-base 16187  df-sets 16188  df-ress 16189  df-plusg 16277  df-mulr 16278  df-starv 16279  df-sca 16280  df-vsca 16281  df-ip 16282  df-tset 16283  df-ple 16284  df-ds 16286  df-unif 16287  df-hom 16288  df-cco 16289  df-rest 16395  df-topn 16396  df-0g 16414  df-gsum 16415  df-topgen 16416  df-pt 16417  df-prds 16420  df-xrs 16474  df-qtop 16479  df-imas 16480  df-xps 16482  df-mre 16558  df-mrc 16559  df-acs 16561  df-mgm 17554  df-sgrp 17596  df-mnd 17607  df-submnd 17648  df-mulg 17854  df-cntz 18059  df-cmn 18507  df-psmet 20057  df-xmet 20058  df-met 20059  df-bl 20060  df-mopn 20061  df-fbas 20062  df-fg 20063  df-cnfld 20066  df-top 21024  df-topon 21041  df-topsp 21063  df-bases 21076  df-cld 21149  df-ntr 21150  df-cls 21151  df-nei 21228  df-lp 21266  df-perf 21267  df-cn 21357  df-cnp 21358  df-haus 21445  df-cmp 21516  df-tx 21691  df-hmeo 21884  df-fil 21975  df-fm 22067  df-flim 22068  df-flf 22069  df-xms 22450  df-ms 22451  df-tms 22452  df-cncf 23006  df-limc 23968  df-dv 23969  df-log 24641  df-cxp 24642  df-asin 24941
This theorem is referenced by:  dvacos  33978  dvreasin  33979
  Copyright terms: Public domain W3C validator